diff --git a/NEWS b/NEWS index 1e9291ae2..413587683 100644 --- a/NEWS +++ b/NEWS @@ -122,6 +122,12 @@ New in spot 2.5.3.dev (not yet released) to update an external structure that references states of the twa that we want to purge. + - spot::scc_filter() now automatically turns automata marked as + inherently-weak into weak automata with state-based acceptance. + The acceptance condition is set to Büchi unless the input had + co-Büchi or t acceptance. spot::scc_filter_states() will pass + inherently-weak automata to spot::scc_filter(). + - spot::cleanup_parity() and spot::cleanup_parity_here() are smarter and now remove from the acceptance condition the parity colors that are not used in the automaton. diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 4ad5a8b8b..9ed38dbee 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -38,7 +38,6 @@ #include #include #include -#include #include namespace spot @@ -166,10 +165,7 @@ namespace spot { if (scc_filter_ == 0) return a; - // If the automaton is weak, using transition-based acceptance - // won't help, so let's preserve state-based acceptance. - if ((state_based_ || a->prop_inherently_weak().is_true()) - && a->prop_state_acc().is_true()) + if (state_based_ && a->prop_state_acc().is_true()) return scc_filter_states(a, arg); else return scc_filter(a, arg); diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index 0d3823ce9..1b5d452d6 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -124,6 +124,53 @@ namespace spot } }; + // Transform inherently weak automata into weak Büchi automata. + template + struct weak_filter: next_filter + { + acc_cond::mark_t acc_m = {0}; + acc_cond::mark_t rej_m = {}; + + template + weak_filter(scc_info* si, Args&&... args) + : next_filter(si, std::forward(args)...) + { + if (!buchi) + { + acc_m = {}; + if (si->get_aut()->acc().is_co_buchi()) + rej_m = {0}; + } + } + + filtered_trans trans(unsigned src, unsigned dst, + bdd cond, acc_cond::mark_t acc) + { + + bool keep; + std::tie(keep, cond, acc) = + this->next_filter::trans(src, dst, cond, acc); + + if (keep) + { + unsigned ss = this->si->scc_of(src); + if (this->si->is_accepting_scc(ss)) + acc = acc_m; + else + acc = rej_m; + } + return filtered_trans(keep, cond, acc); + } + + void fix_acceptance(const twa_graph_ptr& out) + { + if (buchi) + out->set_buchi(); + else + out->copy_acceptance_of(this->si->get_aut()); + } + }; + // Remove acceptance conditions from all edges outside of // non-accepting SCCs. If "RemoveAll" is false, keep those on // transitions entering accepting SCCs. If "PreserveSBA", is set @@ -160,7 +207,7 @@ namespace spot unsigned v = this->si->scc_of(dst); // The basic rules are as follows: // - // - If an edge is between two SCCs, is OK to remove + // - If an edge is between two SCCs, it is OK to remove // all acceptance sets, as this edge cannot be part // of any loop. // - If an edge is in an non-accepting SCC, we can only @@ -370,6 +417,10 @@ namespace spot scc_info* given_si) { twa_graph_ptr res; + // For weak automata, scc_filter() is already doing the right + // thing and preserves state-based acceptance. + if (aut->prop_inherently_weak()) + return scc_filter(aut, remove_all_useless, given_si); if (remove_all_useless) res = scc_filter_apply>>(aut, given_si); @@ -385,9 +436,18 @@ namespace spot scc_info* given_si) { twa_graph_ptr res; - // acc_filter_simplify only works for generalized Büchi - if (aut->acc().is_generalized_buchi()) + if (aut->prop_inherently_weak()) { + if (aut->acc().is_t() || aut->acc().is_co_buchi()) + res = + scc_filter_apply>>(aut, given_si); + else + res = + scc_filter_apply>>(aut, given_si); + } + else if (aut->acc().is_generalized_buchi()) + { + // acc_filter_simplify only works for generalized Büchi if (remove_all_useless) res = scc_filter_applyprop_inherently_weak()) + { + res->prop_weak(true); + res->prop_state_acc(true); + } return res; } diff --git a/spot/twaalgos/sccfilter.hh b/spot/twaalgos/sccfilter.hh index 9361d7b06..6c1451912 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 Laboratoire de +// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015, 2018 Laboratoire de // Recherche et Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -50,13 +50,18 @@ namespace spot /// degeneralization) will work better if transitions going to an /// 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). + /// /// If \a given_sm is supplied, the function will use its result /// without computing a map of its own. /// - /// \warning Calling scc_filter on a TωA that has the SBA property - /// (i.e., transitions leaving accepting states are all marked as - /// accepting) may destroy this property. Use scc_filter_states() - /// instead. + /// \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); diff --git a/tests/core/dca2.test b/tests/core/dca2.test index ce0093c72..eef1d8168 100755 --- a/tests/core/dca2.test +++ b/tests/core/dca2.test @@ -67,7 +67,11 @@ while read l_f; do autfilt -q --acceptance-is=Streett-like and.hoa # Streett | Streett autfilt r.hoa --name="($l_f)|!($r_f)" --product-or=l.hoa -S > or.hoa - autfilt -q -v --acceptance-is=Streett-like or.hoa + if ! grep -q ' weak' l.hoa; then + if ! grep -q ' weak' r.hoa; then + autfilt -q -v --acceptance-is=Streett-like or.hoa || exit 1 + fi + fi autcross --language-preserved --verbose -F or.hoa -F and.hoa \ 'autfilt %H --stats=%M | ltl2tgba >%O' \ diff --git a/tests/core/parity2.test b/tests/core/parity2.test index 09b7d3189..40daa2cbc 100755 --- a/tests/core/parity2.test +++ b/tests/core/parity2.test @@ -236,7 +236,7 @@ AP: 1 "a" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc stutter-invariant -properties: inherently-weak +properties: weak --BODY-- State: 0 [t] 0 @@ -270,7 +270,7 @@ AP: 1 "a" acc-name: Rabin 1 Acceptance: 2 Fin(0) & Inf(1) properties: trans-labels explicit-labels state-acc stutter-invariant -properties: inherently-weak +properties: weak --BODY-- State: 0 [t] 0 @@ -304,7 +304,7 @@ AP: 1 "a" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc stutter-invariant -properties: inherently-weak +properties: weak --BODY-- State: 0 [t] 0 @@ -338,7 +338,7 @@ AP: 1 "a" acc-name: Streett 1 Acceptance: 2 Fin(0) | Inf(1) properties: trans-labels explicit-labels state-acc colored -properties: stutter-invariant inherently-weak +properties: stutter-invariant weak --BODY-- State: 0 {0} [t] 0 @@ -372,7 +372,7 @@ AP: 1 "a" acc-name: parity min odd 3 Acceptance: 3 Fin(0) & (Inf(1) | Fin(2)) properties: trans-labels explicit-labels state-acc colored -properties: stutter-invariant inherently-weak +properties: stutter-invariant weak --BODY-- State: 0 {2} [t] 0 @@ -406,7 +406,7 @@ AP: 1 "a" acc-name: parity max even 3 Acceptance: 3 Inf(2) | (Fin(1) & Inf(0)) properties: trans-labels explicit-labels state-acc colored -properties: stutter-invariant inherently-weak +properties: stutter-invariant weak --BODY-- State: 0 {1} [t] 0 diff --git a/tests/core/prodor.test b/tests/core/prodor.test index c91a48d8d..73bcf6a91 100755 --- a/tests/core/prodor.test +++ b/tests/core/prodor.test @@ -57,23 +57,24 @@ HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" -Acceptance: 2 Inf(0) | Inf(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc complete properties: stutter-invariant --BODY-- State: 0 [!0] 0 -[0] 0 {1} +[0] 0 {0} [!0&1] 1 -[0&1] 1 {1} +[0&1] 1 {0} State: 1 [!0&1] 1 {0} -[0&1] 1 {0 1} +[0&1] 1 {0} [!0&!1] 2 {0} -[0&!1] 2 {0 1} +[0&!1] 2 {0} State: 2 [!0] 2 -[0] 2 {1} +[0] 2 {0} --END-- EOF diff por.hoa exp @@ -88,18 +89,18 @@ HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" -acc-name: generalized-Buchi 2 -Acceptance: 2 Inf(0)&Inf(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc stutter-invariant --BODY-- State: 0 [!0] 0 -[0] 0 {1} +[0] 0 [!0&1] 1 -[0&1] 1 {1} +[0&1] 1 State: 1 -[!0&1] 1 {0} -[0&1] 1 {0 1} +[!0&1] 1 +[0&1] 1 {0} --END-- EOF diff pand.hoa exp diff --git a/tests/core/randomize.test b/tests/core/randomize.test index 216a4b05f..de3059486 100755 --- a/tests/core/randomize.test +++ b/tests/core/randomize.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et +# Copyright (C) 2014, 2015, 2017, 2018 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -33,7 +33,7 @@ AP: 4 "a" "b" "c" "d" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc stutter-invariant -properties: inherently-weak +properties: weak --BODY-- State: 0 [0] 1 diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 327b764f0..b91991215 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -164,7 +164,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec60d690> >" + " *' at 0x7fa7cc23af60> >" ] }, "execution_count": 2, @@ -601,7 +601,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec57bc90> >" + " *' at 0x7fa7cc0e9db0> >" ] }, "execution_count": 6, @@ -677,7 +677,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec58a9f0> >" + " *' at 0x7fa7cc0fabd0> >" ] }, "execution_count": 7, @@ -760,7 +760,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec58ab10> >" + " *' at 0x7fa7cc1ce060> >" ] }, "execution_count": 8, @@ -1279,7 +1279,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec59c840> >" + " *' at 0x7fa7cc10a930> >" ] }, "execution_count": 12, @@ -1393,7 +1393,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec59ca20> >" + " *' at 0x7fa7cc10aab0> >" ] }, "execution_count": 13, @@ -1524,7 +1524,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec59cab0> >" + " *' at 0x7fa7cc10ab40> >" ] }, "execution_count": 14, @@ -1533,7 +1533,8 @@ } ], "source": [ - "spot.translate('GFa -> GFb', 'sbacc')" + "a = spot.translate('GFa -> GFb', 'sbacc')\n", + "a" ] }, { @@ -1547,656 +1548,6 @@ "cell_type": "code", "execution_count": 15, "metadata": {}, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7f16ec59cb10> >" - ] - }, - "execution_count": 15, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "a = spot.translate('F(a & X(!a &Xb))', \"any\"); a" - ] - }, - { - "cell_type": "code", - "execution_count": 16, - "metadata": {}, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "5\n", - "\n", - "5\n", - "\n", - "\n", - "\n", - "0->5\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "6\n", - "\n", - "6\n", - "\n", - "\n", - "\n", - "0->6\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "1->5\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "1->6\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & b\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", - "\n", - "2->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "2->5\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "2->6\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "a & b\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", - "3->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "3->5\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "3->6\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "4->1\n", - "\n", - "\n", - "a & b\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", - "4->5\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "4->6\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "5->5\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "7\n", - "\n", - "7\n", - "\n", - "\n", - "\n", - "5->7\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "8\n", - "\n", - "8\n", - "\n", - "\n", - "\n", - "5->8\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "6->6\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "6->7\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "6->8\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "7->7\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "9\n", - "\n", - "9\n", - "\n", - "\n", - "\n", - "7->9\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "10\n", - "\n", - "10\n", - "\n", - "\n", - "\n", - "7->10\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "8->8\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "8->9\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "8->10\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "9->9\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "\n", - "9->10\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "\n", - "11\n", - "\n", - "11\n", - "\n", - "\n", - "\n", - "9->11\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "\n", - "12\n", - "\n", - "12\n", - "\n", - "\n", - "\n", - "9->12\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "\n", - "10->9\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "\n", - "10->10\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "\n", - "10->11\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "\n", - "10->12\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "\n", - "11->9\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "\n", - "11->10\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "\n", - "11->11\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "\n", - "11->12\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "\n", - "12->9\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "\n", - "12->10\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "\n", - "12->11\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "\n", - "12->12\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7f16ec59c210> >" - ] - }, - "execution_count": 16, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "spot.sl(a)" - ] - }, - { - "cell_type": "code", - "execution_count": 17, - "metadata": {}, "outputs": [ { "data": { @@ -2204,7 +1555,7 @@ "False" ] }, - "execution_count": 17, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } @@ -2222,7 +1573,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 16, "metadata": {}, "outputs": [ { @@ -2259,7 +1610,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 17, "metadata": {}, "outputs": [ { @@ -2392,7 +1743,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec59cbd0> >" + " *' at 0x7fa7cc10a270> >" ] }, "metadata": {}, @@ -2542,7 +1893,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec57b9c0> >" + " *' at 0x7fa7cc0e9b40> >" ] }, "metadata": {}, @@ -2714,7 +2065,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec59ce40> >" + " *' at 0x7fa7cc10abd0> >" ] }, "metadata": {}, @@ -2889,7 +2240,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec59cc90> >" + " *' at 0x7fa7cc10aae0> >" ] }, "metadata": {}, @@ -2906,7 +2257,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 18, "metadata": {}, "outputs": [], "source": [ @@ -2915,7 +2266,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 19, "metadata": {}, "outputs": [ { @@ -3075,10 +2426,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec59cf00> >" + " *' at 0x7fa7cc10acf0> >" ] }, - "execution_count": 21, + "execution_count": 19, "metadata": {}, "output_type": "execute_result" } @@ -3089,7 +2440,7 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 20, "metadata": {}, "outputs": [ { @@ -3151,10 +2502,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec59c8d0> >" + " *' at 0x7fa7cc10a990> >" ] }, - "execution_count": 22, + "execution_count": 20, "metadata": {}, "output_type": "execute_result" } @@ -3165,7 +2516,7 @@ }, { "cell_type": "code", - "execution_count": 23, + "execution_count": 21, "metadata": {}, "outputs": [ { @@ -3174,7 +2525,7 @@ "True" ] }, - "execution_count": 23, + "execution_count": 21, "metadata": {}, "output_type": "execute_result" } @@ -3185,7 +2536,7 @@ }, { "cell_type": "code", - "execution_count": 24, + "execution_count": 22, "metadata": {}, "outputs": [ { @@ -3666,7 +3017,7 @@ }, { "cell_type": "code", - "execution_count": 25, + "execution_count": 23, "metadata": {}, "outputs": [ { @@ -3678,60 +3029,57 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\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", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\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", - "a\n", - "\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f16ec52abd0> >" + " *' at 0x7fa7cc096c00> >" ] }, "metadata": {}, @@ -3755,7 +3103,7 @@ }, { "cell_type": "code", - "execution_count": 26, + "execution_count": 24, "metadata": {}, "outputs": [ { @@ -3831,10 +3179,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec52ae40> >" + " *' at 0x7fa7cc096390> >" ] }, - "execution_count": 26, + "execution_count": 24, "metadata": {}, "output_type": "execute_result" } @@ -3852,7 +3200,7 @@ }, { "cell_type": "code", - "execution_count": 27, + "execution_count": 25, "metadata": {}, "outputs": [ { @@ -3904,10 +3252,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec52ab10> >" + " *' at 0x7fa7cc0e9ba0> >" ] }, - "execution_count": 27, + "execution_count": 25, "metadata": {}, "output_type": "execute_result" } @@ -3925,7 +3273,7 @@ }, { "cell_type": "code", - "execution_count": 28, + "execution_count": 26, "metadata": {}, "outputs": [ { @@ -3993,7 +3341,7 @@ "" ] }, - "execution_count": 28, + "execution_count": 26, "metadata": {}, "output_type": "execute_result" } @@ -4011,7 +3359,7 @@ }, { "cell_type": "code", - "execution_count": 29, + "execution_count": 27, "metadata": {}, "outputs": [ { @@ -4068,10 +3416,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f16ec53da50> >" + " *' at 0x7fa7cc096f00> >" ] }, - "execution_count": 29, + "execution_count": 27, "metadata": {}, "output_type": "execute_result" } @@ -4089,7 +3437,7 @@ }, { "cell_type": "code", - "execution_count": 30, + "execution_count": 28, "metadata": {}, "outputs": [ { @@ -4101,60 +3449,57 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\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", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\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", - "a\n", - "\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f16ec52abd0> >" + " *' at 0x7fa7cc096c00> >" ] }, "metadata": {}, @@ -4169,60 +3514,57 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\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", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f16ec52abd0> >" + " *' at 0x7fa7cc096c00> >" ] }, "metadata": {}, @@ -4247,7 +3589,7 @@ }, { "cell_type": "code", - "execution_count": 31, + "execution_count": 29, "metadata": {}, "outputs": [ { @@ -4259,63 +3601,60 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\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", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & b & c\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f16ec52abd0> >" + " *' at 0x7fa7cc096c00> >" ] }, - "execution_count": 31, + "execution_count": 29, "metadata": {}, "output_type": "execute_result" } @@ -4345,7 +3684,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5" + "version": "3.6.5+" } }, "nbformat": 4, diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 370aab3c6..4454142f0 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -240,7 +240,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128edca50> >" + " *' at 0x7feca4075120> >" ] }, "execution_count": 4, @@ -352,7 +352,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e4cd50> >" + " *' at 0x7fec96f528d0> >" ] }, "execution_count": 5, @@ -462,7 +462,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128edca50> >" + " *' at 0x7feca4075120> >" ] }, "execution_count": 6, @@ -695,7 +695,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e4cab0> >" + " *' at 0x7fec96f528a0> >" ] }, "execution_count": 8, @@ -892,7 +892,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e4cab0> >" + " *' at 0x7fec96f528a0> >" ] }, "execution_count": 11, @@ -977,7 +977,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e6d8a0> >" + " *' at 0x7fec96f52a50> >" ] }, "metadata": {}, @@ -1032,7 +1032,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e6d780> >" + " *' at 0x7fec96f529f0> >" ] }, "metadata": {}, @@ -1126,7 +1126,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e6d090> >" + " *' at 0x7fec96f52ab0> >" ] }, "execution_count": 13, @@ -1257,7 +1257,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e6d090> >" + " *' at 0x7fec96f52ab0> >" ] }, "metadata": {}, @@ -1322,7 +1322,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e6d8a0> >" + " *' at 0x7fec96f52a50> >" ] }, "metadata": {}, @@ -1377,7 +1377,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e6d780> >" + " *' at 0x7fec96f529f0> >" ] }, "metadata": {}, @@ -1609,7 +1609,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e6db40> >" + " *' at 0x7fec96f52b40> >" ] }, "metadata": {}, @@ -1624,14 +1624,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1648,14 +1645,15 @@ "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "a & !b\n", "\n", "\n", @@ -1674,17 +1672,16 @@ "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -1697,7 +1694,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e6dba0> >" + " *' at 0x7fec96f52c00> >" ] }, "metadata": {}, @@ -1794,7 +1791,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e6d180> >" + " *' at 0x7fec96f52b10> >" ] }, "metadata": {}, @@ -1962,7 +1959,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e6dc30> >" + " *' at 0x7fec96f52d80> >" ] }, "execution_count": 18, @@ -2130,7 +2127,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e6dc30> >" + " *' at 0x7fec96f52d80> >" ] }, "execution_count": 19, @@ -2293,7 +2290,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0128e6dc30> >" + " *' at 0x7fec96f52d80> >" ] }, "metadata": {}, @@ -2757,13 +2754,6 @@ "spot.highlight_languages(aut)\n", "aut.show('.bas')" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { @@ -2782,7 +2772,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5" + "version": "3.6.5+" } }, "nbformat": 4, diff --git a/tests/python/product.ipynb b/tests/python/product.ipynb index afe02367e..de0db966a 100644 --- a/tests/python/product.ipynb +++ b/tests/python/product.ipynb @@ -39,14 +39,14 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -78,15 +78,22 @@ "0->1\n", "\n", "\n", - "a\n", + "a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", "\n", @@ -189,223 +196,189 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "0,1\n", + "\n", + "0,1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "1,0\n", + "\n", + "1,0\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "1,1\n", + "\n", + "1,1\n", "\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", + "\n", "\n", - "1->1\n", - "\n", - "\n", - "b & !c\n", - "\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", + "2->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", - "\n", - "\n", "2->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", "\n", "\n", "\n", @@ -420,7 +393,7 @@ } ], "source": [ - "a1 = spot.translate('FGa')\n", + "a1 = spot.translate('FGa & GFb')\n", "a2 = spot.translate('G(Fc U b)')\n", "prod = spot.product(a1, a2)\n", "display_inline(a1, a2, prod)" @@ -451,14 +424,14 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -490,15 +463,22 @@ "0->1\n", "\n", "\n", - "a\n", + "a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", "\n", @@ -593,223 +573,189 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "0,1\n", + "\n", + "0,1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "1,0\n", + "\n", + "1,0\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "1,1\n", + "\n", + "1,1\n", "\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", + "\n", "\n", - "1->1\n", - "\n", - "\n", - "b & !c\n", - "\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", + "2->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", - "\n", - "\n", "2->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", "\n", "\n", "\n", @@ -863,14 +809,14 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -902,15 +848,22 @@ "0->1\n", "\n", "\n", - "a\n", + "a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", "\n", @@ -1005,189 +958,161 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "t\n", - "[all]\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", "0->0\n", - "\n", - "\n", - "!b & c\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "\n", + "!b & !c\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", + "a & b\n", "\n", - "\n", + "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\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", - "1->0\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", + "\n", "\n", - "1->1\n", - "\n", - "\n", - "b & !c\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & c\n", + "2->2\n", + "\n", + "\n", + "a & !b & c\n", "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", - "\n", "2->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "a & b & c\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n", @@ -1267,7 +1192,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "(a,)\n", + "(a, b)\n", "(c, b)\n", "()\n" ] @@ -1312,14 +1237,14 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1351,15 +1276,22 @@ "0->1\n", "\n", "\n", - "a\n", + "a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", "\n", @@ -1454,223 +1386,189 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\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", - "!b & c\n", - "\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "\n", + "!b & !c\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", + "a & b\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\n", + "\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", - "1->0\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", + "\n", "\n", - "1->1\n", - "\n", - "\n", - "b & !c\n", - "\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", + "2->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", - "\n", - "\n", "2->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", "\n", "\n", "\n", @@ -1687,7 +1585,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "(a, c, b)\n" + "(a, b, c)\n" ] } ], @@ -1863,14 +1761,14 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1902,15 +1800,22 @@ "0->1\n", "\n", "\n", - "a\n", + "a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", "\n", @@ -2005,223 +1910,189 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "0,1\n", + "\n", + "0,1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "1,0\n", + "\n", + "1,0\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "1,1\n", + "\n", + "1,1\n", "\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", + "\n", "\n", - "1->1\n", - "\n", - "\n", - "b & !c\n", - "\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", + "2->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", - "\n", - "\n", "2->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", "\n", "\n", "\n", @@ -2314,234 +2185,200 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", "\n", "0\n", "\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", "\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", "2\n", "\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", "\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", + "\n", "\n", - "1->1\n", - "\n", - "\n", - "b & !c\n", - "\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", + "2->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", - "\n", - "\n", "2->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", "\n", "\n", "" @@ -2589,7 +2426,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "264 µs ± 2.11 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)\n" + "219 µs ± 5.11 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)\n" ] } ], @@ -2606,7 +2443,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "4.9 µs ± 45.2 ns per loop (mean ± std. dev. of 7 runs, 100000 loops each)\n" + "5.23 µs ± 532 ns per loop (mean ± std. dev. of 7 runs, 100000 loops each)\n" ] } ], @@ -2656,7 +2493,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5" + "version": "3.6.5+" } }, "nbformat": 4, diff --git a/tests/python/remfin.py b/tests/python/remfin.py index 02a55dda9..5acf3b173 100644 --- a/tests/python/remfin.py +++ b/tests/python/remfin.py @@ -27,10 +27,9 @@ Start: 0 AP: 1 "a" acc-name: co-Buchi Acceptance: 1 Fin(0) -properties: trans-labels explicit-labels state-acc deterministic -properties: inherently-weak +properties: trans-labels explicit-labels state-acc deterministic weak --BODY-- -State: 0 +State: 0 {0} [0] 1 State: 1 [t] 1 diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb index 3010ce323..9d4c8b999 100644 --- a/tests/python/stutter-inv.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -302,7 +302,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc1642b47b0> >" + " *' at 0x7f31a00c1660> >" ] }, "metadata": {}, @@ -449,153 +449,153 @@ "\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", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\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", "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", "1->3\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\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", + "a & !b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", + "\n", "\n", "\n", "\n", "5->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", + "\n", "\n", "\n", "\n", "4->7\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "7->7\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc1642c22d0> >" + " *' at 0x7f31a00c1b40> >" ] }, "metadata": {}, @@ -658,153 +658,153 @@ "\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", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\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", "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", "1->3\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\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", + "a & !b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", + "\n", "\n", "\n", "\n", "5->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", + "\n", "\n", "\n", "\n", "4->7\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "7->7\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc1642c22d0> >" + " *' at 0x7f31a00c1b40> >" ] }, "metadata": {}, @@ -963,7 +963,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc1642b4750> >" + " *' at 0x7f31a00c1630> >" ] }, "metadata": {}, @@ -978,16 +978,16 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "FG(!a | X!a)\n", - "\n", - "FG(!a | X!a)\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "FG(!a | X!a)\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1011,58 +1011,57 @@ "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\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", "\n", "0->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc1642d26c0> >" + " *' at 0x7f31a0114060> >" ] }, "metadata": {}, @@ -1279,7 +1278,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc1642d2720> >" + " *' at 0x7f31a00c1480> >" ] }, "metadata": {}, @@ -1408,7 +1407,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc1643175a0> >" + " *' at 0x7f31a01140c0> >" ] }, "metadata": {}, @@ -1539,7 +1538,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc1642d2ea0> >" + " *' at 0x7f31a00c1ae0> >" ] }, "metadata": {}, @@ -1799,7 +1798,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc1642e62a0> >" + " *' at 0x7f31a005d870> >" ] }, "metadata": {}, @@ -2113,7 +2112,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc1642e62a0> >" + " *' at 0x7f31a005d870> >" ] }, "metadata": {}, @@ -2336,13 +2335,6 @@ "source": [ "100*sum(sistates_size)/sum(aut_size)" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { @@ -2361,7 +2353,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5" + "version": "3.6.5+" } }, "nbformat": 4,