Class: ADSL::DS::DSForEach

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 



523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
 
# 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) ⇒ Object 



519
520
521
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 519

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