class ADSL::DS::DSCreateObj
Attributes
context[R]
context_creation_link[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