diff --git a/NEWS b/NEWS index 097dafbba..4dab8d99b 100644 --- a/NEWS +++ b/NEWS @@ -19,6 +19,13 @@ New in spot 2.7.1.dev (not yet released) - twa::accepting_run() now works on automata using Fin in their acceptance condition. + - simulation-based reductions have learned a trick that sometimes + improve transition-based output when the input is state-based. + (The automaton output by 'ltl2tgba -B GFa | autfilt --small' now + has 1 state instead of 2 in previous versions. Similarly, + 'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1 + state instead of 4.) + New in spot 2.7.1 (2019-02-14) Build diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index 5a96d8a76..a36fdf0ae 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -30,6 +30,7 @@ #include #include #include +#include // Simulation-based reduction, implemented using bdd-based signatures. // @@ -151,10 +152,12 @@ namespace spot return acc_cond::mark_t(res.begin(), res.end()); } - direct_simulation(const const_twa_graph_ptr& in) + direct_simulation(const const_twa_graph_ptr& in, + std::vector* implications = nullptr) : po_size_(0), all_class_var_(bddtrue), - original_(in) + original_(in), + record_implications_(implications) { if (!has_separate_sets(in)) throw std::runtime_error @@ -211,8 +214,62 @@ namespace spot else { a_ = make_twa_graph(in, twa::prop_set::all()); - for (auto& t: a_->edges()) - t.acc ^= all_inf; + + // When we reduce automata with state-based acceptance to + // obtain transition-based acceptance, it helps to pull + // the state-based acceptance on the incoming edges + // instead of the outgoing edges. A typical example + // + // ltl2tgba -B GFa | autfilt --small + // + // The two-state Büchi automaton generated for GFa will + // not be reduced to one state if we push the acceptance + // marks to the outgoing edges. However it will be + // reduced to one state if we pull the acceptance to the + // incoming edges. + if (!Sba && !in->prop_state_acc().is_false() + && !record_implications_) + { + // common_out[i] is the set of acceptance set numbers common to + // all outgoing edges of state i. + std::vector common_out(ns); + scc_info si(a_, scc_info_options::NONE); + for (unsigned s = 0; s < ns; ++s) + { + bool first = true; + for (auto& e : a_->out(s)) + { + if (first) + { + common_out[s] = e.acc; + first = false; + } + else if (common_out[s] != e.acc) + { + // If the automaton does not have + // state-based acceptance, do not change + // pull the marks. Mark the input as + // "not-state-acc" so that we remember + // that. + std::const_pointer_cast(in) + ->prop_state_acc(false); + goto donotpull; + } + } + } + // Pull the common outgoing sets to the incoming + // edges. Doing so seems to favor cases where states + // can be merged. + for (auto& e : a_->edges()) + e.acc = ((e.acc - common_out[e.src]) | common_out[e.dst]) + ^ all_inf; + } + else + { + donotpull: + for (auto& t: a_->edges()) + t.acc ^= all_inf; + } } assert(a_->num_states() == size_a_); @@ -310,10 +367,10 @@ namespace spot } // The core loop of the algorithm. - twa_graph_ptr run(std::vector* implications = nullptr) + twa_graph_ptr run() { main_loop(); - return build_result(implications); + return build_result(); } // Take a state and compute its signature. @@ -440,7 +497,7 @@ namespace spot } // Build the minimal resulting automaton. - twa_graph_ptr build_result(std::vector* implications = nullptr) + twa_graph_ptr build_result() { twa_graph_ptr res = make_twa_graph(a_->get_dict()); res->copy_ap_of(a_); @@ -455,8 +512,8 @@ namespace spot auto* gb = res->create_namer(); - if (implications) - implications->resize(bdd_lstate_.size()); + if (record_implications_) + record_implications_->resize(bdd_lstate_.size()); // Create one state per class. for (auto& p: sorted_classes_) { @@ -468,8 +525,8 @@ namespace spot // update state_mapping for (auto& st : p->second) (*state_mapping)[st] = s; - if (implications) - (*implications)[s] = relation_[cl]; + if (record_implications_) + (*record_implications_)[s] = relation_[cl]; } // Acceptance of states. Only used if Sba && Cosimulation. @@ -597,13 +654,30 @@ namespace spot t.acc = acc; } } + if (!Sba && !Cosimulation && original_->prop_state_acc() + && !record_implications_) + { + // common_in[i] is the set of acceptance set numbers + // common to all incoming edges of state i. + std::vector + common_in(res->num_states(), res->acc().all_sets()); + for (auto& e : res->edges()) + common_in[e.dst] &= e.acc; + // Push the common incoming sets to the outgoing edges. + // Doing so cancels the preprocessing we did in the other + // direction, to prevent marks from moving around the + // automaton if we apply simulation several times, and to + // favor state-based acceptance. + for (auto& e : res->edges()) + e.acc = (e.acc - common_in[e.dst]) | common_in[e.src]; + } // If we recorded implications for the determinization // procedure, we should not remove unreachable states, as that // will invalidate the contents of the IMPLICATIONS vector. // It's OK not to purge the result, as the determinization // will only explore the reachable part anyway. - if (!implications) + if (!record_implications_) res->purge_unreachable_states(); delete gb; @@ -708,6 +782,8 @@ namespace spot automaton_size stat; const const_twa_graph_ptr original_; + + std::vector* record_implications_; }; } // End namespace anonymous. @@ -724,8 +800,8 @@ namespace spot simulation(const const_twa_graph_ptr& t, std::vector* implications) { - direct_simulation simul(t); - return simul.run(implications); + direct_simulation simul(t, implications); + return simul.run(); } twa_graph_ptr diff --git a/tests/core/dra2dba.test b/tests/core/dra2dba.test index 6ecb52957..04c28235b 100755 --- a/tests/core/dra2dba.test +++ b/tests/core/dra2dba.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2017 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2014, 2017, 2019 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -330,4 +330,4 @@ Acc-Sig: +2 EOF autcross 'dstar2tgba -D' --language-preserved -F in.dra --csv=out.csv -grep '3,23,143,184,1,2,0,0,0$' out.csv +grep '3,18,107,144,1,2,0,0,0$' out.csv diff --git a/tests/core/exclusive-tgba.test b/tests/core/exclusive-tgba.test index 9262546b7..87f57d78d 100755 --- a/tests/core/exclusive-tgba.test +++ b/tests/core/exclusive-tgba.test @@ -1,7 +1,7 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2015-2016, 2018-2019 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -166,13 +166,13 @@ diff out2 expected-simpl test "6,50,14" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' --stats='%s,%t,%e'` test "6,24,12" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' | autfilt --exclusive-ap=a,b,c --stats='%s,%t,%e'` -test "5,22,10" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' | +test "4,18,8" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' | autfilt --small --exclusive-ap=a,b,c --stats='%s,%t,%e' --ap=3` # The final automaton has 3 atomic propositions before # simplifications, but only 2 after that. ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' | autfilt --small --exclusive-ap=a,b,c --simplify-ex --ap=3 > out -test "5,21,10" = `autfilt out --stats='%s,%t,%e' --ap=2` +test "4,17,8" = `autfilt out --stats='%s,%t,%e' --ap=2` # Issue #363. diff --git a/tests/core/ltlcrossce.test b/tests/core/ltlcrossce.test index 0c32a8725..cfeaef361 100755 --- a/tests/core/ltlcrossce.test +++ b/tests/core/ltlcrossce.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2016 Laboratoire de Recherche et +# Copyright (C) 2013, 2016, 2019 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -95,7 +95,7 @@ test `grep '^error:' errors | wc -l` = 4 run 1 ltlcross --verbose -D -f 'G(F(p0) & F(G(!p1))) | (F(G(!p0)) & G(F(p1)))' \ "ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors cat errors -test `grep 'info: Comp(' errors | wc -l` = 4 +test `grep 'info: Comp(' errors | wc -l` = 3 grep 'error: P0\*N1 is nonempty' errors grep 'error: P1\*N0 is nonempty' errors grep 'error: P1\*N1 is nonempty' errors diff --git a/tests/core/satmin3.test b/tests/core/satmin3.test index 432caf5d2..2a0a9c95a 100755 --- a/tests/core/satmin3.test +++ b/tests/core/satmin3.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement +# Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -24,7 +24,8 @@ set -e # Make sure the SPOT_SATSOLVER envar works. -# DRA produced by ltl2dstar for GFp0 -> GFp1 +# DRA produced by ltl2dstar for GFp0 -> GFp1, but manually modified +# so that simulation-based reduction do not reduce it to 1 state right away. cat >test.hoa < out cat >expected <\n" ], "text/plain": [ - " *' at 0x7f3f787b3690> >" + " *' at 0x7f1dc8308cf0> >" ] }, "execution_count": 3, @@ -289,162 +289,162 @@ "\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 & !b\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!a & b\n", - "⓿\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "\n", + "\n", "0->2\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", "\n", - "1->3\n", - "\n", - "\n", - "!b\n", - "⓿\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", "\n", - "\n", + "\n", "\n", - "2->0\n", - "\n", - "\n", - "!a & !b\n", + "1->3\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "!a & b\n", - "⓿\n", + "\n", + "\n", + "a & !b\n", "\n", - "\n", + "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !b\n", + "2->1\n", + "\n", + "\n", + "!a & !b\n", "\n", - "\n", + "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "2->1\n", + "\n", + "\n", + "b\n", + "⓿\n", "\n", "\n", "\n", "3->0\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", - "\n", + "\n", "\n", - "3->0\n", - "\n", - "\n", - "!a & b\n", + "3->1\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "a & !b\n", - "⓿\n", + "\n", + "\n", + "!a & !b\n", "\n", - "\n", + "\n", "\n", - "3->2\n", - "\n", - "\n", - "a & b\n", + "3->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f3f78fcd840> >" + " *' at 0x7f1dc82fae40> >" ] }, "execution_count": 4, @@ -680,7 +680,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f78761300> >" + " *' at 0x7f1dc839a480> >" ] }, "execution_count": 5, @@ -913,7 +913,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f78761db0> >" + " *' at 0x7f1dc83222d0> >" ] }, "execution_count": 6, @@ -973,95 +973,96 @@ "\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 & c\n", - "⓿\n", + "\n", + "\n", + "!a & !b & c\n", + "❷\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b & c\n", - "❶\n", + "\n", + "\n", + "!b & !c\n", + "⓿\n", + "❷\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!b & !c\n", - "⓿\n", - "❷\n", + "\n", + "\n", + "a & !b & c\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", + "\n", + "\n", + "b & !c\n", + "⓿\n", + "❷\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b & c\n", - "❶\n", - "❸\n", + "\n", + "\n", + "b & c\n", + "❶\n", + "❸\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!b & c\n", - "❶\n", + "\n", + "\n", + "!c\n", + "⓿\n", + "❷\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!c\n", - "⓿\n", - "❷\n", + "\n", + "\n", + "(!a & b & c) | (a & !b & c)\n", + "❶\n", + "❷\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b & c\n", - "❶\n", - "❸\n", + "\n", + "\n", + "(!a & !b & c) | (a & b & c)\n", + "❶\n", + "❸\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f3f78761ba0> >" + " *' at 0x7f1dc8330240> >" ] }, "execution_count": 7, @@ -1082,7 +1083,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 8, "metadata": {}, "outputs": [ { @@ -1233,10 +1234,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f78761b70> >" + " *' at 0x7f1dc8330930> >" ] }, - "execution_count": 9, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } @@ -1254,7 +1255,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 9, "metadata": {}, "outputs": [ { @@ -1392,10 +1393,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f787b3720> >" + " *' at 0x7f1dc82bf750> >" ] }, - "execution_count": 10, + "execution_count": 9, "metadata": {}, "output_type": "execute_result" } @@ -1417,7 +1418,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 10, "metadata": {}, "outputs": [ { @@ -1478,9 +1479,9 @@ " 40\n", " 2760\n", " 224707\n", - " 8\n", + " 9\n", " 0\n", - " 7\n", + " 8\n", " 0\n", " \n", " \n", @@ -1492,9 +1493,9 @@ " 32\n", " 2008\n", " 155020\n", - " 6\n", + " 7\n", " 0\n", - " 5\n", + " 7\n", " 0\n", " \n", " \n", @@ -1509,8 +1510,8 @@ "\n", " clauses enc.user enc.sys sat.user sat.sys \n", "0 48806 2 0 1 0 \n", - "1 224707 8 0 7 0 \n", - "2 155020 6 0 5 0 " + "1 224707 9 0 8 0 \n", + "2 155020 7 0 7 0 " ] }, "metadata": {}, @@ -1651,10 +1652,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f5be97960> >" + " *' at 0x7f1daa5b8d80> >" ] }, - "execution_count": 11, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } @@ -1672,7 +1673,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 11, "metadata": {}, "outputs": [ { @@ -1718,7 +1719,7 @@ " NaN\n", " NaN\n", " 348\n", - " 15542\n", + " 15974\n", " 1\n", " 0\n", " 0\n", @@ -1728,16 +1729,30 @@ " 1\n", " 2\n", " 5\n", - " 4\n", - " 10\n", - " 32\n", + " 5\n", + " 17\n", + " 40\n", " 960\n", - " 71987\n", + " 73187\n", " 4\n", " 0\n", " 1\n", " 0\n", " \n", + " \n", + " 2\n", + " 2\n", + " 4\n", + " 4\n", + " 11\n", + " 32\n", + " 616\n", + " 37620\n", + " 1\n", + " 0\n", + " 1\n", + " 0\n", + " \n", " \n", "\n", "" @@ -1745,11 +1760,13 @@ "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", "0 2 3 NaN NaN NaN 348 \n", - "1 2 5 4 10 32 960 \n", + "1 2 5 5 17 40 960 \n", + "2 2 4 4 11 32 616 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 15542 1 0 0 0 \n", - "1 71987 4 0 1 0 " + "0 15974 1 0 0 0 \n", + "1 73187 4 0 1 0 \n", + "2 37620 1 0 1 0 " ] }, "metadata": {}, @@ -1764,129 +1781,136 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ") & Inf(\n", - "❶\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", - "⓿\n", + "\n", + "0\n", + "⓿\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", - "⓿\n", + "\n", + "1\n", + "⓿\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", - "❶\n", + "\n", + "2\n", + "❶\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", - "❶\n", + "\n", + "3\n", + "❶\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "(a & b) | (b & c)\n", + "\n", + "\n", + "(a & b) | (b & c)\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !b & !c\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "a | b | c\n", "\n", "\n", - "\n", + "\n", "2->0\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "\n", + "\n", "3->1\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f3f5bdc5cc0> >" + " *' at 0x7f1daa56c390> >" ] }, - "execution_count": 12, + "execution_count": 11, "metadata": {}, "output_type": "execute_result" } @@ -1906,7 +1930,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 12, "metadata": {}, "outputs": [ { @@ -1949,12 +1973,12 @@ " 2\n", " 5\n", " 5\n", - " 16\n", + " 19\n", " 40\n", " 2300\n", - " 285287\n", + " 288887\n", " 13\n", - " 1\n", + " 0\n", " 10\n", " 0\n", " \n", @@ -1966,10 +1990,10 @@ " 6\n", " 16\n", " 368\n", - " 17993\n", + " 18569\n", " 1\n", " 0\n", - " 0\n", + " 1\n", " 0\n", " \n", "
\n", @@ -1980,8 +2004,8 @@ " NaN\n", " NaN\n", " 92\n", - " 2193\n", - " 1\n", + " 2337\n", + " 0\n", " 0\n", " 0\n", " 0\n", @@ -1992,14 +2016,14 @@ ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", - "0 2 5 5 16 40 2300 \n", + "0 2 5 5 19 40 2300 \n", "1 2 2 2 6 16 368 \n", "2 2 1 NaN NaN NaN 92 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 285287 13 1 10 0 \n", - "1 17993 1 0 0 0 \n", - "2 2193 1 0 0 0 " + "0 288887 13 0 10 0 \n", + "1 18569 1 0 1 0 \n", + "2 2337 0 0 0 0 " ] }, "metadata": {}, @@ -2097,10 +2121,10 @@ "
\n" ], "text/plain": [ - " *' at 0x7f3f78761d20> >" + " *' at 0x7f1daa56c5a0> >" ] }, - "execution_count": 13, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } @@ -2118,7 +2142,7 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 13, "metadata": {}, "outputs": [ { @@ -2165,9 +2189,9 @@ " 40\n", " 2742\n", " 173183\n", - " 7\n", - " 0\n", - " 2\n", + " 6\n", + " 1\n", + " 4\n", " 0\n", " \n", " \n", @@ -2181,7 +2205,7 @@ " 45412\n", " 2\n", " 0\n", - " 0\n", + " 1\n", " 0\n", " \n", " \n", @@ -2193,7 +2217,7 @@ " NaN\n", " 363\n", " 10496\n", - " 1\n", + " 0\n", " 0\n", " 0\n", " 0\n", @@ -2209,9 +2233,9 @@ "2 4 3 NaN NaN NaN 363 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 173183 7 0 2 0 \n", - "1 45412 2 0 0 0 \n", - "2 10496 1 0 0 0 " + "0 173183 6 1 4 0 \n", + "1 45412 2 0 1 0 \n", + "2 10496 0 0 0 0 " ] }, "metadata": {}, @@ -2348,10 +2372,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f5bdc5d20> >" + " *' at 0x7f1daa56c7e0> >" ] }, - "execution_count": 14, + "execution_count": 13, "metadata": {}, "output_type": "execute_result" } @@ -2382,7 +2406,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 14, "metadata": {}, "outputs": [ { @@ -2429,9 +2453,9 @@ " NaN\n", " 2747\n", " 173427\n", - " 7\n", + " 6\n", " 0\n", - " 2\n", + " 1\n", " 0\n", " \n", " \n", @@ -2445,7 +2469,7 @@ " 173427\n", " 0\n", " 0\n", - " 0\n", + " 1\n", " 0\n", " \n", " \n", @@ -2473,8 +2497,8 @@ "2 6 4 4 12 32 2747 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 173427 7 0 2 0 \n", - "1 173427 0 0 0 0 \n", + "0 173427 6 0 1 0 \n", + "1 173427 0 0 1 0 \n", "2 173427 0 0 0 0 " ] }, @@ -2619,10 +2643,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f5bdc5f00> >" + " *' at 0x7f1daa56c6c0> >" ] }, - "execution_count": 15, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -2642,7 +2666,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 15, "metadata": {}, "outputs": [ { @@ -2691,7 +2715,7 @@ " 173183\n", " 6\n", " 0\n", - " 2\n", + " 3\n", " 0\n", " \n", " \n", @@ -2733,7 +2757,7 @@ "2 4 3 NaN NaN NaN 2742 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 173183 6 0 2 0 \n", + "0 173183 6 0 3 0 \n", "1 173279 0 0 1 0 \n", "2 173327 0 0 0 0 " ] @@ -2879,10 +2903,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f78fcd630> >" + " *' at 0x7f1daa56cbd0> >" ] }, - "execution_count": 16, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } @@ -2904,7 +2928,7 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 16, "metadata": {}, "outputs": [ { @@ -3045,7 +3069,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f5bd9e060> >" + " *' at 0x7f1daa56cde0> >" ] }, "metadata": {}, @@ -3096,9 +3120,9 @@ " 40\n", " 2742\n", " 173183\n", - " 7\n", - " 0\n", - " 2\n", + " 6\n", + " 1\n", + " 3\n", " 0\n", " HOA: v1 States: 5 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...\n", " \n", @@ -3128,7 +3152,7 @@ " 173327\n", " 0\n", " 0\n", - " 0\n", + " 1\n", " 0\n", " NaN\n", " \n", @@ -3143,9 +3167,9 @@ "2 4 3 NaN NaN NaN 2742 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \\\n", - "0 173183 7 0 2 0 \n", + "0 173183 6 1 3 0 \n", "1 173279 0 0 1 0 \n", - "2 173327 0 0 0 0 \n", + "2 173327 0 0 1 0 \n", "\n", " automaton \n", "0 HOA: v1 States: 5 Start: 0 AP: 3 \"a\" \"c\" \"b\" a... \n", @@ -3172,7 +3196,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 17, "metadata": {}, "outputs": [ { @@ -3333,7 +3357,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f5bd9e0c0> >" + " *' at 0x7f1daa56ce70> >" ] }, "metadata": {}, @@ -3484,7 +3508,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f5bd9e150> >" + " *' at 0x7f1daa56c840> >" ] }, "metadata": {}, @@ -3511,7 +3535,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 18, "metadata": {}, "outputs": [ { @@ -3716,10 +3740,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f78761db0> >" + " *' at 0x7f1dc83222d0> >" ] }, - "execution_count": 19, + "execution_count": 18, "metadata": {}, "output_type": "execute_result" } @@ -3737,7 +3761,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 19, "metadata": {}, "outputs": [ { @@ -3784,7 +3808,7 @@ " NaN\n", " 687\n", " 21896\n", - " 1\n", + " 2\n", " 0\n", " 0\n", " 0\n", @@ -3813,7 +3837,7 @@ "1 6 5 4 12 32 1905 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 21896 1 0 0 0 \n", + "0 21896 2 0 0 0 \n", "1 100457 4 0 2 0 " ] }, @@ -3958,10 +3982,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f5bd9e180> >" + " *' at 0x7f1daa56cea0> >" ] }, - "execution_count": 20, + "execution_count": 19, "metadata": {}, "output_type": "execute_result" } @@ -3973,7 +3997,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 20, "metadata": {}, "outputs": [ { @@ -4034,7 +4058,7 @@ " NaN\n", " 162\n", " 3129\n", - " 1\n", + " 0\n", " 0\n", " 0\n", " 0\n", @@ -4048,7 +4072,7 @@ " NaN\n", " 363\n", " 10496\n", - " 0\n", + " 1\n", " 0\n", " 0\n", " 0\n", @@ -4065,8 +4089,8 @@ "\n", " clauses enc.user enc.sys sat.user sat.sys \n", "0 51612 2 0 1 0 \n", - "1 3129 1 0 0 0 \n", - "2 10496 0 0 0 0 " + "1 3129 0 0 0 0 \n", + "2 10496 1 0 0 0 " ] }, "metadata": {}, @@ -4210,10 +4234,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f3f5bdc5ea0> >" + " *' at 0x7f1daa56cf00> >" ] }, - "execution_count": 21, + "execution_count": 20, "metadata": {}, "output_type": "execute_result" } @@ -4234,7 +4258,7 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 21, "metadata": {}, "outputs": [ { @@ -4277,13 +4301,13 @@ " 2\n", " 7\n", " 7\n", - " 22\n", + " 23\n", " 56\n", " 1379\n", - " 87992\n", - " 3\n", + " 89168\n", + " 4\n", " 0\n", - " 2\n", + " 1\n", " 0\n", " \n", " \n", @@ -4292,10 +4316,10 @@ ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", - "0 2 7 7 22 56 1379 \n", + "0 2 7 7 23 56 1379 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 87992 3 0 2 0 " + "0 89168 4 0 1 0 " ] }, "metadata": {}, @@ -4310,229 +4334,235 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ")\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", - "⓿\n", + "\n", + "0\n", + "⓿\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a & !b & !c\n", + "\n", + "\n", + "!a & !b & !c\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", - "⓿\n", + "\n", + "1\n", + "⓿\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", - "⓿\n", + "\n", + "2\n", + "⓿\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & !b & c\n", + "\n", + "\n", + "(!a & !b & c) | (a & !b & !c)\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "(a & b) | (b & c)\n", + "\n", + "\n", + "(a & b) | (b & c)\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "\n", - "1->4\n", - "\n", - "\n", - "(a & !c) | (a & b)\n", - "\n", - "\n", - "\n", - "6\n", - "\n", - "6\n", - "\n", - "\n", "\n", - "1->6\n", - "\n", - "\n", - "!a | (!b & c)\n", + "1->4\n", + "\n", + "\n", + "!b | c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "!b & c\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b & c\n", "\n", "\n", - "\n", + "\n", "2->4\n", - "\n", - "\n", - "b & c\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", + "\n", "2->5\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", "\n", "\n", - "\n", + "\n", "2->6\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", - "\n", - "4->1\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!a & !b & !c\n", "\n", "\n", - "\n", + "\n", "4->4\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", "\n", "\n", - "\n", + "\n", "5->4\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", + "\n", "5->5\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "a & !b & c\n", "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "⓿\n", - "\n", - "\n", - "\n", - "5->3\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", - "\n", - "\n", - "\n", - "6->1\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "6->6\n", - "\n", - "\n", - "c\n", - "\n", - "\n", + "\n", "\n", - "3->4\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "3->5\n", - "\n", - "\n", - "(a & !b) | (!b & !c)\n", - "\n", - "\n", - "\n", - "3->6\n", - "\n", - "\n", - "b & !c\n", + "3->1\n", + "\n", + "\n", + "!c\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "!a & !b & c\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "6->2\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "6->4\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "6->5\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f3f5bdc5f30> >" + " *' at 0x7f1daa56c0f0> >" ] }, - "execution_count": 22, + "execution_count": 21, "metadata": {}, "output_type": "execute_result" } @@ -4558,7 +4588,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.7" + "version": "3.7.2+" } }, "nbformat": 4,