diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index e59ed5e4a..2b4e51786 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; } @@ -446,10 +456,10 @@ 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()); @@ -472,14 +482,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)); @@ -613,12 +623,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'; @@ -646,9 +656,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 9c5c64dd9..63b9106e7 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -1692,7 +1692,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 dec25e75f..1c8ceacbf 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -15,10 +15,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.4.3+" + "version": "3.5.3" }, - "name": "", - "signature": "sha256:4ddb9b8fc1c41bacd7e47f70861303cde0ad425f842ade8e1f23ee74738914b0" + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -178,7 +177,7 @@ "\n" ], "text": [ - " *' at 0x7fe334de9900> >" + " *' at 0x7fb9189349f0> >" ] } ], @@ -317,7 +316,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -470,7 +469,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -570,7 +569,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c8331b0> >" + " *' at 0x7fb9188abd80> >" ] } ], @@ -640,7 +639,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c833060> >" + " *' at 0x7fb9188abe40> >" ] } ], @@ -716,7 +715,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c8330f0> >" + " *' at 0x7fb9188abdb0> >" ] } ], @@ -839,7 +838,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1029,7 +1028,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1062,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 0x7fe33c833300> >" + " *' at 0x7fb9188ab5d0> >" ] } ], @@ -1215,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 0x7fe33c8332d0> >" + " *' at 0x7fb9188abe10> >" ] } ], @@ -1335,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 0x7fe33c833120> >" + " *' at 0x7fb918910f60> >" ] } ], @@ -1494,7 +1493,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c833330> >" + " *' at 0x7fb9188abb70> >" ] } ], @@ -1964,7 +1963,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c8332a0> >" + " *' at 0x7fb9191c2720> >" ] } ], @@ -2161,7 +2160,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2286,149 +2285,149 @@ "" ], "text": [ - "" + "" ] }, { "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", "" ], "text": [ - "" + "" ] }, { @@ -2441,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 0x7fe334d5cae0> >" + " *' at 0x7fb918234300> >" ] } ], @@ -2735,7 +2734,7 @@ "\n" ], "text": [ - " *' at 0x7fe334d5cfc0> >" + " *' at 0x7fb918234270> >" ] } ], @@ -2805,7 +2804,7 @@ "\n" ], "text": [ - " *' at 0x7fe334d5cae0> >" + " *' at 0x7fb918234330> >" ] } ], @@ -2877,7 +2876,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2930,7 +2929,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -3042,7 +3041,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -3154,7 +3153,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -3169,7 +3168,7 @@ }, { "cell_type": "code", - "collapsed": true, + "collapsed": false, "input": [ "a = spot.translate('FGa')\n", "display(a)\n", @@ -3194,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", @@ -3232,7 +3231,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c833390> >" + " *' at 0x7fb9182341b0> >" ] }, { @@ -3280,7 +3279,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a\n", @@ -3291,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", @@ -3315,7 +3314,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -3400,7 +3399,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c747540> >" + " *' at 0x7fb9182344b0> >" ] } ], @@ -3410,7 +3409,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Adding an automatic proposition to all edges" + "Adding an atomic proposition to all edges" ] }, { @@ -3489,7 +3488,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c747540> >" + " *' at 0x7fb9182344b0> >" ] } ], @@ -3578,7 +3577,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c747540> >" + " *' at 0x7fb9182344b0> >" ] } ], @@ -3588,4 +3587,4 @@ "metadata": {} } ] -} \ No newline at end of file +} diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb index 68ea84c15..0518248d4 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> >" ] } ], diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 04b9c5699..8b7c41e57 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.3rc1" + "version": "3.5.3" }, "name": "" }, @@ -254,7 +254,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0b5ab70> >" + " *' at 0x7f98b673b870> >" ] } ], @@ -356,7 +356,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb270> >" + " *' at 0x7f98b66ad630> >" ] } ], @@ -571,7 +571,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb390> >" + " *' at 0x7f98b66ad300> >" ] } ], @@ -750,7 +750,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb390> >" + " *' at 0x7f98b66ad300> >" ] } ], @@ -830,7 +830,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb660> >" + " *' at 0x7f98b66ad7b0> >" ] }, { @@ -876,7 +876,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb300> >" + " *' at 0x7f98b66ad570> >" ] } ], @@ -962,7 +962,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb150> >" + " *' at 0x7f98b66ad750> >" ] } ], @@ -1087,7 +1087,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb150> >" + " *' at 0x7f98b66ad750> >" ] }, { @@ -1144,7 +1144,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb660> >" + " *' at 0x7f98b66ad7b0> >" ] }, { @@ -1190,7 +1190,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb300> >" + " *' at 0x7f98b66ad570> >" ] } ], @@ -1397,7 +1397,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb750> >" + " *' at 0x7f98b66ad510> >" ] }, { @@ -1471,7 +1471,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb630> >" + " *' at 0x7f98b66adb70> >" ] }, { @@ -1555,7 +1555,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb2d0> >" + " *' at 0x7f98b66ad3c0> >" ] } ], @@ -1701,7 +1701,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb810> >" + " *' at 0x7f98b66adcc0> >" ] } ], @@ -1846,7 +1846,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb810> >" + " *' at 0x7f98b66adcc0> >" ] } ], @@ -1989,7 +1989,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb810> >" + " *' 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", @@ -2317,26 +2317,26 @@ "\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,8 +2346,8 @@ "\n", "5\n", "\n", - "\n", - "3->5\n", + "\n", + "2->5\n", "\n", "\n", "!a & b & c\n", @@ -2358,14 +2358,14 @@ "\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/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 +}