From a14abf27fb293a979bb1726cf7a58bbdafb5e5fa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 17 Feb 2017 17:45:11 +0100 Subject: [PATCH] genltl: typos and shorter descriptions * bin/genltl.cc: Shorten the descriptions of the three new LTL families. * NEWS: Mention those. --- NEWS | 5 +++++ bin/genltl.cc | 6 +++--- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index d0e7d7e1b..8dffadaf2 100644 --- a/NEWS +++ b/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. diff --git a/bin/genltl.cc b/bin/genltl.cc index 264e232a1..e4bb1f7c2 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -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),