spot  2.11.6
Enumerations | Functions
Hard-coded families of formulas.

Enumerations

enum  spot::gen::ltl_pattern_id {
  LTL_BEGIN = 256 , spot::gen::LTL_AND_F = LTL_BEGIN , spot::gen::LTL_AND_FG , spot::gen::LTL_AND_GF ,
  spot::gen::LTL_CCJ_ALPHA , spot::gen::LTL_CCJ_BETA , spot::gen::LTL_CCJ_BETA_PRIME , spot::gen::LTL_DAC_PATTERNS ,
  spot::gen::LTL_EH_PATTERNS , spot::gen::LTL_EIL_GSI , spot::gen::LTL_FXG_OR , spot::gen::LTL_GF_EQUIV ,
  spot::gen::LTL_GF_EQUIV_XN , spot::gen::LTL_GF_IMPLIES , spot::gen::LTL_GF_IMPLIES_XN , spot::gen::LTL_GH_Q ,
  spot::gen::LTL_GH_R , spot::gen::LTL_GO_THETA , spot::gen::LTL_GXF_AND , spot::gen::LTL_HKRSS_PATTERNS ,
  spot::gen::LTL_KR_N , spot::gen::LTL_KR_NLOGN , spot::gen::LTL_KV_PSI , spot::gen::LTL_MS_EXAMPLE ,
  spot::gen::LTL_MS_PHI_H , spot::gen::LTL_MS_PHI_R , spot::gen::LTL_MS_PHI_S , spot::gen::LTL_OR_FG ,
  spot::gen::LTL_OR_G , spot::gen::LTL_OR_GF , spot::gen::LTL_P_PATTERNS , spot::gen::LTL_PPS_ARBITER_STANDARD ,
  spot::gen::LTL_PPS_ARBITER_STRICT , spot::gen::LTL_R_LEFT , spot::gen::LTL_R_RIGHT , spot::gen::LTL_RV_COUNTER ,
  spot::gen::LTL_RV_COUNTER_CARRY , spot::gen::LTL_RV_COUNTER_CARRY_LINEAR , spot::gen::LTL_RV_COUNTER_LINEAR , spot::gen::LTL_SB_PATTERNS ,
  spot::gen::LTL_SEJK_F , spot::gen::LTL_SEJK_J , spot::gen::LTL_SEJK_K , spot::gen::LTL_SEJK_PATTERNS ,
  spot::gen::LTL_TV_F1 , spot::gen::LTL_TV_F2 , spot::gen::LTL_TV_G1 , spot::gen::LTL_TV_G2 ,
  spot::gen::LTL_TV_UU , spot::gen::LTL_U_LEFT , spot::gen::LTL_U_RIGHT , LTL_END
}
 Identifiers for formula patterns. More...
 

Functions

formula spot::gen::ltl_pattern (ltl_pattern_id pattern, int n, int m=-1)
 generate an LTL from a known pattern More...
 
const char * spot::gen::ltl_pattern_name (ltl_pattern_id pattern)
 convert an ltl_pattern_id value into a name More...
 
int spot::gen::ltl_pattern_max (ltl_pattern_id pattern)
 upper bound for LTL patterns More...
 
int spot::gen::ltl_pattern_argc (ltl_pattern_id pattern)
 argument count for LTL patterns More...
 

Detailed Description

Enumeration Type Documentation

◆ ltl_pattern_id

#include <spot/gen/formulas.hh>

Identifiers for formula patterns.

Enumerator
LTL_AND_F 

F(p1)&F(p2)&...&F(pn) [24]

LTL_AND_FG 

FG(p1)&FG(p2)&...&FG(pn)

LTL_AND_GF 

GF(p1)&GF(p2)&...&GF(pn) [10] , [24] .

LTL_CCJ_ALPHA 

F(p1&F(p2&F(p3&...F(pn)))) & F(q1&F(q2&F(q3&...F(qn)))) [10]

LTL_CCJ_BETA 

F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q)))) [10]

LTL_CCJ_BETA_PRIME 

F(p&(Xp)&(XXp)&...(X...X(p))) & F(q&(Xq)&(XXq)&...(X...X(q))) [10]

LTL_DAC_PATTERNS 

55 specification patterns from Dwyer et al. [18]

LTL_EH_PATTERNS 

12 formulas from Etessami and Holzmann. [19]

LTL_EIL_GSI 

Familly sent by Edmond Irani Liu.

LTL_FXG_OR 

F(p0 | XG(p1 | XG(p2 | ... XG(pn))))

LTL_GF_EQUIV 

(GFa1 & GFa2 & ... & GFan) <-> GFz

LTL_GF_EQUIV_XN 

GF(a <-> X[n](a))

