class ADSL::DS::DSAssignment

Public Instance Methods

migrate_state_spass(translation) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 634
def migrate_state_spass(translation)
  context = translation.context
  translation.reserve_names context.p_names, :o do |ps, o|
    translation.create_formula FOL::ForAll.new(ps, o, FOL::Equiv.new(
      var.resolve_action_objset(translation, ps, o),
      FOL::And.new(
        translation.prev_state[ps, o],
        objset.resolve_action_objset(translation, ps, o)
      )
    ))
  end
end
prepare(translation) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 629
def prepare(translation)
  @var.define_predicate translation
  @objset.prepare_action translation
end