Class: ADSL::DS::DSCreateObj

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

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods inherited from DSNode

#list_entity_classes_read, #list_entity_classes_written_to, #replace, #replace_var

Instance Attribute Details

#context ⇒ Object (readonly)

Returns the value of attribute context.



207
208
209
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 207

def context
  @context
end

#context_creation_link ⇒ Object (readonly)

Returns the value of attribute context_creation_link.



207
208
209
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 207

def context_creation_link
  @context_creation_link
end

Instance Method Details

#entity_class_writes ⇒ Object 



114
115
116
 
# File 'lib/adsl/ds/data_store_spec.rb', line 114

def entity_class_writes
  Set[@klass]
end

#migrate_state_spass(translation) ⇒ Object 



215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 215

def migrate_state_spass(translation)
  state = translation.create_state "post_create_#{@klass.name}"
  prev_state = translation.prev_state
  translation.gen_formula_for_unique_arg(@context_creation_link, (0..@context.level-1), @context.level)
  translation.reserve_names @context.p_names, :o do |ps, o|
    created_by_other_create_stmts = translation.create_obj_stmts[@klass].select{|s| s != self}.map do |stmt|
      formula = nil
      translation.reserve_names stmt.context.p_names do |other_ps|
        formula = _exists(other_ps, stmt.context_creation_link[other_ps, o])
      end
      formula
    end
    created_by_other_create_stmts << translation.existed_initially[o]
    child_classes = translation.classes.select{ |c| c.parent == @klass }
    not_of_child_types = child_classes.empty? ? true : _and(child_classes.map{ |c| _not(c[o]) })
    translation.create_formula _for_all(ps, o, _implies(
      @context_creation_link[ps, o], _and(
        context.type_pred(ps),
        _not(created_by_other_create_stmts),
        @klass[o],
        not_of_child_types
      )
    ))
    translation.create_formula _for_all(ps, _implies(@context.type_pred(ps), _exists(o,
      @context_creation_link[ps, o]
    )))
    translation.create_formula _for_all(ps, o,
      _if_then_else_eq(
        @context_creation_link[ps, o],
        _and(_not(prev_state[ps, o]), state[ps, o]),
        _equiv(prev_state[ps, o], state[ps, o])
      )
    )

    relevant_from_relations = translation.classes.map{ |c| c.relations }.flatten.select{ |r| r.from_class == @klass }
    relevant_to_relations = translation.classes.map{ |c| c.relations }.flatten.select{ |r| r.to_class == @klass }
    translation.reserve_names :r do |r|
      translation.create_formula _for_all(ps, o, _implies(
        @context_creation_link[ps, o],
        _for_all(r, _not(_and(
          state[ps, r],
          _or(
            relevant_from_relations.map{ |rel| rel.left_link[r, o] },
            relevant_to_relations.map{ |rel| rel.right_link[r, o] }
          )
        )))
      ))
    end
  end

  translation.prev_state = state
end

#prepare(translation) ⇒ Object 



209
210
211
212
213
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 209

def prepare(translation)
  @context = translation.context
  translation.create_obj_stmts[@klass] << self
  @context_creation_link = translation.create_predicate "created_#{@klass.name}_in_context", context.level + 1
end