spot 2.12.2
|
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... | |
#include <spot/gen/formulas.hh>
Identifiers for formula patterns.
Enumerator | |
---|---|
LTL_AND_F |
|
LTL_AND_FG |
|
LTL_AND_GF | |
LTL_CCJ_ALPHA |
|
LTL_CCJ_BETA |
|
LTL_CCJ_BETA_PRIME |
|
LTL_DAC_PATTERNS | 55 specification patterns from Dwyer et al. [19] |
LTL_EH_PATTERNS | 12 formulas from Etessami and Holzmann. [21] |
LTL_EIL_GSI | Familly sent by Edmond Irani Liu. |
LTL_FXG_OR |
|
LTL_GF_EQUIV |
|
LTL_GF_EQUIV_XN |
|
LTL_GF_IMPLIES |
|
LTL_GF_IMPLIES_XN |
|
LTL_GH_Q |
|
LTL_GH_R |
|
LTL_GO_THETA |
|
LTL_GXF_AND |
|
LTL_HKRSS_PATTERNS | 55 patterns from the Liberouter project. [29] |
LTL_KR_N | Linear formula with doubly exponential DBA. [34] |
LTL_KR_NLOGN | Quasilinear formula with doubly exponential DBA. [34] |
LTL_KV_PSI | Quadratic formula with doubly exponential DBA. [34] , [36] . |
LTL_MS_EXAMPLE |
|
LTL_MS_PHI_H |
|
LTL_MS_PHI_R |
|
LTL_MS_PHI_S |
|
LTL_OR_FG |
|
LTL_OR_G |
|
LTL_OR_GF |
|
LTL_P_PATTERNS | 20 formulas from BEEM. [43] |
LTL_PPS_ARBITER_STANDARD | Arbiter for n clients sending requests, and receiving grants. [45] using standard semantics from [32] . |
LTL_PPS_ARBITER_STRICT | Arbiter for n clients sending requests, and receiving grants. [45] using strict semantics from [32] . |
LTL_R_LEFT |
|
LTL_R_RIGHT |
|
LTL_RV_COUNTER | n-bit counter [49] |
LTL_RV_COUNTER_CARRY | n-bit counter with carry [49] |
LTL_RV_COUNTER_CARRY_LINEAR | linear-size formular for an n-bit counter with carry [49] |
LTL_RV_COUNTER_LINEAR | linear-size formular for an n-bit counter [49] |
LTL_SB_PATTERNS | 27 formulas from Somenzi and Bloem [53] |
LTL_SEJK_F |
|
LTL_SEJK_J |
|
LTL_SEJK_K |
|
LTL_SEJK_PATTERNS | 3 formulas from Sikert et al. [52] |
LTL_TV_F1 |
|
LTL_TV_F2 |
|
LTL_TV_G1 |
|
LTL_TV_G2 |
|
LTL_TV_UU |
|
LTL_U_LEFT |
|
LTL_U_RIGHT |
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.
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.
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.
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.