Class: PgVerify::Interpret::LTLBuilder::LTLBuilderBefore

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) ⇒ LTLBuilderBefore

Returns a new instance of LTLBuilderBefore.



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

def initialize(q); @q = q end

Instance Attribute Details

#qObject

Returns the value of attribute q.



68
69
70
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 68

def q
  @q
end

Instance Method Details

#exists(p) ⇒ Object



76
77
78
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 76

def exists(p)
     
end

#global(p) ⇒ Object



70
71
72
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 70

def global(p)
    
end

#never(p) ⇒ Object



73
74
75
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 73

def never(p) 
    build "( F q ) => ( !(p) U q )", { p: p, q: q }
end

#precedes(p, s) ⇒ Object



82
83
84
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 82

def precedes(p, s)
    
end

#reacts(p, s) ⇒ Object



79
80
81
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 79

def reacts(p, s)
    
end