From f5f5daec9ab661d14fdf547681e0d501aeecfc7e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 28 Jun 2018 23:02:26 +0200 Subject: [PATCH] translate: enable a restricted form of ltl-split for TGBA/BA Fixes #267 * spot/twaalgos/gfguarantee.cc: Fix a typo when comparing automata sizes. * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Use ltl-split even for BA/TGBA, but only of conjunctions with GF(..) in those cases. * tests/core/ltl2tgba2.test: Adjust and add the example of #267. * tests/core/degenid.test, tests/core/parity2.test, tests/core/stutter-tgba.test, tests/python/automata.ipynb, tests/python/highlighting.ipynb, tests/python/stutter-inv.ipynb, bin/spot-x.cc: Adjust. --- bin/spot-x.cc | 3 +- spot/twaalgos/gfguarantee.cc | 2 +- spot/twaalgos/translate.cc | 163 +++-- spot/twaalgos/translate.hh | 1 + tests/core/degenid.test | 8 +- tests/core/ltl2tgba2.test | 6 +- tests/core/parity2.test | 432 +++++-------- tests/core/stutter-tgba.test | 4 +- tests/python/automata.ipynb | 1035 +++++++++++++++---------------- tests/python/highlighting.ipynb | 1030 +++++++++++++++--------------- tests/python/stutter-inv.ipynb | 148 ++--- 11 files changed, 1338 insertions(+), 1494 deletions(-) diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 6d9a446dc..7225d751c 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -46,8 +46,7 @@ more rules based on automata-based implication checks. The default value \ depends on the --low/--medium/--high settings.") }, { nullptr, 0, nullptr, 0, "Translation options:", 0 }, { DOC("ltl-split", "Set to 0 to disable the translation of automata \ -as product or sum of subformulas. This is currently used only when \ -building automata with generic acceptance conditions.") }, +as product or sum of subformulas.") }, { DOC("comp-susp", "Set to 1 to enable compositional suspension, \ as described in our SPIN'13 paper (see Bibliography below). Set to 2, \ to build only the skeleton TGBA without composing it. Set to 0 (the \ diff --git a/spot/twaalgos/gfguarantee.cc b/spot/twaalgos/gfguarantee.cc index 0c37cbf44..9d6ab7d98 100644 --- a/spot/twaalgos/gfguarantee.cc +++ b/spot/twaalgos/gfguarantee.cc @@ -418,7 +418,7 @@ namespace spot if (!is_terminal_automaton(aut, &si2, true)) return reduced; do_g_f_terminal_inplace(si2, state_based); - if (aut->num_states() <= reduced->num_states()) + if (aut->num_states() < reduced->num_states()) return aut; } return reduced; diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 0e054c912..6899adbf8 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -105,7 +105,8 @@ namespace spot simpl_owned_ = simpl_ = new tl_simplifier(options, dict); } - twa_graph_ptr translator::run(formula* f) + + twa_graph_ptr translator::run_aux(formula r) { #define PREF_ (pref_ & (Small | Deterministic)) @@ -118,49 +119,6 @@ namespace spot set_pref(pref_ | postprocessor::Deterministic); } - // Do we want to relabel Boolean subformulas? - // If we have a huge formula such as - // (a1 & a2 & ... & an) U (b1 | b2 | ... | bm) - // then it is more efficient to translate - // a U b - // and then fix the automaton. We use relabel_bse() to find - // sub-formulas that are Boolean but do not have common terms. - // - // This rewriting is enabled only if the formula - // 1) has some Boolean subformula - // 2) has more than relabel_bool_ atomic propositions (the default - // is 4, but this can be changed) - // 3) relabel_bse() actually reduces the number of atomic - // propositions. - relabeling_map m; - formula to_work_on = *f; - if (relabel_bool_ > 0) - { - bool has_boolean_sub = false; // that is not atomic - std::set aps; - to_work_on.traverse([&](const formula& f) - { - if (f.is(op::ap)) - aps.insert(f); - else if (f.is_boolean()) - has_boolean_sub = true; - return false; - }); - unsigned atomic_props = aps.size(); - if (has_boolean_sub && (atomic_props >= (unsigned) relabel_bool_)) - { - formula relabeled = relabel_bse(to_work_on, Pnn, &m); - if (m.size() < atomic_props) - to_work_on = relabeled; - else - m.clear(); - } - } - - formula r = simpl_->simplify(to_work_on); - if (to_work_on == *f) - *f = r; - // This helps ltl_to_tgba_fm() to order BDD variables in a more // natural way (improving the degeneralization). simpl_->clear_as_bdd_cache(); @@ -168,8 +126,7 @@ namespace spot twa_graph_ptr aut; twa_graph_ptr aut2 = nullptr; - if (ltl_split_ && (type_ == Generic - || (type_ & Parity)) && !r.is_syntactic_obligation()) + if (ltl_split_ && !r.is_syntactic_obligation()) { formula r2 = r; unsigned leading_x = 0; @@ -178,11 +135,11 @@ namespace spot r2 = r2[0]; ++leading_x; } - if (type_ == Generic) + if (type_ == Generic || type_ == TGBA) { - // F(q|u|f) = q|F(u)|F(f) + // F(q|u|f) = q|F(u)|F(f) only for generic acceptance // G(q&e&f) = q&G(e)&G(f) - bool want_u = r2.is({op::F, op::Or}); + bool want_u = r2.is({op::F, op::Or}) && (type_ == Generic); if (want_u || r2.is({op::G, op::And})) { std::vector susp; @@ -204,7 +161,12 @@ namespace spot r2 = formula::multop(op2, susp); } } - if (r2.is_syntactic_obligation() || !r2.is(op::And, op::Or)) + if (r2.is_syntactic_obligation() || !r2.is(op::And, op::Or) || + // For TGBA/BA we only do conjunction. There is nothing wrong + // with disjunction, but it seems to generated larger automata + // in many cases and it needs to be further investigated. Maybe + // this could be relaxed in the case of deterministic output. + (r2.is(op::Or) && (type_ == TGBA || type_ == BA))) goto nosplit; bool is_and = r2.is(op::And); @@ -212,16 +174,38 @@ namespace spot std::vector oblg; std::vector susp; std::vector rest; + bool want_g = type_ == TGBA || type_ == BA; for (formula child: r2) { if (child.is_syntactic_obligation()) oblg.push_back(child); else if (child.is_eventual() && child.is_universal() - && (type_ == Generic)) + && (!want_g || child.is(op::G))) susp.push_back(child); else rest.push_back(child); } + + if (!susp.empty()) + { + // The only cases where we accept susp and rest to be both + // non-empty is when doing arbitrary acceptance, or when doing + // Generic or TGBA. + if (!rest.empty() && !(type_ == Generic || type_ == TGBA)) + { + rest.insert(rest.end(), susp.begin(), susp.end()); + susp.clear(); + } + // For Parity, we want to translate all suspendable + // formulas at once. + if (rest.empty() && type_ & Parity) + susp = { formula::multop(r2.kind(), susp) }; + } + // For TGBA and BA, we only split if there is something to + // suspend. + if (susp.empty() && (type_ == TGBA || type_ == BA)) + goto nosplit; + option_map om; if (opt_) om = *opt_; @@ -238,34 +222,26 @@ namespace spot return run(f); }; + // std::cerr << "splitting\n"; aut = nullptr; // All obligations can be converted into a minimal WDBA. if (!oblg.empty()) { formula oblg_f = formula::multop(r2.kind(), oblg); + //std::cerr << "oblg: " << oblg_f << '\n'; aut = transrun(oblg_f); } if (!rest.empty()) { formula rest_f = formula::multop(r2.kind(), rest); - // In case type_ is Parity, all suspendable formulas have - // been put into rest_f. But if the entire rest_f is - // suspendable, we want to handle it like so. - if (rest_f.is_eventual() && rest_f.is_universal()) - { - assert(susp.empty()); - susp.push_back(rest_f); - } + //std::cerr << "rest: " << rest_f << '\n'; + twa_graph_ptr rest_aut = transrun(rest_f); + if (aut == nullptr) + aut = rest_aut; + else if (is_and) + aut = product(aut, rest_aut); else - { - twa_graph_ptr rest_aut = transrun(rest_f); - if (aut == nullptr) - aut = rest_aut; - else if (is_and) - aut = product(aut, rest_aut); - else - aut = product_or(aut, rest_aut); - } + aut = product_or(aut, rest_aut); } if (!susp.empty()) { @@ -273,6 +249,7 @@ namespace spot // Each suspendable formula separately for (formula f: susp) { + //std::cerr << "susp: " << f << '\n'; twa_graph_ptr one = transrun(f); if (!susp_aut) susp_aut = one; @@ -370,6 +347,56 @@ namespace spot aut = std::move(aut2); } + return aut; + } + + twa_graph_ptr translator::run(formula* f) + { + // Do we want to relabel Boolean subformulas? + // If we have a huge formula such as + // (a1 & a2 & ... & an) U (b1 | b2 | ... | bm) + // then it is more efficient to translate + // a U b + // and then fix the automaton. We use relabel_bse() to find + // sub-formulas that are Boolean but do not have common terms. + // + // This rewriting is enabled only if the formula + // 1) has some Boolean subformula + // 2) has more than relabel_bool_ atomic propositions (the default + // is 4, but this can be changed) + // 3) relabel_bse() actually reduces the number of atomic + // propositions. + relabeling_map m; + formula to_work_on = *f; + if (relabel_bool_ > 0) + { + bool has_boolean_sub = false; // that is not atomic + std::set aps; + to_work_on.traverse([&](const formula& f) + { + if (f.is(op::ap)) + aps.insert(f); + else if (f.is_boolean()) + has_boolean_sub = true; + return false; + }); + unsigned atomic_props = aps.size(); + if (has_boolean_sub && (atomic_props >= (unsigned) relabel_bool_)) + { + formula relabeled = relabel_bse(to_work_on, Pnn, &m); + if (m.size() < atomic_props) + to_work_on = relabeled; + else + m.clear(); + } + } + + formula r = simpl_->simplify(to_work_on); + if (to_work_on == *f) + *f = r; + + auto aut = run_aux(r); + if (!m.empty()) relabel_here(aut, &m); return aut; diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh index 0f0ff18be..7e4aadf9a 100644 --- a/spot/twaalgos/translate.hh +++ b/spot/twaalgos/translate.hh @@ -138,6 +138,7 @@ namespace spot protected: void setup_opt(const option_map* opt); void build_simplifier(const bdd_dict_ptr& dict); + twa_graph_ptr run_aux(formula f); private: tl_simplifier* simpl_; diff --git a/tests/core/degenid.test b/tests/core/degenid.test index 8e69a35c8..b13162685 100755 --- a/tests/core/degenid.test +++ b/tests/core/degenid.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2011, 2013, 2014, 2015, 2017 Laboratoire de Recherche -# et Développement de l'Epita (LRDE). +# Copyright (C) 2011, 2013, 2014, 2015, 2017, 2018 Laboratoire de +# Recherche et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -239,7 +239,9 @@ properties: trans-labels explicit-labels state-acc deterministic properties: stutter-invariant --BODY-- State: 0 -[0] 1 +[0&1&2] 1 +[0&!2] 2 +[0&!1&2] 3 State: 1 {0} [1&2] 1 [!2] 2 diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index d2b8e87fe..b48c1b448 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -362,12 +362,14 @@ EOF diff output expected -# These four formulas appear in a NEWS entry for Spot 2.6 +# The first four formulas appear in a NEWS entry for Spot 2.6 +# The 5th one is from issue #267. cat >formulas < pos.hoa ltl2tgba 'FG(a | Xa | G!a)' -H | autfilt -H --destut > neg.hoa autfilt pos.hoa --product neg.hoa -H > prod.hoa autfilt --is-empty prod.hoa -q && exit 1 -autfilt --states=7 prod.hoa -q +autfilt --states=5 prod.hoa -q ltl2tgba '!FG(a | Xa | G!a)' -H | autfilt -H --instut > pos.hoa ltl2tgba 'FG(a | Xa | G!a)' -H | autfilt -H --instut > neg.hoa autfilt pos.hoa --product neg.hoa -H > prod.hoa autfilt --is-empty prod.hoa -q && exit 1 -autfilt --states=9 prod.hoa -q +autfilt --states=6 prod.hoa -q # Check for issue #7. diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index b91991215..3128236d4 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -33,138 +33,152 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "b & c & d\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b & !d\n", "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "b & !c & d\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!d\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "!c & d\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", - "\n", + "\n", "2->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", - "\n", + "\n", "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fa7cc23af60> >" + " *' at 0x7effe06cf120> >" ] }, "execution_count": 2, @@ -191,131 +205,145 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "b & c & d\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b & !d\n", "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "b & !c & d\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!d\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "!c & d\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", - "\n", + "\n", "2->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", - "\n", + "\n", "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", "\n", "\n", "" @@ -348,148 +376,162 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "cluster_0\n", - "\n", + "\n", "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "\n", "cluster_2\n", - "\n", + "\n", "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "c & d\n", - "\n", + "\n", + "\n", + "b & c & d\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!d\n", - "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b & !d\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "b & !c & d\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!d\n", + "\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "!c & d\n", - "\n", + "\n", + "\n", + "!c & d\n", + "\n", "\n", "\n", - "\n", + "\n", "2->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", - "\n", + "\n", "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", - "\n", + "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "" @@ -601,7 +643,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc0e9db0> >" + " *' at 0x7effe05eda80> >" ] }, "execution_count": 6, @@ -677,7 +719,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc0fabd0> >" + " *' at 0x7effe05edab0> >" ] }, "execution_count": 7, @@ -760,7 +802,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc1ce060> >" + " *' at 0x7effe05edae0> >" ] }, "execution_count": 8, @@ -956,16 +998,16 @@ "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "!a & b & c\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "\n", @@ -984,16 +1026,16 @@ "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "!a & b & c\n", "\n", "\n", "\n", @@ -1030,40 +1072,40 @@ "\n", "c\n", "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!b & c\n", - "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "b & !c\n", + "\n", + "\n", + "a\n", "\n", "\n", - "\n", + "\n", "2->2\n", "\n", "\n", "b\n", "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "b & !c\n", + "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "b & c\n", "\n", "\n", "\n", @@ -1072,9 +1114,9 @@ "\n", "!a & c\n", "\n", - "\n", + "\n", "\n", - "4->3\n", + "4->1\n", "\n", "\n", "a & !c\n", @@ -1086,20 +1128,20 @@ "\n", "a & c\n", "\n", - "\n", + "\n", "\n", + "5->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", "5->2\n", "\n", "\n", "!a & b\n", "\n", - "\n", - "\n", - "5->3\n", - "\n", - "\n", - "a & !b\n", - "\n", "\n", "\n", "5->5\n", @@ -1279,7 +1321,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc10a930> >" + " *' at 0x7effe05edba0> >" ] }, "execution_count": 12, @@ -1393,7 +1435,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc10aab0> >" + " *' at 0x7effe05edcf0> >" ] }, "execution_count": 13, @@ -1524,7 +1566,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc10ab40> >" + " *' at 0x7effe05ed930> >" ] }, "execution_count": 14, @@ -1743,7 +1785,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc10a270> >" + " *' at 0x7effe05eda50> >" ] }, "metadata": {}, @@ -1893,7 +1935,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc0e9b40> >" + " *' at 0x7effe06cf0c0> >" ] }, "metadata": {}, @@ -2065,7 +2107,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc10abd0> >" + " *' at 0x7effe05edb40> >" ] }, "metadata": {}, @@ -2240,7 +2282,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc10aae0> >" + " *' at 0x7effe05edbd0> >" ] }, "metadata": {}, @@ -2426,7 +2468,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc10acf0> >" + " *' at 0x7effe05ed870> >" ] }, "execution_count": 19, @@ -2502,7 +2544,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc10a990> >" + " *' at 0x7effe05ed8d0> >" ] }, "execution_count": 20, @@ -2574,7 +2616,7 @@ "0->0\n", "\n", "\n", - "!a\n", + "a\n", "\n", "\n", "\n", @@ -2588,21 +2630,21 @@ "0->1\n", "\n", "\n", - "a\n", + "!a\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", - "!a\n", + "a\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", - "a\n", + "!a\n", "\n", "\n", "\n", @@ -2674,316 +2716,257 @@ { "data": { "text/html": [ - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "
\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "0,1\n", + "\n", + "0,1\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!a & b\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "1,0\n", + "\n", + "1,1\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "1,1\n", - "\n", - "\n", "\n", - "0->3\n", - "\n", - "\n", - "a & b\n", + "0->2\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a & !c\n", - "\n", + "\n", + "\n", + "a & !c\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & !c\n", + "1->2\n", + "\n", + "\n", + "!a & !c\n", "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & c\n", - "\n", + "1->2\n", + "\n", + "\n", + "!a & c\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & c\n", + "\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & b\n", - "\n", + "2->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", "\n", - "\n", + "\n", "\n", - "3->1\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & !c\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & c\n", - "\n", - "\n", + "2->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", "\n", "\n", - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "
\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", "0\n", "\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "1\n", "\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!a & b\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "\n", "\n", - "0->3\n", - "\n", - "\n", - "a & b\n", + "0->2\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a & !c\n", - "\n", + "\n", + "\n", + "a & !c\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & !c\n", + "1->2\n", + "\n", + "\n", + "!a & !c\n", "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & c\n", - "\n", + "1->2\n", + "\n", + "\n", + "!a & c\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & c\n", + "\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & b\n", - "\n", + "2->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", "\n", - "\n", + "\n", "\n", - "3->1\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & !c\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & c\n", - "\n", - "\n", + "2->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", "\n", "\n", "
" @@ -3079,7 +3062,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc096c00> >" + " *' at 0x7effe05ed9c0> >" ] }, "metadata": {}, @@ -3179,7 +3162,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc096390> >" + " *' at 0x7effe05ed9f0> >" ] }, "execution_count": 24, @@ -3252,7 +3235,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc0e9ba0> >" + " *' at 0x7effe05eda20> >" ] }, "execution_count": 25, @@ -3416,7 +3399,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc096f00> >" + " *' at 0x7effe05edb40> >" ] }, "execution_count": 27, @@ -3499,7 +3482,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc096c00> >" + " *' at 0x7effe05ed9c0> >" ] }, "metadata": {}, @@ -3564,7 +3547,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc096c00> >" + " *' at 0x7effe05ed9c0> >" ] }, "metadata": {}, @@ -3651,7 +3634,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7cc096c00> >" + " *' at 0x7effe05ed9c0> >" ] }, "execution_count": 29, @@ -3684,7 +3667,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5+" + "version": "3.6.6" } }, "nbformat": 4, diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index c1f693507..1bccb69c5 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -240,7 +240,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a240ef0f0> >" + " *' at 0x7f7d6b72ef90> >" ] }, "execution_count": 4, @@ -352,7 +352,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a1d7ce8a0> >" + " *' at 0x7f7d6b654870> >" ] }, "execution_count": 5, @@ -462,7 +462,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a240ef0f0> >" + " *' at 0x7f7d6b72ef90> >" ] }, "execution_count": 6, @@ -576,117 +576,117 @@ ")\n", "[Büchi]\n", "\n", - "\n", + "\n", "\n", - "0\n", + "4\n", "\n", - "0\n", + "4\n", "\n", - "\n", + "\n", "\n", - "I->0\n", + "I->4\n", "\n", "\n", "\n", - "\n", + "\n", "\n", - "1\n", + "0\n", "\n", - "1\n", + "0\n", "\n", - "\n", - "\n", - "0->1\n", + "\n", + "\n", + "4->0\n", "\n", "\n", "1\n", "\n", - "\n", - "\n", - "1->1\n", + "\n", + "\n", + "0->0\n", "\n", "\n", "a | b\n", "\n", - "\n", + "\n", "\n", - "2\n", + "1\n", "\n", - "2\n", + "1\n", "\n", - "\n", - "\n", - "1->2\n", + "\n", + "\n", + "0->1\n", "\n", "\n", "!a & !b\n", "\n", - "\n", + "\n", "\n", - "3\n", + "2\n", "\n", - "3\n", + "2\n", "\n", - "\n", - "\n", - "1->3\n", + "\n", + "\n", + "0->2\n", "\n", "\n", "a & b\n", "\n", - "\n", + "\n", "\n", - "4\n", + "3\n", "\n", - "4\n", + "3\n", "\n", - "\n", - "\n", - "1->4\n", + "\n", + "\n", + "0->3\n", "\n", "\n", "a & !b\n", "\n", - "\n", - "\n", - "2->2\n", + "\n", + "\n", + "1->1\n", "\n", "\n", "!b\n", "\n", "\n", - "\n", - "\n", - "2->2\n", + "\n", + "\n", + "1->1\n", "\n", "\n", "b\n", "\n", - "\n", - "\n", - "3->3\n", + "\n", + "\n", + "2->2\n", "\n", "\n", "a & !b\n", "\n", "\n", - "\n", - "\n", - "3->3\n", + "\n", + "\n", + "2->2\n", "\n", "\n", "a & b\n", "\n", - "\n", - "\n", - "4->2\n", + "\n", + "\n", + "3->1\n", "\n", "\n", "!a & b\n", "\n", - "\n", - "\n", - "4->4\n", + "\n", + "\n", + "3->3\n", "\n", "\n", "a & b\n", @@ -695,7 +695,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a1d7ce8d0> >" + " *' at 0x7f7d6b6542a0> >" ] }, "execution_count": 8, @@ -716,12 +716,12 @@ "data": { "text/plain": [ "Prefix:\n", - " 0\n", + " 4\n", " | 1\n", - " 1\n", + " 0\n", " | !a & !b\n", "Cycle:\n", - " 2\n", + " 1\n", " | !b\t{0}" ] }, @@ -773,117 +773,117 @@ ")\n", "[Büchi]\n", "\n", - "\n", + "\n", "\n", - "0\n", + "4\n", "\n", - "0\n", + "4\n", "\n", - "\n", + "\n", "\n", - "I->0\n", + "I->4\n", "\n", "\n", "\n", - "\n", + "\n", "\n", - "1\n", + "0\n", "\n", - "1\n", + "0\n", "\n", - "\n", - "\n", - "0->1\n", + "\n", + "\n", + "4->0\n", "\n", "\n", "1\n", "\n", - "\n", - "\n", - "1->1\n", + "\n", + "\n", + "0->0\n", "\n", "\n", "a | b\n", "\n", - "\n", + "\n", "\n", - "2\n", + "1\n", "\n", - "2\n", + "1\n", "\n", - "\n", - "\n", - "1->2\n", + "\n", + "\n", + "0->1\n", "\n", "\n", "!a & !b\n", "\n", - "\n", + "\n", "\n", - "3\n", + "2\n", "\n", - "3\n", + "2\n", "\n", - "\n", - "\n", - "1->3\n", + "\n", + "\n", + "0->2\n", "\n", "\n", "a & b\n", "\n", - "\n", + "\n", "\n", - "4\n", + "3\n", "\n", - "4\n", + "3\n", "\n", - "\n", - "\n", - "1->4\n", + "\n", + "\n", + "0->3\n", "\n", "\n", "a & !b\n", "\n", - "\n", - "\n", - "2->2\n", + "\n", + "\n", + "1->1\n", "\n", "\n", "!b\n", "\n", "\n", - "\n", - "\n", - "2->2\n", + "\n", + "\n", + "1->1\n", "\n", "\n", "b\n", "\n", - "\n", - "\n", - "3->3\n", + "\n", + "\n", + "2->2\n", "\n", "\n", "a & !b\n", "\n", "\n", - "\n", - "\n", - "3->3\n", + "\n", + "\n", + "2->2\n", "\n", "\n", "a & b\n", "\n", - "\n", - "\n", - "4->2\n", + "\n", + "\n", + "3->1\n", "\n", "\n", "!a & b\n", "\n", - "\n", - "\n", - "4->4\n", + "\n", + "\n", + "3->3\n", "\n", "\n", "a & b\n", @@ -892,7 +892,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a1d7ce8d0> >" + " *' at 0x7f7d6b6542a0> >" ] }, "execution_count": 11, @@ -977,7 +977,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a1d7ce060> >" + " *' at 0x7f7d6b654ab0> >" ] }, "metadata": {}, @@ -1032,7 +1032,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a240e6f60> >" + " *' at 0x7f7d6b654960> >" ] }, "metadata": {}, @@ -1126,7 +1126,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a1d7ce9f0> >" + " *' at 0x7f7d6b654990> >" ] }, "execution_count": 13, @@ -1257,7 +1257,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a1d7ce9f0> >" + " *' at 0x7f7d6b654990> >" ] }, "metadata": {}, @@ -1322,7 +1322,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a1d7ce060> >" + " *' at 0x7f7d6b654ab0> >" ] }, "metadata": {}, @@ -1377,7 +1377,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a240e6f60> >" + " *' at 0x7f7d6b654960> >" ] }, "metadata": {}, @@ -1609,7 +1609,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a1d7bdae0> >" + " *' at 0x7f7d6b654930> >" ] }, "metadata": {}, @@ -1694,7 +1694,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a1d7bd4b0> >" + " *' at 0x7f7d6b654ba0> >" ] }, "metadata": {}, @@ -1791,7 +1791,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a1d7ceb40> >" + " *' at 0x7f7d6b654a80> >" ] }, "metadata": {}, @@ -1840,117 +1840,117 @@ ")\n", "[Büchi]\n", "\n", - "\n", + "\n", "\n", - "0\n", + "4\n", "\n", - "0\n", + "4\n", "\n", - "\n", + "\n", "\n", - "I->0\n", + "I->4\n", "\n", "\n", "\n", - "\n", + "\n", "\n", - "1\n", + "0\n", "\n", - "1\n", + "0\n", "\n", - "\n", - "\n", - "0->1\n", + "\n", + "\n", + "4->0\n", "\n", "\n", "1\n", "\n", - "\n", - "\n", - "1->1\n", + "\n", + "\n", + "0->0\n", "\n", "\n", "a | b\n", "\n", - "\n", + "\n", "\n", - "2\n", + "1\n", "\n", - "2\n", + "1\n", "\n", - "\n", - "\n", - "1->2\n", + "\n", + "\n", + "0->1\n", "\n", "\n", "!a & !b\n", "\n", - "\n", + "\n", "\n", - "3\n", + "2\n", "\n", - "3\n", + "2\n", "\n", - "\n", - "\n", - "1->3\n", + "\n", + "\n", + "0->2\n", "\n", "\n", "a & b\n", "\n", - "\n", + "\n", "\n", - "4\n", + "3\n", "\n", - "4\n", + "3\n", "\n", - "\n", - "\n", - "1->4\n", + "\n", + "\n", + "0->3\n", "\n", "\n", "a & !b\n", "\n", - "\n", - "\n", - "2->2\n", + "\n", + "\n", + "1->1\n", "\n", "\n", "!b\n", "\n", "\n", - "\n", - "\n", - "2->2\n", + "\n", + "\n", + "1->1\n", "\n", "\n", "b\n", "\n", - "\n", - "\n", - "3->3\n", + "\n", + "\n", + "2->2\n", "\n", "\n", "a & !b\n", "\n", "\n", - "\n", - "\n", - "3->3\n", + "\n", + "\n", + "2->2\n", "\n", "\n", "a & b\n", "\n", - "\n", - "\n", - "4->2\n", + "\n", + "\n", + "3->1\n", "\n", "\n", "!a & b\n", "\n", - "\n", - "\n", - "4->4\n", + "\n", + "\n", + "3->3\n", "\n", "\n", "a & b\n", @@ -1959,7 +1959,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a1d7ced50> >" + " *' at 0x7f7d6b654d20> >" ] }, "execution_count": 18, @@ -1999,135 +1999,135 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", - "\n", + "\n", "\n", - "4\n", - "\n", - "4\n", + "3\n", + "\n", + "3\n", "\n", - "\n", + "\n", "\n", - "I->4\n", - "\n", - "\n", + "I->3\n", + "\n", + "\n", "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", "\n", - "\n", - "\n", - "4->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "a & b\n", "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "!b\n", + "\n", "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & !b\n", + "1->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", + "\n", "2\n", "\n", "2\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & b\n", + "2->1\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", + "\n", + "\n", "a & b\n", "\n", - "\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !b\n", - "\n", + "4->1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f6a1d7ced50> >" + " *' at 0x7f7d6b654d20> >" ] }, "execution_count": 19, @@ -2162,135 +2162,135 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", - "\n", + "\n", "\n", - "4\n", - "\n", - "4\n", + "3\n", + "\n", + "3\n", "\n", - "\n", + "\n", "\n", - "I->4\n", - "\n", - "\n", + "I->3\n", + "\n", + "\n", "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", "\n", - "\n", - "\n", - "4->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "a & b\n", "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "!b\n", + "\n", "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & !b\n", + "1->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", + "\n", "2\n", "\n", "2\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & b\n", + "2->1\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", + "\n", + "\n", "a & b\n", "\n", - "\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !b\n", - "\n", + "4->1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f6a1d7ced50> >" + " *' at 0x7f7d6b654d20> >" ] }, "metadata": {}, @@ -2299,117 +2299,112 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "4\n", + "\n", + "3\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "4\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "\n", "u1\n", - "\n", - "...\n", + "\n", + "...\n", "\n", "\n", "\n", "1->u1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "3\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "1->2\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "3\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "b\n", "\n", - "\n", - "\n", - "u2\n", - "\n", - "...\n", - "\n", - "\n", - "\n", - "2->u2\n", - "\n", - "\n", - "\n", - "\n", + "\n", "\n", - "3->3\n", - "\n", - "\n", - "a & b\n", + "3->2\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "" @@ -2436,7 +2431,7 @@ "\n", "0\n", "\n", - "4\n", + "3\n", "\n", "\n", "\n", @@ -2448,7 +2443,7 @@ "\n", "1\n", "\n", - "1\n", + "4\n", "\n", "\n", "\n", @@ -2509,24 +2504,24 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "cluster_0\n", - "\n", + "\n", "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "\n", "cluster_2\n", - "\n", + "\n", "\n", "\n", "cluster_3\n", @@ -2534,7 +2529,7 @@ "\n", "\n", "cluster_4\n", - "\n", + "\n", "\n", "\n", "cluster_5\n", @@ -2556,28 +2551,28 @@ "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", @@ -2588,216 +2583,216 @@ "\n", "\n", "0->3\n", - "\n", + "\n", "\n", "!a & !b\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & b & c\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "!a & b & c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a | !b\n", + "\n", + "\n", + "a | !b\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & b\n", - "\n", + "\n", + "\n", + "!a & b\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "b & !c\n", + "\n", + "\n", + "b & c\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", - "b & c\n", + "\n", + "\n", + "b & !c\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", - "b & !c\n", - "\n", + "\n", + "\n", + "b & c\n", "\n", "\n", "\n", "7->7\n", - "\n", - "\n", - "!b & c\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", "\n", "7->7\n", - "\n", - "\n", - "b & c\n", - "\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & c\n", "\n", "\n", "\n", "3->7\n", - "\n", - "\n", - "a & c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & c\n", "\n", "\n", "\n", "4->7\n", - "\n", - "\n", - "a & c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & b & c\n", + "\n", "\n", "\n", "\n", "4->5\n", - "\n", - "\n", - "!a & b & c\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", "\n", "\n", "\n", "5->6\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & c\n", "\n", "\n", "\n", "5->7\n", - "\n", - "\n", - "a & c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "5->3\n", - "\n", - "\n", + "\n", + "\n", "!a & !b\n", "\n", "\n", "\n", "5->4\n", - "\n", - "\n", - "!a & b & !c\n", - "\n", + "\n", + "\n", + "!a & b & c\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "!a & b & c\n", - "\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "" @@ -2816,13 +2811,6 @@ "spot.highlight_languages(aut)\n", "aut.show('.bas')" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { @@ -2841,7 +2829,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5+" + "version": "3.6.6" } }, "nbformat": 4, diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb index 9d4c8b999..5c9e12e84 100644 --- a/tests/python/stutter-inv.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -302,7 +302,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f31a00c1660> >" + " *' at 0x7f68605f5630> >" ] }, "metadata": {}, @@ -595,7 +595,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f31a00c1b40> >" + " *' at 0x7f68605f5ae0> >" ] }, "metadata": {}, @@ -804,7 +804,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f31a00c1b40> >" + " *' at 0x7f68605f5ae0> >" ] }, "metadata": {}, @@ -890,18 +890,18 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G(F(a & Xa) & F!a)\n", - "\n", - "G(F(a & Xa) & F!a)\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "G(F(a & Xa) & F!a)\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", @@ -918,17 +918,10 @@ "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", @@ -937,33 +930,33 @@ "1\n", "\n", "\n", - "\n", + "\n", "0->1\n", "\n", "\n", - "a\n", - "\n", + "!a\n", + "\n", "\n", "\n", - "\n", + "\n", "1->0\n", "\n", "\n", "a\n", "\n", "\n", - "\n", + "\n", "1->1\n", "\n", "\n", - "a\n", - "\n", + "!a\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f31a00c1630> >" + " *' at 0x7f68605f5a50> >" ] }, "metadata": {}, @@ -1061,7 +1054,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f31a0114060> >" + " *' at 0x7f68605f5b70> >" ] }, "metadata": {}, @@ -1101,18 +1094,18 @@ "\n", "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")) | Inf(\n", - "\n", - ")\n", - "[Fin-less 3]\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) | Inf(\n", + "\n", + ")\n", + "[Fin-less 3]\n", "\n", "\n", "\n", @@ -1133,11 +1126,11 @@ "0\n", "\n", "\n", - "\n", + "\n", "5->0\n", "\n", "\n", - "1\n", + "a\n", "\n", "\n", "\n", @@ -1146,11 +1139,11 @@ "1\n", "\n", "\n", - "\n", + "\n", "5->1\n", "\n", "\n", - "a\n", + "!a\n", "\n", "\n", "\n", @@ -1159,7 +1152,7 @@ "2\n", "\n", "\n", - "\n", + "\n", "5->2\n", "\n", "\n", @@ -1194,64 +1187,57 @@ "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", - "\n", + "\n", "0->1\n", "\n", "\n", - "a\n", - "\n", + "!a\n", + "\n", "\n", "\n", - "\n", + "\n", "1->0\n", "\n", "\n", "a\n", "\n", "\n", - "\n", + "\n", "1->1\n", "\n", "\n", - "a\n", - "\n", + "!a\n", + "\n", "\n", "\n", - "\n", + "\n", "2->2\n", "\n", "\n", "1\n", "\n", "\n", - "\n", + "\n", "2->3\n", "\n", "\n", "!a\n", "\n", "\n", - "\n", + "\n", "2->4\n", "\n", "\n", "a\n", "\n", "\n", - "\n", + "\n", "3->3\n", "\n", "\n", @@ -1259,7 +1245,7 @@ "\n", "\n", "\n", - "\n", + "\n", "3->4\n", "\n", "\n", @@ -1267,7 +1253,7 @@ "\n", "\n", "\n", - "\n", + "\n", "4->3\n", "\n", "\n", @@ -1278,7 +1264,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f31a00c1480> >" + " *' at 0x7f68605f5ba0> >" ] }, "metadata": {}, @@ -1407,7 +1393,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f31a01140c0> >" + " *' at 0x7f686063ef30> >" ] }, "metadata": {}, @@ -1538,7 +1524,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f31a00c1ae0> >" + " *' at 0x7f6860602930> >" ] }, "metadata": {}, @@ -1798,7 +1784,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f31a005d870> >" + " *' at 0x7f6860591c30> >" ] }, "metadata": {}, @@ -2112,7 +2098,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f31a005d870> >" + " *' at 0x7f6860591c30> >" ] }, "metadata": {}, @@ -2353,7 +2339,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5+" + "version": "3.6.6" } }, "nbformat": 4,