class ADSL::DS::DSCreateObj

Attributes

context[R]

Public Instance Methods

entity_class_writes() click to toggle source
# File lib/adsl/ds/data_store_spec.rb, line 114
def entity_class_writes
  Set[@klass]
end
migrate_state_spass(translation) click to toggle source
# 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) click to toggle source
# 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