From c25a67b00dbfd1ab3f7a1d210ea71b970bc26a52 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Feb 2019 15:29:37 +0100 Subject: [PATCH] polish previous two patches * NEWS: Update. * spot/twaalgos/genem.cc, spot/twaalgos/genem.hh, spot/twa/twa.cc: Update copyright years. * spot/twa/twa.hh: Update Doxygen documentation. * spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Simplify data structures, and fix failure of get_accepting_run() to compute accepting runs in SCC that are accepting due to the self-loop optimization of scc_info. * tests/python/highlighting.ipynb: Add three test cases. --- NEWS | 8 +- spot/twa/twa.cc | 2 +- spot/twa/twa.hh | 68 +-- spot/twaalgos/genem.cc | 5 +- spot/twaalgos/genem.hh | 2 +- spot/twaalgos/sccinfo.cc | 180 ++++--- spot/twaalgos/sccinfo.hh | 6 +- tests/python/highlighting.ipynb | 878 ++++++++++++++++++++++++++++++-- 8 files changed, 1007 insertions(+), 142 deletions(-) diff --git a/NEWS b/NEWS index d916a7795..f8102a861 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,12 @@ New in spot 2.7.1.dev (not yet released) - Nothing yet. + Library: + + - Add generic_accepting_run() as a variant of generic_emptiness_check() that + returns an accepting run in an automaton with any acceptance condition. + + - twa::accepting_run() now works on automata using Fin in + their acceptance condition. New in spot 2.7.1 (2019-02-14) diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index 55de28205..4a8d23c4f 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014-2018 Laboratoire de Recherche et Developpement de +// Copyright (C) 2011, 2014-2019 Laboratoire de Recherche et Developpement de // l'EPITA (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 84e3cbf68..b3c7454ee 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2013-2018 Laboratoire de Recherche et +// Copyright (C) 2009, 2011, 2013-2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -828,35 +828,45 @@ namespace spot /// /// If you are calling this method on a product of two automata, /// consider using intersects() instead. + /// + /// Note that if the input automaton uses Fin-acceptance, the + /// emptiness check is not performed on-the-fly. Any on-the-fly + /// automaton would be automatically copied into a twa_graph_ptr + /// first. virtual bool is_empty() const; /// \brief Return an accepting run if one exists. /// - /// Note that this method currently only works for Fin-less - /// acceptance. For acceptance conditions that contain Fin - /// acceptance, you can either rely on is_empty() and not use any - /// accepting run, or remove Fin acceptance using remove_fin() and - /// compute an accepting run on that larger automaton. - /// /// Return nullptr if no accepting run were found. /// /// If you are calling this method on a product of two automata, /// consider using intersecting_run() instead. + /// + /// Note that if the input automaton uses Fin-acceptance, this + /// computation is not performed on-the-fly. Any on-the-fly + /// automaton would be automatically copied into a twa_graph_ptr + /// first. virtual twa_run_ptr accepting_run() const; /// \brief Return an accepting word if one exists. /// - /// Note that this method DOES works with Fin - /// acceptance. - /// /// Return nullptr if no accepting word were found. /// /// If you are calling this method on a product of two automata, /// consider using intersecting_word() instead. + /// + /// Note that if the input automaton uses Fin-acceptance, this + /// computation is not performed on-the-fly. Any on-the-fly + /// automaton would be automatically copied into a twa_graph_ptr + /// first. virtual twa_word_ptr accepting_word() const; /// \brief Check whether the language of this automaton intersects /// that of the \a other automaton. + /// + /// An emptiness check is performed on a product computed + /// on-the-fly, unless some of the operands use Fin-acceptance: in + /// this case an explicit product is performed. virtual bool intersects(const_twa_ptr other) const; /// \brief Return an accepting run recognizing a word accepted by @@ -864,52 +874,42 @@ namespace spot /// /// If \a from_other is true, the returned run will be over the /// \a other automaton. Otherwise, the run will be over this - /// automaton. - /// - /// Note that this method currently only works if the automaton - /// from which the accepting run is extracted uses Fin-less acceptance. - /// (The other automaton can have any acceptance condition.) - /// - /// For acceptance conditions that contain Fin acceptance, you can - /// either rely on intersects() and not use any accepting run, or - /// remove Fin acceptance using remove_fin() and compute an - /// intersecting run on this larger automaton. + /// automaton. (This argument will be deprecated soon, do not + /// use it.) /// /// Return nullptr if no accepting run were found. + /// + /// An emptiness check is performed on a product computed + /// on-the-fly, unless some of the operands use Fin-acceptance: in + /// this case an explicit product is performed. virtual twa_run_ptr intersecting_run(const_twa_ptr other, bool from_other = false) const; - /// \brief Return a word accepted by two automata. /// - /// Note that this method DOES works with Fin - /// acceptance. - /// /// Return nullptr if no accepting word were found. virtual twa_word_ptr intersecting_word(const_twa_ptr other) const; /// \brief Return an accepting run recognizing a word accepted by /// exactly one of the two automata. /// - /// If \a from_other is true, the returned run will be over the - /// \a other automaton. Otherwise, the run will be over this - /// automaton. - /// - /// Note that this method currently only works if the automaton - /// from which the accepting run is extracted uses Fin-less acceptance. - /// (The other automaton can have any acceptance condition.) - /// /// Return nullptr iff the two automata recognize the same /// language. + /// + /// This methods needs to complement at least one automaton (if + /// lucky) or maybe both automata. It will therefore be more + /// efficient on deterministic automata. virtual twa_run_ptr exclusive_run(const_twa_ptr other) const; /// \brief Return a word accepted by exactly one of the two /// automata. /// - /// Note that this method DOES works with Fin acceptance. - /// /// Return nullptr iff the two automata recognize the same /// language. + /// + /// This methods needs to complement at least one automaton (if + /// lucky) or maybe both automata. It will therefore be more + /// efficient on deterministic automata. virtual twa_word_ptr exclusive_word(const_twa_ptr other) const; private: diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index 3258bf8c7..c1fe01815 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018 Laboratoire de Recherche et Developpement +// Copyright (C) 2017-2019 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -255,12 +255,9 @@ namespace spot "does not support alternating automata"); auto aut_ = std::const_pointer_cast(aut); acc_cond old = aut_->acc(); - twa_run_ptr run = std::make_shared(aut_); bool res = generic_emptiness_check_main_nocopy(aut_, run); - aut_->set_acceptance(old); - if (!res) return run; return nullptr; diff --git a/spot/twaalgos/genem.hh b/spot/twaalgos/genem.hh index 2f8a625f7..525f73b09 100644 --- a/spot/twaalgos/genem.hh +++ b/spot/twaalgos/genem.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018 Laboratoire de Recherche et Developpement +// Copyright (C) 2017-2019 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index bd9335c55..2bb344d74 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -48,6 +48,13 @@ namespace spot ("scc_info was run with option STOP_ON_ACC"); } + // this one is not yet needed in the hh file + static void report_need_stop_on_acc() + { + throw std::runtime_error + ("scc_info was not run with option STOP_ON_ACC"); + } + namespace { struct scc @@ -461,88 +468,128 @@ namespace spot determine_usefulness(); } - // Describes an explicit spot::twa_run::step - struct exp_step - { - unsigned src; - bdd cond; - acc_cond::mark_t acc; - }; - // A reimplementation of spot::bfs_steps for explicit automata. // bool filter(const twa_graph::edge_storage_t&) returns true if the // transition has to be filtered out. - // bool match(struct exp_step&, unsigned dest) returns true if the BFS has to - // stop after this transition. + // bool match(const twa_graph::edge_storage_t&) returns true if the BFS + // has to stop after this transition. // Returns the destination of the matched transition, or -1 if no match has // been found. + template static int explicit_bfs_steps(const const_twa_graph_ptr aut, unsigned start, - twa_run::steps& steps, - std::function filter, - std::function match) + twa_run::steps& steps, + edge_filter_type filter, + step_matcher_type match) { - std::unordered_map backlinks; + auto& gr = aut->get_graph(); + // The backlink of each state is the index of the edge that + // discovered it in the BFS, so BACKLINKS effectively describes a + // tree rooted at START. + std::vector backlinks(aut->num_states(), 0); std::deque bfs_queue; bfs_queue.emplace_back(start); - while (!bfs_queue.empty()) - { - unsigned src = bfs_queue.front(); - bfs_queue.pop_front(); - for (auto& t: aut->out(src)) { - if (filter(t)) - continue; - - exp_step s = { src, t.cond, t.acc }; - if (match(s, t.dst)) - { - twa_run::steps path; - for (;;) + unsigned src = bfs_queue.front(); + bfs_queue.pop_front(); + for (auto& t: aut->out(src)) { - path.emplace_front(aut->state_from_number(s.src), s.cond, s.acc); - if (s.src == start) - break; - const auto& i = backlinks.find(s.src); - assert(i != backlinks.end()); - s = i->second; - } - steps.splice(steps.end(), path); - return t.dst; - } + if (filter(t)) + continue; - if (backlinks.emplace(t.dst, s).second) - bfs_queue.push_back(t.dst); + if (match(t)) + { + // Build the path from START to T.DST by following the + // backlinks, starting at the end. + twa_run::steps path; + path.emplace_front(aut->state_from_number(t.src), + t.cond, t.acc); + unsigned src = t.src; + while (src != start) + { + unsigned bl_num = backlinks[src]; + assert(bl_num); + auto& bl_edge = gr.edge_storage(bl_num); + src = bl_edge.src; + path.emplace_front(aut->state_from_number(src), + bl_edge.cond, bl_edge.acc); + } + steps.splice(steps.end(), path); + return t.dst; + } + + if (!backlinks[t.dst]) + { + backlinks[t.dst] = aut->edge_number(t); + bfs_queue.push_back(t.dst); + } + } } - } return -1; } void scc_info::get_accepting_run(unsigned scc, twa_run_ptr r) const { const scc_info::scc_node& node = node_[scc]; - if (!node.is_accepting()) throw std::runtime_error("scc_info::get_accepting_cycle needs to be " "called on an accepting scc"); - acc_cond actual_cond = aut_->acc().restrict_to(node.acc_marks()) - .force_inf(node.acc_marks()); - assert(!actual_cond.uses_fin_acceptance()); + if (SPOT_UNLIKELY(!(options_ & scc_info_options::STOP_ON_ACC))) + report_need_stop_on_acc(); + + unsigned init = aut_->get_init_state_number(); + + // The accepting cycle should honor any edge filter we have. + auto filter = [this](const twa_graph::edge_storage_t& t) + { + if (!filter_) + return false; + // Filter out ignored and cut transitions. + return filter_(t, t.dst, filter_data_) + != edge_filter_choice::keep; + }; + + // The SCC exploration has a small optimization that can flag SCCs + // has accepting if they contain accepting self-loops, even if the + // SCC itself has some Fin acceptance to check. So we have to + // deal with this situation before we look for the more complex + // case of satisfying the condition with a larger cycle. We do + // this first, because it's good to return a small cycle if we + // can. + const acc_cond& acccond = aut_->acc(); + for (unsigned s: node.states()) + for (auto& e: aut_->out(s)) + if (e.src == e.dst && !filter(e) && acccond.accepting(e.acc)) + { + // We have found an accepting self-loop. That's the cycle + // part of our accepting run. + r->cycle.clear(); + r->cycle.emplace_front(aut_->state_from_number(e.src), + e.cond, e.acc); + // Add the prefix. + r->prefix.clear(); + if (e.src != init) + explicit_bfs_steps(aut_, init, r->prefix, + [](const twa_graph::edge_storage_t&) + { + return false; // Do not filter. + }, + [&](const twa_graph::edge_storage_t& t) + { + return t.dst == e.src; + }); + return; + } - // List of states of the SCC - const std::set scc_states(node.states().cbegin(), - node.states().cend()); // Prefix search r->prefix.clear(); - - int init = aut_->get_init_state_number(); int substart; - - if (scc_states.find(init) != scc_states.end()) + if (scc_of(init) == scc) { - // The initial state is in the SCC + // The initial state is in the target SCC: no prefix needed. substart = init; } else @@ -552,19 +599,21 @@ namespace spot { return false; // Do not filter. }, - [&](exp_step&, unsigned dst) + [&](const twa_graph::edge_storage_t& t) { // Match any state in the SCC. - return scc_states.find(dst) != scc_states.end(); + return scc_of(t.dst) == scc; }); } const unsigned start = (unsigned)substart; // Cycle search - + acc_cond actual_cond = acccond.restrict_to(node.acc_marks()) + .force_inf(node.acc_marks()); + assert(!actual_cond.uses_fin_acceptance()); + assert(!actual_cond.is_f()); acc_cond::mark_t acc_to_see = actual_cond.accepting_sets(node.acc_marks()); - r->cycle.clear(); do @@ -572,21 +621,16 @@ namespace spot substart = explicit_bfs_steps(aut_, substart, r->cycle, [&](const twa_graph::edge_storage_t& t) { - if (scc_states.find(t.dst) == scc_states.end()) - return true; // Destination is not in the SCC. - if (filter_) - // Filter out ignored and cut transitions. - return filter_(t, t.dst, filter_data_) - != edge_filter_choice::keep; - return false; + // Stay in the specified SCC. + return scc_of(t.dst) != scc || filter(t); }, - [&](exp_step& st, unsigned dst) + [&](const twa_graph::edge_storage_t& t) { if (!acc_to_see) // We have seen all the marks, go back to start. - return dst == start; - if (st.acc & acc_to_see) + return t.dst == start; + if (t.acc & acc_to_see) { - acc_to_see -= st.acc; + acc_to_see -= t.acc; return true; } return false; diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index b114823fd..9ccf58a2b 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -598,7 +598,11 @@ namespace spot /// \brief Retrieves an accepting run of the automaton whose cycle is in the /// SCC. + /// /// \param scc an accepting scc + /// \param r a run to fill + /// + /// This method needs the STOP_ON_ACC option. void get_accepting_run(unsigned scc, twa_run_ptr r) const; bool is_useful_scc(unsigned scc) const diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 8a558e773..06df171ab 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -240,7 +240,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc2846aa7b0> >" + " *' at 0x7f55b80ee2a0> >" ] }, "execution_count": 4, @@ -352,7 +352,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc2846aa780> >" + " *' at 0x7f55b8012060> >" ] }, "execution_count": 5, @@ -462,7 +462,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc2846aa7b0> >" + " *' at 0x7f55b80ee2a0> >" ] }, "execution_count": 6, @@ -695,7 +695,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc2845d2720> >" + " *' at 0x7f55b8012840> >" ] }, "execution_count": 8, @@ -890,7 +890,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc2845d2720> >" + " *' at 0x7f55b8012840> >" ] }, "execution_count": 11, @@ -902,6 +902,820 @@ "b" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Highlighting an accepting run in an automaton with arbitrary acceptance\n", + "\n", + "This is not as easy as finding accepting runs in (generalized) Büchi automata, so let's have a few example for testing." + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "❶\n", + ") | (Fin(\n", + "⓿\n", + ") & Inf(\n", + "❹\n", + ")) | Fin(\n", + "❷\n", + ")) & Fin(\n", + "❸\n", + ")\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b\n", + "❸\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "0->9\n", + "\n", + "\n", + "a & b\n", + "❸\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "9->5\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "9->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "9->8\n", + "\n", + "\n", + "a & b\n", + "❸\n", + "\n", + "\n", + "\n", + "5->0\n", + "\n", + "\n", + "!a & !b\n", + "❸\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "!a & !b\n", + "❸\n", + "\n", + "\n", + "\n", + "1->9\n", + "\n", + "\n", + "a & !b\n", + "❹\n", + "\n", + "\n", + "\n", + "1->8\n", + "\n", + "\n", + "a & b\n", + "❸\n", + "\n", + "\n", + "\n", + "8->9\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "8->7\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "2->8\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "❸\n", + "\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "!a & b\n", + "❷\n", + "❹\n", + "\n", + "\n", + "\n", + "2->7\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "6->2\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "❶\n", + "❸\n", + "❹\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "a & b\n", + "❷\n", + "\n", + "\n", + "\n", + "7->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", + "❷\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "❹\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !b\n", + "❶\n", + "❸\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", + "\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "a & !b\n", + "❷\n", + "\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f55b802f5d0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "❺\n", + ") & ((Fin(\n", + "❶\n", + ") & (Inf(\n", + "❸\n", + ") | Inf(\n", + "❹\n", + "))) | (Fin(\n", + "⓿\n", + ")|Fin(\n", + "❷\n", + ")))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "0->8\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + "a & !b\n", + "❷\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "8->3\n", + "\n", + "\n", + "a & !b\n", + "❹\n", + "❺\n", + "\n", + "\n", + "\n", + "6->8\n", + "\n", + "\n", + "a & !b\n", + "❶\n", + "❷\n", + "❺\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "!a & b\n", + "❸\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "1->9\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", + "❹\n", + "❺\n", + "\n", + "\n", + "\n", + "9->1\n", + "\n", + "\n", + "a & b\n", + "❹\n", + "\n", + "\n", + "\n", + "9->3\n", + "\n", + "\n", + "!a & b\n", + "❶\n", + "❷\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "9->5\n", + "\n", + "\n", + "a & !b\n", + "❷\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b\n", + "❷\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & b\n", + "❸\n", + "❺\n", + "\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", + "❷\n", + "\n", + "\n", + "\n", + "4->9\n", + "\n", + "\n", + "a & !b\n", + "❷\n", + "\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "a & b\n", + "❺\n", + "\n", + "\n", + "\n", + "7->2\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "\n", + "\n", + "\n", + "7->5\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "!a & b\n", + "❷\n", + "❸\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f55b802f5d0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "i G F a G F b\n", + "\n", + "(Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")) | (Fin(\n", + "❷\n", + ") & Inf(\n", + "❸\n", + "))\n", + "[Rabin 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "❶\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "❶\n", + "❸\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "⓿\n", + "❸\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f55b802f630> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "def show_accrun(string):\n", + " aut = spot.automaton(string)\n", + " run = aut.accepting_run()\n", + " run.highlight(5)\n", + " display(aut)\n", + "\n", + "show_accrun(\"\"\"\n", + "HOA: v1 States: 10 Start: 0 AP: 2 \"a\" \"b\" Acceptance: 5 (Inf(1) | (Fin(0)\n", + "& Inf(4)) | Fin(2)) & Fin(3) properties: trans-labels explicit-labels\n", + "trans-acc --BODY-- State: 0 [0&1] 9 {3} [!0&!1] 0 {3} [0&!1] 5 {0 1} State:\n", + "1 [0&!1] 9 {4} [0&1] 8 {3} State: 2 [!0&!1] 8 {0} [!0&1] 6 {2 4} [0&1]\n", + "2 {3} [!0&1] 7 State: 3 [0&!1] 2 {0 4} [!0&!1] 3 {1 3} [!0&1] 4 {0} State: 4\n", + "[0&!1] 5 {2} [0&1] 0 [!0&1] 1 {0} State: 5 [!0&!1] 0 {3} [!0&!1] 6 {3} State: 6\n", + "[0&1] 3 {2} [!0&1] 1 [0&1] 2 {0 1 3 4} State: 7 [0&1] 1 [!0&1] 7 {0 2}\n", + "State: 8 [!0&1] 7 [!0&!1] 9 {0} State: 9 [0&1] 8 {3} [0&!1] 5 [0&!1]\n", + "1 --END--\n", + "\"\"\")\n", + "show_accrun(\"\"\"\n", + "HOA: v1 States: 10 Start: 0 AP: 2 \"a\" \"b\" Acceptance: 6 Fin(5) &\n", + "((Fin(1) & (Inf(3) | Inf(4))) | Fin(0) | Fin(2)) properties: trans-labels\n", + "explicit-labels trans-acc --BODY-- State: 0 [0&1] 8 {0} [0&!1] 6 {2}\n", + "State: 1 [!0&1] 9 {0 4 5} State: 2 [!0&1] 1 State: 3 [0&!1] 3 {2}\n", + "[0&1] 4 {3 5} State: 4 [0&1] 7 {5} [0&!1] 9 {2} [!0&1] 0 {0 2} State:\n", + "5 [!0&1] 1 [!0&1] 3 {2 3} State: 6 [0&!1] 8 {1 2 5} [!0&1] 7 {3} State:\n", + "7 [0&1] 2 {0} [!0&1] 5 State: 8 [0&!1] 3 {4 5} State: 9 [!0&1] 3 {1 2}\n", + "[0&1] 1 {4} [0&!1] 5 {2} --END--\"\"\")\n", + "show_accrun(\"\"\"\n", + "HOA: v1 States: 4 properties: implicit-labels trans-labels no-univ-branch\n", + "deterministic complete tool: \"ltl2dstar\" \"0.5.4\" name: \"i G F a G F b\"\n", + "comment: \"Union{Safra[NBA=2],Safra[NBA=2]}\" acc-name: Rabin 2 Acceptance:\n", + "4 (Fin(0)&Inf(1))|(Fin(2)&Inf(3)) Start: 0 AP: 2 \"a\" \"b\" --BODY-- State:\n", + "0 {0} 1 0 3 2 State: 1 {1} 1 0 3 2 State: 2 {0 3} 1 0 3 2 State: 3 {1 3}\n", + "1 0 3 2 --END--\n", + "\"\"\")" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -913,7 +1727,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 13, "metadata": {}, "outputs": [ { @@ -975,7 +1789,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc2845e4f00> >" + " *' at 0x7f55b802f720> >" ] }, "metadata": {}, @@ -1030,7 +1844,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc2845e4e40> >" + " *' at 0x7f55b802f3f0> >" ] }, "metadata": {}, @@ -1045,7 +1859,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 14, "metadata": {}, "outputs": [ { @@ -1124,10 +1938,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fc2845d2600> >" + " *' at 0x7f55b8089e40> >" ] }, - "execution_count": 13, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -1138,7 +1952,7 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 15, "metadata": {}, "outputs": [ { @@ -1161,7 +1975,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 16, "metadata": {}, "outputs": [], "source": [ @@ -1174,7 +1988,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 17, "metadata": {}, "outputs": [ { @@ -1253,7 +2067,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc2845d2600> >" + " *' at 0x7f55b8089e40> >" ] }, "metadata": {}, @@ -1318,7 +2132,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc2845e4f00> >" + " *' at 0x7f55b802f720> >" ] }, "metadata": {}, @@ -1373,7 +2187,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc2845e4e40> >" + " *' at 0x7f55b802f3f0> >" ] }, "metadata": {}, @@ -1393,7 +2207,7 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 18, "metadata": {}, "outputs": [ { @@ -1604,7 +2418,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc284574690> >" + " *' at 0x7f55b802f360> >" ] }, "metadata": {}, @@ -1689,7 +2503,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc2845746f0> >" + " *' at 0x7f55b802f2a0> >" ] }, "metadata": {}, @@ -1786,7 +2600,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc284574570> >" + " *' at 0x7f55b802f0f0> >" ] }, "metadata": {}, @@ -1815,7 +2629,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 19, "metadata": {}, "outputs": [ { @@ -1955,10 +2769,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fc284574840> >" + " *' at 0x7f55b802f960> >" ] }, - "execution_count": 18, + "execution_count": 19, "metadata": {}, "output_type": "execute_result" } @@ -1983,7 +2797,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 20, "metadata": {}, "outputs": [ { @@ -2123,10 +2937,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fc284574840> >" + " *' at 0x7f55b802f960> >" ] }, - "execution_count": 19, + "execution_count": 20, "metadata": {}, "output_type": "execute_result" } @@ -2146,7 +2960,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 21, "metadata": {}, "outputs": [ { @@ -2286,7 +3100,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc284574840> >" + " *' at 0x7f55b802f960> >" ] }, "metadata": {}, @@ -2494,7 +3308,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 22, "metadata": {}, "outputs": [ { @@ -2733,7 +3547,7 @@ "" ] }, - "execution_count": 21, + "execution_count": 22, "metadata": {}, "output_type": "execute_result" } @@ -2761,7 +3575,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.7" + "version": "3.7.2+" } }, "nbformat": 4,