Class: ADSL::DS::DSFlatForEach

Inherits:
DSForEachCommon show all
Defined in:
lib/adsl/ds/data_store_spec.rb,
lib/adsl/spass/spass_ds_extensions.rb

Instance Attribute Summary

Attributes inherited from DSForEachCommon

#context, #post_iteration_state, #post_state, #pre_iteration_state, #pre_state

Instance Method Summary collapse

Methods inherited from DSForEachCommon

#migrate_state_spass, #prepare_with_context

Methods inherited from DSNode

#list_entity_classes_read, #list_entity_classes_written_to, #replace, #replace_var

Instance Method Details

#create_iteration_formulae(translation) ⇒ Object 



579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
 
# 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) ⇒ Object 



575
576
577
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 575

def prepare(translation)
  prepare_with_context(translation, true)
end