class ADSL::DS::DSAction
Public Instance Methods
prepare(translation)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 117 def prepare(translation) @args.each do |arg| arg.define_predicate translation end @block.prepare translation end
statements()
click to toggle source
# File lib/adsl/ds/data_store_spec.rb, line 98 def statements @block.statements end
translate(translation)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 124 def translate(translation) translation.context = translation.root_context @args.length.times do |i| cardinality = @cardinalities[i] arg = @args[i] translation.create_formula _for_all(:o, _implies( arg[:o], _and(translation.existed_initially[:o], arg.type[:o]) )) translation.create_formula _exists(:o, arg[:o]) if cardinality[0] > 0 if cardinality[1] == 1 translation.create_formula _for_all(:o1, :o2, _implies( _and(arg[:o1], arg[:o2]), _equal(:o1, :o2) )) end end @block.migrate_state_spass translation translation.create_formula _for_all(:o, _equiv( translation.exists_finally[:o], translation.prev_state[:o] )) end