From 2a38328a5c071100026f2304a87b1618bfc20c58 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 14 Apr 2021 17:31:45 +0200 Subject: [PATCH] replace bdd_satoneset(x,y,bddtrue) loops by minterms_of(x,y) Because the loops iterate in the opposite order, multiple test cases need to be adjusted. * spot/taalgos/tgba2ta.cc, spot/twaalgos/alternation.cc, spot/twaalgos/dualize.cc, spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/simulation.cc, spot/twaalgos/stutter.cc, spot/twaalgos/toweak.cc: Replace loops based on bdd_satonest(x,y,bddtrue) by loops based on minterms_of(x,y). * tests/core/degenscc.test, tests/core/dualize.test, tests/core/genltl.test, tests/core/readsave.test, tests/python/alternation.ipynb, tests/python/automata.ipynb, tests/python/decompose.ipynb, tests/python/decompose_scc.py, tests/python/dualize.py, tests/python/sccinfo.py, tests/python/simstate.py, tests/python/testingaut.ipynb, tests/python/word.ipynb: Adjust expected test cases. The only regression is in genltl.test, but the worsened case should eventually be fixed as discussed in issue #425 anyway. --- spot/taalgos/tgba2ta.cc | 30 +- spot/twaalgos/alternation.cc | 11 +- spot/twaalgos/dualize.cc | 7 +- spot/twaalgos/ltl2tgba_fm.cc | 60 +- spot/twaalgos/simulation.cc | 19 +- spot/twaalgos/stutter.cc | 13 +- spot/twaalgos/toweak.cc | 7 +- tests/core/degenscc.test | 6 +- tests/core/dualize.test | 10 +- tests/core/genltl.test | 4 +- tests/core/readsave.test | 6 +- tests/python/alternation.ipynb | 998 ++++++++++++++++----------------- tests/python/automata.ipynb | 178 +++--- tests/python/decompose.ipynb | 536 ++++++++---------- tests/python/decompose_scc.py | 11 +- tests/python/dualize.py | 16 +- tests/python/sccinfo.py | 10 +- tests/python/simstate.py | 14 +- tests/python/testingaut.ipynb | 593 ++++++++++---------- tests/python/word.ipynb | 218 +++---- 20 files changed, 1315 insertions(+), 1432 deletions(-) diff --git a/spot/taalgos/tgba2ta.cc b/spot/taalgos/tgba2ta.cc index b2d499e54..fc9073aa5 100644 --- a/spot/taalgos/tgba2ta.cc +++ b/spot/taalgos/tgba2ta.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010-2018 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2010-2018, 2021 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -410,12 +410,9 @@ namespace spot delete it; } - bdd satone_tgba_condition; - while ((satone_tgba_condition = bdd_satoneset(tgba_condition, - atomic_propositions_set_, - bddtrue)) != bddfalse) + for (bdd satone_tgba_condition: minterms_of(tgba_condition, + atomic_propositions_set_)) { - tgba_condition -= satone_tgba_condition; state_ta_explicit* init_state = new state_ta_explicit(tgba_init_state->clone(), satone_tgba_condition, true, is_acc); @@ -441,17 +438,9 @@ namespace spot bdd tgba_condition = twa_succ_it->cond(); acc_cond::mark_t tgba_acceptance_conditions = twa_succ_it->acc(); - bdd satone_tgba_condition; - while ((satone_tgba_condition = - bdd_satoneset(tgba_condition, - atomic_propositions_set_, bddtrue)) - != bddfalse) + for (bdd satone_tgba_condition: + minterms_of(tgba_condition, atomic_propositions_set_)) { - tgba_condition -= satone_tgba_condition; - - bdd all_props = bddtrue; - bdd dest_condition; - bool is_acc = false; if (degeneralized) { @@ -463,12 +452,9 @@ namespace spot } if (satone_tgba_condition == source->get_tgba_condition()) - while ((dest_condition = - bdd_satoneset(all_props, - atomic_propositions_set_, bddtrue)) - != bddfalse) + for (bdd dest_condition: + minterms_of(bddtrue, atomic_propositions_set_)) { - all_props -= dest_condition; state_ta_explicit* new_dest = new state_ta_explicit(tgba_state->clone(), dest_condition, false, is_acc); diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index 25d91f473..5a4ef668a 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016-2019 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2016-2019, 2021 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -456,11 +456,8 @@ namespace spot bdd all_letters = bdd_exist(bs, all_vars_); // First loop over all possible valuations atomic properties. - while (all_letters != bddfalse) + for (bdd oneletter: minterms_of(all_letters, ap)) { - bdd oneletter = bdd_satoneset(all_letters, ap, bddtrue); - all_letters -= oneletter; - minato_isop isop(bs & oneletter); bdd cube; while ((cube = isop.next()) != bddfalse) @@ -637,7 +634,7 @@ namespace spot // If it was the last transition, try the next letter. if (transition_ == bddfalse) { - bdd oneletter = bdd_satoneset(all_letters_, ap_, bddtrue); + bdd oneletter = bdd_satoneset(all_letters_, ap_, bddfalse); all_letters_ -= oneletter; // Get a sum of possible transitions matching this letter. isop_ = minato_isop(oneletter & transitions_); diff --git a/spot/twaalgos/dualize.cc b/spot/twaalgos/dualize.cc index e64945574..e42822740 100644 --- a/spot/twaalgos/dualize.cc +++ b/spot/twaalgos/dualize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2019, 2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -153,11 +153,8 @@ namespace spot bdd ap = bdd_exist(bdd_support(delta), all_vars_); bdd letters = bdd_exist(delta, all_vars_); - while (letters != bddfalse) + for (bdd oneletter: minterms_of(letters, ap)) { - bdd oneletter = bdd_satoneset(letters, ap, bddtrue); - letters -= oneletter; - minato_isop isop(delta & oneletter); bdd cube; diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index c560bc2e3..55dc2bddb 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2008-2019, 2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -899,11 +899,8 @@ namespace spot bdd res_det = bddfalse; bdd var_set = bdd_existcomp(bdd_support(res_ndet), dict_.var_set); bdd all_props = bdd_existcomp(res_ndet, dict_.var_set); - while (all_props != bddfalse) + for (bdd label: minterms_of(all_props, var_set)) { - bdd label = bdd_satoneset(all_props, var_set, bddtrue); - all_props -= label; - formula dest = dict_.bdd_to_sere(bdd_appex(res_ndet, label, bddop_and, dict_.var_set)); @@ -998,11 +995,8 @@ namespace spot // Generate (deterministic) successors bdd var_set = bdd_existcomp(bdd_support(res), dict_.var_set); bdd all_props = bdd_existcomp(res, dict_.var_set); - while (all_props != bddfalse) + for (bdd label: minterms_of(all_props, var_set)) { - bdd label = bdd_satoneset(all_props, var_set, bddtrue); - all_props -= label; - formula dest = dict_.bdd_to_sere(bdd_appex(res, label, bddop_and, dict_.var_set)); @@ -1475,11 +1469,8 @@ namespace spot { bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set); bdd all_props = bdd_existcomp(f1, dict_.var_set); - while (all_props != bddfalse) + for (bdd label: minterms_of(all_props, var_set)) { - bdd label = bdd_satoneset(all_props, var_set, bddtrue); - all_props -= label; - formula dest = dict_.bdd_to_sere(bdd_appex(f1, label, bddop_and, dict_.var_set)); @@ -1559,11 +1550,8 @@ namespace spot bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set); bdd all_props = bdd_existcomp(f1, dict_.var_set); bdd missing = !all_props; - while (all_props != bddfalse) + for (bdd label: minterms_of(all_props, var_set)) { - bdd label = bdd_satoneset(all_props, var_set, bddtrue); - all_props -= label; - formula dest = dict_.bdd_to_sere(bdd_appex(f1, label, bddop_and, dict_.var_set)); @@ -1793,16 +1781,15 @@ namespace spot if (t.has_rational) { bdd res = bddfalse; - - bdd var_set = bdd_existcomp(bdd_support(t.symbolic), d_.var_set); - bdd all_props = bdd_existcomp(t.symbolic, d_.var_set); - while (all_props != bddfalse) + bdd var_set = bddtrue; + bdd all_props = bddtrue; + if (d_.exprop) + { + var_set = bdd_existcomp(bdd_support(t.symbolic), d_.var_set); + all_props = bdd_existcomp(t.symbolic, d_.var_set); + } + for (bdd one_prop_set: minterms_of(all_props, var_set)) { - bdd one_prop_set = bddtrue; - if (d_.exprop) - one_prop_set = bdd_satoneset(all_props, var_set, bddtrue); - all_props -= one_prop_set; - minato_isop isop(t.symbolic & one_prop_set); bdd cube; while ((cube = isop.next()) != bddfalse) @@ -2110,24 +2097,21 @@ namespace spot dests.clear(); // Compute all outgoing arcs. - // If EXPROP is set, we will refine the symbolic // representation of the successors for all combinations of // the atomic properties involved in the formula. // VAR_SET is the set of these properties. - bdd var_set = bdd_existcomp(bdd_support(res), d.var_set); - // ALL_PROPS is the combinations we have yet to consider. - // We used to start with `all_props = bddtrue', but it is - // more efficient to start with the set of all satisfiable - // variables combinations. - bdd all_props = bdd_existcomp(res, d.var_set); - while (all_props != bddfalse) + // ALL_PROPS is the satisfiable combinations of VAR_SET to consider. + bdd var_set = bddtrue; + bdd all_props = bddtrue; + if (exprop) { - bdd one_prop_set = bddtrue; - if (exprop) - one_prop_set = bdd_satoneset(all_props, var_set, bddtrue); - all_props -= one_prop_set; + var_set = bdd_existcomp(bdd_support(res), d.var_set); + all_props = bdd_existcomp(res, d.var_set); + } + for (bdd one_prop_set: minterms_of(all_props, var_set)) + { // Compute prime implicants. // The reason we use prime implicants and not bdd_satone() // is that we do not want to get any negation in front of Next diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index ee0686491..9ed9739c3 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -538,7 +538,7 @@ namespace spot stat.states = bdd_lstate_.size(); stat.edges = 0; - unsigned nb_satoneset = 0; + unsigned nb_minterms = 0; unsigned nb_minato = 0; auto all_inf = all_inf_; @@ -573,24 +573,19 @@ namespace spot bdd all_atomic_prop = bdd_exist(sig, nonapvars); // First loop over all possible valuations atomic properties. - while (all_atomic_prop != bddfalse) + for (bdd one: minterms_of(all_atomic_prop, sup_all_atomic_prop)) { - bdd one = bdd_satoneset(all_atomic_prop, - sup_all_atomic_prop, - bddtrue); - all_atomic_prop -= one; - // For each possible valuation, iterate over all possible // destination classes. We use minato_isop here, because // if the same valuation of atomic properties can go // to two different classes C1 and C2, iterating on - // C1 + C2 with the above bdd_satoneset loop will see + // C1 + C2 with the above minters_of loop will see // C1 then (!C1)C2, instead of C1 then C2. // With minatop_isop, we ensure that the no negative // class variable will be seen (likewise for promises). minato_isop isop(sig & one); - ++nb_satoneset; + ++nb_minterms; bdd cond_acc_dest; while ((cond_acc_dest = isop.next()) != bddfalse) @@ -750,8 +745,8 @@ namespace spot true, // stutter inv. }); // !unambiguous and !semi-deterministic are not preserved - if (!Cosimulation && nb_minato == nb_satoneset) - // Note that nb_minato != nb_satoneset does not imply + if (!Cosimulation && nb_minato == nb_minterms) + // Note that nb_minato != nb_minterms does not imply // non-deterministic, because of the merge_edges() above. res->prop_universal(true); if (Sba) diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index d798b290c..f9108048f 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement de +// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -187,7 +187,7 @@ namespace spot void next_edge() { - one_ = bdd_satoneset(cond_, aps_, bddtrue); + one_ = bdd_satoneset(cond_, aps_, bddfalse); cond_ -= one_; if (need_loop_ && (state_->cond() == one_) && (state_ == it_->dst())) @@ -313,11 +313,8 @@ namespace spot for (auto& t : a->out(s.first)) { bdd all = t.cond; - while (all != bddfalse) + for (bdd one: minterms_of(t.cond, atomic_propositions)) { - bdd one = bdd_satoneset(all, atomic_propositions, bddtrue); - all -= one; - stutter_state d(t.dst, one); auto r = ss2num.emplace(d, ss2num.size()); @@ -408,10 +405,8 @@ namespace spot // Do not use td in the loop because the new_edge() // might invalidate it. auto acc = td.acc; - while (all != bddfalse) + for (bdd one: minterms_of(all, atomic_propositions)) { - bdd one = bdd_satoneset(all, atomic_propositions, bddtrue); - all -= one; // Skip if there is a loop for this particular letter. if (bdd_implies(one, selfloops[src]) || bdd_implies(one, selfloops[dst])) diff --git a/spot/twaalgos/toweak.cc b/spot/twaalgos/toweak.cc index 01af20036..8f62477a4 100644 --- a/spot/twaalgos/toweak.cc +++ b/spot/twaalgos/toweak.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement +// Copyright (C) 2017, 2018, 2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -177,11 +177,8 @@ namespace spot bdd ap = bdd_exist(bdd_support(delta), all_states_); bdd letters = bdd_exist(delta, all_states_); - while (letters != bddfalse) + for (bdd oneletter: minterms_of(letters, ap)) { - bdd oneletter = bdd_satoneset(letters, ap, bddtrue); - letters -= oneletter; - minato_isop isop(delta & oneletter); bdd cube; diff --git a/tests/core/degenscc.test b/tests/core/degenscc.test index f50a58cac..b2bd74fc5 100644 --- a/tests/core/degenscc.test +++ b/tests/core/degenscc.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2017, 2019, 2021 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -33,7 +33,7 @@ set -e cat >input < test.sh diff --git a/tests/core/dualize.test b/tests/core/dualize.test index 7e66c3b8f..53bbec8fc 100755 --- a/tests/core/dualize.test +++ b/tests/core/dualize.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017, 2019 Laboratoire de Recherche et +# Copyright (C) 2017, 2019, 2021 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -115,11 +115,11 @@ Acceptance: 1 Fin(0) properties: trans-labels explicit-labels state-acc univ-branch --BODY-- State: 0 -[!0&!1] 0&7 [0&!1] 0&6&7 +[!0&!1] 0&7 State: 1 -[!0] 1&3 [0] 1&2&3 +[!0] 1&3 State: 2 [0] 4 State: 3 @@ -135,10 +135,10 @@ State: 6 {0} State: 7 [!1] 7 State: 8 -[!0] 1&3 [t] 1&2&3 -[!0&!1] 0&7 +[!0] 1&3 [!1] 0&6&7 +[!0&!1] 0&7 --END-- EOF diff output2 expected2 diff --git a/tests/core/genltl.test b/tests/core/genltl.test index ed1785494..d5efb0236 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016-2020 Laboratoire de Recherche et Développement +# Copyright (C) 2016-2021 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -195,7 +195,7 @@ cat >exp< Fb)' | autfilt -B --dot=dA | grep ' (' >out cat >expected <\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "⓿\n", - ")&Inf(\n", - "❶\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "Inf(\n", + "⓿\n", + ")&Inf(\n", + "❶\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1,3\n", + "\n", + "1,3\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "1\n", - "⓿\n", + "\n", + "\n", + "1\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", - "⓿\n", + "\n", + "\n", + "b\n", + "⓿\n", "\n", "\n", "\n", "2\n", - "\n", - "1,4\n", + "\n", + "1,2,3\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "a & b\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "3\n", - "\n", - "1,2,3\n", + "\n", + "1,2,4\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "a & !b\n", + "❶\n", "\n", "\n", "\n", "4\n", - "\n", - "1,2,4\n", + "\n", + "1,4\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & !b\n", - "❶\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "b\n", + "⓿\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & b\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & !b\n", + "❶\n", "\n", "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & !b\n", - "❶\n", - "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "b\n", - "⓿\n", - "\n", - "\n", "\n", - "3->2\n", - "\n", - "\n", - "a & b\n", - "⓿\n", - "❶\n", + "2->4\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "❶\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "a & !b\n", + "❶\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "a & !b\n", - "❶\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "❶\n", "\n", - "\n", + "\n", "\n", - "4->2\n", - "\n", - "\n", - "a & b\n", - "⓿\n", - "❶\n", + "4->3\n", + "\n", + "\n", + "a & !b\n", + "❶\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a & !b\n", - "❶\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "❶\n", "\n", "\n", "\n", @@ -3059,143 +3059,143 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1,3\n", + "\n", + "1,3\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "2\n", - "\n", - "1,4\n", + "\n", + "1,2,3\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "3\n", - "\n", - "1,2,3\n", + "\n", + "1,2,4\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "4\n", - "\n", - "1,2,4\n", + "\n", + "1,4\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", "\n", - "3->2\n", - "\n", - "\n", - "a & b\n", + "2->4\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", - "\n", + "\n", "\n", - "4->2\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "4->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", "\n", "\n", @@ -3237,121 +3237,121 @@ " -->\n", "\n", "\n", + " viewBox=\"0.00 0.00 229.87 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "~0\n", + "\n", + "~0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "~1\n", + "\n", + "{}\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "2\n", - "\n", - "{}\n", + "\n", + "~1\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "\n", + "a\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "!b & p\n", + "\n", + "\n", + "1\n", + "⓿\n", "\n", - "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & !b\n", + "2->1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b & p\n", "\n", "\n", "\n", "3\n", - "\n", - "~1,~0\n", + "\n", + "~1,~0\n", "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & b & p\n", - "\n", - "\n", + "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "⓿\n", + "2->3\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", "\n", "3->0\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "a & !b & p\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "a & !b & p\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", "\n", @@ -3361,178 +3361,178 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "~0,4\n", + "\n", + "~0,4\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "2\n", - "\n", - "3,~1\n", + "\n", + "3,~1\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "3\n", - "\n", - "4,~1,~0\n", + "\n", + "0,4,~1\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "\n", + "a & !b & p\n", "\n", "\n", "\n", "4\n", - "\n", - "0,4,~1\n", + "\n", + "4,~1,~0\n", "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "a & !b & p\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", "\n", "3->0\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "a & !b & p\n", + "\n", + "\n", + "a & !b & p\n", "\n", "\n", "\n", "5\n", - "\n", - "3,~0\n", + "\n", + "3,~0\n", "\n", "\n", "\n", "3->5\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", "\n", "6\n", - "\n", - "3,~1,~0\n", + "\n", + "3,~1,~0\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", "\n", "4->0\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", "\n", "\n", "\n", "4->2\n", - "\n", - "\n", - "a & !b & p\n", + "\n", + "\n", + "a & !b & p\n", "\n", "\n", "\n", "4->5\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "\n", + "a & b & p\n", "\n", - "\n", + "\n", "\n", - "5->4\n", - "\n", - "\n", - "a\n", + "5->3\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "\n", + "a & !b & p\n", "\n", "\n", "\n", "6->4\n", - "\n", - "\n", - "a & !b & p\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", "\n", @@ -3543,121 +3543,121 @@ " -->\n", "\n", "\n", + " viewBox=\"0.00 0.00 229.87 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "~0\n", + "\n", + "~0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "~1\n", + "\n", + "{}\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "2\n", - "\n", - "{}\n", + "\n", + "~1\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "\n", + "a\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "!b & p\n", + "\n", + "\n", + "1\n", + "⓿\n", "\n", - "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & !b\n", + "2->1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b & p\n", "\n", "\n", "\n", "3\n", - "\n", - "~1,~0\n", + "\n", + "~1,~0\n", "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & b & p\n", - "\n", - "\n", + "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "⓿\n", + "2->3\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", "\n", "3->0\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "a & !b & p\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "a & !b & p\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", "\n", @@ -3737,7 +3737,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "The following demonstrate that very weak (non-alternating) Büchi automata can be complemented via alternation removal." + "The following demonstrates that very weak (non-alternating) Büchi automata can be complemented via alternation removal." ] }, { @@ -4042,207 +4042,207 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "⓿\n", - ")&Inf(\n", - "❶\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "Inf(\n", + "⓿\n", + ")&Inf(\n", + "❶\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "!a\n", + "❶\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", - "❶\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "a\n", + "⓿\n", + "❶\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "a & b\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "!a & b\n", - "⓿\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", - "\n", - "\n", - "2->5\n", - "\n", - "\n", - "a & !b\n", - "❶\n", + "\n", + "\n", + "1->5\n", + "\n", + "\n", + "a & !b\n", + "❶\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", - "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "❶\n", + "\n", + "\n", "\n", - "2->6\n", - "\n", - "\n", - "!a & !b\n", + "2->2\n", + "\n", + "\n", + "!b\n", + "⓿\n", + "❶\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "1\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "!a & !b\n", "\n", - "\n", + "\n", "\n", - "4->3\n", - "\n", - "\n", - "a\n", - "⓿\n", - "❶\n", + "3->4\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", + "❶\n", "\n", - "\n", + "\n", "\n", - "4->4\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", + "3->5\n", + "\n", + "\n", + "a & !b\n", + "❶\n", + "\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "❶\n", "\n", "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!a & b\n", - "⓿\n", - "❶\n", - "\n", - "\n", "\n", - "5->3\n", - "\n", - "\n", - "b\n", - "⓿\n", - "❶\n", + "4->4\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "a\n", + "⓿\n", + "❶\n", "\n", "\n", - "\n", - "5->5\n", - "\n", - "\n", - "!b\n", - "❶\n", - "\n", - "\n", - "\n", - "6->3\n", - "\n", - "\n", - "a & b\n", - "⓿\n", - "❶\n", - "\n", - "\n", "\n", - "6->4\n", - "\n", - "\n", - "!a & b\n", - "⓿\n", - "❶\n", + "5->5\n", + "\n", + "\n", + "!b\n", + "❶\n", "\n", - "\n", + "\n", "\n", - "6->5\n", - "\n", - "\n", - "a & !b\n", - "❶\n", + "5->6\n", + "\n", + "\n", + "b\n", + "⓿\n", + "❶\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "1\n", + "⓿\n", + "❶\n", "\n", "\n", "\n", @@ -4296,7 +4296,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.9.1+" + "version": "3.9.2" } }, "nbformat": 4, diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 757538838..ee62dd0bd 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -178,7 +178,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43cde71b0> >" + " *' at 0x7f6a002151e0> >" ] }, "execution_count": 2, @@ -657,7 +657,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c131fc0> >" + " *' at 0x7f6a000cc3c0> >" ] }, "execution_count": 6, @@ -733,7 +733,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c1563c0> >" + " *' at 0x7f6a000cc690> >" ] }, "execution_count": 7, @@ -816,7 +816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c131ba0> >" + " *' at 0x7f6a000cc2a0> >" ] }, "execution_count": 8, @@ -1214,142 +1214,142 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", - "⓿\n", + "\n", + "\n", + "b\n", + "⓿\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a | b\n", - "\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "\n", + "\n", "2->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fe43c156e40> >" + " *' at 0x7f6a000d42a0> >" ] }, "execution_count": 12, @@ -1463,7 +1463,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c163300> >" + " *' at 0x7f6a000d4630> >" ] }, "execution_count": 13, @@ -1594,7 +1594,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c163810> >" + " *' at 0x7f6a000d4c00> >" ] }, "execution_count": 14, @@ -1816,7 +1816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c1694b0> >" + " *' at 0x7f6a000d8510> >" ] }, "metadata": {}, @@ -1974,7 +1974,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c163210> >" + " *' at 0x7f6a000d8420> >" ] }, "metadata": {}, @@ -2132,7 +2132,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c169180> >" + " *' at 0x7f6a000d8300> >" ] }, "metadata": {}, @@ -2280,7 +2280,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c169360> >" + " *' at 0x7f6a000d8270> >" ] }, "metadata": {}, @@ -2469,7 +2469,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c169210> >" + " *' at 0x7f6a00215fc0> >" ] }, "execution_count": 19, @@ -2545,7 +2545,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c169fc0> >" + " *' at 0x7f6a000e1420> >" ] }, "execution_count": 20, @@ -3095,7 +3095,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c156ea0> >" + " *' at 0x7f6a000ccd50> >" ] }, "metadata": {}, @@ -3195,7 +3195,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c156210> >" + " *' at 0x7f6a000ccde0> >" ] }, "execution_count": 24, @@ -3268,7 +3268,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe440654c60> >" + " *' at 0x7f6a000cce70> >" ] }, "execution_count": 25, @@ -3439,7 +3439,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c1316c0> >" + " *' at 0x7f6a00215ab0> >" ] }, "execution_count": 27, @@ -3522,7 +3522,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c156ea0> >" + " *' at 0x7f6a000ccd50> >" ] }, "metadata": {}, @@ -3587,7 +3587,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c156ea0> >" + " *' at 0x7f6a000ccd50> >" ] }, "metadata": {}, @@ -3674,7 +3674,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe43c156ea0> >" + " *' at 0x7f6a000ccd50> >" ] }, "execution_count": 29, @@ -3707,7 +3707,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.9.1+" + "version": "3.9.2" } }, "nbformat": 4, diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb index 4382c10f1..091dead91 100644 --- a/tests/python/decompose.ipynb +++ b/tests/python/decompose.ipynb @@ -61,11 +61,11 @@ "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "\n", "cluster_2\n", - "\n", + "\n", "\n", "\n", "cluster_3\n", @@ -105,28 +105,28 @@ "\n", "c\n", "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", - "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", "\n", "\n", "a & !c\n", @@ -139,16 +139,8 @@ "1\n", "⓿\n", "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "b\n", - "⓿\n", - "\n", "\n", - "\n", + "\n", "4\n", "\n", "4\n", @@ -167,31 +159,39 @@ "\n", "a\n", "\n", - "\n", - "\n", - "3->0\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "⓿\n", + "\n", + "\n", + "\n", + "2->0\n", "\n", "\n", "!a & !c\n", "⓿\n", "\n", - "\n", - "\n", - "3->1\n", + "\n", + "\n", + "2->1\n", "\n", "\n", "!a & c\n", "\n", - "\n", - "\n", - "3->4\n", + "\n", + "\n", + "2->4\n", "\n", "\n", "a & c\n", "\n", - "\n", - "\n", - "3->3\n", + "\n", + "\n", + "2->2\n", "\n", "\n", "a & !c\n", @@ -200,7 +200,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc092f00> >" + " *' at 0x7f1aa01ba3c0> >" ] }, "execution_count": 2, @@ -278,50 +278,50 @@ "\n", "!a & !c\n", "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & b & !c\n", - "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", "\n", "\n", "a & !c\n", "\n", - "\n", - "\n", - "1->1\n", + "\n", + "\n", + "2->2\n", "\n", "\n", "b\n", "⓿\n", "\n", - "\n", - "\n", - "2->0\n", + "\n", + "\n", + "1->0\n", "\n", "\n", "!a & !c\n", "\n", - "\n", - "\n", - "2->2\n", + "\n", + "\n", + "1->1\n", "\n", "\n", "a & !c\n", @@ -330,7 +330,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc211360> >" + " *' at 0x7f1aa01ba2a0> >" ] }, "execution_count": 3, @@ -489,7 +489,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc23f3c0> >" + " *' at 0x7f1aa01ba1b0> >" ] }, "execution_count": 4, @@ -587,7 +587,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0ea4e0> >" + " *' at 0x7f1aa01ba9c0> >" ] }, "execution_count": 5, @@ -669,7 +669,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0ea840> >" + " *' at 0x7f1aa00b6240> >" ] }, "execution_count": 6, @@ -743,51 +743,51 @@ "!a & !c\n", "⓿\n", "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & b & !c\n", - "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", "\n", "\n", "a & !c\n", "\n", - "\n", - "\n", - "1->1\n", + "\n", + "\n", + "2->2\n", "\n", "\n", "b\n", "⓿\n", "\n", - "\n", - "\n", - "2->0\n", + "\n", + "\n", + "1->0\n", "\n", "\n", "!a & !c\n", "⓿\n", "\n", - "\n", - "\n", - "2->2\n", + "\n", + "\n", + "1->1\n", "\n", "\n", "a & !c\n", @@ -796,7 +796,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0eaab0> >" + " *' at 0x7f1aa00b6120> >" ] }, "metadata": {}, @@ -941,7 +941,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc20bc60> >" + " *' at 0x7f1aa01bae40> >" ] }, "metadata": {}, @@ -972,11 +972,11 @@ "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "\n", "cluster_2\n", - "\n", + "\n", "\n", "\n", "cluster_3\n", @@ -1015,28 +1015,28 @@ "\n", "c\n", "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", - "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", "\n", "\n", "a & !c\n", @@ -1049,16 +1049,8 @@ "1\n", "⓿\n", "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "b\n", - "⓿\n", - "\n", "\n", - "\n", + "\n", "4\n", "\n", "4\n", @@ -1077,30 +1069,38 @@ "\n", "a\n", "\n", - "\n", - "\n", - "3->0\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "⓿\n", + "\n", + "\n", + "\n", + "2->0\n", "\n", "\n", "!a & !c\n", "\n", - "\n", - "\n", - "3->1\n", + "\n", + "\n", + "2->1\n", "\n", "\n", "!a & c\n", "\n", - "\n", - "\n", - "3->4\n", + "\n", + "\n", + "2->4\n", "\n", "\n", "a & c\n", "\n", - "\n", - "\n", - "3->3\n", + "\n", + "\n", + "2->2\n", "\n", "\n", "a & !c\n", @@ -1109,7 +1109,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc092cc0> >" + " *' at 0x7f1aa01baea0> >" ] }, "metadata": {}, @@ -1512,7 +1512,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0ea570> >" + " *' at 0x7f1aa00b6c60> >" ] }, "execution_count": 8, @@ -1522,60 +1522,16 @@ ], "source": [ "aut = spot.automaton(\"\"\"\n", - "HOA: v1\n", - "States: 9\n", - "Start: 2\n", - "AP: 3 \"a\" \"b\" \"c\"\n", - "acc-name: Rabin 2\n", - "Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n", - "properties: trans-labels explicit-labels state-acc complete\n", - "properties: deterministic\n", - "--BODY--\n", - "State: 0 {2}\n", - "[0&!2] 0\n", - "[0&2] 1\n", - "[!0&!2] 5\n", - "[!0&2] 6\n", - "State: 1 {2}\n", - "[0] 1\n", - "[!0] 6\n", - "State: 2 {2}\n", - "[0&!1&!2] 3\n", - "[0&1&!2] 4\n", - "[!0&!2] 5\n", - "[2] 6\n", - "State: 3 {1 2}\n", - "[0&!2] 0\n", - "[0&2] 1\n", - "[!0&!2] 5\n", - "[!0&2] 6\n", - "State: 4 {1 2}\n", - "[0&!1&!2] 0\n", - "[0&!1&2] 1\n", - "[!0&!2] 5\n", - "[!0&2] 6\n", - "[0&1&!2] 7\n", - "[0&1&2] 8\n", - "State: 5 {1 2}\n", - "[0&!1&!2] 0\n", - "[!0&!2] 5\n", - "[2] 6\n", - "[0&1&!2] 7\n", - "State: 6 {1 2}\n", - "[t] 6\n", - "State: 7 {3}\n", - "[0&!1&!2] 0\n", - "[0&!1&2] 1\n", - "[!0&!2] 5\n", - "[!0&2] 6\n", - "[0&1&!2] 7\n", - "[0&1&2] 8\n", - "State: 8 {3}\n", - "[0&!1] 1\n", - "[!0] 6\n", - "[0&1] 8\n", - "--END--\n", - "\"\"\")\n", + "HOA: v1 States: 9 Start: 2 AP: 3 \"a\" \"b\" \"c\" acc-name: Rabin 2 Acceptance:\n", + "4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) properties: trans-labels\n", + "explicit-labels state-acc complete properties: deterministic --BODY--\n", + "State: 0 {2} [0&!2] 0 [0&2] 1 [!0&!2] 5 [!0&2] 6 State: 1 {2} [0] 1 [!0]\n", + "6 State: 2 {2} [0&!1&!2] 3 [0&1&!2] 4 [!0&!2] 5 [2] 6 State: 3 {1 2}\n", + "[0&!2] 0 [0&2] 1 [!0&!2] 5 [!0&2] 6 State: 4 {1 2} [0&!1&!2] 0 [0&!1&2]\n", + "1 [!0&!2] 5 [!0&2] 6 [0&1&!2] 7 [0&1&2] 8 State: 5 {1 2} [0&!1&!2] 0\n", + "[!0&!2] 5 [2] 6 [0&1&!2] 7 State: 6 {1 2} [t] 6 State: 7 {3} [0&!1&!2]\n", + "0 [0&!1&2] 1 [!0&!2] 5 [!0&2] 6 [0&1&!2] 7 [0&1&2] 8 State: 8 {3} [0&!1]\n", + "1 [!0] 6 [0&1] 8 --END--\"\"\")\n", "aut" ] }, @@ -1942,7 +1898,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0eaa50> >" + " *' at 0x7f1aa00b6510> >" ] }, "metadata": {}, @@ -2174,7 +2130,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc092cc0> >" + " *' at 0x7f1aa01baea0> >" ] }, "metadata": {}, @@ -2384,7 +2340,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc21dea0> >" + " *' at 0x7f1aa01bad80> >" ] }, "metadata": {}, @@ -2772,7 +2728,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0ea7b0> >" + " *' at 0x7f1aa00b6570> >" ] }, "execution_count": 10, @@ -2933,7 +2889,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0ab3f0> >" + " *' at 0x7f1aa00b6e70> >" ] }, "metadata": {}, @@ -3072,7 +3028,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc211570> >" + " *' at 0x7f1aa01baf00> >" ] }, "metadata": {}, @@ -3224,7 +3180,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc23fa80> >" + " *' at 0x7f1aa00b6a20> >" ] }, "metadata": {}, @@ -3577,7 +3533,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc21d750> >" + " *' at 0x7f1aa00b6120> >" ] }, "execution_count": 12, @@ -3587,55 +3543,15 @@ ], "source": [ "aut = spot.automaton(\"\"\"\n", - "HOA: v1\n", - "States: 8\n", - "Start: 7\n", - "AP: 3 \"a\" \"b\" \"c\"\n", - "acc-name: Streett 2\n", - "Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\n", - "properties: trans-labels explicit-labels state-acc complete\n", - "properties: deterministic\n", - "--BODY--\n", - "State: 0 {2}\n", - "[0&1] 0\n", - "[0&!1] 3\n", - "[!0] 4\n", - "State: 1 {2}\n", - "[0&1&2] 0\n", - "[0&1&!2] 1\n", - "[0&!1&!2] 2\n", - "[0&!1&2] 3\n", - "[!0&2] 4\n", - "[!0&!2] 7\n", - "State: 2 {2}\n", - "[0&1&!2] 1\n", - "[0&!1&!2] 2\n", - "[0&2] 3\n", - "[!0&2] 4\n", - "[!0&!2] 7\n", - "State: 3 {0 3}\n", - "[0] 3\n", - "[!0] 4\n", - "State: 4 {1 3}\n", - "[t] 4\n", - "State: 5 {3}\n", - "[0&!1] 3\n", - "[!0] 4\n", - "[0&1] 5\n", - "State: 6 {3}\n", - "[0&!1&!2] 2\n", - "[0&!1&2] 3\n", - "[!0&2] 4\n", - "[0&1&2] 5\n", - "[0&1&!2] 6\n", - "[!0&!2] 7\n", - "State: 7 {3}\n", - "[0&!1&!2] 2\n", - "[2] 4\n", - "[0&1&!2] 6\n", - "[!0&!2] 7\n", - "--END--\n", - "\"\"\")\n", + "HOA: v1 States: 8 Start: 7 AP: 3 \"a\" \"b\" \"c\" acc-name: Streett\n", + "2 Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) properties:\n", + "trans-labels explicit-labels state-acc complete properties: deterministic\n", + "--BODY-- State: 0 {2} [0&1] 0 [0&!1] 3 [!0] 4 State: 1 {2} [0&1&2]\n", + "0 [0&1&!2] 1 [0&!1&!2] 2 [0&!1&2] 3 [!0&2] 4 [!0&!2] 7 State: 2 {2}\n", + "[0&1&!2] 1 [0&!1&!2] 2 [0&2] 3 [!0&2] 4 [!0&!2] 7 State: 3 {0 3} [0] 3\n", + "[!0] 4 State: 4 {1 3} [t] 4 State: 5 {3} [0&!1] 3 [!0] 4 [0&1] 5 State:\n", + "6 {3} [0&!1&!2] 2 [0&!1&2] 3 [!0&2] 4 [0&1&2] 5 [0&1&!2] 6 [!0&!2]\n", + "7 State: 7 {3} [0&!1&!2] 2 [2] 4 [0&1&!2] 6 [!0&!2] 7 --END--\"\"\")\n", "aut" ] }, @@ -3960,7 +3876,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0ea480> >" + " *' at 0x7f1aa00c01b0> >" ] }, "metadata": {}, @@ -4137,7 +4053,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc23fae0> >" + " *' at 0x7f1aa00b6f60> >" ] }, "metadata": {}, @@ -4295,7 +4211,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc092c00> >" + " *' at 0x7f1aa029e660> >" ] }, "metadata": {}, @@ -4313,7 +4229,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "The subtlety of Streett acceptance is that if a path that does not visit any accepting set infinitely often *is* accepting. So when disabling SCCs, we must be careful to label them with a combination of rejecting acceptance sets.\n", + "The subtlety of Streett acceptance is that a path that does not visit any accepting set infinitely often *is* accepting. So when disabling SCCs, we must be careful to label them with a combination of rejecting acceptance sets.\n", "\n", "This is easy to understand using an example. In the following extraction of the **strong** and **inherently terminal** parts, the rejecting SCCs (that were either rejecting or strictly inherently weak originally) have been labeled by the same acceptance sets, to ensure that they are rejected." ] @@ -4644,7 +4560,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0ea3c0> >" + " *' at 0x7f1aa00c0a80> >" ] }, "execution_count": 14, @@ -4767,7 +4683,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc23fbd0> >" + " *' at 0x7f1aa00c0540> >" ] }, "execution_count": 15, @@ -4865,7 +4781,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0eac90> >" + " *' at 0x7f1aa00c8090> >" ] }, "metadata": {}, @@ -4941,7 +4857,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc21d7e0> >" + " *' at 0x7f1aa00c0270> >" ] }, "metadata": {}, @@ -5035,7 +4951,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0eaab0> >" + " *' at 0x7f1aa00c8090> >" ] }, "execution_count": 18, @@ -5185,7 +5101,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0ab6f0> >" + " *' at 0x7f1aa00c8a50> >" ] }, "execution_count": 19, @@ -5345,7 +5261,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0abb70> >" + " *' at 0x7f1aa00d0cc0> >" ] }, "metadata": {}, @@ -5447,7 +5363,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc092c00> >" + " *' at 0x7f1aa00b6780> >" ] }, "metadata": {}, @@ -5582,7 +5498,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0abae0> >" + " *' at 0x7f1aa00c0570> >" ] }, "metadata": {}, @@ -5606,7 +5522,7 @@ "# `decompose_scc()` by SCC number\n", "\n", "Decompose SCC can also be called by SCC numbers.\n", - "The example below show the different SCC numbers and the state they contains, before extracting the sub-automaton containing SCC 0 and 2 (i.e., anything leading to states 1 and 4 of the original automaton). This example also shows that when an `scc_info` is available for to automaton to decompose, it can be passed to `decompose_scc()` in lieu of the automaton: doing so is faster because `decompose_scc()` does not need to rebuild this object. " + "The example below show the different SCC numbers and the state they contains, before extracting the sub-automaton containing SCC 0 and 1 (i.e., anything leading to states 1 and 4 of the original automaton). This example also shows that when an `scc_info` is available for to automaton to decompose, it can be passed to `decompose_scc()` in lieu of the automaton: doing so is faster because `decompose_scc()` does not need to rebuild this object. " ] }, { @@ -5619,9 +5535,9 @@ "output_type": "stream", "text": [ "SCC #0 contains states [1]\n", - "SCC #1 contains states [2]\n", - "SCC #2 contains states [4]\n", - "SCC #3 contains states [0, 3]\n" + "SCC #1 contains states [4]\n", + "SCC #2 contains states [3]\n", + "SCC #3 contains states [0, 2]\n" ] }, { @@ -5647,11 +5563,11 @@ "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "\n", "cluster_2\n", - "\n", + "\n", "\n", "\n", "cluster_3\n", @@ -5691,28 +5607,28 @@ "\n", "c\n", "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", - "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", "\n", "\n", "a & !c\n", @@ -5725,16 +5641,8 @@ "1\n", "⓿\n", "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "b\n", - "⓿\n", - "\n", "\n", - "\n", + "\n", "4\n", "\n", "4\n", @@ -5753,31 +5661,39 @@ "\n", "a\n", "\n", - "\n", - "\n", - "3->0\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "⓿\n", + "\n", + "\n", + "\n", + "2->0\n", "\n", "\n", "!a & !c\n", "⓿\n", "\n", - "\n", - "\n", - "3->1\n", + "\n", + "\n", + "2->1\n", "\n", "\n", "!a & c\n", "\n", - "\n", - "\n", - "3->4\n", + "\n", + "\n", + "2->4\n", "\n", "\n", "a & c\n", "\n", - "\n", - "\n", - "3->3\n", + "\n", + "\n", + "2->2\n", "\n", "\n", "a & !c\n", @@ -5786,7 +5702,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0ea1e0> >" + " *' at 0x7f1aa00c85d0> >" ] }, "metadata": {}, @@ -5927,7 +5843,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0ea630> >" + " *' at 0x7f1aa00c8cf0> >" ] }, "execution_count": 21, @@ -5941,14 +5857,14 @@ "for scc in range(si.scc_count()):\n", " print(\"SCC #{} contains states {}\".format(scc, list(si.states_of(scc))))\n", "display(aut)\n", - "spot.decompose_scc(si, '0,2')" + "spot.decompose_scc(si, '0,1')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ - "If an SCC number N is prefixed by `a`, it signifies that we want to extract the Nth *accepting* SCC. In the above example SCC 2 is rejecting so SCC `a2` denotes SCC 3." + "If an SCC number N is prefixed by `a`, it signifies that we want to extract the (N+1)th *accepting* SCC. In the above example SCC 1 is rejecting so `a0`, `a1`, and `a2` denote respectively SCCs 0, 2, and 3." ] }, { @@ -6030,7 +5946,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f09cc0eae70> >" + " *' at 0x7f1aa00c8b10> >" ] }, "execution_count": 22, @@ -6059,7 +5975,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.9.1+" + "version": "3.9.2" } }, "nbformat": 4, diff --git a/tests/python/decompose_scc.py b/tests/python/decompose_scc.py index 238a64547..5f6ad46cb 100644 --- a/tests/python/decompose_scc.py +++ b/tests/python/decompose_scc.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et +# Copyright (C) 2017, 2021 Laboratoire de Recherche et # Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -22,7 +22,14 @@ import spot aut = spot.translate('(Ga -> Gb) W c') si = spot.scc_info(aut) -assert (spot.decompose_scc(si, 2).to_str('hoa', '1.1') == """HOA: v1.1 +# Extract the only rejecting SCC. Its number might differ +# if the generation of the automaton changes, so just scan +# for it. +rej = [j for j in range(si.scc_count()) if si.is_rejecting_scc(j)] +assert len(rej) == 1 +s = spot.decompose_scc(si, rej[0]).to_str('hoa', '1.1') + +assert (s == """HOA: v1.1 States: 3 Start: 0 AP: 3 "b" "a" "c" diff --git a/tests/python/dualize.py b/tests/python/dualize.py index 6a054bf10..81d2a2b23 100755 --- a/tests/python/dualize.py +++ b/tests/python/dualize.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017-2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2017-2019, 2021 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -573,17 +573,17 @@ properties: deterministic univ-branch --BODY-- State: 0 {0} [0&1] 0 -[0&!1] 1 +[0&!1] 2 +[!0&1] 0&1 [!0&!1] 1&2 -[!0&1] 0&2 State: 1 -[0&1] 0 -[0&!1] 1 -[!0&!1] 1&2 -[!0&1] 0&2 -State: 2 [!0&1] 3 [0 | !1] 4 +State: 2 +[0&1] 0 +[0&!1] 2 +[!0&1] 0&1 +[!0&!1] 1&2 State: 3 {0} [!0] 3 [0] 4 diff --git a/tests/python/sccinfo.py b/tests/python/sccinfo.py index ddf5d69f6..fc6eeeea3 100644 --- a/tests/python/sccinfo.py +++ b/tests/python/sccinfo.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2017, 2021 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -75,10 +75,10 @@ while todo: todo.add(s) assert seen == {0, 1, 2, 3} assert trans == [(0, 0), (0, 1), (0, 2), (0, 3), - (3, 0), (3, 1), (3, 3), (3, 4), - (1, 1), (2, 2), (4, 1), (4, 4)] -assert transi == [(0, 0, 1), (0, 3, 4), (3, 0, 7), - (3, 3, 9), (1, 1, 5), (2, 2, 6), (4, 4, 12)] + (2, 0), (2, 1), (2, 2), (2, 4), + (1, 1), (4, 1), (4, 4), (3, 3)] +assert transi == [(0, 0, 1), (0, 2, 3), (2, 0, 6), + (2, 2, 8), (1, 1, 5), (4, 4, 12), (3, 3, 10)] assert not spot.is_weak_automaton(a, si) diff --git a/tests/python/simstate.py b/tests/python/simstate.py index d24962721..3a639b094 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -620,24 +620,24 @@ properties: trans-labels explicit-labels trans-acc stutter-invariant State: 0 [0] 0 [!0] 1 {0} -[0&1] 2 {0} -[!0&1] 3 +[!0&1] 2 +[0&1] 3 {0} State: 1 [1] 1 [!1] 1 {0} -[!0&1] 3 +[!0&1] 2 [0&1] 4 State: 2 -[0&1] 2 {0} -State: 3 [!1] 1 {0} -[!0&1] 3 +[!0&1] 2 [0&1] 5 +State: 3 +[0&1] 3 {0} State: 4 [0&!1] 6 State: 5 [!0&!1] 1 {0} -[!0&1] 3 +[!0&1] 2 [0&1] 5 [0&!1] 6 {0} State: 6 diff --git a/tests/python/testingaut.ipynb b/tests/python/testingaut.ipynb index 7dd2de302..36e7faa57 100644 --- a/tests/python/testingaut.ipynb +++ b/tests/python/testingaut.ipynb @@ -34,11 +34,11 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -62,29 +62,29 @@ "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f930090abd0> >" + " *' at 0x7fb57416b570> >" ] }, "execution_count": 2, @@ -119,272 +119,272 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "init\n", + "\n", + "init\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "0\n", - "!a & b\n", + "\n", + "0\n", + "!a & b\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "3\n", - "\n", - "0\n", - "a & b\n", + "\n", + "0\n", + "a & !b\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "4\n", - "\n", - "0\n", - "a & !b\n", + "\n", + "0\n", + "a & b\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "5\n", - "\n", - "\n", - "1\n", - "a & b\n", + "\n", + "\n", + "1\n", + "!a & !b\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "\n", "6\n", - "\n", - "\n", - "1\n", - "!a & b\n", + "\n", + "\n", + "1\n", + "!a & b\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", - "{}\n", + "\n", + "\n", + "{}\n", "\n", "\n", "\n", "7\n", - "\n", - "\n", - "1\n", - "a & !b\n", + "\n", + "\n", + "1\n", + "a & !b\n", "\n", "\n", "\n", "2->7\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "\n", "8\n", - "\n", - "\n", - "1\n", - "!a & !b\n", + "\n", + "\n", + "1\n", + "a & b\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "{}\n", + "\n", + "\n", + "{}\n", "\n", "\n", - "\n", + "\n", "3->4\n", - "\n", - "\n", - "{b}\n", - "\n", - "\n", - "\n", - "3->5\n", - "\n", - "\n", - "{}\n", - "\n", - "\n", - "\n", - "3->6\n", - "\n", - "\n", - "{a}\n", - "\n", - "\n", - "\n", - "3->7\n", - "\n", - "\n", - "{b}\n", - "\n", - "\n", - "\n", - "3->8\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "\n", "9\n", - "\n", - "0\n", - "!a & !b\n", + "\n", + "0\n", + "!a & !b\n", "\n", "\n", - "\n", + "\n", "3->9\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "\n", + "\n", "4->2\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "\n", + "\n", "4->3\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", - "\n", + "\n", "4->4\n", - "\n", - "\n", - "{}\n", + "\n", + "\n", + "{}\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "{a, b}\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "\n", + "4->8\n", + "\n", + "\n", + "{}\n", "\n", "\n", - "\n", + "\n", "4->9\n", - "\n", - "\n", - "{a}\n", - "\n", - "\n", - "\n", - "5->5\n", - "\n", - "\n", - "{}\n", - "\n", - "\n", - "\n", - "5->6\n", - "\n", - "\n", - "{a}\n", - "\n", - "\n", - "\n", - "5->7\n", - "\n", - "\n", - "{b}\n", - "\n", - "\n", - "\n", - "5->8\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", - "\n", + "\n", "6->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", - "\n", + "\n", "6->6\n", - "\n", - "\n", - "{}\n", + "\n", + "\n", + "{}\n", "\n", "\n", - "\n", + "\n", "6->7\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", - "\n", + "\n", "6->8\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "\n", + "8->5\n", + "\n", + "\n", + "{a, b}\n", + "\n", + "\n", + "\n", + "8->6\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "\n", + "8->7\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "\n", + "8->8\n", + "\n", + "\n", + "{}\n", "\n", "\n", "\n" @@ -425,137 +425,137 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "init\n", + "\n", + "init\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "0\n", - "!a & b\n", + "\n", + "0\n", + "!a & b\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "3\n", - "\n", - "0\n", - "a & b\n", + "\n", + "0\n", + "a & !b\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "4\n", - "\n", - "0\n", - "a & !b\n", + "\n", + "0\n", + "a & b\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "5\n", - "\n", - "\n", - "1\n", - "a & b\n", + "\n", + "\n", + "1\n", + "a & b\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "{b}\n", - "\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "1\n", - "!a & b\n", - "\n", - "\n", - "\n", - "3->6\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", - "\n", + "\n", "4->2\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "1\n", + "!a & b\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "\n", "5->6\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "\n" @@ -595,118 +595,118 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "init\n", + "\n", + "init\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "1\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "4\n", - "\n", - "1\n", + "\n", + "3\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "5\n", - "\n", - "\n", - "4\n", + "\n", + "\n", + "4\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "{b}\n", - "\n", - "\n", - "\n", - "3->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", - "\n", + "\n", "4->2\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "\n" @@ -723,6 +723,13 @@ "source": [ "spot.minimize_ta(ta).show('.A')" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -741,7 +748,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.7.5" + "version": "3.9.2" } }, "nbformat": 4, diff --git a/tests/python/word.ipynb b/tests/python/word.ipynb index af7bc95ea..26f891bca 100644 --- a/tests/python/word.ipynb +++ b/tests/python/word.ipynb @@ -31,14 +31,14 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -68,105 +68,105 @@ "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", - "\n", - "\n", - "2->5\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "a & b\n", - "⓿\n", - "\n", - "\n", + "\n", "\n", - "3->3\n", - "\n", - "\n", - "!a & b\n", + "3->5\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", "\n", "\n", "\n", "5->4\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f956c0198d0> >" + " *' at 0x7f14f57d93c0> >" ] }, "execution_count": 2, @@ -198,10 +198,12 @@ " 0\n", " | !a\n", " 1\n", - " | a\n", + " | !a\n", "Cycle:\n", " 2\n", " | a & b\t{0}\n", + " 3\n", + " | !a & b\n", "\n" ] } @@ -253,16 +255,16 @@ "name": "stdout", "output_type": "stream", "text": [ - "!a; a; cycle{a & b}\n" + "!a; !a; cycle{a & b; !a & b}\n" ] }, { "data": { "text/latex": [ - "$\\lnot a; a; \\mathsf{cycle}\\{a \\land b\\}$" + "$\\lnot a; \\lnot a; \\mathsf{cycle}\\{a \\land b; \\lnot a \\land b\\}$" ], "text/plain": [ - " *' at 0x7f956c019de0> >" + " *' at 0x7f14f57d9ed0> >" ] }, "execution_count": 5, @@ -292,14 +294,14 @@ "data": { "image/svg+xml": [ "\n", - "\n", - "\n", + "\n", + "\n", "\n", - "\n", - "abprefixcycle\n", - "cycle" + "abprefixcycle\n", + "cycle" ], "text/plain": [ "" @@ -331,22 +333,24 @@ "output_type": "stream", "text": [ "!a\n", - "a\n", - "a & b\n" + "!a\n", + "a & b\n", + "!a & b\n" ] } ], "source": [ "print(spot.bdd_format_formula(aut.get_dict(), word.prefix[0]))\n", "print(spot.bdd_format_formula(aut.get_dict(), word.prefix[1]))\n", - "print(spot.bdd_format_formula(aut.get_dict(), word.cycle[0]))" + "print(spot.bdd_format_formula(aut.get_dict(), word.cycle[0]))\n", + "print(spot.bdd_format_formula(aut.get_dict(), word.cycle[1]))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ - "Calling `simplifify()` will produce a shorter word that is compatible with the original word. For instance in the above word, the initial `a` is compatible with both `a & b` and `a & !b`. The word obtained by restricting `a` to `a & b` is therefore still accepted, allowing us to remove the prefix." + "Calling `simplifify()` will produce a shorter word that is compatible with the original word. For instance in the above word, the second `a` is compatible with `!a & b`, so the prefix can be shortened by rotating the cycle." ] }, { @@ -358,7 +362,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "!a; cycle{a & b}\n" + "!a; cycle{!a & b; a & b}\n" ] } ], @@ -382,10 +386,10 @@ { "data": { "text/latex": [ - "$\\lnot a; \\mathsf{cycle}\\{a \\land b\\}$" + "$\\lnot a; \\mathsf{cycle}\\{\\lnot a \\land b; a \\land b\\}$" ], "text/plain": [ - " *' at 0x7f956c0388a0> >" + " *' at 0x7f14f57d9660> >" ] }, "execution_count": 9, @@ -436,7 +440,7 @@ "$a; a \\land b; \\mathsf{cycle}\\{\\lnot a \\land \\lnot b; \\lnot a \\land b\\}$" ], "text/plain": [ - " *' at 0x7f956c038b70> >" + " *' at 0x7f14f5799ea0> >" ] }, "execution_count": 11, @@ -501,76 +505,76 @@ "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f956c0388d0> >" + " *' at 0x7f14f5799ed0> >" ] }, "execution_count": 13, @@ -599,7 +603,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.7.5" + "version": "3.9.2" } }, "nbformat": 4,