Class: PgVerify::Interpret::LTLBuilder::LTLBuilderAfter

Inherits:
LTLBuilderBase
  • Object
show all
Defined in:
lib/pg-verify/interpret/spec/ltl_builder.rb

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods inherited from LTLBuilderBase

#build

Constructor Details

#initialize(q) ⇒ LTLBuilderAfter

Returns a new instance of LTLBuilderAfter.



49
 
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 49

def initialize(q); @q = q end

Instance Attribute Details

#q ⇒ Object

Returns the value of attribute q.



48
49
50
 
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 48

def q
  @q
end

Instance Method Details

#exists(p) ⇒ Object 



56
57
58
 
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 56

def exists(p)
     build "( G !(q) ) || ( F ( q && F p ) )", { p: p, q: q }
end

#global(p) ⇒ Object 



50
51
52
 
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 50

def global(p)
     build "G ( q -> G p )", { p: p, q: q }
end

#never(p) ⇒ Object 



53
54
55
 
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 53

def never(p) 
    build "G ( q -> G !(p))", { p: p, q: q }
end

#precedes(p, s) ⇒ Object 



62
63
64
 
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 62

def precedes(p, s)
    build "G !(q) || F ( q && !(p) W s )", { p: p, q: q, s: s} 
end

#reacts(p, s) ⇒ Object 



59
60
61
 
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 59

def reacts(p, s)
    build "G ( q => G (p => F s) )", { p: p, q: q, s: s} 
end