diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index 3f041ac1c..419b33fe3 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -836,54 +836,63 @@ namespace spot void pg_print(std::ostream& os, const const_twa_graph_ptr& arena) { - auto owner = ensure_parity_game(arena, "pg_print"); - // Ensure coloring - assert([&]() - { - bool max; - bool odd; - arena->acc().is_parity(max, odd, true); - return max && odd; - }() && "pg_printer needs max-odd parity"); - assert([&]() - { - for (unsigned ie = 0; ie < arena->num_edges(); ++ie) - { - const auto& es = arena->edge_storage(ie+1); - if (!es.acc) - return false; - } - return true; - }() && "Arena must be colorized"); + ensure_parity_game(arena, "pg_print"); - unsigned ns = arena->num_states(); - unsigned init = arena->get_init_state_number(); - os << "parity " << ns - 1 << ";\n"; - std::vector seen(ns, false); - std::vector todo({init}); - while (!todo.empty()) + auto do_print = [&os](const const_twa_graph_ptr& arena) { - unsigned src = todo.back(); - todo.pop_back(); - if (seen[src]) - continue; - seen[src] = true; - os << src << ' '; - os << arena->out(src).begin()->acc.max_set() - 1 << ' '; - os << (*owner)[src] << ' '; - bool first = true; - for (auto& e: arena->out(src)) + const region_t& owner = get_state_players(arena); + + unsigned ns = arena->num_states(); + unsigned init = arena->get_init_state_number(); + os << "parity " << ns - 1 << ";\n"; + std::vector seen(ns, false); + std::vector todo({init}); + while (!todo.empty()) { - if (!first) - os << ','; - first = false; - os << e.dst; - if (!seen[e.dst]) - todo.push_back(e.dst); + unsigned src = todo.back(); + todo.pop_back(); + if (seen[src]) + continue; + seen[src] = true; + os << src << ' '; + os << arena->out(src).begin()->acc.max_set() - 1 << ' '; + os << owner[src] << ' '; + bool first = true; + for (auto& e: arena->out(src)) + { + if (!first) + os << ','; + first = false; + os << e.dst; + if (!seen[e.dst]) + todo.push_back(e.dst); + } + if (src == init) + os << " \"INIT\""; + os << ";\n"; } - if (src == init) - os << " \"INIT\""; - os << ";\n"; + }; + // Ensure coloring + // PGSolver format expects max odd and colored + bool is_par, max, odd; + is_par = arena->acc().is_parity(max, odd, true); + assert(is_par && "pg_printer needs parity condition"); + bool is_colored = (max & odd) ? std::all_of(arena->edges().begin(), + arena->edges().end(), + [](const auto& e) + { + return (bool) e.acc; + }) + : false; + if (is_colored) + do_print(arena); + else + { + auto arena2 = change_parity(arena, parity_kind_max, parity_style_odd); + colorize_parity_here(arena2, true); + set_state_players(arena2, + get_state_players(arena)); + do_print(arena2); } } diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 5a5d1297a..41aa736e2 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -837,13 +837,10 @@ namespace spot if (force_sbacc) dpa = sbacc(dpa); reduce_parity_here(dpa, true); - change_parity_here(dpa, parity_kind_max, - parity_style_odd); assert(( [&dpa]() -> bool { bool max, odd; - dpa->acc().is_parity(max, odd); - return max && odd; + return dpa->acc().is_parity(max, odd); }())); assert(is_deterministic(dpa)); return dpa; @@ -936,7 +933,6 @@ namespace spot if (bv) sw.start(); dpa = split_2step(tmp, outs, true); - colorize_parity_here(dpa, true); if (bv) bv->split_time += sw.stop(); if (vs) @@ -959,7 +955,6 @@ namespace spot if (bv) sw.start(); dpa = split_2step(aut, outs, true); - colorize_parity_here(dpa, true); if (bv) bv->split_time += sw.stop(); if (vs) @@ -1031,8 +1026,6 @@ namespace spot if (bv) sw.start(); dpa = split_2step(dpa, outs, true); - change_parity_here(dpa, parity_kind_max, parity_style_odd); - colorize_parity_here(dpa, true); if (bv) bv->split_time += sw.stop(); if (vs) diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 9319d96a8..6cb449012 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -232,7 +232,7 @@ LAR construction done in X seconds DPA has 4 states, 1 colors split inputs and outputs done in X seconds automaton has 12 states -solving game with acceptance: parity max odd 3 +solving game with acceptance: co-Büchi game solved in X seconds EOF ltlsynt -f "G(Fi0 && Fi1 && Fi2) -> G(i1 <-> o0)" --outs="o0" --algo=lar \ @@ -708,7 +708,7 @@ LAR construction done in X seconds DPA has 4 states, 1 colors split inputs and outputs done in X seconds automaton has 9 states -solving game with acceptance: Streett 1 +solving game with acceptance: Büchi game solved in X seconds simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates @@ -727,7 +727,7 @@ LAR construction done in X seconds DPA has 2 states, 0 colors split inputs and outputs done in X seconds automaton has 4 states -solving game with acceptance: Streett 1 +solving game with acceptance: all game solved in X seconds simplification took X seconds trying to create strategy directly for (a | x) -> x @@ -738,7 +738,7 @@ LAR construction done in X seconds DPA has 2 states, 0 colors split inputs and outputs done in X seconds automaton has 4 states -solving game with acceptance: Streett 1 +solving game with acceptance: all game solved in X seconds simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates @@ -797,7 +797,7 @@ LAR construction done in X seconds DPA has 2 states, 1 colors split inputs and outputs done in X seconds automaton has 5 states -solving game with acceptance: Streett 1 +solving game with acceptance: Büchi game solved in X seconds simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates @@ -819,7 +819,7 @@ LAR construction done in X seconds DPA has 2 states, 0 colors split inputs and outputs done in X seconds automaton has 4 states -solving game with acceptance: Streett 1 +solving game with acceptance: all game solved in X seconds simplification took X seconds trying to create strategy directly for a -> c @@ -830,7 +830,7 @@ LAR construction done in X seconds DPA has 2 states, 0 colors split inputs and outputs done in X seconds automaton has 4 states -solving game with acceptance: Streett 1 +solving game with acceptance: all game solved in X seconds simplification took X seconds trying to create strategy directly for a -> d @@ -841,7 +841,7 @@ LAR construction done in X seconds DPA has 2 states, 0 colors split inputs and outputs done in X seconds automaton has 4 states -solving game with acceptance: Streett 1 +solving game with acceptance: all game solved in X seconds simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates @@ -903,7 +903,7 @@ LAR construction done in X seconds DPA has 1 states, 0 colors split inputs and outputs done in X seconds automaton has 2 states -solving game with acceptance: Streett 1 +solving game with acceptance: all game solved in X seconds translating formula done in X seconds automaton has 2 states and 2 colors @@ -911,7 +911,7 @@ LAR construction done in X seconds DPA has 2 states, 2 colors split inputs and outputs done in X seconds automaton has 5 states -solving game with acceptance: parity max odd 4 +solving game with acceptance: Streett 1 game solved in X seconds EOF @@ -927,7 +927,7 @@ ACD construction done in X seconds DPA has 2 states, 2 colors split inputs and outputs done in X seconds automaton has 6 states -solving game with acceptance: parity max odd 4 +solving game with acceptance: generalized-Streett 1 1 game solved in X seconds simplification took X seconds translating formula done in X seconds @@ -936,7 +936,7 @@ ACD construction done in X seconds DPA has 1 states, 0 colors split inputs and outputs done in X seconds automaton has 2 states -solving game with acceptance: Streett 1 +solving game with acceptance: all game solved in X seconds simplification took X seconds EOF @@ -959,7 +959,7 @@ LAR construction done in X seconds DPA has 1 states, 1 colors split inputs and outputs done in X seconds automaton has 3 states -solving game with acceptance: Streett 1 +solving game with acceptance: Büchi game solved in X seconds EOF ltlsynt -f "G(o1) & (GFi <-> GFo1)" --outs="o1" --verbose\ @@ -977,7 +977,7 @@ LAR construction done in X seconds DPA has 2 states, 2 colors split inputs and outputs done in X seconds automaton has 6 states -solving game with acceptance: parity max odd 4 +solving game with acceptance: Streett 1 game solved in X seconds simplification took X seconds EOF diff --git a/tests/python/_mealy.ipynb b/tests/python/_mealy.ipynb index 4e7374852..c2aeb125c 100644 --- a/tests/python/_mealy.ipynb +++ b/tests/python/_mealy.ipynb @@ -65,78 +65,70 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett 1]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a & !c\n", - "\n", + "\n", + "\n", + "!a & !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", + "\n", + "a | c\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", + "\n", + "\n", + "!b & !d\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "b | d\n", - "\n", + "\n", + "\n", + "b | d\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f32ec50ce40> >" + " *' at 0x7fc1244a3d50> >" ] }, "execution_count": 4, @@ -216,7 +208,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f32ec571c30> >" + " *' at 0x7fc124439570> >" ] }, "execution_count": 6, @@ -290,7 +282,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f32ec571c30> >" + " *' at 0x7fc124439570> >" ] }, "execution_count": 8, @@ -301,6 +293,14 @@ "source": [ "x" ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "923a59d6", + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -319,7 +319,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.9.2" + "version": "3.8.10" } }, "nbformat": 4, diff --git a/tests/python/games.ipynb b/tests/python/games.ipynb index ac3490b2b..891ebcd94 100644 --- a/tests/python/games.ipynb +++ b/tests/python/games.ipynb @@ -689,246 +689,230 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[parity max odd 3]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "I->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "4->10\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "4->11\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "5->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1->6\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "1->7\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "7->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "8->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "3->9\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "9->2\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "9->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "10->0\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "10->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "11->1\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "11->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f202420db10> >" + " *' at 0x7f657c403180> >" ] }, "execution_count": 8, @@ -963,43 +947,43 @@ "States: 12\n", "Start: 4\n", "AP: 2 \"b\" \"a\"\n", - "acc-name: parity max odd 3\n", - "Acceptance: 3 Fin(2) & (Inf(1) | Fin(0))\n", - "properties: trans-labels explicit-labels trans-acc colored complete\n", + "acc-name: co-Buchi\n", + "Acceptance: 1 Fin(0)\n", + "properties: trans-labels explicit-labels trans-acc complete\n", "properties: deterministic\n", "spot-state-player: 0 0 0 0 0 1 1 1 1 1 1 1\n", "controllable-AP: 0\n", "--BODY--\n", "State: 0\n", - "[!1] 5 {1}\n", - "[1] 6 {2}\n", + "[!1] 5\n", + "[1] 6 {0}\n", "State: 1\n", - "[1] 6 {2}\n", - "[!1] 7 {2}\n", + "[1] 6 {0}\n", + "[!1] 7 {0}\n", "State: 2\n", - "[t] 8 {1}\n", + "[t] 8\n", "State: 3\n", - "[t] 9 {1}\n", + "[t] 9\n", "State: 4\n", - "[!1] 10 {1}\n", - "[1] 11 {1}\n", + "[!1] 10\n", + "[1] 11\n", "State: 5\n", - "[t] 0 {1}\n", + "[t] 0\n", "State: 6\n", - "[t] 1 {2}\n", + "[t] 1 {0}\n", "State: 7\n", - "[t] 0 {2}\n", + "[t] 0 {0}\n", "State: 8\n", - "[t] 2 {1}\n", + "[t] 2\n", "State: 9\n", - "[!0] 2 {1}\n", - "[0] 3 {2}\n", + "[!0] 2\n", + "[0] 3 {0}\n", "State: 10\n", - "[!0] 0 {1}\n", - "[0] 3 {1}\n", + "[!0] 0\n", + "[0] 3\n", "State: 11\n", - "[!0] 1 {1}\n", - "[0] 3 {1}\n", + "[!0] 1\n", + "[0] 3\n", "--END--\n" ] } @@ -1049,246 +1033,230 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[parity max odd 3]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "I->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "4->10\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "4->11\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "5->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1->6\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "1->7\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "7->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "8->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "3->9\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "9->2\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "9->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "10->0\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "10->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "11->1\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "11->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f202420df90> >" + " *' at 0x7f658c612f30> >" ] }, "execution_count": 11, diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb index 08af437e2..3e8b4f5ea 100644 --- a/tests/python/synthesis.ipynb +++ b/tests/python/synthesis.ipynb @@ -59,644 +59,587 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[parity max odd 3]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "I->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "25\n", - "\n", - "25\n", + "\n", + "25\n", "\n", "\n", "\n", "9->25\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "26\n", - "\n", - "26\n", + "\n", + "26\n", "\n", "\n", "\n", "9->26\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "27\n", - "\n", - "27\n", + "\n", + "27\n", "\n", "\n", "\n", "9->27\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "28\n", - "\n", - "28\n", + "\n", + "28\n", "\n", "\n", "\n", "9->28\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "0->10\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "0->11\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "10->1\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "11->0\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "\n", "1->12\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", "\n", "\n", "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", "\n", "\n", "1->13\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", "\n", "\n", "\n", "12->1\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "13->0\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", "\n", "\n", "2->14\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", "\n", "\n", "\n", "16\n", - "\n", - "16\n", + "\n", + "16\n", "\n", "\n", "\n", "2->16\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "14->15\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "16->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "3->13\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", "\n", "\n", "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", "\n", "\n", "3->17\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", "\n", "\n", "\n", "17->2\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "17->3\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "4->14\n", - "\n", - "\n", - "i0\n", - "\n", + "\n", + "\n", + "i0\n", "\n", "\n", "\n", "18\n", - "\n", - "18\n", + "\n", + "18\n", "\n", "\n", "\n", "4->18\n", - "\n", - "\n", - "!i0\n", - "\n", + "\n", + "\n", + "!i0\n", "\n", "\n", "\n", "18->4\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "5->14\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "5->16\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "5->18\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", "\n", "\n", "5->19\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "19->5\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "6->11\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", "\n", "6->20\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "21\n", - "\n", - "21\n", + "\n", + "21\n", "\n", "\n", "\n", "6->21\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "20->4\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "20->7\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "21->4\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "21->6\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "7->12\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "7->13\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "22\n", - "\n", - "22\n", + "\n", + "22\n", "\n", "\n", "\n", "7->22\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "23\n", - "\n", - "23\n", + "\n", + "23\n", "\n", "\n", "\n", "7->23\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "22->4\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "22->7\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "23->4\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "23->6\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->13\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "8->17\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "8->23\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "24\n", - "\n", - "24\n", + "\n", + "24\n", "\n", "\n", "\n", "8->24\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "24->5\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "24->8\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "25->8\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "26->3\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "27->6\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "28->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f01fc12f030> >" + " *' at 0x7fc9680c32d0> >" ] }, "metadata": {}, @@ -743,583 +686,526 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[parity max odd 3]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "I->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "25\n", - "\n", - "25\n", + "\n", + "25\n", "\n", "\n", "\n", "9->25\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "26\n", - "\n", - "26\n", + "\n", + "26\n", "\n", "\n", "\n", "9->26\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "27\n", - "\n", - "27\n", + "\n", + "27\n", "\n", "\n", "\n", "9->27\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "28\n", - "\n", - "28\n", + "\n", + "28\n", "\n", "\n", "\n", "9->28\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "0->10\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "0->11\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "10->1\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "11->0\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "\n", "1->12\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", "\n", "\n", "1->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "12->1\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "13->0\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", "\n", "\n", "2->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "16\n", - "\n", - "16\n", + "\n", + "16\n", "\n", "\n", "\n", "2->16\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "14->15\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "16->2\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "3->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", "\n", "\n", "3->17\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "17->2\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "17->3\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "4->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "18\n", - "\n", - "18\n", + "\n", + "18\n", "\n", "\n", "\n", "4->18\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "18->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "5->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5->16\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5->18\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", "\n", "\n", "5->19\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "19->5\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6->11\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", "\n", "6->20\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "21\n", - "\n", - "21\n", + "\n", + "21\n", "\n", "\n", "\n", "6->21\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "20->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "20->7\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "21->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "21->6\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->12\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "22\n", - "\n", - "22\n", + "\n", + "22\n", "\n", "\n", "\n", "7->22\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "23\n", - "\n", - "23\n", + "\n", + "23\n", "\n", "\n", "\n", "7->23\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "22->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "22->7\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "23->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "23->6\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->17\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->23\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "24\n", - "\n", - "24\n", + "\n", + "24\n", "\n", "\n", "\n", "8->24\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "24->5\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "24->8\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "25->8\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "26->3\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "27->6\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "28->0\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -1668,7 +1554,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f01fc1b5f00> >" + " *' at 0x7fc9682230f0> >" ] }, "metadata": {}, @@ -1855,7 +1741,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f01fc12fd80> >" + " *' at 0x7fc968069180> >" ] }, "metadata": {}, @@ -1992,7 +1878,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f01fc1b5bd0> >" + " *' at 0x7fc968069210> >" ] }, "metadata": {}, @@ -2085,7 +1971,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f01fc1b5cc0> >" + " *' at 0x7fc968069180> >" ] }, "metadata": {}, @@ -2178,7 +2064,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f01fc2a8b70> >" + " *' at 0x7fc968069210> >" ] }, "metadata": {}, @@ -2315,7 +2201,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f01fc1b5de0> >" + " *' at 0x7fc968069060> >" ] }, "metadata": {}, @@ -2715,7 +2601,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2879,56 +2765,52 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett 1]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "I->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "i0\n", - "\n", + "\n", + "\n", + "i0\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "3->7\n", - "\n", - "\n", - "!i0\n", - "\n", + "\n", + "\n", + "!i0\n", "\n", "\n", "\n", @@ -2948,7 +2830,7 @@ "\n", "\n", "1\n", - "\n", + "\n", "\n", "\n", "\n", @@ -2956,7 +2838,7 @@ "\n", "\n", "1\n", - "\n", + "\n", "\n", "\n", "\n", @@ -2976,7 +2858,7 @@ "\n", "\n", "1\n", - "\n", + "\n", "\n", "\n", "\n", @@ -2984,51 +2866,47 @@ "\n", "\n", "!o0\n", - "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "6->0\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "7->1\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f01fc14bb10> >" + " *' at 0x7fc968143d80> >" ] }, "metadata": {}, @@ -3145,7 +3023,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f01fc12f090> >" + " *' at 0x7fc9680c3330> >" ] }, "metadata": {}, @@ -3378,7 +3256,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3507,7 +3385,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3559,72 +3437,64 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett 1]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", - "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", - "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", @@ -3634,72 +3504,64 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett 1]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", - "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", - "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "o1\n", - "\n", + "\n", + "\n", + "o1\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "!o1\n", - "\n", + "\n", + "\n", + "!o1\n", "\n", "\n", "\n", @@ -3939,7 +3801,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4004,7 +3866,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f01fc14bae0> >" + " *' at 0x7fc968143bd0> >" ] }, "metadata": {}, @@ -4117,7 +3979,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4297,7 +4159,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4421,7 +4283,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f01fc1b5f90> >" + " *' at 0x7fc968069ed0> >" ] }, "execution_count": 16, diff --git a/tests/python/synthesis.py b/tests/python/synthesis.py index 559dc2d24..98ac889d8 100644 --- a/tests/python/synthesis.py +++ b/tests/python/synthesis.py @@ -35,18 +35,18 @@ tc.assertEqual(game.to_str(), """HOA: v1 States: 3 Start: 0 AP: 1 "a" -acc-name: Streett 1 -Acceptance: 2 Fin(0) | Inf(1) -properties: trans-labels explicit-labels trans-acc colored complete +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc complete properties: deterministic spot-state-player: 0 1 1 controllable-AP: --BODY-- State: 0 -[!0] 1 {0} -[0] 2 {1} +[!0] 1 +[0] 2 {0} State: 1 -[t] 0 {0} +[t] 0 State: 2 -[t] 0 {1} +[t] 0 {0} --END--""")