354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
|
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 354
def migrate_state_spass(translation)
return if @objset1.type.nil? or @objset2.type.nil?
state = translation.create_state "post_deleteref_#{@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::Equiv.new(
state[ps, r],
FOL::And.new(
prev_state[ps, r],
FOL::ForAll.new(o1, o2, FOL::Not.new(FOL::And.new(
objset1, objset2,
prev_state[ps, o1], prev_state[ps, o2],
@relation.left_link[r, o1], @relation.right_link[r, o2]
)))
)
))
end
translation.prev_state = state
end
|