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