Method: ADSL::DS::DSForEach#create_iteration_formulae

Defined in:

lib/adsl/spass/spass_ds_extensions.rb

#create_iteration_formulae(translation) ⇒ Object

# File 'lib/adsl/spass/spass_ds_extensions.rb', line 523

def create_iteration_formulae(translation)
  raise "Not implemented for flexible arities"
  translation.create_formula _if_then_else_eq(
    _exists(:c, :o, _and(old_state[:c, :o], @objset.resolve_action_objset(translation, :c, :o))),
    _for_all(:parent, :c, :o, _implies(@context.parent_of_link[:parent, :c], _and(
      _if_then_else(
        @context.first[:parent, :c],
        _equiv(old_state[:parent, :o], @pre_iteration_state[:c, :o]),
        _for_all(:prev, _implies(
          @context.just_before[:prev, :c],
          _equiv(@post_iteration_state[:prev, :o], @pre_iteration_state[:c, :o])
        ))
      ),
      _implies(
        @context.last[:parent, :c],
        _equiv(@post_state[:parent, :o], @post_iteration_state[:c, :o])
      )
    ))),
    _for_all(:c, :o, _equiv(@pre_state[:c, :o], @post_state[:c, :o]))
  )
end