From 67b5d2aa9a4cde950e7d78ef8126b9e59dd094c8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 9 Nov 2023 22:13:05 +0100 Subject: [PATCH] fix several algorithms that incorrectly preserved !weak This massive set of changes was triggered by issue #546. In addition to the better handling of !weak, this also adds some weak properties in a few places. * spot/twaalgos/product.cc (product_aux): Throw some exception if an automaton with t or f acceptance has the !weak property. This is a cheap sanity check to help detect algorithms that incorrectly assumed !weak input would necessarily become !weak output. * spot/twaalgos/hoa.cc (print_hoa): Likewise, also do not assume that terminal implies very-weak. * spot/parseaut/parseaut.yy: Add several diagnostics for similar cases. E.g., a one-state automaton cannot be declared as !very-weak. * tests/core/parseaut.test: Check those new diagnostics. * spot/twa/twa.cc (twa::intersecting_run): Temporary remove the weak property by setting it to maybe, not to false. * spot/twaalgos/minimize.cc, spot/twaalgos/parity.cc, spot/twaalgos/sccfilter.cc, spot/twaalgos/simulation.cc: Account for the fact that these algorithm may in fact improve the weakness. * spot/twaalgos/strength.cc: Only look at colors used by the acceptance condition when deciding weakness. * spot/twaalgos/synthesis.cc: Declare the strategy as weak. * bin/randaut.cc: Add weak to automata with t/f acceptance. * spot/kripke/kripke.hh: Make kripke structures as weak. * tests/core/acc_word.test, tests/core/alternating.test, tests/core/complement.test, tests/core/complete.test, tests/core/ltlsynt.test, tests/core/randomize.test, tests/core/readsave.test, tests/core/remfin.test, tests/core/sccsimpl.test, tests/core/strength.test, tests/core/wdba2.test, tests/ltsmin/kripke.test, tests/python/automata-io.ipynb, tests/python/automata.ipynb, tests/python/dbranch.py, tests/python/highlighting.ipynb, tests/python/kripke.py, tests/python/ltsmin-dve.ipynb, tests/python/mealy.py, tests/python/simstate.py: Adjust all these test cases. * NEWS: Mention the fixes. --- NEWS | 12 ++ bin/randaut.cc | 2 + spot/kripke/kripke.hh | 5 +- spot/parseaut/parseaut.yy | 24 ++++ spot/twa/twa.cc | 4 +- spot/twaalgos/hoa.cc | 9 +- spot/twaalgos/minimize.cc | 10 ++ spot/twaalgos/parity.cc | 9 +- spot/twaalgos/product.cc | 16 +++ spot/twaalgos/sccfilter.cc | 21 +++- spot/twaalgos/simulation.cc | 10 +- spot/twaalgos/strength.cc | 10 +- spot/twaalgos/synthesis.cc | 4 + tests/core/acc_word.test | 4 +- tests/core/alternating.test | 2 +- tests/core/complement.test | 10 +- tests/core/complete.test | 6 +- tests/core/ltlsynt.test | 2 +- tests/core/parseaut.test | 23 +++- tests/core/randomize.test | 6 +- tests/core/readsave.test | 10 +- tests/core/remfin.test | 6 +- tests/core/sccsimpl.test | 6 +- tests/core/strength.test | 6 +- tests/core/wdba2.test | 3 +- tests/ltsmin/kripke.test | 6 +- tests/python/automata-io.ipynb | 4 +- tests/python/automata.ipynb | 187 ++++++++++++++++---------------- tests/python/dbranch.py | 2 +- tests/python/highlighting.ipynb | 4 +- tests/python/kripke.py | 10 +- tests/python/ltsmin-dve.ipynb | 2 +- tests/python/mealy.py | 8 +- tests/python/simstate.py | 8 +- 34 files changed, 287 insertions(+), 164 deletions(-) diff --git a/NEWS b/NEWS index df7bf8dd3..928adf584 100644 --- a/NEWS +++ b/NEWS @@ -116,6 +116,18 @@ New in spot 2.11.6.dev (not yet released) presence of unsatisifable or universal acceptance conditions that were not f or t. (Part of issue #546.) + - Several algorithms were incorrectly dealing with the "!weak" + property. Because they (rightly) assumed that a weak input would + produce a weak output, they also wrongly assumed that a non-weak + output would produce a non-weak output. Unfortunately removing + states or edges in a non-weak automaton can lead a weak automaton. + The incorrect property lead to issue #546. In addition to fixing + several algorithms, product() and print_hoa() will now raise an + exception if automaton with t or f acceptance is declared !weak. + (This cheap check will not catch all automata incorrectly labeled + by !weak, but helps detects some issues nonetheless.) + + New in spot 2.11.6 (2023-08-01) Bug fixes: diff --git a/bin/randaut.cc b/bin/randaut.cc index 4e2065c2a..ec1a06a88 100644 --- a/bin/randaut.cc +++ b/bin/randaut.cc @@ -385,6 +385,8 @@ main(int argc, char** argv) if (opt_acceptance) aut->set_acceptance(accs, code); + if (aut->acc().is_t() || aut->acc().is_f()) + aut->prop_weak(true); if (opt_uniq) { diff --git a/spot/kripke/kripke.hh b/spot/kripke/kripke.hh index 8b039f37c..ed540ac41 100644 --- a/spot/kripke/kripke.hh +++ b/spot/kripke/kripke.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2013, 2014, 2016, 2017, 2019, 2020 Laboratoire -// de Recherche et Developpement de l'Epita +// Copyright (C) 2009, 2010, 2013, 2014, 2016, 2017, 2019, 2020, 2023 +// Laboratoire de Recherche et Developpement de l'Epita // // This file is part of Spot, a model checking library. // @@ -180,6 +180,7 @@ namespace spot kripke(const bdd_dict_ptr& d) : fair_kripke(d) { + prop_weak(true); } virtual ~kripke(); diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 5b8792e96..c52beb1e3 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -691,6 +691,19 @@ header: format-version header-items } if (t != e) a->prop_terminal(t->second.val); + if (a->acc().is_t() || a->acc().is_f()) + { + if (w != e && !w->second.val) + error(w->second.loc, "an automaton with this condition" + " is necessarily weak"); + if (iw != e && !iw->second.val) + error(iw->second.loc, "an automaton with this condition" + " is necessarily inherently-weak"); + if (vw != e && !vw->second.val + && (res.states == 0 || res.states == 1)) + error(vw->second.loc, "an automaton with 0 or 1 state " + "is necessarily very-weak"); + } auto u = p.find("unambiguous"); if (u != e) { @@ -2743,6 +2756,17 @@ static void fix_properties(result_& r) if (r.acc_style == State_Acc || (r.acc_style == Mixed_Acc && !r.trans_acc_seen)) r.aut_or_ks->prop_state_acc(true); + if (r.aut_or_ks->acc().is_t() || r.aut_or_ks->acc().is_f()) + { + r.aut_or_ks->prop_weak(true); + unsigned ns; + if (r.opts.want_kripke) + ns = r.h->ks->num_states(); + else + ns = r.h->aut->num_states(); + if (ns == 0 || ns == 1) + r.aut_or_ks->prop_very_weak(true); + } } static void check_version(const result_& r) diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index c1c113e87..6ada4b6f4 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -171,8 +171,8 @@ namespace spot // for weak automata, otherwise project(g1) would be unable to // compute the correct marks. See issue #471. It's OK to // optimize the right part if g2 is weak. - spot::trival g1weak = g1->prop_weak(); - std::const_pointer_cast(g1)->prop_weak(false); + trival g1weak = g1->prop_weak(); + std::const_pointer_cast(g1)->prop_weak(trival::maybe()); auto run = generic_accepting_run(product(g1, g2)); std::const_pointer_cast(g1)->prop_weak(g1weak); if (!run) diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index e6147afda..c8e7b13b9 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2022 Laboratoire de Recherche et +// Copyright (C) 2014-2023 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -507,6 +507,11 @@ namespace spot } } + if (SPOT_UNLIKELY(aut->prop_weak().is_false() + && (aut->acc().is_t() || aut->acc().is_f()))) + throw std::runtime_error("print_hoa(): automaton is declared not weak, " + "but the acceptance makes this impossible"); + metadata md(aut, implicit_labels, state_labels); if (acceptance == Hoa_Acceptance_States && !md.has_state_acc) @@ -724,7 +729,7 @@ namespace spot } if (aut->prop_terminal()) prop(" terminal"); - if (aut->prop_very_weak() && (verbose || aut->prop_terminal() != true)) + if (aut->prop_very_weak()) prop(" very-weak"); if (aut->prop_weak() && (verbose || (aut->prop_terminal() != true && aut->prop_very_weak() != true))) diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index 1ac961d46..889028e57 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -556,6 +556,16 @@ namespace spot // add a quick check inside minimize_dfa. if (a->prop_terminal()) res->prop_terminal(true); + else if (a->num_states() == 1) + { + // If thie automaton has only one state, check w + for (auto& e: a->out(0)) + if (e.cond == bddtrue && a->acc().accepting(e.acc)) + { + res->prop_terminal(true); + break; + } + } return res; } diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc index c8507ac53..98ac010fe 100644 --- a/spot/twaalgos/parity.cc +++ b/spot/twaalgos/parity.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016, 2018, 2019, 2022 Laboratoire de Recherche et +// Copyright (C) 2016, 2018, 2019, 2022, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -649,6 +649,13 @@ namespace spot e.acc = acc_cond::mark_t({n}); } + // Reducing the number of colors could turn a non-weak automaton + // into a weak one + if (aut->prop_weak().is_false()) + aut->prop_weak(trival::maybe()); + if (aut->prop_very_weak().is_false()) + aut->prop_very_weak(trival::maybe()); + return aut; } } diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index b337a5a43..dc12b34f8 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -27,6 +27,8 @@ #include #include +using namespace std::string_literals; + namespace spot { namespace @@ -102,6 +104,13 @@ namespace spot enum acc_op { and_acc, or_acc, xor_acc, xnor_acc }; + [[noreturn]] static + void report_should_be_weak(const char* what) + { + std::string s = what + " automaton is declared not weak, " + "but the acceptance makes this impossible"s; + throw std::runtime_error(s); + } static twa_graph_ptr product_aux(const const_twa_graph_ptr& left, @@ -128,6 +137,13 @@ namespace spot bool leftweak = left->prop_weak().is_true(); bool rightweak = right->prop_weak().is_true(); + if (SPOT_UNLIKELY(!leftweak && left->prop_weak().is_false() + && (lacc.is_t() || lacc.is_f()))) + report_should_be_weak("product: left"); + if (SPOT_UNLIKELY(!rightweak && right->prop_weak().is_false() + && (racc.is_t() || racc.is_f()))) + report_should_be_weak("product: right"); + // The conjunction of two co-Büchi automata is a co-Büchi automaton. // The disjunction of two Büchi automata is a Büchi automaton. // diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index 65e022453..20dea3f7e 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2009-2018, 2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -428,6 +428,15 @@ namespace spot res = scc_filter_apply>>(aut, given_si); res->prop_copy(aut, { true, true, false, true, false, true }); + if (res->num_edges() != aut->num_edges()) + { + if (res->prop_weak().is_false()) + res->prop_weak(trival::maybe()); + if (res->prop_very_weak().is_false()) + res->prop_very_weak(trival::maybe()); + } + if (res->prop_weak().is_true() && res->num_states() <= 1) + res->prop_very_weak(true); return res; } @@ -496,6 +505,16 @@ namespace spot if (!given_si) delete si; } + else + if (res->num_edges() != aut->num_edges()) + { + if (res->prop_weak().is_false()) + res->prop_weak(trival::maybe()); + if (res->prop_very_weak().is_false()) + res->prop_very_weak(trival::maybe()); + } + if (res->prop_weak().is_true() && res->num_states() <= 1) + res->prop_very_weak(true); return res; } diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index 404a8eebc..aa3ed2a15 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -761,11 +761,19 @@ namespace spot delete gb; res->prop_copy(original_, { false, // state-based acc forced below - true, // weakness preserved, + true, // weakness preserved false, true, // determinism improved true, // completeness preserved true, // stutter inv. }); + + // weakness can actually be improved + if (res->prop_weak().is_false()) + res->prop_weak(trival::maybe()); + if (res->prop_very_weak().is_false()) + res->prop_very_weak(trival::maybe()); + if (res->prop_inherently_weak().is_false()) + res->prop_inherently_weak(trival::maybe()); // !unambiguous and !semi-deterministic are not preserved if (!Cosimulation && nb_minato == nb_minterms) // Note that nb_minato != nb_minterms does not imply diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 1ef93a7c2..8140b1b0a 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010-2011, 2013-2018 Laboratoire de Recherche et -// Développement de l'Epita (LRDE) +// Copyright (C) 2010-2011, 2013-2018, 2023 Laboratoire de Recherche +// et Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -43,6 +43,8 @@ namespace spot if (inweak) si->determine_unknown_acceptance(); + acc_cond::mark_t mask = aut->get_acceptance().used_sets(); + bool is_inweak = true; bool is_weak = true; bool is_single_state_scc = true; @@ -66,9 +68,9 @@ namespace spot if (first) { first = false; - m = t.acc; + m = t.acc & mask; } - else if (m != t.acc) + else if (m != (t.acc & mask)) { is_weak = false; if (!inweak) diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 0aff98880..11a154da3 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -1469,6 +1469,9 @@ namespace spot edge.acc = {}; } res->set_acceptance(acc_cond::acc_code::t()); + res->prop_weak(true); + if (res->prop_terminal().is_false()) + res->prop_terminal(trival::maybe()); res->set_named_prop("synthesis-outputs", new bdd(output_bdd)); return ret_sol_exists(res); @@ -1478,6 +1481,7 @@ namespace spot if (!want_strategy) return ret_sol_exists(nullptr); auto res = make_twa_graph(dict); + res->prop_weak(true); bdd output_bdd = bddtrue; std::set ins_f = form2props.aps_of(f_g).first; diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test index 5f3b6880b..4fc5a5602 100644 --- a/tests/core/acc_word.test +++ b/tests/core/acc_word.test @@ -79,7 +79,7 @@ AP: 2 "b" "a" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc !complete -properties: deterministic stutter-invariant terminal +properties: deterministic stutter-invariant terminal very-weak spot.highlight.edges: 1 1 2 1 --BODY-- State: 0 {0} @@ -113,7 +113,7 @@ AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic stutter-invariant terminal +properties: deterministic stutter-invariant terminal very-weak spot.highlight.edges: 1 3 2 3 5 3 6 3 7 2 8 2 --BODY-- State: 0 {0} diff --git a/tests/core/alternating.test b/tests/core/alternating.test index df4e47624..6706eddc8 100755 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -472,7 +472,7 @@ Start: 0 AP: 1 "a" acc-name: all Acceptance: 0 t -properties: trans-labels explicit-labels state-acc deterministic +properties: trans-labels explicit-labels state-acc deterministic weak --BODY-- State: 0 [!0] 1 diff --git a/tests/core/complement.test b/tests/core/complement.test index eb3902d28..ebaafa1c2 100755 --- a/tests/core/complement.test +++ b/tests/core/complement.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015-2019, 2021 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2015-2019, 2021, 2023 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -41,7 +41,7 @@ AP: 0 acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc complete -properties: deterministic +properties: deterministic very-weak --BODY-- State: 0 [t] 0 @@ -74,7 +74,7 @@ AP: 1 "a" acc-name: co-Buchi Acceptance: 1 Fin(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic weak +properties: deterministic very-weak --BODY-- State: 0 [0] 2 @@ -93,7 +93,7 @@ AP: 1 "a" acc-name: co-Buchi Acceptance: 1 Fin(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic stutter-invariant weak +properties: deterministic stutter-invariant very-weak --BODY-- State: 0 {0} [t] 0 diff --git a/tests/core/complete.test b/tests/core/complete.test index 7f557f67c..1d1be12bc 100755 --- a/tests/core/complete.test +++ b/tests/core/complete.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015-2017, 2022 Laboratoire de Recherche et Développement +# Copyright (C) 2015-2017, 2022, 2023 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -151,7 +151,7 @@ AP: 1 "a" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic +properties: deterministic weak --BODY-- State: 0 {0} [0] 1 @@ -169,7 +169,7 @@ AP: 1 "a" acc-name: none Acceptance: 0 f properties: trans-labels explicit-labels state-acc complete -properties: deterministic +properties: deterministic weak --BODY-- State: 0 [t] 1 diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index d6f5815f5..f11e1dbd1 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -611,7 +611,7 @@ Start: 0 AP: 3 "c" "a" "b" acc-name: all Acceptance: 0 t -properties: trans-labels explicit-labels state-acc deterministic +properties: trans-labels explicit-labels state-acc deterministic weak controllable-AP: 0 --BODY-- State: 0 diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index 7dabd563d..52748b07c 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014-2018, 2020-2022 Laboratoire de Recherche et +# Copyright (C) 2014-2018, 2020-2023 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -664,7 +664,7 @@ Start: 0 AP: 1 "a" acc-name: all Acceptance: 0 t -properties: trans-labels explicit-labels state-acc deterministic +properties: trans-labels explicit-labels state-acc deterministic weak --BODY-- State: 0 [0] 1 @@ -1322,7 +1322,7 @@ AP: 2 "a" "b" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc complete -properties: deterministic +properties: deterministic weak --BODY-- State: 0 [0&!1] 0 @@ -1778,7 +1778,7 @@ Start: 0 AP: 1 "a" Acceptance: 1 t properties: trans-labels explicit-labels trans-acc complete -properties: deterministic +properties: deterministic weak --BODY-- State: 0 "F(a)" [0] 1 {0} @@ -1844,7 +1844,7 @@ AP: 1 "a" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc complete -properties: deterministic +properties: deterministic weak --BODY-- State: 0 "F(a)" [0] 1 @@ -2079,6 +2079,15 @@ properties: complete !weak very-weak --BODY-- State: 0 0 --END-- +HOA: v1 +States: 1 +Start: 0 +AP: 0 +Acceptance: 0 t +properties: complete !very-weak +--BODY-- +State: 0 0 +--END-- EOF expecterr input <\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -178,7 +178,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a002151e0> >" + " *' at 0x7f773078f870> >" ] }, "execution_count": 2, @@ -211,10 +211,10 @@ "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "[Büchi]\n", "\n", "\n", @@ -607,11 +607,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -657,7 +657,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000cc3c0> >" + " *' at 0x7f77307ac6c0> >" ] }, "execution_count": 6, @@ -683,11 +683,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -733,7 +733,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000cc690> >" + " *' at 0x7f77307ac840> >" ] }, "execution_count": 7, @@ -816,7 +816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000cc2a0> >" + " *' at 0x7f77307ac930> >" ] }, "execution_count": 8, @@ -872,11 +872,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -983,11 +983,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1349,7 +1349,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000d42a0> >" + " *' at 0x7f77307ad320> >" ] }, "execution_count": 12, @@ -1463,7 +1463,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000d4630> >" + " *' at 0x7f77307ad500> >" ] }, "execution_count": 13, @@ -1496,11 +1496,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1594,7 +1594,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000d4c00> >" + " *' at 0x7f77307add70> >" ] }, "execution_count": 14, @@ -1816,7 +1816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000d8510> >" + " *' at 0x7f77307ae280> >" ] }, "metadata": {}, @@ -1974,7 +1974,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000d8420> >" + " *' at 0x7f77307ae250> >" ] }, "metadata": {}, @@ -2132,7 +2132,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000d8300> >" + " *' at 0x7f77307adda0> >" ] }, "metadata": {}, @@ -2147,11 +2147,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2280,7 +2280,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000d8270> >" + " *' at 0x7f77307adbc0> >" ] }, "metadata": {}, @@ -2469,7 +2469,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a00215fc0> >" + " *' at 0x7f77307adad0> >" ] }, "execution_count": 19, @@ -2495,11 +2495,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2545,7 +2545,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000e1420> >" + " *' at 0x7f77307ad440> >" ] }, "execution_count": 20, @@ -2582,13 +2582,6 @@ "execution_count": 22, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "no\n" - ] - }, { "data": { "text/html": [ @@ -3016,7 +3009,6 @@ "# Using +1 in the display options is a convenient way to shift the \n", "# set numbers in the output, as an aid in reading the product.\n", "a1 = spot.translate('GF(a <-> Xa)')\n", - "print(a1.prop_weak())\n", "a2 = spot.translate('a U b & GFc')\n", "display_inline(a1.show('.t'), a2.show('.t+1'))\n", "# the product should display pairs of states, unless asked not to (using '1').\n", @@ -3045,11 +3037,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -3095,7 +3087,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000ccd50> >" + " *' at 0x7f77307af1e0> >" ] }, "metadata": {}, @@ -3195,7 +3187,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000ccde0> >" + " *' at 0x7f77307afa20> >" ] }, "execution_count": 24, @@ -3268,7 +3260,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000cce70> >" + " *' at 0x7f77307ac750> >" ] }, "execution_count": 25, @@ -3439,7 +3431,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a00215ab0> >" + " *' at 0x7f77307aef40> >" ] }, "execution_count": 27, @@ -3472,11 +3464,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -3522,7 +3514,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000ccd50> >" + " *' at 0x7f77307af1e0> >" ] }, "metadata": {}, @@ -3537,11 +3529,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -3587,7 +3579,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000ccd50> >" + " *' at 0x7f77307af1e0> >" ] }, "metadata": {}, @@ -3624,11 +3616,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -3674,7 +3666,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a000ccd50> >" + " *' at 0x7f77307af1e0> >" ] }, "execution_count": 29, @@ -3689,11 +3681,18 @@ " e.cond &= c\n", "a" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, @@ -3707,7 +3706,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.9.2" + "version": "3.11.6" } }, "nbformat": 4, diff --git a/tests/python/dbranch.py b/tests/python/dbranch.py index 268c4a3c6..99c81bdf6 100644 --- a/tests/python/dbranch.py +++ b/tests/python/dbranch.py @@ -65,7 +65,7 @@ Start: 0 AP: 3 "b" "a" "c" acc-name: all Acceptance: 0 t -properties: trans-labels explicit-labels state-acc univ-branch +properties: trans-labels explicit-labels state-acc univ-branch weak --BODY-- State: 0 [1] 1 diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 15f9047a8..6d9ac1ed8 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -506,7 +506,7 @@ "acc-name: Buchi\n", "Acceptance: 1 Inf(0)\n", "properties: trans-labels explicit-labels state-acc deterministic\n", - "properties: stutter-invariant terminal\n", + "properties: stutter-invariant terminal very-weak\n", "--BODY--\n", "State: 0 {0}\n", "[t] 0\n", @@ -526,7 +526,7 @@ "acc-name: Buchi\n", "Acceptance: 1 Inf(0)\n", "properties: trans-labels explicit-labels state-acc !complete\n", - "properties: deterministic stutter-invariant terminal\n", + "properties: deterministic stutter-invariant terminal very-weak\n", "spot.highlight.states: 0 0 1 5 2 5\n", "spot.highlight.edges: 2 1 4 1 5 1 6 2\n", "--BODY--\n", diff --git a/tests/python/kripke.py b/tests/python/kripke.py index 3670f592d..2d65ebc5d 100644 --- a/tests/python/kripke.py +++ b/tests/python/kripke.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2019, 2022 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2019, 2022, 2023 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -45,7 +45,7 @@ Start: 1 AP: 2 "p1" "p2" acc-name: all Acceptance: 0 t -properties: state-labels explicit-labels state-acc +properties: state-labels explicit-labels state-acc weak --BODY-- State: [0&1] 0 0 @@ -65,7 +65,7 @@ Start: 1 AP: 2 "p1" "p2" acc-name: all Acceptance: 0 t -properties: state-labels explicit-labels state-acc +properties: state-labels explicit-labels state-acc weak --BODY-- State: [0&1] 0 "s0" 0 @@ -83,7 +83,7 @@ Start: 1 AP: 2 "p1" "p2" acc-name: all Acceptance: 0 t -properties: state-labels explicit-labels state-acc +properties: state-labels explicit-labels state-acc weak --BODY-- State: [0&1] 0 "s0" 0 diff --git a/tests/python/ltsmin-dve.ipynb b/tests/python/ltsmin-dve.ipynb index 05530ca8e..7b474ce30 100644 --- a/tests/python/ltsmin-dve.ipynb +++ b/tests/python/ltsmin-dve.ipynb @@ -1773,7 +1773,7 @@ "AP: 3 \"a<1\" \"b>2\" \"dead\"\n", "acc-name: all\n", "Acceptance: 0 t\n", - "properties: state-labels explicit-labels state-acc\n", + "properties: state-labels explicit-labels state-acc weak\n", "--BODY--\n", "State: [0&!1&!2] 0 \"a=0, b=0, Q=0\"\n", "1 2\n", diff --git a/tests/python/mealy.py b/tests/python/mealy.py index 7f6070146..ef61daca9 100644 --- a/tests/python/mealy.py +++ b/tests/python/mealy.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2021-2023 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -557,7 +557,7 @@ Start: 0 AP: 2 "a" "b" acc-name: all Acceptance: 0 t -properties: trans-labels explicit-labels state-acc deterministic +properties: trans-labels explicit-labels state-acc deterministic weak controllable-AP: 1 --BODY-- State: 0 @@ -598,7 +598,7 @@ Start: 0 AP: 2 "a" "b" acc-name: all Acceptance: 0 t -properties: trans-labels explicit-labels state-acc deterministic +properties: trans-labels explicit-labels state-acc deterministic weak controllable-AP: 1 --BODY-- State: 0 @@ -677,4 +677,4 @@ spot.minimize_mealy(aut, 1) auts = spot.split_2step(aut) spot.minimize_mealy(auts, -1) spot.minimize_mealy(auts, 0) -spot.minimize_mealy(auts, 1) \ No newline at end of file +spot.minimize_mealy(auts, 1) diff --git a/tests/python/simstate.py b/tests/python/simstate.py index b0b62267d..4874fd478 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2017-2018, 2020-2022 Laboratoire de Recherche +# Copyright (C) 2015, 2017-2018, 2020-2023 Laboratoire de Recherche # et Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -539,10 +539,10 @@ States: 1 Start: 0 AP: 1 "a" Acceptance: 1 t -properties: trans-labels explicit-labels state-acc colored -properties: deterministic +properties: trans-labels explicit-labels state-acc deterministic +properties: very-weak --BODY-- -State: 0 {0} +State: 0 [0] 0 --END--''')