diff --git a/NEWS b/NEWS index fd2d45167ab6ff09b13cefa817ba7971a01aeef2..8c30267bf014f10b3a36e1345c0dd59b9be613af 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,13 @@ New in spot 2.4.0.dev (not yet released) - Nothing yet. + Tools: + + - genltl learned to generate 4 new families of formulas, taken + from Müller & Sickert's GandALF'17 paper: + --ms-example=RANGE GF(a1&X(a2&X(a3&...)))&F(b1&F(b2&F(b3&...))) + --ms-phi-h=RANGE FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|... + --ms-phi-r=RANGE (FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...)) + --ms-phi-s=RANGE (FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...)) New in spot 2.4 (2017-09-06) diff --git a/bin/genltl.cc b/bin/genltl.cc index 90ef4618ba30fa48f945342ce5dbe49425416770..ed88035f2bd5561afd923963a3e7c49d44f9b13c 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -106,6 +106,14 @@ static const argp_option options[] = { "kv-psi", gen::LTL_KV_PSI, "RANGE", 0, "quadratic formula with doubly exponential DBA", 0 }, OPT_ALIAS(kr-n2), + { "ms-example", gen::LTL_MS_EXAMPLE, "RANGE", 0, + "GF(a1&X(a2&X(a3&...)))&F(b1&F(b2&F(b3&...)))", 0 }, + { "ms-phi-h", gen::LTL_MS_PHI_H, "RANGE", 0, + "FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|...", 0 }, + { "ms-phi-r", gen::LTL_MS_PHI_R, "RANGE", 0, + "(FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...))", 0 }, + { "ms-phi-s", gen::LTL_MS_PHI_S, "RANGE", 0, + "(FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...))", 0 }, { "or-fg", gen::LTL_OR_FG, "RANGE", 0, "FG(p1)|FG(p2)|...|FG(pn)", 0 }, OPT_ALIAS(ccj-xi), { "or-g", gen::LTL_OR_G, "RANGE", 0, "G(p1)|G(p2)|...|G(pn)", 0 }, diff --git a/bin/man/genltl.x b/bin/man/genltl.x index 5935f4c2d0f09f6d8bce854ba6e52d50e8dba182..7ff602d461d0fdba20ec4969977d143e18dfea1c 100644 --- a/bin/man/genltl.x +++ b/bin/man/genltl.x @@ -46,6 +46,10 @@ kv O. Kupferman and M. Y. Vardi: From Linear Time to Branching Time. ACM Transactions on Computational Logic, 6(2):273-294, 2005. .TP +ms +D. Müller and S. Sickert: LTL to Deterministic Emerson-Lei Automata. +Proceedings of GandALF'17. EPTCS 256. +.TP p R. Pelánek: BEEM: benchmarks for explicit model checkers Proceedings of Spin'07. LNCS 4595. diff --git a/spot/gen/formulas.cc b/spot/gen/formulas.cc index 5dd46023b9223318ad8672ce0d7579bb9d5b5568..239e66d29338a415daf53b256e4348e60d068994 100644 --- a/spot/gen/formulas.cc +++ b/spot/gen/formulas.cc @@ -41,6 +41,59 @@ namespace spot { namespace { + static formula + ms_example(const char* a, const char* b, int n) + { + formula ax = formula::tt(); + formula fb = formula::tt(); + for (int i = n; i > 0; --i) + { + std::ostringstream ans; + ans << a << i; + ax = And_(formula::ap(ans.str()), X_(ax)); + ans.str(""); + ans << b << i; + fb = F_(And_(formula::ap(ans.str()), fb)); + } + return And_(G_(F_(ax)), fb); + } + + static formula + ms_phi_h(const char* a, const char* b, int n) + { + formula fa = formula::ap(a); + formula fb = formula::ap(b); + formula out = formula::ff(); + do + { + out = Or_(F_(G_(Or_(fa, fb))), out); + fa = Not_(fa); + fb = X_(fb); + } + while (n--); + return out; + } + + static formula + ms_phi_rs(const char* a, const char* b, int n, bool r = true) + { + formula fgan = [=]() { + std::ostringstream ans; + ans << a << n; + return F_(G_(formula::ap(ans.str()))); + } (); + formula gfbn = [=]() { + std::ostringstream ans; + ans << b << n; + return G_(F_(formula::ap(ans.str()))); + } (); + formula top = r ? And_(fgan, gfbn) : Or_(fgan, gfbn); + if (n == 0) + return top; + formula sub = ms_phi_rs(a, b, n - 1, !r); + return r ? Or_(sub, top) : And_(sub, top); + } + // G(p_0 & XF(p_1 & XF(p_2 & ... XF(p_n)))) // This is a generalization of eh-pattern=9 static formula @@ -1128,6 +1181,14 @@ namespace spot return combunop_n("p", n, op::G, false); case LTL_OR_GF: return GF_n("p", n, false); + case LTL_MS_EXAMPLE: + return ms_example("a", "b", n); + case LTL_MS_PHI_H: + return ms_phi_h("a", "b", n); + case LTL_MS_PHI_R: + return ms_phi_rs("a", "b", n, true); + case LTL_MS_PHI_S: + return ms_phi_rs("a", "b", n, false); case LTL_P_PATTERNS: return p_pattern(n); case LTL_R_LEFT: @@ -1186,6 +1247,10 @@ namespace spot "kr-n", "kr-nlogn", "kv-psi", + "ms-example", + "ms-phi-h", + "ms-phi-r", + "ms-phi-s", "or-fg", "or-g", "or-gf", @@ -1241,6 +1306,10 @@ namespace spot case LTL_KR_N: case LTL_KR_NLOGN: case LTL_KV_PSI: + case LTL_MS_EXAMPLE: + case LTL_MS_PHI_H: + case LTL_MS_PHI_R: + case LTL_MS_PHI_S: case LTL_OR_FG: case LTL_OR_G: case LTL_OR_GF: diff --git a/spot/gen/formulas.hh b/spot/gen/formulas.hh index 12d0d9b5d84d03e2ba9d8f99489fea6b3efda800..37efa28ffac200cfd6b2f66d334c0a6947b67738 100644 --- a/spot/gen/formulas.hh +++ b/spot/gen/formulas.hh @@ -160,6 +160,20 @@ // series = {Lecture Notes in Computer Science}, // publisher = {Springer-Verlag} // } +// +// @InProceedings{muller.17.gandalf, +// author = {David M\"uller and Salomon Sickert}, +// title = {{LTL} to Deterministic {E}merson-{L}ei Automata}, +// booktitle = {Proceedings of the 8th International Sumposium on Games, +// Automata, Logics and Formal Verification (GandALF'17)}, +// year = 2017, +// publisher = {Springer-Verlag} +// series = {Electronic Proceedings in Theoretical Computer Science}, +// volume = {256}, +// publisher = {Open Publishing Association}, +// pages = {180--194}, +// doi = {10.4204/EPTCS.256.13} +// } namespace spot { @@ -184,6 +198,10 @@ namespace spot LTL_KR_N, LTL_KR_NLOGN, LTL_KV_PSI, + LTL_MS_EXAMPLE, + LTL_MS_PHI_H, + LTL_MS_PHI_R, + LTL_MS_PHI_S, LTL_OR_FG, LTL_OR_G, LTL_OR_GF, diff --git a/tests/core/genltl.test b/tests/core/genltl.test index 27246b0c9e7718c0574ce1ba5342547990479e76..711e739ecdf13fd42fd98501ac97a1e674b8df95 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -134,3 +134,26 @@ diff out exp test \$(genltl --kr-n2=4 | ltl2tgba --low --stats=%s) -ge 16 test \$(genltl --kr-nlogn=4 | ltl2tgba --low --stats=%s) -ge 16 test \$(genltl --kr-n=4 | ltl2tgba --low --stats=%s) -ge 16 + +genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \ + --format=%F=%L,%f | + ltl2tgba -G -D -F-/2 --stats='%<,%s' > out +cat >exp<