LTL_GF_IMPLIES 

(GFa1 & GFa2 & ... & GFan) -> GFz

LTL_GF_IMPLIES_XN 

GF(a -> X[n](a))

LTL_GH_Q 

(F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1})) [24]

LTL_GH_R 

(GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1})) [24]

LTL_GO_THETA 

!((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r))) [23]

LTL_GXF_AND 

G(p0 & XF(p1 & XF(p2 & ... XF(pn))))

LTL_HKRSS_PATTERNS 

55 patterns from the Liberouter project. [27]

LTL_KR_N 

Linear formula with doubly exponential DBA. [32]

LTL_KR_NLOGN 

Quasilinear formula with doubly exponential DBA. [32]

LTL_KV_PSI 

Quadratic formula with doubly exponential DBA. [32] , [34] .

LTL_MS_EXAMPLE 

GF(a1&X(a2&X(a3&...Xan)))&F(b1&F(b2&F(b3&...&Xbm))) [40]

LTL_MS_PHI_H 

FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|... [40]

LTL_MS_PHI_R 

(FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...)) [40]

LTL_MS_PHI_S 

(FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...)) [40]

LTL_OR_FG 

FG(p1)|FG(p2)|...|FG(pn) [10]

LTL_OR_G 

G(p1)|G(p2)|...|G(pn) [24]

LTL_OR_GF 

GF(p1)|GF(p2)|...|GF(pn) [24]

LTL_P_PATTERNS 

20 formulas from BEEM. [41]

LTL_PPS_ARBITER_STANDARD 

Arbiter for n clients sending requests, and receiving grants. [43] using standard semantics from [30] .

LTL_PPS_ARBITER_STRICT 

Arbiter for n clients sending requests, and receiving grants. [43] using strict semantics from [30] .

LTL_R_LEFT 

(((p1 R p2) R p3) ... R pn)

LTL_R_RIGHT 

(p1 R (p2 R (... R pn)))

LTL_RV_COUNTER 

n-bit counter [47]

LTL_RV_COUNTER_CARRY 

n-bit counter with carry [47]

LTL_RV_COUNTER_CARRY_LINEAR 

linear-size formular for an n-bit counter with carry [47]

LTL_RV_COUNTER_LINEAR 

linear-size formular for an n-bit counter [47]

LTL_SB_PATTERNS 

27 formulas from Somenzi and Bloem [51]

LTL_SEJK_F 

f(0,j)=(GFa0 U X^j(b)), f(i,j)=(GFai U G(f(i-1,j))) [50]

LTL_SEJK_J 

(GFa1&...&GFan) -> (GFb1&...&GFbn) [50]

LTL_SEJK_K 

(GFa1|FGb1)&...&(GFan|FGbn) [50]

LTL_SEJK_PATTERNS 

3 formulas from Sikert et al. [50]

LTL_TV_F1 

G(p -> (q | Xq | ... | XX...Xq) [52]

LTL_TV_F2 

G(p -> (q | X(q | X(... | Xq))) [52]

LTL_TV_G1 

G(p -> (q & Xq & ... & XX...Xq) [52]

LTL_TV_G2 

G(p -> (q & X(q & X(... & Xq))) [52]

LTL_TV_UU 

G(p1 -> (p1 U (p2 & (p2 U (p3 & (p3 U ...)))))) [52]

LTL_U_LEFT 

(((p1 U p2) U p3) ... U pn) [24]

LTL_U_RIGHT 

(p1 U (p2 U (... U pn))) [24] , [23] .

Function Documentation

◆ ltl_pattern()

formula spot::gen::ltl_pattern ( ltl_pattern_id  pattern,
int  n,
int  m = -1 
)

#include <spot/gen/formulas.hh>

generate an LTL from a known pattern

The pattern is specified using one value from the ltl_pattern_id enum. See the man page of the genltl binary for a description of those patterns, and bibliographic references.

◆ ltl_pattern_argc()

int spot::gen::ltl_pattern_argc ( ltl_pattern_id  pattern)

#include <spot/gen/formulas.hh>

argument count for LTL patterns

Return the number of arguments expected by an LTL pattern.

◆ ltl_pattern_max()

int spot::gen::ltl_pattern_max ( ltl_pattern_id  pattern)

#include <spot/gen/formulas.hh>

upper bound for LTL patterns

If an LTL pattern has an upper bound, this returns it. Otherwise, this returns 0.

◆ ltl_pattern_name()

const char* spot::gen::ltl_pattern_name ( ltl_pattern_id  pattern)

#include <spot/gen/formulas.hh>

convert an ltl_pattern_id value into a name

The returned name is suitable to be used as an option key for the genltl binary.


Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1