genltl: typos and shorter descriptions
* bin/genltl.cc: Shorten the descriptions of the three new LTL families. * NEWS: Mention those.
This commit is contained in:
parent
16e71b5093
commit
a14abf27fb
2 changed files with 8 additions and 3 deletions
5
NEWS
5
NEWS
|
|
@ -12,6 +12,11 @@ New in spot 2.3.0.dev (not yet released)
|
|||
- The option (y) has been added to --dot. It splits the universal
|
||||
edges with the same targets but different colors.
|
||||
|
||||
- genltl learnt three new families for formulas: --kr-n2=RANGE,
|
||||
--kr-nlogn=RANGE, and --kr-n=RANGE. These formulas, from
|
||||
Kupferman & Rosenberg [MoChArt'10] are recognizable by
|
||||
deterministic Büchi automata with at least 2^2^n states.
|
||||
|
||||
Library:
|
||||
|
||||
- spot::twa_run::as_twa() has an option to preserve state names.
|
||||
|
|
|
|||
|
|
@ -260,11 +260,11 @@ static const argp_option options[] =
|
|||
{ "go-theta", OPT_GO_THETA, "RANGE", 0,
|
||||
"!((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r)))", 0 },
|
||||
{ "kr-n", OPT_KR_N, "RANGE", 0,
|
||||
"formula of linear size with doubly exponential DBA", 0 },
|
||||
"linear formula with doubly exponential DBA", 0 },
|
||||
{ "kr-nlogn", OPT_KR_NLOGN, "RANGE", 0,
|
||||
"forumla of n log n size with doubly exponential DBA", 0 },
|
||||
"quasilinear formula with doubly exponential DBA", 0 },
|
||||
{ "kv-phi", OPT_KV_PHI, "RANGE", 0,
|
||||
"forumla of quadratic size with doubly exponential DBA", 0 },
|
||||
"quadratic formula with doubly exponential DBA", 0 },
|
||||
OPT_ALIAS(kr-n2),
|
||||
{ "or-fg", OPT_OR_FG, "RANGE", 0, "FG(p1)|FG(p2)|...|FG(pn)", 0 },
|
||||
OPT_ALIAS(ccj-xi),
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue