F(p0 | XG(p1 | XG(p2 | ... XG(pn))))
Definition: formulas.hh:60
Definition: formulas.hh:146
Definition: formulas.hh:161
Definition: automata.hh:26
Definition: formulas.hh:107
Definition: formulas.hh:152
(GFa1 & GFa2 & ... & GFan) <-> GFz
Definition: formulas.hh:62
Definition: formulas.hh:58
Definition: formulas.hh:46
Definition: formulas.hh:101
Definition: formulas.hh:155
int ltl_pattern_argc(ltl_pattern_id pattern)
argument count for LTL patterns
Definition: formulas.hh:167
Definition: formulas.hh:98
Definition: formulas.hh:137
Definition: formulas.hh:110
int ltl_pattern_max(ltl_pattern_id pattern)
upper bound for LTL patterns
formula ltl_pattern(ltl_pattern_id pattern, int n, int m=-1)
generate an LTL from a known pattern
Definition: formulas.hh:43
Definition: formulas.hh:92
Definition: formulas.hh:170
Definition: formulas.hh:85
GF(a <-> X[n](a))
Definition: formulas.hh:64
const char * ltl_pattern_name(ltl_pattern_id pattern)
convert an ltl_pattern_id value into a name
Definition: formulas.hh:158
Definition: formulas.hh:131
Definition: formulas.hh:52
Definition: formulas.hh:177
Definition: formulas.hh:71
Definition: formulas.hh:120
Definition: formulas.hh:149
GF(a -> X[n](a))
Definition: formulas.hh:68
Definition: formulas.hh:74
Definition: formulas.hh:88
Definition: formulas.hh:113
Definition: formulas.hh:37
Definition: formulas.hh:77
ltl_pattern_id
Identifiers for formula patterns.
Definition: formulas.hh:33
Definition: formulas.hh:55
Definition: formulas.hh:82
(((p1 R p2) R p3) ... R pn)
Definition: formulas.hh:126
Definition: formulas.hh:116
(p1 R (p2 R (... R pn)))
Definition: formulas.hh:128
Definition: formulas.hh:104
Definition: formulas.hh:140
G(p0 & XF(p1 & XF(p2 & ... XF(pn))))
Definition: formulas.hh:79
Definition: formulas.hh:134
Definition: formulas.hh:124
Definition: formulas.hh:49
Definition: formulas.hh:95
(GFa1 & GFa2 & ... & GFan) -> GFz
Definition: formulas.hh:66
Definition: formulas.hh:173
Definition: formulas.hh:164
Definition: formulas.hh:143
FG(p1)&FG(p2)&...&FG(pn)
Definition: formulas.hh:39