From 0e71dd70c157d008b6bfa9299bcf1efe77be21fd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 17 Nov 2023 13:41:19 +0100 Subject: [PATCH] sccfilter: some inherently-weak automata should have t acceptance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * spot/twaalgos/sccfilter.cc: If an inherently-weak automaton has no rejecting cycle, reduce its acceptance to t instead of Büchi. * spot/twa/acc.hh (operator==, operator<): Fix comparisons of true acceptances. * NEWS: Mention these two changes. * spot/twaalgos/sccfilter.hh: Update documentation. * spot/twaalgos/determinize.cc (tgba_determinize): The call to scc_filter assume that the input BA is never reduced to t acceptance. Call scc_filter with an extra option to ensure that. * spot/twaalgos/postproc.cc (do_scc_filter): Adjust to add the extra option when we want to build Büchi or coBuchi. (ensure_ba): Don't mark trivial SCCs as accepting. * tests/core/complement.test, tests/core/dstar.test, tests/core/ltlsynt.test, tests/core/readsave.test, tests/core/wdba2.test, tests/python/_product_susp.ipynb, tests/python/automata-io.ipynb, tests/python/dualize.py, tests/python/highlighting.ipynb, tests/python/intrun.py, tests/python/setacc.py, tests/python/simstate.py, tests/python/stutter-inv.ipynb, tests/python/zlktree.py: Adjust test cases. --- NEWS | 13 + spot/twa/acc.hh | 12 +- spot/twaalgos/determinize.cc | 2 +- spot/twaalgos/postproc.cc | 27 +- spot/twaalgos/sccfilter.cc | 40 ++- spot/twaalgos/sccfilter.hh | 17 +- tests/core/complement.test | 4 +- tests/core/dstar.test | 6 +- tests/core/ltlsynt.test | 14 +- tests/core/readsave.test | 29 +- tests/core/wdba2.test | 8 +- tests/python/_product_susp.ipynb | 548 +++++++++++++++---------------- tests/python/automata-io.ipynb | 498 ++++++++++++++-------------- tests/python/dualize.py | 4 +- tests/python/highlighting.ipynb | 327 +++++++++--------- tests/python/intrun.py | 16 +- tests/python/setacc.py | 6 +- tests/python/simstate.py | 3 +- tests/python/stutter-inv.ipynb | 124 +++---- tests/python/zlktree.py | 1 + 20 files changed, 857 insertions(+), 842 deletions(-) diff --git a/NEWS b/NEWS index 72e24d612..d89e92050 100644 --- a/NEWS +++ b/NEWS @@ -108,6 +108,15 @@ New in spot 2.11.6.dev (not yet released) removal of superfluous APs that is now performed by ltlsynt (search for --polarity and --global-equivalence above). + - scc_filter used to reduce automata tagged with the inherently-weak + property to weak Büchi automata (unless the acceptance was already + t or co-Büchi). In case where the input automaton had no + rejecting cycle, the Büchi acceptance was overkill: scc_filter + will now use "t" acceptance. This change may have unexpected + conseqences in code paths that assume running scc_filter on a + Büchi automaton will always return a Büchi automaton. For those, + a "keep_one_color" option has been added to scc_filter. + - ltsmin's interface will now point to README.ltsmin in case an error is found while running divine or spins. @@ -143,6 +152,10 @@ New in spot 2.11.6.dev (not yet released) - The automaton parser forgot to update the list of highlighted edges while dropping edges labeled by bddfalse. (issue #548.) + - The comparison operators for acceptance condition (==, !=) + could fail to equate two "t" condition, because we have two ways + to represent "t": the empty condition, or the empty "Inf({})". + New in spot 2.11.6 (2023-08-01) Bug fixes: diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 766dd5224..b7817aa0b 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -482,6 +482,9 @@ namespace spot bool operator==(const acc_code& other) const { + // We have two ways to represent t, unfortunately. + if (is_t() && other.is_t()) + return true; unsigned pos = size(); if (other.size() != pos) return false; @@ -513,6 +516,9 @@ namespace spot bool operator<(const acc_code& other) const { + // We have two ways to represent t, unfortunately. + if (is_t() && other.is_t()) + return false; unsigned pos = size(); auto osize = other.size(); if (pos < osize) @@ -1560,7 +1566,11 @@ namespace spot bool operator==(const acc_cond& other) const { - return other.num_sets() == num_ && other.get_acceptance() == code_; + if (other.num_sets() != num_) + return false; + const acc_code& ocode = other.get_acceptance(); + // We have two ways to represent t, unfortunately. + return (ocode == code_ || (ocode.is_t() && code_.is_t())); } bool operator!=(const acc_cond& other) const diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index 2bc84cd6a..c87d992dd 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -881,7 +881,7 @@ namespace spot aut_tmp->copy_state_names_from(a); if (use_simulation) { - aut_tmp = spot::scc_filter(aut_tmp); + aut_tmp = spot::scc_filter(aut_tmp, true, nullptr, true); auto aut2 = simulation(aut_tmp, &implications, trans_pruning); if (pretty_print) aut2->copy_state_names_from(aut_tmp); diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 1a2915dda..cbf677414 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -47,13 +47,28 @@ namespace spot namespace { static twa_graph_ptr - ensure_ba(twa_graph_ptr& a) + ensure_ba(twa_graph_ptr& a, bool no_trivial) { if (a->acc().is_t()) { auto m = a->set_buchi(); - for (auto& t: a->edges()) - t.acc = m; + if (!no_trivial) + { + for (auto& t: a->edges()) + t.acc = m; + } + else + { + scc_info si(a); + unsigned nc = si.scc_count(); + for (unsigned i = 0; i < nc; ++i) + // Cannot use "is_accepting_scc" because the + // acceptance condition was already changed. + if (!si.is_trivial(i)) + for (auto& e: si.edges_of(i)) + const_cast(e.acc) = m; + } + a->prop_state_acc(true); } return a; } @@ -219,7 +234,7 @@ namespace spot if (state_based_ && a->prop_state_acc().is_true()) return scc_filter_states(a, arg); else - return scc_filter(a, arg); + return scc_filter(a, arg, nullptr, type_ == CoBuchi || type_ == Buchi); } twa_graph_ptr @@ -251,7 +266,7 @@ namespace spot if (state_based_) tmp = sbacc(tmp); if (type_ == Buchi) - tmp = ensure_ba(tmp); + tmp = ensure_ba(tmp, level_ == High); if (want_parity) { if (!acd_was_used_ || (COMP_ && !was_complete)) @@ -480,7 +495,7 @@ namespace spot // We just need to add an acceptance set if there is none. dba_is_minimal = dba_is_wdba = true; if (type_ == Buchi) - ensure_ba(dba); + ensure_ba(dba, level_ == High); } else { diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index 20dea3f7e..9d8f2cfca 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -124,12 +124,14 @@ namespace spot } }; - // Transform inherently weak automata into weak Büchi automata. - template + // Transform inherently weak automata into weak Büchi automata, or + // t automata. + template struct weak_filter: next_filter { acc_cond::mark_t acc_m = {0}; acc_cond::mark_t rej_m = {}; + bool true_acc = false; template weak_filter(scc_info* si, Args&&... args) @@ -141,6 +143,23 @@ namespace spot if (si->get_aut()->acc().is_co_buchi()) rej_m = {0}; } + if (!keep_one_color) + { + unsigned ns = si->scc_count(); + bool may_reject = false; + for (unsigned i = 0; i < ns; ++i) + if (!si->is_trivial(i) && !si->is_accepting_scc(i)) + { + may_reject = true; + break; + } + if (!may_reject) + { + true_acc = true; + acc_m = {}; + rej_m = {}; + } + } } filtered_trans trans(unsigned src, unsigned dst, @@ -164,7 +183,9 @@ namespace spot void fix_acceptance(const twa_graph_ptr& out) { - if (buchi) + if (true_acc) + out->set_generalized_buchi(0); + else if (buchi) out->set_buchi(); else out->copy_acceptance_of(this->si->get_aut()); @@ -216,8 +237,8 @@ namespace spot // // The above rules are made more complex with two flags: // - // - If PreserveSBA is set, we have to tree a transition - // leaving an SCC as other transitions inside the SCC, + // - If PreserveSBA is set, we have to treat a transition + // leaving an SCC like other transitions inside the SCC, // otherwise we will break the property that all // transitions leaving the same state have identical set // membership. @@ -442,7 +463,7 @@ namespace spot twa_graph_ptr scc_filter(const const_twa_graph_ptr& aut, bool remove_all_useless, - scc_info* given_si) + scc_info* given_si, bool keep_one_color) { twa_graph_ptr res; scc_info* si = given_si; @@ -455,10 +476,13 @@ namespace spot | scc_info_options::TRACK_STATES_IF_FIN_USED); if (aut->acc().is_t() || aut->acc().is_co_buchi()) res = - scc_filter_apply>>(aut, si); + scc_filter_apply>>(aut, si); + else if (keep_one_color) + res = + scc_filter_apply>>(aut, si); else res = - scc_filter_apply>>(aut, si); + scc_filter_apply>>(aut, si); } else if (aut->acc().is_generalized_buchi()) { diff --git a/spot/twaalgos/sccfilter.hh b/spot/twaalgos/sccfilter.hh index 6c1451912..4d34ca5d4 100644 --- a/spot/twaalgos/sccfilter.hh +++ b/spot/twaalgos/sccfilter.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015, 2018 Laboratoire de +// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015, 2018, 2023 Laboratoire de // Recherche et Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -51,20 +51,25 @@ namespace spot /// accepting SCC are accepting. /// /// If the input is inherently weak, the output will be a weak - /// automaton with state-based acceptance. The acceptance condition - /// is set to Büchi unless the input was co-Büchi or t (in which - /// case we keep this acceptance). + /// automaton with state-based acceptance. If the automaton had no + /// rejecting SCC, the acceptance condition is set to "t". + /// Otherwise, the acceptance condition is set to Büchi unless the + /// input was co-Büchi (in which case we keep this acceptance). /// - /// If \a given_sm is supplied, the function will use its result + /// If \a given_si is supplied, the function will use its result /// without computing a map of its own. /// + /// If \a keep_one_color is set, the output will keep at least color + /// if the input had colors. Normally scc_filter removes as many + /// colors as possible. + /// /// \warning Calling scc_filter on a TωA that is not inherently weak /// and has the SBA property (i.e., transitions leaving accepting /// states are all marked as accepting) may destroy this property. /// Use scc_filter_states() instead. SPOT_API twa_graph_ptr scc_filter(const const_twa_graph_ptr& aut, bool remove_all_useless = false, - scc_info* given_si = nullptr); + scc_info* given_si = nullptr, bool keep_one_color = false); /// \brief Prune unaccepting SCCs. /// diff --git a/tests/core/complement.test b/tests/core/complement.test index ebaafa1c2..d6d0eebd5 100755 --- a/tests/core/complement.test +++ b/tests/core/complement.test @@ -76,10 +76,10 @@ Acceptance: 1 Fin(0) properties: trans-labels explicit-labels state-acc complete properties: deterministic very-weak --BODY-- -State: 0 +State: 0 {0} [0] 2 [!0] 3 -State: 1 +State: 1 {0} [t] 0 State: 2 {0} [t] 2 diff --git a/tests/core/dstar.test b/tests/core/dstar.test index 80ad5ac37..c745ced4e 100755 --- a/tests/core/dstar.test +++ b/tests/core/dstar.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013-2016, 2018, 2020, 2022 Laboratoire de Recherche -# et Développement de l'Epita (LRDE). +# Copyright (C) 2013-2016, 2018, 2020, 2022, 2023 Laboratoire de +# Recherche et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -298,7 +298,7 @@ digraph "aut.dsa" { I [label="", style=invis, width=0] I -> 0 0 [label="0"] - 0 -> 0 [label="1\n{0}"] + 0 -> 0 [label="1"] } EOF diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index f11e1dbd1..d1a7a9dee 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -736,7 +736,7 @@ there are 2 subformulas trying to create strategy directly for (b & (b | y)) -> y direct strategy might exist but was not found. translating formula done in X seconds -automaton has 2 states and 1 colors +automaton has 2 states and 0 colors LAR construction done in X seconds DPA has 2 states, 0 colors split inputs and outputs done in X seconds @@ -747,7 +747,7 @@ simplification took X seconds trying to create strategy directly for (a | x) -> x direct strategy might exist but was not found. translating formula done in X seconds -automaton has 2 states and 1 colors +automaton has 2 states and 0 colors LAR construction done in X seconds DPA has 2 states, 0 colors split inputs and outputs done in X seconds @@ -850,7 +850,7 @@ there are 3 subformulas trying to create strategy directly for a -> b direct strategy might exist but was not found. translating formula done in X seconds -automaton has 2 states and 1 colors +automaton has 2 states and 0 colors LAR construction done in X seconds DPA has 2 states, 0 colors split inputs and outputs done in X seconds @@ -861,7 +861,7 @@ simplification took X seconds trying to create strategy directly for a -> c direct strategy might exist but was not found. translating formula done in X seconds -automaton has 2 states and 1 colors +automaton has 2 states and 0 colors LAR construction done in X seconds DPA has 2 states, 0 colors split inputs and outputs done in X seconds @@ -872,7 +872,7 @@ simplification took X seconds trying to create strategy directly for a -> d direct strategy might exist but was not found. translating formula done in X seconds -automaton has 2 states and 1 colors +automaton has 2 states and 0 colors LAR construction done in X seconds DPA has 2 states, 0 colors split inputs and outputs done in X seconds @@ -934,7 +934,7 @@ ltlsynt -f 'G(c) & (G(a) <-> GFb)' --outs=b,c --decompose=yes --pol=no \ cat >exp <expected <, 5, 1 , 5, 1 , 4, 1 -, 4, 1 , 4, 1 , 6, 1 <(a & !b & (b | (!b M F!a))) | (!a & (b | (!b & (b W Ga)))), 3 states>, 5, 1 <(a & (a U !b)) | (!a & (!a R b)), 3 states>, 5, 1 -, 4, 1 -, 3, 1 +, 4, 1 +<((a & F!b) | (!a & Gb)) U (Fa & G!b), 3 states>, 6, 1 +, 4, 1 EOF diff output expected @@ -580,12 +580,12 @@ digraph "" { rankdir=LR node [shape="ellipse",width="0.5",height="0.5"] I [label="", style=invis, width=0] - 0 [label="6", peripheries=2] + 0 [label="6"] u0 [label="...", shape=none, width=0, height=0, tooltip="hidden successors"] - 1 [label="0", peripheries=2] - 2 [label="1", peripheries=2] - 3 [label="2", peripheries=2] - 4 [label="3", peripheries=2] + 1 [label="0"] + 2 [label="1"] + 3 [label="2"] + 4 [label="3"] } EOF @@ -806,8 +806,8 @@ HOA: v1 States: 3 Start: 1 AP: 2 "a" "b" -acc-name: Buchi -Acceptance: 1 Inf(0) +acc-name: all +Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic properties: very-weak --BODY-- @@ -815,7 +815,7 @@ State: 0 [1] 2 State: 1 [0] 0 -State: 2 {0} +State: 2 [0] 2 --END-- EOF @@ -824,14 +824,15 @@ diff output4 expect4 diff output4b expect4 diff output4c expect4 -autfilt -Hv --small input4 >output5 test `autfilt --is-weak -c output4` = 1 +test `autfilt -B --small output4d | autfilt --is-terminal -c` = 0 test `autfilt --is-terminal -c output4` = 0 sed 's/\[0\]/[t]/g' expect4 > output4d -test `autfilt --is-terminal -c output4d` = 1 - +test `autfilt -B --small output4d | autfilt --is-terminal -c` = 1 +test `autfilt --is-terminal -c output4d` = 0 # FIXME: Issue #553 +autfilt -B -Hv --small input4 >output5 cat >expect5<\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "6\n", - "\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "I->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "a & b & c\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "6->0\n", - "\n", - "\n", - "!a & !b & c\n", + "\n", + "\n", + "!a & !b & c\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "!a & b & c\n", + "\n", + "\n", + "!a & b & c\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "\n", "4\n", - "\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "6->4\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n", "5\n", - "\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!b & c\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b & c\n", + "\n", + "\n", + "b & c\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "b & !c\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "4->0\n", - "\n", - "\n", - "!a & c\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a & c\n", + "\n", + "\n", + "a & c\n", "\n", "\n", "\n", "5->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "5->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", @@ -1131,199 +1125,193 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "6\n", - "\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "I->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "a & b & c\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "6->0\n", - "\n", - "\n", - "!a & !b & c\n", + "\n", + "\n", + "!a & !b & c\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "!a & b & c\n", + "\n", + "\n", + "!a & b & c\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "\n", "4\n", - "\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "6->4\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n", "5\n", - "\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!b & c\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b & c\n", + "\n", + "\n", + "b & c\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "b & !c\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "4->0\n", - "\n", - "\n", - "!a & c\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a & c\n", + "\n", + "\n", + "a & c\n", "\n", "\n", "\n", "5->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "5->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", @@ -1719,65 +1707,64 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\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", - "\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", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", @@ -1934,65 +1921,64 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\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", - "\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", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", @@ -2067,126 +2053,128 @@ "\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", - "a\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", + "!a\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", diff --git a/tests/python/automata-io.ipynb b/tests/python/automata-io.ipynb index 092fbbff2..6de56f9f5 100644 --- a/tests/python/automata-io.ipynb +++ b/tests/python/automata-io.ipynb @@ -121,60 +121,60 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f5770723f00> >" + " *' at 0x7fc24c50bf00> >" ] }, "execution_count": 3, @@ -250,60 +250,60 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f57706f5690> >" + " *' at 0x7fc24c50b780> >" ] }, "metadata": {}, @@ -315,60 +315,60 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\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", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f57706daa80> >" + " *' at 0x7fc24c50bb70> >" ] }, "metadata": {}, @@ -437,60 +437,60 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f57706f5840> >" + " *' at 0x7fc24c50be10> >" ] }, "metadata": {}, @@ -527,61 +527,61 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Hello world\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f57707760f0> >" + " *' at 0x7fc24c50b750> >" ] }, "metadata": {}, @@ -593,55 +593,55 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Hello world 2\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", "0->0\n", - "\n", - "\n", - "1\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "1\n", + "⓿\n", + "❶\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", - "⓿\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f5770685930> >" + " *' at 0x7fc24c50bde0> >" ] }, "metadata": {}, @@ -698,60 +698,60 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\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", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f57706f5720> >" + " *' at 0x7fc24c50b690> >" ] }, "metadata": {}, @@ -763,53 +763,53 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\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", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f57706f5900> >" + " *' at 0x7fc24c50bd20> >" ] }, "metadata": {}, @@ -821,51 +821,51 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", + "\n", "GFa\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", "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f5770798e70> >" + " *' at 0x7fc24c50b690> >" ] }, "metadata": {}, @@ -877,64 +877,64 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", + "\n", "a & GFb\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", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\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", + "b\n", "⓿\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f57706f5720> >" + " *' at 0x7fc24c50bae0> >" ] }, "metadata": {}, @@ -964,60 +964,60 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\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", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f577072d060> >" + " *' at 0x7fc24c50b6c0> >" ] }, "execution_count": 10, @@ -1041,7 +1041,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, @@ -1055,7 +1055,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5" + "version": "3.11.6" } }, "nbformat": 4, diff --git a/tests/python/dualize.py b/tests/python/dualize.py index b870e1e5e..b4e459a18 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, 2021-2022 Laboratoire de Recherche et +# Copyright (C) 2017-2019, 2021-2023 Laboratoire de Recherche et # Développement de l'EPITA. # # This file is part of Spot, a model checking library. @@ -114,7 +114,7 @@ properties: deterministic stutter-invariant very-weak --BODY-- State: 0 {0} [t] 0 -State: 1 +State: 1 {0} [0] 0 [!0] 2 State: 2 diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 6d9ac1ed8..a35f88334 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -54,11 +54,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -170,11 +170,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -247,7 +247,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc20027d80> >" + " *' at 0x7fb7ec3bb720> >" ] }, "execution_count": 4, @@ -282,11 +282,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -359,7 +359,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc2002e2a0> >" + " *' at 0x7fb7ec3bbb40> >" ] }, "execution_count": 5, @@ -392,11 +392,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -469,7 +469,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc20027d80> >" + " *' at 0x7fb7ec3bb720> >" ] }, "execution_count": 6, @@ -702,7 +702,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc2002e360> >" + " *' at 0x7fb7ec3bba50> >" ] }, "execution_count": 8, @@ -897,7 +897,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc2002e360> >" + " *' at 0x7fb7ec3bba50> >" ] }, "execution_count": 11, @@ -1235,7 +1235,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc2002edb0> >" + " *' at 0x7fb7ec3dc8d0> >" ] }, "metadata": {}, @@ -1496,7 +1496,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc20027de0> >" + " *' at 0x7fb7ef60adc0> >" ] }, "metadata": {}, @@ -1679,7 +1679,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc2002e570> >" + " *' at 0x7fb7ef60a7f0> >" ] }, "metadata": {}, @@ -1746,11 +1746,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1796,7 +1796,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc2002e480> >" + " *' at 0x7fb7ec3bbdb0> >" ] }, "metadata": {}, @@ -1851,7 +1851,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc2002e6c0> >" + " *' at 0x7fb7ef60b810> >" ] }, "metadata": {}, @@ -1945,7 +1945,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc2002ec60> >" + " *' at 0x7fb7ec3bbc60> >" ] }, "execution_count": 14, @@ -2074,7 +2074,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc2002ec60> >" + " *' at 0x7fb7ec3bbc60> >" ] }, "metadata": {}, @@ -2089,11 +2089,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2139,7 +2139,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc2002e480> >" + " *' at 0x7fb7ec3bbdb0> >" ] }, "metadata": {}, @@ -2194,7 +2194,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc2002e6c0> >" + " *' at 0x7fb7ef60b810> >" ] }, "metadata": {}, @@ -2232,7 +2232,7 @@ " | a & b\t{0}\n", "Cycle:\n", " 1 * 4\n", - " | a\t{0,1}\n", + " | a\t{0}\n", "\n" ] }, @@ -2245,143 +2245,141 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")&Inf(\n", - "❶\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0 * 3\n", + "\n", + "0 * 3\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1 * 2\n", + "\n", + "1 * 2\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "2\n", - "\n", - "2 * 2\n", + "\n", + "2 * 2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "3\n", - "\n", - "1 * 1\n", + "\n", + "1 * 1\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "4\n", - "\n", - "2 * 1\n", + "\n", + "2 * 1\n", "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "5\n", - "\n", - "1 * 0\n", + "\n", + "1 * 0\n", "\n", "\n", "\n", "3->5\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "4->5\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "6\n", - "\n", - "2 * 0\n", + "\n", + "2 * 0\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "7\n", - "\n", - "1 * 4\n", + "\n", + "1 * 4\n", "\n", "\n", "\n", "5->7\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", @@ -2392,40 +2390,37 @@ "\n", "\n", "6->8\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "7->7\n", - "\n", - "\n", - "a\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "8->7\n", - "\n", - "\n", - "a\n", - "❶\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "8->8\n", "\n", "\n", - "1\n", - "❶\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7efc20044780> >" + " *' at 0x7fb7ef60a7f0> >" ] }, "metadata": {}, @@ -2440,11 +2435,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2510,7 +2505,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc200449c0> >" + " *' at 0x7fb7ef60af10> >" ] }, "metadata": {}, @@ -2525,89 +2520,89 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "I->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "4\n", - "\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7efc200448d0> >" + " *' at 0x7fb7ef60b840> >" ] }, "metadata": {}, @@ -2776,7 +2771,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc20044f30> >" + " *' at 0x7fb7ec3dd860> >" ] }, "execution_count": 19, @@ -2944,7 +2939,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc20044f30> >" + " *' at 0x7fb7ec3dd860> >" ] }, "execution_count": 20, @@ -3107,7 +3102,7 @@ "\n" ], "text/plain": [ - " *' at 0x7efc20044f30> >" + " *' at 0x7fb7ec3dd860> >" ] }, "metadata": {}, @@ -3601,7 +3596,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, @@ -3615,7 +3610,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.9.1+" + "version": "3.11.6" } }, "nbformat": 4, diff --git a/tests/python/intrun.py b/tests/python/intrun.py index 02a7aedd6..1494d4665 100644 --- a/tests/python/intrun.py +++ b/tests/python/intrun.py @@ -52,27 +52,27 @@ tc.assertEqual(str(r), """Prefix: 1 | a 0 - | 1 {0} + | 1 0 - | a {0} + | a Cycle: 0 - | 1 {0} + | 1 """) tc.assertEqual(r.as_twa().to_str(), """HOA: v1 States: 4 Start: 0 AP: 1 "a" -acc-name: Buchi -Acceptance: 1 Inf(0) +acc-name: all +Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 [0] 1 -State: 1 {0} +State: 1 [t] 2 -State: 2 {0} +State: 2 [0] 3 -State: 3 {0} +State: 3 [t] 3 --END--""") diff --git a/tests/python/setacc.py b/tests/python/setacc.py index 7246bf5cc..c61b3262a 100644 --- a/tests/python/setacc.py +++ b/tests/python/setacc.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016, 2018, 2021, 2022 Laboratoire de Recherche et +# Copyright (C) 2016, 2018, 2021, 2022, 2023 Laboratoire de Recherche et # Développement de l'EPITA. # # This file is part of Spot, a model checking library. @@ -104,10 +104,10 @@ except RuntimeError as e: from gc import collect acc = spot.translate('a').acc() collect() -tc.assertEqual(acc, spot.acc_cond('Inf(0)')) +tc.assertEqual(acc, spot.acc_cond('t')) acc = spot.translate('b').get_acceptance() collect() -tc.assertEqual(acc, spot.acc_code('Inf(0)')) +tc.assertEqual(acc, spot.acc_code('t')) c = spot.acc_cond('Fin(0)&Fin(1)&(Inf(2)|Fin(3))') diff --git a/tests/python/simstate.py b/tests/python/simstate.py index 4874fd478..6a52124f9 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -538,7 +538,8 @@ tc.assertEqual(spot.reduce_iterated_sba(aut).to_str(), '''HOA: v1 States: 1 Start: 0 AP: 1 "a" -Acceptance: 1 t +acc-name: all +Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic properties: very-weak --BODY-- diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb index 4b02a9c0f..627a6a826 100644 --- a/tests/python/stutter-inv.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -12,7 +12,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -24,7 +23,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -70,7 +68,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -98,7 +95,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -106,7 +102,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -137,7 +132,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -145,7 +139,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -171,7 +164,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -196,7 +188,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -221,7 +212,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -249,7 +239,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -313,7 +302,7 @@ "\n" ], "text/plain": [ - " *' at 0x7faad816be40> >" + " *' at 0x7ff008667960> >" ] }, "metadata": {}, @@ -342,7 +331,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -350,7 +338,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -407,7 +394,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -415,7 +401,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -425,7 +410,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -619,7 +603,7 @@ "\n" ], "text/plain": [ - " *' at 0x7faad816be70> >" + " *' at 0x7ff0086679f0> >" ] }, "metadata": {}, @@ -632,7 +616,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -662,7 +645,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -830,7 +812,7 @@ "\n" ], "text/plain": [ - " *' at 0x7faad816be70> >" + " *' at 0x7ff0086679f0> >" ] }, "metadata": {}, @@ -843,7 +825,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -851,7 +832,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -859,7 +839,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -899,7 +878,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -986,7 +964,7 @@ "\n" ], "text/plain": [ - " *' at 0x7faad8057690> >" + " *' at 0x7ff008667cc0> >" ] }, "metadata": {}, @@ -1084,7 +1062,7 @@ "\n" ], "text/plain": [ - " *' at 0x7faad8253210> >" + " *' at 0x7ff008667cf0> >" ] }, "metadata": {}, @@ -1104,7 +1082,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1295,7 +1272,7 @@ "\n" ], "text/plain": [ - " *' at 0x7faad8057ea0> >" + " *' at 0x7ff0086677b0> >" ] }, "metadata": {}, @@ -1314,7 +1291,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1425,7 +1401,7 @@ "\n" ], "text/plain": [ - " *' at 0x7faad8247a20> >" + " *' at 0x7ff0086677e0> >" ] }, "metadata": {}, @@ -1439,7 +1415,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1447,7 +1422,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1478,87 +1452,83 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "I->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "3->0\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", - "⓿\n", + "\n", + "1\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", - "⓿\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\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" ], "text/plain": [ - " *' at 0x7faad8057450> >" + " *' at 0x7ff008667ed0> >" ] }, "metadata": {}, @@ -1573,7 +1543,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1605,7 +1574,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1820,7 +1788,7 @@ "\n" ], "text/plain": [ - " *' at 0x7faad816b390> >" + " *' at 0x7ff0086676c0> >" ] }, "metadata": {}, @@ -1845,7 +1813,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1874,7 +1841,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -2136,7 +2102,7 @@ "\n" ], "text/plain": [ - " *' at 0x7faad816b390> >" + " *' at 0x7ff0086676c0> >" ] }, "metadata": {}, @@ -2158,7 +2124,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -2186,7 +2151,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -2309,7 +2273,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -2337,7 +2300,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -2367,7 +2329,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, @@ -2381,7 +2343,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.6rc1" + "version": "3.11.6" } }, "nbformat": 4, diff --git a/tests/python/zlktree.py b/tests/python/zlktree.py index c3cb262f2..c86c4a8b0 100644 --- a/tests/python/zlktree.py +++ b/tests/python/zlktree.py @@ -27,6 +27,7 @@ trans-acc --BODY-- State: 0 [!0&!1] 3 [!0&!1] 4 State: 1 [!0&!1] 4 {3} [0&!1] 0 {2} [!0&1] 1 {2} State: 2 [!0&1] 0 {0 2} [!0&!1] 1 State: 3 [!0&1] 2 State: 4 [0&!1] 3 --END--""") b = spot.zielonka_tree_transform(a) +spot.is_weak_automaton(b) tc.assertTrue(spot.are_equivalent(a, b)) tc.assertTrue(b.acc().is_buchi())