Class: ADSL::DS::DSAction

Inherits:
DSNode show all
Includes:
FOL
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

#prepare(translation) ⇒ Object 



117
118
119
120
121
122
 
# 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 ⇒ Object 



98
99
100
 
# File 'lib/adsl/ds/data_store_spec.rb', line 98

def statements
  @block.statements
end

#translate(translation) ⇒ Object 



124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
 
# 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