diff --git a/NEWS b/NEWS index f6ec9ad15..2fbe8d2bf 100644 --- a/NEWS +++ b/NEWS @@ -51,6 +51,13 @@ New in spot 2.10.6.dev (not yet released) include each other, and are used to show a regression (in speed) present in Spot 2.10.x and fixed in 2.11. + - genltl learned --eil-gsi to generate a familly a function whose + translation and simplification used to be very slow. In particular + + genltl --eil-gsi=23 | ltlfilt --from-ltlf | ltl2tgba + + was reported as taking 9 days. This is now instantaneous. + Library: - The new function suffix_operator_normal_form() implements @@ -149,7 +156,8 @@ New in spot 2.10.6.dev (not yet released) and q₃ can be merged (taking the union of their outgoing transitions). This is cheap function is automatically called by spot::translate() after translation of a formula to GBA, before - further simplification. + further simplification. This was introduced to help with automata + produced from formulas output by "genltl --eil-gsi" (see above). - spot::parallel_policy is an object that can be passed to some algorithm to specify how many threads can be used if Spot has been diff --git a/bin/genltl.cc b/bin/genltl.cc index 6c632de7a..6393024c2 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2015-2019 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2015-2019, 2022 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -84,6 +84,8 @@ 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 }, + { "eil-gsi", gen::LTL_EIL_GSI, "RANGE", 0, + "G[0..n]((a S b) -> c) rewritten using future operators", 0 }, { "fxg-or", gen::LTL_FXG_OR, "RANGE", 0, "F(p0 | XG(p1 | XG(p2 | ... XG(pn))))", 0}, { "gf-equiv", gen::LTL_GF_EQUIV, "RANGE", 0, diff --git a/spot/gen/formulas.cc b/spot/gen/formulas.cc index 3f63b07e7..10841e820 100644 --- a/spot/gen/formulas.cc +++ b/spot/gen/formulas.cc @@ -1281,6 +1281,21 @@ namespace spot } } + // G[0..n]((a S b) -> c) rewritten using future operators, + // from Edmond Irani Liu (EIL). GSI stands for "Globally Since Implies." + static formula eil_gsi(int n, std::string a, std::string b, std::string c) + { + formula fa = formula::ap(a); + formula fb = formula::ap(b); + formula res = fb; + for (int i = 1; i <= n; ++i) + { + formula tmp = formula::And({formula::strong_X(i, fa), res}); + res = formula::Or({formula::strong_X(i, fb), tmp}); + } + return formula::Implies(res, formula::strong_X(n, formula::ap(c))); + } + formula ltl_pattern(ltl_pattern_id pattern, int n, int m) { if (n < 0) @@ -1317,6 +1332,8 @@ namespace spot return dac_pattern(n); case LTL_EH_PATTERNS: return eh_pattern(n); + case LTL_EIL_GSI: + return eil_gsi(n, "a", "b", "c"); case LTL_FXG_OR: return FXG_or_n("p", n); case LTL_GF_EQUIV: @@ -1418,6 +1435,7 @@ namespace spot "ccj-beta-prime", "dac-patterns", "eh-patterns", + "eil-gsi", "fxg-or", "gf-equiv", "gf-equiv-xn", @@ -1485,6 +1503,7 @@ namespace spot return 55; case LTL_EH_PATTERNS: return 12; + case LTL_EIL_GSI: case LTL_FXG_OR: case LTL_GF_EQUIV: case LTL_GF_EQUIV_XN: @@ -1554,6 +1573,7 @@ namespace spot case LTL_CCJ_BETA_PRIME: case LTL_DAC_PATTERNS: case LTL_EH_PATTERNS: + case LTL_EIL_GSI: case LTL_FXG_OR: case LTL_GF_EQUIV: case LTL_GF_EQUIV_XN: diff --git a/spot/gen/formulas.hh b/spot/gen/formulas.hh index ac5974e48..ef5a0d850 100644 --- a/spot/gen/formulas.hh +++ b/spot/gen/formulas.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Developpement de -// l'EPITA (LRDE). +// Copyright (C) 2017-2019, 2022 Laboratoire de Recherche et +// Developpement de l'EPITA (LRDE). // // This file is part of Spot, a model checking library. // @@ -56,6 +56,8 @@ namespace spot /// 12 formulas from Etessami and Holzmann. /// \cite etessami.00.concur LTL_EH_PATTERNS, + /// Familly sent by Edmond Irani Liu + LTL_EIL_GSI, /// `F(p0 | XG(p1 | XG(p2 | ... XG(pn))))` LTL_FXG_OR, /// `(GFa1 & GFa2 & ... & GFan) <-> GFz` diff --git a/tests/core/genltl.test b/tests/core/genltl.test index d943c4cae..622950f65 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -269,3 +269,43 @@ diff range1.ltl range2.ltl genltl --sb-patterns=1..20 | ltlfilt -v --nth 10..20 > range1.ltl genltl --sb-patterns=1..9 > range2.ltl diff range1.ltl range2.ltl + + +# Edmond Irani Liu sent a bug report where formula 23 in this series +# took 9 days to produce, despite the small size of the resulting +# automaton. I (ADL) later found this to be caused by simulation +# applied on a non-deterministic automaton with many non-deterministic +# choices going to state that simulate one another, which in turn lead +# to massive slowdown of the minato_isop algorithm. As a workaround, +# I introduced delay_branching_here(), a cheap function that is called +# before simplification. In this case, this is enough to determinize +# the automaton, simplifying simulation-based reduction greatly. +genltl --eil-gsi=1..25 | ltlfilt --from-ltlf | ltl2tgba --stats=%s,%e >output +cat >expected <