class ADSL::Spass::SpassTranslator::ChainedContext
Attributes
before_pred[RW]
first[RW]
just_before[RW]
last[RW]
Public Class Methods
new(translation, name, parent)
click to toggle source
Calls superclass method
ADSL::Spass::SpassTranslator::ContextCommon::new
# File lib/adsl/spass/spass_translator.rb, line 136 def initialize(translation, name, parent) super @before_pred = translation.create_predicate "#{@type_pred.name}_before", @type_pred.arity + 1 @just_before = translation.create_predicate "#{@type_pred.name}_just_before", @type_pred.arity + 1 @first = translation.create_predicate "#{@type_pred.name}_first", @type_pred.arity @last = translation.create_predicate "#{@type_pred.name}_last", @type_pred.arity ps = [] (@type_pred.arity-1).times{ |i| ps << "p#{i}" } translation.create_formula _for_all(ps, :c, _not(@before_pred[ps, :c, :c])) translation.create_formula _for_all(ps, :c1, :c2, _implies(@before_pred[ps, :c1, :c2], _and( @type_pred[ps, :c1], @type_pred[ps, :c2], _not(@before_pred[ps, :c2, :c1]), _implies( _and(@type_pred[ps, :c1], @type_pred[ps, :c2]), _or(_equal(:c1, :c2), @before_pred[ps, :c1, :c2], @before_pred[ps, :c2, :c1]) ) ))) translation.create_formula _for_all(ps, :c1, :c2, :c3, _implies( _and(@before_pred[ps, :c1, :c2], @before_pred[ps, :c2, :c3]), @before_pred[ps, :c1, :c3] )) translation.create_formula _for_all(ps, :c1, :c2, _equiv( @just_before[ps, :c1, :c2], _and( @before_pred[ps, :c1, :c2], _not(_exists(:mid, _and(@before_pred[ps, :c1, :mid], @before_pred[ps, :mid, :c2]))) ) )) translation.create_formula _for_all(ps, _and( _equiv( _exists(:c, @type_pred[ps, :c]), _exists(:c, @first[ps, :c]), _exists(:c, @last[ps, :c]) ), _for_all(ps, :c, _implies( @type_pred[ps, :c], _one_of(@last[ps, :c], _exists(:next, @just_before[ps, :c, :next])) )), _for_all(ps, :c, _equiv(@first[ps, :c], _and(@type_pred[ps, :c], _not(_exists(:pre, @before_pred[ps, :pre, :c]))) )), _for_all(ps, :c, _equiv(@last[ps, :c], _and(@type_pred[ps, :c], _not(_exists(:post, @before_pred[ps, :c, :post]))) )) )) end
Public Instance Methods
same_level_before_formula(ps, c1, c2)
click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 186 def same_level_before_formula(ps, c1, c2) @before_pred[ps, c1, c2] end