diff --git a/NEWS b/NEWS index 45dda07fa..ab5cc9a9f 100644 --- a/NEWS +++ b/NEWS @@ -21,6 +21,13 @@ New in spot 2.3.5.dev (not yet released) transforming automata (in the same way as we have ltlcross for LTL translators). + - genltl learned two generate to new families of formulas: + --fxg-or=RANGE F(p0 | XG(p1 | XG(p2 | ... XG(pn)))) + --gxf-and=RANGE G(p0 & XF(p1 & XF(p2 & ... XF(pn)))) + The later is a generalization of --eh-pattern=9, for which a + single state TGBA always exists (but previous version of Spot + would build larger automata). + - autfilt learned to build the union (--sum) or the intersection (--sum-and) of two languages by putting two automata side-by-side and fiddling with the initial states. This complements the already diff --git a/bin/genltl.cc b/bin/genltl.cc index 2e4e32b6d..90ef4618b 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -84,12 +84,16 @@ static const argp_option options[] = { "eh-patterns", gen::LTL_EH_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL, "Etessami and Holzmann [Concur'00] patterns " "(range should be included in 1..12)", 0 }, + { "fxg-or", gen::LTL_FXG_OR, "RANGE", 0, + "F(p0 | XG(p1 | XG(p2 | ... XG(pn))))", 0}, { "gh-q", gen::LTL_GH_Q, "RANGE", 0, "(F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))", 0 }, { "gh-r", gen::LTL_GH_R, "RANGE", 0, "(GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1}))", 0 }, { "go-theta", gen::LTL_GO_THETA, "RANGE", 0, "!((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r)))", 0 }, + { "gxf-and", gen::LTL_GXF_AND, "RANGE", 0, + "G(p0 & XF(p1 & XF(p2 & ... XF(pn))))", 0}, { "hkrss-patterns", gen::LTL_HKRSS_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL, "Holeček et al. patterns from the Liberouter project " diff --git a/spot/gen/formulas.cc b/spot/gen/formulas.cc index f36414a2b..5dd46023b 100644 --- a/spot/gen/formulas.cc +++ b/spot/gen/formulas.cc @@ -41,6 +41,40 @@ namespace spot { namespace { + // G(p_0 & XF(p_1 & XF(p_2 & ... XF(p_n)))) + // This is a generalization of eh-pattern=9 + static formula + GXF_and_n(std::string name, int n) + { + formula result = formula::tt(); + + for (; n >= 0; --n) + { + std::ostringstream p; + p << name << n; + formula f = formula::ap(p.str()); + result = And_(f, X_(F_(result))); + } + return G_(result); + } + + // F(p_0 | XG(p_1 | XG(p_2 | ... XG(p_n)))) + // This the dual of the above + static formula + FXG_or_n(std::string name, int n) + { + formula result = formula::ff(); + + for (; n >= 0; --n) + { + std::ostringstream p; + p << name << n; + formula f = formula::ap(p.str()); + result = Or_(f, X_(G_(result))); + } + return F_(result); + } + // F(p_1 & F(p_2 & F(p_3 & ... F(p_n)))) static formula E_n(std::string name, int n) @@ -1070,12 +1104,16 @@ namespace spot return dac_pattern(n); case LTL_EH_PATTERNS: return eh_pattern(n); + case LTL_FXG_OR: + return FXG_or_n("p", n); case LTL_GH_Q: return Q_n("p", n); case LTL_GH_R: return R_n("p", n); case LTL_GO_THETA: return fair_response("p", "q", "r", n); + case LTL_GXF_AND: + return GXF_and_n("p", n); case LTL_HKRSS_PATTERNS: return hkrss_pattern(n); case LTL_KR_N: @@ -1139,9 +1177,11 @@ namespace spot "ccj-beta-prime", "dac-patterns", "eh-patterns", + "fxg-or", "gh-q", "gh-r", "go-theta", + "gxf-and", "hkrss-patterns", "kr-n", "kr-nlogn", @@ -1190,9 +1230,11 @@ namespace spot return 55; case LTL_EH_PATTERNS: return 12; + case LTL_FXG_OR: case LTL_GH_Q: case LTL_GH_R: case LTL_GO_THETA: + case LTL_GXF_AND: return 0; case LTL_HKRSS_PATTERNS: return 55; diff --git a/spot/gen/formulas.hh b/spot/gen/formulas.hh index 8da91963c..12d0d9b5d 100644 --- a/spot/gen/formulas.hh +++ b/spot/gen/formulas.hh @@ -175,9 +175,11 @@ namespace spot LTL_CCJ_BETA_PRIME, LTL_DAC_PATTERNS, LTL_EH_PATTERNS, + LTL_FXG_OR, LTL_GH_Q, LTL_GH_R, LTL_GO_THETA, + LTL_GXF_AND, LTL_HKRSS_PATTERNS, LTL_KR_N, LTL_KR_NLOGN, diff --git a/tests/core/genltl.test b/tests/core/genltl.test index 88ddae403..27246b0c9 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -110,7 +110,8 @@ EOF diff output expected -genltl --kr-n2=1..2 --kr-nlogn=1..2 --kr-n=1..2 --format=%F=%L,%f | +genltl --kr-n2=1..2 --kr-nlogn=1..2 --kr-n=1..2 --gxf-and=0..3 --fxg-or=0..3 \ + --format=%F=%L,%f | ltl2tgba --low --det -F-/2 --stats='%<,%s' > out cat >exp<