diff --git a/NEWS b/NEWS index bd6265530..db61afd3b 100644 --- a/NEWS +++ b/NEWS @@ -24,6 +24,12 @@ New in spot 2.7.5.dev (not yet released) - genaut learned --m-nba=N to generate Max Michel's NBA familly. (NBAs with N+1 states whose determinized have at least N! states.) + - Due to some new simplification of parity acceptance, the output of + "ltl2tgba -P -D" is now using a minimal number of colors. This + means that recurrence properties have an acceptance condition + amongst "Inf(0)", "t", or "f", and persistance properties have an + acceptance condition among "Fin(0)", "t", or "f". + Library: - Add generic_accepting_run() as a variant of generic_emptiness_check() that @@ -117,6 +123,13 @@ New in spot 2.7.5.dev (not yet released) - The postprocessor and translator classes are now using reduce_parity() for further simplifications. + - The code for checking recurrence/persistence properties can also + use the fact the reduce_parity() with return "Inf(0)" (or "t" or + "f") for deterministic automata corresponding to recurrence + properties, and "Fin(0)" (or "t" or "f") for persistence + properties. This can be altered with the SPOT_PR_CHECK + environment variable. + New in spot 2.7.5 (2019-06-05) Build: diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x index d0e6e94ab..a243b34b1 100644 --- a/bin/man/spot-x.x +++ b/bin/man/spot-x.x @@ -132,8 +132,8 @@ ignoring them), and setting this variable will interfer with that. .TP \fBSPOT_PR_CHECK\fR 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 +or recurrence property of a formula f. The values it can take are between +1 and 3. All methods work either on f or !f thanks to the duality of persistence and recurrence classes. See .UR https://spot.lrde.epita.fr/hierarchy.html this page @@ -145,8 +145,13 @@ for more details. If it is set to: It will try to check if f (or !f) is co-Büchi realizable in order to tell if f belongs to the persistence (or the recurrence) class. .IP 2 -It checks if f (or !f) is det-Büchi realizable to tell if f belongs -to the recurrence (or the persistence) class. +It checks if f (or !f) is det-Büchi realizable via a reduction +to deterministic-Rabin in order to tell if f belongs to the +recurrence (or the persistance) class. +.IP 3 +It checks if f (or !f) is det-Büchi realizable via a reduction +to deterministic-parity in order to tell if f belongs to the +recurrence (or the persistance) class. .RE .RE diff --git a/doc/org/hierarchy.org b/doc/org/hierarchy.org index b19a6ab68..b0c0e4d80 100644 --- a/doc/org/hierarchy.org +++ b/doc/org/hierarchy.org @@ -520,7 +520,7 @@ automata. For the subclass of /obligation/ properties, using =-D= is a sure way to obain a deterministic automaton (and even a minimal one), but for the /recurrence/ properties that are not /obligations/ the translator -does not make any special effort to produce deterministic automata, +does not make /too much/ effort to produce deterministic automata, even with =-D= (this might change in the future). All properties that are not in the /persistence/ class (this includes @@ -585,106 +585,40 @@ $txt [[file:hier-recurrence-3.svg]] One way to obtain a deterministic Büchi automaton (it has to exist, since this is -a /recurrence/ property), is to chain a few algorithms implemented in Spot: +a /recurrence/ property), is to request a deterministic automaton with parity +acceptance using =-P=. The number of color output with =-P= is always reduced +to the minimal number possible, so for a /recurrence/ property the output +automaton can only have one of three possible acceptance: =Inf(0)=, =t=, or =f=. - 1. Determinize the non-deterministic automaton to obtain a - deterministic automaton with parity acceptance: this is done by - using =ltl2tgba -P -D=, with option =-P= indicating that parity - acceptance is desired. - - #+NAME: hier-recurrence-4 - #+BEGIN_SRC sh :exports code - ltl2tgba -P -D 'G(Gb | Fa)' -d - #+END_SRC - #+BEGIN_SRC dot :file hier-recurrence-4.svg :var txt=hier-recurrence-4 :exports results - $txt - #+END_SRC - #+RESULTS: - [[file:hier-recurrence-4.svg]] - - 2. Transform the parity acceptance into Rabin acceptance: this is - done with =autfilt --generalized-rabin=. Because of the type of - parity acceptance used, the result will actually be Rabin and not - generalized Rabin. - - #+NAME: hier-recurrence-5 - #+BEGIN_SRC sh :exports code - ltl2tgba -P -D 'G(Gb | Fa)' | - autfilt --generalized-rabin -d - #+END_SRC - #+BEGIN_SRC dot :file hier-recurrence-5.svg :var txt=hier-recurrence-5 :exports results - $txt - #+END_SRC - - #+RESULTS: - [[file:hier-recurrence-5.svg]] - - (The only change here is in the acceptance condition.) - - 3. In step 4 we are going to convert the automaton to state-based - Büchi, and this sometimes works better if the input Rabin automaton - also uses state-based acceptance. So let us add =-S= to the - previous command: - - #+NAME: hier-recurrence-6 - #+BEGIN_SRC sh :results verbatim :exports code - ltl2tgba -P -D 'G(Gb | Fa)' | - autfilt -S --generalized-rabin -d - #+END_SRC - - #+BEGIN_SRC dot :file hier-recurrence-6.svg :var txt=hier-recurrence-6 :exports results - $txt - #+END_SRC - - #+RESULTS: - [[file:hier-recurrence-6.svg]] - - 4. Finally, convert the resulting automaton to BA, using =autfilt - -B=. Spot can convert automata with any acceptance condition to - BA, but when the input is a deterministic Rabin automaton, it uses - a dedicated algorithm that preserves determinism whenever possible - (and we know it is possible, because we are working on a - recurrence formula). Adding =-D= here to suggest that we are - trying to obtain a deterministic automaton does not hurt, as it - will enable simplifications as a side-effect (without =-D= we - simply get a larger deterministic automaton). - - #+NAME: hier-recurrence-7 - #+BEGIN_SRC sh :exports code - ltl2tgba -P -D 'G(Gb | Fa)' | - autfilt -S --generalized-rabin | - autfilt -B -D -d - #+END_SRC - - #+BEGIN_SRC dot :file hier-recurrence-7.svg :var txt=hier-recurrence-7 :exports results - $txt - #+END_SRC - - #+RESULTS: - [[file:hier-recurrence-7.svg]] - -Here we are lucky that the deterministic Büchi automaton is even -smaller than the original non-deterministic version. As said earlier, -passing =-S= to the first =autfilt= was optional, but in this case it -helps producing a smaller automaton. Here is what we get without it: - -#+NAME: hier-recurrence-8 +#+NAME: hier-recurrence-4 #+BEGIN_SRC sh :exports code -ltl2tgba -P -D 'G(Gb | Fa)' | - autfilt --generalized-rabin | - autfilt -B -D -d +ltl2tgba -P -D 'G(Gb | Fa)' -d #+END_SRC - -#+BEGIN_SRC dot :file hier-recurrence-8.svg :var txt=hier-recurrence-8 :exports results +#+BEGIN_SRC dot :file hier-recurrence-4.svg :var txt=hier-recurrence-4 :exports results $txt #+END_SRC - #+RESULTS: -[[file:hier-recurrence-8.svg]] +[[file:hier-recurrence-4.svg]] -It is likely that =ltl2tgba -B -D= will implement all this processing -chain in the future, but so originally =-D= was only expressing a -preference not a requirement. +Note that if the acceptance is =t=, the property is a monitor, and if +its =f=, the property is =false=. In any way, if you would like to +obtain a DBA for any recurrent property, a sure way to avoid these +difference is to pipe the result through =autfilt -B= + +#+NAME: hier-recurrence-5 +#+BEGIN_SRC sh :exports code +ltl2tgba -P -D 'G(Gb | Fa)' | autfilt -B -d +#+END_SRC +#+BEGIN_SRC dot :file hier-recurrence-5.svg :var txt=hier-recurrence-5 :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:hier-recurrence-5.svg]] + + +It is likely that =ltl2tgba -B -D= will implement these steps in the +future, but so originally =-D= was only expressing a preference not a +requirement. ** Persistence @@ -725,8 +659,9 @@ $txt Note that in this example, we know that =GFa= is trivial enough that =ltl2tgba -D GFa= will generate a deterministic automaton. In the -general case we might have to determinize the automaton as we did in -the previous section (we will do it again below). +general case we might have to determinize the automaton using =-P -D= as +we did in the previous section. For persistence properties, =-P -D= should +return an automaton whose acceptance is one of =Fin(0)=, =t=, or =f=. /Persistence/ properties can be represented by weak Büchi automata. The translator is aware of that, so when it detects that the input @@ -739,10 +674,8 @@ optimization is simply not applied.) If the input is a weak property that is not syntactically weak, the output will not necessarily be weak. One costly way to obtain a weak automaton for a formula $\varphi$ would be to first compute a -deterministic Büchi automaton of the recurrence $\lnot\varphi$ then -complement the acceptance of the resulting automaton, yielding a -deterministic co-Büchi automaton, and then transform that into a Büchi -automaton. +deterministic co-Büchi automaton $\varphi$ then transform that into a +Büchi automaton. Let's do that on the persistence formula =F(G!a | G(b U a))=, just for the fun of it. @@ -766,15 +699,11 @@ $txt #+RESULTS: [[file:hier-persistence-3.svg]] -Furthermore it appears that =ltl2tgba -D= does generate a deterministic -Büchi automaton for the complement, instead we get a non-deterministic -generalized Büchi automaton: +So let's determinize using parity acceptance: #+NAME: hier-persistence-4 #+BEGIN_SRC sh :exports code -ltlfilt --negate -f 'F(G!a | G(b U a))' | - ltl2tgba -D | - autfilt --highlight-nondet=5 -d +ltl2tgba -P -D 'F(G!a | G(b U a))' -d #+END_SRC #+BEGIN_SRC dot :file hier-persistence-4.svg :var txt=hier-persistence-4 :exports results $txt @@ -783,58 +712,16 @@ $txt #+RESULTS: [[file:hier-persistence-4.svg]] -So let us use the same tricks as in the previous section, -determinizing this automaton into a Rabin automaton, and then back to -deterministic Büchi: - -#+NAME: hier-persistence-5 -#+BEGIN_SRC sh :exports code -ltlfilt --negate -f 'F(G!a | G(b U a))' | - ltl2tgba -P -D | - autfilt --generalized-rabin | - autfilt --tgba -D -d -#+END_SRC -#+BEGIN_SRC dot :file hier-persistence-5.svg :var txt=hier-persistence-5 :exports results -$txt -#+END_SRC - -#+RESULTS: -[[file:hier-persistence-5.svg]] - -This is a deterministic Büchi automaton for the negation of our formula. -Now we can complement it to obtain a deterministic co-Büchi automaton for =F(G!a | G(b U a))=: - -#+NAME: hier-persistence-6 -#+BEGIN_SRC sh :exports code -ltlfilt --negate -f 'F(G!a | G(b U a))' | - ltl2tgba -P -D | - autfilt --generalized-rabin | - autfilt --tgba -D | - autfilt --complement -d -#+END_SRC - -#+BEGIN_SRC dot :file hier-persistence-6.svg :var txt=hier-persistence-6 :exports results -$txt -#+END_SRC - -#+RESULTS: -[[file:hier-persistence-6.svg]] - -And finally we convert the result back to Büchi: +And finally we convert the result back to Büchi with =autfilt -B=. #+NAME: hier-persistence-7 #+BEGIN_SRC sh :exports code -ltlfilt --negate -f 'F(G!a | G(b U a))' | - ltl2tgba -P -D | - autfilt --generalized-rabin | - autfilt --tgba -D | - autfilt --complement -B -d +ltl2tgba -P -D 'F(G!a | G(b U a))' | autfilt -B --highlight-nondet --small -d #+END_SRC - #+BEGIN_SRC dot :file hier-persistence-7.svg :var txt=hier-persistence-7 :exports results $txt #+END_SRC #+RESULTS: [[file:hier-persistence-7.svg]] -That is indeed, a weak automaton. +That is indeed, a weak non-deterministic automaton. diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc index 870a46ae6..d069fd65b 100644 --- a/spot/tl/hierarchy.cc +++ b/spot/tl/hierarchy.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de +// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement de // l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -65,79 +65,91 @@ namespace spot return !cobuchi->intersects(not_aut); } + [[noreturn]] static void invalid_spot_pr_check() + { + throw std::runtime_error("invalid value for SPOT_PR_CHECK " + "(should be 1, 2, or 3)"); + } + + static prcheck + algo_to_perform(bool is_persistence, bool aut_given) + { + static unsigned value = [&]() + { + int val; + try + { + auto s = getenv("SPOT_PR_CHECK"); + val = s ? std::stoi(s) : 0; + } + catch (const std::exception& e) + { + invalid_spot_pr_check(); + } + if (val < 0 || val > 3) + invalid_spot_pr_check(); + return val; + }(); + switch (value) + { + case 0: + if (aut_given && !is_persistence) + return prcheck::via_Parity; + else + return prcheck::via_CoBuchi; + case 1: + return prcheck::via_CoBuchi; + case 2: + return prcheck::via_Rabin; + case 3: + return prcheck::via_Parity; + default: + SPOT_UNREACHABLE(); + } + SPOT_UNREACHABLE(); + return prcheck::via_Parity; + } + static bool detbuchi_realizable(const twa_graph_ptr& aut) { if (is_universal(aut)) return true; - // if aut is a non-deterministic TGBA, we do - // TGBA->DPA->DRA->(D?)BA. The conversion from DRA to - // BA will preserve determinism if possible. + bool want_old = algo_to_perform(false, true) == prcheck::via_Rabin; + if (want_old) + { + // if aut is a non-deterministic TGBA, we do + // TGBA->DPA->DRA->(D?)BA. The conversion from DRA to + // BA will preserve determinism if possible. + spot::postprocessor p; + p.set_type(spot::postprocessor::Generic); + p.set_pref(spot::postprocessor::Deterministic); + p.set_level(spot::postprocessor::Low); + auto dpa = p.run(aut); + if (dpa->acc().is_generalized_buchi()) + { + assert(is_deterministic(dpa)); + return true; + } + else + { + auto dra = to_generalized_rabin(dpa); + return rabin_is_buchi_realizable(dra); + } + } + // Converting reduce_parity() will produce a Büchi automaton (or + // an automaton with "t" or "f" acceptance) if the parity + // automaton is DBA-realizable. spot::postprocessor p; - p.set_type(spot::postprocessor::Generic); + p.set_type(spot::postprocessor::Parity); p.set_pref(spot::postprocessor::Deterministic); p.set_level(spot::postprocessor::Low); auto dpa = p.run(aut); - if (dpa->acc().is_generalized_buchi()) - { - assert(is_deterministic(dpa)); - return true; - } - else - { - auto dra = to_generalized_rabin(dpa); - return rabin_is_buchi_realizable(dra); - } + return dpa->acc().is_f() || dpa->acc().is_generalized_buchi(); } } - [[noreturn]] static void invalid_spot_pr_check() - { - throw std::runtime_error("invalid value for SPOT_PR_CHECK " - "(should be 1 or 2)"); - } - - static prcheck - algo_to_perform(bool is_persistence, bool aut_given) - { - static prcheck env_algo = [&]() - { - int val; - try - { - auto s = getenv("SPOT_PR_CHECK"); - val = s ? std::stoi(s) : 0; - } - catch (const std::exception& e) - { - invalid_spot_pr_check(); - } - if (val == 0) - { - if (aut_given && !is_persistence) - return prcheck::via_Rabin; - else if (is_persistence || !aut_given) - return prcheck::via_CoBuchi; - else - SPOT_UNREACHABLE(); - } - else if (val == 1) - { - return prcheck::via_CoBuchi; - } - else if (val == 2) - { - return prcheck::via_Rabin; - } - else - { - invalid_spot_pr_check(); - } - }(); - return env_algo; - } - bool is_persistence(formula f, twa_graph_ptr aut, prcheck algo) { @@ -161,6 +173,7 @@ namespace spot ltl_to_tgba_fm(f, make_bdd_dict(), true)); case prcheck::via_Rabin: + case prcheck::via_Parity: return detbuchi_realizable(ltl_to_tgba_fm(formula::Not(f), make_bdd_dict(), true)); @@ -195,6 +208,7 @@ namespace spot make_bdd_dict(), true)); case prcheck::via_Rabin: + case prcheck::via_Parity: return detbuchi_realizable(aut ? aut : ltl_to_tgba_fm(f, make_bdd_dict(), true)); diff --git a/spot/tl/hierarchy.hh b/spot/tl/hierarchy.hh index 49b66aa6a..347d175f8 100644 --- a/spot/tl/hierarchy.hh +++ b/spot/tl/hierarchy.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement +// Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -37,6 +37,9 @@ namespace spot /// /// If PR_via_CoBuchi, they will check if the formula is cobuchi_realizable. /// + /// If PR_via_Parity, they will check if the formula is + /// detbuchi/cobuchi-realizable by calling reduce_parity() on a DPA. + /// /// Note that is_persistence() and is_recurrence() will work on a formula f /// or its negation because of the duality of both classes /// (see https://spot.lrde.epita.fr/hierarchy.html for details). @@ -47,6 +50,7 @@ namespace spot Auto, via_CoBuchi, via_Rabin, + via_Parity, }; /// \ingroup tl_hier diff --git a/tests/core/hierarchy.test b/tests/core/hierarchy.test index a7794c5c9..0c962d211 100755 --- a/tests/core/hierarchy.test +++ b/tests/core/hierarchy.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -70,31 +70,33 @@ ltlfilt -q --safety --guarantee -f '(Gb R (b xor Gb)) W (a W Xa)' # make sure SPOT_PR_CHECK is read. randltl -n -1 a b c | ltlfilt -v --syntactic-safety --syntactic-guarantee \ --syntactic-obligation --syntactic-recurrence --syntactic-persistence \ - -n 100 > res -cat res | SPOT_PR_CHECK=x ltlfilt --recurrence 2>err && exit 1 -cat res | SPOT_PR_CHECK=9 ltlfilt --recurrence 2>err && exit 1 + -n 500 > res +SPOT_PR_CHECK=x ltlfilt res --recurrence 2>err && exit 1 +SPOT_PR_CHECK=9 ltlfilt res --recurrence 2>err && exit 1 grep SPOT_PR_CHECK err # Testing Recurrence. -cat res | ltlfilt --recurrence > r0 -for i in 1 2; do - cat res | SPOT_PR_CHECK=$i ltlfilt --recurrence > r$i +ltlfilt res --recurrence > r0 +for i in 1 2 3; do + SPOT_PR_CHECK=$i ltlfilt res --recurrence > r$i done diff r0 r2 diff r1 r2 -cat res | ltlfilt -o %h.ltl +diff r2 r3 +ltlfilt res -o %h.ltl cat R.ltl O.ltl G.ltl S.ltl B.ltl | sort > rogsb.ltl sort r2 > r3 diff r3 rogsb.ltl # Testing Persistence. -cat res | ltlfilt --persistence > p0 -for i in 1 2; do - cat res | SPOT_PR_CHECK=$i ltlfilt --persistence > p$i +ltlfilt res --persistence > p0 +for i in 1 2 3; do + SPOT_PR_CHECK=$i ltlfilt res --persistence > p$i done diff p0 p2 diff p1 p2 -cat res | ltlfilt -o %h.ltl +diff p2 p3 +ltlfilt res -o %h.ltl cat P.ltl O.ltl G.ltl S.ltl B.ltl | sort > pogsb.ltl sort p2 > p3 diff p3 pogsb.ltl