Class: PgVerify::Interpret::LTLBuilder::LTLBuilderGlobally

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

Instance Method Summary collapse

Methods inherited from LTLBuilderBase

#build

Instance Method Details

#exists(p) ⇒ Object 



36
37
38
 
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 36

def exists(p)
    build "F p", { p: p }
end

#global(p) ⇒ Object 



30
31
32
 
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 30

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

#never(p) ⇒ Object 



33
34
35
 
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 33

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

#precedes(p, s) ⇒ Object 



42
43
44
 
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 42

def precedes(p, s)
    build "!(p) W s", { p: p, s: s }
end

#reacts(p, s) ⇒ Object 



39
40
41
 
# File 'lib/pg-verify/interpret/spec/ltl_builder.rb', line 39

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