diff --git a/NEWS b/NEWS index c3d817ac3..4b2fc5add 100644 --- a/NEWS +++ b/NEWS @@ -1,8 +1,18 @@ New in spot 1.99.4a (not yet released) + * Rename dtgba_complement() as dtwa_complement(), rename the header + as complement.hh, and restrict the purpose of this function to + just complete the automaton and complement its acceptance + condition. Any further acceptance condition transformation + can be done with to_generalized_buchi() or remove_fin(). + + * The remove_fin() has learnt how to better deal with automata that + are declared as weak. This code was previously in + dtgba_complement(). + Python: - * Add bindings for complete(). + * Add bindings for complete() and dtwa_complement() * Formulas now have a custom __format__ function. See https://spot.lrde.epita.fr/tut01.html for examples. diff --git a/bench/stutter/stutter_invariance_randomgraph.cc b/bench/stutter/stutter_invariance_randomgraph.cc index b3b22f354..1751509b5 100644 --- a/bench/stutter/stutter_invariance_randomgraph.cc +++ b/bench/stutter/stutter_invariance_randomgraph.cc @@ -19,7 +19,8 @@ #include "misc/timer.hh" #include "tl/apcollect.hh" -#include "twaalgos/dtgbacomp.hh" +#include "twaalgos/complement.hh" +#include "twaalgos/remfin.hh" #include "twaalgos/randomgraph.hh" #include "twaalgos/dot.hh" #include "twaalgos/product.hh" @@ -80,7 +81,7 @@ main(int argc, char** argv) true); } while (a->is_empty()); - auto na = spot::dtgba_complement(a); + auto na = spot::remove_fin(spot::dtwa_complement(a)); std::cout << d << ',' << props_n << ',' << seed; stats.print(a); diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 86a9b0272..8904b5d0d 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -53,7 +53,7 @@ #include "twaalgos/isweakscc.hh" #include "twaalgos/reducerun.hh" #include "twaalgos/word.hh" -#include "twaalgos/dtgbacomp.hh" +#include "twaalgos/complement.hh" #include "twaalgos/cleanacc.hh" #include "misc/formater.hh" #include "twaalgos/stats.hh" @@ -1016,7 +1016,7 @@ namespace if (!no_complement && pos[n] && ((want_stats && !(*pstats)[n].nondeterministic) || (!want_stats && is_deterministic(pos[n])))) - comp_pos[n] = dtgba_complement(pos[n]); + comp_pos[n] = dtwa_complement(pos[n]); } // ---------- Negative Formula ---------- @@ -1056,7 +1056,7 @@ namespace if (!no_complement && neg[n] && ((want_stats && !(*nstats)[n].nondeterministic) || (!want_stats && is_deterministic(neg[n])))) - comp_neg[n] = dtgba_complement(neg[n]); + comp_neg[n] = dtwa_complement(neg[n]); } } diff --git a/src/tests/dstar.test b/src/tests/dstar.test index 7e161739a..fcc7fde77 100755 --- a/src/tests/dstar.test +++ b/src/tests/dstar.test @@ -244,7 +244,7 @@ digraph G { node [shape="circle"] I [label="", style=invis, width=0] I -> 0 - 0 [label="0"] + 0 [label="0", peripheries=2] 0 -> 1 [label="!a & !b"] 0 -> 2 [label="a & !b"] 1 [label="1", peripheries=2] diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index e326272d4..bf73e6f8b 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -60,7 +60,8 @@ #include "twaalgos/simulation.hh" #include "twaalgos/compsusp.hh" #include "twaalgos/powerset.hh" -#include "twaalgos/dtgbacomp.hh" +#include "twaalgos/complement.hh" +#include "twaalgos/remfin.hh" #include "twaalgos/complete.hh" #include "twaalgos/dtbasat.hh" #include "twaalgos/dtgbasat.hh" @@ -338,7 +339,7 @@ checked_main(int argc, char** argv) bool opt_determinize = false; unsigned opt_determinize_threshold = 0; unsigned opt_o_threshold = 0; - bool opt_dtgbacomp = false; + bool opt_dtwacomp = false; bool reject_bigger = false; bool opt_monitor = false; bool containment = false; @@ -411,7 +412,7 @@ checked_main(int argc, char** argv) } else if (!strcmp(argv[formula_index], "-DC")) { - opt_dtgbacomp = true; + opt_dtwacomp = true; } else if (!strncmp(argv[formula_index], "-DS", 3) || !strncmp(argv[formula_index], "-DT", 3)) @@ -1203,14 +1204,14 @@ checked_main(int argc, char** argv) a = satminimized; } - if (opt_dtgbacomp) + if (opt_dtwacomp) { - tm.start("DTGBA complement"); - a = dtgba_complement(ensure_digraph(a)); - tm.stop("DTGBA complement"); + tm.start("DTωA complement"); + a = remove_fin(dtwa_complement(ensure_digraph(a))); + tm.stop("DTωA complement"); } - if (opt_determinize || opt_dtgbacomp || opt_dtbasat >= 0 + if (opt_determinize || opt_dtwacomp || opt_dtbasat >= 0 || opt_dtgbasat >= 0) { if (scc_filter && (reduction_dir_sim || reduction_rev_sim)) diff --git a/src/tests/ltl2dstar4.test b/src/tests/ltl2dstar4.test index 7acecfe96..6e4844c4c 100755 --- a/src/tests/ltl2dstar4.test +++ b/src/tests/ltl2dstar4.test @@ -41,13 +41,13 @@ $ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l | ltl2dstar --ltl2nba=spin:$ltl2tgba@-s $STR - - | $autfilt --tgba --stats '%S %E %A %s %e %t %a %d' | tee out -test "`cat out`" = '9 144 4 25 416 416 2 0' +test "`cat out`" = '9 144 4 25 149 416 2 0' $ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l | ltl2dstar --ltl2nba=spin:$ltl2tgba@-s $STR - - | SPOT_STREETT_CONV_MIN=1 $autfilt --tgba --stats '%S %E %A %s %e %t %a %d' | tee out -test "`cat out`" = '9 144 4 25 482 482 2 0' +test "`cat out`" = '9 144 4 25 218 482 2 0' LTL2DSTAR="ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L" diff --git a/src/tests/remfin.test b/src/tests/remfin.test index cab5644c8..22bf2d5f7 100755 --- a/src/tests/remfin.test +++ b/src/tests/remfin.test @@ -218,20 +218,13 @@ Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc --BODY-- State: 0 -[0&1] 0 -[!0&!1] 0 -[!0&1] 0 -[0&!1] 0 -[!0&!1] 1 -[!0&1] 1 -[!0&!1] 2 -[0&!1] 2 +[t] 0 +[!0] 1 +[!1] 2 State: 1 {0} -[!0&!1] 1 -[!0&1] 1 +[!0] 1 State: 2 {0} -[!0&!1] 2 -[0&!1] 2 +[!1] 2 --END-- HOA: v1 States: 4 @@ -275,7 +268,7 @@ State: 2 [!1] 0 [0&!1] 1 {0} [!0&!1] 2 {0} -[!0&!1] 3 {0} +[!0&!1] 3 State: 3 [!0&!1] 3 {0 1 4} --END-- @@ -325,31 +318,30 @@ Acceptance: 2 Inf(1) | Inf(0) properties: trans-labels explicit-labels state-acc --BODY-- State: 0 -[!0] 6 [0] 0 +[!0] 6 [0] 8 [0] 9 State: 1 {0 1} -[!0] 3 -[0] 3 +[t] 3 State: 2 {0 1} -[!0] 5 [0] 1 +[!0] 5 State: 3 {0 1} -[!0] 6 [0] 0 +[!0] 6 State: 4 {0 1} -[!0] 6 [0] 4 +[!0] 6 State: 5 {0 1} -[!0] 7 [0] 3 +[!0] 7 State: 6 -[!0] 6 [0] 0 -State: 7 {1} [!0] 6 +State: 7 {1} [0] 4 +[!0] 6 State: 8 [0] 8 State: 9 {1} @@ -547,68 +539,61 @@ Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc --BODY-- State: 0 -[0&1] 0 -[!0&!1] 0 -[!0&1] 0 -[0&!1] 0 -[!0&!1] 1 -[!0&1] 1 -[!0&!1] 2 -[0&!1] 2 +[t] 0 +[!0] 1 +[!1] 2 State: 1 {0} -[!0&!1] 1 -[!0&1] 1 +[!0] 1 State: 2 {0} -[!0&!1] 2 -[0&!1] 2 +[!1] 2 --END-- HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" -acc-name: generalized-Buchi 2 -Acceptance: 2 Inf(0)&Inf(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 -[t] 0 {0 1} -[0] 1 {0 1} -[!0] 2 {0 1} +[t] 0 {0} +[0] 1 {0} +[!0] 2 {0} State: 1 -[1] 0 {1} -[0&1] 1 {1} -[!0&1] 2 {0 1} +[1] 0 +[0&1] 1 +[!0&1] 2 {0} State: 2 [!1] 0 [0&!1] 1 [!0&!1] 2 [!0&!1] 3 State: 3 -[!0&!1] 3 {0 1} +[!0&!1] 3 {0} --END-- HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" -acc-name: generalized-Buchi 2 -Acceptance: 2 Inf(0)&Inf(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 -[t] 0 {1} -[0] 1 {1} -[!0] 2 {0 1} +[t] 0 +[0] 1 +[!0] 2 {0} State: 1 -[1] 0 {1} -[0&1] 1 {0 1} -[!0&1] 2 {0 1} +[1] 0 +[0&1] 1 {0} +[!0&1] 2 {0} State: 2 [!1] 0 -[0&!1] 1 {0 1} -[!0&!1] 2 {0 1} -[!0&!1] 3 {0 1} +[0&!1] 1 {0} +[!0&!1] 2 {0} +[!0&!1] 3 State: 3 -[!0&!1] 3 {0 1} +[!0&!1] 3 {0} --END-- HOA: v1 States: 1 @@ -646,47 +631,42 @@ State: 0 [!0] 0 [0] 1 State: 1 {0} -[!0] 1 -[0] 1 +[t] 1 --END-- HOA: v1 -States: 10 +States: 9 Start: 2 AP: 1 "p1" acc-name: Buchi Acceptance: 1 Inf(0) -properties: trans-labels explicit-labels state-acc +properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 -[!0] 6 [0] 0 +[!0] 6 [0] 8 -[0] 9 -State: 1 {0} -[!0] 3 -[0] 3 -State: 2 {0} -[!0] 5 +State: 1 +[t] 3 +State: 2 [0] 1 -State: 3 {0} -[!0] 6 +[!0] 5 +State: 3 [0] 0 -State: 4 {0} [!0] 6 -[0] 4 -State: 5 {0} -[!0] 7 +State: 4 +[0] 4 {0} +[!0] 6 +State: 5 [0] 3 +[!0] 7 State: 6 -[!0] 6 [0] 0 -State: 7 {0} [!0] 6 -[0] 4 +State: 7 +[0] 4 {0} +[!0] 6 State: 8 -[0] 8 -State: 9 {0} -[0] 9 +[0] 8 {0} --END-- HOA: v1 States: 15 @@ -694,83 +674,75 @@ Start: 13 AP: 2 "p1" "p0" acc-name: Buchi Acceptance: 1 Inf(0) -properties: trans-labels explicit-labels state-acc +properties: trans-labels explicit-labels trans-acc --BODY-- -State: 0 {0} +State: 0 +[0&1] 0 {0} +[!0&1] 1 {0} +[0&!1] 11 {0} [!0&!1] 12 -[0&!1] 11 -[!0&1] 1 -[0&1] 0 -State: 1 {0} +State: 1 +[0&1] 0 {0} +[!0&1] 1 {0} +[0&!1] 11 {0} [!0&!1] 12 -[0&!1] 11 -[!0&1] 1 -[0&1] 0 -State: 2 {0} -[!0&!1] 10 -[0&!1] 11 -[!0&1] 2 +State: 2 +[!0&1] 2 {0} [0&1] 9 -State: 3 {0} +[!0&!1] 10 {0} +[0&!1] 11 {0} +State: 3 +[!0&1] 1 {0} +[0&1] 3 {0} +[0&!1] 11 {0} [!0&!1] 12 -[0&!1] 11 -[!0&1] 1 -[0&1] 3 -State: 4 {0} -[!0&!1] 12 -[0&!1] 12 -[!0&1] 4 -[0&1] 7 -State: 5 {0} -[!0&!1] 10 -[0&!1] 12 -[!0&1] 5 +State: 4 +[!0&1] 4 {0} +[0&1] 7 {0} +[!1] 12 +State: 5 +[!0&1] 5 {0} [0&1] 8 -State: 6 {0} -[!0&!1] 12 -[0&!1] 11 -[!0&1] 4 -[0&1] 6 -State: 7 {0} -[!0&!1] 12 +[!0&!1] 10 {0} [0&!1] 12 -[!0&1] 4 -[0&1] 7 +State: 6 +[!0&1] 4 {0} +[0&1] 6 {0} +[0&!1] 11 {0} +[!0&!1] 12 +State: 7 +[!0&1] 4 {0} +[0&1] 7 {0} +[!1] 12 State: 8 -[!0&!1] 12 -[0&!1] 12 -[!0&1] 8 -[0&1] 8 -[!0&1] 14 -[0&1] 14 +[1] 8 +[!1] 12 +[1] 14 State: 9 -[!0&!1] 12 -[0&!1] 11 [!0&1] 1 [0&1] 3 -State: 10 {0} -[!0&!1] 10 -[0&!1] 12 -[!0&1] 5 -[0&1] 8 -State: 11 {0} -[!0&!1] 12 [0&!1] 11 +[!0&!1] 12 +State: 10 +[!0&1] 5 {0} +[0&1] 8 +[!0&!1] 10 {0} +[0&!1] 12 +State: 11 +[0&1] 6 {0} [!0&1] 8 -[0&1] 6 +[0&!1] 11 {0} +[!0&!1] 12 State: 12 -[!0&!1] 12 -[0&!1] 12 -[!0&1] 8 -[0&1] 8 +[1] 8 +[!1] 12 State: 13 -[!0&!1] 10 -[0&!1] 11 [!0&1] 2 [0&1] 3 -State: 14 {0} -[!0&1] 14 -[0&1] 14 +[!0&!1] 10 +[0&!1] 11 +State: 14 +[1] 14 {0} --END-- HOA: v1 States: 4 @@ -797,44 +769,26 @@ State: 3 {0} [!0&1] 3 --END-- HOA: v1 -States: 6 -Start: 5 +States: 5 +Start: 4 AP: 2 "p0" "p1" acc-name: Buchi Acceptance: 1 Inf(0) -properties: trans-labels explicit-labels state-acc complete -properties: deterministic +properties: trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0 -[!0&!1] 0 -[0&!1] 0 -[!0&1] 0 -[0&1] 0 +[0] 1 State: 1 -[!0&!1] 0 -[0&!1] 2 +[t] 1 {0} +State: 2 [!0&1] 0 -[0&1] 2 -State: 2 {0} -[!0&!1] 2 -[0&!1] 2 -[!0&1] 2 -[0&1] 2 -State: 3 {0} -[!0&!1] 3 -[0&!1] 2 -[!0&1] 1 -[0&1] 2 +[0] 1 {0} +[!0&!1] 2 {0} +State: 3 +[1] 0 +[!1] 2 State: 4 -[!0&!1] 3 -[0&!1] 3 -[!0&1] 1 -[0&1] 1 -State: 5 -[!0&!1] 4 -[0&!1] 4 -[!0&1] 4 -[0&1] 4 +[t] 3 --END-- HOA: v1 States: 5 @@ -845,24 +799,18 @@ Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc --BODY-- State: 0 -[!0&!1] 2 [0&!1] 0 -[!0&1] 2 +[!0] 2 [0&1] 3 State: 1 -[!0&!1] 2 [0&!1] 1 -[!0&1] 2 -[0&1] 2 +[!0 | 1] 2 State: 2 {0} -[!0&!1] 2 [0&!1] 0 -[!0&1] 2 -[0&1] 2 +[!0 | 1] 2 State: 3 -[!0&!1] 2 [0&!1] 0 -[!0&1] 2 +[!0] 2 [0&1] 3 [0&1] 4 State: 4 {0} diff --git a/src/twaalgos/Makefile.am b/src/twaalgos/Makefile.am index bf600ea36..66da8ff9c 100644 --- a/src/twaalgos/Makefile.am +++ b/src/twaalgos/Makefile.am @@ -33,10 +33,10 @@ twaalgos_HEADERS = \ canonicalize.hh \ cleanacc.hh \ complete.hh \ + complement.hh \ compsusp.hh \ copy.hh \ cycles.hh \ - dtgbacomp.hh \ degen.hh \ dot.hh \ dtbasat.hh \ @@ -90,10 +90,10 @@ libtwaalgos_la_SOURCES = \ canonicalize.cc \ cleanacc.cc \ complete.cc \ + complement.cc \ compsusp.cc \ copy.cc \ cycles.cc \ - dtgbacomp.cc \ degen.cc \ dot.cc \ dtbasat.cc \ diff --git a/src/twaalgos/complement.cc b/src/twaalgos/complement.cc new file mode 100644 index 000000000..446bd5f87 --- /dev/null +++ b/src/twaalgos/complement.cc @@ -0,0 +1,35 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#include "complement.hh" +#include "sccinfo.hh" +#include "complete.hh" +#include "cleanacc.hh" + +namespace spot +{ + twa_graph_ptr + dtwa_complement(const const_twa_graph_ptr& aut) + { + // Simply complete the automaton, and complement its acceptance. + auto res = cleanup_acceptance_here(complete(aut)); + res->set_acceptance(res->num_sets(), res->get_acceptance().complement()); + return res; + } +} diff --git a/src/twaalgos/dtgbacomp.hh b/src/twaalgos/complement.hh similarity index 57% rename from src/twaalgos/dtgbacomp.hh rename to src/twaalgos/complement.hh index ed3f05cda..b1f2b391d 100644 --- a/src/twaalgos/dtgbacomp.hh +++ b/src/twaalgos/complement.hh @@ -23,13 +23,19 @@ namespace spot { - /// \brief Complement a deterministic TGBA + /// \brief Complement a deterministic TωA /// - /// The automaton \a aut should be deterministic. It does no need - /// to be complete. Acceptance can be transition-based, or - /// state-based. Unless the input automaton is marked as weak (in - /// which case the output will also be weak and deterministic) the - /// resulting automaton is very unlikely to be deterministic. + /// The automaton \a aut should be deterministic. It will be + /// completed if it isn't already. In these conditions, + /// complementing the automaton can be done by just complementing + /// the acceptance condition. + /// + /// In particular, this implies that an input that use + /// generalized Büchi will be output as generalized co-Büchi. + /// + /// Functions like to_generalized_buchi() or remove_fin() are + /// frequently called after dtwa_complement() to obtain an easier + /// acceptance condition (maybe at the cost of loosing determinism.) SPOT_API twa_graph_ptr - dtgba_complement(const const_twa_graph_ptr& aut); + dtwa_complement(const const_twa_graph_ptr& aut); } diff --git a/src/twaalgos/dtgbacomp.cc b/src/twaalgos/dtgbacomp.cc deleted file mode 100644 index 2edb181dc..000000000 --- a/src/twaalgos/dtgbacomp.cc +++ /dev/null @@ -1,187 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include "dtgbacomp.hh" -#include "sccinfo.hh" -#include "complete.hh" -#include "cleanacc.hh" - -namespace spot -{ - namespace - { - static twa_graph_ptr - dtgba_complement_nonweak(const const_twa_graph_ptr& aut) - { - // Clone the original automaton. - auto res = make_twa_graph(aut, - { false, // state based - false, // inherently_weak - false, // deterministic - true, // stutter inv. - }); - // Copy the old acceptance condition before we replace it. - acc_cond oldacc = aut->acc(); // Copy it! - - // We will modify res in place, and the resulting - // automaton will only have one acceptance set. - // This changes aut->acc(); - res->set_buchi(); - // The resulting automaton is weak. - res->prop_inherently_weak(); - res->prop_state_based_acc(); - - unsigned num_sets = oldacc.num_sets(); - unsigned n = res->num_states(); - // We will duplicate the automaton as many times as we have - // acceptance sets, and we need one extra sink state. - res->new_states(num_sets * n + 1); - unsigned sink = res->num_states() - 1; - // The sink state has an accepting self-loop. - res->new_acc_edge(sink, sink, bddtrue); - - for (unsigned src = 0; src < n; ++src) - { - // Keep track of all conditions on edge leaving state - // SRC, so we can complete it. - bdd missingcond = bddtrue; - for (auto& t: res->out(src)) - { - if (t.dst >= n) // Ignore edges we added. - break; - missingcond -= t.cond; - acc_cond::mark_t curacc = t.acc; - // The original edge must not accept anymore. - t.acc = 0U; - - // Edge that were fully accepting are never cloned. - if (oldacc.accepting(curacc)) - continue; - // Save t.cond and t.dst as the reference to t - // is invalided by calls to new_edge(). - unsigned dst = t.dst; - bdd cond = t.cond; - - // Iterate over all the acceptance conditions in 'curacc', - // an duplicate it for each clone for which it does not - // belong to the acceptance set. - unsigned add = 0; - for (unsigned set = 0; set < num_sets; ++set) - { - add += n; - if (!oldacc.has(curacc, set)) - { - // Clone the edge - res->new_acc_edge(src + add, dst + add, cond); - assert(dst + add < sink); - // Using `t' is disallowed from now on as it is a - // reference to a edge that may have been - // reallocated. - - // At least one edge per cycle should have a - // nondeterministic copy from the original clone. - // We use state numbers to select it, as any cycle - // is guaranteed to have at least one edge - // with dst <= src. FIXME: Computing a feedback - // arc set would be better. - if (dst <= src) - res->new_edge(src, dst + add, cond); - } - } - assert(add == num_sets * n); - } - // Complete the original automaton. - if (missingcond != bddfalse) - res->new_edge(src, sink, missingcond); - } - res->merge_edges(); - res->purge_dead_states(); - return res; - } - - static twa_graph_ptr - dtgba_complement_weak(const const_twa_graph_ptr& aut) - { - // Clone the original automaton. - auto res = make_twa_graph(aut, - { true, // state based - true, // inherently weak - true, // determinisitic - true, // stutter inv. - }); - scc_info si(res); - - // We will modify res in place, and the resulting - // automaton will only have one acceptance set. - acc_cond::mark_t all_acc = res->set_buchi(); - res->prop_state_based_acc(); - - unsigned sink = res->num_states(); - - for (unsigned src = 0; src < sink; ++src) - { - acc_cond::mark_t acc = 0U; - unsigned scc = si.scc_of(src); - if (si.is_rejecting_scc(scc) && !si.is_trivial(scc)) - acc = all_acc; - - // Keep track of all conditions on edge leaving state - // SRC, so we can complete it. - bdd missingcond = bddtrue; - for (auto& t: res->out(src)) - { - missingcond -= t.cond; - t.acc = acc; - } - // Complete the original automaton. - if (missingcond != bddfalse) - { - if (res->num_states() == sink) - { - res->new_state(); - res->new_acc_edge(sink, sink, bddtrue); - } - res->new_edge(src, sink, missingcond); - } - } - //res->merge_edges(); - return res; - } - } - - twa_graph_ptr dtgba_complement(const const_twa_graph_ptr& aut) - { - if (aut->acc().is_generalized_buchi()) - { - if (aut->is_inherently_weak()) - return dtgba_complement_weak(aut); - else - return dtgba_complement_nonweak(aut); - } - else - { - // Simply complete the automaton, and complement its - // acceptance. - auto res = cleanup_acceptance_here(complete(aut)); - res->set_acceptance(res->num_sets(), - res->get_acceptance().complement()); - return res; - } - } -} diff --git a/src/twaalgos/minimize.cc b/src/twaalgos/minimize.cc index ff8d9369c..aff462559 100644 --- a/src/twaalgos/minimize.cc +++ b/src/twaalgos/minimize.cc @@ -44,7 +44,8 @@ #include "twaalgos/ltl2tgba_fm.hh" #include "twaalgos/bfssteps.hh" #include "twaalgos/isdet.hh" -#include "twaalgos/dtgbacomp.hh" +#include "twaalgos/complement.hh" +#include "twaalgos/remfin.hh" namespace spot { @@ -632,7 +633,7 @@ namespace spot { // If the automaton is deterministic, complementing is // easy. - aut_neg_f = dtgba_complement(aut_f); + aut_neg_f = remove_fin(dtwa_complement(aut_f)); } else { @@ -654,7 +655,7 @@ namespace spot { // Complement the minimized WDBA. assert(min_aut_f->is_inherently_weak()); - auto neg_min_aut_f = dtgba_complement(min_aut_f); + auto neg_min_aut_f = remove_fin(dtwa_complement(min_aut_f)); if (product(aut_f, neg_min_aut_f)->is_empty()) // Finally, we are now sure that it was safe // to minimize the automaton. diff --git a/src/twaalgos/postproc.cc b/src/twaalgos/postproc.cc index 1a7d2cfef..9f72917ce 100644 --- a/src/twaalgos/postproc.cc +++ b/src/twaalgos/postproc.cc @@ -139,6 +139,23 @@ namespace spot return do_sba_simul(d, ba_simul_); } + twa_graph_ptr + postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg) + { + if (scc_filter_ == 0) + return a; + if (state_based_ && a->has_state_based_acc()) + return scc_filter_states(a); + else + return scc_filter(a, arg); + } + + twa_graph_ptr + postprocessor::do_scc_filter(const twa_graph_ptr& a) + { + return do_scc_filter(a, scc_filter_ > 1); + } + #define PREF_ (pref_ & (Small | Deterministic)) #define COMP_ (pref_ & Complete) #define SBACC_ (pref_ & SBAcc) @@ -146,22 +163,6 @@ namespace spot twa_graph_ptr postprocessor::run(twa_graph_ptr a, formula f) { - if (type_ != Generic && !a->acc().is_generalized_buchi()) - a = to_generalized_buchi(a); - - if (PREF_ == Any && level_ == Low) - if (type_ == Generic - || type_ == TGBA - || (type_ == BA && a->is_sba()) - || (type_ == Monitor && a->num_sets() == 0)) - { - if (COMP_) - a = complete(a); - if (SBACC_) - a = sbacc(a); - return a; - } - if (simul_ < 0) simul_ = (level_ == Low) ? 1 : 3; if (ba_simul_ < 0) @@ -171,6 +172,28 @@ namespace spot if (type_ == BA || SBACC_) state_based_ = true; + bool tgb_used = false; + if (type_ != Generic && !a->acc().is_generalized_buchi()) + { + a = to_generalized_buchi(a); + tgb_used = true; + } + + if (PREF_ == Any && level_ == Low) + if (type_ == Generic + || type_ == TGBA + || (type_ == BA && a->is_sba()) + || (type_ == Monitor && a->num_sets() == 0)) + { + if (tgb_used) + a = do_scc_filter(a); + if (COMP_) + a = complete(a); + if (SBACC_) + a = sbacc(a); + return a; + } + int original_acc = a->num_sets(); // Remove useless SCCs. @@ -178,13 +201,8 @@ namespace spot // Do not bother about acceptance conditions, they will be // ignored. a = scc_filter_states(a); - else if (scc_filter_ > 0) - { - if (state_based_ && a->has_state_based_acc()) - a = scc_filter_states(a); - else - a = scc_filter(a, scc_filter_ > 1); - } + else + a = do_scc_filter(a); if (type_ == Monitor) { @@ -380,7 +398,7 @@ namespace spot in = dba; } - const_twa_graph_ptr res = complete(in); + twa_graph_ptr res = complete(in); if (target_acc == 1) { if (sat_states_ != -1) @@ -408,14 +426,7 @@ namespace spot if (res) { - if (state_based_) - // FIXME: This does not simplify generalized acceptance - // conditions, but calling scc_filter() would break the - // BA-typeness of res by removing acceptance marks from - // out-of-SCC transitions. - dba = scc_filter_states(res); - else - dba = scc_filter(res, true); + dba = do_scc_filter(res, true); dba_is_minimal = true; } } @@ -438,18 +449,12 @@ namespace spot { if (dba && !dba_is_minimal) // WDBA is already clean. { - if (state_based_ && dba->has_state_based_acc()) - dba = scc_filter_states(dba); - else - dba = scc_filter(dba, true); + dba = do_scc_filter(dba, true); assert(!sim); } else if (sim) { - if (state_based_ && sim->has_state_based_acc()) - sim = scc_filter_states(sim); - else - sim = scc_filter(sim, true); + sim = do_scc_filter(sim, true); assert(!dba); } } diff --git a/src/twaalgos/postproc.hh b/src/twaalgos/postproc.hh index 1c7208ab9..19cdd43e1 100644 --- a/src/twaalgos/postproc.hh +++ b/src/twaalgos/postproc.hh @@ -105,6 +105,8 @@ namespace spot twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt); twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt); twa_graph_ptr do_degen(const twa_graph_ptr& input); + twa_graph_ptr do_scc_filter(const twa_graph_ptr& a, bool arg); + twa_graph_ptr do_scc_filter(const twa_graph_ptr& a); output_type type_; int pref_; diff --git a/src/twaalgos/powerset.cc b/src/twaalgos/powerset.cc index 53e9feda2..fd5ebca9a 100644 --- a/src/twaalgos/powerset.cc +++ b/src/twaalgos/powerset.cc @@ -34,7 +34,8 @@ #include "twaalgos/gtec/gtec.hh" #include "twaalgos/sccfilter.hh" #include "twaalgos/ltl2tgba_fm.hh" -#include "twaalgos/dtgbacomp.hh" +#include "twaalgos/complement.hh" +#include "twaalgos/remfin.hh" #include "misc/bitvect.hh" #include "misc/bddlt.hh" @@ -426,7 +427,7 @@ namespace spot if (product(det, neg_aut)->is_empty()) // Complement the DBA. - if (product(aut, dtgba_complement(det))->is_empty()) + if (product(aut, remove_fin(dtwa_complement(det)))->is_empty()) // Finally, we are now sure that it was safe // to determinize the automaton. return det; diff --git a/src/twaalgos/remfin.cc b/src/twaalgos/remfin.cc index bfe284e3d..de7ced8be 100644 --- a/src/twaalgos/remfin.cc +++ b/src/twaalgos/remfin.cc @@ -22,6 +22,7 @@ #include #include "cleanacc.hh" #include "totgba.hh" +#include "isdet.hh" #include "mask.hh" //#define TRACE @@ -450,6 +451,54 @@ namespace spot return res; } + static twa_graph_ptr + remove_fin_det_weak(const const_twa_graph_ptr& aut) + { + // Clone the original automaton. + auto res = make_twa_graph(aut, + { + true, // state based + true, // inherently weak + true, // determinisitic + true, // stutter inv. + }); + scc_info si(res); + + // We will modify res in place, and the resulting + // automaton will only have one acceptance set. + acc_cond::mark_t all_acc = res->set_buchi(); + res->prop_state_based_acc(); + res->prop_deterministic(); + + unsigned sink = res->num_states(); + for (unsigned src = 0; src < sink; ++src) + { + acc_cond::mark_t acc = 0U; + unsigned scc = si.scc_of(src); + if (si.is_accepting_scc(scc) && !si.is_trivial(scc)) + acc = all_acc; + // Keep track of all conditions on edge leaving state + // SRC, so we can complete it. + bdd missingcond = bddtrue; + for (auto& t: res->out(src)) + { + missingcond -= t.cond; + t.acc = acc; + } + // Complete the original automaton. + if (missingcond != bddfalse) + { + if (res->num_states() == sink) + { + res->new_state(); + res->new_acc_edge(sink, sink, bddtrue); + } + res->new_edge(src, sink, missingcond); + } + } + //res->merge_edges(); + return res; + } } twa_graph_ptr remove_fin(const const_twa_graph_ptr& aut) @@ -457,6 +506,10 @@ namespace spot if (!aut->acc().uses_fin_acceptance()) return std::const_pointer_cast(aut); + // FIXME: we should check whether the automaton is weak. + if (aut->is_inherently_weak() && is_deterministic(aut)) + return remove_fin_det_weak(aut); + if (auto maybe = streett_to_generalized_buchi_maybe(aut)) return maybe; @@ -609,13 +662,13 @@ namespace spot unsigned nst = aut->num_states(); auto res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); - res->prop_copy(aut, { false, false, false, true }); + res->prop_copy(aut, { true, false, false, true }); res->new_states(nst); res->set_acceptance(aut->num_sets() + extra_sets, new_code); res->set_init_state(aut->get_init_state_number()); + bool sbacc = aut->has_state_based_acc(); scc_info si(aut); - unsigned nscc = si.scc_count(); std::vector state_map(nst); for (unsigned n = 0; n < nscc; ++n) @@ -643,7 +696,12 @@ namespace spot // Create the main copy for (auto s: states) for (auto& t: aut->out(s)) - res->new_edge(s, t.dst, t.cond, (t.acc & main_sets) | main_add); + { + acc_cond::mark_t a = 0U; + if (sbacc || SPOT_LIKELY(si.scc_of(t.dst) == n)) + a = (t.acc & main_sets) | main_add; + res->new_edge(s, t.dst, t.cond, a); + } // We do not need any other copy if the SCC is non-accepting, // of if it does not intersect any Fin. @@ -673,22 +731,27 @@ namespace spot // We need only one non-deterministic jump per // cycle. As an approximation, we only do // them on back-links. - // - // The acceptance marks on these edge - // are useless, but we keep them to preserve - // state-based acceptance if any. if (t.dst <= s) - res->new_edge(s, nd, t.cond, - (t.acc & main_sets) | main_add); + { + acc_cond::mark_t a = 0U; + if (sbacc) + a = (t.acc & main_sets) | main_add; + res->new_edge(s, nd, t.cond, a); + } } } } } + // If the input had no Inf, the output is a state-based automaton. + if (allinf == 0U) + res->prop_state_based_acc(); + res->purge_dead_states(); trace << "before cleanup: " << res->get_acceptance() << '\n'; cleanup_acceptance_here(res); trace << "after cleanup: " << res->get_acceptance() << '\n'; + res->merge_edges(); return res; } } diff --git a/src/twaalgos/stutter.cc b/src/twaalgos/stutter.cc index c2cdf99b2..6d1b20b3b 100644 --- a/src/twaalgos/stutter.cc +++ b/src/twaalgos/stutter.cc @@ -27,7 +27,8 @@ #include "twaalgos/product.hh" #include "twaalgos/ltl2tgba_fm.hh" #include "twaalgos/isdet.hh" -#include "twaalgos/dtgbacomp.hh" +#include "twaalgos/complement.hh" +#include "twaalgos/remfin.hh" #include "twa/twaproduct.hh" #include "twa/bddprint.hh" #include @@ -635,8 +636,7 @@ namespace spot aut->prop_deterministic(is_deterministic(aut)); if (!aut->is_deterministic()) return false; - - neg = dtgba_complement(aut); + neg = remove_fin(dtwa_complement(aut)); } is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()), diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 6d7005cd5..97571e824 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -113,6 +113,7 @@ #include "twaalgos/degen.hh" #include "twaalgos/copy.hh" #include "twaalgos/complete.hh" +#include "twaalgos/complement.hh" #include "twaalgos/emptiness.hh" #include "twaalgos/gtec/gtec.hh" #include "twaalgos/lbtt.hh" @@ -266,6 +267,7 @@ namespace std { %include "twaalgos/dot.hh" %include "twaalgos/copy.hh" %include "twaalgos/complete.hh" +%include "twaalgos/complement.hh" %include "twaalgos/emptiness.hh" %include "twaalgos/gtec/gtec.hh" %include "twaalgos/lbtt.hh"