From c6f4b186556164f5e062e50cad5092adff884d9a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 26 Aug 2024 15:27:23 +0200 Subject: [PATCH] genltl: add --lily-patterns * spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement support for --lily-pattern. * doc/spot.bib, bin/man/genltl.x: Add references. * NEWS: Mention it. * tests/core/ltlsynt.test: Use these formulas. * tests/core/genltl.test: Adjust. --- NEWS | 7 +++++ bin/genltl.cc | 5 +++ bin/man/genltl.x | 10 ++++-- doc/spot.bib | 11 +++++++ spot/gen/formulas.cc | 69 +++++++++++++++++++++++++++++++++++++---- spot/gen/formulas.hh | 3 ++ tests/core/genltl.test | 6 ++++ tests/core/ltlsynt.test | 29 +++++++++++++++++ 8 files changed, 131 insertions(+), 9 deletions(-) diff --git a/NEWS b/NEWS index cacacf5d2..0436d7cf8 100644 --- a/NEWS +++ b/NEWS @@ -15,6 +15,13 @@ New in spot 2.12.0.dev (not yet released) specify which atomic propositions are input or output, as this can be inferred from their name. + - genltl learned --lily-patterns to generate the example LTL + synthesis specifications from Lily 1.0.2. Those come with input + and output atomic proposition rewriten in the form "iNN" or "oNN", + so they can be fed to ltlsynt directly, as in + + % genltl --lily-patterns | ltlsynt -q + - autfilt learned --restrict-dead-end-edges, to restricts labels of edges leading to dead-ends. See the description of restrict_dead_end_edges_here() below. diff --git a/bin/genltl.cc b/bin/genltl.cc index 3a3cb169e..5a3ab3539 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -115,6 +115,11 @@ static const argp_option options[] = { "kv-psi", gen::LTL_KV_PSI, "RANGE", 0, "quadratic formula with doubly exponential DBA", 0 }, OPT_ALIAS(kr-n2), + { "lily-patterns", gen::LTL_LILY_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL, + "LTL synthesis specification examples from Lily 1.0.2 " + "[Jobstmann & Bloem, FMCAD'06] " + "(range should be included in 1..23)", 0 }, + OPT_ALIAS(jb-patterns), { "ms-example", gen::LTL_MS_EXAMPLE, "RANGE[,RANGE]", 0, "GF(a1&X(a2&X(a3&...Xan)))&F(b1&F(b2&F(b3&...&Xbm)))", 0 }, { "ms-phi-h", gen::LTL_MS_PHI_H, "RANGE", 0, diff --git a/bin/man/genltl.x b/bin/man/genltl.x index db40c653b..35c2c1f66 100644 --- a/bin/man/genltl.x +++ b/bin/man/genltl.x @@ -29,13 +29,17 @@ gh J. Geldenhuys and H. Hansen: Larger automata and less work for LTL model checking. Proceedings of Spin'06. LNCS 3925. .TP +go +P. Gastin and D. Oddoux: Fast LTL to Büchi Automata Translation. +Proceedings of CAV'01. LNCS 2102. +.TP hkrss J. Holeček, T. Kratochvila, V. Řehák, D. Šafránek, and P. Šimeček: Verification Results in Liberouter Project. Tech. Report 03, CESNET, 2004. .TP -go -P. Gastin and D. Oddoux: Fast LTL to Büchi Automata Translation. -Proceedings of CAV'01. LNCS 2102. +jb, lily +B. Jobstmann, and R. Bloem: +Optimizations for LTL Synthesis. Proceedings of FMCAD'06. IEEE. .TP kr O. Kupferman and A. Rosenberg: The Blow-Up in Translating LTL to Deterministic diff --git a/doc/spot.bib b/doc/spot.bib index a2d5c1e9d..bc2b39a1f 100644 --- a/doc/spot.bib +++ b/doc/spot.bib @@ -639,6 +639,17 @@ doi = {10.4204/EPTCS.229.10} } +@InProceedings{ jobsmann.06.fmcad, + author = {Barbara Jobstmann and Roderick Bloem}, + title = {Optimizations for {LTL} Systhesis}, + booktitle = {Proceedings of the 6th International Conference on Formal + Methods in Computer-Aided Design (FMCAD'06)}, + year = {2006}, + month = nov, + publisher = {IEEE}, + doi = {10.1109/FMCAD.2006.22} +} + @InCollection{ klein.07.ciaa, year = {2007}, booktitle = {Proceedings of the 12th International Conference on the diff --git a/spot/gen/formulas.cc b/spot/gen/formulas.cc index d888f4053..ad7f2e8d4 100644 --- a/spot/gen/formulas.cc +++ b/spot/gen/formulas.cc @@ -824,6 +824,56 @@ namespace spot return spot::relabel(parse_formula(formulas[n - 1]), Pnn); } + static formula + lily_pattern(int n) + { + static const char* formulas[] = { + "G(i2->(X(o0&X(o0&Xo0))&(o0->X!o0)&(i0->X(!o0 U i1))))", + "G(i2->(X(o0|X(o0|Xo0))&(o0->X!o0)&(i0->X(!o0 U i1))))", + "G(i0->Xi1)->G(i2->(X(o0|X(o0|Xo0))&(o0->X!o0)&(i0->X(!o0 U i1))))", + "G(i0->X(i1|Xi1))->" + "G(i2->(X(o0|X(o0|Xo0))&(o0->X!o0)&(i0->X(!o0 U i1))))", + "G(i0->X(i1|Xi1))->" + "G(i2->(X(i0|o0|X(i0|o0|X(i0|o0)))&(o0->X!o0)&(i0->X(!o0 U i1))))", + "G(i0->X(i1|X(i1|Xi1)))->" + "G(i2->(X(i0|o0|X(i0|o0|X(i0|o0)))&(o0->X!o0)&(i0->X(!o0 U i1))))", + "G(i0->X(i1|Xi1))->G(i0->(X(!o0 U i1)" + "&(o0->X!o0)&(i2->(i0|o0|X(i0|o0|X(i0|o0|X(i0|o0)))))))", + "GFi0->GFo0", + "GFi0->(!o0&G(!o0->((!o0 U i0)&(i0->Fo0)))&GFo0)", + "(GFi1|Fi0)->(GFo1|Go0)", + "!(G(i1->Fo0)&G(i0->Fo1))", + "G!o1|G(i1->Fo0)|G(i0->Fo1)", + "Gi0->(Fo0&(G!i0->F!o0))", + "G!(o0&o1)&(GFi0->GFo0)&(GFi1->GFo1)", + // lily=15 This matches the original formula from Lily, not + // the unrealizable version from Syfco. See + // https://github.com/reactive-systems/syfco/issues/55 + "G(i0->(!(o0&o1)&Fo0&(i1->Fo1)))&((!o0 U i0)|G!o0)&((!o1 U i1)|G!o1)", + // lily=16 Same comment as above. + "G(i0->(!(o0&o1)&!(o0&o2)&!(o1&o2)&Fo0&(i1->Fo1)&(i2->Fo2)))&" + "((!o0 U i0)|G!o0)&((!o1 U i1)|G!o1)&((!o2 U i2)|G!o2)", + "G(!(o0&o1)&!(o1&o2)&!(o0&o2))&(GFi0->GFo0)&(GFi1->GFo1)&GFo2", + "G(!(o0&o1)&!(o0&o2)&!(o0&o3)&!(o1&o2)&!(o1&o3)&!(o2&o3))&" + "(GFi0->GFo0)&(GFi1->GFo1)&(GFi2->GFo2)&GFo3", + "GFi1->G(o1->(!(o0&o1)&(o1 U i1)&(o0->(o0 U i1))&(i0->Fo0)&Fo1))", + "(!i1&G((!i1&!o2)->X!i1)&G(i1->F!i1)&G(o2->Xi1))->" + "G((o1&X!o1)->(o2&(o0|o1)&((o0&X!o0)->o2)&((!o0&(!i0|!i1))->" + "Xo0)&((!o1&(i0|!i1))->Xo1)&(i0->F!o0)&F!o1))", + "(G(!i0|!i1)&G(!i0|!i2)&G(!i0|!i3)&G(!i1|!i2)&G(!i1|!i3)&" + "G(!i2|!i3))->G((!o0|!o1)&(!o0|!o2)&(!o0|!o3)&(!o1|!o2)&(!o1|!o3)&" + "(!o2|!o3)&G(i0->(Xo0|XXo0|XXXo0))&G(i1->(Xo1|XXo1|XXXo1))&" + "G(i2->(Xo2|XXo2|XXXo2))&G(i3->(Xo3|XXo3|XXXo3)))", + "(!i0&!i1&!i2&G!(i0&i1)&GF!i2&G((!i2&o0)->X!i2)&G(i2->X(!i2|" + "X(!i2|X(!i2 | X!i2)))))->G(!(i2&Xo0)&(i1->F!o0)&(i0->Fo0))", + "(G((i0&Xo0)->Xi0)&GF!i0)->GX(!i0&X!o0)", + }; + constexpr unsigned max = (sizeof formulas)/(sizeof *formulas); + if (n < 1 || (unsigned) n > max) + bad_number("lily-patterns", n, max); + return parse_formula(formulas[n - 1]); + } + static formula p_pattern(int n) { @@ -1359,12 +1409,8 @@ namespace spot return kr1_exp(n, "a", "b", "c", "d", "y", "z"); case LTL_KV_PSI: return kv_exp(n, "a", "b", "c", "d"); - case LTL_OR_FG: - return FG_n("p", n, false); - case LTL_OR_G: - return combunop_n("p", n, op::G, false); - case LTL_OR_GF: - return GF_n("p", n, false); + case LTL_LILY_PATTERNS: + return lily_pattern(n); case LTL_MS_EXAMPLE: return ms_example("a", "b", n, m); case LTL_MS_PHI_H: @@ -1373,6 +1419,12 @@ namespace spot return ms_phi_rs("a", "b", n, true); case LTL_MS_PHI_S: return ms_phi_rs("a", "b", n, false); + case LTL_OR_FG: + return FG_n("p", n, false); + case LTL_OR_G: + return combunop_n("p", n, op::G, false); + case LTL_OR_GF: + return GF_n("p", n, false); case LTL_P_PATTERNS: return p_pattern(n); case LTL_PPS_ARBITER_STANDARD: @@ -1448,6 +1500,7 @@ namespace spot "kr-n", "kr-nlogn", "kv-psi", + "lily-patterns", "ms-example", "ms-phi-h", "ms-phi-r", @@ -1518,6 +1571,9 @@ namespace spot case LTL_KR_N: case LTL_KR_NLOGN: case LTL_KV_PSI: + return 0; + case LTL_LILY_PATTERNS: + return 23; case LTL_MS_EXAMPLE: case LTL_MS_PHI_H: case LTL_MS_PHI_R: @@ -1586,6 +1642,7 @@ namespace spot case LTL_KR_N: case LTL_KR_NLOGN: case LTL_KV_PSI: + case LTL_LILY_PATTERNS: return 1; case LTL_MS_EXAMPLE: return 2; diff --git a/spot/gen/formulas.hh b/spot/gen/formulas.hh index 131b234b5..044ab753f 100644 --- a/spot/gen/formulas.hh +++ b/spot/gen/formulas.hh @@ -91,6 +91,9 @@ namespace spot /// \cite kupferman.10.mochart , /// \cite kupferman.05.tcl . LTL_KV_PSI, + /// LTL synthesis examples specification from the Lily 1.0.2 + /// distribution. \cite jobstmann.06.fmcad + LTL_LILY_PATTERNS, /// `GF(a1&X(a2&X(a3&...Xan)))&F(b1&F(b2&F(b3&...&Xbm)))` /// \cite muller.17.gandalf LTL_MS_EXAMPLE, diff --git a/tests/core/genltl.test b/tests/core/genltl.test index add4b1d99..3597179d9 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -241,6 +241,12 @@ test $? = 2 test "`cat err`" = \ "genltl: no pattern hkrss-patterns=0, supported range is 1..55" +genltl --lily-patterns=0 2> err && exit 1 +test $? = 2 +test "`cat err`" = \ + "genltl: no pattern lily-patterns=0, supported range is 1..23" + + genltl --kr-n=0 2> err && exit 1 test $? = 2 test "`cat err`" = "genltl: no pattern kr-n=0, supported range is 1.." diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index acd935560..9500550ea 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -1316,3 +1316,32 @@ f2='G(i1->(o1|!o2)) & G(!i1->(o3|!o4)) & G(i2->(!o1|o2)) & G(!i2->(!o3|o4))&Go5' ltlsynt -f "$f2" --polarity=before-decom --verbose 2>out 1>&2 sed 's/ [0-9.e-]* seconds/ X seconds/g;s/ -> /->/g;' out > outx diff outx exp + + +genltl --lily-patterns | ltlsynt -q > out && exit 2 +cat >expected <