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": [
+ ""
+ ],
+ "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"
+ ],
+ "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"
+ ],
+ "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": [
+ ""
+ ],
+ "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"
+ ],
+ "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": [
+ ""
+ ],
+ "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"
+ ],
+ "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": [
+ ""
+ ],
+ "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"
+ ],
+ "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"
+ ],
+ "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"
+ ],
+ "text": [
+ " *' at 0x7fd168433d20> >"
+ ]
+ }
+ ],
+ "prompt_number": 12
+ },
+ {
+ "cell_type": "code",
+ "collapsed": true,
+ "input": [],
+ "language": "python",
+ "metadata": {},
+ "outputs": [],
+ "prompt_number": null
+ }
+ ],
+ "metadata": {}
+ }
+ ]
+}