class ADSL::DS::DSFlatForEach
Public Instance Methods
create_iteration_formulae(translation)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 579 def create_iteration_formulae(translation) context = translation.context translation.reserve_names context.p_names, :o, :c1, :c2 do |ps, o, c1, c2| ps_without_last = ps.first(ps.length - 1) translation.create_formula _for_all(ps, o, _implies( @context.type_pred(ps), _equiv(@pre_state[ps_without_last, o], @pre_iteration_state[ps, o]) )) translation.create_formula _for_all(ps_without_last, o, _if_then_else( _not(_exists(ps.last, @context.type_pred(ps))), _equiv(@pre_state[ps_without_last, o], @post_state[ps_without_last, o]), _implies( @context.parent.type_pred(ps_without_last), _equiv( @post_state[ps_without_last, o], _or( _and( @pre_state[ps_without_last, o], _for_all(ps.last, _implies( @context.type_pred(ps), @post_iteration_state[ps, o] )) ), _and( _not(@pre_state[ps_without_last, o]), _exists(ps.last, @post_iteration_state[ps, o]) ) ) ) ) )) end end
prepare(translation)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 575 def prepare(translation) prepare_with_context(translation, true) end