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_LILY_PATTERNS ,   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 ,   spot::gen::LTLF_CHOMP_MEALY , spot::gen::LTLF_TV_COUNTER_MEALY , spot::gen::LTLF_TV_DOUBLE_COUNTERS_MEALY , spot::gen::LTLF_TV_NIM_MEALY ,   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
const char *	spot::gen::ltl_pattern_name (ltl_pattern_id pattern)
	convert an ltl_pattern_id value into a name
int	spot::gen::ltl_pattern_max (ltl_pattern_id pattern)
	upper bound for LTL patterns
int	spot::gen::ltl_pattern_argc (ltl_pattern_id pattern)
	argument count for LTL patterns

Detailed Description

Enumeration Type Documentation

ltl_pattern_id

enum spot::gen::ltl_pattern_id

#include <spot/gen/formulas.hh>

Identifiers for formula patterns.

Enumerator
LTL_AND_F	F(p1)&F(p2)&...&F(pn) [30]
LTL_AND_FG	FG(p1)&FG(p2)&...&FG(pn)
LTL_AND_GF	GF(p1)&GF(p2)&...&GF(pn) [10] , [30] .
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. [22]
LTL_EH_PATTERNS	12 formulas from Etessami and Holzmann. [25]
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})) [30]
LTL_GH_R	(GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1})) [30]
LTL_GO_THETA	!((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r))) [29]
LTL_GXF_AND	G(p0 & XF(p1 & XF(p2 & ... XF(pn))))
LTL_HKRSS_PATTERNS	55 patterns from the Liberouter project. [32]
LTL_KR_N	Linear formula with doubly exponential DBA. [37]
LTL_KR_NLOGN	Quasilinear formula with doubly exponential DBA. [37]
LTL_KV_PSI	Quadratic formula with doubly exponential DBA. [37] , [39] .
LTL_LILY_PATTERNS	LTL synthesis examples specification from the Lily 1.0.2 distribution. [jobstmann.06.fmcad]
LTL_MS_EXAMPLE	GF(a1&X(a2&X(a3&...Xan)))&F(b1&F(b2&F(b3&...&Xbm))) [45]
LTL_MS_PHI_H	FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|... [45]
LTL_MS_PHI_R	(FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...)) [45]
LTL_MS_PHI_S	(FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...)) [45]
LTL_OR_FG	FG(p1)|FG(p2)|...|FG(pn) [10]
LTL_OR_G	G(p1)|G(p2)|...|G(pn) [30]
LTL_OR_GF	GF(p1)|GF(p2)|...|GF(pn) [30]
LTL_P_PATTERNS	20 formulas from BEEM. [46]
LTL_PPS_ARBITER_STANDARD	Arbiter for n clients sending requests, and receiving grants. [48] using standard semantics from [35] .
LTL_PPS_ARBITER_STRICT	Arbiter for n clients sending requests, and receiving grants. [48] using strict semantics from [35] .
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 [52]
LTL_RV_COUNTER_CARRY	n-bit counter with carry [52]
LTL_RV_COUNTER_CARRY_LINEAR	linear-size formular for an n-bit counter with carry [52]
LTL_RV_COUNTER_LINEAR	linear-size formular for an n-bit counter [52]
LTL_SB_PATTERNS	27 formulas from Somenzi and Bloem [56]
LTL_SEJK_F	f(0,j)=(GFa0 U X^j(b)), f(i,j)=(GFai U G(f(i-1,j))) [55]
LTL_SEJK_J	(GFa1&...&GFan) -> (GFb1&...&GFbn) [55]
LTL_SEJK_K	(GFa1|FGb1)&...&(GFan|FGbn) [55]
LTL_SEJK_PATTERNS	3 formulas from Sikert et al. [55]
LTL_TV_F1	G(p -> (q | Xq | ... | XX...Xq) [58]
LTL_TV_F2	G(p -> (q | X(q | X(... | Xq))) [58]
LTL_TV_G1	G(p -> (q & Xq & ... & XX...Xq) [58]
LTL_TV_G2	G(p -> (q & X(q & X(... & Xq))) [58]
LTL_TV_UU	G(p1 -> (p1 U (p2 & (p2 U (p3 & (p3 U ...)))))) [58]
LTL_U_LEFT	(((p1 U p2) U p3) ... U pn) [30]
LTL_U_RIGHT	(p1 U (p2 U (... U pn))) [30] , [29] .
LTLF_CHOMP_MEALY	Chomp game specified in LTLf with Mealy semantics.
LTLF_TV_COUNTER_MEALY	Single Counter LTLf with Mealy semantics [57]
LTLF_TV_DOUBLE_COUNTERS_MEALY	Double Counters LTLf with Mealy semantics [57]
LTLF_TV_NIM_MEALY	Nim game specified in LTLf with Mealy semantics [57]

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.