Class: ADSL::DS::DSAssignment

Inherits:
DSNode show all
Defined in:
lib/adsl/ds/data_store_spec.rb,
lib/adsl/spass/spass_ds_extensions.rb

Instance Method Summary collapse

Methods inherited from DSNode

#list_entity_classes_read, #list_entity_classes_written_to, #replace, #replace_var

Instance Method Details

#migrate_state_spass(translation) ⇒ Object 



634
635
636
637
638
639
640
641
642
643
644
645
 
# 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) ⇒ Object 



629
630
631
632
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 629

def prepare(translation)
  @var.define_predicate translation
  @objset.prepare_action translation
end