diff --git a/NEWS b/NEWS index 74e1765b7..a07046a3e 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,13 @@ New in spot 2.5.1.dev (not yet released) Library: + - Option "a" of print_dot(), for printing the acceptance condition, + is now enabled by default. Option "A", introduced in Spot 2.4, + can be used to hide the acceptance condition in case you do not + want it. This change of course affects the --dot option of all + the command-line tools, as well as the various way to display + automata using the Python bindings. + - cleanup_parity() and cleanup_parity_here() are smarter and now remove from the acceptance condition the parity colors that are not used in the automaton. diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 4cc2b771a..b6b90008e 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -92,7 +92,7 @@ static const argp_option options[] = OPTION_ARG_OPTIONAL, "GraphViz's format. Add letters for " "(1) force numbered states, " - "(a) show acceptance condition, " + "(a) show acceptance condition (default), " "(A) hide acceptance condition, " "(b) acceptance sets as bullets, " "(B) bullets except for Büchi/co-Büchi automata, " diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index c8d19233e..cbf1ab75f 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -49,7 +49,7 @@ autfilt example.hoa --dot #+END_SRC #+BEGIN_SRC sh :results verbatim :exports results -SPOT_DOTEXTRA= autfilt example.hoa --dot= +SPOT_DOTEXTRA= autfilt example.hoa --dot #+END_SRC #+RESULTS: @@ -469,13 +469,12 @@ State: 2 EOF #+END_SRC -(Note: the '=.=' argument passed to =--dot= below hides default -options discussed [[file:oaut.org::#default-dot][on another page]], while the '=a=' causes the -acceptance condition to be displayed.) +(Note: that the =--dot= option used below uses some default options +discussed [[file:oaut.org::#default-dot][on another page]].) #+NAME: autfilt-ex1 #+BEGIN_SRC sh :results verbatim :exports code -autfilt aut-ex1.hoa --dot=.a +autfilt aut-ex1.hoa --dot #+END_SRC #+RESULTS: autfilt-ex1 @@ -516,7 +515,7 @@ Using =-S= will "push" the acceptance membership of the transitions to the state #+NAME: autfilt-ex2 #+BEGIN_SRC sh :results verbatim :exports code -autfilt -S aut-ex1.hoa --dot=.a +autfilt -S aut-ex1.hoa --dot= #+END_SRC #+RESULTS: autfilt-ex2 @@ -578,7 +577,7 @@ Using =--cnf-acceptance= simply rewrites the acceptance condition in Conjunctive #+NAME: autfilt-ex3 #+BEGIN_SRC sh :results verbatim :exports code -autfilt --cnf-acceptance aut-ex1.hoa --dot=.a +autfilt --cnf-acceptance aut-ex1.hoa --dot #+END_SRC #+RESULTS: autfilt-ex3 @@ -622,7 +621,7 @@ altered copies of strongly-connected components. #+NAME: autfilt-ex4 #+BEGIN_SRC sh :results verbatim :exports code -autfilt --remove-fin aut-ex1.hoa --dot=.a +autfilt --remove-fin aut-ex1.hoa --dot #+END_SRC #+RESULTS: autfilt-ex4 @@ -668,7 +667,7 @@ reflect the fact that these sets can never be visited. #+NAME: autfilt-ex5 #+BEGIN_SRC sh :results verbatim :exports code -autfilt --mask-acc=1,2 aut-ex1.hoa --dot=.a +autfilt --mask-acc=1,2 aut-ex1.hoa --dot #+END_SRC #+RESULTS: autfilt-ex5 @@ -715,7 +714,7 @@ Here are the results of these three options on our example: #+NAME: autfilt-ex6a #+BEGIN_SRC sh :results verbatim :exports code -autfilt --remove-ap=a aut-ex1.hoa --dot=.a +autfilt --remove-ap=a aut-ex1.hoa --dot #+END_SRC #+RESULTS: autfilt-ex6a @@ -754,7 +753,7 @@ $txt #+NAME: autfilt-ex6b #+BEGIN_SRC sh :results verbatim :exports code -autfilt --remove-ap=a=0 aut-ex1.hoa --dot=.a +autfilt --remove-ap=a=0 aut-ex1.hoa --dot #+END_SRC #+RESULTS: autfilt-ex6b @@ -787,7 +786,7 @@ $txt #+NAME: autfilt-ex6c #+BEGIN_SRC sh :results verbatim :exports code -autfilt --remove-ap=a=1 aut-ex1.hoa --dot=.a +autfilt --remove-ap=a=1 aut-ex1.hoa --dot #+END_SRC #+RESULTS: autfilt-ex6c diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 1e54d72ea..1a8a6709b 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -222,7 +222,7 @@ State: 0 0 0 1 1 State: 1 1 0 0 0 --END-- EOF -autfilt --merge concept-te.hoa -d +autfilt --merge concept-te.hoa -d.A #+END_SRC #+BEGIN_SRC dot :file concept-te1.svg :var txt=te1 :exports results $txt @@ -244,7 +244,7 @@ following transition structure: #+NAME: te2 #+BEGIN_SRC sh :results verbatim :exports none -autfilt concept-te.hoa -d +autfilt concept-te.hoa -d.A #+END_SRC #+BEGIN_SRC dot :file concept-te2.svg :var txt=te2 :exports results $txt @@ -545,7 +545,7 @@ by Spot: #+NAME: twa-example1 #+BEGIN_SRC sh :results verbatim :exports none -ltlfilt -l -f 'GFa | FGb' | ltl2dstar --output-format=hoa - - | autfilt --merge -d.a +ltlfilt -l -f 'GFa | FGb' | ltl2dstar --output-format=hoa - - | autfilt --merge -d #+END_SRC #+BEGIN_SRC dot :file concept-twa1.svg :var txt=twa-example1 :exports results $txt @@ -822,7 +822,7 @@ Acc-Sig: +0 +1 #+NAME: dstar-example1 #+BEGIN_SRC sh :results verbatim :exports none -echo '| F G p0 G F p1' | ltl2dstar --output-format=native - - | autfilt -d.a +echo '| F G p0 G F p1' | ltl2dstar --output-format=native - - | autfilt -d #+END_SRC #+BEGIN_SRC dot :file concept-dstar.svg :var txt=dstar-example1 :exports results $txt @@ -881,7 +881,7 @@ State: 3 {1 3} #+NAME: hoa1 #+BEGIN_SRC sh :results verbatim :exports none -ltldo ltl2dstar -f 'FGp0 | GFp1' -d.a +ltldo ltl2dstar -f 'FGp0 | GFp1' -d #+END_SRC #+BEGIN_SRC dot :file concept-hoa.svg :var txt=hoa1 :exports results $txt diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index 3ea005063..91b79eb40 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -83,7 +83,7 @@ Acc-Sig: Let's display this automaton with =autfilt=: #+NAME: fagfb #+BEGIN_SRC sh :results verbatim :exports code -autfilt fagfb --dot=.a +autfilt fagfb --dot #+END_SRC #+RESULTS: fagfb @@ -121,11 +121,6 @@ $txt #+RESULTS: [[file:fagfb.svg]] -We used =--dot=a= to display Spot's representation of the acceptance -condition (which uses the same convention as in the [[file:hoa.org][HOA format]]). The -extra dot is because we use some [[file:oaut.org][environment variables]] to produce a -more colorful output by default in these pages. - =dstar2tgba= can now be used to convert this DRA into a TGBA, a BA, or a Monitor, using the same options as [[file:ltl2tgba.org][=ltl2tgba=]]. @@ -204,45 +199,9 @@ Here is the translation of =GFa | GFb= to a 4-state Streett automaton: #+NAME: gfafgb #+BEGIN_SRC sh :results verbatim :exports code ltlfilt -f 'GFa & GFb' -l | ltl2dstar --automata=streett --ltl2nba=spin:ltl2tgba@-Ds - gfagfb -autfilt --dot=.a gfagfb +autfilt --dot gfagfb #+END_SRC -#+RESULTS: gfafgb -#+begin_example -digraph G { - rankdir=LR - label=<(Fin(⓿) | Inf(❶)) & (Fin(❷) | Inf(❸))> - labelloc="t" - node [shape="circle"] - fontname="Lato" - node [fontname="Lato"] - edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] - I [label="", style=invis, width=0] - I -> 0 - 0 [label=<0
❶❸>] - 0 -> 0 [label=] - 0 -> 1 [label=] - 0 -> 2 [label=] - 0 -> 3 [label=] - 1 [label=<1
⓿❸>] - 1 -> 0 [label=] - 1 -> 1 [label=] - 1 -> 2 [label=] - 1 -> 3 [label=] - 2 [label=<2
❶❷>] - 2 -> 0 [label=] - 2 -> 1 [label=] - 2 -> 2 [label=] - 2 -> 3 [label=] - 3 [label=<3
⓿❷>] - 3 -> 0 [label=] - 3 -> 1 [label=] - 3 -> 2 [label=] - 3 -> 3 [label=] -} -#+end_example - #+BEGIN_SRC dot :file gfafgb.svg :var txt=gfafgb :exports results $txt #+END_SRC diff --git a/doc/org/hierarchy.org b/doc/org/hierarchy.org index b92b00921..929f1b665 100644 --- a/doc/org/hierarchy.org +++ b/doc/org/hierarchy.org @@ -362,7 +362,7 @@ for the obligation property =a <-> GXa=: #+NAME: hier-oblig-3 #+BEGIN_SRC sh :results verbatim :exports code -ltldo 'ltl2dstar --automata=streett' -f 'a <-> GXa' -d.a +ltldo 'ltl2dstar --automata=streett' -f 'a <-> GXa' -d #+END_SRC #+BEGIN_SRC dot :file hier-oblig-3.svg :var txt=hier-oblig-3 :exports results $txt @@ -602,7 +602,7 @@ a /recurrence/ property), is to chain a few algorithms implemented in Spot: #+NAME: hier-recurrence-4 #+BEGIN_SRC sh :results verbatim :exports code - ltl2tgba -G -D 'G(Gb | Fa)' -d.a + ltl2tgba -G -D 'G(Gb | Fa)' -d #+END_SRC #+BEGIN_SRC dot :file hier-recurrence-4.svg :var txt=hier-recurrence-4 :exports results $txt @@ -618,7 +618,7 @@ a /recurrence/ property), is to chain a few algorithms implemented in Spot: #+NAME: hier-recurrence-5 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -G -D 'G(Gb | Fa)' | - autfilt --generalized-rabin -d.a + autfilt --generalized-rabin -d #+END_SRC #+BEGIN_SRC dot :file hier-recurrence-5.svg :var txt=hier-recurrence-5 :exports results $txt @@ -637,7 +637,7 @@ a /recurrence/ property), is to chain a few algorithms implemented in Spot: #+NAME: hier-recurrence-6 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -G -D 'G(Gb | Fa)' | - autfilt -S --generalized-rabin -d.a + autfilt -S --generalized-rabin -d #+END_SRC #+BEGIN_SRC dot :file hier-recurrence-6.svg :var txt=hier-recurrence-6 :exports results @@ -661,7 +661,7 @@ a /recurrence/ property), is to chain a few algorithms implemented in Spot: #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -G -D 'G(Gb | Fa)' | autfilt -S --generalized-rabin | - autfilt -B -D -d.a + autfilt -B -D -d #+END_SRC #+BEGIN_SRC dot :file hier-recurrence-7.svg :var txt=hier-recurrence-7 :exports results @@ -680,7 +680,7 @@ helps producing a smaller automaton. Here is what we get without it: #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -G -D 'G(Gb | Fa)' | autfilt --generalized-rabin | - autfilt -B -D -d.a + autfilt -B -D -d #+END_SRC #+BEGIN_SRC dot :file hier-recurrence-8.svg :var txt=hier-recurrence-8 :exports results @@ -701,7 +701,7 @@ persistence formula is =FGa=, and using =-D= on this is hopeless. #+NAME: hier-persistence-1 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -D FGa -d.a +ltl2tgba -D FGa -d #+END_SRC #+BEGIN_SRC dot :file hier-persistence-1.svg :var txt=hier-persistence-1 :exports results $txt @@ -721,7 +721,7 @@ complementation ourselves: #+BEGIN_SRC sh :results verbatim :exports code ltlfilt --negate -f FGa | ltl2tgba -D | - autfilt --complement -d.a + autfilt --complement -d #+END_SRC #+BEGIN_SRC dot :file hier-persistence-2.svg :var txt=hier-persistence-2 :exports results $txt @@ -780,7 +780,7 @@ generalized Büchi automaton: #+BEGIN_SRC sh :results verbatim :exports code ltlfilt --negate -f 'F(G!a | G(b U a))' | ltl2tgba -D | - autfilt --highlight-nondet=5 -d.a + autfilt --highlight-nondet=5 -d #+END_SRC #+BEGIN_SRC dot :file hier-persistence-4.svg :var txt=hier-persistence-4 :exports results $txt @@ -798,7 +798,7 @@ deterministic Büchi: ltlfilt --negate -f 'F(G!a | G(b U a))' | ltl2tgba -G -D | autfilt --generalized-rabin | - autfilt --tgba -D -d.a + autfilt --tgba -D -d #+END_SRC #+BEGIN_SRC dot :file hier-persistence-5.svg :var txt=hier-persistence-5 :exports results $txt @@ -816,8 +816,9 @@ ltlfilt --negate -f 'F(G!a | G(b U a))' | ltl2tgba -G -D | autfilt --generalized-rabin | autfilt --tgba -D | - autfilt --complement -d.ab + autfilt --complement -d #+END_SRC + #+BEGIN_SRC dot :file hier-persistence-6.svg :var txt=hier-persistence-6 :exports results $txt #+END_SRC diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 97acad8c3..e3e3853aa 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -147,7 +147,7 @@ $txt #+RESULTS: [[file:dotex2.svg]] -The above TGBA has two acceptance sets: ⓿ and ❶. The position of +The above TGBA has two acceptance sets: ⓿ and ❶. The definition of these acceptance sets ensures that atomic propositions =a= and =b= must be true infinitely often. @@ -733,7 +733,7 @@ expectations. #+NAME: ltl2tgba-fga #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba "FGa" -D -d.a +ltl2tgba "FGa" -D -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-fga.svg :var txt=ltl2tgba-fga :exports results @@ -747,7 +747,7 @@ ltl2tgba "FGa" -D -d.a #+NAME: ltl2tgba-fga-D #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba "FGa" -G -D -d.a +ltl2tgba "FGa" -G -D -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-fga-D.svg :var txt=ltl2tgba-fga-D :exports results @@ -771,7 +771,7 @@ For instance the following deterministic automaton #+NAME: ltl2tgba-det1 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba "F(a W FGb)" -G -D -d.a +ltl2tgba "F(a W FGb)" -G -D -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-det1.svg :var txt=ltl2tgba-det1 :exports results @@ -785,7 +785,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.a +ltl2tgba "F(a W FGb)" -x '!det-scc' -G -D -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-det2.svg :var txt=ltl2tgba-det2 :exports results @@ -831,7 +831,7 @@ acceptance (another name for =parity min odd 2=): #+NAME: ltl2tgba-dp1 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba "FGa" -D -P -d.a +ltl2tgba "FGa" -D -P -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-dp1.svg :var txt=ltl2tgba-dp1 :exports results @@ -846,7 +846,7 @@ for =parity min even 1=): #+NAME: ltl2tgba-dp2 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba "GFa & GFb" -D -P -d.a +ltl2tgba "GFa & GFb" -D -P -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-dp2.svg :var txt=ltl2tgba-dp2 :exports results @@ -861,7 +861,7 @@ we can specify it as an argument to the =--parity= option. For instance #+NAME: ltl2tgba-dp3 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba "GFa & GFb" -D -P'min odd' -d.a +ltl2tgba "GFa & GFb" -D -P'min odd' -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-dp3.svg :var txt=ltl2tgba-dp3 :exports results @@ -879,7 +879,7 @@ requested) should belong to exactly one acceptance set. #+NAME: ltl2tgba-dp4 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba "GFa & GFb" -D -p -d.a +ltl2tgba "GFa & GFb" -D -p -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-dp4.svg :var txt=ltl2tgba-dp4 :exports results @@ -891,7 +891,7 @@ ltl2tgba "GFa & GFb" -D -p -d.a #+NAME: ltl2tgba-dp5 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba "GFa & GFb" -D -p'min odd' -d.a +ltl2tgba "GFa & GFb" -D -p'min odd' -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-dp5.svg :var txt=ltl2tgba-dp5 :exports results @@ -906,7 +906,7 @@ acceptance if needed: #+NAME: ltl2tgba-dp6 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba "GFa & GFb" -D -S -p'max even' -d.a +ltl2tgba "GFa & GFb" -D -S -p'max even' -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-dp6.svg :var txt=ltl2tgba-dp6 :exports results diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 99c2636c6..4452bf75e 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -856,7 +856,7 @@ The dot output can also be customized via two environment variables: (for any value of =xyz=, even empty) will ignore the =SPOT_DOTDEFAULT= variable. If the argument of =--dot= contains a dot character, then this dot is replaced by the contents of - =SPOT_DOTDEFAULT=. So ~--dot=.a~ would be equivalent to =--dot=vcsna= + =SPOT_DOTDEFAULT=. So ~--dot=.A~ would be equivalent to =--dot=vcsnA= with our example definition of =SPOT_DOTDEFAULT=. - =SPOT_DOTEXTRA= may contains an arbitrary string that will be emitted in the dot output before the first state. This can be used to modify diff --git a/doc/org/randaut.org b/doc/org/randaut.org index 23d31d588..324614948 100644 --- a/doc/org/randaut.org +++ b/doc/org/randaut.org @@ -293,7 +293,7 @@ $txt #+NAME: randaut5b #+BEGIN_SRC sh :results verbatim :exports code -randaut -Q6 -e0.4 -S -a.2 -A 'Streett 1..3' 2 --dot=.a +randaut -Q6 -e0.4 -S -a.2 -A 'Streett 1..3' 2 --dot #+END_SRC #+RESULTS: randaut5b @@ -346,7 +346,7 @@ give =randaut= some freedom, as in this example. #+NAME: randaut5c #+BEGIN_SRC sh :results verbatim :exports code -randaut -Q10 -S --colored -A 'parity rand rand 3..4' 2 --dot=.a +randaut -Q10 -S --colored -A 'parity rand rand 3..4' 2 --dot #+END_SRC #+RESULTS: randaut5c @@ -511,14 +511,14 @@ to the same sets). This leaves us with one extra SCC that should necessarily mix accepting and rejecting cycles. (Note: the '=.=' argument passed to =--dot= below hides default -options discussed [[file:oaut.org::#default-dot][on another page]], while '=a=' causes the acceptance -condition to be displayed and'=s=' shows SCCs.) +options discussed [[file:oaut.org::#default-dot][on another page]], while '=s=' causes SCCs to be +displayed.) #+NAME: randaut7 #+BEGIN_SRC sh :results verbatim :exports code randaut -n -1 --colored -A'parity min odd 4' a b | autfilt --sccs=5 --trivial-sccs=1 --rejecting-sccs=1 \ - --inherently-weak-sccs=2 --weak-sccs=1 -n 1 --dot=.as + --inherently-weak-sccs=2 --weak-sccs=1 -n 1 --dot=.s #+END_SRC #+BEGIN_SRC dot :file randaut7.svg :var txt=randaut7 :exports results diff --git a/doc/org/satmin.org b/doc/org/satmin.org index ef7719ae8..a91207488 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -416,7 +416,7 @@ ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa - - > output.hoa Let's draw it: #+NAME: autfiltsm1 #+BEGIN_SRC sh :results verbatim :exports code -autfilt output.hoa --dot=.a +autfilt output.hoa --dot #+END_SRC #+RESULTS: autfiltsm1 #+begin_example @@ -467,28 +467,8 @@ solver used): #+NAME: autfiltsm2 #+BEGIN_SRC sh :results verbatim :exports code -autfilt --sat-minimize output.hoa --dot=.a +autfilt --sat-minimize output.hoa --dot #+END_SRC -#+RESULTS: autfiltsm2 -#+begin_example -digraph G { - rankdir=LR - label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸))> - labelloc="t" - node [shape="circle"] - fontname="Lato" - node [fontname="Lato"] - edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0"] - 0 -> 0 [label=❶>] - 0 -> 0 [label=⓿❷>] - 0 -> 0 [label=❶❷>] - 0 -> 0 [label=⓿❸>] -} -#+end_example #+BEGIN_SRC dot :file autfiltsm2.svg :var txt=autfiltsm2 :exports results $txt @@ -500,31 +480,9 @@ We can also attempt to build a state-based version with #+NAME: autfiltsm3 #+BEGIN_SRC sh :results verbatim :exports code -autfilt -S --sat-minimize output.hoa --dot=.a +autfilt -S --sat-minimize output.hoa --dot #+END_SRC -#+RESULTS: autfiltsm3 -#+begin_example -digraph G { - rankdir=LR - label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸))> - labelloc="t" - node [shape="circle"] - fontname="Lato" - node [fontname="Lato"] - edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] - I [label="", style=invis, width=0] - I -> 0 - 0 [label=<0
❶❷>] - 0 -> 0 [label=] - 0 -> 1 [label=] - 1 [label=<1
⓿❸>] - 1 -> 0 [label=] - 1 -> 1 [label=] -} -#+end_example - #+BEGIN_SRC dot :file autfiltsm3.svg :var txt=autfiltsm3 :exports results $txt #+END_SRC @@ -543,7 +501,7 @@ Let's try with generalized co-Büchi for instance: #+NAME: autfiltsm4 #+BEGIN_SRC sh :results verbatim :exports code -autfilt -S --sat-minimize='acc="generalized-co-Buchi 2"' output.hoa --dot=.a +autfilt -S --sat-minimize='acc="generalized-co-Buchi 2"' output.hoa --dot #+END_SRC #+RESULTS: autfiltsm4 @@ -582,7 +540,7 @@ attempt to create a co-Büchi automaton with #+NAME: autfiltsm5 #+BEGIN_SRC sh :results verbatim :exports code -autfilt -S --sat-minimize='acc="Fin(0)"' output.hoa --dot=.a +autfilt -S --sat-minimize='acc="Fin(0)"' output.hoa --dot #+END_SRC #+RESULTS: autfiltsm5 @@ -615,7 +573,7 @@ smaller than the output. Let's take this small TGBA as input: #+NAME: autfiltsm6 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba 'GFa & GFb' >output2.hoa -autfilt output2.hoa --dot=.a +autfilt output2.hoa --dot #+END_SRC #+RESULTS: autfiltsm6 @@ -663,32 +621,9 @@ However if we allow more states, it will work: #+NAME: autfiltsm8 #+BEGIN_SRC sh :results verbatim :exports code -autfilt --sat-minimize='acc="Buchi",max-states=3' output2.hoa --dot=.a +autfilt --sat-minimize='acc="Buchi",max-states=3' output2.hoa --dot #+END_SRC -#+RESULTS: autfiltsm8 -#+begin_example -digraph G { - rankdir=LR - label=⓿)> - labelloc="t" - node [shape="circle"] - fontname="Lato" - node [fontname="Lato"] - edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0"] - 0 -> 0 [label=] - 0 -> 0 [label=⓿>] - 0 -> 1 [label=⓿>] - 1 [label="1"] - 1 -> 0 [label=] - 1 -> 1 [label=] -} -#+end_example - #+BEGIN_SRC dot :file autfiltsm8.svg :var txt=autfiltsm8 :exports results $txt #+END_SRC @@ -758,32 +693,8 @@ automaton is not colored: #+NAME: autfiltsm9 #+BEGIN_SRC sh :results verbatim :exports code -autfilt -S --sat-minimize='acc="parity max even 3"' output2.hoa --dot=.a +autfilt -S --sat-minimize='acc="parity max even 3"' output2.hoa --dot #+END_SRC -#+RESULTS: autfiltsm9 -#+begin_example -digraph G { - rankdir=LR - label=❷) | (Fin(❶) & Inf(⓿))> - labelloc="t" - node [shape="circle"] - fontname="Lato" - node [fontname="Lato"] - edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] - I [label="", style=invis, width=0] - I -> 0 - 0 [label=<0>] - 0 -> 0 [label=] - 0 -> 1 [label=] - 0 -> 2 [label=] - 1 [label=<1>] - 1 -> 1 [label=] - 1 -> 2 [label=] - 2 [label=<2
⓿>] - 2 -> 0 [label=<1>] -} -#+end_example #+BEGIN_SRC dot :file autfiltsm9.svg :var txt=autfiltsm9 :exports results $txt @@ -797,31 +708,8 @@ belong to exactly one acceptance set: #+NAME: autfiltsm10 #+BEGIN_SRC sh :results verbatim :exports code -autfilt -S --sat-minimize='acc="parity max even 3",colored' output2.hoa --dot=.a +autfilt -S --sat-minimize='acc="parity max even 3",colored' output2.hoa --dot #+END_SRC -#+RESULTS: autfiltsm10 -#+begin_example -digraph G { - rankdir=LR - label=❷) | (Fin(❶) & Inf(⓿))> - labelloc="t" - node [shape="circle"] - fontname="Lato" - node [fontname="Lato"] - edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] - I [label="", style=invis, width=0] - I -> 0 - 0 [label=<0
❶>] - 0 -> 0 [label=] - 0 -> 1 [label=] - 1 [label=<1
❶>] - 1 -> 1 [label=] - 1 -> 2 [label=] - 2 [label=<2
❷>] - 2 -> 0 [label=<1>] -} -#+end_example #+BEGIN_SRC dot :file autfiltsm10.svg :var txt=autfiltsm10 :exports results $txt diff --git a/doc/org/tut23.org b/doc/org/tut23.org index ad258ddd3..78c019fd3 100644 --- a/doc/org/tut23.org +++ b/doc/org/tut23.org @@ -9,7 +9,7 @@ co-Büchi automaton (recognizing =GFa=) and then print it. #+NAME: tut23-dot #+BEGIN_SRC sh :results verbatim :exports none :var txt=tut23-cpp -autfilt --dot=.a <tut24.hoa <> EOF -autfilt --dot=.a tut24.hoa +autfilt --dot tut24.hoa #+END_SRC #+BEGIN_SRC dot :file tut24in.svg :var txt=tut24dot :exports results diff --git a/doc/org/tut30.org b/doc/org/tut30.org index 982a3fb09..04ae60efe 100644 --- a/doc/org/tut30.org +++ b/doc/org/tut30.org @@ -14,46 +14,9 @@ ltldo ltl2dstar -f 'F(Xp1 xor XXp1)' > tut30.hoa #+NAME: tut30in #+BEGIN_SRC sh :results verbatim :exports none -autfilt tut30.hoa --dot=.a +autfilt tut30.hoa --dot #+END_SRC -#+RESULTS: tut30in -#+begin_example -digraph G { - rankdir=LR - label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸)) | (Fin(❹) & Inf(❺))> - labelloc="t" - node [shape="circle"] - fontname="Lato" - node [fontname="Lato"] - edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] - I [label="", style=invis, width=0] - I -> 6 - 0 [label=<0
❷❺>] - 0 -> 2 [label=] - 0 -> 4 [label=] - 1 [label=<1
❷❺>] - 1 -> 4 [label=] - 1 -> 3 [label=] - 2 [label=<2
❸❹>] - 2 -> 0 [label=] - 2 -> 4 [label=] - 3 [label=<3
❸❹>] - 3 -> 4 [label=] - 3 -> 1 [label=] - 4 [label=<4
❶❷❹>] - 4 -> 4 [label=] - 4 -> 4 [label=] - 5 [label=<5
❷❹>] - 5 -> 2 [label=] - 5 -> 3 [label=] - 6 [label=<6
❷❹>] - 6 -> 5 [label=] - 6 -> 5 [label=] -} -#+end_example - #+BEGIN_SRC dot :file tut30in.svg :var txt=tut30in :exports results $txt #+END_SRC diff --git a/doc/org/tut31.org b/doc/org/tut31.org index 4dc00e8a1..ad9603fec 100644 --- a/doc/org/tut31.org +++ b/doc/org/tut31.org @@ -34,7 +34,7 @@ State: 2 cat >tut31.hoa <> EOF -autfilt --dot=.a tut31.hoa +autfilt --dot tut31.hoa #+END_SRC #+BEGIN_SRC dot :file tut31in.svg :var txt=tut31dot :exports results diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 39fbc87d5..f3826025f 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -88,7 +88,7 @@ namespace spot bool opt_force_acc_trans_ = false; bool opt_vertical_ = false; bool opt_name_ = false; - bool opt_show_acc_ = false; + bool opt_show_acc_ = true; bool mark_states_ = false; bool dcircles_ = false; bool opt_scc_ = false; diff --git a/tests/core/det.test b/tests/core/det.test index 7b259e67d..8248860e6 100755 --- a/tests/core/det.test +++ b/tests/core/det.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013-2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2013-2018 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -116,6 +116,8 @@ run 0 ../ikwiad -x -DC 'GFa & XGFb' > out.tgba cat >ex.tgba < 0 diff --git a/tests/core/dstar.test b/tests/core/dstar.test index 585c70374..bfa5c35da 100755 --- a/tests/core/dstar.test +++ b/tests/core/dstar.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et +# Copyright (C) 2013-2016, 2018 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -61,6 +61,8 @@ run 0 ../ikwiad -d -XD dra.dstar | tee stdout cat >expected < 0 @@ -83,6 +85,8 @@ run 0 ../ikwiad -d -XDB -R3 dra.dstar | tee stdout cat >expected < 0 @@ -128,6 +132,8 @@ run 0 ../ikwiad -d -XDB dsa.dstar | tee stdout cat >expected < 1 @@ -212,7 +218,7 @@ State: 3 "str\n\"ing" Acc-Sig: -0 +1 3 3 3 3 State: 4 "more\"string\"" Acc-Sig: +0 +1 3 4 3 4 EOF -run 0 autfilt -d -B dra.dstar | tee stdout +run 0 autfilt -dA -B dra.dstar | tee stdout cat >expected <expected< stdout cat >expected < 0 @@ -327,7 +329,7 @@ autfilt --name=%F --dot=nsc stdout 2>stderr && exit 1 cat >expected <output +SPOT_DOTDEFAULT=bra ltl2tgba --dot='Ae.f(Lato)' 'GFa & GFb' >output cat output zero='⓿' @@ -562,7 +562,7 @@ EOF # States should be circled even if <5 causes all states to be named, # because the names are smaller then 2 characters anyway. -ltl2tgba --det 'Ga | Gb | Gc' -d'<5' | grep -v '>' >out +ltl2tgba --det 'Ga | Gb | Gc' -d'A<5' | grep -v '>' >out diff out expected3 # Let's pretend that this is some used supplied input, as discussed in @@ -867,7 +867,7 @@ EOF diff output6 expect6 -run 0 autfilt -dk input6 >output6d +run 0 autfilt -dAk input6 >output6d cat >expect6d < output9 +autfilt -dA input9 > output9 cat >expected9 < output9b +autfilt -H1.1 input9 | autfilt -dA > output9b diff output9 output9b test 2 = `ltl2tgba 'GFa' 'a U b' 'a U b U c'| autfilt --ap=2..3 --count` @@ -1042,7 +1042,7 @@ test 2 = `genltl --dac=1..3 | ltl2tgba --stats='%e,"%h",%s' | autfilt --states=2..3 -F-/3 --stats='%<,"%h"' | wc -l` # --dot=d -ltl2tgba 'GF(a <-> Fb)' | autfilt -B --dot=d | grep ' (' >out +ltl2tgba 'GF(a <-> Fb)' | autfilt -B --dot=dA | grep ' (' >out cat >expected <expected <out +ltl2tgba 'a U b' | autfilt --remove-ap=b=0 --dot=dA >out cat >expected < 0 @@ -53,6 +55,8 @@ digraph G { } digraph G { rankdir=LR + label="t\n[Fin-less 2]" + labelloc="t" node [shape="circle"] I [label="", style=invis, width=0] I -> 0 @@ -67,6 +71,8 @@ digraph G { } digraph G { rankdir=LR + label="t\n[Fin-less 2]" + labelloc="t" node [shape="circle"] I [label="", style=invis, width=0] I -> 0 @@ -80,6 +86,8 @@ digraph G { } digraph G { rankdir=LR + label="t\n[Fin-less 2]" + labelloc="t" node [shape="circle"] I [label="", style=invis, width=0] I -> 0 @@ -96,6 +104,8 @@ digraph G { } digraph G { rankdir=LR + label="t\n[Fin-less 2]" + labelloc="t" node [shape="circle"] I [label="", style=invis, width=0] I -> 0 @@ -110,6 +120,8 @@ digraph G { } digraph G { rankdir=LR + label="t\n[Fin-less 2]" + labelloc="t" I [label="", style=invis, width=0] I -> 0 0 [label="0"] @@ -223,6 +235,8 @@ digraph G { } digraph G { rankdir=LR + label="t\n[all]" + labelloc="t" node [shape="circle"] I [label="", style=invis, width=0] I -> 2 @@ -235,6 +249,8 @@ digraph G { 2 -> 0 digraph G { rankdir=LR + label="t\n[all]" + labelloc="t" node [shape="circle"] I [label="", style=invis, width=0] I -> 0 diff --git a/tests/core/wdba.test b/tests/core/wdba.test index f4ead1d25..e3e5175f0 100755 --- a/tests/core/wdba.test +++ b/tests/core/wdba.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2014, 2015 Laboratoire de Recherche et +# Copyright (C) 2010, 2014, 2015, 2018 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -99,7 +99,7 @@ while read f; do # worked. x=`../ikwiad -f -Rm "!($f)" | grep -v -- '->' | - sed -n 's/.*label="\(..*\)".*/\1/p' | + sed -n 's/.*\[.*label="\(..*\)".*/\1/p' | tr -d '0-9\n'` case $x in "") echo "OK !($f)";; diff --git a/tests/python/_autparserr.ipynb b/tests/python/_autparserr.ipynb index 7bbd51789..138d3ae1c 100644 --- a/tests/python/_autparserr.ipynb +++ b/tests/python/_autparserr.ipynb @@ -74,11 +74,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "1\n", @@ -112,7 +113,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f72fc2978d0> >" + " *' at 0x7f6380ea5f30> >" ] }, "metadata": {}, @@ -123,6 +124,11 @@ "evalue": "\n_example.aut:20.2: syntax error, unexpected identifier\n_example.aut:20.1-3: ignoring this invalid label\n_example.aut:20.5: state number is larger than state count...\n_example.aut:14.1-9: ... declared here.\n ()", "output_type": "error", "traceback": [ + "Traceback \u001b[0;36m(most recent call last)\u001b[0m:\n", + " File \u001b[1;32m\"/home/adl/.local/lib/python3.6/site-packages/IPython/core/interactiveshell.py\"\u001b[0m, line \u001b[1;32m2910\u001b[0m, in \u001b[1;35mrun_code\u001b[0m\n exec(code_obj, self.user_global_ns, self.user_ns)\n", + " File \u001b[1;32m\"\"\u001b[0m, line \u001b[1;32m1\u001b[0m, in \u001b[1;35m\u001b[0m\n for a in spot.automata('_example.aut'):\n", + " File \u001b[1;32m\"/home/adl/git/spot/python/spot/__init__.py\"\u001b[0m, line \u001b[1;32m446\u001b[0m, in \u001b[1;35mautomata\u001b[0m\n a = p.parse(_bdd_dict).aut\n", + "\u001b[0;36m File \u001b[0;32m\"/home/adl/git/spot/python/spot/impl.py\"\u001b[0;36m, line \u001b[0;32m5173\u001b[0;36m, in \u001b[0;35mparse\u001b[0;36m\u001b[0m\n\u001b[0;31m return _impl.automaton_stream_parser_parse(self, *args)\u001b[0m\n", "\u001b[0;36m File \u001b[0;32m\"\"\u001b[0;36m, line \u001b[0;32munknown\u001b[0m\n\u001b[0;31mSyntaxError\u001b[0m\u001b[0;31m:\u001b[0m \n_example.aut:20.2: syntax error, unexpected identifier\n_example.aut:20.1-3: ignoring this invalid label\n_example.aut:20.5: state number is larger than state count...\n_example.aut:14.1-9: ... declared here.\n\n" ] } @@ -146,11 +152,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "1\n", @@ -184,7 +191,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f72fc2ce090> >" + " *' at 0x7f6380e09360> >" ] }, "execution_count": 4, @@ -216,8 +223,8 @@ "\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-cmd |'\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/__init__.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 479\u001b[0m See `spot.automata` for a list of supported formats.\"\"\"\n\u001b[1;32m 480\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 481\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 482\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 483\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 464\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 465\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--> 466\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 467\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 468\u001b[0m \u001b[0;31m# reporting the following error: \" 481\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 482\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 483\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~/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 464\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 465\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--> 466\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 467\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 468\u001b[0m \u001b[0;31m# reporting the following error: \"\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'sleep 3; cat _example.aut |'\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mtimeout\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0;36m1\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/__init__.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 479\u001b[0m See `spot.automata` for a list of supported formats.\"\"\"\n\u001b[1;32m 480\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 481\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 482\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 483\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 423\u001b[0m \u001b[0;32melse\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 424\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 425\u001b[0;31m \u001b[0mout\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0merr\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mcommunicate\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtimeout\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0mtimeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 426\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mTimeoutExpired\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 427\u001b[0m \u001b[0;31m# Using subprocess.check_output() with timeout\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m~/git/spot/python/spot/__init__.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 479\u001b[0m See `spot.automata` for a list of supported formats.\"\"\"\n\u001b[1;32m 480\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 481\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 482\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 483\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~/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 423\u001b[0m \u001b[0;32melse\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 424\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 425\u001b[0;31m \u001b[0mout\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0merr\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mcommunicate\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtimeout\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0mtimeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 426\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mTimeoutExpired\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 427\u001b[0m \u001b[0;31m# Using subprocess.check_output() with timeout\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", "\u001b[0;32m/usr/lib/python3.6/subprocess.py\u001b[0m in \u001b[0;36mcommunicate\u001b[0;34m(self, input, timeout)\u001b[0m\n\u001b[1;32m 841\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 842\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 843\u001b[0;31m \u001b[0mstdout\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mstderr\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m_communicate\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0minput\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mendtime\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mtimeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 844\u001b[0m \u001b[0;32mfinally\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 845\u001b[0m \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m_communication_started\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;32mTrue\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", "\u001b[0;32m/usr/lib/python3.6/subprocess.py\u001b[0m in \u001b[0;36m_communicate\u001b[0;34m(self, input, endtime, orig_timeout)\u001b[0m\n\u001b[1;32m 1513\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 1514\u001b[0m \u001b[0mready\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mselector\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mselect\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtimeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 1515\u001b[0;31m \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m_check_timeout\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mendtime\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0morig_timeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 1516\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 1517\u001b[0m \u001b[0;31m# XXX Rewrite these to use non-blocking I/O on the file\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", "\u001b[0;32m/usr/lib/python3.6/subprocess.py\u001b[0m in \u001b[0;36m_check_timeout\u001b[0;34m(self, endtime, orig_timeout)\u001b[0m\n\u001b[1;32m 869\u001b[0m \u001b[0;32mreturn\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 870\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0m_time\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m>\u001b[0m \u001b[0mendtime\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 871\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0mTimeoutExpired\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0margs\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0morig_timeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 872\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 873\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n", @@ -266,11 +273,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "1\n", @@ -310,7 +318,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f72fc2ce5a0> >" + " *' at 0x7f6380e098a0> >" ] }, "metadata": {}, @@ -324,7 +332,7 @@ "\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/__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 464\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 465\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--> 466\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 467\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 468\u001b[0m \u001b[0;31m# reporting the following error: \" 466\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 467\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 468\u001b[0m \u001b[0;31m# reporting the following error: \" 481\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 482\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~/git/spot/python/spot/__init__.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 480\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 481\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 482\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/__init__.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 481\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 482\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--> 483\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 484\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 485\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m~/git/spot/python/spot/__init__.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 481\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 482\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--> 483\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 484\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 485\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n", "\u001b[0;31mRuntimeError\u001b[0m: Failed to read automaton from true|" ] } @@ -393,7 +401,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.4" + "version": "3.6.4+" } }, "nbformat": 4, diff --git a/tests/python/automata-io.ipynb b/tests/python/automata-io.ipynb index ea4395d4f..afeafa394 100644 --- a/tests/python/automata-io.ipynb +++ b/tests/python/automata-io.ipynb @@ -61,6 +61,8 @@ "\n", "digraph G {\n", " rankdir=LR\n", + " label=<
[Büchi]>\n", + " labelloc=\"t\"\n", " node [shape=\"circle\"]\n", " node [style=\"filled\", fillcolor=\"#ffffaa\"]\n", " fontname=\"Lato\"\n", @@ -122,11 +124,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "1\n", @@ -166,7 +169,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa1c833b9f0> >" + " *' at 0x7f1f40579030> >" ] }, "execution_count": 3, @@ -245,11 +248,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "1\n", @@ -289,7 +293,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa1c82e10c0> >" + " *' at 0x7f1f40528ab0> >" ] }, "metadata": {}, @@ -304,11 +308,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -348,7 +353,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa1c82abab0> >" + " *' at 0x7f1f40528360> >" ] }, "metadata": {}, @@ -420,11 +425,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "1\n", @@ -464,7 +470,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa1c82ab870> >" + " *' at 0x7f1f40528b10> >" ] }, "metadata": {}, @@ -504,11 +510,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "1\n", @@ -548,7 +555,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa1c82aba50> >" + " *' at 0x7f1f40542fc0> >" ] }, "metadata": {}, @@ -563,42 +570,48 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")&Inf(\n", + "❶\n", + ")\n", + "[gen. Büchi 2]\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", - "1\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "1\n", + "⓿\n", + "❶\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", - "⓿\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fa1c82e10f0> >" + " *' at 0x7f1f405426f0> >" ] }, "metadata": {}, @@ -658,11 +671,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -702,7 +716,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa1c82ab900> >" + " *' at 0x7f1f404d3390> >" ] }, "metadata": {}, @@ -717,11 +731,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -755,7 +770,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa1c82e1120> >" + " *' at 0x7f1f405427e0> >" ] }, "metadata": {}, @@ -770,11 +785,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -803,7 +822,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa1c82ab930> >" + " *' at 0x7f1f40dc6240> >" ] }, "metadata": {}, @@ -818,11 +837,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -862,7 +885,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa1c82e1030> >" + " *' at 0x7f1f405426f0> >" ] }, "metadata": {}, @@ -895,11 +918,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -939,7 +963,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa1c82e1120> >" + " *' at 0x7f1f405338d0> >" ] }, "execution_count": 10, @@ -953,7 +977,7 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 11, "metadata": {}, "outputs": [], "source": [ @@ -977,7 +1001,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.4" + "version": "3.6.4+" } }, "nbformat": 4, diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index a43b340c4..c13ea1afd 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -32,11 +32,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -145,7 +146,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d08673930> >" + " *' at 0x7fb100253060> >" ] }, "execution_count": 2, @@ -172,10 +173,11 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -447,7 +449,7 @@ } ], "source": [ - "a.show(\".ast\")" + "a.show(\".st\")" ] }, { @@ -494,11 +496,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "1\n", @@ -538,7 +541,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d0857cbd0> >" + " *' at 0x7fb1002c4fc0> >" ] }, "execution_count": 6, @@ -564,11 +567,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "1\n", @@ -608,7 +612,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d08673960> >" + " *' at 0x7fb10017ff90> >" ] }, "execution_count": 7, @@ -641,11 +645,13 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "1\n", @@ -684,7 +690,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d08673b40> >" + " *' at 0x7fb1002029f0> >" ] }, "execution_count": 8, @@ -734,10 +740,11 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -827,10 +834,11 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "6\n", @@ -1030,11 +1038,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -1144,7 +1156,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d0858c360> >" + " *' at 0x7fb100190660> >" ] }, "execution_count": 12, @@ -1177,11 +1189,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -1245,7 +1261,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d0857c450> >" + " *' at 0x7fb100190240> >" ] }, "execution_count": 13, @@ -1278,11 +1294,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -1363,7 +1380,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d0857c420> >" + " *' at 0x7fb100190600> >" ] }, "execution_count": 14, @@ -1396,11 +1413,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -1462,7 +1483,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d0857c480> >" + " *' at 0x7fb1001908a0> >" ] }, "execution_count": 15, @@ -1488,11 +1509,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -1932,7 +1957,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d0b183ae0> >" + " *' at 0x7fb10016f9f0> >" ] }, "execution_count": 16, @@ -2016,388 +2041,122 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "(Inf(\n", - "⓿\n", - ") & Fin(\n", - "❶\n", - ") & Fin(\n", - "❸\n", - ")) | (Inf(\n", - "❷\n", - ")&Inf(\n", - "❸\n", - ")) | Inf(\n", - "❶\n", - ")\n", + "\n", + "(Inf(\n", + "⓿\n", + ") & Fin(\n", + "❶\n", + ") & Fin(\n", + "❸\n", + ")) | (Inf(\n", + "❷\n", + ")&Inf(\n", + "❸\n", + ")) | Inf(\n", + "❶\n", + ")\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "❸\n", + "0->0\n", + "\n", + "\n", + "1\n", + "❸\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "❶\n", - "❸\n", + "0->1\n", + "\n", + "\n", + "a\n", + "❶\n", + "❸\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", - "⓿\n", - "❸\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "⓿\n", + "❸\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "❸\n", + "1->0\n", + "\n", + "\n", + "b\n", + "❸\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", - "⓿\n", - "❸\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "❸\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & b\n", - "❷\n", - "❸\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", + "❷\n", + "❸\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "!b\n", + "2->0\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b\n", - "⓿\n", + "2->1\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", "\n", "\n", - "" + "\n" ], "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "⓿\n", - ") | Inf(\n", - "❶\n", - ") | (Inf(\n", - "❷\n", - ")&Inf(\n", - "❸\n", - "))\n", - "[Fin-less 4]\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "❸\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "❶\n", - "❸\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!a\n", - "❸\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "❸\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", - "❸\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!a & b\n", - "❷\n", - "❸\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", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", - "\n", - "\n", - "" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\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\n", - "⓿\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", - "⓿\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\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", - "3->4\n", - "\n", - "\n", - "a | b\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", - "\n", - "\n", - "" - ], - "text/plain": [ - "" + " *' at 0x7fb100190a20> >" ] }, "metadata": {}, @@ -2412,11 +2171,299 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ") | Inf(\n", + "❶\n", + ") | (Inf(\n", + "❷\n", + ")&Inf(\n", + "❸\n", + "))\n", + "[Fin-less 4]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "❸\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "❶\n", + "❸\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "❸\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "❸\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "❸\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", + "❷\n", + "❸\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", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fb100248e10> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\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\n", + "⓿\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", + "⓿\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\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", + "3->4\n", + "\n", + "\n", + "a | b\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fb10016fb70> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -2550,7 +2597,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d0858c600> >" + " *' at 0x7fb100248e10> >" ] }, "metadata": {}, @@ -2559,9 +2606,9 @@ ], "source": [ "a = spot.automaton('example1.aut')\n", - "display(a.show('.a'))\n", - "display(spot.remove_fin(a).show('.a'))\n", - "display(a.postprocess('TGBA', 'complete').show('.a'))\n", + "display(a)\n", + "display(spot.remove_fin(a))\n", + "display(a.postprocess('TGBA', 'complete'))\n", "display(a.postprocess('BA'))" ] }, @@ -2588,11 +2635,24 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "(Inf(\n", + "⓿\n", + ") & Fin(\n", + "❶\n", + ") & Fin(\n", + "❸\n", + ")) | (Inf(\n", + "❷\n", + ")&Inf(\n", + "❸\n", + ")) | Inf(\n", + "❶\n", + ")\n", "\n", "\n", "0\n", @@ -2707,7 +2767,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d0858c450> >" + " *' at 0x7fb100190de0> >" ] }, "execution_count": 21, @@ -2733,11 +2793,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -2777,7 +2838,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d0858c390> >" + " *' at 0x7fb100190d20> >" ] }, "execution_count": 22, @@ -3142,10 +3203,10 @@ "source": [ "# Using +1 in the display options is a convient way to shift the \n", "# set numbers in the output, as an aid in reading the product.\n", - "a1 = spot.translate('a W c'); display(a1.show('.bat'))\n", - "a2 = spot.translate('a U b'); display(a2.show('.bat+1'))\n", + "a1 = spot.translate('a W c'); display(a1.show('.t'))\n", + "a2 = spot.translate('a U b'); display(a2.show('.t+1'))\n", "# the product should display pairs of states, unless asked not to (using 1).\n", - "p = spot.product(a1, a2); display(p.show('.bat')); display(p.show('.bat1'))" + "p = spot.product(a1, a2); display(p.show('.t')); display(p.show('.t1'))" ] }, { @@ -3169,11 +3230,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -3213,7 +3278,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d0858c1b0> >" + " *' at 0x7fb10019c990> >" ] }, "metadata": {}, @@ -3243,64 +3308,71 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "⓿\n", - ") & Inf(\n", - "❶\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a\n", + "0->0\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "❶\n", + "0->1\n", + "\n", + "\n", + "a\n", + "❶\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "1->0\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a\n", - "❶\n", + "1->1\n", + "\n", + "\n", + "a\n", + "❶\n", "\n", "\n", - "" + "\n" ], "text/plain": [ - "" + " *' at 0x7fb10019c1b0> >" ] }, "execution_count": 25, @@ -3309,7 +3381,7 @@ } ], "source": [ - "spot.tgba_determinize(a).show('.ba')" + "spot.tgba_determinize(a)" ] }, { @@ -3327,64 +3399,71 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "⓿\n", - ") & Inf(\n", - "❶\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a\n", + "0->0\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "❶\n", + "0->1\n", + "\n", + "\n", + "a\n", + "❶\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "1->0\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a\n", - "❶\n", + "1->1\n", + "\n", + "\n", + "a\n", + "❶\n", "\n", "\n", - "" + "\n" ], "text/plain": [ - "" + " *' at 0x7fb10019ca20> >" ] }, "execution_count": 26, @@ -3393,7 +3472,7 @@ } ], "source": [ - "aut = spot.translate('FGa', 'generic', 'deterministic'); aut.show('.ba')" + "aut = spot.translate('FGa', 'generic', 'deterministic'); aut" ] }, { @@ -3467,7 +3546,7 @@ } ], "source": [ - "spot.translate('FGa', 'coBuchi').show('.ba')" + "spot.translate('FGa', 'coBuchi').show('.b')" ] }, { @@ -3541,7 +3620,7 @@ } ], "source": [ - "spot.translate('FGa', 'coBuchi', 'deterministic').show('.ba')" + "spot.translate('FGa', 'coBuchi', 'deterministic').show('.b')" ] }, { @@ -3565,11 +3644,17 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "0\n", @@ -3617,7 +3702,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d0858c570> >" + " *' at 0x7fb10019ca20> >" ] }, "execution_count": 29, @@ -3654,11 +3739,17 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "0\n", @@ -3706,7 +3797,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9d0858c570> >" + " *' at 0x7fb10019ca20> >" ] }, "execution_count": 30, @@ -3739,7 +3830,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.4" + "version": "3.6.4+" } }, "nbformat": 4, diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index c7247503a..29c1bce74 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -3,9 +3,7 @@ { "cell_type": "code", "execution_count": 1, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "import spot\n", @@ -29,9 +27,7 @@ { "cell_type": "code", "execution_count": 2, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "a = spot.translate('a U b U c')" @@ -47,17 +43,16 @@ { "cell_type": "code", "execution_count": 3, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "2\n", @@ -148,9 +143,7 @@ { "cell_type": "code", "execution_count": 4, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -161,11 +154,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "2\n", @@ -228,7 +222,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe1205e8990> >" + " *' at 0x7f5e8c08c090> >" ] }, "execution_count": 4, @@ -252,9 +246,7 @@ { "cell_type": "code", "execution_count": 5, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -265,11 +257,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "2\n", @@ -332,7 +325,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe1205e8a80> >" + " *' at 0x7f5e857897b0> >" ] }, "execution_count": 5, @@ -354,9 +347,7 @@ { "cell_type": "code", "execution_count": 6, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -367,11 +358,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "2\n", @@ -434,7 +426,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe1205e8990> >" + " *' at 0x7f5e8c08c090> >" ] }, "execution_count": 6, @@ -458,9 +450,7 @@ { "cell_type": "code", "execution_count": 7, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -530,9 +520,7 @@ { "cell_type": "code", "execution_count": 8, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -543,11 +531,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -651,7 +643,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d1b0> >" + " *' at 0x7f5e85789bd0> >" ] }, "execution_count": 8, @@ -666,9 +658,7 @@ { "cell_type": "code", "execution_count": 9, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -695,9 +685,7 @@ { "cell_type": "code", "execution_count": 10, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "r.highlight(5) # the parameter is a color number" @@ -713,9 +701,7 @@ { "cell_type": "code", "execution_count": 11, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -726,11 +712,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -834,7 +824,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d1b0> >" + " *' at 0x7f5e85789bd0> >" ] }, "execution_count": 11, @@ -858,9 +848,7 @@ { "cell_type": "code", "execution_count": 12, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -871,11 +859,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "1\n", @@ -915,7 +904,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d2d0> >" + " *' at 0x7f5e85799030> >" ] }, "metadata": {}, @@ -930,11 +919,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -963,7 +956,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d150> >" + " *' at 0x7f5e85799720> >" ] }, "metadata": {}, @@ -979,9 +972,7 @@ { "cell_type": "code", "execution_count": 13, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -992,11 +983,17 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")&Inf(\n", + "❶\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "0\n", @@ -1052,7 +1049,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d2a0> >" + " *' at 0x7f5e857a9660> >" ] }, "execution_count": 13, @@ -1067,9 +1064,7 @@ { "cell_type": "code", "execution_count": 14, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1096,9 +1091,7 @@ { "cell_type": "code", "execution_count": 15, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "run.highlight(5)\n", @@ -1111,9 +1104,7 @@ { "cell_type": "code", "execution_count": 16, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1124,11 +1115,17 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")&Inf(\n", + "❶\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "0\n", @@ -1184,7 +1181,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d2a0> >" + " *' at 0x7f5e857a9660> >" ] }, "metadata": {}, @@ -1199,11 +1196,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "1\n", @@ -1243,7 +1241,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d2d0> >" + " *' at 0x7f5e85799030> >" ] }, "metadata": {}, @@ -1258,11 +1256,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -1291,7 +1293,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d150> >" + " *' at 0x7f5e85799720> >" ] }, "metadata": {}, @@ -1312,9 +1314,7 @@ { "cell_type": "code", "execution_count": 17, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1345,11 +1345,17 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")&Inf(\n", + "❶\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "0\n", @@ -1496,7 +1502,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d210> >" + " *' at 0x7f5e857a9930> >" ] }, "metadata": {}, @@ -1511,11 +1517,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -1572,7 +1582,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d1e0> >" + " *' at 0x7f5e857a9a20> >" ] }, "metadata": {}, @@ -1587,11 +1597,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "3\n", @@ -1658,7 +1669,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d270> >" + " *' at 0x7f5e857a9900> >" ] }, "metadata": {}, @@ -1687,9 +1698,7 @@ { "cell_type": "code", "execution_count": 18, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1700,11 +1709,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -1808,7 +1821,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d330> >" + " *' at 0x7f5e857a9a50> >" ] }, "execution_count": 18, @@ -1837,9 +1850,7 @@ { "cell_type": "code", "execution_count": 19, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1850,11 +1861,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "4\n", @@ -1958,7 +1973,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d330> >" + " *' at 0x7f5e857a9a50> >" ] }, "execution_count": 19, @@ -1982,9 +1997,7 @@ { "cell_type": "code", "execution_count": 20, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1995,11 +2008,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "4\n", @@ -2103,7 +2120,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe12058d330> >" + " *' at 0x7f5e857a9a50> >" ] }, "metadata": {}, @@ -2112,10 +2129,14 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -2218,10 +2239,14 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -2288,9 +2313,7 @@ { "cell_type": "code", "execution_count": 21, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -2525,7 +2548,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.4" + "version": "3.6.4+" } }, "nbformat": 4, diff --git a/tests/python/ltsmin-dve.ipynb b/tests/python/ltsmin-dve.ipynb index 51d0978b3..7962e3b22 100644 --- a/tests/python/ltsmin-dve.ipynb +++ b/tests/python/ltsmin-dve.ipynb @@ -3,9 +3,7 @@ { "cell_type": "code", "execution_count": 1, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "import spot\n", @@ -32,9 +30,7 @@ { "cell_type": "code", "execution_count": 2, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "!rm -f test1.dve" @@ -43,9 +39,7 @@ { "cell_type": "code", "execution_count": 3, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -89,9 +83,7 @@ { "cell_type": "code", "execution_count": 4, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "m = spot.ltsmin.load('test1.dve')" @@ -109,9 +101,7 @@ { "cell_type": "code", "execution_count": 5, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "!rm -f test1.dve test1.dve.cpp test1.dve2C" @@ -130,9 +120,7 @@ { "cell_type": "code", "execution_count": 6, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "%%dve m\n", @@ -171,9 +159,7 @@ { "cell_type": "code", "execution_count": 7, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -197,9 +183,7 @@ { "cell_type": "code", "execution_count": 8, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -228,9 +212,7 @@ { "cell_type": "code", "execution_count": 9, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -241,11 +223,13 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "0\n", @@ -421,7 +405,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f402430f9c0> >" + " *' at 0x7f74b867eab0> >" ] }, "execution_count": 9, @@ -437,17 +421,17 @@ { "cell_type": "code", "execution_count": 10, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "0\n", @@ -718,17 +702,17 @@ { "cell_type": "code", "execution_count": 11, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "0\n", @@ -1076,9 +1060,7 @@ { "cell_type": "code", "execution_count": 12, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1089,11 +1071,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "1\n", @@ -1133,7 +1116,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f4024027150> >" + " *' at 0x7f74b860d990> >" ] }, "execution_count": 12, @@ -1148,9 +1131,7 @@ { "cell_type": "code", "execution_count": 13, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1161,16 +1142,20 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", "\n", - "a=0, b=0, Q=0 * 1\n", + "a=0, b=0, Q=0 * 1\n", "\n", "\n", "I->0\n", @@ -1180,7 +1165,7 @@ "\n", "1\n", "\n", - "a=1, b=0, Q=0 * 1\n", + "a=1, b=0, Q=0 * 1\n", "\n", "\n", "0->1\n", @@ -1191,7 +1176,7 @@ "\n", "2\n", "\n", - "a=0, b=1, Q=0 * 1\n", + "a=0, b=1, Q=0 * 1\n", "\n", "\n", "0->2\n", @@ -1202,7 +1187,7 @@ "\n", "3\n", "\n", - "a=1, b=1, Q=0 * 1\n", + "a=1, b=1, Q=0 * 1\n", "\n", "\n", "2->3\n", @@ -1213,7 +1198,7 @@ "\n", "4\n", "\n", - "a=0, b=2, Q=0 * 1\n", + "a=0, b=2, Q=0 * 1\n", "\n", "\n", "2->4\n", @@ -1224,7 +1209,7 @@ "\n", "5\n", "\n", - "a=1, b=2, Q=0 * 1\n", + "a=1, b=2, Q=0 * 1\n", "\n", "\n", "4->5\n", @@ -1235,7 +1220,7 @@ "\n", "6\n", "\n", - "a=0, b=3, Q=0 * 1\n", + "a=0, b=3, Q=0 * 1\n", "\n", "\n", "4->6\n", @@ -1246,7 +1231,7 @@ "\n", "7\n", "\n", - "a=0, b=2, Q=1 * 1\n", + "a=0, b=2, Q=1 * 1\n", "\n", "\n", "4->7\n", @@ -1257,7 +1242,7 @@ "\n", "8\n", "\n", - "a=0, b=3, Q=1 * 0\n", + "a=0, b=3, Q=1 * 0\n", "\n", "\n", "6->8\n", @@ -1278,7 +1263,7 @@ "\n", "9\n", "\n", - "a=1, b=2, Q=1 * 1\n", + "a=1, b=2, Q=1 * 1\n", "\n", "\n", "7->9\n", @@ -1297,7 +1282,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f402430ffc0> >" + " *' at 0x7f74b867e5d0> >" ] }, "execution_count": 13, @@ -1319,9 +1304,7 @@ { "cell_type": "code", "execution_count": 14, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1344,9 +1327,7 @@ { "cell_type": "code", "execution_count": 15, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "def model_check(f, m):\n", @@ -1359,9 +1340,7 @@ { "cell_type": "code", "execution_count": 16, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1387,10 +1366,8 @@ }, { "cell_type": "code", - "execution_count": 21, - "metadata": { - "collapsed": true - }, + "execution_count": 17, + "metadata": {}, "outputs": [], "source": [ "def model_debug(f, m):\n", @@ -1402,10 +1379,8 @@ }, { "cell_type": "code", - "execution_count": 23, - "metadata": { - "collapsed": false - }, + "execution_count": 18, + "metadata": {}, "outputs": [ { "data": { @@ -1422,7 +1397,7 @@ " | !\"a<1\" & !\"b > 1\" & dead" ] }, - "execution_count": 23, + "execution_count": 18, "metadata": {}, "output_type": "execute_result" } @@ -1440,10 +1415,8 @@ }, { "cell_type": "code", - "execution_count": 24, - "metadata": { - "collapsed": false - }, + "execution_count": 19, + "metadata": {}, "outputs": [ { "data": { @@ -1454,11 +1427,13 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "0\n", @@ -1513,10 +1488,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f4024027720> >" + " *' at 0x7f74b860ded0> >" ] }, - "execution_count": 24, + "execution_count": 19, "metadata": {}, "output_type": "execute_result" } @@ -1542,7 +1517,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.3" + "version": "3.6.4+" } }, "nbformat": 4, diff --git a/tests/python/ltsmin-pml.ipynb b/tests/python/ltsmin-pml.ipynb index 1e6140d55..8503c7703 100644 --- a/tests/python/ltsmin-pml.ipynb +++ b/tests/python/ltsmin-pml.ipynb @@ -3,9 +3,7 @@ { "cell_type": "code", "execution_count": 1, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "import spot\n", @@ -31,9 +29,7 @@ { "cell_type": "code", "execution_count": 2, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stderr", @@ -42,8 +38,8 @@ "SpinS Promela Compiler - version 1.1 (3-Feb-2015)\n", "(C) University of Twente, Formal Methods and Tools group\n", "\n", - "Parsing tmpmmk02hmw.pml...\n", - "Parsing tmpmmk02hmw.pml done (0.0 sec)\n", + "Parsing tmpfz39v5au.pml...\n", + "Parsing tmpfz39v5au.pml done (0.0 sec)\n", "\n", "Optimizing graphs...\n", " StateMerging changed 0 states/transitions.\n", @@ -229,8 +225,8 @@ " Found 2 / 2 (100.0%) Commuting actions \n", "Generating guard dependency matrices done (0.0 sec)\n", "\n", - "Written C code to /home/adl/git/spot/tests/python/tmpmmk02hmw.pml.spins.c\n", - "Compiled C code to PINS library tmpmmk02hmw.pml.spins\n", + "Written C code to /home/adl/git/spot/tests/python/tmpfz39v5au.pml.spins.c\n", + "Compiled C code to PINS library tmpfz39v5au.pml.spins\n", "\n" ] } @@ -257,9 +253,7 @@ { "cell_type": "code", "execution_count": 3, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -289,9 +283,7 @@ { "cell_type": "code", "execution_count": 4, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -302,17 +294,19 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "0\n", "\n", - "P_0._pc=0, P_0.a=0, P_0.b=0\n", - ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "P_0._pc=0, P_0.a=0, P_0.b=0\n", + ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", "\n", "\n", "I->0\n", @@ -322,8 +316,8 @@ "\n", "1\n", "\n", - "P_0._pc=0, P_0.a=1, P_0.b=0\n", - ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "P_0._pc=0, P_0.a=1, P_0.b=0\n", + ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", "\n", "\n", "0->1\n", @@ -333,8 +327,8 @@ "\n", "2\n", "\n", - "P_0._pc=0, P_0.a=0, P_0.b=1\n", - ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "P_0._pc=0, P_0.a=0, P_0.b=1\n", + ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", "\n", "\n", "0->2\n", @@ -344,8 +338,8 @@ "\n", "3\n", "\n", - "P_0._pc=0, P_0.a=2, P_0.b=0\n", - "!"P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "P_0._pc=0, P_0.a=2, P_0.b=0\n", + "!"P_0.a < 2" & !"P_0.b > 1" & !dead\n", "\n", "\n", "1->3\n", @@ -355,8 +349,8 @@ "\n", "4\n", "\n", - "P_0._pc=0, P_0.a=1, P_0.b=1\n", - ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "P_0._pc=0, P_0.a=1, P_0.b=1\n", + ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", "\n", "\n", "1->4\n", @@ -371,8 +365,8 @@ "\n", "5\n", "\n", - "P_0._pc=0, P_0.a=0, P_0.b=2\n", - ""P_0.a < 2" & "P_0.b > 1" & !dead\n", + "P_0._pc=0, P_0.a=0, P_0.b=2\n", + ""P_0.a < 2" & "P_0.b > 1" & !dead\n", "\n", "\n", "2->5\n", @@ -382,8 +376,8 @@ "\n", "6\n", "\n", - "P_0._pc=0, P_0.a=3, P_0.b=0\n", - "!"P_0.a < 2" & !"P_0.b > 1" & dead\n", + "P_0._pc=0, P_0.a=3, P_0.b=0\n", + "!"P_0.a < 2" & !"P_0.b > 1" & dead\n", "\n", "\n", "3->6\n", @@ -393,8 +387,8 @@ "\n", "7\n", "\n", - "P_0._pc=0, P_0.a=2, P_0.b=1\n", - "!"P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "P_0._pc=0, P_0.a=2, P_0.b=1\n", + "!"P_0.a < 2" & !"P_0.b > 1" & !dead\n", "\n", "\n", "3->7\n", @@ -409,8 +403,8 @@ "\n", "8\n", "\n", - "P_0._pc=0, P_0.a=1, P_0.b=2\n", - ""P_0.a < 2" & "P_0.b > 1" & !dead\n", + "P_0._pc=0, P_0.a=1, P_0.b=2\n", + ""P_0.a < 2" & "P_0.b > 1" & !dead\n", "\n", "\n", "4->8\n", @@ -425,8 +419,8 @@ "\n", "9\n", "\n", - "P_0._pc=0, P_0.a=0, P_0.b=3\n", - ""P_0.a < 2" & "P_0.b > 1" & dead\n", + "P_0._pc=0, P_0.a=0, P_0.b=3\n", + ""P_0.a < 2" & "P_0.b > 1" & dead\n", "\n", "\n", "5->9\n", @@ -441,8 +435,8 @@ "\n", "10\n", "\n", - "P_0._pc=0, P_0.a=3, P_0.b=1\n", - "!"P_0.a < 2" & !"P_0.b > 1" & dead\n", + "P_0._pc=0, P_0.a=3, P_0.b=1\n", + "!"P_0.a < 2" & !"P_0.b > 1" & dead\n", "\n", "\n", "7->10\n", @@ -452,8 +446,8 @@ "\n", "11\n", "\n", - "P_0._pc=0, P_0.a=2, P_0.b=2\n", - "!"P_0.a < 2" & "P_0.b > 1" & !dead\n", + "P_0._pc=0, P_0.a=2, P_0.b=2\n", + "!"P_0.a < 2" & "P_0.b > 1" & !dead\n", "\n", "\n", "7->11\n", @@ -468,8 +462,8 @@ "\n", "12\n", "\n", - "P_0._pc=0, P_0.a=1, P_0.b=3\n", - ""P_0.a < 2" & "P_0.b > 1" & dead\n", + "P_0._pc=0, P_0.a=1, P_0.b=3\n", + ""P_0.a < 2" & "P_0.b > 1" & dead\n", "\n", "\n", "8->12\n", @@ -489,8 +483,8 @@ "\n", "13\n", "\n", - "P_0._pc=0, P_0.a=3, P_0.b=2\n", - "!"P_0.a < 2" & "P_0.b > 1" & dead\n", + "P_0._pc=0, P_0.a=3, P_0.b=2\n", + "!"P_0.a < 2" & "P_0.b > 1" & dead\n", "\n", "\n", "11->13\n", @@ -500,8 +494,8 @@ "\n", "14\n", "\n", - "P_0._pc=0, P_0.a=2, P_0.b=3\n", - "!"P_0.a < 2" & "P_0.b > 1" & dead\n", + "P_0._pc=0, P_0.a=2, P_0.b=3\n", + "!"P_0.a < 2" & "P_0.b > 1" & dead\n", "\n", "\n", "11->14\n", @@ -527,7 +521,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fe0808e0240> >" + " *' at 0x7fb9a46cb540> >" ] }, "execution_count": 4, @@ -554,9 +548,7 @@ { "cell_type": "code", "execution_count": 5, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "!rm -rf test1.pml" @@ -565,9 +557,7 @@ { "cell_type": "code", "execution_count": 6, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -599,9 +589,7 @@ { "cell_type": "code", "execution_count": 7, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "model2 = spot.ltsmin.load('test1.pml')" @@ -610,9 +598,7 @@ { "cell_type": "code", "execution_count": 8, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -635,9 +621,7 @@ { "cell_type": "code", "execution_count": 9, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "!rm -f test1.pml test1.pml.spins.c test1.pml.spins" @@ -660,7 +644,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.1" + "version": "3.6.4+" } }, "nbformat": 4, diff --git a/tests/python/product.ipynb b/tests/python/product.ipynb index 05c583bfd..b083245bd 100644 --- a/tests/python/product.ipynb +++ b/tests/python/product.ipynb @@ -3,9 +3,7 @@ { "cell_type": "code", "execution_count": 1, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "from IPython.display import display, HTML\n", @@ -36,9 +34,7 @@ { "cell_type": "code", "execution_count": 2, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -385,9 +381,7 @@ { "cell_type": "code", "execution_count": 3, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -741,9 +735,7 @@ { "cell_type": "code", "execution_count": 4, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1091,9 +1083,7 @@ { "cell_type": "code", "execution_count": 5, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -1133,9 +1123,7 @@ { "cell_type": "code", "execution_count": 6, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1531,9 +1519,7 @@ { "cell_type": "code", "execution_count": 7, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -1578,9 +1564,7 @@ { "cell_type": "code", "execution_count": 8, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -1632,9 +1616,7 @@ { "cell_type": "code", "execution_count": 9, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -2033,17 +2015,23 @@ { "cell_type": "code", "execution_count": 10, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")&Inf(\n", + "❶\n", + ")&Inf(\n", + "❷\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", "0\n", @@ -2249,15 +2237,13 @@ { "cell_type": "code", "execution_count": 11, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "1000 loops, best of 3: 231 µs per loop\n" + "234 µs ± 14.8 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)\n" ] } ], @@ -2268,16 +2254,13 @@ { "cell_type": "code", "execution_count": 12, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "The slowest run took 5.96 times longer than the fastest. This could mean that an intermediate result is being cached.\n", - "100000 loops, best of 3: 4.6 µs per loop\n" + "3.45 µs ± 160 ns per loop (mean ± std. dev. of 7 runs, 100000 loops each)\n" ] } ], @@ -2311,7 +2294,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.4" + "version": "3.6.4+" } }, "nbformat": 4, diff --git a/tests/python/testingaut.ipynb b/tests/python/testingaut.ipynb index 1564c5230..b96107f3c 100644 --- a/tests/python/testingaut.ipynb +++ b/tests/python/testingaut.ipynb @@ -3,9 +3,7 @@ { "cell_type": "code", "execution_count": 1, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "from IPython.display import display, HTML\n", @@ -25,9 +23,7 @@ { "cell_type": "code", "execution_count": 2, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -38,11 +34,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -82,7 +79,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f99b4744e40> >" + " *' at 0x7ff5dc5e2b70> >" ] }, "execution_count": 2, @@ -106,17 +103,15 @@ { "cell_type": "code", "execution_count": 3, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", @@ -130,14 +125,14 @@ "\n", "\n", "2\n", - "\n", - "0\n", - "!a & b\n", + "\n", + "0\n", + "!a & b\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "!a & b\n", "\n", "\n", @@ -166,60 +161,60 @@ "\n", "\n", "5\n", - "\n", - "\n", - "1\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", - "1\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", - "1\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", - "1\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", + "\n", + "\n", "{a}\n", "\n", "\n", @@ -236,45 +231,45 @@ "\n", "\n", "3->5\n", - "\n", - "\n", - "{}\n", + "\n", + "\n", + "{}\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "3->7\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "3->8\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "9\n", - "\n", - "0\n", - "!a & !b\n", + "\n", + "0\n", + "!a & !b\n", "\n", "\n", "3->9\n", - "\n", - "\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", @@ -290,57 +285,57 @@ "\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", "" @@ -370,17 +365,15 @@ { "cell_type": "code", "execution_count": 4, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", @@ -394,14 +387,14 @@ "\n", "\n", "2\n", - "\n", - "0\n", - "!a & b\n", + "\n", + "0\n", + "!a & b\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "!a & b\n", "\n", "\n", @@ -430,21 +423,21 @@ "\n", "\n", "5\n", - "\n", - "\n", - "1\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", + "\n", + "\n", "{a}\n", "\n", "\n", @@ -455,22 +448,22 @@ "\n", "\n", "6\n", - "\n", - "\n", - "1\n", - "!a & b\n", + "\n", + "\n", + "1\n", + "!a & b\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "{a}\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", @@ -480,15 +473,15 @@ "\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", "" @@ -517,17 +510,15 @@ { "cell_type": "code", "execution_count": 5, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", @@ -541,13 +532,13 @@ "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "!a & b\n", "\n", "\n", @@ -574,20 +565,20 @@ "\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", + "\n", + "\n", "{a}\n", "\n", "\n", @@ -598,15 +589,15 @@ "\n", "\n", "3->5\n", - "\n", - "\n", - "{a}\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", @@ -616,9 +607,9 @@ "\n", "\n", "5->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "" @@ -653,7 +644,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.3" + "version": "3.6.4+" } }, "nbformat": 4, diff --git a/tests/python/word.ipynb b/tests/python/word.ipynb index 6d6bc28ee..9a3b06111 100644 --- a/tests/python/word.ipynb +++ b/tests/python/word.ipynb @@ -31,11 +31,15 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "0\n", @@ -145,7 +149,7 @@ "\n" ], "text/plain": [ - " *' at 0x7ff774426a50> >" + " *' at 0x7fbc9033b090> >" ] }, "execution_count": 2, @@ -460,11 +464,13 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "0\n", @@ -519,7 +525,7 @@ "\n" ], "text/plain": [ - " *' at 0x7ff77439aae0> >" + " *' at 0x7fbc902577b0> >" ] }, "execution_count": 13, @@ -548,7 +554,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.4" + "version": "3.6.4+" } }, "nbformat": 4,