From 0895f115032afd98b241d1290f5058d635bc3fe7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 4 Jan 2015 23:33:49 +0100 Subject: [PATCH] hoa: use the tgba_digraph interface to save automata * src/tgbaalgos/hoa.cc: Here. * src/tgbatest/det.test, src/tgbatest/hoaparse.test, src/tgbatest/monitor.test, doc/org/oaut.org: Adjust. --- doc/org/oaut.org | 204 +++++++++++++++++++++++++++---------- src/tgbaalgos/hoa.cc | 135 +++++++++++------------- src/tgbatest/det.test | 32 +++--- src/tgbatest/hoaparse.test | 28 ++--- src/tgbatest/monitor.test | 10 +- 5 files changed, 246 insertions(+), 163 deletions(-) diff --git a/doc/org/oaut.org b/doc/org/oaut.org index d6a06fd4d..4f98170f0 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -18,7 +18,7 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' #+begin_example -8, --utf8 enable UTF-8 characters in output (ignored with --lbtt or --spin) - --dot[=c|h|n|N|t|v] GraphViz's format (default). Add letters to chose + --dot[=c|h|n|N|s|t|v] GraphViz's format (default). Add letters to chose (c) circular nodes, (h) horizontal layout, (v) vertical layout, (n) with name, (N) without name, (s) with SCCs, (t) always transition-based @@ -70,36 +70,36 @@ ltl2tgba -H 'a U b' '(Ga -> Gb) W c' HOA: v1 name: "a U b" States: 2 -Start: 0 +Start: 1 AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc deterministic --BODY-- -State: 0 -[1] 1 -[0&!1] 0 -State: 1 {0} -[t] 1 +State: 0 {0} +[t] 0 +State: 1 +[1] 0 +[0&!1] 1 --END-- HOA: v1 name: "(Gb | F!a) W c" States: 5 -Start: 0 +Start: 1 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 -[0&1&!2] 1 -[!1&!2] 0 {0} +[0] 0 {0} +State: 1 +[0&1&!2] 0 +[!1&!2] 1 {0} [1&!2] 2 [2] 3 -State: 1 -[0] 1 {0} State: 2 -[!1&!2] 0 {0} +[!1&!2] 1 {0} [1&!2] 2 [!1&2] 3 [1&2] 4 @@ -122,44 +122,142 @@ perl -pe 's/\\\n//g;s/\\/\\\\/g;s/graph G/graph cluster/g' #+RESULTS: hoafex #+begin_example digraph root { - graph [labelloc=t, rankdir=LR]; - node [label="\\N", shape=circle]; - graph [bb="0,0,441.5,240"]; + graph [bb="0,0,425,231.06", + labelloc=t, + lheight=0.21, + rankdir=LR + ]; + node [label="\\N", + shape=circle + ]; subgraph cluster { graph [bb="", label="(Gb | F!a) W c", - lp="210,204.3"]; - I [label="", height="0.013889", pos="1.5,52.096", style=invis, width=0]; - 1 [label=1, height="0.5", pos="58.5,52.096", width="0.5"]; - 0 [label=0, height="0.5", pos="200.5,125.1", width="0.5"]; - 2 [label=2, height="0.5", pos="200.5,36.096", width="0.5"]; - 3 [label=3, height="0.5", pos="402.5,36.096", width="0.5"]; - 4 [label=4, height="0.5", pos="311.5,36.096", width="0.5"]; - I -> 1 [pos="e,40.289,51.899 2.1401,51.899 5.0641,51.899 17.545,51.899 30.02,51.899"]; - 1 -> 1 [label="!a & !c\\n{0}", lp="58.5,104.9", pos="e,64.879,68.937 52.121,68.937 50.819,78.757 52.945,87.899 58.5,87.899 61.972,87.899 64.104,84.328 64.898,79.252"]; - 1 -> 0 [label="a & b & !c", lp="129.5,122.4", pos="e,182.73,120.16 70.933,64.972 77.488,71.315 85.934,78.673 94.5,83.899 119.36,99.071 150.8,110.38 172.96,117.24"]; - 1 -> 2 [label="a & !c", lp="129.5,71.399", pos="e,186.37,47.576 76.161,56.715 97.536,61.72 134.41,67.692 164.5,58.899 169.03,57.576 173.53,55.492 177.73,53.105"]; - 1 -> 3 [label=c, lp="254.5,12.399", pos="e,386.31,27.685 67.29,36.084 73.522,26.595 82.839,15.343 94.5,9.8989 110.16,2.587 284.7,0 332.5,8.8989 347.81,11.749 364.08,17.824 377.08,23.491"]; - 0 -> 0 [label="b\\n{0}", lp="200.5,177.9", pos="e,209.73,140.44 191.27,140.44 188.67,150.81 191.75,160.9 200.5,160.9 206.24,160.9 209.54,156.56 210.4,150.64"]; - 2 -> 1 [label="!a & !c\\n{0}", lp="129.5,37.899", pos="e,70.329,37.864 184.44,27.616 178.36,24.91 171.27,22.254 164.5,20.899 133.99,14.798 123.67,10.072 94.5,20.899 88.556,23.106 82.935,26.783 77.98,30.848"]; - 2 -> 2 [label="a & !c", lp="200.5,80.399", pos="e,209.73,51.441 191.27,51.441 188.67,61.808 191.75,71.899 200.5,71.899 206.24,71.899 209.54,67.553 210.4,61.635"]; - 2 -> 3 [label="!a & c", lp="311.5,110.4", pos="e,391.52,50.509 213.43,48.678 229.77,63.836 259.52,88.261 290.5,97.899 308.32,103.45 315.05,104.52 332.5,97.899 353.31,90.008 371.91,72.788 384.69,58.494"]; - 2 -> 4 [label="a & c", lp="254.5,44.399", pos="e,293.14,35.899 218.83,35.899 236.26,35.899 262.75,35.899 282.95,35.899"]; - 3 -> 3 [label="1\\n{0}", lp="402.5,88.899", pos="e,410.17,52.19 394.83,52.19 392.98,62.288 395.54,71.899 402.5,71.899 406.96,71.899 409.61,67.955 410.45,62.465"]; - 4 -> 3 [label="!a", lp="358.5,44.399", pos="e,384.42,35.899 329.92,35.899 342.58,35.899 359.64,35.899 374.05,35.899"]; - 4 -> 4 [label=a, lp="311.5,80.399", pos="e,319.52,52.19 303.48,52.19 301.55,62.288 304.22,71.899 311.5,71.899 316.16,71.899 318.93,67.955 319.82,62.465"]; + labelloc=t, + lheight=0.21, + lp="196.5,196.66", + lwidth=1.14, + rankdir=LR + ]; + node [height="", + label="\\N", + pos="", + shape=circle, + style="", + width="" + ]; + edge [label="", + lp="", + pos="" + ]; + I [height=0.013889, + label="", + pos="1,49.162", + style=invis, + width=0.013889]; + 1 [height=0.5, + label=1, + pos="56,49.162", + width=0.5]; + I -> 1 [pos="e,37.942,49.324 1.1549,49.324 2.6725,49.324 15.097,49.324 27.628,49.324"]; + 1 -> 1 [label="!a & !c\\n{0}", + lp="56,100.32", + pos="e,62.379,66.361 49.621,66.361 48.319,76.181 50.445,85.324 56,85.324 59.472,85.324 61.604,81.752 62.398,76.677"]; + 0 [height=0.5, + label=0, + pos="189,121.16", + width=0.5]; + 1 -> 0 [label="a & b & !c", + lp="122.5,113.82", + pos="e,171.82,115.02 70.135,60.558 76.501,65.71 84.4,71.688 92,76.324 114.85,90.263 142.72,102.89 162.53,111.19"]; + 2 [height=0.5, + label=2, + pos="189,34.162", + width=0.5]; + 1 -> 2 [label="a & !c", + lp="122.5,64.823", + pos="e,174.09,44.491 73.626,53.241 93.026,57.118 125.9,61.52 153,54.324 157.19,53.213 161.39,51.47 165.37,49.466"]; + 3 [height=0.5, + label=3, + pos="375,34.162", + width=0.5]; + 1 -> 3 [label=c, + lp="240.5,9.8235", + pos="e,359.03,25.984 66.028,34.328 72.163,25.634 81.128,15.425 92,10.324 114,0 275.42,0.3271 310,7.3235 323.76,10.107 338.24,15.942 349.94,21.478"]; + 0 -> 0 [label="b\\n{0}", + lp="189,172.32", + pos="e,197.63,137.24 180.37,137.24 178.11,147.47 180.99,157.32 189,157.32 194.26,157.32 197.3,153.08 198.14,147.27"]; + 2 -> 1 [label="!a & !c\\n{0}", + lp="122.5,35.324", + pos="e,68.596,36.184 172.36,26.591 166.44,24.064 159.55,21.586 153,20.324 126.38,15.197 117.5,11.13 92,20.324 86.432,22.331 81.123,25.651 76.398,29.343"]; + 2 -> 2 [label="a & !c", + lp="189,77.824", + pos="e,197.63,50.24 180.37,50.24 178.11,60.474 180.99,70.324 189,70.324 194.26,70.324 197.3,66.082 198.14,60.273"]; + 2 -> 3 [label="!a & c", + lp="292,105.82", + pos="e,363.94,48.712 202.25,46.94 217.46,61.618 244.99,85.026 274,94.324 289.24,99.207 295.12,100.21 310,94.324 329.12,86.764 345.87,70.495 357.43,56.803"]; + 4 [height=0.5, + label=4, + pos="292,34.162", + width=0.5]; + 2 -> 4 [label="a & c", + lp="240.5,41.824", + pos="e,273.78,34.324 207.13,34.324 222.59,34.324 245.58,34.324 263.59,34.324"]; + 3 -> 3 [label="1\\n{0}", + lp="375,85.324", + pos="e,382.03,50.988 367.97,50.988 366.41,60.949 368.75,70.324 375,70.324 379,70.324 381.4,66.475 382.2,61.092"]; + 4 -> 3 [label="!a", + lp="333.5,41.824", + pos="e,356.85,34.324 310.18,34.324 320.81,34.324 334.69,34.324 346.8,34.324"]; + 4 -> 4 [label=a, + lp="292,77.824", + pos="e,299.03,50.988 284.97,50.988 283.41,60.949 285.75,70.324 292,70.324 296,70.324 298.4,66.475 299.2,61.092"]; } subgraph cluster_gv1 { graph [bb="", label="a U b", - lp="83,91.5"]; - I_gv1 [label="", height="0.013889", pos="271.5,162.1", style=invis, width=0]; - "1_gv1" [label=1, height="0.5", pos="328.5,162.1", width="0.5"]; - "0_gv1" [label=0, height="0.72222", peripheries=2, pos="414.5,162.1", width="0.72222"]; - I_gv1 -> "1_gv1" [pos="e,310.29,162.1 272.14,162.1 275.06,162.1 287.55,162.1 300.02,162.1"]; - "1_gv1" -> "1_gv1" [label="a & !b", lp="328.5,206.6", pos="e,334.88,179.13 322.12,179.13 320.82,188.95 322.94,198.1 328.5,198.1 331.97,198.1 334.1,194.52 334.9,189.45"]; - "1_gv1" -> "0_gv1" [label=b, lp="369.5,170.6", pos="e,392.32,162.1 346.74,162.1 357.03,162.1 370.2,162.1 382.19,162.1"]; - "0_gv1" -> "0_gv1" [label=1, lp="414.5,210.6", pos="e,422.51,182.68 406.49,182.68 405.39,192.94 408.05,202.1 414.5,202.1 418.63,202.1 421.21,198.34 422.24,192.94"]; + labelloc=t, + lheight=0.21, + lp="80.5,88.5", + lwidth=0.43, + rankdir=LR + ]; + node [height="", + label="\\N", + peripheries="", + pos="", + shape=circle, + style="", + width="" + ]; + edge [label="", + lp="", + pos="" + ]; + I_gv1 [height=0.013889, + label="", + pos="261,156.16", + style=invis, + width=0.013889]; + "1_gv1" [height=0.5, + label=1, + pos="316,156.16", + width=0.5]; + I_gv1 -> "1_gv1" [pos="e,297.94,156.16 261.15,156.16 262.67,156.16 275.1,156.16 287.63,156.16"]; + "1_gv1" -> "1_gv1" [label="a & !b", + lp="316,199.66", + pos="e,322.38,173.2 309.62,173.2 308.32,183.02 310.44,192.16 316,192.16 319.47,192.16 321.6,188.59 322.4,183.51"]; + "0_gv1" [height=0.72222, + label=0, + peripheries=2, + pos="399,156.16", + width=0.72222]; + "1_gv1" -> "0_gv1" [label=b, + lp="355.5,163.66", + pos="e,376.81,156.16 334.18,156.16 343.61,156.16 355.6,156.16 366.64,156.16"]; + "0_gv1" -> "0_gv1" [label=1, + lp="399,203.66", + pos="e,406.68,177.15 391.32,177.15 390.37,187.25 392.93,196.16 399,196.16 402.89,196.16 405.34,192.5 406.35,187.22"]; } } #+end_example @@ -214,21 +312,21 @@ ltl2tgba -Hm '(Ga -> Gb) W c' HOA: v1 name: "(Gb | F!a) W c" States: 5 -Start: 0 +Start: 1 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels --BODY-- -State: 0 -[0&1&!2] 1 -[!1&!2] 0 {0} +State: 0 {0} +[0] 0 +State: 1 +[0&1&!2] 0 +[!1&!2] 1 {0} [1&!2] 2 [2] 3 -State: 1 {0} -[0] 1 State: 2 -[!1&!2] 0 {0} +[!1&!2] 1 {0} [1&!2] 2 [!1&2] 3 [1&2] 4 @@ -250,8 +348,8 @@ and single-line output: ltl2tgba -Htl 'a U b' '(Ga -> Gb) W c' #+END_SRC #+RESULTS: -: HOA: v1 name: "a U b" States: 2 Start: 0 AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0 [1] 1 [0&!1] 0 State: 1 [t] 1 {0} --END-- -: HOA: v1 name: "(Gb | F!a) W c" States: 5 Start: 0 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 [0&1&!2] 1 [!1&!2] 0 {0} [1&!2] 2 [2] 3 State: 1 [0] 1 {0} State: 2 [!1&!2] 0 {0} [1&!2] 2 [!1&2] 3 [1&2] 4 State: 3 [t] 3 {0} State: 4 [!1] 3 [1] 4 --END-- +: HOA: v1 name: "a U b" States: 2 Start: 1 AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0 [t] 0 {0} State: 1 [1] 0 [0&!1] 1 --END-- +: HOA: v1 name: "(Gb | F!a) W c" States: 5 Start: 1 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 [0] 0 {0} State: 1 [0&1&!2] 0 [!1&!2] 1 {0} [1&!2] 2 [2] 3 State: 2 [!1&!2] 1 {0} [1&!2] 2 [!1&2] 3 [1&2] 4 State: 3 [t] 3 {0} State: 4 [!1] 3 [1] 4 --END-- * LBTT output diff --git a/src/tgbaalgos/hoa.cc b/src/tgbaalgos/hoa.cc index 747793aa2..f1322af4c 100644 --- a/src/tgbaalgos/hoa.cc +++ b/src/tgbaalgos/hoa.cc @@ -24,6 +24,7 @@ #include #include #include "tgba/tgba.hh" +#include "tgba/tgbagraph.hh" #include "hoa.hh" #include "reachiter.hh" #include "misc/escape.hh" @@ -36,7 +37,7 @@ namespace spot { namespace { - struct metadata + struct metadata final { // Assign a number to each atomic proposition. typedef std::map ap_map; @@ -44,16 +45,8 @@ namespace spot typedef std::vector vap_t; vap_t vap; - // Map each state to a number. - typedef std::unordered_map state_map; - state_map sm; - // Map each number to its states. - typedef std::vector number_map; - number_map nm; - std::vector common_acc; - bool state_acc; + bool has_state_acc; bool is_complete; bool is_deterministic; @@ -62,22 +55,15 @@ namespace spot typedef std::map sup_map; sup_map sup; - metadata(const const_tgba_ptr& aut) - : state_acc(true), is_complete(true), is_deterministic(true) + metadata(const const_tgba_digraph_ptr& aut) { - number_all_states_and_fill_sup(aut); + check_det_and_comp(aut); number_all_ap(); } - ~metadata() - { - for (auto s: nm) - s->destroy(); - } - std::ostream& emit_acc(std::ostream& os, - const const_tgba_ptr& aut, + const const_tgba_digraph_ptr& aut, acc_cond::mark_t b) { // FIXME: We could use a cache for this. @@ -97,70 +83,54 @@ namespace spot return os; } - void number_all_states_and_fill_sup(const const_tgba_ptr& aut) + void check_det_and_comp(const const_tgba_digraph_ptr& aut) { std::string empty; - // Scan the whole automaton to number states. - std::deque todo; - - const state* init = aut->get_init_state(); - sm[init] = 0; - nm.push_back(init); - todo.push_back(init); - - while (!todo.empty()) + unsigned ns = aut->num_states(); + bool deterministic = true; + bool complete = true; + bool state_acc = true; + for (unsigned src = 0; src < ns; ++src) { - auto src = todo.front(); - todo.pop_front(); - bool notfirst = false; - acc_cond::mark_t prev = 0U; - bool st_acc = true; bdd sum = bddfalse; bdd available = bddtrue; - for (auto i: aut->succ(src)) + bool st_acc = true; + bool notfirst = false; + acc_cond::mark_t prev = 0U; + for (auto& t: aut->out(src)) { - const state* dst = i->current_state(); - bdd cond = i->current_condition(); - if (is_complete) - sum |= cond; - if (is_deterministic) + if (complete) + sum |= t.cond; + if (deterministic) { - if (!bdd_implies(cond, available)) - is_deterministic = false; + if (!bdd_implies(t.cond, available)) + deterministic = false; else - available -= cond; - } - sup.insert(std::make_pair(cond, empty)); - if (sm.insert(std::make_pair(dst, nm.size())).second) - { - nm.push_back(dst); - todo.push_back(dst); - } - else - { - dst->destroy(); + available -= t.cond; } + sup.insert(std::make_pair(t.cond, empty)); if (st_acc) { - acc_cond::mark_t acc = i->current_acceptance_conditions(); - if (notfirst && prev != acc) + if (notfirst && prev != t.acc) { st_acc = false; } else { notfirst = true; - prev = acc; + prev = t.acc; } } } - if (is_complete) - is_complete &= sum == bddtrue; - + if (complete) + complete &= sum == bddtrue; common_acc.push_back(st_acc); state_acc &= st_acc; } + is_deterministic = deterministic; + is_complete = complete; + has_state_acc = state_acc; } void number_all_ap() @@ -240,21 +210,25 @@ namespace spot Hoa_Acceptance_Mixed /// mix state-based and transition-based }; - std::ostream& + static std::ostream& hoa_reachable(std::ostream& os, - const const_tgba_ptr& aut, + const const_tgba_digraph_ptr& aut, hoa_acceptance acceptance, hoa_alias alias, bool newline) { (void) alias; + // Calling get_init_state_number() may add a state to empty + // automata, so it has to be done first. + unsigned init = aut->get_init_state_number(); + metadata md(aut); - if (acceptance == Hoa_Acceptance_States && !md.state_acc) + if (acceptance == Hoa_Acceptance_States && !md.has_state_acc) acceptance = Hoa_Acceptance_Transitions; - unsigned num_states = md.nm.size(); + unsigned num_states = aut->num_states(); const char nl = newline ? '\n' : ' '; os << "HOA: v1" << nl; @@ -262,7 +236,7 @@ namespace spot if (n) escape_str(os << "name: \"", *n) << '"' << nl; os << "States: " << num_states << nl - << "Start: 0" << nl + << "Start: " << init << nl << "AP: " << md.vap.size(); auto d = aut->get_dict(); for (auto& i: md.vap) @@ -311,24 +285,26 @@ namespace spot this_acc = (md.common_acc[i] ? Hoa_Acceptance_States : Hoa_Acceptance_Transitions); - tgba_succ_iterator* j = aut->succ_iter(md.nm[i]); - j->first(); - os << "State: " << i; - if (this_acc == Hoa_Acceptance_States && !j->done()) - md.emit_acc(os, aut, j->current_acceptance_conditions()); + if (this_acc == Hoa_Acceptance_States) + { + acc_cond::mark_t acc = 0U; + for (auto& t: aut->out(i)) + { + acc = t.acc; + break; + } + md.emit_acc(os, aut, acc); + } os << nl; - for (; !j->done(); j->next()) + for (auto& t: aut->out(i)) { - const state* dst = j->current_state(); - os << '[' << md.sup[j->current_condition()] << "] " << md.sm[dst]; + os << '[' << md.sup[t.cond] << "] " << t.dst; if (this_acc == Hoa_Acceptance_Transitions) - md.emit_acc(os, aut, j->current_acceptance_conditions()); + md.emit_acc(os, aut, t.acc); os << nl; - dst->destroy(); } - aut->release_iter(j); } os << "--END--"; // No newline. Let the caller decide. return os; @@ -362,7 +338,12 @@ namespace spot break; } } - return hoa_reachable(os, aut, acceptance, alias, newline); + + auto a = std::dynamic_pointer_cast(aut); + if (!a) + a = make_tgba_digraph(aut, tgba::prop_set::all()); + + return hoa_reachable(os, a, acceptance, alias, newline); } } diff --git a/src/tgbatest/det.test b/src/tgbatest/det.test index edb617122..5b8b94676 100755 --- a/src/tgbatest/det.test +++ b/src/tgbatest/det.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -83,7 +83,7 @@ EOF # FIXME: we should improve this output cat >ex.hoa <<'EOF' HOA: v1 -States: 5 +States: 7 Start: 0 AP: 1 "a" acc-name: Buchi @@ -93,21 +93,25 @@ properties: trans-labels explicit-labels state-acc State: 0 [!0] 0 [0] 1 -[!0] 2 +[!0] 3 State: 1 [!0] 0 -[0] 3 -[!0] 2 -State: 2 {0} -[!0] 2 -State: 3 +[0] 2 +[!0] 3 +State: 2 [!0] 0 -[0] 3 -[!0] 2 -[0] 4 +[0] 2 +[!0] 3 +[0] 5 +State: 3 {0} +[!0] 3 State: 4 {0} -[!0] 2 -[0] 4 +[!0] 3 +State: 5 {0} +[!0] 3 +[0] 5 +State: 6 {0} +[t] 6 --END-- EOF diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test index 204c51f56..886f0ccc9 100755 --- a/src/tgbatest/hoaparse.test +++ b/src/tgbatest/hoaparse.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014 Laboratoire de Recherche et Développement de +# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -271,16 +271,16 @@ Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels state-acc complete deterministic --BODY-- State: 0 {0} -[!0&!1] 1 +[!0&!1] 2 [0&!1] 0 -[!0&1] 2 -[0&1] 2 -State: 1 {0} +[!0&1] 1 +[0&1] 1 +State: 1 {1} [!0&!1] 1 [0&!1] 1 [!0&1] 1 [0&1] 1 -State: 2 {1} +State: 2 {0} [!0&!1] 2 [0&!1] 2 [!0&1] 2 @@ -561,23 +561,23 @@ EOF expectok input <