From 4815a361def303d8a1dfbaa8b49b2df00eb792c1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 19 Jun 2018 16:42:30 +0200 Subject: [PATCH] translate: add ltl-split option * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Build automata with generic acceptance by doing product of automata for smaller subformulas. * bin/spot-x.cc: Mention ltl-split. * NEWS: Mention the change, and show some results. * tests/core/genltl.test, tests/python/_product_susp.ipynb, tests/python/highlighting.ipynb: Adjust test cases. * doc/org/ltl2tgba.org: Update. * tests/core/gragsa.test: Add another formula to cover more code. --- NEWS | 36 +++ bin/spot-x.cc | 3 + doc/org/ltl2tgba.org | 81 ++++-- spot/twaalgos/translate.cc | 171 ++++++++++-- spot/twaalgos/translate.hh | 2 + tests/core/genltl.test | 40 +-- tests/core/gragsa.test | 6 +- tests/python/_product_susp.ipynb | 455 ++++++++++++++----------------- tests/python/highlighting.ipynb | 441 +++++++++++++++++------------- 9 files changed, 736 insertions(+), 499 deletions(-) diff --git a/NEWS b/NEWS index a8ecc27b2..9fa1a4a2f 100644 --- a/NEWS +++ b/NEWS @@ -87,6 +87,35 @@ New in spot 2.5.3.dev (not yet released) a "suspendable" automaton B. They are also optimized for the case that A is weak. + - When 'generic' acceptance is enabled, the translation routine will + split the input formula on Boolean operators into components that + are syntactically 'obligation', 'suspendable', or 'something + else'. Those will be translated separately and combined with + product()/product_susp(). This is inspired by the ways things are + done in ltl2dstar or delag, and can be disabled by passing option + -xltl-split=0, as in ltl2tgba -G -D -xltl-split=0. Here are the + sizes of deterministic automata produced with generic acceptance + using two versions of ltl2tgba and delag for reference. + + ltl2tgba -GD rabinizer 4 + 2.5 2.6 delag + ------------- ------------- + FGa0&GFb0 5 1 1 + (FGa1&GFb1)|FGa0|GFb0 8 1 1 + (FGa2&GFb2)|((FGa1|GFb1)&FGa0&GFb0) 497 1 1 + FGa0|GFb0 2 1 1 + (FGa1|GFb1)&FGa0&GFb0 16 1 1 + (FGa2|GFb2)&((FGa1&GFb1)|FGa0|GFb0) 29 1 1 + GFa1 <-> GFz 4 1 1 + (GFa1 & GFa2) <-> GFz 8 1 1 + (GFa1 & GFa2 & GFa3) <-> GFz 21 1 1 + GFa1 -> GFz 5 1 1 + (GFa1 & GFa2) -> GFz 12 1 1 + (GFa1 & GFa2 & GFa3) -> GFz 41 1 1 + FG(a|b)|FG(!a|Xb) 4 2 2 + FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21 5 4 + FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170 15 8 + - print_dot(), used to print automata in GraphViz's format, underwent several changes: @@ -219,6 +248,13 @@ New in spot 2.5.3.dev (not yet released) Make sure to quote %L to protect the potential commas: genltl --format='%F,"%L",%f' ... + - In Spot 2.5 and prior running "ltl2tgba --generic --det" on some + formula would attempt to translate it as deterministic TGBA or + determinize it into an automaton with parity acceptance. Version + 2.5 introduced --parity to force parity acceptance on the output. + This version finally gives --generic some more natural semantics: + any acceptance condition can be used. + New in spot 2.5.3 (2018-04-20) diff --git a/bin/spot-x.cc b/bin/spot-x.cc index b9d1a77b0..6d9a446dc 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -45,6 +45,9 @@ static const argp_option options[] = 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.") }, { 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/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index e3e3853aa..5b510864d 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -18,8 +18,8 @@ a quick summary: - =--ba= (or =-B=) outputs state-based Büchi automata - =--monitor= (or =-M=) outputs monitors - =--generic --deterministic= (or =-DG=) will do whatever it takes to - produce a deterministic automaton, and may output generalized Büchi, - or parity acceptance. + produce a deterministic automaton, and may use any acceptance + condition - =--parity --deterministic= (or =-DP=) will produce a deterministic automaton with parity acceptance. @@ -466,8 +466,7 @@ In particular, for properties more complex than obligations, it is possible that no deterministic TGBA exist, and even if it exists, =ltl2tgba= might not find it: so a non-deterministic automaton can be returned in this case. If you absolutely want a deterministic -automaton, [[#generic][read on about the =--generic= option below]]. - +automaton, see [[#generic][the =--generic= option]] or [[#parity][the =--parity= option]]. An example formula where the difference between =-D= and =--small= is flagrant is =Ga|Gb|Gc=: @@ -724,9 +723,15 @@ expectations. :END: The =--generic= (or =-G=) option allows =ltl2tgba= to use more - complex acceptance. Combined with =--deterministic= (or =-D=) this - allows the use of a determinization algorithm that produces - automata with parity acceptance. + complex acceptance conditions. This is done by splitting the LTL + formulas on Boolean connectives to recognize some subformulas that + are either to translate with different types of acceptance + conditions, and then combining everything back together. + + Combined with =--deterministic= (or =-D=) this allows the use of a + determinization algorithm that produces automata with parity + acceptance. This is only used for subformulas for which we do not + know a better way to get a deterministic automaton. For instance =FGa= is the typical formula for which not deterministic TGBA exists. @@ -743,7 +748,7 @@ ltl2tgba "FGa" -D -d #+RESULTS: [[file:ltl2tgba-fga.svg]] - But with =--generic=, =ltl2tgba= will output the following Rabin automaton: + But with =--generic=, =ltl2tgba= will output the following co-Büchi automaton: #+NAME: ltl2tgba-fga-D #+BEGIN_SRC sh :results verbatim :exports code @@ -757,9 +762,54 @@ ltl2tgba "FGa" -G -D -d #+RESULTS: [[file:ltl2tgba-fga-D.svg]] -Note that determinization algorithm implemented actually outputs -parity acceptance, but =Fin(0)&Inf(1)= can be interpreted either as -=Rabin 1= or =parity min odd 2=. + +If we translate =Fb|Gc= as a deterministic automaton with any +acceptance condition, we get a weak and deterministic Büchi automaton: + +#+NAME: ltl2tgba-fbgc-D +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba "Fb|Gc" -G -D -d +#+END_SRC + +#+BEGIN_SRC dot :file ltl2tgba-fbgc-D.svg :var txt=ltl2tgba-fbgc-D :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:ltl2tgba-fbgc-D.svg]] + + +Finally if we translate the conjunction of these two subformulas, a +product of these two automata will be made, producing: + +#+NAME: ltl2tgba-fbgcfga-D +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba "(Fb|Gc)&FGa" -G -D -d +#+END_SRC + +#+BEGIN_SRC dot :file ltl2tgba-fbgcfga-D.svg :var txt=ltl2tgba-fbgcfga-D :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:ltl2tgba-fbgcfga-D.svg]] + +Disabling the splitting of the original formula LTL formulas can be +done using option =-x ltl-split=0=. In that case the formula +=(Fb|Gc)&FGa= will be translated into a single TGBA, and because this +TGBA is non-deterministic, it will then be determinized into an +automaton with parity acceptance: + +#+NAME: ltl2tgba-fbgcfga-nosplit-D +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba "(Fb|Gc)&FGa" -G -D -xltl-split=0 -d +#+END_SRC +#+BEGIN_SRC dot :file ltl2tgba-fbgcfga-nosplit-D.svg :var txt=ltl2tgba-fbgcfga-nosplit-D :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:ltl2tgba-fbgcfga-nosplit-D.svg]] The [[./man/spot-x.7.html][=spot-x=]](7) man page lists a few =-x= options (=det-scc=, @@ -785,7 +835,7 @@ would be larger if SCC-based optimizations were disabled: #+NAME: ltl2tgba-det2 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba "F(a W FGb)" -x '!det-scc' -G -D -d +ltl2tgba "F(a W FGb)" -xdet-scc=0 -G -D -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-det2.svg :var txt=ltl2tgba-det2 :exports results @@ -795,11 +845,10 @@ ltl2tgba "F(a W FGb)" -x '!det-scc' -G -D -d #+RESULTS: [[file:ltl2tgba-det2.svg]] -While the =--generic= option currently only builds automata with -generalized-Büchi or parity acceptance, this is very likely to change -in the future. - * Deterministic automata with =--parity --deterministic= + :PROPERTIES: + :CUSTOM_ID: parity + :END: Using the =--parity= (or upper-case =-P=) option will force the acceptance condition to be of a parity type. This has to be diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index bd8277c7c..603d77051 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -26,6 +26,7 @@ #include #include #include +#include namespace spot { @@ -35,7 +36,9 @@ namespace spot comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0; relabel_bool_ = tls_impl_ = -1; gf_guarantee_ = level_ != Low; + ltl_split_ = true; + opt_ = opt; if (!opt) return; @@ -49,6 +52,7 @@ namespace spot } tls_impl_ = opt->get("tls-impl", -1); gf_guarantee_ = opt->get("gf-guarantee", gf_guarantee_); + ltl_split_ = opt->get("ltl-split", 1); } void translator::build_simplifier(const bdd_dict_ptr& dict) @@ -95,6 +99,8 @@ namespace spot throw std::runtime_error ("tls-impl should take a value between 0 and 3"); } + if (comp_susp_ > 0 || (ltl_split_ && type_ == Generic)) + options.favor_event_univ = true; simpl_owned_ = simpl_ = new tl_simplifier(options, dict); } @@ -160,37 +166,160 @@ namespace spot twa_graph_ptr aut; twa_graph_ptr aut2 = nullptr; - if (comp_susp_ > 0) - { - // FIXME: Handle unambiguous_ automata? - int skel_wdba = skel_wdba_; - if (skel_wdba < 0) - skel_wdba = (pref_ & postprocessor::Deterministic) ? 1 : 2; - aut = compsusp(r, simpl_->get_dict(), skel_wdba == 0, - skel_simul_ == 0, early_susp_ != 0, - comp_susp_ == 2, skel_wdba == 2, false); + if (ltl_split_ && type_ == Generic && !r.is_syntactic_obligation()) + { + formula r2 = r; + unsigned leading_x = 0; + while (r2.is(op::X)) + { + r2 = r2[0]; + ++leading_x; + } + // F(q|u|f) = q|F(u)|F(f) + // G(q&e&f) = q&G(e)&G(f) + bool want_u = r2.is({op::F, op::Or}); + if (want_u || r2.is({op::G, op::And})) + { + std::vector susp; + std::vector rest; + auto op1 = r2.kind(); + auto op2 = r2[0].kind(); + for (formula child: r2[0]) + { + bool u = child.is_universal(); + bool e = child.is_eventual(); + if (u && e) + susp.push_back(child); + else if ((want_u && u) || (!want_u && e)) + susp.push_back(formula::unop(op1, child)); + else + rest.push_back(child); + } + susp.push_back(formula::unop(op1, formula::multop(op2, rest))); + r2 = formula::multop(op2, susp); + } + if (r2.is_syntactic_obligation() || !r2.is(op::And, op::Or)) + goto nosplit; + + bool is_and = r2.is(op::And); + // Let's classify subformulas. + std::vector oblg; + std::vector susp; + std::vector rest; + for (formula child: r2) + { + if (child.is_syntactic_obligation()) + oblg.push_back(child); + else if (child.is_eventual() && child.is_universal()) + susp.push_back(child); + else + rest.push_back(child); + } + option_map om; + if (opt_) + om = *opt_; + om.set("ltl-split", 0); + translator translate_without_split(simpl_, &om); + translate_without_split.set_pref(pref_); + translate_without_split.set_level(level_); + translate_without_split.set_type(type_); + auto transrun = [&](formula f) + { + if (f == r2) + return translate_without_split.run(f); + else + return run(f); + }; + + aut = nullptr; + // All obligations can be converted into a minimal WDBA. + if (!oblg.empty()) + { + formula oblg_f = formula::multop(r2.kind(), oblg); + aut = transrun(oblg_f); + } + if (!rest.empty()) + { + formula rest_f = formula::multop(r2.kind(), rest); + 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); + } + if (!susp.empty()) + { + twa_graph_ptr susp_aut = nullptr; + // Each suspendable formula separately + for (formula f: susp) + { + twa_graph_ptr one = transrun(f); + if (!susp_aut) + susp_aut = one; + else if (is_and) + susp_aut = product(susp_aut, one); + else + susp_aut = product_or(susp_aut, one); + } + if (aut == nullptr) + aut = susp_aut; + else if (is_and) + aut = product_susp(aut, susp_aut); + else + aut = product_or_susp(aut, susp_aut); + } + if (leading_x > 0) + { + unsigned init = aut->get_init_state_number(); + do + { + unsigned tmp = aut->new_state(); + aut->new_edge(tmp, init, bddtrue); + init = tmp; + } + while (--leading_x); + aut->set_init_state(init); + } } else { - if (gf_guarantee_ && PREF_ != Any) + nosplit: + if (comp_susp_ > 0) { - bool det = unambiguous || (PREF_ == Deterministic); - bool sba = type_ == BA || (pref_ & SBAcc); - if ((type_ & (BA | Parity | Generic)) || type_ == TGBA) - aut2 = gf_guarantee_to_ba_maybe(r, simpl_->get_dict(), det, sba); - if (aut2 && (type_ & (BA | Parity)) && (pref_ & Deterministic)) - return finalize(aut2); - if (!aut2 && (type_ & (Generic | Parity | CoBuchi))) + // FIXME: Handle unambiguous_ automata? + int skel_wdba = skel_wdba_; + if (skel_wdba < 0) + skel_wdba = (pref_ & postprocessor::Deterministic) ? 1 : 2; + + aut = compsusp(r, simpl_->get_dict(), skel_wdba == 0, + skel_simul_ == 0, early_susp_ != 0, + comp_susp_ == 2, skel_wdba == 2, false); + } + else + { + if (gf_guarantee_ && PREF_ != Any) { - aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(), sba); - if (aut2 - && (type_ & (CoBuchi | Parity)) + bool det = unambiguous || (PREF_ == Deterministic); + bool sba = type_ == BA || (pref_ & SBAcc); + if ((type_ & (BA | Parity | Generic)) || type_ == TGBA) + aut2 = gf_guarantee_to_ba_maybe(r, simpl_->get_dict(), + det, sba); + if (aut2 && ((type_ == BA) || (type_ & Parity)) && (pref_ & Deterministic)) return finalize(aut2); + if (!aut2 && (type_ & (Generic | Parity | CoBuchi))) + { + aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(), sba); + if (aut2 + && (type_ & (CoBuchi | Parity)) + && (pref_ & Deterministic)) + return finalize(aut2); + } } } - bool exprop = unambiguous || level_ == postprocessor::High; aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop, true, false, false, nullptr, nullptr, diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh index 10eecf908..0f0ff18be 100644 --- a/spot/twaalgos/translate.hh +++ b/spot/twaalgos/translate.hh @@ -149,6 +149,8 @@ namespace spot int relabel_bool_; int tls_impl_; bool gf_guarantee_; + bool ltl_split_; + const option_map* opt_; }; /// @} diff --git a/tests/core/genltl.test b/tests/core/genltl.test index c38f86495..53c11e798 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -183,29 +183,29 @@ cat >exp< %T" \ "ltl2tgba -G -D %f > %T" \ "ltl2tgba -G -D %f | autfilt --gsa=unique-fin > %T" \ diff --git a/tests/python/_product_susp.ipynb b/tests/python/_product_susp.ipynb index baf49cda2..a8bd194d0 100644 --- a/tests/python/_product_susp.ipynb +++ b/tests/python/_product_susp.ipynb @@ -2216,84 +2216,62 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ") & Inf(\n", - "❶\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Inf(\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\n", + "⓿\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", "\n", - "0->2\n", - "\n", - "\n", - "a\n", + "0->1\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "❶\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a\n", - "❶\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -2368,111 +2346,110 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ") & (Inf(\n", - "❶\n", - ")&Inf(\n", - "❷\n", - "))\n", - "[Streett-like 3]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")&Inf(\n", + "❶\n", + ")\n", + "[gen. Büchi 2]\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", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "a\n", + "⓿\n", + "❶\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a\n", - "❷\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "❶\n", + "\n", + "\n", + "a\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a\n", + "❶\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a\n", - "❷\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!a\n", - "❷\n", - "\n", - "\n", + "\n", "\n", - "2->2\n", - "\n", - "\n", - "a\n", - "❶\n", + "2->3\n", + "\n", + "\n", + "a\n", + "❶\n", "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!a\n", - "❶\n", - "❷\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a\n", + "⓿\n", + "❶\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -2494,84 +2471,62 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ") & Inf(\n", - "❶\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Inf(\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\n", + "⓿\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", "\n", - "0->2\n", - "\n", - "\n", - "a\n", + "0->1\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "❶\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a\n", - "❶\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -2646,111 +2601,110 @@ "\n", "\n", - "\n", - "\n", - "\n", - "(Fin(\n", - "⓿\n", - ") & Inf(\n", - "❶\n", - ")) | Inf(\n", - "❷\n", - ")\n", - "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ") | Inf(\n", + "❶\n", + ")\n", + "[Fin-less 2]\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", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "a\n", + "⓿\n", + "❶\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a\n", - "❷\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "❶\n", + "\n", + "\n", + "a\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a\n", + "❶\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a\n", - "❷\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!a\n", - "❷\n", - "\n", - "\n", + "\n", "\n", - "2->2\n", - "\n", - "\n", - "a\n", - "❶\n", + "2->3\n", + "\n", + "\n", + "a\n", + "❶\n", "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!a\n", - "❶\n", - "❷\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a\n", + "⓿\n", + "❶\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -3140,7 +3094,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 7, "metadata": {}, "outputs": [ { @@ -3506,13 +3460,6 @@ "source": [ "test(spot.translate('(Ga | GF!a)'), spot.translate('false'))" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 4454142f0..c1f693507 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -240,7 +240,7 @@ "\n" ], "text/plain": [ - " *' at 0x7feca4075120> >" + " *' at 0x7f6a240ef0f0> >" ] }, "execution_count": 4, @@ -352,7 +352,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f528d0> >" + " *' at 0x7f6a1d7ce8a0> >" ] }, "execution_count": 5, @@ -462,7 +462,7 @@ "\n" ], "text/plain": [ - " *' at 0x7feca4075120> >" + " *' at 0x7f6a240ef0f0> >" ] }, "execution_count": 6, @@ -695,7 +695,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f528a0> >" + " *' at 0x7f6a1d7ce8d0> >" ] }, "execution_count": 8, @@ -892,7 +892,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f528a0> >" + " *' at 0x7f6a1d7ce8d0> >" ] }, "execution_count": 11, @@ -977,7 +977,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f52a50> >" + " *' at 0x7f6a1d7ce060> >" ] }, "metadata": {}, @@ -1032,7 +1032,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f529f0> >" + " *' at 0x7f6a240e6f60> >" ] }, "metadata": {}, @@ -1126,7 +1126,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f52ab0> >" + " *' at 0x7f6a1d7ce9f0> >" ] }, "execution_count": 13, @@ -1257,7 +1257,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f52ab0> >" + " *' at 0x7f6a1d7ce9f0> >" ] }, "metadata": {}, @@ -1322,7 +1322,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f52a50> >" + " *' at 0x7f6a1d7ce060> >" ] }, "metadata": {}, @@ -1377,7 +1377,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f529f0> >" + " *' at 0x7f6a240e6f60> >" ] }, "metadata": {}, @@ -1609,7 +1609,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f52b40> >" + " *' at 0x7f6a1d7bdae0> >" ] }, "metadata": {}, @@ -1694,7 +1694,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f52c00> >" + " *' at 0x7f6a1d7bd4b0> >" ] }, "metadata": {}, @@ -1791,7 +1791,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f52b10> >" + " *' at 0x7f6a1d7ceb40> >" ] }, "metadata": {}, @@ -1959,7 +1959,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f52d80> >" + " *' at 0x7f6a1d7ced50> >" ] }, "execution_count": 18, @@ -2127,7 +2127,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f52d80> >" + " *' at 0x7f6a1d7ced50> >" ] }, "execution_count": 19, @@ -2290,7 +2290,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fec96f52d80> >" + " *' at 0x7f6a1d7ced50> >" ] }, "metadata": {}, @@ -2509,233 +2509,295 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ") & Inf(\n", - "❶\n", - ")\n", - "[Rabin 1]\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", - "\n", + "\n", "\n", "\n", "cluster_4\n", - "\n", + "\n", + "\n", + "\n", + "cluster_5\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", + "\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", + "\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", + "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "\n", + "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", - "\n", - "\n", - "6\n", - "\n", - "6\n", - "\n", - "\n", - "\n", - "4->6\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "7\n", - "\n", - "7\n", - "\n", - "\n", - "\n", - "4->7\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "6->4\n", - "\n", - "\n", - "!b\n", - "❶\n", - "\n", - "\n", - "\n", - "6->6\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", - "\n", - "6->7\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "7->4\n", - "\n", - "\n", - "b\n", - "❶\n", - "\n", - "\n", - "\n", - "7->6\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", - "7->7\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", "\n", - "1->4\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!a & b & !c\n", + "0->4\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", - "\n", + "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", - "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "!a & b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "⓿\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a | !b\n", + "\n", + "\n", "\n", - "2->5\n", - "\n", - "\n", - "!a & b & c\n", + "2->2\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "!b & !c\n", + "⓿\n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "!b & c\n", + "⓿\n", + "\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + "b & !c\n", + "⓿\n", + "\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "b & c\n", + "⓿\n", + "\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "3->7\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!a & b & c\n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "5->7\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "\n", + "\n", "5->4\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a & b & !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", - "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "❶\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "!a & b & c\n", + "⓿\n", "\n", "\n", "" @@ -2754,6 +2816,13 @@ "spot.highlight_languages(aut)\n", "aut.show('.bas')" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": {