diff --git a/NEWS b/NEWS index 832dfb571..599fcbe74 100644 --- a/NEWS +++ b/NEWS @@ -26,6 +26,10 @@ New in spot 2.5.3.dev (not yet released) tooltip in SVG figures when the mouse is over the acceptance condition. + - print_dot() has a new option "u" to hide "true states" behind + "exiting transitions". This can be used to display alternating + automata in a way many people expect. + - cleanup_parity() and cleanup_parity_here() are smarter and now remove from the acceptance condition the parity colors that are not used in the automaton. diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index b6b90008e..1a1eafadb 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -88,7 +88,7 @@ static const argp_option options[] = /**************************************************/ { nullptr, 0, nullptr, 0, "Output format:", 3 }, { "dot", 'd', - "1|a|A|b|B|c|C(COLOR)|e|f(FONT)|h|k|n|N|o|r|R|s|t|v|y|+INT|, int> univ_done; + std::vector true_states_; acc_cond::mark_t inf_sets_ = {}; acc_cond::mark_t fin_sets_ = {}; @@ -102,6 +103,7 @@ namespace spot bool opt_all_bullets = false; bool opt_ordered_edges_ = false; bool opt_numbered_edges_ = false; + bool opt_hide_true_states_ = false; bool opt_orig_show_ = false; bool max_states_given_ = false; // related to max_states_ bool opt_latex_ = false; @@ -130,6 +132,28 @@ namespace spot return max_states_given_; } + void find_true_states() + { + unsigned n = aut_->num_states(); + true_states_.resize(n, false); + auto& g = aut_->get_graph(); + auto& acc = aut_->acc(); + for (unsigned s = 0; s < n; ++s) + { + auto& ss = g.state_storage(s); + if (ss.succ == ss.succ_tail) + { + auto& es = g.edge_storage(ss.succ); + if (es.cond == bddtrue + + && es.src == es.dst + && acc.accepting(es.acc)) + true_states_[s] = true; + } + } + } + + void parse_opts(const char* options) { @@ -267,6 +291,9 @@ namespace spot case 's': opt_scc_ = true; break; + case 'u': + opt_hide_true_states_ = true; + break; case 'v': opt_vertical_ = true; break; @@ -430,6 +457,13 @@ namespace spot return tmp_dst.str(); } + template + void print_true_state(U to, V from) const + { + os_ << " T" << to << 'T' << from << " [label=\"\", style=invis, "; + os_ << (opt_vertical_ ? "height=0]\n" : "width=0]\n"); + } + void print_dst(int dst, bool print_edges = false, const char* style = nullptr, int color_num = -1) @@ -444,7 +478,15 @@ namespace spot { for (unsigned d: aut_->univ_dests(dst)) { - os_ << " " << dest << " -> " << d; + bool dst_is_hidden_true_state = + opt_hide_true_states_ && true_states_[d]; + if (dst_is_hidden_true_state) + print_true_state(d, dest); + os_ << " " << dest << " -> "; + if (dst_is_hidden_true_state) + os_ << 'T' << d << 'T' << dest; + else + os_ << d; if (style && *style) os_ << " [" << style << ']'; os_ << '\n'; @@ -679,11 +721,20 @@ namespace spot process_link(const twa_graph::edge_storage_t& t, int number, bool print_edges) { + bool dst_is_hidden_true_state = + (t.dst < true_states_.size()) && true_states_[t.dst]; + if (print_edges) { - os_ << " " << t.src << " -> " << (int)t.dst; + if (dst_is_hidden_true_state) + print_true_state(t.dst, t.src); + os_ << " " << t.src << " -> "; + if (dst_is_hidden_true_state) + os_ << 'T' << t.dst << 'T' << t.src; + else + os_ << (int)t.dst; if (aut_->is_univ_dest(t.dst) && highlight_edges_ - && !opt_shared_univ_dest_) + && !opt_shared_univ_dest_ && !dst_is_hidden_true_state) { auto idx = aut_->get_graph().index_of_edge(t); auto iter = highlight_edges_->find(idx); @@ -746,6 +797,8 @@ namespace spot void print(const const_twa_graph_ptr& aut) { aut_ = aut; + if (opt_hide_true_states_) + find_true_states(); sn_ = aut->get_named_prop>("state-names"); // We have no names. Do we have product sources? @@ -851,6 +904,8 @@ namespace spot } for (auto s: si->states_of(i)) { + if (opt_hide_true_states_ && true_states_[s]) + continue; process_state(s); int trans_num = 0; unsigned scc_of_s = si->scc_of(s); @@ -871,6 +926,8 @@ namespace spot unsigned ns = aut_->num_states(); for (unsigned n = 0; n < ns; ++n) { + if (opt_hide_true_states_ && true_states_[n]) + continue; if (!si || !si->reachable_state(n)) process_state(n); int trans_num = 0; diff --git a/tests/python/alternation.ipynb b/tests/python/alternation.ipynb index 1ffac2739..20d543ba7 100644 --- a/tests/python/alternation.ipynb +++ b/tests/python/alternation.ipynb @@ -7,233 +7,69 @@ "outputs": [], "source": [ "import spot\n", - "spot.setup(show_default='.ba')" + "from spot.jupyter import display_inline\n", + "spot.setup(show_default='.bav')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ - "These test cases for the `remove_alternation()` algorithm." + "# Support for alternating automata" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The following automata are what we will use as examples." ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "VWAA for FGa && GFb\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "-1\n", - "\n", - "\n", - "\n", - "\n", - "0->-1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "-1->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "-1->3\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "-4\n", - "\n", - "\n", - "\n", - "\n", - "1->-4\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "-4->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "-4->2\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "2->5\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "5->5\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "" - ], - "text/plain": [ - "" - ] - }, - "execution_count": 2, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ - "aut = spot.automaton('''\n", - "HOA: v1\n", - "tool: \"ltl3ba\" \"1.1.3\"\n", - "name: \"VWAA for FGa && GFb\"\n", - "States: 6\n", - "Start: 0\n", - "acc-name: co-Buchi\n", - "Acceptance: 1 Fin(0)\n", - "AP: 2 \"a\" \"b\"\n", - "properties: trans-labels explicit-labels state-acc univ-branch very-weak\n", - "--BODY--\n", - "State: 0 \"(FG(a) && GF(b))\"\n", - " [t] 3&1\n", - "State: 1 \"GF(b)\"\n", - " [(1)] 1\n", - " [(!1)] 2&1\n", - "State: 2 \"F(b)\" {0}\n", - " [(1)] 5\n", - " [(!1)] 2\n", - "State: 3 \"FG(a)\" {0}\n", - " [(0)] 4\n", - " [t] 3\n", - "State: 4 \"G(a)\"\n", - " [(0)] 4\n", - "State: 5 \"t\"\n", - " [t] 5\n", - "--END--\n", - "'''); aut.show('.1ab')" + "aut1, aut2, aut3, aut4, aut5 = spot.automata('''\n", + "HOA: v1 tool: \"ltl3ba\" \"1.1.3\" name: \"VWAA for FGa && GFb\" States: 6\n", + "Start: 0 acc-name: co-Buchi Acceptance: 1 Fin(0) AP: 2 \"a\" \"b\" properties:\n", + "trans-labels explicit-labels state-acc univ-branch very-weak --BODY--\n", + "State: 0 \"(FG(a) && GF(b))\" [t] 3&1 State: 1 \"GF(b)\" [(1)] 1 [(!1)]\n", + "2&1 State: 2 \"F(b)\" {0} [(1)] 5 [(!1)] 2 State: 3 \"FG(a)\" {0} [(0)] 4\n", + "[t] 3 State: 4 \"G(a)\" [(0)] 4 State: 5 \"t\" [t] 5 --END--\n", + "/* Example from ADL's PSL2TGBA talk. */\n", + "HOA: v1 States: 3 Start: 0 acc-name: co-Buchi Acceptance: 1 Fin(0) AP:\n", + "3 \"a\" \"b\" \"p\" --BODY-- State: 0 \"(a;a*;b)*\" {0} [0] 1 [!0] 2 State: 1\n", + "\"a*;b;(a;a*;b)*\" {0} [0&1&2] 0&1 [!1&2] 1 [!0&!1] 2 [!0&1&2] 0 State:\n", + "2 [t] 2 --END--\n", + "HOA: v1 States: 5 Start: 3 acc-name: co-Buchi Acceptance: 1 Fin(0) AP:\n", + "3 \"a\" \"b\" \"p\" --BODY-- State: 0 \"(a;a*;b)*\" {0} [0] 1 [!0] 2 State: 1\n", + "\"a*;b;(a;a*;b)*\" {0} [0&1&2] 0&1 [!1&2] 1 [!0&!1] 2 [!0&1&2] 0 State:\n", + "2 [t] 2 State: 3 [0] 4&0 State: 4 [t] 3 --END--\n", + "HOA: v1 States: 3 Start: 0 acc-name: co-Buchi Acceptance: 1 Fin(0) AP:\n", + "3 \"a\" \"b\" \"p\" --BODY-- State: 0 \"(a;a*;b)*\" {0} [0] 1 [!0] 2 State: 1\n", + "\"a*;b;(a;a*;b)*\" {0} [0&1&2] 0&1 [!1&2] 1 [!0&!1] 2 [!0&1&2] 0 State:\n", + "2 [t] 2 --END--\n", + "HOA: v1 tool: \"ltl3dra\" \"0.2.2\" name: \"VWAA for GFa\" States: 3 Start: 0\n", + "acc-name: co-Buchi Acceptance: 1 Fin(0) AP: 1 \"a\" properties: trans-labels\n", + "explicit-labels state-acc univ-branch very-weak --BODY-- State: 0 \"GF(a)\"\n", + "[t] 1&0 State: 1 \"F(a)\" {0} [(0)] 2 [t] 1 State: 2 \"t\" [t] 2 --END--\n", + "''')" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Various display options" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Here is the default output, using the `bav` options as set by default in the first cell. " ] }, { @@ -243,184 +79,643 @@ "outputs": [ { "data": { - "image/svg+xml": [ - "\n", + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "VWAA for FGa && GFb\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "(FG(a) && GF(b))\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "GF(b)\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "FG(a)\n", + "\n", + "\n", + "\n", + "\n", + "-1->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "\n", + "1->-4\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "G(a)\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "-4->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "F(b)\n", + "\n", + "\n", + "\n", + "\n", + "-4->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "t\n", + "\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "
\n", "\n", "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "(a;a*;b)*\n", + "\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1,3\n", + "\n", + "a*;b;(a;a*;b)*\n", + "\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "1,4\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", "\n", "\n", - "\n", + "\n", "1->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "\n", + "\n", + "!a & !b\n", "\n", - "\n", + "\n", "\n", - "3\n", - "\n", - "1,2,3\n", + "-1\n", + "\n", "\n", - "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "!b\n", - "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "I->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "\n", + "3->-4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "(a;a*;b)*\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "a*;b;(a;a*;b)*\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4->0\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "4\n", - "\n", - "1,2,4\n", + "\n", + "4\n", "\n", - "\n", + "\n", + "\n", + "-4->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "(a;a*;b)*\n", + "\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "a*;b;(a;a*;b)*\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", "\n", - "1->4\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "VWAA for GFa\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "GF(a)\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "F(a)\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "t\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n" + "\n", + "
" ], "text/plain": [ - " *' at 0x7fefe020aa20> >" + "" ] }, - "execution_count": 3, "metadata": {}, - "output_type": "execute_result" + "output_type": "display_data" } ], "source": [ - "aut2 = spot.remove_alternation(aut, True); aut2" + "display_inline(aut1, aut2, aut3, aut4, aut5)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "If the state labels take too much space, you can reduce the size of the automaton by forcing states to be numbered with option `1`. The original label is still displayed as a tooltip when the mouse is over the state." ] }, { @@ -430,166 +725,648 @@ "outputs": [ { "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "text/html": [ + "
\n", + "\n", + "VWAA for FGa && GFb\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", "\n", "\n", - "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1,3\n", + "\n", + "\n", + "1\n", + "\n", "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "1\n", "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "1,4\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "1,2,3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "!b\n", "\n", - "\n", - "\n", - "4\n", - "\n", - "1,2,4\n", + "\n", + "\n", + "-1->3\n", + "\n", + "\n", "\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "\n", + "-4\n", + "\n", "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "1->-4\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!b\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", "\n", "\n", - "\n", - "3->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "3->4\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "\n", + "-4->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", - "4->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", "\n", "\n", - "\n" + "
\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "I->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "\n", + "3->-4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "-4->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "VWAA for GFa\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "
" ], "text/plain": [ - " *' at 0x7fefe02e5f60> >" + "" ] }, - "execution_count": 4, "metadata": {}, - "output_type": "execute_result" + "output_type": "display_data" } ], "source": [ - "spot.scc_filter(aut2, True)" + "display_inline(aut1.show('.bav1'), aut2.show('.bav1'), aut3.show('.bav1'), aut4.show('.bav1'), aut5.show('.bav1'))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "When working with alternating automata, it is quite common to hide \"true states\", and display \"exiting transitions instead\". You can do that with option `u`." ] }, { @@ -599,147 +1376,585 @@ "outputs": [ { "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", + "text/html": [ + "
\n", + "\n", + "VWAA for FGa && GFb\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", - "\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "\n", + "1->-4\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "-4->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "\n", + "2->T5T2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", "\n", - "\n", - "1\n", - "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", + "\n", + "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", + "0->T2T0\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!b & p\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!b & p\n", "\n", "\n", "\n", "-1\n", - "\n", + "\n", "\n", "\n", "\n", "1->-1\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "\n", + "a & b & p\n", "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "1->T2T1\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "-1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "-1->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "" + "
\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "I->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "\n", + "3->-4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n", + "0->T2T0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "\n", + "1->T2T1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "-4->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n", + "0->T2T0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "\n", + "1->T2T1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "VWAA for GFa\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "1->T2T1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "
" ], "text/plain": [ - "" + "" ] }, - "execution_count": 5, "metadata": {}, - "output_type": "execute_result" + "output_type": "display_data" } ], "source": [ - "# Example from ADL's PSL2TGBA talk.\n", - "aut = spot.automaton('''\n", - "HOA: v1\n", - "States: 3\n", - "Start: 0\n", - "acc-name: co-Buchi\n", - "Acceptance: 1 Fin(0)\n", - "AP: 3 \"a\" \"b\" \"p\"\n", - "--BODY--\n", - "State: 0 \"(a;a*;b)*\" {0}\n", - " [0] 1\n", - " [!0] 2\n", - "State: 1 \"a*;b;(a;a*;b)*\" {0}\n", - " [0&1&2] 0&1\n", - " [!1&2] 1\n", - " [!0&!1] 2\n", - " [!0&1&2] 0\n", - "State: 2\n", - " [t] 2\n", - "--END--\n", - "'''); aut.show('.1ab')" + "display_inline(aut1.show('.bav1u'), aut2.show('.bav1u'), aut3.show('.bav1u'), aut4.show('.bav1u'), aut5.show('.bav1u'))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Let's make sure that option `u` and `s` (to display SCCs) work well together:" ] }, { @@ -749,147 +1964,641 @@ "outputs": [ { "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "text/html": [ + "
\n", + "\n", + "VWAA for FGa && GFb\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "\n", + "cluster_3\n", + "\n", + "\n", + "\n", + "cluster_4\n", + "\n", + "\n", + "\n", + "cluster_5\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "~0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", "\n", "\n", - "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", - "\n", - "\n", - "1\n", - "\n", - "~1\n", + "\n", + "\n", + "-1\n", + "\n", "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "{}\n", + "\n", + "\n", + "2\n", + "\n", + "\n", "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & b & p\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b & p\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "~1,~0\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & b & p\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b\n", "\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "\n", + "\n", + "2->T5T2\n", + "\n", + "\n", + "b\n", "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "a & !b & p\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", "\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "\n", + "1->-4\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "-4->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a\n", "\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->3\n", + "\n", + "\n", "\n", "\n", - "\n" + "
\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n", + "0->T2T0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "\n", + "1->T2T1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "I->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "\n", + "3->-4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n", + "0->T2T0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "\n", + "1->T2T1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "-4->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n", + "0->T2T0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "\n", + "1->T2T1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "VWAA for GFa\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "1->T2T1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "
" ], "text/plain": [ - " *' at 0x7fefe020ab40> >" + "" ] }, - "execution_count": 6, "metadata": {}, - "output_type": "execute_result" + "output_type": "display_data" } ], "source": [ - "spot.remove_alternation(aut, True)" + "display_inline(aut1.show('.bav1us'), aut2.show('.bav1us'), aut3.show('.bav1us'), \n", + " aut4.show('.bav1us'), aut5.show('.bav1us'))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Alternation removal" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The `remove_alternation()` function works on any alternating automaton that is weak (not necessarily very weak), i.e., in each SCC all transition should belong to the same accepting sets.\n", + "\n", + "The second argument of `remove_alternation()`, set to `True` below, simply asks for states to be labeled to help debugging. As the function builds Transition-based Generalized Büchi acceptance, it can be worthwhile to apply `scc_filter()` in an attempt to reduce the number of acceptance sets.\n", + "\n", + "The next cell shows this two-step process on our first example automaton." ] }, { @@ -899,193 +2608,494 @@ "outputs": [ { "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", + "text/html": [ + "
\n", + "\n", + "VWAA for FGa && GFb\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "I->3\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "-4\n", - "\n", - "\n", - "\n", - "\n", - "3->-4\n", - "\n", - "\n", - "a\n", - "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "\n", - "0\n", - "\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", + "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", + "-1->1\n", + "\n", + "\n", "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-1->3\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "!b & p\n", + "\n", + "\n", + "b\n", "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", + "\n", "\n", - "-1\n", - "\n", + "-4\n", + "\n", "\n", - "\n", - "\n", - "1->-1\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "\n", + "1->-4\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "-4->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4->2\n", + "\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "!b\n", "\n", - "\n", - "\n", - "-1->0\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "2->T5T2\n", + "\n", + "\n", + "b\n", "\n", - "\n", - "\n", - "-1->1\n", - "\n", - "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "\n", - "-4->0\n", - "\n", - "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1,3\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "1,4\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "1,2,3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", - "\n", + "\n", "4\n", - "\n", - "4\n", + "\n", + "1,2,4\n", "\n", - "\n", - "\n", - "-4->4\n", - "\n", - "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "" + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1,3\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "1,4\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "1,2,3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "1,2,4\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "
" ], "text/plain": [ - "" + "" ] }, - "execution_count": 7, "metadata": {}, - "output_type": "execute_result" + "output_type": "display_data" } ], "source": [ - "aut = spot.automaton('''\n", - "HOA: v1\n", - "States: 5\n", - "Start: 3\n", - "acc-name: co-Buchi\n", - "Acceptance: 1 Fin(0)\n", - "AP: 3 \"a\" \"b\" \"p\"\n", - "--BODY--\n", - "State: 0 \"(a;a*;b)*\" {0}\n", - " [0] 1\n", - " [!0] 2\n", - "State: 1 \"a*;b;(a;a*;b)*\" {0}\n", - " [0&1&2] 0&1\n", - " [!1&2] 1\n", - " [!0&!1] 2\n", - " [!0&1&2] 0\n", - "State: 2\n", - " [t] 2\n", - "State: 3\n", - " [0] 4&0\n", - "State: 4\n", - " [t] 3\n", - "--END--\n", - "'''); aut.show('.1ab')" + "nba1t = spot.remove_alternation(aut1, True)\n", + "nba1 = spot.scc_filter(nba1t, True)\n", + "display_inline(aut1.show('.bav1u'), nba1t, nba1)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Let's apply this process to the other 4 automata (which are not very-weak, unlike `aut1`). The states marked with `~` are part of a break-point construction." ] }, { @@ -1095,923 +3105,508 @@ "outputs": [ { "data": { - "image/svg+xml": [ - "\n", + "text/html": [ + "
\n", "\n", "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "3\n", + "\n", + "~0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "~0,4\n", + "\n", + "~1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "3,~1\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "4,~1,~0\n", - "\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "a & b & p\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "0,4,~1\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & !b & p\n", - "\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "a & !b & p\n", - "\n", - "\n", - "\n", - "5\n", - "\n", - "3,~0\n", - "\n", - "\n", - "\n", - "3->5\n", - "\n", - "\n", - "!a & b & p\n", - "\n", - "\n", - "\n", - "6\n", - "\n", - "3,~1,~0\n", - "\n", - "\n", - "\n", - "3->6\n", - "\n", - "\n", - "a & b & p\n", - "\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "a & !b & p\n", - "\n", - "\n", - "\n", - "4->5\n", - "\n", - "\n", - "!a & b & p\n", - "\n", - "\n", - "\n", - "4->6\n", - "\n", - "\n", - "a & b & p\n", - "\n", - "\n", - "\n", - "5->4\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "6->3\n", - "\n", - "\n", - "a & b & p\n", - "\n", - "\n", - "\n", - "6->4\n", - "\n", - "\n", - "a & !b & p\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7fefe021a990> >" - ] - }, - "execution_count": 8, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "spot.remove_alternation(aut, True)" - ] - }, - { - "cell_type": "code", - "execution_count": 9, - "metadata": {}, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "-7\n", - "\n", - "\n", - "\n", - "\n", - "I->-7\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "-7->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "-7->3\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "-4\n", - "\n", - "\n", - "\n", - "\n", - "3->-4\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & b & p\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b & p\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "-1\n", - "\n", - "\n", - "\n", - "\n", - "1->-1\n", - "\n", - "\n", - "a & b & p\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "-1->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "-1->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "-4->3\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "\n", - "-4->4\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "5\n", - "\n", - "5\n", - "\n", - "\n", - "\n", - "4->5\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "5->5\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "" - ], - "text/plain": [ - "" - ] - }, - "execution_count": 9, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "# Example from ADL's PSL2TGBA talk.\n", - "aut = spot.automaton('''\n", - "HOA: v1\n", - "States: 6\n", - "Start: 0&3\n", - "Acceptance: 1 Fin(0)\n", - "AP: 3 \"a\" \"b\" \"p\"\n", - "--BODY--\n", - "State: 0 \"(a;a*;b)*\" {0}\n", - " [0] 1\n", - " [!0] 2\n", - "State: 1 \"a*;b;(a;a*;b)*\" {0}\n", - " [0&1&2] 0&1\n", - " [!1&2] 1\n", - " [!0&!1] 2\n", - " [!0&1&2] 0\n", - "State: 2\n", - " [t] 2\n", - "State: 3\n", - " [0] 3\n", - " [!0] 3&4\n", - "State: 4 {0}\n", - " [!0] 4\n", - " [0] 5\n", - "State: 5\n", - " [t] 5\n", - "--END--\n", - "'''); aut.show('.1ab')" - ] - }, - { - "cell_type": "code", - "execution_count": 10, - "metadata": {}, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "~0,3\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "3,~1\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "3,4\n", + "\n", + "{}\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "a & !b & p\n", - "\n", + "\n", + "\n", + "!b & p\n", "\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "3,4,~1\n", - "\n", - "\n", "\n", - "1->4\n", - "\n", - "\n", - "!a & !b & p\n", - "\n", - "\n", - "\n", - "\n", - "5\n", - "\n", - "3,4,~0\n", - "\n", - "\n", - "\n", - "1->5\n", - "\n", - "\n", - "!a & b & p\n", - "\n", - "\n", - "\n", - "\n", - "6\n", - "\n", - "3,~1,~0\n", - "\n", - "\n", - "\n", - "1->6\n", - "\n", - "\n", - "a & b & p\n", - "\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!a\n", - "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "3\n", + "\n", + "~1,~0\n", "\n", - "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", "\n", - "2->3\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->1\n", - "\n", - "\n", - "a & !b & p\n", - "\n", - "\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!a & !b & p\n", - "\n", - "\n", - "\n", - "4->5\n", - "\n", - "\n", - "!a & b & p\n", - "\n", - "\n", - "\n", - "4->6\n", - "\n", - "\n", - "a & b & p\n", - "\n", - "\n", - "\n", - "\n", - "5->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "\n", - "5->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "\n", - "6->1\n", - "\n", - "\n", - "a & !b & p\n", - "\n", - "\n", - "\n", - "\n", - "6->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "6->5\n", - "\n", - "\n", - "!a & b & p\n", - "\n", - "\n", - "\n", - "\n", - "6->6\n", - "\n", - "\n", - "a & b & p\n", - "\n", + "3->1\n", + "\n", + "\n", + "a & !b & p\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7fefe020aed0> >" - ] - }, - "execution_count": 10, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "spot.remove_alternation(aut, True)" - ] - }, - { - "cell_type": "code", - "execution_count": 11, - "metadata": {}, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "VWAA for GFa\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "GF(a)\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "-1\n", - "\n", - "\n", - "\n", - "\n", - "0->-1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "-1->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "F(a)\n", - "\n", - "\n", - "\n", - "\n", - "-1->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "t\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7fefe022d630> >" - ] - }, - "execution_count": 11, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "a = spot.automaton('''\n", - "HOA: v1\n", - "tool: \"ltl3dra\" \"0.2.2\"\n", - "name: \"VWAA for GFa\"\n", - "States: 3\n", - "Start: 0\n", - "acc-name: co-Buchi\n", - "Acceptance: 1 Fin(0)\n", - "AP: 1 \"a\"\n", - "properties: trans-labels explicit-labels state-acc univ-branch very-weak\n", - "--BODY--\n", - "State: 0 \"GF(a)\"\n", - " [t] 1&0\n", - "State: 1 \"F(a)\" {0}\n", - " [(0)] 2\n", - " [t] 1\n", - "State: 2 \"t\"\n", - " [t] 2\n", - "--END--\n", - "'''); a" - ] - }, - { - "cell_type": "code", - "execution_count": 12, - "metadata": {}, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", + "\n", + "
\n", "\n", "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "3\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "0,1\n", + "\n", + "~0,4\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "3,~1\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "4,~1,~0\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "0,4,~1\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b & p\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b & p\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "3,~0\n", + "\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "3,~1,~0\n", + "\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "a & !b & p\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "6->4\n", + "\n", + "\n", + "a & !b & p\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "~0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "~1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "{}\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "~1,~0\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & !b & p\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", - "\n" + "\n", + "
" ], "text/plain": [ - " *' at 0x7fefe0279fc0> >" + "" ] }, - "execution_count": 12, "metadata": {}, - "output_type": "execute_result" + "output_type": "display_data" } ], "source": [ - "spot.remove_alternation(a, True)" + "nba2, nba3, nba4, nba5 = [spot.scc_filter(spot.remove_alternation(a, True), True) for a in (aut2, aut3, aut4, aut5)]\n", + "display_inline(nba2, nba3, nba4, nba5)" ] } ],