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