From a325de8678eac5946e06567ae4cd3a13eced60f0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Jun 2018 17:09:18 +0200 Subject: [PATCH] postproc: simplify the acceptance condition * spot/twaalgos/postproc.cc: Here. * spot/twaalgos/cobuchi.cc, spot/twaalgos/totgba.cc: Fix some bug uncovered by the new simplified automata. * tests/core/satmin2.test, tests/core/sccdot.test, tests/core/sim3.test, tests/python/decompose.ipynb, tests/python/satmin.ipynb: Update expected results. * NEWS: Mention the simplification and the bug. --- NEWS | 9 +- spot/twaalgos/cobuchi.cc | 10 +- spot/twaalgos/postproc.cc | 23 + spot/twaalgos/totgba.cc | 47 +- tests/core/satmin2.test | 3 +- tests/core/sccdot.test | 2 +- tests/core/sim3.test | 14 +- tests/python/decompose.ipynb | 236 ++-- tests/python/satmin.ipynb | 2583 ++++++++++++++++------------------ 9 files changed, 1397 insertions(+), 1530 deletions(-) diff --git a/NEWS b/NEWS index 86a57d9e0..4276cd9c9 100644 --- a/NEWS +++ b/NEWS @@ -116,6 +116,10 @@ New in spot 2.5.3.dev (not yet released) FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21 4 4 FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170 8 8 + - The automaton postprocessor will now simplify acceptance + conditions more aggressively, calling spot::simplify_acceptance() + or spot::cleanup_acceptance() depanding on the optimization level. + - print_dot(), used to print automata in GraphViz's format, underwent several changes: @@ -216,7 +220,10 @@ New in spot 2.5.3.dev (not yet released) - The HOA parser will now accept Alias: declarations that occur before AP:. - - the option --allow-dups of randltl now works properly + - The option --allow-dups of randltl now works properly. + + - Converting generalized-co-Büchi to Streett using dnf_to_nca() + could produce bogus automata if the input had rejecting SCCs. Deprecation notice: diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index 40b0d86a7..9fab6b64d 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -133,7 +133,7 @@ namespace spot product_states* res_map_; // States of the aug. sub. cons. scc_info si_; // SCC information. unsigned nb_states_; // Number of states. - unsigned was_rabin_; // Was it Rabin before Streett? + unsigned was_dnf_; // Was it DNF before Streett? std::vector* orig_states_; // Match old Rabin st. from new. std::vector* orig_clauses_; // Associated Rabin clauses. unsigned orig_num_st_; // Rabin original nb states. @@ -148,7 +148,7 @@ namespace spot bv->set(state); unsigned clause = 0; unsigned state = st.first; - if (was_rabin_) + if (was_dnf_) { clause = (*orig_clauses_)[state]; assert((int)clause >= 0); @@ -194,7 +194,7 @@ namespace spot const const_twa_graph_ptr ref_power, std::vector& pairs, bool named_states = false, - bool was_rabin = false, + bool was_dnf = false, unsigned orig_num_st = 0) : aut_(ref_prod), state_based_(aut_->prop_state_acc().is_true()), @@ -206,10 +206,10 @@ namespace spot si_(res_, (scc_info_options::TRACK_STATES | scc_info_options::TRACK_SUCCS)), nb_states_(res_->num_states()), - was_rabin_(was_rabin), + was_dnf_(was_dnf), orig_num_st_(orig_num_st ? orig_num_st : ref_prod->num_states()) { - if (was_rabin) + if (was_dnf) { orig_states_ = ref_prod->get_named_prop> ("original-states"); diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 9ed38dbee..0c14af47f 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -39,6 +39,7 @@ #include #include #include +#include namespace spot { @@ -230,6 +231,27 @@ namespace spot throw std::runtime_error("postprocessor: the Colored setting only works " "for parity acceptance"); + + + // Attempt to simplify the acceptance condition, unless this is a + // parity automaton and we want parity acceptance in the output. + auto simplify_acc = [&](twa_graph_ptr in) + { + if (PREF_ == Any && level_ == Low) + return in; + if (!(want_parity && in->acc().is_parity())) + { + if (level_ == High) + return simplify_acceptance(in); + else + return cleanup_acceptance(in); + } + if (level_ == High) + return cleanup_parity(in); + return in; + }; + a = simplify_acc(a); + if (!a->is_existential() && // We will probably have to revisit this condition later. // Currently, the intent is that postprocessor should never @@ -438,6 +460,7 @@ namespace spot { dba = tgba_determinize(to_generalized_buchi(sim), false, det_scc_, det_simul_, det_stutter_); + dba = simplify_acc(dba); if (level_ != Low) dba = simulation(dba); sim = nullptr; diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index 1b4022cbf..4e2c6c802 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -76,35 +76,32 @@ namespace spot void split_dnf_clauses(const acc_cond::acc_code& code) { - bool one_conjunction = false; - const acc_cond::acc_op root_op = code.back().sub.op; - auto s = code.back().sub.size; - while (s) + auto pos = &code.back(); + if (pos->sub.op == acc_cond::acc_op::Or) + --pos; + auto start = &code.front(); + while (pos > start) { - --s; - if (code[s].sub.op == acc_cond::acc_op::And - || ((one_conjunction = root_op == acc_cond::acc_op::And))) + const unsigned short size = pos[0].sub.size; + if (pos[0].sub.op == acc_cond::acc_op::And) { - s = one_conjunction ? s + 1 : s; - const unsigned short size = code[s].sub.size; acc_cond::mark_t fin = {}; acc_cond::mark_t inf = {}; - for (unsigned i = 1; i <= size; i += 2) + for (int i = 1; i <= (int)size; i += 2) { - if (code[s-i].sub.op == acc_cond::acc_op::Fin) - fin |= code[s-i-1].mark; - else if (code[s-i].sub.op == acc_cond::acc_op::Inf) - inf |= code[s-i-1].mark; + if (pos[-i].sub.op == acc_cond::acc_op::Fin) + fin |= pos[-i - 1].mark; + else if (pos[-i].sub.op == acc_cond::acc_op::Inf) + inf |= pos[-i - 1].mark; else SPOT_UNREACHABLE(); } all_clauses_.emplace_back(fin, inf); set_to_keep_.emplace_back(fin | inf); - s -= size; } - else if (code[s].sub.op == acc_cond::acc_op::Fin) // Fin + else if (pos[0].sub.op == acc_cond::acc_op::Fin) // Fin { - auto m1 = code[--s].mark; + auto m1 = pos[-1].mark; for (unsigned int s : m1.sets()) { all_clauses_.emplace_back(acc_cond::mark_t({s}), @@ -112,9 +109,9 @@ namespace spot set_to_keep_.emplace_back(acc_cond::mark_t({s})); } } - else if (code[s].sub.op == acc_cond::acc_op::Inf) // Inf + else if (pos[0].sub.op == acc_cond::acc_op::Inf) // Inf { - auto m2 = code[--s].mark; + auto m2 = pos[-1].mark; all_clauses_.emplace_back(acc_cond::mark_t({}), m2); set_to_keep_.emplace_back(m2); } @@ -122,6 +119,7 @@ namespace spot { SPOT_UNREACHABLE(); } + pos -= size + 1; } #if TRACE trace << "\nPrinting all clauses\n"; @@ -244,10 +242,12 @@ namespace spot trace << "accepting clauses\n"; for (unsigned i = 0; i < res.size(); ++i) { - trace << "scc(" << i << ") --> "; + trace << "scc(" << i << ") -->"; for (auto elt : res[i]) - trace << elt << ','; - trace << '\n' + trace << ' ' << elt; + if (si_.is_rejecting_scc(i)) + trace << " rej"; + trace << '\n'; } trace << '\n'; #endif @@ -341,6 +341,7 @@ namespace spot { if (!si_.is_useful_scc(scc)) continue; + trace << "scc #" << scc << '\n'; bool rej_scc = acc_clauses_[scc].empty(); for (auto st : si_.states_of(scc)) @@ -388,7 +389,7 @@ namespace spot acc_cond::mark_t m = {}; if (same_scc || state_based_) - m = all_set_to_add_; + m = e.acc | all_set_to_add_; for (const auto& p_dst : st_repr_[e.dst]) res_->new_edge(src, p_dst.second, e.cond, m); diff --git a/tests/core/satmin2.test b/tests/core/satmin2.test index 42f9958e9..113e23d86 100755 --- a/tests/core/satmin2.test +++ b/tests/core/satmin2.test @@ -335,7 +335,8 @@ HOA: v1 States: 1 Start: 0 AP: 1 "a" -Acceptance: 2 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1)) +acc-name: generalized-co-Buchi 2 +Acceptance: 2 Fin(0)|Fin(1) properties: trans-labels explicit-labels trans-acc colored complete properties: deterministic --BODY-- diff --git a/tests/core/sccdot.test b/tests/core/sccdot.test index 073a4820b..03fb2318a 100755 --- a/tests/core/sccdot.test +++ b/tests/core/sccdot.test @@ -156,7 +156,7 @@ HOA: v1 States: 8 Start: 0 AP: 2 "a" "b" -Acceptance: 3 (Inf(0)&Inf(1)) & Fin(2) +Acceptance: 3 Fin(2) & (Inf(0)&Inf(1)) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 diff --git a/tests/core/sim3.test b/tests/core/sim3.test index 147863a8a..c692e017c 100755 --- a/tests/core/sim3.test +++ b/tests/core/sim3.test @@ -1,7 +1,7 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2015, 2018 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -55,25 +55,25 @@ HOA: v1 States: 5 Start: 0 AP: 2 "b" "a" -acc-name: Rabin 2 -Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) +acc-name: Streett 1 +Acceptance: 2 Fin(0) | Inf(1) properties: trans-labels explicit-labels state-acc complete properties: deterministic --BODY-- State: 0 [!1] 1 [1] 3 -State: 1 {1 3} +State: 1 {1} [0&!1] 1 [!0&!1] 2 [0&1] 3 [!0&1] 4 -State: 2 {1} +State: 2 [0&!1] 1 [!0&!1] 2 [0&1] 3 [!0&1] 4 -State: 3 {0 3} +State: 3 {0 1} [0&!1] 1 [!0&!1] 2 [0&1] 3 diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb index 5b562d771..577ea6a67 100644 --- a/tests/python/decompose.ipynb +++ b/tests/python/decompose.ipynb @@ -200,7 +200,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42fa8f00> >" + " *' at 0x7fd3d85c40f0> >" ] }, "execution_count": 2, @@ -330,7 +330,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f5f4b0> >" + " *' at 0x7fd3d85c40c0> >" ] }, "execution_count": 3, @@ -489,7 +489,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f5f720> >" + " *' at 0x7fd3d860a060> >" ] }, "execution_count": 4, @@ -587,7 +587,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f5fae0> >" + " *' at 0x7fd3d85c4120> >" ] }, "execution_count": 5, @@ -669,7 +669,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f50bd0> >" + " *' at 0x7fd3d8571690> >" ] }, "execution_count": 6, @@ -796,7 +796,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b437fb030> >" + " *' at 0x7fd3d8571360> >" ] }, "metadata": {}, @@ -941,7 +941,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42fb30c0> >" + " *' at 0x7fd3d860a240> >" ] }, "metadata": {}, @@ -1109,7 +1109,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b437fb030> >" + " *' at 0x7fd3d862fed0> >" ] }, "metadata": {}, @@ -1512,7 +1512,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f7a780> >" + " *' at 0x7fd3d8571540> >" ] }, "execution_count": 8, @@ -1942,7 +1942,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f7a8a0> >" + " *' at 0x7fd3d85c4030> >" ] }, "metadata": {}, @@ -2174,7 +2174,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b437fb030> >" + " *' at 0x7fd3d85c4150> >" ] }, "metadata": {}, @@ -2384,7 +2384,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f5f5a0> >" + " *' at 0x7fd3d85bbfc0> >" ] }, "metadata": {}, @@ -2772,7 +2772,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f0a5a0> >" + " *' at 0x7fd3d8571a80> >" ] }, "execution_count": 10, @@ -2788,7 +2788,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "The weak automata seem to be good candidates for further simplification. Let's add a call to `postprocess()` to out decomposition loop, trying to preserve the determinism and state-based acceptance of the original automaton." + "The weak automata seem to be good candidates for further simplification. Let's add a call to `postprocess()` to our decomposition loop, trying to preserve the determinism and state-based acceptance of the original automaton." ] }, { @@ -2933,7 +2933,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42fb30c0> >" + " *' at 0x7fd3d8571bd0> >" ] }, "metadata": {}, @@ -3072,7 +3072,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42fa8f30> >" + " *' at 0x7fd3d8571b10> >" ] }, "metadata": {}, @@ -3093,16 +3093,14 @@ "strong\n", "\n", "strong\n", - "(Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")) | (Fin(\n", - "\n", - ") & Inf(\n", - "\n", - "))\n", - "[Rabin 2]\n", + "Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & Inf(\n", + "\n", + "))\n", + "[parity min even 3]\n", "\n", "cluster_0\n", "\n", @@ -3137,8 +3135,8 @@ "3\n", "\n", "3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", @@ -3185,7 +3183,7 @@ "4\n", "\n", "4\n", - "\n", + "\n", "\n", "\n", "\n", @@ -3199,7 +3197,7 @@ "5\n", "\n", "5\n", - "\n", + "\n", "\n", "\n", "\n", @@ -3282,7 +3280,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f0a4e0> >" + " *' at 0x7fd3d8571630> >" ] }, "metadata": {}, @@ -3635,7 +3633,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f7a720> >" + " *' at 0x7fd3d8571ab0> >" ] }, "execution_count": 12, @@ -4018,7 +4016,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f7a6f0> >" + " *' at 0x7fd3d85719c0> >" ] }, "metadata": {}, @@ -4195,7 +4193,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f0a4e0> >" + " *' at 0x7fd3d8571630> >" ] }, "metadata": {}, @@ -4353,7 +4351,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f7a840> >" + " *' at 0x7fd3d85715d0> >" ] }, "metadata": {}, @@ -4702,7 +4700,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f1b390> >" + " *' at 0x7fd3d857d8d0> >" ] }, "execution_count": 14, @@ -4775,7 +4773,7 @@ "\n", "\n", "\n", - "\n", + "\n", "0->0\n", "\n", "\n", @@ -4788,7 +4786,7 @@ "1\n", "\n", "\n", - "\n", + "\n", "0->1\n", "\n", "\n", @@ -4801,7 +4799,7 @@ "2\n", "\n", "\n", - "\n", + "\n", "0->2\n", "\n", "\n", @@ -4825,7 +4823,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f1b600> >" + " *' at 0x7fd3d850d7e0> >" ] }, "execution_count": 15, @@ -4892,7 +4890,7 @@ "\n", "\n", "\n", - "\n", + "\n", "0->0\n", "\n", "\n", @@ -4906,7 +4904,7 @@ "\n", "\n", "\n", - "\n", + "\n", "0->1\n", "\n", "\n", @@ -4923,7 +4921,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f6c930> >" + " *' at 0x7fd3d8571bd0> >" ] }, "metadata": {}, @@ -4968,7 +4966,7 @@ "\n", "\n", "\n", - "\n", + "\n", "0->0\n", "\n", "\n", @@ -4982,7 +4980,7 @@ "\n", "\n", "\n", - "\n", + "\n", "0->1\n", "\n", "\n", @@ -4999,7 +4997,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f6c930> >" + " *' at 0x7fd3d8571bd0> >" ] }, "metadata": {}, @@ -5062,7 +5060,7 @@ "\n", "\n", "\n", - "\n", + "\n", "0->0\n", "\n", "\n", @@ -5076,7 +5074,7 @@ "\n", "\n", "\n", - "\n", + "\n", "0->1\n", "\n", "\n", @@ -5093,7 +5091,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f1bd80> >" + " *' at 0x7fd3d850d720> >" ] }, "execution_count": 18, @@ -5243,7 +5241,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f1b750> >" + " *' at 0x7fd3d850d780> >" ] }, "execution_count": 19, @@ -5403,7 +5401,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f2c690> >" + " *' at 0x7fd3d850dd80> >" ] }, "metadata": {}, @@ -5505,7 +5503,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f7a840> >" + " *' at 0x7fd3d85715d0> >" ] }, "metadata": {}, @@ -5640,7 +5638,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f2c120> >" + " *' at 0x7fd3d850d090> >" ] }, "metadata": {}, @@ -5664,12 +5662,12 @@ "# `decompose_scc()` by SCC number\n", "\n", "Decompose SCC can also be called by SCC numbers.\n", - "The example below show the different SCC numbers and the state they contains, before extracting the sub-automaton containing SCC 1 and 2 (i.e., anything leading to states 1 and 4 of the original automaton). This example also shows that when an `scc_info` is available for to automaton to decompose, it can be passed to `decompose_scc()` in lieu of the automaton: doing so is faster because `decompose_scc()` does not need to rebuild this object. " + "The example below show the different SCC numbers and the state they contains, before extracting the sub-automaton containing SCC 0 and 2 (i.e., anything leading to states 1 and 4 of the original automaton). This example also shows that when an `scc_info` is available for to automaton to decompose, it can be passed to `decompose_scc()` in lieu of the automaton: doing so is faster because `decompose_scc()` does not need to rebuild this object. " ] }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 22, "metadata": {}, "outputs": [ { @@ -5844,7 +5842,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f6c990> >" + " *' at 0x7fd3d85c4060> >" ] }, "metadata": {}, @@ -5859,122 +5857,136 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "cluster_0\n", - "\n", + "\n", "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "\n", "cluster_2\n", - "\n", + "\n", "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "a & c\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f6b42f6c900> >" + " *' at 0x7fd3d860a240> >" ] }, - "execution_count": 21, + "execution_count": 22, "metadata": {}, "output_type": "execute_result" } @@ -5985,7 +5997,7 @@ "for scc in range(si.scc_count()):\n", " print(\"SCC #{} containts states {}\".format(scc, list(si.states_of(scc))))\n", "display(aut)\n", - "spot.decompose_scc(si, '1,2')" + "spot.decompose_scc(si, '0,2')" ] }, { @@ -5997,7 +6009,7 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 23, "metadata": {}, "outputs": [ { @@ -6074,10 +6086,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f6b42f2c150> >" + " *' at 0x7fd3d850d8d0> >" ] }, - "execution_count": 22, + "execution_count": 23, "metadata": {}, "output_type": "execute_result" } @@ -6103,7 +6115,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5" + "version": "3.6.5+" } }, "nbformat": 4, diff --git a/tests/python/satmin.ipynb b/tests/python/satmin.ipynb index a34f9d170..16e9e44a5 100644 --- a/tests/python/satmin.ipynb +++ b/tests/python/satmin.ipynb @@ -256,7 +256,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7b085aaea0> >" + " *' at 0x7f79c85a5150> >" ] }, "execution_count": 3, @@ -444,7 +444,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7b0861fc90> >" + " *' at 0x7f79c857fb40> >" ] }, "execution_count": 4, @@ -680,7 +680,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7b085b5060> >" + " *' at 0x7f79c85d20f0> >" ] }, "execution_count": 5, @@ -913,7 +913,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7b08561b70> >" + " *' at 0x7f79c857f5d0> >" ] }, "execution_count": 6, @@ -973,96 +973,95 @@ "\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", - "!b & !c\n", - "\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", "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", - "!c\n", - "\n", - "\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "(!a & c) | (b & c)\n", - "\n", - "\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7b08561b40> >" + " *' at 0x7f79c857fc00> >" ] }, "execution_count": 7, @@ -1234,7 +1233,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7b08561c00> >" + " *' at 0x7f79c857f9c0> >" ] }, "execution_count": 8, @@ -1267,140 +1266,133 @@ "\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", - "0->0\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", - "\n", + "\n", + "1\n", + "\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "(!a & b) | (b & c)\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", - "\n", + "\n", + "2\n", + "\n", "\n", "\n", - "\n", + "\n", "0->2\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", - "\n", + "\n", + "3\n", + "\n", "\n", "\n", - "\n", + "\n", "0->3\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "(a & b) | (b & c)\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", - "\n", - "1->3\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", "\n", - "2->0\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "b & c\n", + "1->3\n", + "\n", + "\n", + "b & c\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "!a & !b & !c\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "b & !c\n", + "\n", + "\n", + "a | b | c\n", "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!a | b | c\n", + "\n", + "\n", + "3->2\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" ], "text/plain": [ - " *' at 0x7f7b08561bd0> >" + " *' at 0x7f79c851b090> >" ] }, "execution_count": 9, @@ -1470,9 +1462,9 @@ " NaN\n", " NaN\n", " NaN\n", - " 1428\n", - " 73430\n", - " 4\n", + " 996\n", + " 48806\n", + " 2\n", " 0\n", " 1\n", " 0\n", @@ -1484,11 +1476,11 @@ " 5\n", " 16\n", " 40\n", - " 3960\n", - " 336307\n", - " 13\n", - " 1\n", - " 19\n", + " 2760\n", + " 224707\n", + " 9\n", + " 0\n", + " 6\n", " 0\n", " \n", "
\n", @@ -1496,13 +1488,13 @@ " 5\n", " 4\n", " 4\n", - " 12\n", + " 11\n", " 32\n", " 2008\n", - " 116372\n", - " 5\n", + " 155020\n", + " 6\n", " 0\n", - " 4\n", + " 7\n", " 0\n", "
\n", " \n", @@ -1511,14 +1503,14 @@ ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", - "0 6 3 NaN NaN NaN 1428 \n", - "1 6 5 5 16 40 3960 \n", - "2 5 4 4 12 32 2008 \n", + "0 6 3 NaN NaN NaN 996 \n", + "1 6 5 5 16 40 2760 \n", + "2 5 4 4 11 32 2008 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 73430 4 0 1 0 \n", - "1 336307 13 1 19 0 \n", - "2 116372 5 0 4 0 " + "0 48806 2 0 1 0 \n", + "1 224707 9 0 6 0 \n", + "2 155020 6 0 7 0 " ] }, "metadata": {}, @@ -1533,140 +1525,133 @@ "\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", - "0->0\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", - "\n", + "\n", + "1\n", + "\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "(!a & b) | (b & c)\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", - "\n", + "\n", + "2\n", + "\n", "\n", "\n", - "\n", + "\n", "0->2\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", - "\n", + "\n", + "3\n", + "\n", "\n", "\n", - "\n", + "\n", "0->3\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "(a & b) | (b & c)\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", - "\n", - "1->3\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", "\n", - "2->0\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "b & c\n", + "1->3\n", + "\n", + "\n", + "b & c\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "!a & !b & !c\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "b & !c\n", + "\n", + "\n", + "a | b | c\n", "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!a | b | c\n", + "\n", + "\n", + "3->2\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" ], "text/plain": [ - " *' at 0x7f7b0cb8d6f0> >" + " *' at 0x7f79cdb10330> >" ] }, "execution_count": 10, @@ -1732,9 +1717,9 @@ " NaN\n", " NaN\n", " NaN\n", - " 483\n", - " 24470\n", - " 2\n", + " 348\n", + " 15542\n", + " 1\n", " 0\n", " 0\n", " 0\n", @@ -1743,28 +1728,14 @@ " 1\n", " 2\n", " 5\n", - " 5\n", - " 16\n", - " 40\n", - " 1335\n", - " 111187\n", - " 5\n", - " 0\n", " 4\n", - " 0\n", - " \n", - "
\n", - " 2\n", - " 2\n", - " 4\n", - " 4\n", - " 12\n", + " 10\n", " 32\n", - " 856\n", - " 57332\n", + " 960\n", + " 71987\n", " 3\n", " 0\n", - " 1\n", + " 2\n", " 0\n", "
\n", " \n", @@ -1773,14 +1744,12 @@ ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", - "0 2 3 NaN NaN NaN 483 \n", - "1 2 5 5 16 40 1335 \n", - "2 2 4 4 12 32 856 \n", + "0 2 3 NaN NaN NaN 348 \n", + "1 2 5 4 10 32 960 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 24470 2 0 0 0 \n", - "1 111187 5 0 4 0 \n", - "2 57332 3 0 1 0 " + "0 15542 1 0 0 0 \n", + "1 71987 3 0 2 0 " ] }, "metadata": {}, @@ -1795,140 +1764,126 @@ "\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 & c\n", + "\n", + "\n", + "(!a & !b) | (!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) | (!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) | (b & c)\n", + "\n", + "\n", + "a & !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 & !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->2\n", - "\n", - "\n", - "b & c\n", + "\n", + "\n", + "(a & b) | (b & c)\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "b & !c\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "b\n", "\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "b | c\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!c\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7b0cb8dc00> >" + " *' at 0x7f79cdb107b0> >" ] }, "execution_count": 11, @@ -1994,13 +1949,13 @@ " 2\n", " 5\n", " 5\n", - " 18\n", + " 16\n", " 40\n", - " 3050\n", - " 437037\n", - " 20\n", + " 2300\n", + " 285287\n", + " 13\n", " 0\n", - " 17\n", + " 9\n", " 0\n", " \n", "
\n", @@ -2010,9 +1965,9 @@ " 2\n", " 6\n", " 16\n", - " 488\n", - " 28449\n", - " 2\n", + " 368\n", + " 17993\n", + " 1\n", " 0\n", " 0\n", " 0\n", @@ -2024,8 +1979,8 @@ " NaN\n", " NaN\n", " NaN\n", - " 68\n", - " 1285\n", + " 92\n", + " 2193\n", " 0\n", " 0\n", " 0\n", @@ -2037,14 +1992,14 @@ ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", - "0 2 5 5 18 40 3050 \n", - "1 2 2 2 6 16 488 \n", - "2 2 1 NaN NaN NaN 68 \n", + "0 2 5 5 16 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 437037 20 0 17 0 \n", - "1 28449 2 0 0 0 \n", - "2 1285 0 0 0 0 " + "0 285287 13 0 9 0 \n", + "1 17993 1 0 0 0 \n", + "2 2193 0 0 0 0 " ] }, "metadata": {}, @@ -2142,7 +2097,7 @@ "
\n" ], "text/plain": [ - " *' at 0x7f7b0cb8dd50> >" + " *' at 0x7f79cdb108d0> >" ] }, "execution_count": 12, @@ -2205,54 +2160,40 @@ " 0\n", " 6\n", " 6\n", + " 5\n", + " 13\n", + " 40\n", + " 2742\n", + " 173183\n", " 6\n", - " 19\n", - " 48\n", - " 3894\n", - " 258719\n", - " 9\n", " 0\n", - " 6\n", + " 3\n", " 0\n", " \n", "
\n", " 1\n", - " 6\n", - " 5\n", - " 5\n", - " 15\n", - " 40\n", - " 2005\n", - " 106302\n", - " 5\n", - " 0\n", - " 2\n", - " 0\n", - "
\n", - "
\n", - " 2\n", " 5\n", " 4\n", " 4\n", " 11\n", " 32\n", - " 676\n", - " 24632\n", - " 1\n", + " 964\n", + " 45412\n", + " 2\n", + " 0\n", " 0\n", - " 1\n", " 0\n", "
\n", "
\n", - " 3\n", + " 2\n", " 4\n", " 3\n", " NaN\n", " NaN\n", " NaN\n", " 363\n", - " 10553\n", - " 0\n", + " 10496\n", + " 1\n", " 0\n", " 0\n", " 0\n", @@ -2263,16 +2204,14 @@ ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", - "0 6 6 6 19 48 3894 \n", - "1 6 5 5 15 40 2005 \n", - "2 5 4 4 11 32 676 \n", - "3 4 3 NaN NaN NaN 363 \n", + "0 6 6 5 13 40 2742 \n", + "1 5 4 4 11 32 964 \n", + "2 4 3 NaN NaN NaN 363 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 258719 9 0 6 0 \n", - "1 106302 5 0 2 0 \n", - "2 24632 1 0 1 0 \n", - "3 10553 0 0 0 0 " + "0 173183 6 0 3 0 \n", + "1 45412 2 0 0 0 \n", + "2 10496 1 0 0 0 " ] }, "metadata": {}, @@ -2287,129 +2226,129 @@ "\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) | (!b & !c)\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", "\n", "\n", - "\n", + "\n", "0->2\n", - "\n", - "\n", - "(!a & b) | (b & c)\n", + "\n", + "\n", + "(!a & b) | (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 & !c\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "\n", + "\n", "1->0\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "\n", + "\n", "1->2\n", - "\n", - "\n", - "(!a & b) | (b & c)\n", + "\n", + "\n", + "b & c\n", "\n", "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", "\n", - "2->2\n", - "\n", - "\n", - "c\n", + "1->3\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "b | c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7b0cb8dde0> >" + " *' at 0x7f79c857fba0> >" ] }, "execution_count": 13, @@ -2488,11 +2427,11 @@ " NaN\n", " NaN\n", " NaN\n", - " 3899\n", - " 258963\n", - " 10\n", + " 2747\n", + " 173427\n", + " 6\n", " 0\n", - " 3\n", + " 1\n", " 0\n", "
\n", "
\n", @@ -2502,8 +2441,8 @@ " NaN\n", " NaN\n", " NaN\n", - " 3899\n", - " 258963\n", + " 2747\n", + " 173427\n", " 0\n", " 0\n", " 1\n", @@ -2514,10 +2453,10 @@ " 6\n", " 4\n", " 4\n", - " 11\n", + " 12\n", " 32\n", - " 3899\n", - " 258963\n", + " 2747\n", + " 173427\n", " 0\n", " 0\n", " 0\n", @@ -2529,14 +2468,14 @@ ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", - "0 6 1 NaN NaN NaN 3899 \n", - "1 6 3 NaN NaN NaN 3899 \n", - "2 6 4 4 11 32 3899 \n", + "0 6 1 NaN NaN NaN 2747 \n", + "1 6 3 NaN NaN NaN 2747 \n", + "2 6 4 4 12 32 2747 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 258963 10 0 3 0 \n", - "1 258963 0 0 1 0 \n", - "2 258963 0 0 0 0 " + "0 173427 6 0 1 0 \n", + "1 173427 0 0 1 0 \n", + "2 173427 0 0 0 0 " ] }, "metadata": {}, @@ -2551,129 +2490,136 @@ "\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) | (!b & !c)\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", "\n", "\n", "\n", "1\n", - "\n", - "1\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", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & 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->0\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", + "a & !b & c\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "(a & b) | (b & c)\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!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" ], "text/plain": [ - " *' at 0x7f7b08561690> >" + " *' at 0x7f79cdb10b10> >" ] }, "execution_count": 14, @@ -2738,56 +2684,42 @@ " 0\n", " 6\n", " 6\n", + " 5\n", + " 13\n", + " 40\n", + " 2742\n", + " 173183\n", " 6\n", - " 19\n", - " 48\n", - " 3894\n", - " 258719\n", - " 10\n", " 0\n", - " 6\n", + " 3\n", " 0\n", "
\n", "
\n", " 1\n", - " 6\n", " 5\n", - " 5\n", - " 14\n", - " 40\n", - " 3894\n", - " 258767\n", - " 0\n", - " 0\n", + " 4\n", + " 4\n", + " 12\n", + " 32\n", + " 2742\n", + " 173279\n", " 0\n", + " 1\n", + " 1\n", " 0\n", "
\n", "
\n", " 2\n", - " 5\n", - " 4\n", - " 4\n", - " 10\n", - " 32\n", - " 3894\n", - " 258815\n", - " 1\n", - " 0\n", - " 0\n", - " 0\n", - "
\n", - "
\n", - " 3\n", " 4\n", " 3\n", " NaN\n", " NaN\n", " NaN\n", - " 363\n", - " 10325\n", + " 2742\n", + " 173327\n", + " 0\n", " 0\n", " 0\n", - " 1\n", " 0\n", "
\n", " \n", @@ -2796,16 +2728,14 @@ ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", - "0 6 6 6 19 48 3894 \n", - "1 6 5 5 14 40 3894 \n", - "2 5 4 4 10 32 3894 \n", - "3 4 3 NaN NaN NaN 363 \n", + "0 6 6 5 13 40 2742 \n", + "1 5 4 4 12 32 2742 \n", + "2 4 3 NaN NaN NaN 2742 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 258719 10 0 6 0 \n", - "1 258767 0 0 0 0 \n", - "2 258815 1 0 0 0 \n", - "3 10325 0 0 1 0 " + "0 173183 6 0 3 0 \n", + "1 173279 0 1 1 0 \n", + "2 173327 0 0 0 0 " ] }, "metadata": {}, @@ -2820,122 +2750,136 @@ "\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) | (!b & !c)\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "(!a & !c) | (!b & !c)\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "c | (a & b)\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & b & !c\n", "\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", "\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "(a & b) | (b & c)\n", "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "(!a & b) | (b & !c)\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7b08561ab0> >" + " *' at 0x7f79cdb10c30> >" ] }, "execution_count": 15, @@ -2972,122 +2916,136 @@ "\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) | (!b & !c)\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "(!a & !c) | (!b & !c)\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "c | (a & b)\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & b & !c\n", "\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", "\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "(a & b) | (b & c)\n", "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "(!a & b) | (b & !c)\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7b0cb610f0> >" + " *' at 0x7f79cdb109f0> >" ] }, "metadata": {}, @@ -3133,59 +3091,44 @@ " 0\n", " 6\n", " 6\n", - " 6\n", - " 19\n", - " 48\n", - " 3894\n", - " 258719\n", - " 10\n", - " 0\n", " 5\n", - " 0\n", - " HOA: v1 States: 6 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...\n", - " \n", - "
\n", - " 1\n", - " 6\n", - " 5\n", - " 5\n", - " 14\n", + " 13\n", " 40\n", - " 3894\n", - " 258767\n", - " 0\n", - " 0\n", + " 2742\n", + " 173183\n", + " 7\n", " 0\n", + " 3\n", " 0\n", " HOA: v1 States: 5 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...\n", "
\n", "
\n", - " 2\n", + " 1\n", " 5\n", " 4\n", " 4\n", - " 10\n", + " 12\n", " 32\n", - " 3894\n", - " 258815\n", - " 0\n", + " 2742\n", + " 173279\n", " 0\n", " 0\n", + " 1\n", " 0\n", " HOA: v1 States: 4 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...\n", "
\n", "
\n", - " 3\n", + " 2\n", " 4\n", " 3\n", " NaN\n", " NaN\n", " NaN\n", - " 363\n", - " 10325\n", + " 2742\n", + " 173327\n", + " 0\n", " 0\n", " 0\n", - " 1\n", " 0\n", " NaN\n", "
\n", @@ -3195,22 +3138,19 @@ ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", - "0 6 6 6 19 48 3894 \n", - "1 6 5 5 14 40 3894 \n", - "2 5 4 4 10 32 3894 \n", - "3 4 3 NaN NaN NaN 363 \n", + "0 6 6 5 13 40 2742 \n", + "1 5 4 4 12 32 2742 \n", + "2 4 3 NaN NaN NaN 2742 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \\\n", - "0 258719 10 0 5 0 \n", - "1 258767 0 0 0 0 \n", - "2 258815 0 0 0 0 \n", - "3 10325 0 0 1 0 \n", + "0 173183 7 0 3 0 \n", + "1 173279 0 0 1 0 \n", + "2 173327 0 0 0 0 \n", "\n", " automaton \n", - "0 HOA: v1 States: 6 Start: 0 AP: 3 \"a\" \"c\" \"b\" a... \n", - "1 HOA: v1 States: 5 Start: 0 AP: 3 \"a\" \"c\" \"b\" a... \n", - "2 HOA: v1 States: 4 Start: 0 AP: 3 \"a\" \"c\" \"b\" a... \n", - "3 NaN " + "0 HOA: v1 States: 5 Start: 0 AP: 3 \"a\" \"c\" \"b\" a... \n", + "1 HOA: v1 States: 4 Start: 0 AP: 3 \"a\" \"c\" \"b\" a... \n", + "2 NaN " ] }, "metadata": {}, @@ -3251,198 +3191,149 @@ "\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) | (!b & !c)\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "c | (a & b)\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & b & !c\n", "\n", - "\n", - "\n", - "5\n", - "\n", - "5\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", "\n", - "\n", - "\n", - "2->5\n", - "\n", - "\n", - "(!a & !c) | (!b & !c)\n", - "\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "!a & !b & c\n", - "\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "(!a & b) | (b & !c)\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", - "4->5\n", - "\n", - "\n", - "a & b & c\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", + "\n", "\n", - "1->1\n", - "\n", - "\n", - "c\n", + "0->3\n", + "\n", + "\n", + "b & c\n", "\n", - "\n", - "\n", - "5->2\n", - "\n", - "\n", - "(!a & !c) | (b & !c)\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", "\n", - "\n", - "\n", - "5->1\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "a & b & !c\n", "\n", - "\n", - "\n", - "5->5\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "1\n", "\n", - "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", "\n", - "3->2\n", - "\n", - "\n", - "b & !c\n", + "2->2\n", + "\n", + "\n", + "a & !b & c\n", "\n", - "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", "\n", - "3->4\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", + "2->4\n", + "\n", + "\n", + "(!a & b) | (b & !c)\n", "\n", - "\n", + "\n", "\n", - "3->5\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", + "4->3\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7b0cb61300> >" + " *' at 0x7f79cdb10a80> >" ] }, "metadata": {}, @@ -3464,294 +3355,136 @@ "\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) | (!b & !c)\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "(!a & !c) | (!b & !c)\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "c | (a & b)\n", - "\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "!a & !b & c\n", - "\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7f7b0cb613f0> >" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "automaton from line 2:\n" - ] - }, - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", - "\n", + "\n", + "2\n", + "\n", "\n", "\n", - "\n", + "\n", "0->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "(a & b) | (b & c)\n", "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "\n", + "\n", "0->3\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "(!a & !c) | (!b & !c)\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "c | (a & b)\n", - "\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", - "\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "(!a & b) | (b & !c)\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7b0cb61480> >" + " *' at 0x7f79cdb10e40> >" ] }, "metadata": {}, @@ -3983,7 +3716,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7b08561b70> >" + " *' at 0x7f79c857f5d0> >" ] }, "execution_count": 18, @@ -4049,11 +3782,11 @@ " NaN\n", " NaN\n", " NaN\n", - " 975\n", - " 32912\n", + " 687\n", + " 21896\n", " 1\n", " 0\n", - " 1\n", + " 0\n", " 0\n", " \n", "
\n", @@ -4061,13 +3794,13 @@ " 6\n", " 5\n", " 4\n", - " 10\n", + " 12\n", " 32\n", - " 2705\n", - " 150257\n", - " 6\n", + " 1905\n", + " 100457\n", + " 4\n", " 0\n", - " 3\n", + " 2\n", " 0\n", "
\n", " \n", @@ -4076,12 +3809,12 @@ ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", - "0 6 3 NaN NaN NaN 975 \n", - "1 6 5 4 10 32 2705 \n", + "0 6 3 NaN NaN NaN 687 \n", + "1 6 5 4 12 32 1905 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 32912 1 0 1 0 \n", - "1 150257 6 0 3 0 " + "0 21896 1 0 0 0 \n", + "1 100457 4 0 2 0 " ] }, "metadata": {}, @@ -4096,122 +3829,136 @@ "\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", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "(!a & b) | (b & !c)\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "(a & !b) | (!b & c)\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "(a & !b) | (!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 & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!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", + "\n", "2->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "(!a & b) | (b & !c)\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "\n", + "\n", "3->1\n", - "\n", - "\n", - "a | c\n", + "\n", + "\n", + "c | (!a & !b) | (a & b)\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "(!a & b & !c) | (a & !b & !c)\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7b0cb61510> >" + " *' at 0x7f79cdb10e40> >" ] }, "execution_count": 19, @@ -4271,12 +4018,12 @@ " 4\n", " 12\n", " 32\n", - " 1732\n", - " 77340\n", - " 3\n", + " 1220\n", + " 51612\n", + " 2\n", " 0\n", " 1\n", - " 0\n", + " 1\n", " \n", "
\n", " 1\n", @@ -4301,7 +4048,7 @@ " NaN\n", " 363\n", " 10496\n", - " 0\n", + " 1\n", " 0\n", " 0\n", " 0\n", @@ -4312,14 +4059,14 @@ ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", - "0 6 4 4 12 32 1732 \n", + "0 6 4 4 12 32 1220 \n", "1 4 2 NaN NaN NaN 162 \n", "2 4 3 NaN NaN NaN 363 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 77340 3 0 1 0 \n", + "0 51612 2 0 1 1 \n", "1 3129 0 0 0 0 \n", - "2 10496 0 0 0 0 " + "2 10496 1 0 0 0 " ] }, "metadata": {}, @@ -4463,7 +4210,7 @@ "
\n" ], "text/plain": [ - " *' at 0x7f7b085aaf30> >" + " *' at 0x7f79cdae52a0> >" ] }, "execution_count": 20, @@ -4529,14 +4276,14 @@ " 0\n", " 2\n", " 7\n", - " 5\n", - " 14\n", - " 40\n", - " 1869\n", - " 135032\n", - " 5\n", + " 7\n", + " 22\n", + " 56\n", + " 1379\n", + " 87992\n", + " 4\n", " 0\n", - " 2\n", + " 1\n", " 0\n", " \n", " \n", @@ -4545,10 +4292,10 @@ ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", - "0 2 7 5 14 40 1869 \n", + "0 2 7 7 22 56 1379 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 135032 5 0 2 0 " + "0 87992 4 0 1 0 " ] }, "metadata": {}, @@ -4563,157 +4310,226 @@ "\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) | (!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", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "!a & !b & c\n", "\n", "\n", - "\n", + "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", - "\n", + "\n", "0->4\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "(a & b) | (b & c)\n", "\n", - "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", "\n", - "1->1\n", - "\n", - "\n", - "!a & !b & !c\n", + "1->4\n", + "\n", + "\n", + "(a & !c) | (a & b)\n", "\n", - "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "!b & c\n", + "1->6\n", + "\n", + "\n", + "!a | (!b & c)\n", "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "b | (a & !c)\n", + "2->0\n", + "\n", + "\n", + "!b & c\n", "\n", - "\n", + "\n", "\n", - "2->3\n", - "\n", - "\n", - "1\n", + "2->4\n", + "\n", + "\n", + "b & c\n", "\n", - "\n", + "\n", "\n", - "3->2\n", - "\n", - "\n", - "!c\n", + "2->5\n", + "\n", + "\n", + "!b & !c\n", "\n", - "\n", + "\n", "\n", - "3->3\n", - "\n", - "\n", - "c\n", + "2->6\n", + "\n", + "\n", + "b & !c\n", "\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "(!a & !b) | (!b & !c)\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!c\n", "\n", "\n", - "\n", + "\n", "4->4\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "5->5\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", + "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", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !b & c\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7b0cb61660> >" + " *' at 0x7f79cdae5270> >" ] }, "execution_count": 21, @@ -4724,6 +4540,13 @@ "source": [ "spot.sat_minimize(small, acc=\"co-Buchi\", states=7, state_based=True, display_log=True)" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -4742,7 +4565,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5" + "version": "3.6.5+" } }, "nbformat": 4,