From c76df95c69c521389ff77dd229532dfbfa9fafe8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 3 Jun 2018 14:38:04 +0200 Subject: [PATCH] genltl: three new families --sejk-{j,k,patterns} MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit These correspond to the first three blocks of table 1 in S. Sickert, J. Esparza, S. Jaax, and J. Křetínský: Limit-Deterministic Büchi Automata for Linear Temporal Logic. CAV'16. LNCS 9780. For #353. * spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement the new families. * tests/core/genltl.test: Test it. * bin/man/genltl.x, NEWS: Document it. --- NEWS | 6 +++++ bin/genltl.cc | 7 ++++++ bin/man/genltl.x | 5 +++++ spot/gen/formulas.cc | 51 ++++++++++++++++++++++++++++++++++++++++-- spot/gen/formulas.hh | 32 ++++++++++++++++++++++++++ tests/core/genltl.test | 13 ++++++++++- 6 files changed, 111 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index ff2925ce6..990d6e614 100644 --- a/NEWS +++ b/NEWS @@ -22,6 +22,12 @@ New in spot 2.5.3.dev (not yet released) product to avoid exceeding the number of supported acceptance sets. + - genltl learned to generate three new families of formulas: + --sejk-j=RANGE (GFa1&...&GFan) -> (GFb1&...&GFbn) + --sejk-k=RANGE (GFa1|FGb1)&...&(GFan|FGbn) + --sejk-patterns[=RANGE] φ₁,φ₂,φ₃ from Sikert et al's [CAV'16] + paper (range should be included in 1..3) + Library: - spot::twa_graph::merge_states() is a new method that merges states diff --git a/bin/genltl.cc b/bin/genltl.cc index 169b7fbcb..e0e3dd865 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -141,6 +141,13 @@ static const argp_option options[] = { "sb-patterns", gen::LTL_SB_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL, "Somenzi and Bloem [CAV'00] patterns " "(range should be included in 1..27)", 0 }, + { "sejk-j", gen::LTL_SEJK_J, "RANGE", 0, + "(GFa1&...&GFan) -> (GFb1&...&GFbn)", 0 }, + { "sejk-k", gen::LTL_SEJK_K, "RANGE", 0, + "(GFa1|FGb1)&...&(GFan|FGbn)", 0 }, + { "sejk-patterns", gen::LTL_SEJK_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL, + "φ₁,φ₂,φ₃ from Sikert et al's [CAV'16] paper " + "(range should be included in 1..3)", 0 }, { "tv-f1", gen::LTL_TV_F1, "RANGE", 0, "G(p -> (q | Xq | ... | XX...Xq)", 0 }, { "tv-f2", gen::LTL_TV_F2, "RANGE", 0, diff --git a/bin/man/genltl.x b/bin/man/genltl.x index 7ff602d46..a21b40083 100644 --- a/bin/man/genltl.x +++ b/bin/man/genltl.x @@ -62,6 +62,11 @@ sb F. Somenzi and R. Bloem: Efficient Büchi Automata for LTL Formulae. Proceedings of CAV'00. LNCS 1855. .TP +sejk +S. Sickert, J. Esparza, S. Jaax, and J. Křetínský: Limit-Deterministic +Büchi Automata for Linear Temporal Logic. +Proceedings of CAV'16. LNCS 9780. +.TP tv D. Tabakov and M. Y. Vardi: Optimized Temporal Monitors for SystemC. Proceedings of RV'10. LNCS 6418. diff --git a/spot/gen/formulas.cc b/spot/gen/formulas.cc index a47c0a1de..8d1cfea27 100644 --- a/spot/gen/formulas.cc +++ b/spot/gen/formulas.cc @@ -1139,6 +1139,41 @@ namespace spot return res; } + + static formula + sejk_j(std::string a, std::string b, int n) + { + return formula::Implies(GF_n(a, n), GF_n(b, n)); + } + + static formula + sejk_k(std::string a, std::string b, int n) + { + formula result = formula::tt(); + for (int i = 1; i <= n; ++i) + { + formula ai = formula::ap(a + std::to_string(i)); + formula bi = formula::ap(b + std::to_string(i)); + result = formula::And({result, + formula::Or({G_(F_(ai)), F_(G_(bi))})}); + } + return result; + } + + static formula + sejk_pattern(int n) + { + static const char* formulas[] = { + "GF(Fa | Gb | FG(a | Xb))", + "FG(Ga | F!b | GF(a & Xb))", + "GF(Fa | GXb | FG(a | XXb))", + }; + + constexpr unsigned max = (sizeof formulas)/(sizeof *formulas); + if (n < 1 || (unsigned) n > max) + bad_number("sejk-patterns", n, max); + return spot::relabel(parse_formula(formulas[n - 1]), Pnn); + } } formula ltl_pattern(ltl_pattern_id pattern, int n) @@ -1222,6 +1257,12 @@ namespace spot return ltl_counter("b", "m", n, true); case LTL_SB_PATTERNS: return sb_pattern(n); + case LTL_SEJK_J: + return sejk_j("a", "b", n); + case LTL_SEJK_K: + return sejk_k("a", "b", n); + case LTL_SEJK_PATTERNS: + return sejk_pattern(n); case LTL_TV_F1: return tv_f1("p", "q", n); case LTL_TV_F2: @@ -1281,6 +1322,9 @@ namespace spot "rv-counter-carry-linear", "rv-counter-linear", "sb-patterns", + "sejk-j", + "sejk-k", + "sejk-patterns", "tv-f1", "tv-f2", "tv-g1", @@ -1346,6 +1390,11 @@ namespace spot return 0; case LTL_SB_PATTERNS: return 27; + case LTL_SEJK_J: + case LTL_SEJK_K: + return 0; + case LTL_SEJK_PATTERNS: + return 3; case LTL_TV_F1: case LTL_TV_F2: case LTL_TV_G1: @@ -1358,8 +1407,6 @@ namespace spot break; } throw std::runtime_error("unsupported pattern"); - } - } } diff --git a/spot/gen/formulas.hh b/spot/gen/formulas.hh index cff83aa50..b56bee195 100644 --- a/spot/gen/formulas.hh +++ b/spot/gen/formulas.hh @@ -174,6 +174,35 @@ // pages = {180--194}, // doi = {10.4204/EPTCS.256.13} // } +// +// @InProceedings{sickert.16.cav, +// author = {Salomon Sickert and Javier Esparza and Stefaan Jaax +// and Jan K{\v{r}}et{\'i}nsk{\'y}}, +// title = {Limit-Deterministic {B\"u}chi Automata for Linear Temporal Logic} +// booktitle = {Proceedings of the 28th International Conference on +// Computer Aided Verification (CAV'16)}, +// year = 2016, +// publisher = {Springer-Verlag} +// series = {Lecture Notes in Computer Science}, +// volume = {9780}, +// pages = {312--332}, +// doi = {10.1007/978-3-319-41540-6_17} +// } +// +// @InProceedings{kretisnky.12.cav, +// author = {Jan K{\v{r}}et{\'i}nsk{\'y} and Javier Esparza}, +// title = {Deterministic Automata for the {(F,G)}-Fragment of +// {LTL}}, +// booktitle = {24th International Conference on Computer Aided +// Verification (CAV'12)}, +// year = 2012, +// pages = {7--22}, +// doi = {10.1007/978-3-642-31424-7_7}, +// url = {https://doi.org/10.1007/978-3-642-31424-7_7}, +// isbn = {978-3-642-31424-7}, +// publisher = {Springer}, +// } + namespace spot { @@ -215,6 +244,9 @@ namespace spot LTL_RV_COUNTER_CARRY_LINEAR, LTL_RV_COUNTER_LINEAR, LTL_SB_PATTERNS, + LTL_SEJK_J, + LTL_SEJK_K, + LTL_SEJK_PATTERNS, LTL_TV_F1, LTL_TV_F2, LTL_TV_G1, diff --git a/tests/core/genltl.test b/tests/core/genltl.test index 8c8e67e76..3615e0ebc 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -29,7 +29,8 @@ s/[=[].*/=1/p res=`genltl $opts --format="--%F=%L"` test "$opts" = "$res" -run 0 genltl --dac=1..5 --eh=1..5 --pos --neg --format="%F:%L %f" >output +run 0 genltl --dac=1..5 --eh=1..5 --sejk-p --pos --neg \ + --format="%F:%L %f" >output cat >expected < err && exit 1 test $? = 2 test "`cat err`" = "genltl: no pattern sb-patterns=0, supported range is 1..27" + +genltl --sejk-patterns=0 2> err && exit 1 +test $? = 2 +test "`cat err`" = "genltl: no pattern sejk-patterns=0, supported range is 1..3"