dot: make "a" the default
Fixes #319. * spot/twaalgos/dot.cc: Enable "a" by default. * bin/common_aoutput.cc, NEWS: Document it. * doc/org/autfilt.org, doc/org/concepts.org, doc/org/dstar2tgba.org, doc/org/hierarchy.org, doc/org/ltl2tgba.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/satmin.org, doc/org/tut23.org, doc/org/tut24.org, doc/org/tut30.org, doc/org/tut31.org: Adjust or simplify the documentation. * tests/core/det.test, tests/core/dstar.test, tests/core/monitor.test, tests/core/neverclaimread.test, tests/core/readsave.test, tests/core/tgbagraph.test, tests/core/wdba.test, tests/python/_autparserr.ipynb, tests/python/automata-io.ipynb, tests/python/automata.ipynb, tests/python/highlighting.ipynb tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb, tests/python/product.ipynb, tests/python/testingaut.ipynb, tests/python/word.ipynb: Adjust test cases.
This commit is contained in:
Alexandre Duret-Lutz
parent
15fdac6059
commit
2a308182db
31 changed files with 1357 additions and 1429 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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(<font color="#5DA5DA">⓿</font>) | Inf(<font color="#F17CB0">❶</font>)) & (Fin(<font color="#FAA43A">❷</font>) | Inf(<font color="#B276B2">❸</font>))>
|
||||
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<br/><font color="#F17CB0">❶</font><font color="#B276B2">❸</font>>]
|
||||
0 -> 0 [label=<a & b>]
|
||||
0 -> 1 [label=<!a & b>]
|
||||
0 -> 2 [label=<a & !b>]
|
||||
0 -> 3 [label=<!a & !b>]
|
||||
1 [label=<1<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
|
||||
1 -> 0 [label=<a & b>]
|
||||
1 -> 1 [label=<!a & b>]
|
||||
1 -> 2 [label=<a & !b>]
|
||||
1 -> 3 [label=<!a & !b>]
|
||||
2 [label=<2<br/><font color="#F17CB0">❶</font><font color="#FAA43A">❷</font>>]
|
||||
2 -> 0 [label=<a & b>]
|
||||
2 -> 1 [label=<!a & b>]
|
||||
2 -> 2 [label=<a & !b>]
|
||||
2 -> 3 [label=<!a & !b>]
|
||||
3 [label=<3<br/><font color="#5DA5DA">⓿</font><font color="#FAA43A">❷</font>>]
|
||||
3 -> 0 [label=<a & b>]
|
||||
3 -> 1 [label=<!a & b>]
|
||||
3 -> 2 [label=<a & !b>]
|
||||
3 -> 3 [label=<!a & !b>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file gfafgb.svg :var txt=gfafgb :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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(<font color="#5DA5DA">â¿</font>) & Inf(<font color="#F17CB0">â¶</font>)) | (Fin(<font color="#FAA43A">â·</font>) & Inf(<font color="#B276B2">â¸</font>))>
|
||||
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=<a & b<br/><font color="#F17CB0">â¶</font>>]
|
||||
0 -> 0 [label=<!a & !b<br/><font color="#5DA5DA">â¿</font><font color="#FAA43A">â·</font>>]
|
||||
0 -> 0 [label=<a & !b<br/><font color="#F17CB0">â¶</font><font color="#FAA43A">â·</font>>]
|
||||
0 -> 0 [label=<!a & b<br/><font color="#5DA5DA">â¿</font><font color="#B276B2">â¸</font>>]
|
||||
}
|
||||
#+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(<font color="#5DA5DA">â¿</font>) & Inf(<font color="#F17CB0">â¶</font>)) | (Fin(<font color="#FAA43A">â·</font>) & Inf(<font color="#B276B2">â¸</font>))>
|
||||
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<br/><font color="#F17CB0">â¶</font><font color="#FAA43A">â·</font>>]
|
||||
0 -> 0 [label=<b>]
|
||||
0 -> 1 [label=<!b>]
|
||||
1 [label=<1<br/><font color="#5DA5DA">â¿</font><font color="#B276B2">â¸</font>>]
|
||||
1 -> 0 [label=<!a>]
|
||||
1 -> 1 [label=<a>]
|
||||
}
|
||||
#+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=<Inf(<font color="#5DA5DA">⓿</font>)>
|
||||
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=<!b>]
|
||||
0 -> 0 [label=<a & b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
0 -> 1 [label=<!a & b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
1 [label="1"]
|
||||
1 -> 0 [label=<a>]
|
||||
1 -> 1 [label=<!a>]
|
||||
}
|
||||
#+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=<Inf(<font color="#FAA43A">❷</font>) | (Fin(<font color="#F17CB0">❶</font>) & Inf(<font color="#5DA5DA">⓿</font>))>
|
||||
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=<!a>]
|
||||
0 -> 1 [label=<a & !b>]
|
||||
0 -> 2 [label=<a & b>]
|
||||
1 [label=<1>]
|
||||
1 -> 1 [label=<!b>]
|
||||
1 -> 2 [label=<b>]
|
||||
2 [label=<2<br/><font color="#5DA5DA">⓿</font>>]
|
||||
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=<Inf(<font color="#FAA43A">❷</font>) | (Fin(<font color="#F17CB0">❶</font>) & Inf(<font color="#5DA5DA">⓿</font>))>
|
||||
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<br/><font color="#F17CB0">❶</font>>]
|
||||
0 -> 0 [label=<!b>]
|
||||
0 -> 1 [label=<b>]
|
||||
1 [label=<1<br/><font color="#F17CB0">❶</font>>]
|
||||
1 -> 1 [label=<!a>]
|
||||
1 -> 2 [label=<a>]
|
||||
2 [label=<2<br/><font color="#FAA43A">❷</font>>]
|
||||
2 -> 0 [label=<1>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file autfiltsm10.svg :var txt=autfiltsm10 :exports results
|
||||
$txt
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
autfilt --dot <<EOF
|
||||
$txt
|
||||
EOF
|
||||
#+END_SRC
|
||||
|
|
|
|||
|
|
@ -37,7 +37,7 @@ State: 2
|
|||
cat >tut24.hoa <<EOF
|
||||
<<tut24in>>
|
||||
EOF
|
||||
autfilt --dot=.a tut24.hoa
|
||||
autfilt --dot tut24.hoa
|
||||
#+END_SRC
|
||||
|
||||
#+BEGIN_SRC dot :file tut24in.svg :var txt=tut24dot :exports results
|
||||
|
|
|
|||
|
|
@ -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(<font color="#5DA5DA">⓿</font>) & Inf(<font color="#F17CB0">❶</font>)) | (Fin(<font color="#FAA43A">❷</font>) & Inf(<font color="#B276B2">❸</font>)) | (Fin(<font color="#60BD68">❹</font>) & Inf(<font color="#F15854">❺</font>))>
|
||||
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<br/><font color="#FAA43A">❷</font><font color="#F15854">❺</font>>]
|
||||
0 -> 2 [label=<!p1>]
|
||||
0 -> 4 [label=<p1>]
|
||||
1 [label=<1<br/><font color="#FAA43A">❷</font><font color="#F15854">❺</font>>]
|
||||
1 -> 4 [label=<!p1>]
|
||||
1 -> 3 [label=<p1>]
|
||||
2 [label=<2<br/><font color="#B276B2">❸</font><font color="#60BD68">❹</font>>]
|
||||
2 -> 0 [label=<!p1>]
|
||||
2 -> 4 [label=<p1>]
|
||||
3 [label=<3<br/><font color="#B276B2">❸</font><font color="#60BD68">❹</font>>]
|
||||
3 -> 4 [label=<!p1>]
|
||||
3 -> 1 [label=<p1>]
|
||||
4 [label=<4<br/><font color="#F17CB0">❶</font><font color="#FAA43A">❷</font><font color="#60BD68">❹</font>>]
|
||||
4 -> 4 [label=<!p1>]
|
||||
4 -> 4 [label=<p1>]
|
||||
5 [label=<5<br/><font color="#FAA43A">❷</font><font color="#60BD68">❹</font>>]
|
||||
5 -> 2 [label=<!p1>]
|
||||
5 -> 3 [label=<p1>]
|
||||
6 [label=<6<br/><font color="#FAA43A">❷</font><font color="#60BD68">❹</font>>]
|
||||
6 -> 5 [label=<!p1>]
|
||||
6 -> 5 [label=<p1>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file tut30in.svg :var txt=tut30in :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ State: 2
|
|||
cat >tut31.hoa <<EOF
|
||||
<<tut31in>>
|
||||
EOF
|
||||
autfilt --dot=.a tut31.hoa
|
||||
autfilt --dot tut31.hoa
|
||||
#+END_SRC
|
||||
|
||||
#+BEGIN_SRC dot :file tut31in.svg :var txt=tut31dot :exports results
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue