Class: ADSL::DS::DSEither

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

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

#is_trues ⇒ Object (readonly)

Returns the value of attribute is_trues.



383
384
385
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 383

def is_trues
  @is_trues
end

#resolution_link ⇒ Object (readonly)

Returns the value of attribute resolution_link.



383
384
385
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 383

def resolution_link
  @resolution_link
end

Instance Method Details

#migrate_state_spass(translation) ⇒ Object 



404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 404

def migrate_state_spass(translation)
  post_state = translation.create_state :post_either
  prev_state = translation.prev_state
  context = translation.context

  pre_states = []
  post_states = []
  @blocks.length.times do |i|
    pre_states << translation.create_state(:pre_of_either)
  end
  translation.create_formula FOL::ForAll.new(:r, FOL::Implies.new(
    translation.is_either_resolution[:r],
    FOL::OneOf.new(is_trues.map{ |pred| pred[:r] })
  ))

  translation.reserve_names context.p_names, :resolution, :o do |ps, resolution, o|
    translation.create_formula FOL::ForAll.new(ps, FOL::Implies.new(
      translation.context.type_pred(ps),
      FOL::Exists.new(resolution, FOL::And.new(
        @resolution_link[ps, resolution],
        FOL::And.new((0..@blocks.length-1).map { |i|
          FOL::Equiv.new(is_trues[i][resolution], FOL::ForAll.new(o, FOL::Equiv.new(prev_state[ps, o], pre_states[i][ps, o])))
        })
      ))
    ))
  end

  @blocks.length.times do |i|
    translation.prev_state = pre_states[i]
    @blocks[i].migrate_state_spass translation
    post_states << translation.prev_state
  end
    
  translation.reserve_names context.p_names, :resolution, :o do |ps, resolution, o|
    translation.create_formula FOL::ForAll.new(ps, FOL::Implies.new(
      translation.context.type_pred(ps),
      FOL::Exists.new(resolution, FOL::And.new(
        @resolution_link[ps, resolution],
        FOL::And.new((0..@blocks.length-1).map { |i|
          FOL::Equiv.new(is_trues[i][resolution], FOL::ForAll.new(o, FOL::Equiv.new(post_state[ps, o], post_states[i][ps, o])))
        })
      ))
    ))
  end
  
  translation.prev_state = post_state
end

#prepare(translation) ⇒ Object 



385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
 
# File 'lib/adsl/spass/spass_ds_extensions.rb', line 385

def prepare(translation)
  context = translation.context
  @resolution_link = translation.create_predicate :resolution_link, context.level+1
  translation.reserve_names context.p_names, :r do |ps, r|
    translation.gen_formula_for_unique_arg(@resolution_link, (0..ps.length-1), ps.length)
    translation.create_formula _for_all(ps, r, _implies(@resolution_link[ps, r], _and(
      translation.context.type_pred(ps),
      translation.is_either_resolution[r]
    )))
  end
  @is_trues = []
  @blocks.length.times do |i|
    is_trues << translation.create_predicate("either_resolution_#{i}_is_true", 1)
  end
  @blocks.each do |block|
    block.prepare(translation)
  end
end