class ADSL::DS::DSForEach
Public Instance Methods
create_iteration_formulae(translation)
click to toggle source
# 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
prepare(translation)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 519 def prepare(translation) prepare_with_context(translation, false) end