class ADSL::DS::DSCreateTup
Public Instance Methods
migrate_state_spass(translation)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 313 def migrate_state_spass(translation) return if @objset1.type.nil? or @objset2.type.nil? state = translation.create_state "post_create_#{@relation.from_class.name}_#{@relation.name}" prev_state = translation.prev_state context = translation.context translation.reserve_names context.p_names, :r, :o1, :o2 do |ps, r, o1, o2| objset1 = @objset1.resolve_action_objset(translation, ps, o1) objset2 = @objset2.resolve_action_objset(translation, ps, o2) translation.create_formula FOL::ForAll.new(ps, r, FOL::Implies.new( context.type_pred(ps), FOL::Equiv.new( state[ps, r], FOL::Or.new( prev_state[ps, r], FOL::Exists.new(o1, o2, FOL::And.new( prev_state[ps, o1], prev_state[ps, o2], @relation.left_link[r, o1], @relation.right_link[r, o2], objset1, objset2 )) ) ) )) translation.create_formula FOL::ForAll.new(ps, o1, o2, FOL::Implies.new( FOL::And.new(prev_state[ps, o1], prev_state[ps, o2], objset1, objset2), FOL::Exists.new(r, FOL::And.new(state[ps, r], @relation.left_link[r, o1], @relation.right_link[r, o2])) )) end translation.prev_state = state end
prepare(translation)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 308 def prepare(translation) @objset1.prepare_action translation @objset2.prepare_action translation end