From 9ab4b840fdf5e807a8268f0bfd37f4b7fff8ee5a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 2 Jun 2017 11:23:42 +0200 Subject: [PATCH] simulation: do not depend on bdd numbers for ordering classes Fixes #262 again. Reported by Maximilien Colange. * spot/twaalgos/simulation.cc: Use state numbers to order classes, not their signatures. The problem was that even if two simulation of the same automaton assign the same signature, the BDD identifier used for that signature might be different, and therefore the ordering obtained by using BDDs as keys in a map can be different. A side-effect of this change is that the order of states in automata produced by simulation-based reduction may change; many tests had to be updated. * tests/core/ltl2tgba.test: Add a new test case based on Maximilien's report. * tests/core/complement.test, tests/core/det.test, tests/core/parseaut.test, tests/core/prodor.test, tests/core/scc.test, tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb, tests/python/decompose.ipynb, tests/python/decompose_scc.py, tests/python/highlighting.ipynb, tests/python/piperead.ipynb, tests/python/sccinfo.py, tests/python/simstate.py, tests/python/testingaut.ipynb, tests/python/word.ipynb: Update test case for new order of states. --- spot/twaalgos/simulation.cc | 54 +- tests/core/complement.test | 4 +- tests/core/det.test | 42 +- tests/core/ltl2tgba.test | 8 + tests/core/parseaut.test | 50 +- tests/core/prodor.test | 10 +- tests/core/scc.test | 2 +- tests/python/atva16-fig2a.ipynb | 118 ++-- tests/python/automata.ipynb | 930 ++++++++++++++++---------------- tests/python/decompose.ipynb | 650 +++++++++++----------- tests/python/decompose_scc.py | 19 +- tests/python/highlighting.ipynb | 122 ++--- tests/python/piperead.ipynb | 76 ++- tests/python/sccinfo.py | 10 +- tests/python/simstate.py | 15 +- tests/python/testingaut.ipynb | 532 +++++++++--------- tests/python/word.ipynb | 224 +++++--- 17 files changed, 1464 insertions(+), 1402 deletions(-) diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index 9fd965a7c..4363a22db 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -275,7 +275,7 @@ namespace spot // We run through the map bdd/list, and we update // the previous_class_ with the new data. - for (auto& p: bdd_lstate_) + for (auto& p: sorted_classes_) { // If the signature of a state is bddfalse (no // edges) the class of this state is bddfalse @@ -283,11 +283,11 @@ namespace spot // simplifications in the signature by removing a // edge which has as a destination a state with // no outgoing edge. - if (p.first == bddfalse) - for (auto s: p.second) + if (p->first == bddfalse) + for (unsigned s: p->second) previous_class_[s] = bddfalse; else - for (auto s: p.second) + for (unsigned s: p->second) previous_class_[s] = *it_bdd; ++it_bdd; } @@ -302,10 +302,10 @@ namespace spot { update_previous_class(); nb_partition_before = bdd_lstate_.size(); - bdd_lstate_.clear(); nb_po_before = po_size_; po_size_ = 0; update_sig(); + // print_partition(); go_to_next_it(); } @@ -347,8 +347,18 @@ namespace spot void update_sig() { + bdd_lstate_.clear(); + sorted_classes_.clear(); for (unsigned s = 0; s < size_a_; ++s) - bdd_lstate_[compute_sig(s)].emplace_back(s); + { + bdd sig = compute_sig(s); + auto p = bdd_lstate_.emplace(std::piecewise_construct, + std::make_tuple(sig), + std::make_tuple()); + p.first->second.emplace_back(s); + if (p.second) + sorted_classes_.emplace_back(p.first); + } } @@ -390,7 +400,7 @@ namespace spot std::list::iterator it_bdd = used_var_.begin(); - for (auto& p: bdd_lstate_) + for (auto& p: sorted_classes_) { // If the signature of a state is bddfalse (no edges) the // class of this state is bddfalse instead of an anonymous @@ -398,9 +408,9 @@ namespace spot // removing an edge which has as a destination a state // with no outgoing edge. bdd acc = bddfalse; - if (p.first != bddfalse) + if (p->first != bddfalse) acc = *it_bdd; - now_to_next.emplace_back(p.first, acc); + now_to_next.emplace_back(p->first, acc); ++it_bdd; } @@ -450,16 +460,16 @@ namespace spot if (implications) implications->resize(bdd_lstate_.size()); - // Create one state per partition. - for (auto& p: bdd_lstate_) + // Create one state per class. + for (auto& p: sorted_classes_) { - bdd cl = previous_class_[p.second.front()]; + bdd cl = previous_class_[p->second.front()]; // A state may be referred to either by // its class, or by all the implied classes. auto s = gb->new_state(cl.id()); gb->alias_state(s, relation_[cl].id()); // update state_mapping - for (auto& st : p.second) + for (auto& st : p->second) (*state_mapping)[st] = s; if (implications) (*implications)[s] = relation_[cl]; @@ -479,14 +489,14 @@ namespace spot auto all_inf = all_inf_; // For each class, we will create // all the edges between the states. - for (auto& p: bdd_lstate_) + for (auto& p: sorted_classes_) { // All states in p.second have the same class, so just // pick the class of the first one first one. - bdd src = previous_class_[p.second.front()]; + bdd src = previous_class_[p->second.front()]; // Get the signature to derive successors. - bdd sig = compute_sig(p.second.front()); + bdd sig = compute_sig(p->second.front()); if (Cosimulation) sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial)); @@ -621,12 +631,12 @@ namespace spot // where is the new class name. void print_partition() { - for (auto& p: bdd_lstate_) + for (auto& p: sorted_classes_) { std::cerr << "partition: " - << bdd_format_isop(a_->get_dict(), p.first) + << bdd_format_isop(a_->get_dict(), p->first) << std::endl; - for (auto s: p.second) + for (auto s: p->second) std::cerr << " - " << a_->format_state(a_->state_from_number(s)) << '\n'; @@ -654,9 +664,13 @@ namespace spot // Represent the class of each state at the previous iteration. vector_state_bdd previous_class_; - // The list of state for each class at the current_iteration. + // The list of states for each class at the current_iteration. // Computed in `update_sig'. map_bdd_lstate bdd_lstate_; + // The above map, sorted by states number instead of BDD + // identifier to avoid non-determinism while iterating over all + // states. + std::vector sorted_classes_; // The queue of free bdd. They will be used as the identifier // for the class. diff --git a/tests/core/complement.test b/tests/core/complement.test index 6a1f4c1c2..2ef1566ac 100755 --- a/tests/core/complement.test +++ b/tests/core/complement.test @@ -118,11 +118,11 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0] 1 {1} [!0] 0 -State: 1 [0] 1 {1} +State: 1 [!0] 0 {0} +[0] 1 {1} --END-- EOF diff out expected diff --git a/tests/core/det.test b/tests/core/det.test index 9d4014ee5..eeb7d3c22 100755 --- a/tests/core/det.test +++ b/tests/core/det.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2013-2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -148,20 +148,20 @@ cat >expected-nd.hoa <expected-rand.hoa <expected-rand2.hoa <res2 ltl2tgba --low --any 'Fp0 -> XXG(1 U Gp1)' "$s" >>res2 diff res1 res2 + +# Another case where different but isomorphic automata +# were output (issue #262 again). +f1='F(Gp0 <-> Gp1)' +f2='Gp1 | FGp0' +(ltl2tgba -xsimul=1 --low "$f1"; ltl2tgba -xsimul=1 --low "$f2") > res1 +ltl2tgba -xsimul=1 --low "$f1" "$f2" > res2 +diff res1 res2 diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index c7e952bd3..ae39ed017 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -1712,7 +1712,7 @@ cat >expected <\u2776\n", ")\n", "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "2\n", "\n", "2\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a | b\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !b\n", "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", - "\u2776\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "\u2776\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!a & b\n", - "\u2776\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !b\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "1->1\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", + "1->1\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f79506d2900> >" + " *' at 0x7f6b2060be40> >" ] } ], diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 841518fc9..d3e5cc8f0 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -177,7 +177,7 @@ "\n" ], "text": [ - " *' at 0x7f7fe56a0540> >" + " *' at 0x7f9ae817a8d0> >" ] } ], @@ -204,113 +204,113 @@ "output_type": "pyout", "prompt_number": 3, "svg": [ - "\n", + "\n", "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "" @@ -371,7 +371,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a & !b\n", @@ -382,7 +382,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "b\n", @@ -393,13 +393,13 @@ "4\n", "\n", "\n", - "0->4\n", + "0->4\n", "\n", "\n", "!a & !b\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "c & d\n", @@ -411,7 +411,7 @@ "2\n", "\n", "\n", - "1->2\n", + "1->2\n", "\n", "\n", "!c & d\n", @@ -423,44 +423,44 @@ "3\n", "\n", "\n", - "1->3\n", + "1->3\n", "\n", "\n", "!d\n", "\u24ff\n", "\n", "\n", - "2->1\n", + "2->1\n", "\n", "\n", "c\n", "\n", "\n", - "2->2\n", + "2->2\n", "\n", "\n", "!c\n", "\n", "\n", - "3->1\n", + "3->1\n", "\n", "\n", "c & d\n", "\n", "\n", - "3->2\n", + "3->2\n", "\n", "\n", "!c & d\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "!d\n", "\n", "\n", - "4->4\n", + "4->4\n", "\n", "\n", "1\n", @@ -569,7 +569,7 @@ "\n" ], "text": [ - " *' at 0x7f7fe4d87f90> >" + " *' at 0x7f9ae816aa20> >" ] } ], @@ -639,7 +639,7 @@ "\n" ], "text": [ - " *' at 0x7f7fe4da41b0> >" + " *' at 0x7f9ae816a4b0> >" ] } ], @@ -715,7 +715,7 @@ "\n" ], "text": [ - " *' at 0x7f7fe4e0f330> >" + " *' at 0x7f9ae816a300> >" ] } ], @@ -1061,121 +1061,121 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a | b\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "!a & !b\n", + "3->2\n", + "\n", + "\n", + "a | b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a | b\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "a | b\n", + "3->3\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f7fe4da4510> >" + " *' at 0x7f9ae816a9f0> >" ] } ], @@ -1214,69 +1214,69 @@ "G\n", "\n", "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "2\n", "\n", "2\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "b\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!a\n", - "\u24ff\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f7fe4da4540> >" + " *' at 0x7f9ae816a870> >" ] } ], @@ -1334,67 +1334,67 @@ "\n", "1\n", "\n", - "\n", "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "b\n", "\n", "\n", "2\n", "\n", + "\n", "2\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!a\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!b\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!b\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f7fe4da4570> >" + " *' at 0x7f9ae816a690> >" ] } ], @@ -1493,7 +1493,7 @@ "\n" ], "text": [ - " *' at 0x7f7fe4da43c0> >" + " *' at 0x7f9ae816a6f0> >" ] } ], @@ -1963,7 +1963,7 @@ "\n" ], "text": [ - " *' at 0x7f7fe4da4150> >" + " *' at 0x7f9ae816a3f0> >" ] } ], @@ -2292,136 +2292,136 @@ "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a\n", - "\u24ff\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "!a\n", - "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", + "\u24ff\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "4\n", + "\n", + "4\n", "\n", - "\n", - "0->4\n", - "\n", - "\n", - "a | b\n", + "\n", + "1->4\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "1\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "" @@ -2440,145 +2440,145 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "I->2\n", - "\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\n", "\n", - "0\n", - "\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", - "\n", - "2->0\n", - "\n", - "\n", - "a\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\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", + "b\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "0->5\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "4->5\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "5->2\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "5->4\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "5->1\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "5->3\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "3->4\n", "\n", "\n", "a & !b\n", "\n", - "\n", - "3->1\n", + "\n", + "5\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "2->5\n", "\n", "\n", "!a & !b\n", "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n" ], "text": [ - " *' at 0x7f7fe4da4660> >" + " *' at 0x7f9ae817a3f0> >" ] } ], @@ -2734,7 +2734,7 @@ "\n" ], "text": [ - " *' at 0x7f7fe4da4450> >" + " *' at 0x7f9ae816aab0> >" ] } ], @@ -2804,7 +2804,7 @@ "\n" ], "text": [ - " *' at 0x7f7fe4e0f5a0> >" + " *' at 0x7f9ae816ae10> >" ] } ], @@ -3193,35 +3193,35 @@ "G\n", "\n", "\n", - "\n", - "1\n", + "\n", + "0\n", "\n", - "1\n", + "0\n", "\n", - "\n", - "I->1\n", + "\n", + "I->0\n", "\n", "\n", "\n", - "\n", - "1->1\n", + "\n", + "0->0\n", "\n", "\n", - "1\n", + "1\n", "\n", - "\n", - "0\n", + "\n", + "1\n", "\n", - "0\n", + "1\n", "\n", - "\n", - "1->0\n", + "\n", + "0->1\n", "\n", "\n", "a\n", "\n", - "\n", - "0->0\n", + "\n", + "1->1\n", "\n", "\n", "a\n", @@ -3231,7 +3231,7 @@ "\n" ], "text": [ - " *' at 0x7f7fe4da46f0> >" + " *' at 0x7f9ae816af60> >" ] }, { @@ -3279,7 +3279,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a\n", @@ -3290,21 +3290,21 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a\n", "\u2776\n", "\n", "\n", - "1->0\n", + "1->0\n", "\n", "\n", "!a\n", "\u24ff\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a\n", @@ -3399,7 +3399,7 @@ "\n" ], "text": [ - " *' at 0x7f7fe4da4090> >" + " *' at 0x7f9ae81250f0> >" ] } ], @@ -3488,7 +3488,7 @@ "\n" ], "text": [ - " *' at 0x7f7fe4da4090> >" + " *' at 0x7f9ae81250f0> >" ] } ], @@ -3577,7 +3577,7 @@ "\n" ], "text": [ - " *' at 0x7f7fe4da4090> >" + " *' at 0x7f9ae81250f0> >" ] } ], diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb index debcfdcd9..8d4ab68b2 100644 --- a/tests/python/decompose.ipynb +++ b/tests/python/decompose.ipynb @@ -80,138 +80,138 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", "cluster_0\n", - "\n", + "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "cluster_2\n", - "\n", + "\n", "\n", "cluster_3\n", - "\n", + "\n", "\n", "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", - "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & !c\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!a\n", + "\n", + "4->1\n", + "\n", + "\n", + "!a\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!a & c\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a & c\n", "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & c\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & c\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !c\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fa1681b0690> >" + " *' at 0x7f3a2c7d9690> >" ] } ], @@ -278,7 +278,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -289,7 +289,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & b & !c\n", @@ -328,7 +328,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0660> >" + " *' at 0x7f3a2c7d9360> >" ] } ], @@ -395,30 +395,30 @@ "\n", "!a & !c\n", "\n", - "\n", - "2\n", + "\n", + "1\n", "\n", - "2\n", + "1\n", "\n", - "\n", - "0->2\n", + "\n", + "0->1\n", "\n", "\n", "c\n", "\n", - "\n", - "1\n", + "\n", + "2\n", "\n", - "1\n", + "2\n", "\n", - "\n", - "0->1\n", + "\n", + "0->2\n", "\n", "\n", "a & !c\n", "\n", - "\n", - "2->2\n", + "\n", + "1->1\n", "\n", "\n", "1\n", @@ -429,8 +429,8 @@ "\n", "3\n", "\n", - "\n", - "3->2\n", + "\n", + "3->1\n", "\n", "\n", "!a\n", @@ -441,26 +441,26 @@ "\n", "a\n", "\n", - "\n", - "1->0\n", + "\n", + "2->0\n", "\n", "\n", "!a & !c\n", "\n", - "\n", - "1->2\n", + "\n", + "2->1\n", "\n", "\n", "!a & c\n", "\n", - "\n", - "1->3\n", + "\n", + "2->3\n", "\n", "\n", "a & c\n", "\n", - "\n", - "1->1\n", + "\n", + "2->2\n", "\n", "\n", "a & !c\n", @@ -469,7 +469,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b03f0> >" + " *' at 0x7f3a2c7d9510> >" ] } ], @@ -559,7 +559,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0510> >" + " *' at 0x7f3a2c7d9660> >" ] } ], @@ -636,7 +636,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0ed0> >" + " *' at 0x7f3a2c7d9ed0> >" ] } ], @@ -700,7 +700,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -712,7 +712,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & b & !c\n", @@ -752,7 +752,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b05a0> >" + " *' at 0x7f3a30923420> >" ] }, { @@ -801,30 +801,30 @@ "!a & !c\n", "\u24ff\n", "\n", - "\n", - "2\n", + "\n", + "1\n", "\n", - "2\n", + "1\n", "\n", - "\n", - "0->2\n", + "\n", + "0->1\n", "\n", "\n", "c\n", "\n", - "\n", - "1\n", + "\n", + "2\n", "\n", - "1\n", + "2\n", "\n", - "\n", - "0->1\n", + "\n", + "0->2\n", "\n", "\n", "a & !c\n", "\n", - "\n", - "2->2\n", + "\n", + "1->1\n", "\n", "\n", "1\n", @@ -835,8 +835,8 @@ "\n", "3\n", "\n", - "\n", - "3->2\n", + "\n", + "3->1\n", "\n", "\n", "!a\n", @@ -847,27 +847,27 @@ "\n", "a\n", "\n", - "\n", - "1->0\n", + "\n", + "2->0\n", "\n", "\n", "!a & !c\n", "\u24ff\n", "\n", - "\n", - "1->2\n", + "\n", + "2->1\n", "\n", "\n", "!a & c\n", "\n", - "\n", - "1->3\n", + "\n", + "2->3\n", "\n", "\n", "a & c\n", "\n", - "\n", - "1->1\n", + "\n", + "2->2\n", "\n", "\n", "a & !c\n", @@ -876,7 +876,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b05d0> >" + " *' at 0x7f3a2c7d9e40> >" ] }, { @@ -889,137 +889,137 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "option: wt\n", - "Inf(\n", - "\u24ff\n", - ")\n", + "\n", + "option: wt\n", + "Inf(\n", + "\u24ff\n", + ")\n", "cluster_0\n", - "\n", + "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "cluster_2\n", - "\n", + "\n", "\n", "cluster_3\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a & !c\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "c\n", + "0->1\n", + "\n", + "\n", + "c\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "\n", + "\n", + "1\n", + "\u24ff\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "\n", + "2->2\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!a\n", + "\n", + "4->1\n", + "\n", + "\n", + "!a\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "2->0\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!a & c\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a & c\n", "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & c\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & c\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !c\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fa1681b0e70> >" + " *' at 0x7f3a2c7d9540> >" ] } ], @@ -1424,7 +1424,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b04b0> >" + " *' at 0x7f3a2c777360> >" ] } ], @@ -1749,7 +1749,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e420> >" + " *' at 0x7f3a2c777450> >" ] }, { @@ -1946,7 +1946,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0540> >" + " *' at 0x7f3a2c7d95d0> >" ] }, { @@ -2126,7 +2126,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0360> >" + " *' at 0x7f3a2c7d9e40> >" ] } ], @@ -2461,7 +2461,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b03c0> >" + " *' at 0x7f3a30923420> >" ] } ], @@ -2605,7 +2605,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e4b0> >" + " *' at 0x7f3a2c7774e0> >" ] }, { @@ -2724,7 +2724,7 @@ "\n" ], "text": [ - " *' at 0x7fa16823e5a0> >" + " *' at 0x7f3a2c7d9e70> >" ] }, { @@ -2904,7 +2904,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0ea0> >" + " *' at 0x7f3a2d0686f0> >" ] } ], @@ -3261,7 +3261,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e420> >" + " *' at 0x7f3a2c7774e0> >" ] } ], @@ -3551,7 +3551,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e4b0> >" + " *' at 0x7f3a2c7773f0> >" ] }, { @@ -3703,7 +3703,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0e40> >" + " *' at 0x7f3a2c7d9e40> >" ] }, { @@ -3840,7 +3840,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b05a0> >" + " *' at 0x7f3a2c7d93f0> >" ] } ], @@ -4143,7 +4143,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e450> >" + " *' at 0x7f3a2c777510> >" ] } ], @@ -4254,7 +4254,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e660> >" + " *' at 0x7f3a2c777750> >" ] } ], @@ -4346,7 +4346,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e5d0> >" + " *' at 0x7f3a2c777870> >" ] }, { @@ -4412,7 +4412,7 @@ "\n" ], "text": [ - " *' at 0x7fa16823e5a0> >" + " *' at 0x7f3a2c7d9ea0> >" ] } ], @@ -4498,7 +4498,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e540> >" + " *' at 0x7f3a2c777930> >" ] } ], @@ -4653,7 +4653,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e990> >" + " *' at 0x7f3a2c777990> >" ] } ], @@ -4782,7 +4782,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814ea50> >" + " *' at 0x7f3a2c777420> >" ] }, { @@ -4870,7 +4870,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0e70> >" + " *' at 0x7f3a2c7d9540> >" ] }, { @@ -4987,7 +4987,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814eab0> >" + " *' at 0x7f3a2c777a50> >" ] } ], @@ -5025,115 +5025,83 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", "cluster_0\n", - "\n", + "\n", "\n", "cluster_1\n", - "\n", - "\n", - "cluster_2\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "\n", + "2\n", + "\n", + "2\n", "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & c\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !c\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fa1681b0360> >" + " *' at 0x7f3a2c777870> >" ] } ], @@ -5246,7 +5214,7 @@ "\n" ], "text": [ - " *' at 0x7fa16816a1b0> >" + " *' at 0x7f3a2c7941b0> >" ] } ], diff --git a/tests/python/decompose_scc.py b/tests/python/decompose_scc.py index a92669979..6566605ac 100644 --- a/tests/python/decompose_scc.py +++ b/tests/python/decompose_scc.py @@ -20,7 +20,6 @@ import spot aut = spot.translate('(Ga -> Gb) W c') - si = spot.scc_info(aut) assert (spot.decompose_scc(si, 2).to_str('hoa', '1.1') == """HOA: v1.1 @@ -50,7 +49,7 @@ except ValueError: else: raise AssertionError -assert (spot.decompose_acc_scc(aut, 1).to_str('hoa', '1.1') == """HOA: v1.1 +assert (spot.decompose_acc_scc(aut, 0).to_str('hoa', '1.1') == """HOA: v1.1 States: 4 Start: 0 AP: 3 "b" "a" "c" @@ -61,17 +60,17 @@ properties: deterministic --BODY-- State: 0 [!1&!2] 0 -[1&!2] 1 -[2] 2 -State: 1 +[2] 1 +[1&!2] 2 +State: 1 {0} +[t] 1 +State: 2 [!1&!2] 0 -[1&!2] 1 -[!1&2] 2 +[!1&2] 1 +[1&!2] 2 [1&2] 3 -State: 2 {0} -[t] 2 State: 3 -[!1] 2 +[!1] 1 [1] 3 --END--""") diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 861e2282c..ac3fdf7ea 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -254,7 +254,7 @@ "\n" ], "text": [ - " *' at 0x7f304c67b690> >" + " *' at 0x7f98b673b870> >" ] } ], @@ -356,7 +356,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60b2d0> >" + " *' at 0x7f98b66ad630> >" ] } ], @@ -571,7 +571,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60b150> >" + " *' at 0x7f98b66ad300> >" ] } ], @@ -750,7 +750,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60b150> >" + " *' at 0x7f98b66ad300> >" ] } ], @@ -830,7 +830,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60b870> >" + " *' at 0x7f98b66ad7b0> >" ] }, { @@ -876,7 +876,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60b840> >" + " *' at 0x7f98b66ad570> >" ] } ], @@ -962,7 +962,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60b8a0> >" + " *' at 0x7f98b66ad750> >" ] } ], @@ -1087,7 +1087,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60b8a0> >" + " *' at 0x7f98b66ad750> >" ] }, { @@ -1144,7 +1144,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60b870> >" + " *' at 0x7f98b66ad7b0> >" ] }, { @@ -1190,7 +1190,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60b840> >" + " *' at 0x7f98b66ad570> >" ] } ], @@ -1397,7 +1397,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60b6f0> >" + " *' at 0x7f98b66ad510> >" ] }, { @@ -1471,7 +1471,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60b690> >" + " *' at 0x7f98b66adb70> >" ] }, { @@ -1555,7 +1555,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60b810> >" + " *' at 0x7f98b66ad3c0> >" ] } ], @@ -1701,7 +1701,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60bab0> >" + " *' at 0x7f98b66adcc0> >" ] } ], @@ -1846,7 +1846,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60bab0> >" + " *' at 0x7f98b66adcc0> >" ] } ], @@ -1989,7 +1989,7 @@ "\n" ], "text": [ - " *' at 0x7f304c60bab0> >" + " *' at 0x7f98b66adcc0> >" ] }, { @@ -2202,51 +2202,51 @@ "\n", "\n", "\n", - "\n", - "1\n", + "\n", + "0\n", "\n", - "1\n", + "0\n", "\n", - "\n", - "I->1\n", + "\n", + "I->0\n", "\n", "\n", "\n", - "\n", - "0\n", + "\n", + "1\n", "\n", - "0\n", + "1\n", "\n", - "\n", - "1->0\n", + "\n", + "0->1\n", "\n", "\n", "a\n", "\n", - "\n", - "2\n", + "\n", + "3\n", "\n", - "2\n", + "3\n", "\n", - "\n", - "1->2\n", + "\n", + "0->3\n", "\n", "\n", "!a & !b\n", "\n", - "\n", - "3\n", + "\n", + "2\n", "\n", - "3\n", + "2\n", "\n", - "\n", - "1->3\n", + "\n", + "0->2\n", "\n", "\n", "!a & b\n", "\n", - "\n", - "0->0\n", + "\n", + "1->1\n", "\n", "\n", "1\n", @@ -2263,7 +2263,7 @@ "6\n", "\n", "\n", - "4->6\n", + "4->6\n", "\n", "\n", "!c\n", @@ -2274,69 +2274,69 @@ "7\n", "\n", "\n", - "4->7\n", + "4->7\n", "\n", "\n", "c\n", "\n", "\n", - "6->4\n", + "6->4\n", "\n", "\n", "!b\n", "\u2776\n", "\n", "\n", - "6->6\n", + "6->6\n", "\n", "\n", "b & !c\n", "\n", "\n", - "6->7\n", + "6->7\n", "\n", "\n", "b & c\n", "\n", "\n", - "7->4\n", + "7->4\n", "\n", "\n", "b\n", "\u2776\n", "\n", "\n", - "7->6\n", + "7->6\n", "\n", "\n", "!b & !c\n", "\n", "\n", - "7->7\n", + "7->7\n", "\n", "\n", "!b & c\n", "\n", - "\n", - "2->4\n", + "\n", + "3->4\n", "\n", "\n", "a\n", "\n", - "\n", - "3->4\n", + "\n", + "2->4\n", "\n", "\n", "a\n", "\n", - "\n", - "3->2\n", + "\n", + "2->3\n", "\n", "\n", "!a & !b\n", "\n", - "\n", - "3->3\n", + "\n", + "2->2\n", "\n", "\n", "!a & b & !c\n", @@ -2346,26 +2346,26 @@ "\n", "5\n", "\n", - "\n", - "3->5\n", + "\n", + "2->5\n", "\n", "\n", "!a & b & c\n", "\n", "\n", - "5->4\n", + "5->4\n", "\n", "\n", "a\n", "\n", - "\n", - "5->2\n", + "\n", + "5->3\n", "\n", "\n", "!a & !b\n", "\n", - "\n", - "5->3\n", + "\n", + "5->2\n", "\n", "\n", "!a & b\n", diff --git a/tests/python/piperead.ipynb b/tests/python/piperead.ipynb index 4f9392704..874c75352 100644 --- a/tests/python/piperead.ipynb +++ b/tests/python/piperead.ipynb @@ -15,10 +15,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.4.3+" + "version": "3.5.3" }, - "name": "", - "signature": "sha256:8de782e4035d4a93101b749825f0975f5f8cee034332d048014ba13dfa232983" + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -111,7 +110,7 @@ "\n" ], "text": [ - " *' at 0x7fad7cc5f330> >" + " *' at 0x7f2bb6866420> >" ] }, { @@ -162,7 +161,7 @@ "\n" ], "text": [ - " *' at 0x7fad7cc5f4e0> >" + " *' at 0x7f2bb47205d0> >" ] }, { @@ -208,7 +207,7 @@ "\n" ], "text": [ - " *' at 0x7fad7cc5f270> >" + " *' at 0x7f2bb4720360> >" ] }, { @@ -227,36 +226,36 @@ "G\n", "\n", "\n", - "\n", - "1\n", + "\n", + "0\n", "\n", - "1\n", + "0\n", "\n", - "\n", - "I->1\n", + "\n", + "I->0\n", "\n", "\n", "\n", - "\n", - "0\n", + "\n", + "1\n", "\n", - "0\n", + "1\n", "\n", - "\n", - "1->0\n", + "\n", + "0->1\n", "\n", "\n", "a\n", "\n", - "\n", - "0->0\n", + "\n", + "1->1\n", "\n", "\n", "b\n", "\u24ff\n", "\n", - "\n", - "0->0\n", + "\n", + "1->1\n", "\n", "\n", "!b\n", @@ -265,7 +264,7 @@ "\n" ], "text": [ - " *' at 0x7fad7cc5f330> >" + " *' at 0x7f2bb47203f0> >" ] } ], @@ -342,7 +341,7 @@ "\n" ], "text": [ - " *' at 0x7fad7cc5f4e0> >" + " *' at 0x7f2bb4720660> >" ] } ], @@ -371,10 +370,11 @@ "evalue": "Command 'non-existing-command' returned non-zero exit status 127", "output_type": "pyerr", "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mCalledProcessError\u001b[0m Traceback (most recent call last)", + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mCalledProcessError\u001b[0m Traceback (most recent call last)", "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'non-existing-command|'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", - "\u001b[0;32m/home/adl/git/spot/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 457\u001b[0m See `spot.automata` for a list of supported formats.\"\"\"\n\u001b[1;32m 458\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 459\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 460\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 461\u001b[0m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", - "\u001b[0;32m/home/adl/git/spot/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, debug, *sources)\u001b[0m\n\u001b[1;32m 442\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 443\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 444\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 445\u001b[0m \u001b[0;31m# deleting o explicitely now prevents Python 3.5 from\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 446\u001b[0m \u001b[0;31m# reporting the following error: \" 465\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 466\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 467\u001b[0m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m/home/adl/git/spot/python/spot/__init__.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, no_sid, debug, *sources)\u001b[0m\n\u001b[1;32m 448\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 449\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 450\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 451\u001b[0m \u001b[0;31m# deleting o explicitely now prevents Python 3.5 from\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 452\u001b[0m \u001b[0;31m# reporting the following error: \"\n" ], "text": [ - " *' at 0x7fad7cc5f780> >" + " *' at 0x7f2bb4720570> >" ] }, { @@ -453,9 +453,10 @@ "evalue": "Command 'ltl2tgba \"syntax U U error\"' returned non-zero exit status 2", "output_type": "pyerr", "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mCalledProcessError\u001b[0m Traceback (most recent call last)", + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mCalledProcessError\u001b[0m Traceback (most recent call last)", "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0;32mfor\u001b[0m \u001b[0ma\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"ltl2tgba 'a U b'|\"\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m'ltl2tgba \"syntax U U error\"|'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 2\u001b[0m \u001b[0mdisplay\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0ma\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", - "\u001b[0;32m/home/adl/git/spot/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, debug, *sources)\u001b[0m\n\u001b[1;32m 442\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 443\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 444\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 445\u001b[0m \u001b[0;31m# deleting o explicitely now prevents Python 3.5 from\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 446\u001b[0m \u001b[0;31m# reporting the following error: \" 450\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 451\u001b[0m \u001b[0;31m# deleting o explicitely now prevents Python 3.5 from\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 452\u001b[0m \u001b[0;31m# reporting the following error: \" 465\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 466\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;31mStopIteration\u001b[0m: ", + "\nDuring handling of the above exception, another exception occurred:\n", + "\u001b[0;31mRuntimeError\u001b[0m Traceback (most recent call last)", "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'true|'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", - "\u001b[0;32m/home/adl/git/spot/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 459\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 460\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 461\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 462\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 463\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m/home/adl/git/spot/python/spot/__init__.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 465\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 466\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 467\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 468\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 469\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n", "\u001b[0;31mRuntimeError\u001b[0m: Failed to read automaton from true|" ] } ], "prompt_number": 6 - }, - { - "cell_type": "code", - "collapsed": false, - "input": [], - "language": "python", - "metadata": {}, - "outputs": [] } ], "metadata": {} } ] -} \ No newline at end of file +} diff --git a/tests/python/sccinfo.py b/tests/python/sccinfo.py index 19c5d21c1..16267fdf4 100644 --- a/tests/python/sccinfo.py +++ b/tests/python/sccinfo.py @@ -70,10 +70,10 @@ while todo: seen.add(s) todo.add(s) assert seen == {0, 1, 2, 3} -assert trans == [(1, 0), (1, 1), (1, 2), (1, 3), - (2, 1), (2, 2), (2, 3), (2, 4), - (0, 0), (3, 3), (4, 3), (4, 4)] -assert transi == [(1, 1, 3), (1, 2, 4), (2, 1, 6), (2, 2, 7), - (0, 0, 1), (3, 3, 10), (4, 4, 12)] +assert trans == [(0, 0), (0, 1), (0, 2), (0, 3), + (3, 0), (3, 1), (3, 3), (3, 4), + (1, 1), (2, 2), (4, 1), (4, 4)] +assert transi == [(0, 0, 1), (0, 3, 4), (3, 0, 7), + (3, 3, 9), (1, 1, 5), (2, 2, 6), (4, 4, 12)] assert not spot.is_weak_automaton(a, si) diff --git a/tests/python/simstate.py b/tests/python/simstate.py index 9c4943ac7..ec8a8aea8 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -75,21 +75,21 @@ Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3))) properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- -State: 0 "{₀[1]₀}" -[0&1] 1 {3} -[!0&1] 0 +State: 0 "{₀[0]₀}" [0&!1] 0 {1} [!0&!1] 0 -State: 1 "{₀[1]{₂[0]₂}₀}{₁[2]₁}" +[!0&1] 0 [0&1] 1 {3} -[!0&1] 2 +State: 1 "{₀[0]{₂[2]₂}₀}{₁[1]₁}" [0&!1] 0 {1} [!0&!1] 0 {2} -State: 2 "{₀[1]₀}{₁[2]₁}" -[0&1] 1 {3} [!0&1] 2 +[0&1] 1 {3} +State: 2 "{₀[0]₀}{₁[1]₁}" [0&!1] 0 {1} [!0&!1] 0 {2} +[!0&1] 2 +[0&1] 1 {3} --END--""" aut = spot.automaton(""" @@ -166,4 +166,3 @@ State: 11 "{₀[1#1]{₁[0#0,0#1]{₂[1#0]₂}₁}₀}" [0&1] 9 {1} [!0&1] 1 {1} --END--""" - diff --git a/tests/python/testingaut.ipynb b/tests/python/testingaut.ipynb index 9d7f44e85..1185ceb52 100644 --- a/tests/python/testingaut.ipynb +++ b/tests/python/testingaut.ipynb @@ -1,7 +1,23 @@ { "metadata": { - "name": "", - "signature": "sha256:1a85b698ebae51aaba0387d782d1cf5c6cdf54f69dd6b4b9c7189f8676eb4c88" + "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.3" + }, + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -58,36 +74,36 @@ "G\n", "\n", "\n", - "\n", - "1\n", + "\n", + "0\n", "\n", - "1\n", + "0\n", "\n", - "\n", - "I->1\n", + "\n", + "I->0\n", "\n", "\n", "\n", - "\n", - "1->1\n", + "\n", + "0->0\n", "\n", "\n", "a\n", "\n", - "\n", - "0\n", + "\n", + "1\n", "\n", "\n", - "0\n", + "1\n", "\n", - "\n", - "1->0\n", + "\n", + "0->1\n", "\n", "\n", "b\n", "\n", - "\n", - "0->0\n", + "\n", + "1->1\n", "\n", "\n", "b\n", @@ -96,7 +112,7 @@ "\n" ], "text": [ - " *' at 0x7f2e817bf6c0> >" + " *' at 0x7f99b4744e40> >" ] } ], @@ -125,240 +141,240 @@ "output_type": "pyout", "prompt_number": 3, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", - "\n", - "init\n", + "\n", + "init\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "1\n", - "!a & b\n", + "\n", + "0\n", + "!a & b\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "3\n", - "\n", - "1\n", - "a & b\n", + "\n", + "0\n", + "a & b\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "4\n", - "\n", - "1\n", - "a & !b\n", + "\n", + "0\n", + "a & !b\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "5\n", - "\n", - "\n", - "0\n", - "a & b\n", + "\n", + "\n", + "1\n", + "a & b\n", "\n", "\n", "2->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "6\n", - "\n", - "\n", - "0\n", - "!a & b\n", + "\n", + "\n", + "1\n", + "!a & b\n", "\n", "\n", "2->6\n", - "\n", - "\n", - "{}\n", + "\n", + "\n", + "{}\n", "\n", "\n", "7\n", - "\n", - "\n", - "0\n", - "a & !b\n", + "\n", + "\n", + "1\n", + "a & !b\n", "\n", "\n", "2->7\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "8\n", - "\n", - "\n", - "0\n", - "!a & !b\n", + "\n", + "\n", + "1\n", + "!a & !b\n", "\n", "\n", "2->8\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "{a}\n", + "3->2\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "{}\n", + "3->3\n", + "\n", + "\n", + "{}\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "{b}\n", + "3->4\n", + "\n", + "\n", + "{b}\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "{}\n", + "3->5\n", + "\n", + "\n", + "{}\n", "\n", "\n", - "3->6\n", - "\n", - "\n", - "{a}\n", + "3->6\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "3->7\n", - "\n", - "\n", - "{b}\n", + "3->7\n", + "\n", + "\n", + "{b}\n", "\n", "\n", - "3->8\n", - "\n", - "\n", - "{a, b}\n", + "3->8\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "9\n", - "\n", - "1\n", - "!a & !b\n", + "\n", + "0\n", + "!a & !b\n", "\n", "\n", - "3->9\n", - "\n", - "\n", - "{a, b}\n", + "3->9\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "4->2\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "{}\n", + "\n", + "\n", + "{}\n", "\n", "\n", "4->9\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "{}\n", + "\n", + "\n", + "{}\n", "\n", "\n", "5->6\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "5->7\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "5->8\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "{}\n", + "\n", + "\n", + "{}\n", "\n", "\n", "6->7\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "6->8\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], @@ -386,124 +402,124 @@ "output_type": "pyout", "prompt_number": 4, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", - "\n", - "init\n", + "\n", + "init\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "1\n", - "!a & b\n", + "\n", + "0\n", + "!a & b\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "3\n", - "\n", - "1\n", - "a & b\n", + "\n", + "0\n", + "a & b\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "4\n", - "\n", - "1\n", - "a & !b\n", + "\n", + "0\n", + "a & !b\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "5\n", - "\n", - "\n", - "0\n", - "a & b\n", + "\n", + "\n", + "1\n", + "a & b\n", "\n", "\n", "2->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "{a}\n", + "3->2\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "{b}\n", + "3->4\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "6\n", - "\n", - "\n", - "0\n", - "!a & b\n", + "\n", + "\n", + "1\n", + "!a & b\n", "\n", "\n", - "3->6\n", - "\n", - "\n", - "{a}\n", + "3->6\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "4->2\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "5->6\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], @@ -530,122 +546,114 @@ "output_type": "pyout", "prompt_number": 5, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", - "\n", - "init\n", + "\n", + "init\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "4\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "5\n", - "\n", - "\n", - "4\n", + "\n", + "\n", + "4\n", "\n", "\n", "2->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "{a}\n", + "3->2\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "{b}\n", + "3->4\n", + "\n", + "\n", + "{b}\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "{a}\n", + "3->5\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "4->2\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], "prompt_number": 5 - }, - { - "cell_type": "code", - "collapsed": false, - "input": [], - "language": "python", - "metadata": {}, - "outputs": [] } ], "metadata": {} } ] -} \ No newline at end of file +} diff --git a/tests/python/word.ipynb b/tests/python/word.ipynb index 7e554b7d3..d5e7e61ec 100644 --- a/tests/python/word.ipynb +++ b/tests/python/word.ipynb @@ -1,7 +1,23 @@ { "metadata": { - "name": "", - "signature": "sha256:4fc3934cf5fa0e612923dc4253b5e40115b103a93f588595a6706ec77e7994a9" + "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.3" + }, + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -31,7 +47,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "aut = spot.translate('G(Fa <-> Xb)'); aut" + "aut = spot.translate('G(Fa <-> XXb)'); aut" ], "language": "python", "metadata": {}, @@ -47,99 +63,150 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "a\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", - "\n", - "0->3\n", - "\n", - "\n", - "!a\n", + "\n", + "1->3\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!a & b\n", + "\n", + "4\n", + "\n", + "4\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "1->4\n", + "\n", + "\n", + "!a\n", "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!a & b\n", + "\n", + "5\n", + "\n", + "5\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "1->5\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & b\n", + "2->3\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "!a\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fb71c0e18a0> >" + " *' at 0x7fdf783f0510> >" ] } ], @@ -168,12 +235,12 @@ "text": [ "Prefix:\n", " 0\n", - " | !a\n", - "Cycle:\n", + " | a\n", " 1\n", - " | a & b\t{0}\n", - " 2\n", - " | !a & b" + " | a\n", + "Cycle:\n", + " 3\n", + " | a & b\t{0}" ] } ], @@ -200,7 +267,7 @@ "output_type": "stream", "stream": "stdout", "text": [ - "!a\n", + "a\n", "{0}\n" ] } @@ -228,7 +295,7 @@ "output_type": "pyout", "prompt_number": 5, "text": [ - "!a; cycle{a & b; !a & b}" + "a; a; cycle{a & b}" ] } ], @@ -246,8 +313,8 @@ "collapsed": false, "input": [ "print(spot.bdd_format_formula(aut.get_dict(), word.prefix[0]))\n", - "print(spot.bdd_format_formula(aut.get_dict(), word.cycle[0]))\n", - "print(spot.bdd_format_formula(aut.get_dict(), word.cycle[1]))" + "print(spot.bdd_format_formula(aut.get_dict(), word.prefix[1]))\n", + "print(spot.bdd_format_formula(aut.get_dict(), word.cycle[0]))" ], "language": "python", "metadata": {}, @@ -256,9 +323,9 @@ "output_type": "stream", "stream": "stdout", "text": [ - "!a\n", - "a & b\n", - "!a & b\n" + "a\n", + "a\n", + "a & b\n" ] } ], @@ -268,7 +335,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Calling `simplifify()` will produce a shorter word that is compatible with the original word. For instance in the above word, the initial `!a` is compatible with both `a & b` and `!a & b`. The word obtained by restricting `!a` to `!a & b` is therefore still accepted, but it allows removing the prefix by rotating the cycle:" + "Calling `simplifify()` will produce a shorter word that is compatible with the original word. For instance in the above word, the initial `a` is compatible with both `a & b` and `a & !b`. The word obtained by restricting `a` to `a & b` is therefore still accepted, allowing us to remove the prefix." ] }, { @@ -286,7 +353,7 @@ "output_type": "pyout", "prompt_number": 7, "text": [ - "cycle{!a & b; a & b}" + "cycle{a & b}" ] } ], @@ -313,7 +380,7 @@ "output_type": "pyout", "prompt_number": 8, "text": [ - "cycle{!a & b; a & b}" + "cycle{a & b}" ] } ], @@ -478,7 +545,7 @@ "\n" ], "text": [ - " *' at 0x7fb71c0e1a20> >" + " *' at 0x7fdf783f0e40> >" ] } ], @@ -598,9 +665,10 @@ "evalue": "a twa_word may not have an empty cycle", "output_type": "pyerr", "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mRuntimeError\u001b[0m Traceback (most recent call last)", + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mRuntimeError\u001b[0m Traceback (most recent call last)", "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[0;31m# ... as long as this word is not printed.\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 2\u001b[0;31m \u001b[0mprint\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mw\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", - "\u001b[0;32m/home/adl/git/spot/python/spot/impl.py\u001b[0m in \u001b[0;36m__str__\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 3599\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 3600\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0m__str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m->\u001b[0m \u001b[0;34m\"std::string\"\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 3601\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word___str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 3602\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 3603\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtwa_word\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m/home/adl/git/spot/python/spot/impl.py\u001b[0m in \u001b[0;36m__str__\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 4160\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 4161\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0m__str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m->\u001b[0m \u001b[0;34m\"std::string\"\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 4162\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word___str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 4163\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 4164\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtwa_word\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", "\u001b[0;31mRuntimeError\u001b[0m: a twa_word may not have an empty cycle" ] } @@ -611,4 +679,4 @@ "metadata": {} } ] -} \ No newline at end of file +}