class ADSL::DS::DSForEachCommon
Attributes
context[R]
post_iteration_state[R]
post_state[R]
pre_iteration_state[R]
pre_state[R]
Public Instance Methods
migrate_state_spass(translation)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 484 def migrate_state_spass(translation) return if @objset.type.nil? @pre_state = translation.prev_state @post_state = translation.create_state :post_for_each translation.reserve_names @context.parent.p_names, :o do |ps, o| translation.create_formula _for_all(ps, o, _equiv( _and(@objset.resolve_action_objset(translation, ps, o), @pre_state[ps, o]), @context.type_pred(ps, o) )) end translation.context = @context @pre_iteration_state = translation.create_state :pre_iteration @post_iteration_state = translation.create_state :post_iteration translation.prev_state = @pre_iteration_state @block.migrate_state_spass translation translation.reserve_names @context.p_names, :o do |ps, o| translation.create_formula _for_all(ps, o, _equiv( translation.prev_state[ps, o], @post_iteration_state[ps, o] )) end create_iteration_formulae translation translation.context = @context.parent translation.prev_state = post_state end
prepare_with_context(translation, flat_context)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 476 def prepare_with_context(translation, flat_context) @context = translation.create_context "for_each_context", flat_context, translation.context @objset.prepare_action translation translation.context = @context @block.prepare translation translation.context = @context.parent end