From da65479696c043d089b7e92010a5ec26885556f5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 18 Oct 2017 14:45:21 +0200 Subject: [PATCH 01/12] Bump version to 2.4.1.dev * NEWS, configure.ac: Here. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index f86ad9c94..5011f24ea 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.4.1.dev (not yet released) + + Nothing yet. + New in spot 2.4.1 (2017-10-05) Bugs fixed: diff --git a/configure.ac b/configure.ac index aac8ae758..27c20f27a 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.4.1], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.4.1.dev], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) From b521fef2260a707898fc26b4a8f5e282e0fd3b6b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 7 Oct 2017 13:10:03 +0200 Subject: [PATCH 02/12] simulation: do not create scc_info * spot/twaalgos/simulation.cc: Remove useless creation of scc_info object. --- spot/twaalgos/simulation.cc | 5 ----- 1 file changed, 5 deletions(-) diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index cddc529cc..e7b8979ed 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -27,7 +27,6 @@ #include #include #include -#include #include #include #include @@ -164,8 +163,6 @@ namespace spot throw std::runtime_error ("direct_simulation() does not yet support alternation"); - scc_info_.reset(new scc_info(in)); - unsigned ns = in->num_states(); size_a_ = ns; unsigned init_state_number = in->get_init_state_number(); @@ -710,8 +707,6 @@ namespace spot automaton_size stat; - std::unique_ptr scc_info_; - const const_twa_graph_ptr original_; }; From e6c4eb15c13f4b8143d60af3431f570fccad661a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 11 Oct 2017 14:35:23 +0200 Subject: [PATCH 03/12] genaut: fix ks_nca * spot/gen/automata.cc (ks_nca): The output is complete. * tests/core/genaut.test: Add test. * NEWS: Mention the bug. --- NEWS | 5 ++++- spot/gen/automata.cc | 2 +- tests/core/genaut.test | 2 ++ 3 files changed, 7 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 5011f24ea..71c8d0a7b 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,9 @@ New in spot 2.4.1.dev (not yet released) - Nothing yet. + Bugs fixed: + + - Automata produced by "genaut --ks-nca=N" were incorrectly marked + as not complete. New in spot 2.4.1 (2017-10-05) diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc index f543d4682..e634d4e8a 100644 --- a/spot/gen/automata.cc +++ b/spot/gen/automata.cc @@ -87,7 +87,7 @@ namespace spot aut->merge_edges(); aut->prop_state_acc(true); aut->prop_universal(false); - aut->prop_complete(false); + aut->prop_complete(true); aut->prop_inherently_weak(false); aut->prop_stutter_invariant(false); aut->prop_semi_deterministic(false); diff --git a/tests/core/genaut.test b/tests/core/genaut.test index ec93c0b42..cddbe0c3f 100644 --- a/tests/core/genaut.test +++ b/tests/core/genaut.test @@ -43,6 +43,8 @@ cat >expected <err && exit 1 grep positive err genaut --l-nba=0 2>err && exit 1 From 42452ba4a3ac24aa97ec5f28b8327d90de346caf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 11 Oct 2017 21:47:31 +0200 Subject: [PATCH 04/12] simplify: improve the logic of some implication checks Fixes #293. * spot/tl/simplify.cc: Test implications that would yield tt or ff first. In rules of the form "if a => b, a op b = b" also check if b => a, and in this case return smallest(a,b). * tests/core/reduccmp.test: Add a test. * NEWS: Mention it. --- NEWS | 3 + spot/tl/simplify.cc | 115 ++++++++++++++++++++++++++++----------- tests/core/reduccmp.test | 9 +++ 3 files changed, 96 insertions(+), 31 deletions(-) diff --git a/NEWS b/NEWS index 71c8d0a7b..c3e22a033 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,9 @@ New in spot 2.4.1.dev (not yet released) - Automata produced by "genaut --ks-nca=N" were incorrectly marked as not complete. + - Fix some cases for which the highest setting of formulas + simplification would produce worse results than lower settings. + New in spot 2.4.1 (2017-10-05) Bugs fixed: diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index e06c44411..8c4e82bb9 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -30,6 +30,7 @@ #include #include #include +#include #include #include #include @@ -1756,10 +1757,17 @@ namespace spot case op::U: // if a => b, then a U b = b + if (c_->implication(a, b)) + { + // but if also b => a, pick the smallest one. + if ((length_boolone(a) < length_boolone(b)) + && c_->implication(b, a)) + return a; + return b; + } // if (a U b) => b, then a U b = b (for stronger containment) - if (c_->implication(a, b) - || (opt_.containment_checks_stronger - && c_->contained(bo, b))) + if (opt_.containment_checks_stronger + && c_->contained(bo, b)) return b; // if !a => b, then a U b = Fb // if a eventual && b => a, then a U b = Fb @@ -1795,7 +1803,13 @@ namespace spot case op::R: // if b => a, then a R b = b if (c_->implication(b, a)) - return b; + { + // but if also a => b, pick the smallest one. + if ((length_boolone(a) < length_boolone(b)) + && c_->implication(a, b)) + return a; + return b; + } // if b => !a, then a R b = Gb // if a universal && a => b, then a R b = Gb if (c_->implication_neg(b, a, true) @@ -1825,15 +1839,23 @@ namespace spot break; case op::W: - // if a => b, then a W b = b - // if a W b => b, then a W b = b (for stronger containment) - if (c_->implication(a, b) - || (opt_.containment_checks_stronger - && c_->contained(bo, b))) - return b; // if !a => b then a W b = 1 if (c_->implication_neg(a, b, false)) return formula::tt(); + // if a => b, then a W b = b + if (c_->implication(a, b)) + { + // but if also b => a, pick the smallest one. + if ((length_boolone(a) < length_boolone(b)) + && c_->implication(b, a)) + return a; + return b; + } + + // if a W b => b, then a W b = b (for stronger containment) + if (opt_.containment_checks_stronger + && c_->contained(bo, b)) + return b; // if a => b, then a W (b W c) = b W c // (Beware: even if a => b we do not have a W (b U c) = b U c) if (b.is(op::W) && c_->implication(a, b[0])) @@ -1853,12 +1875,18 @@ namespace spot break; case op::M: - // if b => a, then a M b = b - if (c_->implication(b, a)) - return b; // if b => !a, then a M b = 0 if (c_->implication_neg(b, a, true)) return formula::ff(); + // if b => a, then a M b = b + if (c_->implication(b, a)) + { + // but if also a => b, pick the smallest one. + if ((length_boolone(a) < length_boolone(b)) + && c_->implication(a, b)) + return a; + return b; + } // if b => a, then a M (b M c) = b M c if (b.is(op::M) && c_->implication(b[0], a)) return b; @@ -2003,24 +2031,49 @@ namespace spot if ((opt_.synt_impl | opt_.containment_checks) && mo.is(op::Or, op::And)) - for (unsigned i = 0; i < mos; ++i) - { - formula fi = mo[i]; - formula fo = mo.all_but(i); - // if fi => fo, then fi | fo = fo - // if fo => fi, then fi & fo = fo - if ((mo.is(op::Or) && c_->implication(fi, fo)) - || (mo.is(op::And) && c_->implication(fo, fi))) - return recurse(fo); - // if fi => !fo, then fi & fo = false - // if fo => !fi, then fi & fo = false - // if !fi => fo, then fi | fo = true - // if !fo => fi, then fi | fo = true - bool is_and = mo.is(op::And); - if (c_->implication_neg(fi, fo, is_and) - || c_->implication_neg(fo, fi, is_and)) - return recurse(is_and ? formula::ff() : formula::tt()); - } + { + // Do not merge these two loops, as rewritings from the + // second loop could prevent rewritings from the first one + // to trigger. + for (unsigned i = 0; i < mos; ++i) + { + formula fi = mo[i]; + formula fo = mo.all_but(i); + // if fi => !fo, then fi & fo = false + // if fo => !fi, then fi & fo = false + // if !fi => fo, then fi | fo = true + // if !fo => fi, then fi | fo = true + bool is_and = mo.is(op::And); + if (c_->implication_neg(fi, fo, is_and) + || c_->implication_neg(fo, fi, is_and)) + return recurse(is_and ? formula::ff() : formula::tt()); + } + for (unsigned i = 0; i < mos; ++i) + { + formula fi = mo[i]; + formula fo = mo.all_but(i); + // if fi => fo, then fi | fo = fo + // if fo => fi, then fi & fo = fo + if ((mo.is(op::Or) && c_->implication(fi, fo)) + || (mo.is(op::And) && c_->implication(fo, fi))) + { + // We are about to pick fo, but hold on! + // Maybe we actually have fi <=> fo, in + // which case we could decide to work on fi or fo. + // + // As a heuristic, let's return the smallest + // subformula. So we only need to check this + // other implication if fi is smaller than fo, + // otherwise we don't care. + if ((length_boolone(fi) < length_boolone(fo)) + && ((mo.is(op::Or) && c_->implication(fo, fi)) + || (mo.is(op::And) && c_->implication(fi, fo)))) + return recurse(fi); + else + return recurse(fo); + } + } + } vec res; res.reserve(mos); diff --git a/tests/core/reduccmp.test b/tests/core/reduccmp.test index 66e5b185c..bf743bc7b 100755 --- a/tests/core/reduccmp.test +++ b/tests/core/reduccmp.test @@ -114,6 +114,15 @@ GFa R Fa, GFa FGa R Fa, GFa FGa R a, FGa R a Ga R a, Ga + +# issue 293 +F(G!p1 | p1) W Fp1, 1 +F(p1 | G!p1) W Fp1, 1 +F(Fp1 -> p1) W Fp1, 1 +G(Fp0 | (p0 M (Fp0 W p0))), GFp0 +G((p0 M (Fp0 W p0)) | Fp0), GFp0 +G((Fp0) W ((p0 M (Fp0 W p0)))), GFp0 +!G((Fp0) W ((p0 M (Fp0 W p0)))), FG!p0 EOF cp common.txt nottau.txt From 5b037f96e0380ba63bbfb68fb5be3356df4408ce Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 15 Oct 2017 11:15:53 +0200 Subject: [PATCH 05/12] man: add missing crossrefs in spot(7) Part of #292. * bin/man/spot.x, bin/spot.cc: Here. --- bin/man/spot.x | 13 ++++++++----- bin/spot.cc | 5 ++++- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/bin/man/spot.x b/bin/man/spot.x index f46305aa5..8ac229dde 100644 --- a/bin/man/spot.x +++ b/bin/man/spot.x @@ -11,16 +11,19 @@ that are listed below. .\" Add any additional description here [SEE ALSO] -.BR randltl (1) +.BR autfilt (1) +.BR autcross (1) +.BR dstar2tgba (1) +.BR genaut (1) .BR genltl (1) -.BR ltlfilt (1) -.BR ltlrind (1) -.BR randaut (1) .BR ltl2tgba (1) .BR ltl2tgta (1) -.BR autfilt (1) .BR ltlcross (1) .BR ltldo (1) +.BR ltlfilt (1) +.BR ltlgrind (1) +.BR randaut (1) +.BR randltl (1) .BR spot-x (7) .UR https://spot.lrde.epita.fr/ diff --git a/bin/spot.cc b/bin/spot.cc index 1478f1234..0cbe27f16 100644 --- a/bin/spot.cc +++ b/bin/spot.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -39,6 +39,7 @@ static const argp_option options[] = "reproduce a bug.") }, { nullptr, 0, nullptr, 0, "Tools that output automata:", 0 }, { DOC("randaut", "Generate random ω-automata.") }, + { DOC("genaut", "Generate ω from scalable patterns.") }, { DOC("ltl2tgba", "Convert LTL or PSL into variants of Transition-based " "Generalized Büchi Automata.") }, { DOC("ltl2tgta", "Convert LTL or PSL into variants of Transition-based " @@ -47,6 +48,8 @@ static const argp_option options[] = { DOC("dstar2tgba", "Convert ω-automata into variants of " "Transition-based Büchi automata.") }, { nullptr, 0, nullptr, 0, "Tools that run other tools:", 0 }, + { DOC("autcross", "Cross-compare tools processing ω-automata," + " watch for bugs, and generate statistics.") }, { DOC("ltlcross", "Cross-compare translators of LTL or PSL formulas " "into ω-automata, watch for bugs, and generate statistics.") }, { DOC("ltldo", "Wrap any tool that inputs LTL or PSL formulas and possibly " From 427c69695488ba2528b21faa29467a95f20924c7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 15 Oct 2017 18:48:00 +0200 Subject: [PATCH 06/12] org: fix the example for ltlcross --verbose * doc/org/ltlcross.org: Use SPOT_HOA_TOLERANT=1 to work around a bug in ltl3ba -H1. --- doc/org/ltlcross.org | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 64c98e0a5..e5338c0d5 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -983,21 +983,21 @@ ltlcross -f 'FGa' ltl2tgba 'ltl3ba -H1' --determinize --verbose #+END_SRC #+BEGIN_SRC sh :results verbatim :exports results -ltlcross -f 'FGa' ltl2tgba 'ltl3ba -H1' --determinize --verbose 2>&1 +SPOT_HOA_TOLERANT=1 ltlcross -f 'FGa' ltl2tgba 'ltl3ba -H1' --determinize --verbose 2>&1 #+END_SRC #+RESULTS: #+begin_example F(G(a)) -Running [P0]: ltl2tgba -H 'F(G(a))'>'lcr-o0-Ak0bYx' -Running [P1]: ltl3ba -H1 -f '<>([](a))'>'lcr-o1-5U1MyT' -Running [N0]: ltl2tgba -H '!(F(G(a)))'>'lcr-o0-sX2kaf' -Running [N1]: ltl3ba -H1 -f '!(<>([](a)))'>'lcr-o1-4siKPA' +Running [P0]: ltl2tgba -H 'F(G(a))'>'lcr-o0-opbyhq' +Running [P1]: ltl3ba -H1 -f '<>([](a))'>'lcr-o1-aP47sS' +Running [N0]: ltl2tgba -H '!(F(G(a)))'>'lcr-o0-UV1eFk' +Running [N1]: ltl3ba -H1 -f '!(<>([](a)))'>'lcr-o1-bFSrTM' info: collected automata: info: P0 (2 st.,3 ed.,1 sets) info: N0 (1 st.,2 ed.,1 sets) deterministic complete info: P1 (2 st.,3 ed.,1 sets) -info: N1 (3 st.,5 ed.,1 sets) univ-edges deterministic complete +info: N1 (3 st.,5 ed.,1 sets) univ-edges complete Performing sanity checks and gathering statistics... info: getting rid of universal edges... info: N1 (3 st.,5 ed.,1 sets) -> (2 st.,4 ed.,1 sets) @@ -1005,10 +1005,10 @@ info: complementing non-deterministic automata via determinization... info: P0 (2 st.,3 ed.,1 sets) -> (2 st.,4 ed.,2 sets) Comp(P0) info: P1 (2 st.,3 ed.,1 sets) -> (2 st.,4 ed.,2 sets) Comp(P1) info: getting rid of any Fin acceptance... -info: Comp(P0) (2 st.,4 ed.,2 sets) -> (3 st.,7 ed.,2 sets) +info: Comp(P0) (2 st.,4 ed.,2 sets) -> (2 st.,4 ed.,1 sets) info: Comp(N0) (1 st.,2 ed.,1 sets) -> (2 st.,3 ed.,1 sets) info: P1 (2 st.,3 ed.,1 sets) -> (2 st.,3 ed.,1 sets) -info: Comp(P1) (2 st.,4 ed.,2 sets) -> (4 st.,9 ed.,2 sets) +info: Comp(P1) (2 st.,4 ed.,2 sets) -> (2 st.,4 ed.,1 sets) info: Comp(N1) (2 st.,4 ed.,1 sets) -> (3 st.,6 ed.,1 sets) info: check_empty P0*N0 info: check_empty Comp(N0)*Comp(P0) @@ -1065,21 +1065,21 @@ ltlcross -f 'FGa' ltl2tgba 'ltl3ba -H1' --verbose #+END_SRC #+BEGIN_SRC sh :results verbatim :exports results -ltlcross -f 'FGa' ltl2tgba 'ltl3ba -H1' --verbose 2>&1 +SPOT_HOA_TOLERANT=1 ltlcross -f 'FGa' ltl2tgba 'ltl3ba -H1' --verbose 2>&1 #+END_SRC #+RESULTS: #+begin_example F(G(a)) -Running [P0]: ltl2tgba -H 'F(G(a))'>'lcr-o0-jD32mW' -Running [P1]: ltl3ba -H1 -f '<>([](a))'>'lcr-o1-w6IJYI' -Running [N0]: ltl2tgba -H '!(F(G(a)))'>'lcr-o0-dac1Av' -Running [N1]: ltl3ba -H1 -f '!(<>([](a)))'>'lcr-o1-OZL7fi' +Running [P0]: ltl2tgba -H 'F(G(a))'>'lcr-o0-cq9s5c' +Running [P1]: ltl3ba -H1 -f '<>([](a))'>'lcr-o1-Fb0iii' +Running [N0]: ltl2tgba -H '!(F(G(a)))'>'lcr-o0-X5dGvn' +Running [N1]: ltl3ba -H1 -f '!(<>([](a)))'>'lcr-o1-tLO5Ks' info: collected automata: info: P0 (2 st.,3 ed.,1 sets) info: N0 (1 st.,2 ed.,1 sets) deterministic complete info: P1 (2 st.,3 ed.,1 sets) -info: N1 (3 st.,5 ed.,1 sets) univ-edges deterministic complete +info: N1 (3 st.,5 ed.,1 sets) univ-edges complete Performing sanity checks and gathering statistics... info: getting rid of universal edges... info: N1 (3 st.,5 ed.,1 sets) -> (2 st.,4 ed.,1 sets) From 1a0dcf4f69af477d8eb0bd4d6b49e4c3845aa610 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 17 Oct 2017 17:58:59 +0200 Subject: [PATCH 07/12] document the recent changes to implication rules * doc/tl/tl.tex: This adds the rules implemented in 0a2bca137 for #293. --- doc/tl/tl.tex | 122 ++++++++++++++++++++++++++++---------------------- 1 file changed, 69 insertions(+), 53 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index dbaad34ce..1670668dd 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -118,6 +118,7 @@ \newcommand{\equivM}{\stackrel{\dag}{\equiv}} \def\limplies{\rightarrow} +\def\simpe{\rightleftharpoons} \def\simp{\rightrightharpoons} \def\Simp{\stackrel{+}{\simp}} \def\liff{\leftrightarrow} @@ -1724,60 +1725,75 @@ In the following rewritings rules, $f\simp g$ means that $g$ was proved to be implied by $f$ using either of the above two methods. Additionally, implications denoted by $f\Simp g$ are only checked if the ``\verb|tl_simplifier_options::containment_checks_stronger|'' -option is set (otherwise the rewriting rule is not applied). As in -the previous section, formulas $e$ and $u$ represent respectively -pure eventualities and purely universal formulas. +option is set (otherwise the rewriting rule is not applied). We write +$f\simpe g$ iff $f\simp g$ and $f\simp f$. -\begin{equation*} -\begin{array}{cccr@{\,}l} -\text{if}& f\simp g &\text{then}& f\OR g &\equiv g \\ -\text{if}& f\simp g &\text{then}& f\AND g &\equiv f \\ -\text{if}& f\simp \NOT g &\text{then}& f\OR g &\equiv \1 \\ -\text{if}& f\simp \NOT g &\text{then}& f\AND g &\equiv \0 \\ -\text{if}& f\simp g &\text{then}& f\U g &\equiv g \\ -\text{if}& (f\U g)\Simp g &\text{then}& f\U g &\equiv g \\ -\text{if}& (\NOT f)\simp g &\text{then}& f\U g &\equiv \F g \\ -\text{if}& g\simp e &\text{then}& e\U g &\equiv \F g \\ -\text{if}& f\simp g &\text{then}& f\U (g \U h) &\equiv g \U h \\ -\text{if}& f\simp g &\text{then}& f\U (g \W h) &\equiv g \W h \\ -\text{if}& g\simp f &\text{then}& f\U (g \U h) &\equiv f \U h \\ -\text{if}& f\simp h &\text{then}& f\U (g \R (h \U k)) &\equiv g \R (h \U k) \\ -\text{if}& f\simp h &\text{then}& f\U (g \R (h \W k)) &\equiv g \R (h \W k) \\ -\text{if}& f\simp h &\text{then}& f\U (g \M (h \U k)) &\equiv g \M (h \U k) \\ -\text{if}& f\simp h &\text{then}& f\U (g \M (h \W k)) &\equiv g \M (h \W k) \\ -\text{if}& f\simp h &\text{then}& (f\U g) \U h &\equiv g \U h \\ -\text{if}& f\simp h &\text{then}& (f\W g) \U h &\equiv g \U h \\ -\text{if}& g\simp h &\text{then}& (f\U g) \U h &\equiv (f \U g) \OR h \\ -\text{if}& f\simp g &\text{then}& f\W g &\equiv g \\ -\text{if}& (f\W g)\Simp g &\text{then}& f\W g &\equiv g \\ -\text{if}& (\NOT f)\simp g &\text{then}& f\W g &\equiv \1 \\ -\text{if}& f\simp g &\text{then}& f\W (g \W h) &\equiv g \W h \\ -\text{if}& g\simp f &\text{then}& f\W (g \U h) &\equiv f \W h \\ -\text{if}& g\simp f &\text{then}& f\W (g \W h) &\equiv f \W h \\ -\text{if}& f\simp h &\text{then}& (f\U g) \W h &\equiv g \W h \\ -\text{if}& f\simp h &\text{then}& (f\W g) \W h &\equiv g \W h \\ -\text{if}& g\simp h &\text{then}& (f\W g) \W h &\equiv (f \W g) \OR h \\ -\text{if}& g\simp h &\text{then}& (f\U g) \W h &\equiv (f \U g) \OR h \\ -\text{if}& g\simp f &\text{then}& f\R g &\equiv g \\ -\text{if}& g\simp \NOT f &\text{then}& f\R g &\equiv \G g \\ -\text{if}& u\simp g &\text{then}& u\R g &\equiv \G g \\ -\text{if}& g\simp f &\text{then}& f\R (g \R h) &\equiv g \R h \\ -\text{if}& g\simp f &\text{then}& f\R (g \M h) &\equiv g \M h \\ -\text{if}& f\simp g &\text{then}& f\R (g \R h) &\equiv f \R h \\ -\text{if}& h\simp f &\text{then}& (f\R g) \R h &\equiv g \R h \\ -\text{if}& h\simp f &\text{then}& (f\M g) \R h &\equiv g \R h \\ -\text{if}& g\simp h &\text{then}& (f\R g) \R h &\equiv (f \AND g) \R h \\ -\text{if}& g\simp h &\text{then}& (f\M g) \R h &\equiv (f \AND g) \R h \\ -\text{if}& g\simp f &\text{then}& f\M g &\equiv g \\ -\text{if}& g\simp \NOT f &\text{then}& f\M g &\equiv \0 \\ -\text{if}& g\simp f &\text{then}& f\M (g \M h) &\equiv g \M h \\ -\text{if}& f\simp g &\text{then}& f\M (g \M h) &\equiv f \M h \\ -\text{if}& f\simp g &\text{then}& f\M (g \R h) &\equiv f \M h \\ -\text{if}& h\simp f &\text{then}& (f\M g) \M h &\equiv g \M h \\ -\text{if}& h\simp f &\text{then}& (f\R g) \M h &\equiv g \M h \\ -\text{if}& g\simp h &\text{then}& (f\M g) \M h &\equiv (f \AND g) \M h \\ -\end{array} -\end{equation*} +As in the previous section, formulas $e$ and $u$ represent +respectively pure eventualities and purely universal formulas. + +Finally $|f|_b$ denote the length of $f$ were all Boolean subformulas +are counted as one. + +\def\flessg{(f\simpe g) \land (|f|_b<|g|_b)} +\def\glessf{(f\simpe g) \land (|g|_b<|f|_b)} + +\begingroup +\allowdisplaybreaks +\begin{alignat*}{3} +\text{if~} & f\simp \NOT g && \text{~then~} & f\OR g & \equiv \1 \\ +\text{if~} & f\simp \NOT g && \text{~then~} & f\AND g & \equiv \0 \\ +\text{if~} & \flessg && \text{~then~} & f\OR g & \equiv f \\ +\text{if~} & f\simp g && \text{~then~} & f\OR g & \equiv g \\ +\text{if~} & \glessf && \text{~then~} & f\AND g & \equiv g \\ +\text{if~} & f\simp g && \text{~then~} & f\AND g & \equiv f \\ +\text{if~} & \flessg && \text{~then~} & f\U g & \equiv f \\ +\text{if~} & f\simp g && \text{~then~} & f\U g & \equiv g \\ +\text{if~} & (f\U g)\Simp g && \text{~then~} & f\U g & \equiv g \\ +\text{if~} & (\NOT f)\simp g && \text{~then~} & f\U g & \equiv \F g \\ +\text{if~} & g\simp e && \text{~then~} & e\U g & \equiv \F g \\ +\text{if~} & f\simp g && \text{~then~} & f\U (g \U h) & \equiv g \U h \\ +\text{if~} & f\simp g && \text{~then~} & f\U (g \W h) & \equiv g \W h \\ +\text{if~} & g\simp f && \text{~then~} & f\U (g \U h) & \equiv f \U h \\ +\text{if~} & f\simp h && \text{~then~} & f\U (g \R (h \U k)) & \equiv g \R (h \U k) \\ +\text{if~} & f\simp h && \text{~then~} & f\U (g \R (h \W k)) & \equiv g \R (h \W k) \\ +\text{if~} & f\simp h && \text{~then~} & f\U (g \M (h \U k)) & \equiv g \M (h \U k) \\ +\text{if~} & f\simp h && \text{~then~} & f\U (g \M (h \W k)) & \equiv g \M (h \W k) \\ +\text{if~} & f\simp h && \text{~then~} & (f\U g) \U h & \equiv g \U h \\ +\text{if~} & f\simp h && \text{~then~} & (f\W g) \U h & \equiv g \U h \\ +\text{if~} & g\simp h && \text{~then~} & (f\U g) \U h & \equiv (f \U g) \OR h \\ +\text{if~} & (\NOT f)\simp g && \text{~then~} & f\W g & \equiv \1 \\ +\text{if~} & \flessg && \text{~then~} & f\W g & \equiv f \\ +\text{if~} & f\simp g && \text{~then~} & f\W g & \equiv g \\ +\text{if~} & (f\W g)\Simp g && \text{~then~} & f\W g & \equiv g \\ +\text{if~} & f\simp g && \text{~then~} & f\W (g \W h) & \equiv g \W h \\ +\text{if~} & g\simp f && \text{~then~} & f\W (g \U h) & \equiv f \W h \\ +\text{if~} & g\simp f && \text{~then~} & f\W (g \W h) & \equiv f \W h \\ +\text{if~} & f\simp h && \text{~then~} & (f\U g) \W h & \equiv g \W h \\ +\text{if~} & f\simp h && \text{~then~} & (f\W g) \W h & \equiv g \W h \\ +\text{if~} & g\simp h && \text{~then~} & (f\W g) \W h & \equiv (f \W g) \OR h \\ +\text{if~} & g\simp h && \text{~then~} & (f\U g) \W h & \equiv (f \U g) \OR h \\ +\text{if~} & \flessg && \text{~then~} & f\R g & \equiv f \\ +\text{if~} & g\simp f && \text{~then~} & f\R g & \equiv g \\ +\text{if~} & g\simp \NOT f && \text{~then~} & f\R g & \equiv \G g \\ +\text{if~} & u\simp g && \text{~then~} & u\R g & \equiv \G g \\ +\text{if~} & g\simp f && \text{~then~} & f\R (g \R h) & \equiv g \R h \\ +\text{if~} & g\simp f && \text{~then~} & f\R (g \M h) & \equiv g \M h \\ +\text{if~} & f\simp g && \text{~then~} & f\R (g \R h) & \equiv f \R h \\ +\text{if~} & h\simp f && \text{~then~} & (f\R g) \R h & \equiv g \R h \\ +\text{if~} & h\simp f && \text{~then~} & (f\M g) \R h & \equiv g \R h \\ +\text{if~} & g\simp h && \text{~then~} & (f\R g) \R h & \equiv (f \AND g) \R h \\ +\text{if~} & g\simp h && \text{~then~} & (f\M g) \R h & \equiv (f \AND g) \R h \\ +\text{if~} & \flessg && \text{~then~} & f\M g & \equiv f \\ +\text{if~} & g\simp f && \text{~then~} & f\M g & \equiv g \\ +\text{if~} & g\simp \NOT f && \text{~then~} & f\M g & \equiv \0 \\ +\text{if~} & g\simp f && \text{~then~} & f\M (g \M h) & \equiv g \M h \\ +\text{if~} & f\simp g && \text{~then~} & f\M (g \M h) & \equiv f \M h \\ +\text{if~} & f\simp g && \text{~then~} & f\M (g \R h) & \equiv f \M h \\ +\text{if~} & h\simp f && \text{~then~} & (f\M g) \M h & \equiv g \M h \\ +\text{if~} & h\simp f && \text{~then~} & (f\R g) \M h & \equiv g \M h \\ +\text{if~} & g\simp h && \text{~then~} & (f\M g) \M h & \equiv (f \AND g) \M h \\ +\end{alignat*} +\endgroup Many of the above rules were collected from the literature~\cite{somenzi.00.cav,tauriainen.03.a83,babiak.12.tacas} and From d597c58106a9f4d14ba3fd40396a670b6dd3e3e5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 18 Oct 2017 14:59:29 +0200 Subject: [PATCH 08/12] org: improve wording * doc/org/tut04.org: This tests equivalence, not equality. --- doc/org/tut04.org | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/doc/org/tut04.org b/doc/org/tut04.org index b4ced9a03..536eff066 100644 --- a/doc/org/tut04.org +++ b/doc/org/tut04.org @@ -4,7 +4,8 @@ #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html -This page shows how to test whether two LTL/PSL formulas are equal. +This page shows how to test whether two LTL/PSL formulas are +equivalent, i.e., if they denote the same languages. * Shell From 7510743b47f6329b22d4f3d3cc7ba6302e993a5d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 23 Oct 2017 17:58:32 +0200 Subject: [PATCH 09/12] org: update for gpg-signed Debian repository * doc/org/install.org: Mention the GPG key. --- doc/org/install.org | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/doc/org/install.org b/doc/org/install.org index 95f55b6be..51d6b7d51 100644 --- a/doc/org/install.org +++ b/doc/org/install.org @@ -61,6 +61,7 @@ for Sid (a.k.a. Debian unstable). Here is how to install the stable packages: #+BEGIN_SRC sh +wget -q -O - https://www.lrde.epita.fr/repo/debian.gpg | apt-key add - echo 'deb http://www.lrde.epita.fr/repo/debian/ stable/' >> /etc/apt/sources.list apt-get update apt-get install spot libspot-dev spot-doc python3-spot # Or a subset of those @@ -69,11 +70,17 @@ apt-get install spot libspot-dev spot-doc python3-spot # Or a subset of those Here is how to install the unstable packages: #+BEGIN_SRC sh +wget -q -O - https://www.lrde.epita.fr/repo/debian.gpg | apt-key add - echo 'deb http://www.lrde.epita.fr/repo/debian/ unstable/' >> /etc/apt/sources.list apt-get update apt-get install spot libspot-dev spot-doc python3-spot # Or a subset of those #+END_SRC +Note that our Debian repository is signed since that is the new Debian +policy, and both of the above command blocks start with a download of +our [[https://www.lrde.epita.fr/repo/debian.gpg][GPG key]]. Its fingerprint is =209B 7362 CFD6 FECF B41D 717F 03D9 +9E74 44F2 A84A=, if you want to verify it. + The package =spot= contains the [[file:tools.org][command-line tools]]. =libspot-dev= contains the header files if you plan to use Spot in a C++14 program. =spot-doc= contains some html (including these pages) and pdf @@ -83,8 +90,6 @@ examples). The packages containing the libraries (=libspot0=, =libbddx0=, =libspotltsmin0=) are automatically installed as dependencies of the previous packages. -#+END_SRC - * Installing from git The =master= branch of the git repository contains the code for the From 8d461b25bdda88a198914b8180c6c1c55fd0e735 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 19 Oct 2017 11:45:44 +0200 Subject: [PATCH 10/12] bin: add shorthand for ltl3tela That's the new name of ltl3hoa. * bin/common_trans.cc: Add it. --- bin/common_trans.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/bin/common_trans.cc b/bin/common_trans.cc index 20c8ca495..dba69ef38 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -54,6 +54,8 @@ static shorthands_t shorthands_ltl[] = { { "ltl3ba", " -f %s>%O" }, { "ltl3dra", " -f %s>%O" }, { "ltl3hoa", " -f %f>%O" }, + // ltl3tela is the new name of ltl3hoa + { "ltl3tela", " -f %f>%O" }, { "modella", " %[MWei^]L %O" }, { "spin", " -f %s>%O" }, }; From ed5463cf6f09cfb7f0531177f83d192058ef0097 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 7 Nov 2017 07:44:27 +0100 Subject: [PATCH 11/12] Release Spot 2.4.2 * NEWS, configure.ac, doc/org/setup.org: Update. --- NEWS | 6 +++++- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 11 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index c3e22a033..28be2fa88 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,8 @@ -New in spot 2.4.1.dev (not yet released) +New in spot 2.4.2 (2017-11-07) + + Tools: + + - ltlcross and ltldo support ltl3tela, the new name of ltl3hoa. Bugs fixed: diff --git a/configure.ac b/configure.ac index 27c20f27a..3f91f50db 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.4.1.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.4.2], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) diff --git a/doc/org/setup.org b/doc/org/setup.org index f3a078913..a59a432b3 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,8 +1,8 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.4.1 -#+MACRO: LASTRELEASE 2.4.1 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.4.1.tar.gz][=spot-2.4.1.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-4-1/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2017-10-05 +#+MACRO: SPOTVERSION 2.4.2 +#+MACRO: LASTRELEASE 2.4.2 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.4.2.tar.gz][=spot-2.4.2.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-4-2/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2017-11-07 From 7c8d52640ea8a2a2d2ad4a0b2d1304582b70665a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 7 Nov 2017 07:46:53 +0100 Subject: [PATCH 12/12] Bump version to 2.4.2.dev * configure.ac, NEWS: Here. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 28be2fa88..7ac09a585 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.4.2.dev (not yet released) + + Nothing yet. + New in spot 2.4.2 (2017-11-07) Tools: diff --git a/configure.ac b/configure.ac index 3f91f50db..420b42df2 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.4.2], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.4.2.dev], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])