From f3657a676306e13e0e92787313f6d1f96f104996 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 19 Apr 2019 17:19:39 +0200 Subject: [PATCH 01/10] * doc/org/ltlcross.org: Fix ltlcross.csv example. --- doc/org/ltlcross.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 6febcb1b6..12593f0fb 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -708,7 +708,7 @@ looking whether the command specification for a translator has the form "={short name}actual command=". For instance, after -#+BEGIN_SRC sh :exports code +#+BEGIN_SRC sh :results silent genltl --and-f=1..5 | ltlcross '{small} ltl2tgba -s --small %f >%O' \ '{deter} ltl2tgba -s --deter %f >%O' --csv=ltlcross.csv From e7ac892d32ca7c7bcc4dd693bbfa76696f99c020 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 23 Apr 2019 23:08:00 +0200 Subject: [PATCH 02/10] man: minor fixes * bin/man/spot-x.x, bin/man/dstar2tgba.x, bin/spot-x.cc: Cosmetics changes. * bin/man/README: New file. --- bin/man/README | 14 ++++++++++++++ bin/man/dstar2tgba.x | 8 ++++++-- bin/man/spot-x.x | 24 +++++++++++++++--------- bin/spot-x.cc | 6 +++--- 4 files changed, 38 insertions(+), 14 deletions(-) create mode 100644 bin/man/README diff --git a/bin/man/README b/bin/man/README new file mode 100644 index 000000000..711b5ca8a --- /dev/null +++ b/bin/man/README @@ -0,0 +1,14 @@ +To help with keeping man pages in sync with the binaries, the man page +for PROGRAM is automatically generated from two sources: + 1. the --help output of bin/PROGRAM, + 2. the bin/man/PROGRAM.x file + +The tool help2man is responsible for doing this conversion. + +The PROGRAM.x file has [sections] headers to indicate sections. The +rest of the file uses groff macros for man pages. For detail on this +syntax, run "man groff_man". + +Note that some of the standard sections will be forced to the top or +bottom of the manpage by help2man, the rest will appear as ordered in +PROGRAM.x. diff --git a/bin/man/dstar2tgba.x b/bin/man/dstar2tgba.x index bb0b2e384..e5318bc0e 100644 --- a/bin/man/dstar2tgba.x +++ b/bin/man/dstar2tgba.x @@ -60,9 +60,13 @@ would make more sense. [BIBLIOGRAPHY] .TP 1. - +.UR http://www.ltl2dstar.de/docs/ltl2dstar.html +The +.BR ltl2dstar manual +.UE . -Documents the output format of ltl2dstar. +Documents the output format of +.BR ltl2dstar . .TP 2. diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x index e6c534cec..d0e6e94ab 100644 --- a/bin/man/spot-x.x +++ b/bin/man/spot-x.x @@ -55,17 +55,15 @@ convenient when chaining tools in a pipe. Set this variable to passed to the printer by suffixing the output format with \fB=\fR and the options. For instance running .in +4n -.nf -.ft C +.EX % SPOT_DEFAULT_FORMAT=dot=bar autfilt ... -.fi +.EN .in -4n is the same as running .in +4n -.nf -.ft C +.EX % autfilt --dot=bar ... -.fi +.EE .in -4n but the use of the environment variable makes more sense if you set it up once for many commands. @@ -105,6 +103,7 @@ Specifies the default algorithm that should be used by the \f(CWis_obligation()\fR function. The value should be one of the following: .RS +.RS .IP 1 Make sure that the formula and its negation are realizable by non-deterministic co-Büchi automata. @@ -115,6 +114,7 @@ realizable by deterministic Büchi automata. Make sure that the formula is realizable by a weak and deterministic Büchi automata. .RE +.RE .TP \fBSPOT_OOM_ABORT\fR @@ -134,9 +134,12 @@ ignoring them), and setting this variable will interfer with that. Select the default algorithm that must be used to check the persistence or recurrence property of a formula f. The values it can take are 1 or 2. Both methods work either on f or !f thanks to the duality of -persistence and recurrence classes. -See "https://spot.lrde.epita.fr/hierarchy.html" for more details. If -it is set to: +persistence and recurrence classes. See +.UR https://spot.lrde.epita.fr/hierarchy.html +this page +.UE +for more details. If it is set to: +.RS .RS .IP 1 It will try to check if f (or !f) is co-Büchi realizable in order to @@ -145,6 +148,7 @@ tell if f belongs to the persistence (or the recurrence) class. It checks if f (or !f) is det-Büchi realizable to tell if f belongs to the recurrence (or the persistence) class. .RE +.RE .TP \fBSPOT_SATLOG\fR @@ -202,6 +206,7 @@ variable should hold a value between 1 and 8, corresponding to the following tests described in our Spin'15 paper (see the BIBLIOGRAPHY section). The default is 8. .RS +.RS .IP 1 sl(a) x sl(!a) .IP 2 @@ -219,6 +224,7 @@ sl(a) x sl(!a), performed on-the-fly .IP 8 cl(a) x cl(!a) .RE +.RE .TP \fBSPOT_TMPDIR\fR, \fBTMPDIR\fR diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 7225d751c..10acb4219 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -43,7 +43,7 @@ static const argp_option options[] = (0) disables it, (1) enables rules based on syntactic implications, \ (2) additionally allows automata-based implication checks, (3) enables \ more rules based on automata-based implication checks. The default value \ -depends on the --low/--medium/--high settings.") }, +depends on the --low, --medium, or --high settings.") }, { nullptr, 0, nullptr, 0, "Translation options:", 0 }, { DOC("ltl-split", "Set to 0 to disable the translation of automata \ as product or sum of subformulas.") }, From 936481dcbd5fd2804b99e656a0ce9cb597ebb845 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 26 Apr 2019 10:05:45 +0200 Subject: [PATCH 03/10] * bin/spot-x.cc (ba-simul): Update documentation. --- bin/spot-x.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 10acb4219..8fc759f54 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -122,7 +122,10 @@ simulation. Set to 3 to iterate both direct and reverse simulations. \ The default is 3, except when option --low is specified, in which case \ the default is 1.") }, { DOC("ba-simul", "Set to 0 to disable simulation-based reductions \ -on the Büchi automaton (i.e., after degeneralization has been performed). \ +on automata where state-based acceptance must be preserved (e.g., \ +after degeneralization has been performed). The name suggests this applies \ +only to Büchi automata for historical reasons; it really applies to any \ +state-based acceptance nowadays. \ Set to 1 to use only direct simulation. Set to 2 to use only reverse \ simulation. Set to 3 to iterate both direct and reverse simulations. \ The default is 3 in --high mode, and 0 otherwise.") }, From 26e2f9cec8932c989fe492ae589ad7dd4532ba19 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 26 Apr 2019 11:27:11 +0200 Subject: [PATCH 04/10] sepsets: fix infinite loop * tests/core/sepsets.test: New test case. * spot/twaalgos/sepsets.cc: Fix the code. * NEWS: Mention the problem. --- NEWS | 5 ++++- spot/twaalgos/sepsets.cc | 19 +++++++++---------- tests/core/sepsets.test | 22 +++++++++++++++++++++- 3 files changed, 34 insertions(+), 12 deletions(-) diff --git a/NEWS b/NEWS index 0a6ea570c..bc38b8b1c 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,9 @@ New in spot 2.7.3.dev (not yet released) - Nothing yet. + Bugs fixed: + + - separate_sets_here() (and therefore autfilt --separate-sets) could + loop infinitely on some inputs. New in spot 2.7.3 (2019-04-19) diff --git a/spot/twaalgos/sepsets.cc b/spot/twaalgos/sepsets.cc index 001e88f36..cce0c935e 100644 --- a/spot/twaalgos/sepsets.cc +++ b/spot/twaalgos/sepsets.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2018 Laboratoire de Recherche et +// Copyright (C) 2015-2019 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -56,7 +56,7 @@ namespace spot // Fix the acceptance condition auto& code = aut->acc().get_acceptance(); // If code were empty, then common would have been 0. - assert (!code.empty()); + assert(!code.empty()); acc_cond::acc_word* pos = &code.back(); acc_cond::acc_word* start = &code.front(); while (pos > start) @@ -69,14 +69,13 @@ namespace spot break; case acc_cond::acc_op::Fin: case acc_cond::acc_op::FinNeg: - if (!(pos[-1].mark & common)) - break; - for (auto p: map) - if (pos[-1].mark & p.first) - { - pos[-1].mark -= p.first; - pos[-1].mark |= p.second; - } + if (pos[-1].mark & common) + for (auto p: map) + if (pos[-1].mark & p.first) + { + pos[-1].mark -= p.first; + pos[-1].mark |= p.second; + } SPOT_FALLTHROUGH; case acc_cond::acc_op::Inf: case acc_cond::acc_op::InfNeg: diff --git a/tests/core/sepsets.test b/tests/core/sepsets.test index 055544c7a..9957da874 100755 --- a/tests/core/sepsets.test +++ b/tests/core/sepsets.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015 Laboratoire de Recherche et Développement de +# Copyright (C) 2015, 2019 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -39,6 +39,16 @@ State: 2 [!0&1&!2] 1 [0&!2] 2 {0 1} --END-- +HOA: v1 +States: 1 +Start: 0 +AP: 3 "p0" "p1" "p2" +Acceptance: 3 (Fin(1) | Inf(0)) & (Fin(2) | Inf(1)) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 {0 1 2} +[0&!1&!2] 0 +--END-- EOF cat >expected < out From b928d8c82abe16b16c93aa0256f64170120494e4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 26 Apr 2019 11:33:04 +0200 Subject: [PATCH 05/10] fix "requires separate Inf and Fin sets" error from ltl2tgba -G MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Report from David Müller. * spot/twaalgos/simulation.cc: Add wrapper to deal with automata sharing Fin/Inf sets. * tests/core/ltl2tgba2.test: New test cases. * NEWS: Mention the change. --- NEWS | 5 ++++ spot/twaalgos/simulation.cc | 52 ++++++++++++++++++++++++++++--------- tests/core/ltl2tgba2.test | 13 ++++++++++ 3 files changed, 58 insertions(+), 12 deletions(-) diff --git a/NEWS b/NEWS index bc38b8b1c..3c08bff40 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,11 @@ New in spot 2.7.3.dev (not yet released) - separate_sets_here() (and therefore autfilt --separate-sets) could loop infinitely on some inputs. + - In some situation, ltl2tgba -G could abort with + "direct_simulation() requires separate Inf and Fin sets". This + was fixed by teaching simulation-based reductions how to deal + with such cases. + New in spot 2.7.3 (2019-04-19) Bugs fixed: diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index 5a96d8a76..9cbe1a675 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -30,6 +30,7 @@ #include #include #include +#include // Simulation-based reduction, implemented using bdd-based signatures. // @@ -710,43 +711,70 @@ namespace spot const const_twa_graph_ptr original_; }; + template + twa_graph_ptr + wrap_simul(Fun f, const Aut& a) + { + if (has_separate_sets(a)) + return f(a); + // If the input has acceptance sets common to Fin and Inf, + // separate them before doing the simulation, and merge them + // back afterwards. Doing will temporarily introduce more sets + // and may exceed the number of sets we support. But it's + // better than refusing to apply simulation-based reductions to + // automata sharing Fin/Inf sets. + auto b = make_twa_graph(a, twa::prop_set::all()); + separate_sets_here(b); + return simplify_acceptance_here(f(b)); + } + } // End namespace anonymous. twa_graph_ptr simulation(const const_twa_graph_ptr& t) { - direct_simulation simul(t); - return simul.run(); + return wrap_simul([](const const_twa_graph_ptr& t) { + direct_simulation simul(t); + return simul.run(); + }, t); } twa_graph_ptr simulation(const const_twa_graph_ptr& t, std::vector* implications) { - direct_simulation simul(t); - return simul.run(implications); + return wrap_simul([implications](const const_twa_graph_ptr& t) { + direct_simulation simul(t); + return simul.run(implications); + }, t); } twa_graph_ptr simulation_sba(const const_twa_graph_ptr& t) { - direct_simulation simul(t); - return simul.run(); + return wrap_simul([](const const_twa_graph_ptr& t) { + direct_simulation simul(t); + return simul.run(); + }, t); } twa_graph_ptr cosimulation(const const_twa_graph_ptr& t) { - direct_simulation simul(t); - return simul.run(); + return wrap_simul([](const const_twa_graph_ptr& t) { + direct_simulation simul(t); + return simul.run(); + }, t); } twa_graph_ptr cosimulation_sba(const const_twa_graph_ptr& t) { - direct_simulation simul(t); - return simul.run(); + return wrap_simul([](const const_twa_graph_ptr& t) { + direct_simulation simul(t); + return simul.run(); + }, t); } @@ -783,13 +811,13 @@ namespace spot twa_graph_ptr iterated_simulations(const const_twa_graph_ptr& t) { - return iterated_simulations_(t); + return wrap_simul(iterated_simulations_, t); } twa_graph_ptr iterated_simulations_sba(const const_twa_graph_ptr& t) { - return iterated_simulations_(t); + return wrap_simul(iterated_simulations_, t); } } // End namespace spot. diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 11b022023..9c9e695bf 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -409,3 +409,16 @@ f='(a R !b) & (c R !d) & G((!b | !d) & (!a | Fb) & (!c | Fd) ' f=$f'& (!b | X(b | (a R !b))) & (!d | X(d | (c R !d))) & F(a | !b) & F(c | !d))' test '8,1' = `ltl2tgba "$f" --stats=%s,%d` test '8,1' = `ltl2tgba -GD "$f" --stats=%s,%d` + + +# Two formulas for which ltl2tgba 2.7.3 was raising an error with -GDS +# Reported by David Müller. +cat >in <out +cat >expected < Date: Fri, 26 Apr 2019 15:55:52 +0200 Subject: [PATCH 06/10] formula: fix syntactic-SI detection for ; operator Reported by Victor Khomenko. * spot/tl/formula.cc: Rewrite the siPSL detection for ";". * tests/core/ltlfilt.test: Add more tests. * tests/core/kind.test: Adjust. * NEWS: Mention the bug. --- NEWS | 4 ++ spot/tl/formula.cc | 30 +++++++------- tests/core/kind.test | 22 +++++----- tests/core/ltlfilt.test | 92 +++++++++++++++++++++++++++++++++++++++-- 4 files changed, 119 insertions(+), 29 deletions(-) diff --git a/NEWS b/NEWS index 3c08bff40..f4f4be734 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,10 @@ New in spot 2.7.3.dev (not yet released) was fixed by teaching simulation-based reductions how to deal with such cases. + - The code for detecting syntactically stutter-invariant PSL + formulas was incorrectly handling the ";" operator, causing some + stutter-sensitive formulas to be flagged a stutter-invariant. + New in spot 2.7.3 (2019-04-19) Bugs fixed: diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index 5d2bba518..36397d2d4 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -1125,10 +1125,9 @@ namespace spot is_.boolean = true; is_.sugar_free_boolean = true; is_.in_nenoform = true; - is_.syntactic_si = true; // Assuming LTL (for PSL a Boolean - // term is not stared will be regarded - // as not stuttering were this - // matters.) + is_.syntactic_si = true; // Assuming LTL (for PSL, a Boolean + // term that is not stared will be regarded as non-SI where + // this matters.) is_.sugar_free_ltl = true; is_.ltl_formula = true; is_.psl_formula = true; @@ -1544,9 +1543,12 @@ namespace spot is_.syntactic_si = syntactic_si; if (op_ == op::Fusion) is_.accepting_eword = false; - // A concatenation is an siSERE if it contains one stared - // Boolean, and the other operands are siSERE (i.e., - // sub-formulas that verify is_syntactic_stutter_invariant() and + // A concatenation is an siSERE if looks like + // r;b* or b*;r + // where b is Boolean and r is siSERE. generalized to n-ary + // concatenation, it means all arguments should be of the + // form b*, except one that is siSERE (i.e., a sub-formula + // that verify is_syntactic_stutter_invariant() and // !is_boolean()); if (op_ == op::Concat) { @@ -1554,22 +1556,18 @@ namespace spot for (unsigned i = 0; i < s; ++i) { auto ci = children[i]; - if (ci->is_syntactic_stutter_invariant() - && !ci->is_boolean()) - continue; - if (ci->is(op::Star)) + if (ci->is_Kleene_star()) { sb += ci->nth(0)->is_boolean(); - if (sb > 1) - break; } - else + else if (!ci->is_syntactic_stutter_invariant() + || ci->is_boolean()) { sb = 0; break; } } - is_.syntactic_si = sb == 1; + is_.syntactic_si = sb == s - 1; } break; } diff --git a/tests/core/kind.test b/tests/core/kind.test index 416eb0c1d..a7b859d97 100755 --- a/tests/core/kind.test +++ b/tests/core/kind.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2012, 2015, 2017 Laboratoire de Recherche +# Copyright (C) 2010-2012, 2015, 2017, 2019 Laboratoire de Recherche # et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -59,12 +59,13 @@ Fa -> Gb,xLPsopra {a;c*;b}|->F!b,&!Pra {a;c*;b}|->GFa,&!Pra {a;c*;b}|->FGa,&!Pa -{a[+];c[+];b*}|->!Fb,&xPsopra -{a[+];c*;b[+]}|->G!b,&!xPsopra -{a*;c[+];b[+]}|->!Gb,&xPra -{a[+];c*;b[+]}|->F!b,&!xPra -{a[+];c[+];b*}|->GFa,&!xPra -{a*;c[+];b[+]}|->FGa,&!xPa +{a[+];c[+];b*}|->!Fb,&Psopra +{a*;c[+];b*}|->!Fb,&xPsopra +{a[+];c*;b[+]}|->G!b,&!Psopra +{a*;c[+];b[+]}|->!Gb,&Pra +{a[+];c*;b[+]}|->F!b,&!Pra +{a[+];c[+];b*}|->GFa,&!Pra +{a*;c[+];b[+]}|->FGa,&!Pa {a;c;b|(d;e)}|->!Xb,&fPFsgopra {a;c;b|(d;e)}|->X!b,&!fPFsgopra {a;c;b|(d;e)}|->!Fb,&Psopra @@ -87,7 +88,7 @@ Fa -> Gb,xLPsopra {a;c*;b}<>->!GFb,&Ppa {a;c*;b}<>->GFb,&!Pa {a;c*;b}<>->!FGb,&Pa -{a*;c[+];b[+]}<>->!FGb,&xPa +{a*;c[+];b[+]}<>->!FGb,&Pa {a;c|d;b}<>->!Gb,&Pgopra {a;c|d;b}<>->G!b,&!Psopra {a;c|d;b}<>->FGb,&!Ppa @@ -126,8 +127,9 @@ Fa M b,&!xLPgopra !{a;b*;c}!,&fPsopra {a;b*;p112}[]->0,&!fPsopra !{a;b*;c.2},&!fPgopr -!{a[+];b*;c[+]},&!xfPgopra -{a[+];b*;c[+]},&!xfPsopra +!{a[+];b*;c[+]},&!fPgopra +!{a[+];b*;c*},&!xfPgopra +{a[+];b*;c[+]},&!fPsopra {a[+] && b || c[+]},&!fPsopra {a[+] && b[+] || c[+]},&!xfPsopra {p[+]:p[+]},&!xfPsoprla diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index d4d2092d5..998b5ab1a 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013-2018 Laboratoire de Recherche et Développement de +# Copyright (C) 2013-2019 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -29,7 +29,7 @@ checkopt() { cat >exp run 0 ltlfilt "$@" formulas > out - diff exp out + diff -u exp out } # The empty lines in the file are meant, we want to make sure that @@ -48,6 +48,16 @@ G(a & Xb) Xa F(a & !Xa & Xb) {a & {b|c} } + +{a[=2:3]}|->b +{a[->2:3]}|->b +{a[->1];a*}|->b /* becomes {(!a)*;a[+]}|->b */ +{a*;(!a)*;a*}|->b +{a*;(!a)[+];a*}|->b +{a[+];(!a)*;a*}|->b +{a*;(!a)*;a[+]}|->b +{a*;(!a)[+];a[+]}|->b +{a*;(!c)[+];a[+]}|->b EOF checkopt --boolean < b +{a[*];{!a}[*];a[*]}[]-> b +{a[*];{!a}[+];a[*]}[]-> b +{a[+];{!a}[*];a[*]}[]-> b +{a[*];{!a}[*];a[+]}[]-> b +{a[*];{!a}[+];a[+]}[]-> b EOF checkopt -c --stutter-invariant < b +{a[*];{!a}[+];a[*]}[]-> b +{a[+];{!a}[*];a[*]}[]-> b +{a[*];{!a}[*];a[+]}[]-> b EOF checkopt --simplify <1..2]}[]-> (b & X(b W a)))) +a R (!a | X({a[->1..2]}[]-> b)) +a R (b W !a) +{a[*];{!a}[*];a[*]}[]-> b +!a R ((b & X(b W !a)) W a) +(b & X((b W !a) & ((b & X(b W !a)) W a))) W !a +!a R (a R (b W !a)) +!a R (a | X(a R (b W !a))) +!a R (c | X(c R (b W !a))) EOF checkopt --simplify --eventual --unique < b +{a[->2..3]}[]-> b +{{!a}[*];a[+]}[]-> b +{a[*];{!a}[*];a[*]}[]-> b +{a[*];{!a}[+];a[*]}[]-> b +{a[+];{!a}[*];a[*]}[]-> b +{a[*];{!a}[*];a[+]}[]-> b +{a[*];{!a}[+];a[+]}[]-> b +{a[*];{!c}[+];a[+]}[]-> b EOF checkopt --obligation < b +{a[->2..3]}[]-> b +{{!a}[*];a[+]}[]-> b +{a[*];{!a}[*];a[*]}[]-> b +{a[*];{!a}[+];a[*]}[]-> b +{a[+];{!a}[*];a[*]}[]-> b +{a[*];{!a}[*];a[+]}[]-> b +{a[*];{!a}[+];a[+]}[]-> b +{a[*];{!c}[+];a[+]}[]-> b EOF checkopt --guarantee < b +{a[->2..3]}[]-> b +{{!a}[*];a[+]}[]-> b +{a[*];{!a}[*];a[*]}[]-> b +{a[*];{!a}[+];a[*]}[]-> b +{a[+];{!a}[*];a[*]}[]-> b +{a[*];{!a}[*];a[+]}[]-> b +{a[*];{!a}[+];a[+]}[]-> b +{a[*];{!c}[+];a[+]}[]-> b EOF checkopt -v --ap=3 < b +{a[->2..3]}[]-> b +{{!a}[*];a[+]}[]-> b +{a[*];{!a}[*];a[*]}[]-> b +{a[*];{!a}[+];a[*]}[]-> b +{a[+];{!a}[*];a[*]}[]-> b +{a[*];{!a}[*];a[+]}[]-> b +{a[*];{!a}[+];a[+]}[]-> b EOF checkopt --ap=2..3 < b +{a[->2..3]}[]-> b +{{!a}[*];a[+]}[]-> b +{a[*];{!a}[*];a[*]}[]-> b +{a[*];{!a}[+];a[*]}[]-> b +{a[+];{!a}[*];a[*]}[]-> b +{a[*];{!a}[*];a[+]}[]-> b +{a[*];{!a}[+];a[+]}[]-> b +{a[*];{!c}[+];a[+]}[]-> b EOF checkopt -v --stutter-invariant < b +{a[->2..3]}[]-> b +{a[*];{!c}[+];a[+]}[]-> b EOF checkopt --equivalent-to 'GFa | FGb' < Date: Fri, 26 Apr 2019 22:14:19 +0200 Subject: [PATCH 07/10] formula: b* is siSERE Since b[+] and [*0] are siSERE, b* is siSERE as well. Suggested by Victor Khomenko. * spot/tl/formula.cc: Implement that for Star and also in the concatenation rule. * tests/core/kind.test, tests/core/ltlfilt.test: Adjust. --- spot/tl/formula.cc | 7 ++++--- tests/core/kind.test | 2 +- tests/core/ltlfilt.test | 1 + 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index 36397d2d4..707c62d0f 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1549,7 +1549,8 @@ namespace spot // concatenation, it means all arguments should be of the // form b*, except one that is siSERE (i.e., a sub-formula // that verify is_syntactic_stutter_invariant() and - // !is_boolean()); + // !is_boolean()). Since b* is siSERE, that means we + // want at least s-1 operands of the form b*. if (op_ == op::Concat) { unsigned sb = 0; // stared Boolean formulas seen @@ -1567,7 +1568,7 @@ namespace spot break; } } - is_.syntactic_si = sb == s - 1; + is_.syntactic_si = sb >= s - 1; } break; } @@ -1594,7 +1595,7 @@ namespace spot if (max_ == unbounded()) { is_.finite = false; - is_.syntactic_si = min_ == 1 && children[0]->is_boolean(); + is_.syntactic_si = min_ <= 1 && children[0]->is_boolean(); } else { diff --git a/tests/core/kind.test b/tests/core/kind.test index a7b859d97..e07fd02b9 100755 --- a/tests/core/kind.test +++ b/tests/core/kind.test @@ -135,7 +135,7 @@ Fa M b,&!xLPgopra {p[+]:p[+]},&!xfPsoprla (!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla {b[+][:*0..3]},&!fPsopra -{a->c[*]},fPsopra +{a->c[*]},xfPsopra EOF run 0 ../kind input diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index 998b5ab1a..5c10a1b0e 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -130,6 +130,7 @@ b W GFa a U Fb a & (b | c) {{!a}[*];a[+]}[]-> b +{a[*];{!a}[*];a[*]}[]-> b {a[*];{!a}[+];a[*]}[]-> b {a[+];{!a}[*];a[*]}[]-> b {a[*];{!a}[*];a[+]}[]-> b From ba89cb5db5833f88e3e0a8c3fd58e4f0bc2d7ca0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 26 Apr 2019 23:01:43 +0200 Subject: [PATCH 08/10] * THANKS: Add Victor Khomenko. --- THANKS | 1 + 1 file changed, 1 insertion(+) diff --git a/THANKS b/THANKS index 84ad867bd..e5c564715 100644 --- a/THANKS +++ b/THANKS @@ -46,6 +46,7 @@ Tereza Šťastná Tobias Meggendorfer. Tomáš Babiak Valentin Iovene +Victor Khomenko Vitus Lam Yann Thierry-Mieg Yannick Molinghen From 90e5f6ed7d81047ba48913bc87b72d08dc4dd1fa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 27 Apr 2019 06:25:21 +0200 Subject: [PATCH 09/10] Release Spot 2.7.4 * doc/org/setup.org, configure.ac, NEWS: Update version. --- NEWS | 2 +- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index f4f4be734..9de534c6f 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.7.3.dev (not yet released) +New in spot 2.7.4 (2019-04-27) Bugs fixed: diff --git a/configure.ac b/configure.ac index c98284cf1..e7cd3d3b6 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.7.3.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.7.4], [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 6cef40ea9..0309bd846 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,11 +1,11 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.7.3 -#+MACRO: LASTRELEASE 2.7.3 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.7.3.tar.gz][=spot-2.7.3.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-7-3/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2019-04-19 +#+MACRO: SPOTVERSION 2.7.4 +#+MACRO: LASTRELEASE 2.7.4 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.7.4.tar.gz][=spot-2.7.4.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-7-4/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2019-04-27 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From 09d9e0c52a534470c04eb882b4f521d7f77671d2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 27 Apr 2019 06:28:04 +0200 Subject: [PATCH 10/10] Bump version to 2.7.4.dev * NEWS, configure.ac: Here. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 9de534c6f..38f926b82 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.7.4.dev (not yet released) + + Nothing yet. + New in spot 2.7.4 (2019-04-27) Bugs fixed: diff --git a/configure.ac b/configure.ac index e7cd3d3b6..d0173ec98 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.7.4], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.7.4.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])