From fa06cfa30387e1f52bff236a341f2145dfa9de0f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 2 Dec 2016 17:56:47 +0100 Subject: [PATCH] alternation: implement remove_alternation() for weak alt automata MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This mixes the subset construction (for 1-state rejecting SCCs) and the breakpoint construction (for larger rejecting SCCs). The algorithm should probably be rewritten in a cleaner and more efficient way, but that should do for a first version. It should be easy to extend it to support Büchi acceptance (since the breakpoint construction works for this) when we need it. * spot/twaalgos/alternation.hh, spot/twaalgos/alternation.cc (remove_alternation): New function. * tests/python/alternation.ipynb: New file. * tests/Makefile.am, doc/org/tut.org: Add it. --- doc/org/tut.org | 1 + spot/twaalgos/alternation.cc | 396 ++++++- spot/twaalgos/alternation.hh | 13 +- tests/Makefile.am | 1 + tests/python/alternation.ipynb | 1799 ++++++++++++++++++++++++++++++++ 5 files changed, 2206 insertions(+), 4 deletions(-) create mode 100644 tests/python/alternation.ipynb diff --git a/doc/org/tut.org b/doc/org/tut.org index b0904ff9c..c658583ab 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -75,3 +75,4 @@ real notebooks instead. automata. - [[https://spot.lrde.epita.fr/ipynb/atva16-fig2a.html][=atva16-fig2a.ipynb=]] first example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]]. - [[https://spot.lrde.epita.fr/ipynb/atva16-fig2b.html][=atva16-fig2b.ipynb=]] second example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]]. +- [[https://spot.lrde.epita.fr/ipynb/alternation.html][=alternation.ipynb=]] examples of alternating automata. diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index 7208c73cb..fa4005cb7 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -17,9 +17,11 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include #include +#include +#include #include +#include namespace spot { @@ -62,6 +64,8 @@ namespace spot return res; } + + void outedge_combiner::new_dests(unsigned st, bdd out) const { minato_isop isop(out); @@ -85,4 +89,394 @@ namespace spot } } + + + namespace + { + class alternation_remover final + { + protected: + const_twa_graph_ptr aut_; + scc_info si_; + enum scc_class : char { accept, reject_1, reject_more }; + std::vector class_of_; + bool has_reject_more_ = false; + unsigned reject_1_count_ = 0; + std::set true_states_; + + void classify_each_scc() + { + auto& g = aut_->get_graph(); + unsigned sc = si_.scc_count(); + for (unsigned n = 0; n < sc; ++n) + { + if (si_.is_trivial(n)) + continue; + if (si_.states_of(n).size() == 1) + { + if (si_.is_rejecting_scc(n)) + { + class_of_[n] = scc_class::reject_1; + ++reject_1_count_; + } + else + { + // For size one, scc_info should always be able to + // decide rejecting/accepting. + assert(si_.is_accepting_scc(n)); + + unsigned s = si_.states_of(n).front(); + auto& ss = g.state_storage(s); + if (ss.succ == ss.succ_tail) + { + auto& es = g.edge_storage(ss.succ); + if (es.cond == bddtrue && !aut_->is_univ_dest(es.dst)) + true_states_.emplace(s); + } + } + } + else + { + acc_cond::mark_t m; + bool first = true; + for (auto src: si_.states_of(n)) + for (auto& t: aut_->out(src)) + for (unsigned d: aut_->univ_dests(t.dst)) + if (si_.scc_of(d) == n) + { + if (first) + { + first = false; + m = t.acc; + if (!aut_->acc().accepting(m)) + { + class_of_[n] = reject_more; + has_reject_more_ = true; + } + // In case of a universal edge we only + // need to check the first destination + // inside the SCC, because the other + // have the same t.acc. + break; + } + else if (m != t.acc) + { + throw std::runtime_error + ("alternation_removal() only work with weak " + "alternating automata"); + } + } + } + } + } + + std::vector state_to_var_; + std::map var_to_state_; + std::vector scc_to_var_; + std::map var_to_mark_; + bdd all_vars_; + bdd all_marks_; + bdd all_states_; + + void allocate_state_vars() + { + auto d = aut_->get_dict(); + // We need one BDD variable per possible output state. If + // that state is in a reject_more SCC we actually use two + // variables for the breakpoint. + unsigned ns = aut_->num_states(); + state_to_var_.reserve(ns); + bdd all_states = bddtrue; + for (unsigned s = 0; s < ns; ++s) + { + if (!si_.reachable_state(s)) + { + state_to_var_.push_back(0); + continue; + } + scc_class c = class_of_[si_.scc_of(s)]; + bool r = c == scc_class::reject_more; + int v = d->register_anonymous_variables(1 + r, this); + state_to_var_.push_back(v); + var_to_state_[v] = s; + all_states &= bdd_ithvar(v); + if (r) + { + var_to_state_[v + 1] = ~s; + all_states &= bdd_ithvar(v + 1); + } + } + // We also use one BDD variable per reject_1 SCC. Each of + // these variables will represent a bit in mark_t. We reserve + // the first bit for the break_point construction if we have + // some reject_more SCC. + unsigned nc = si_.scc_count(); + scc_to_var_.reserve(nc); + unsigned mark_pos = has_reject_more_; + bdd all_marks = bddtrue; + for (unsigned s = 0; s < nc; ++s) + { + scc_class c = class_of_[s]; + if (c == scc_class::reject_1) + { + int v = d->register_anonymous_variables(1, this); + scc_to_var_.emplace_back(v); + var_to_mark_.emplace(v, acc_cond::mark_t({mark_pos++})); + bdd bv = bdd_ithvar(v); + all_marks &= bv; + } + else + { + scc_to_var_.emplace_back(0); + } + } + all_marks_ = all_marks; + all_states_ = all_states; + all_vars_ = all_states & all_marks; + } + + std::map state_as_bdd_cache_; + + bdd state_as_bdd(unsigned s) + { + auto p = state_as_bdd_cache_.emplace(s, bddfalse); + if (!p.second) + return p.first->second; + + bool marked = (int)s < 0; + if (marked) + s = ~s; + + unsigned scc_s = si_.scc_of(s); + bdd res = bddfalse; + for (auto& e: aut_->out(s)) + { + bdd dest = bddtrue; + for (unsigned d: aut_->univ_dests(e.dst)) + { + unsigned scc_d = si_.scc_of(d); + scc_class c = class_of_[scc_d]; + bool mark = + marked && (scc_s == scc_d) && (c == scc_class::reject_more); + dest &= bdd_ithvar(state_to_var_[d] + mark); + if (c == scc_class::reject_1 && scc_s == scc_d) + dest &= bdd_ithvar(scc_to_var_[scc_s]); + } + res |= e.cond & dest; + } + + p.first->second = res; + return res; + } + + acc_cond::mark_t bdd_to_state(bdd b, std::vector& s) + { + acc_cond::mark_t m = 0U; + while (b != bddtrue) + { + assert(bdd_low(b) == bddfalse); + int v = bdd_var(b); + auto it = var_to_state_.find(v); + if (it != var_to_state_.end()) + { + s.push_back(it->second); + } + else + { + auto it2 = var_to_mark_.find(v); + assert(it2 != var_to_mark_.end()); + m |= it2->second; + } + b = bdd_high(b); + } + return m; + } + + void simplify_state_set(std::vector& ss) + { + auto to_remove = true_states_; + for (unsigned i: ss) + if ((int)i < 0) + to_remove.emplace(~i); + + auto i = + std::remove_if(ss.begin(), ss.end(), + [&] (unsigned s) { + return to_remove.find(s) != to_remove.end(); + }); + ss.erase(i, ss.end()); + std::sort(ss.begin(), ss.end()); + } + + bool has_mark(const std::vector& ss) + { + for (unsigned i: ss) + if ((int)i < 0) + return true; + return false; + } + + void set_mark(std::vector& ss) + { + for (unsigned& s: ss) + if (class_of_[si_.scc_of(s)] == scc_class::reject_more) + s = ~s; + } + + public: + alternation_remover(const const_twa_graph_ptr& aut) + : aut_(aut), si_(aut), class_of_(si_.scc_count(), scc_class::accept) + { + } + + ~alternation_remover() + { + aut_->get_dict()->unregister_all_my_variables(this); + } + + + twa_graph_ptr run(bool named_states) + { + // First, we classify each SCC into three possible classes: + // + // 1) trivial or accepting + // 2) rejecting of size 1 + // 3) rejecting of size >1 + classify_each_scc(); + + // Rejecting SCCs of size 1 can be handled using genralized + // Büchi acceptance, using one set per SCC, as in Gastin & + // Oddoux CAV'01. See also Boker & et al. ICALP'10. Larger + // rejecting SCCs require a more expensive procedure known as + // the break point construction. See Miyano & Hayashi (TCS + // 1984). We are currently combining the two constructions. + auto res = make_twa_graph(aut_->get_dict()); + res->copy_ap_of(aut_); + // We preserve deterministic-like properties, and + // stutter-invariance. + res->prop_copy(aut_, {false, false, true, true}); + res->set_generalized_buchi(has_reject_more_ + reject_1_count_); + + // We for easier computation of outgoing sets, we will + // represent states using BDD variables. + allocate_state_vars(); + + // Conversion between state-sets and states. + typedef std::vector state_set; + std::vector s_to_ss; + std::map ss_to_s; + std::stack todo; + + std::vector* state_name = nullptr; + if (named_states) + { + state_name = new std::vector(); + res->set_named_prop("state-names", state_name); + } + + auto new_state = [&](state_set& ss, bool& need_mark) + { + simplify_state_set(ss); + + if (has_reject_more_) + { + need_mark = has_mark(ss); + if (!need_mark) + set_mark(ss); + } + + auto p = ss_to_s.emplace(ss, 0); + if (!p.second) + return p.first->second; + unsigned s = res->new_state(); + assert(s == s_to_ss.size()); + p.first->second = s; + s_to_ss.emplace_back(ss); + todo.emplace(s); + + if (named_states) + { + std::ostringstream os; + bool notfirst = false; + for (unsigned s: ss) + { + if (notfirst) + os << ','; + else + notfirst = true; + if ((int)s < 0) + { + os << '~'; + s = ~s; + } + os << s; + } + if (!notfirst) + os << "{}"; + state_name->emplace_back(os.str()); + } + return s; + }; + + const auto& i = aut_->univ_dests(aut_->get_init_state_number()); + state_set is(i.begin(), i.end()); + bool has_mark = false; + res->set_init_state(new_state(is, has_mark)); + + acc_cond::mark_t all_marks = res->acc().all_sets(); + + state_set v; + while (!todo.empty()) + { + unsigned s = todo.top(); + todo.pop(); + + bdd bs = bddtrue; + for (unsigned se: s_to_ss[s]) + bs &= state_as_bdd(se); + + + bdd ap = bdd_exist(bdd_support(bs), all_vars_); + bdd all_letters = bdd_exist(bs, all_vars_); + + // First loop over all possible valuations atomic properties. + while (all_letters != bddfalse) + { + bdd oneletter = bdd_satoneset(all_letters, ap, bddtrue); + all_letters -= oneletter; + + minato_isop isop(bs & oneletter); + bdd cube; + while ((cube = isop.next()) != bddfalse) + { + bdd cond = bdd_exist(cube, all_vars_); + bdd dest = bdd_existcomp(cube, all_vars_); + v.clear(); + acc_cond::mark_t m = bdd_to_state(dest, v); + unsigned d = new_state(v, has_mark); + if (has_mark) + m.set(0); + res->new_edge(s, d, cond, all_marks - m); + } + } + } + res->merge_edges(); + return res; + } + }; + + } + + + twa_graph_ptr remove_alternation(const const_twa_graph_ptr& aut, + bool named_states) + { + if (!aut->is_alternating()) + // Nothing to do, why was this function called at all? + return std::const_pointer_cast(aut); + + alternation_remover ar(aut); + return ar.run(named_states); + } + } diff --git a/spot/twaalgos/alternation.hh b/spot/twaalgos/alternation.hh index a54123106..f4ba737fd 100644 --- a/spot/twaalgos/alternation.hh +++ b/spot/twaalgos/alternation.hh @@ -90,7 +90,14 @@ namespace spot } /// @} - - - + /// \brief Remove universal edges from an automaton. + /// + /// This procedure is restricted to weak alternating automata as + /// input, and produces TGBAs as output. (Generalized Büchi + /// acceptance is only used in presence of size-1 rejecting-SCCs.) + /// + /// \param named_states name each state for easier debugging + SPOT_API + twa_graph_ptr remove_alternation(const const_twa_graph_ptr& aut, + bool named_states = false); } diff --git a/tests/Makefile.am b/tests/Makefile.am index 8d9e5a1c3..4248f5773 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -302,6 +302,7 @@ if USE_PYTHON TESTS_ipython = \ python/acc_cond.ipynb \ python/accparse.ipynb \ + python/alternation.ipynb \ python/atva16-fig2a.ipynb \ python/atva16-fig2b.ipynb \ python/automata-io.ipynb \ diff --git a/tests/python/alternation.ipynb b/tests/python/alternation.ipynb new file mode 100644 index 000000000..ca231e52c --- /dev/null +++ b/tests/python/alternation.ipynb @@ -0,0 +1,1799 @@ +{ + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.5.2+" + }, + "name": "" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "code", + "collapsed": true, + "input": [ + "import spot\n", + "spot.setup(show_default='.ba')" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "These test cases for the `remove_alternation()` algorithm." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "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')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 2, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\u24ff\n", + "\n", + "\n", + "-1->3\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "1->-4\n", + "\n", + "!b\n", + "\n", + "\n", + "-4->1\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\u24ff\n", + "\n", + "\n", + "-4->2\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 2 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut2 = spot.remove_alternation(aut, True); aut2" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 3, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1,3\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "1,4\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3\n", + "\n", + "1,2,3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!b\n", + "\u2776\n", + "\n", + "\n", + "4\n", + "\n", + "1,2,4\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7fd1684339f0> >" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.scc_filter(aut2, True)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 4, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1,3\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "2\n", + "\n", + "1,4\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "3\n", + "\n", + "1,2,3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "4\n", + "\n", + "1,2,4\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7fd16b5891e0> >" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "# 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')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 5, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\u24ff\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 5 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.remove_alternation(aut, True)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 6, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "~0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "~1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "{}\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "~1,~0\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & !b & p\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7fd16843a2d0> >" + ] + } + ], + "prompt_number": 6 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "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')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 7, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "I->3\n", + "\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "3->-4\n", + "\n", + "a\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "-4->0\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "-4->4\n", + "\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 7 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.remove_alternation(aut, True)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 8, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "3\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "~0,4\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "3,~1\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "3\n", + "\n", + "4,~1,~0\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "4\n", + "\n", + "0,4,~1\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b & p\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b & p\n", + "\n", + "\n", + "5\n", + "\n", + "3,~0\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "6\n", + "\n", + "3,~1,~0\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "a & !b & p\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "6->4\n", + "\n", + "\n", + "a & !b & p\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7fd168433c90> >" + ] + } + ], + "prompt_number": 8 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "# 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')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 9, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "-7\n", + "\n", + "\n", + "\n", + "I->-7\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\u24ff\n", + "\n", + "\n", + "-7->0\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "-7->3\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "3->-4\n", + "\n", + "!a\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "a & b & p\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "-4->3\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\u24ff\n", + "\n", + "\n", + "-4->4\n", + "\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 9 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.remove_alternation(aut, True)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 10, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "~0,3\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "3,~1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "3,4\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & p\n", + "\u2776\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "4\n", + "\n", + "3,4,~1\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!a & !b & p\n", + "\u2776\n", + "\n", + "\n", + "5\n", + "\n", + "3,4,~0\n", + "\n", + "\n", + "1->5\n", + "\n", + "\n", + "!a & b & p\n", + "\u2776\n", + "\n", + "\n", + "6\n", + "\n", + "3,~1,~0\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + "a & b & p\n", + "\u2776\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "a & !b & p\n", + "\u2776\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a & !b & p\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!a & b & p\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "a & b & p\n", + "\u2776\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "a\n", + "\u2776\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "a & !b & p\n", + "\u2776\n", + "\n", + "\n", + "6->2\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "6->5\n", + "\n", + "\n", + "!a & b & p\n", + "\u2776\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & b & p\n", + "\u2776\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7fd1684d6420> >" + ] + } + ], + "prompt_number": 10 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "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" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 11, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "GF(a)\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "1\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "F(a)\n", + "\u24ff\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "t\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7fd168433d50> >" + ] + } + ], + "prompt_number": 11 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.remove_alternation(a, True)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 12, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7fd168433d20> >" + ] + } + ], + "prompt_number": 12 + }, + { + "cell_type": "code", + "collapsed": true, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": null + } + ], + "metadata": {} + } + ] +}