Class: ADSL::DS::DSForEachCommon

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

Direct Known Subclasses

DSFlatForEach, DSForEach

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods inherited from DSNode

#list_entity_classes_read, #list_entity_classes_written_to, #replace, #replace_var

Instance Attribute Details

#context ⇒ Object (readonly)

Returns the value of attribute context.



474
475
476
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 474

def context
  @context
end

#post_iteration_state ⇒ Object (readonly)

Returns the value of attribute post_iteration_state.



474
475
476
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 474

def post_iteration_state
  @post_iteration_state
end

#post_state ⇒ Object (readonly)

Returns the value of attribute post_state.



474
475
476
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 474

def post_state
  @post_state
end

#pre_iteration_state ⇒ Object (readonly)

Returns the value of attribute pre_iteration_state.



474
475
476
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 474

def pre_iteration_state
  @pre_iteration_state
end

#pre_state ⇒ Object (readonly)

Returns the value of attribute pre_state.



474
475
476
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 474

def pre_state
  @pre_state
end

Instance Method Details

#migrate_state_spass(translation) ⇒ Object 



484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 484

def migrate_state_spass(translation)
  return if @objset.type.nil?

  @pre_state = translation.prev_state
  @post_state = translation.create_state :post_for_each
  
  translation.reserve_names @context.parent.p_names, :o do |ps, o|
    translation.create_formula _for_all(ps, o, _equiv(
      _and(@objset.resolve_action_objset(translation, ps, o), @pre_state[ps, o]),
      @context.type_pred(ps, o)
    ))
  end

  translation.context = @context
  
  @pre_iteration_state = translation.create_state :pre_iteration
  @post_iteration_state = translation.create_state :post_iteration
  
  translation.prev_state = @pre_iteration_state
  @block.migrate_state_spass translation
  
  translation.reserve_names @context.p_names, :o do |ps, o|
    translation.create_formula _for_all(ps, o, _equiv(
      translation.prev_state[ps, o],
      @post_iteration_state[ps, o]
    ))
  end

  create_iteration_formulae translation
  translation.context = @context.parent
  translation.prev_state = post_state
end

#prepare_with_context(translation, flat_context) ⇒ Object 



476
477
478
479
480
481
482
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 476

def prepare_with_context(translation, flat_context)
  @context = translation.create_context "for_each_context", flat_context, translation.context
  @objset.prepare_action translation
  translation.context = @context
  @block.prepare translation
  translation.context = @context.parent
end