From f3e57901a4ea7174b3c4aeb8a1e41bc5be524c0c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 20 Jun 2019 13:23:37 +0200 Subject: [PATCH] simulation: improve merging of transiant-SCCs * spot/twaalgos/simulation.cc: Code this. * tests/core/det.test, tests/core/dra2dba.test, tests/core/satmin.test, tests/core/sim3.test, tests/python/decompose.ipynb, tests/python/dualize.py: Adjust test cases. * NEWS: Mention the optimization. --- NEWS | 3 + spot/twaalgos/simulation.cc | 52 +++++- tests/core/det.test | 18 +- tests/core/dra2dba.test | 3 +- tests/core/satmin.test | 16 +- tests/core/sim3.test | 2 +- tests/python/decompose.ipynb | 313 +++++++++++++++-------------------- tests/python/dualize.py | 33 ++-- 8 files changed, 215 insertions(+), 225 deletions(-) diff --git a/NEWS b/NEWS index 285c26ba1..0a5e9034b 100644 --- a/NEWS +++ b/NEWS @@ -45,6 +45,9 @@ New in spot 2.7.5.dev (not yet released) 'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1 state instead of 4.) + - simulation-based reductions hae learned another trick to better + merge states from transiant SCCs. + - acc_cond::top_disjuncts() and acc_cond::top_conjuncts() can be used to split an acceptance condition on the top-level & or |. These methods also exist in acc_cond::acc_code. diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index 889736fcd..41d049ef7 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -23,6 +23,7 @@ #include #include #include +#include #include #include #include @@ -493,7 +494,7 @@ namespace spot } } - // Build the minimal resulting automaton. + // Build the simplified automaton. twa_graph_ptr build_result() { twa_graph_ptr res = make_twa_graph(a_->get_dict()); @@ -526,6 +527,9 @@ namespace spot (*record_implications_)[s] = relation_[cl]; } + std::vector signatures; + signatures.reserve(sorted_classes_.size()); + // Acceptance of states. Only used if Sba && Cosimulation. std::vector accst; if (Sba && Cosimulation) @@ -538,6 +542,7 @@ namespace spot unsigned nb_minato = 0; auto all_inf = all_inf_; + unsigned srcst = 0; // For each class, we will create // all the edges between the states. for (auto& p: sorted_classes_) @@ -552,7 +557,11 @@ namespace spot if (Cosimulation) sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial)); - // Get all the variable in the signature. + assert(gb->get_state(src.id()) == srcst); + assert(signatures.size() == srcst); + signatures.push_back(bdd_exist(sig, all_proms_)); + + // Get all the variables in the signature. bdd sup_sig = bdd_support(sig); // Get the variable in the signature which represents the @@ -607,7 +616,6 @@ namespace spot // acceptance conditions on the input automaton, // we must revert them to create a new edge. acc ^= all_inf; - if (Cosimulation) { if (Sba) @@ -617,7 +625,7 @@ namespace spot // to all edges leaving src. As we // can't do this here, store this in a table // so we can fix it later. - accst[gb->get_state(src.id())] = acc; + accst[srcst] = acc; acc = {}; } gb->new_edge(dst.id(), src.id(), cond, acc); @@ -628,6 +636,7 @@ namespace spot } } } + ++srcst; } res->set_init_state(gb->get_state(previous_class_ @@ -652,6 +661,41 @@ namespace spot } } + // Attempt to merge trivial SCCs + if (!record_implications_ && res->num_states() > 1) + { + scc_info si(res, scc_info_options::NONE); + unsigned nscc = si.scc_count(); + unsigned nstates = res->num_states(); + std::vector redirect(nstates); + std::iota(redirect.begin(), redirect.end(), 0); + bool changed = false; + for (unsigned scc = 0; scc < nscc; ++scc) + if (si.is_trivial(scc)) + { + unsigned s = si.one_state_of(scc); + bdd ref = signatures[s]; + for (unsigned i = 0; i < nstates; ++i) + if (si.reachable_state(i) + && signatures[i] == ref && !si.is_trivial(si.scc_of(i))) + { + changed = true; + redirect[s] = i; + break; + } + } + if (changed) + { + if (Cosimulation) + for (auto& e: res->edges()) + e.src = redirect[e.src]; + else + for (auto& e: res->edges()) + e.dst = redirect[e.dst]; + res->set_init_state(redirect[res->get_init_state_number()]); + } + } + // If we recorded implications for the determinization // procedure, we should not remove unreachable states, as that // will invalidate the contents of the IMPLICATIONS vector. diff --git a/tests/core/det.test b/tests/core/det.test index 112876710..70db98b7c 100755 --- a/tests/core/det.test +++ b/tests/core/det.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013-2018 Laboratoire de Recherche et Développement de +# Copyright (C) 2013-2019 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -24,17 +24,17 @@ set -e cat >formulas <<'EOF' 1,13,X((a M F((!b & !c) | (b & c))) W (G!c U b)) 1,5,X(((a & b) R (!a U !c)) R b) -1,9,XXG(Fa U Xb) +1,8,XXG(Fa U Xb) 1,5,(!a M !b) W F!c 1,3,(b & Fa & GFc) R a 1,2,(a R (b W a)) W G(!a M (b | c)) 1,11,(Fa W b) R (!a | Fc) -1,7,X(G(!a M !b) | G(a | G!a)) +1,6,X(G(!a M !b) | G(a | G!a)) 1,2,Fa W Gb -1,3,Ga | GFb +1,2,Ga | GFb 1,9,G((G!a & ((!b & X!c) | (b & Xc))) | (Fa & ((!b & Xc) | (b & X!c)))) 1,5,a M G(F!b | X!a) -1,4,G!a R XFb +1,3,G!a R XFb 1,4,XF(!a | GFb) 1,5,X(GF!a U a) 1,5,(a | G(a M !b)) W Fc @@ -43,14 +43,14 @@ cat >formulas <<'EOF' 1,2,XG!a R Fb 1,4,GFc | (a & Fb) 1,6,X(a R (Fb R F!b)) -1,2,G(Xa M Fa) -1,4,X(Gb | GFa) +1,1,G(Xa M Fa) +1,3,X(Gb | GFa) 1,9,X(Gc | XG((b & Ga) | (!b & F!a))) 1,2,Ga R Fb 1,3,G(a U (b | X((!a & !c) | (a & c)))) 1,5,XG((G!a & F!b) | (Fa & (a | Gb))) -1,9,(a U X!a) | XG(!b & Fc) -1,4,X(G!a | GFa) +1,7,(a U X!a) | XG(!b & Fc) +1,3,X(G!a | GFa) 1,4,G(G!a | F!c | G!b) EOF diff --git a/tests/core/dra2dba.test b/tests/core/dra2dba.test index 04c28235b..b2bf0faf4 100755 --- a/tests/core/dra2dba.test +++ b/tests/core/dra2dba.test @@ -330,4 +330,5 @@ Acc-Sig: +2 EOF autcross 'dstar2tgba -D' --language-preserved -F in.dra --csv=out.csv -grep '3,18,107,144,1,2,0,0,0$' out.csv +cat out.csv +grep '3,17,104,136,1,1,0,0,0$' out.csv diff --git a/tests/core/satmin.test b/tests/core/satmin.test index 64bef08f1..71ca9ee54 100755 --- a/tests/core/satmin.test +++ b/tests/core/satmin.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2017, 2018 Laboratoire de Recherche et Développement +# Copyright (C) 2013, 2017, 2018, 2019 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -949,7 +949,7 @@ cat >expected <<'EOF' "!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","16",4 "!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","17",4 "X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","1",5 -"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","2",7 +"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","2",6 "X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","3",6 "X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","4",6 "X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","6",6 @@ -1013,7 +1013,7 @@ cat >expected <<'EOF' "!((F(p0)) W (G(p1)))","16",2 "!((F(p0)) W (G(p1)))","17",2 "(G(F(p1))) | (G(p0))","1",3 -"(G(F(p1))) | (G(p0))","2",3 +"(G(F(p1))) | (G(p0))","2",2 "(G(F(p1))) | (G(p0))","3",2 "(G(F(p1))) | (G(p0))","4",2 "(G(F(p1))) | (G(p0))","6",2 @@ -1076,8 +1076,8 @@ cat >expected <<'EOF' "!((p0) M (G((F(!(p1))) | (X(!(p0))))))","15",4 "!((p0) M (G((F(!(p1))) | (X(!(p0))))))","16",4 "!((p0) M (G((F(!(p1))) | (X(!(p0))))))","17",4 -"(G(!(p0))) R (X(F(p1)))","1",4 -"(G(!(p0))) R (X(F(p1)))","2",4 +"(G(!(p0))) R (X(F(p1)))","1",3 +"(G(!(p0))) R (X(F(p1)))","2",3 "(G(!(p0))) R (X(F(p1)))","3",3 "(G(!(p0))) R (X(F(p1)))","4",3 "(G(!(p0))) R (X(F(p1)))","6",3 @@ -1333,7 +1333,7 @@ cat >expected <<'EOF' "!(X((p0) R ((F(p1)) R (F(!(p1))))))","16",3 "!(X((p0) R ((F(p1)) R (F(!(p1))))))","17",3 "G((X(p0)) M (F(p0)))","1",2 -"G((X(p0)) M (F(p0)))","2",2 +"G((X(p0)) M (F(p0)))","2",1 "G((X(p0)) M (F(p0)))","3",1 "G((X(p0)) M (F(p0)))","4",1 "G((X(p0)) M (F(p0)))","6",1 @@ -1365,7 +1365,7 @@ cat >expected <<'EOF' "!(G((X(p0)) M (F(p0))))","16",2 "!(G((X(p0)) M (F(p0))))","17",2 "X((G(F(p1))) | (G(p0)))","1",4 -"X((G(F(p1))) | (G(p0)))","2",4 +"X((G(F(p1))) | (G(p0)))","2",3 "X((G(F(p1))) | (G(p0)))","3",3 "X((G(F(p1))) | (G(p0)))","4",3 "X((G(F(p1))) | (G(p0)))","6",3 @@ -1493,7 +1493,7 @@ cat >expected <<'EOF' "!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","16",7 "!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","17",7 "X((G(F(p0))) | (G(!(p0))))","1",4 -"X((G(F(p0))) | (G(!(p0))))","2",4 +"X((G(F(p0))) | (G(!(p0))))","2",3 "X((G(F(p0))) | (G(!(p0))))","3",3 "X((G(F(p0))) | (G(!(p0))))","4",3 "X((G(F(p0))) | (G(!(p0))))","6",3 diff --git a/tests/core/sim3.test b/tests/core/sim3.test index 8a5a398b4..c4375c646 100755 --- a/tests/core/sim3.test +++ b/tests/core/sim3.test @@ -47,7 +47,7 @@ State: 6 {0 3} --END-- EOF -test "`autfilt --small input --stats=%S,%s`" = 7,2 +test "`autfilt --small input --stats=%S,%s`" = 7,1 autfilt -S --high --small input -H > out cat >expected <\n" ], "text/plain": [ - " *' at 0x7fd3d85c40f0> >" + " *' at 0x7f6b8c2eaf30> >" ] }, "execution_count": 2, @@ -330,7 +330,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d85c40c0> >" + " *' at 0x7f6b8c2f7270> >" ] }, "execution_count": 3, @@ -489,7 +489,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d860a060> >" + " *' at 0x7f6b8c2f70f0> >" ] }, "execution_count": 4, @@ -587,7 +587,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d85c4120> >" + " *' at 0x7f6b8c2f7540> >" ] }, "execution_count": 5, @@ -669,7 +669,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d8571690> >" + " *' at 0x7f6b8c2f7810> >" ] }, "execution_count": 6, @@ -796,7 +796,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d8571360> >" + " *' at 0x7f6b8c2f7630> >" ] }, "metadata": {}, @@ -941,7 +941,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d860a240> >" + " *' at 0x7f6b8c2f7420> >" ] }, "metadata": {}, @@ -1109,7 +1109,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d862fed0> >" + " *' at 0x7f6b8c2f7a50> >" ] }, "metadata": {}, @@ -1512,7 +1512,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d8571540> >" + " *' at 0x7f6b8c283210> >" ] }, "execution_count": 8, @@ -1942,7 +1942,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d85c4030> >" + " *' at 0x7f6b8c283360> >" ] }, "metadata": {}, @@ -2174,7 +2174,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d85c4150> >" + " *' at 0x7f6b8c2f7a50> >" ] }, "metadata": {}, @@ -2384,7 +2384,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d85bbfc0> >" + " *' at 0x7f6b8c2f7bd0> >" ] }, "metadata": {}, @@ -2772,7 +2772,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d8571a80> >" + " *' at 0x7f6b8c2838d0> >" ] }, "execution_count": 10, @@ -2933,7 +2933,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d8571bd0> >" + " *' at 0x7f6b8c2f7450> >" ] }, "metadata": {}, @@ -3072,7 +3072,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d8571b10> >" + " *' at 0x7f6b8c2f7d50> >" ] }, "metadata": {}, @@ -3087,200 +3087,145 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "strong\n", - "\n", - "strong\n", - "Inf(\n", - "⓿\n", - ") | (Fin(\n", - "❶\n", - ") & Inf(\n", - "❷\n", - "))\n", - "[parity min even 3]\n", + "\n", + "strong\n", + "Inf(\n", + "⓿\n", + ") | (Fin(\n", + "❶\n", + ") & Inf(\n", + "❷\n", + "))\n", + "[parity min even 3]\n", "\n", "cluster_0\n", - "\n", + "\n", "\n", "\n", "cluster_1\n", - "\n", - "\n", - "\n", - "cluster_2\n", - "\n", - "\n", - "\n", - "cluster_3\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", "\n", - "3\n", - "\n", - "3\n", - "⓿\n", - "❶\n", + "2\n", + "\n", + "2\n", + "❶\n", "\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", + "⓿\n", + "❶\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", + "0->1\n", + "\n", + "\n", + "!a & !c\n", "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a & !c\n", "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "❶\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !c\n", "\n", - "\n", + "\n", "\n", - "5\n", - "\n", - "5\n", - "❷\n", - "\n", - "\n", - "\n", - "3->5\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "a & !c\n", - "\n", - "\n", - "\n", - "5->3\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "\n", - "5->4\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "\n", - "5->5\n", - "\n", - "\n", - "a & b & !c\n", + "3\n", + "\n", + "3\n", + "❷\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "a & !c\n", - "\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a & !c\n", "\n", - "\n", - "\n", - "2->5\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fd3d8571630> >" + " *' at 0x7f6b8c2f7930> >" ] }, "metadata": {}, @@ -3633,7 +3578,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d8571ab0> >" + " *' at 0x7f6b8c2ea960> >" ] }, "execution_count": 12, @@ -4016,7 +3961,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d85719c0> >" + " *' at 0x7f6b8c2ea7e0> >" ] }, "metadata": {}, @@ -4193,7 +4138,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d8571630> >" + " *' at 0x7f6b8c2f7900> >" ] }, "metadata": {}, @@ -4351,7 +4296,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d85715d0> >" + " *' at 0x7f6b8c2f7600> >" ] }, "metadata": {}, @@ -4700,7 +4645,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d857d8d0> >" + " *' at 0x7f6b8c2eafc0> >" ] }, "execution_count": 14, @@ -4823,7 +4768,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d850d7e0> >" + " *' at 0x7f6b8c283b70> >" ] }, "execution_count": 15, @@ -4921,7 +4866,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d8571bd0> >" + " *' at 0x7f6b8c283810> >" ] }, "metadata": {}, @@ -4997,7 +4942,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d8571bd0> >" + " *' at 0x7f6b8c283810> >" ] }, "metadata": {}, @@ -5091,7 +5036,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d850d720> >" + " *' at 0x7f6b8c2922d0> >" ] }, "execution_count": 18, @@ -5241,7 +5186,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d850d780> >" + " *' at 0x7f6b8c292270> >" ] }, "execution_count": 19, @@ -5401,7 +5346,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d850dd80> >" + " *' at 0x7f6b8c2eadb0> >" ] }, "metadata": {}, @@ -5503,7 +5448,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d85715d0> >" + " *' at 0x7f6b8c3302d0> >" ] }, "metadata": {}, @@ -5638,7 +5583,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d850d090> >" + " *' at 0x7f6b8c330270> >" ] }, "metadata": {}, @@ -5842,7 +5787,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d85c4060> >" + " *' at 0x7f6b8c2f77b0> >" ] }, "metadata": {}, @@ -5983,7 +5928,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d860a240> >" + " *' at 0x7f6b8c2f7a50> >" ] }, "execution_count": 21, @@ -6086,7 +6031,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd3d850d8d0> >" + " *' at 0x7f6b8c2f7b70> >" ] }, "execution_count": 22, @@ -6115,7 +6060,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.6+" + "version": "3.7.3" } }, "nbformat": 4, diff --git a/tests/python/dualize.py b/tests/python/dualize.py index b919eaac0..e5d9cc0aa 100755 --- a/tests/python/dualize.py +++ b/tests/python/dualize.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de +# Copyright (C) 2017-2019 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -553,7 +553,7 @@ dual = spot.dualize(aut) h = dual.to_str('hoa') assert h == """HOA: v1 -States: 6 +States: 5 Start: 0 AP: 2 "a" "b" acc-name: co-Buchi @@ -561,27 +561,24 @@ Acceptance: 1 Fin(0) properties: trans-labels explicit-labels state-acc complete properties: deterministic univ-branch --BODY-- -State: 0 -[0] 1 -[!0] 1&2 -State: 1 {0} -[0&1] 1 -[0&!1] 4 -[!0&!1] 2&4 -[!0&1] 1&2 +State: 0 {0} +[0&1] 0 +[0&!1] 1 +[!0&!1] 1&2 +[!0&1] 0&2 +State: 1 +[0&1] 0 +[0&!1] 1 +[!0&!1] 1&2 +[!0&1] 0&2 State: 2 [!0&1] 3 -[0 | !1] 5 +[0 | !1] 4 State: 3 {0} [!0] 3 -[0] 5 +[0] 4 State: 4 -[0&1] 1 -[0&!1] 4 -[!0&!1] 2&4 -[!0&1] 1&2 -State: 5 -[t] 5 +[t] 4 --END--""" opts = spot.option_map() -- GitLab