From 838bfb2ae30cbbdee8d6191da993f05da537ff97 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 17 Mar 2015 09:08:20 +0100 Subject: [PATCH] dotty: colored acceptance sets MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This implement several new options for --dot in order to allow emptiness sets to be output as colored ⓿ or ❶... Also add a SPOT_DOTDEFAULT environment variable. * NEWS, src/bin/man/spot-x.x, src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Document the new options. * doc/org/.dir-locals.el, doc/org/init.el.in: Setup SPOT_DOTEXTRA and SPOT_DOTDEFAULT for all documents. * doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, doc/org/ltldo.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/satmin.org: Adjust to this new setup. * src/misc/escape.cc, src/misc/escape.hh (escape_html): New function. * src/tgba/acc.cc, src/tgba/acc.hh (to_text, to_html): New method. * src/tgbaalgos/dotty.cc: Implement the new options. * src/tgbatest/readsave.test, wrap/python/tests/automata.ipynb: More tests. * wrap/python/spot.py: Make sure the default argument for dotty_reachable is None, so that SPOT_DOTDEFAULT is honored. --- NEWS | 8 +- doc/org/.dir-locals.el | 2 + doc/org/autfilt.org | 17 +- doc/org/dstar2tgba.org | 133 +++-- doc/org/init.el.in | 3 + doc/org/ltl2tgba.org | 472 +++++++----------- doc/org/ltldo.org | 5 +- doc/org/oaut.org | 325 ++++++------ doc/org/randaut.org | 249 +++++----- doc/org/satmin.org | 151 ++---- src/bin/common_aoutput.cc | 9 +- src/bin/dstar2tgba.cc | 11 +- src/bin/man/spot-x.x | 9 + src/misc/escape.cc | 25 + src/misc/escape.hh | 7 + src/tgba/acc.cc | 89 +++- src/tgba/acc.hh | 18 + src/tgbaalgos/dotty.cc | 296 +++++++++-- src/tgbatest/readsave.test | 38 +- wrap/python/spot.py | 4 +- wrap/python/tests/automata.ipynb | 822 ++++++++++++++++++------------- 21 files changed, 1500 insertions(+), 1193 deletions(-) diff --git a/NEWS b/NEWS index 7332d71fe..54b2d5922 100644 --- a/NEWS +++ b/NEWS @@ -110,9 +110,11 @@ New in spot 1.99b (not yet released) - GraphViz output now uses an horizontal layout by default. The --dot option of the various command-line tools takes an optional parameter to fine-tune the GraphViz output (including vertical - layout, round states, and named automata). The environment - variable SPOT_DOTEXTRA can also be used to add extra attributes - to the output graph. + layout, round states, named automata, and different ways to + colorize the acceptance sets). The environment + variables SPOT_DOTDEFAULT and SPOT_DOTEXTRA can also be used + to respectively provide a default argument to --dot, and + add extra attributes to the output graph. - Never claims can now be output in the style usd by Spin since version 6.2.4 (i.e., using do..od instead of if..fi, and with diff --git a/doc/org/.dir-locals.el b/doc/org/.dir-locals.el index 27c5a42aa..06b36defe 100644 --- a/doc/org/.dir-locals.el +++ b/doc/org/.dir-locals.el @@ -8,6 +8,8 @@ (setq org-babel-sh-command (concat "PATH=../../src/bin" path-separator "$PATH sh")) + (setenv "SPOT_DOTDEFAULT" "brf(Lato)") + (setenv "SPOT_DOTEXTRA" "node[style=filled, fillcolor=\"#ffffa0\"]") (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (python . t) diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index c7a712cf0..80a2704e3 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -27,7 +27,7 @@ same stream, =autfilt= will process them in batch. The output format can be controlled using [[file:oaut.org][the common output options]] (like =--spin=, =--lbtt=, =--dot=, =--hoaf=...). -#+BEGIN_SRC sh :results verbatim :exports both +#+BEGIN_SRC sh :results verbatim :exports code cat >example.hoa < 1 -: 1 [label="0"] -: 1 -> 1 [label="p0\n{0}"] -: 1 -> 1 [label="!p0"] +: rankdir=LR +: I [label="", style=invis, width=0] +: I -> 0 +: 0 [label="0"] +: 0 -> 0 [label="p0\n{0}"] +: 0 -> 0 [label="!p0"] : } The =--spin= options implicitly requires a degeneralization: diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index 57ed9887b..45c234bc7 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -68,48 +68,58 @@ a Monitor, using the same options as [[file:ltl2tgba.org][=ltl2tgba=]]. For instance here is the conversion to a Büchi automaton (=-B=) in [[http://http://www.graphviz.org/][GraphViz]]'s format: -#+BEGIN_SRC sh :results verbatim :exports both +#+BEGIN_SRC sh :results verbatim :exports code dstar2tgba -B fagfb #+END_SRC + +#+BEGIN_SRC sh :results verbatim :exports results +SPOT_DOTEXTRA= dstar2tgba -B fagfb --dot= +#+END_SRC #+RESULTS: #+begin_example digraph G { rankdir=LR I [label="", style=invis, width=0] - I -> 0 - 0 [label="0"] - 0 -> 0 [label="!a"] - 0 -> 1 [label="a"] - 1 [label="1", peripheries=2] - 1 -> 1 [label="b"] - 1 -> 2 [label="!b"] + I -> 1 + 0 [label="0", peripheries=2] + 0 -> 0 [label="b"] + 0 -> 2 [label="!b"] + 1 [label="1"] + 1 -> 0 [label="a"] + 1 -> 1 [label="!a"] 2 [label="2"] - 2 -> 1 [label="b"] + 2 -> 0 [label="b"] 2 -> 2 [label="!b"] } #+end_example -Which can be rendered as: +Which can be rendered as (note that in this documentation +we use some [[file:aout.org][environement variables]] to produce a more colorful +output by default): #+NAME: fagfb2ba -#+BEGIN_SRC sh :results verbatim :exports none -dstar2tgba -B fagfb | sed 's/\\/\\\\/' +#+BEGIN_SRC sh :results verbatim :exports code +dstar2tgba -B fagfb #+END_SRC #+RESULTS: fagfb2ba #+begin_example digraph G { rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] - I -> 0 - 0 [label="0"] - 0 -> 0 [label="!a"] - 0 -> 1 [label="a"] - 1 [label="1", peripheries=2] - 1 -> 1 [label="b"] - 1 -> 2 [label="!b"] + I -> 1 + 0 [label="0", peripheries=2] + 0 -> 0 [label=] + 0 -> 2 [label=] + 1 [label="1"] + 1 -> 0 [label=] + 1 -> 1 [label=] 2 [label="2"] - 2 -> 1 [label="b"] - 2 -> 2 [label="!b"] + 2 -> 0 [label=] + 2 -> 2 [label=] } #+end_example @@ -153,7 +163,7 @@ T0_S3: Here is the translation of =GFa & GFb= to a 4-state Streett automaton: #+BEGIN_SRC sh :results verbatim :exports both -ltlfilt -f 'GFa & GFb' -l | ltl2dstar --automata=streett --ltl2nba=spin:../../src/bin/ltl2tgba@-sD - gfagfb +ltlfilt -f 'GFa & GFb' -l | ltl2dstar --automata=streett --ltl2nba=spin:ltl2tgba@-Ds - gfagfb cat gfagfb #+END_SRC #+RESULTS: @@ -195,42 +205,27 @@ And now its conversion by =dstar2tgba= to a 2-state Büchi automaton. We don't pass any option to =dstar2tgba= because converting to TGBA in GraphViz's format is the default: +#+NAME: gfagfb2ba #+BEGIN_SRC sh :results verbatim :exports code dstar2tgba gfagfb #+END_SRC -#+RESULTS: -#+begin_example -digraph G { - rankdir=LR - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0"] - 0 -> 1 [label="1"] - 1 [label="1"] - 1 -> 1 [label="!a & !b"] - 1 -> 1 [label="a & !b\n{0}"] - 1 -> 1 [label="!a & b\n{1}"] - 1 -> 1 [label="a & b\n{0,1}"] -} -#+end_example - -#+NAME: gfagfb2ba -#+BEGIN_SRC sh :results verbatim :exports none -dstar2tgba gfagfb | sed 's/\\/\\\\/g' -#+END_SRC #+RESULTS: gfagfb2ba #+begin_example digraph G { rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] I -> 0 0 [label="0"] - 0 -> 1 [label="1"] + 0 -> 1 [label=<1>] 1 [label="1"] - 1 -> 1 [label="!a & !b"] - 1 -> 1 [label="a & !b\\n{0}"] - 1 -> 1 [label="!a & b\\n{1}"] - 1 -> 1 [label="a & b\\n{0,1}"] + 1 -> 1 [label=] + 1 -> 1 [label=⓿>] + 1 -> 1 [label=❶>] + 1 -> 1 [label=⓿❶>] } #+end_example @@ -355,33 +350,33 @@ head -n 10 | while read f; do echo "$f" ltlfilt -l -f "$f" | - ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-sD - - | + ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - | dstar2tgba -B --stats=' DRA: %Sst.; BA: %sst.; det.? %d; complete? %p' done #+END_SRC #+RESULTS: #+begin_example -c U (c & (a | b | (Xc U (a & Xc)))) - DRA: 3st.; BA: 2st.; det.? 1; complete? 0 -!b | F!c - DRA: 3st.; BA: 3st.; det.? 1; complete? 1 -(!a R F!b) R !b - DRA: 6st.; BA: 5st.; det.? 1; complete? 0 -b U !c - DRA: 3st.; BA: 2st.; det.? 1; complete? 0 +(b | Fa) R Fc + DRA: 9st.; BA: 6st.; det.? 1; complete? 1 +Ga U (Gc R (!a | Gc)) + DRA: 7st.; BA: 7st.; det.? 0; complete? 0 GFc DRA: 3st.; BA: 3st.; det.? 1; complete? 1 -(F!c U a) R !a - DRA: 6st.; BA: 5st.; det.? 1; complete? 0 -b | G!b - DRA: 4st.; BA: 3st.; det.? 1; complete? 0 -!a R (!c & (!a | (F!b U (!a & F!b)))) - DRA: 5st.; BA: 4st.; det.? 1; complete? 0 -F(a & !b & G!c) - DRA: 2st.; BA: 3st.; det.? 0; complete? 0 -GF!c - DRA: 3st.; BA: 3st.; det.? 1; complete? 1 +!a | (a R b) + DRA: 3st.; BA: 2st.; det.? 1; complete? 0 +Xc R (G!c R (b | G!c)) + DRA: 4st.; BA: 2st.; det.? 1; complete? 0 +c & G(b | F(a & c)) + DRA: 5st.; BA: 3st.; det.? 1; complete? 0 +XXFc + DRA: 4st.; BA: 4st.; det.? 1; complete? 1 +XFc | Gb + DRA: 5st.; BA: 4st.; det.? 1; complete? 1 +G(((!a & Gc) | (a & F!c)) U (!a | Ga)) + DRA: 6st.; BA: 5st.; det.? 1; complete? 1 +a & !b + DRA: 3st.; BA: 2st.; det.? 1; complete? 0 #+end_example An important point you should be aware of when comparing these numbers @@ -426,6 +421,6 @@ states and $n$ acceptance pairs. Our translation to TGBA limits this to $|Q|\cdot(2^n+1)$ states. Sometimes, as in the [[#streett_to_tgba_example][example for =GFa & GFb=]] the output of this -conversion will happen to be deterministic. Let's say that this is -luck: Spot does not implement any algorithm to preserve the -determinism of Streett automata. +conversion happens to be deterministic. This is pure luck: Spot does +not implement any algorithm to preserve the determinism of Streett +automata. diff --git a/doc/org/init.el.in b/doc/org/init.el.in index 560ba0482..e0b1a7a6a 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -24,6 +24,9 @@ (setq org-babel-sh-command (concat "PATH=@abs_top_builddir@/src/bin" path-separator "$PATH sh")) +(setenv "SPOT_DOTDEFAULT" "brf(Lato)") +(setenv "SPOT_DOTEXTRA" "node[style=filled, fillcolor=\"#ffffa0\"]") + (setq org-export-html-home/up-format "
UP | HOME diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index afff7fddb..c03ca5fbf 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -14,9 +14,12 @@ option. Formulas to translate may be specified using [[file:ioltl.org][common input options for LTL/PSL formulas]]. -#+BEGIN_SRC sh :results verbatim :exports both +#+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -f 'Fa & GFb' #+END_SRC +#+BEGIN_SRC sh :results verbatim :exports results +SPOT_DOTEXTRA= ltl2tgba -f 'Fa & GFb' --dot= +#+END_SRC #+RESULTS: #+begin_example digraph G { @@ -47,23 +50,29 @@ ltl2tgba "Fa & GFb" | dot -Tpdf > tgba.pdf #+END_SRC #+RESULTS: -The result would look like this: +The result would look like this (note that in this documentation +we use some [[file:aout.org][environement variables]] to produce a more colorful +output by default) #+NAME: dotex #+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba "Fa & GFb" | sed 's/\\/\\\\/' +ltl2tgba "Fa & GFb" #+END_SRC #+RESULTS: dotex #+begin_example digraph G { rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] I -> 1 0 [label="0"] - 0 -> 0 [label="b\\n{0}"] - 0 -> 0 [label="!b"] + 0 -> 0 [label=⓿>] + 0 -> 0 [label=] 1 [label="1"] - 1 -> 0 [label="a"] - 1 -> 1 [label="!a"] + 1 -> 0 [label=] + 1 -> 1 [label=] } #+end_example @@ -74,53 +83,39 @@ $txt #+RESULTS: [[file:dotex.png]] -The string between braces, ={0}=, represents the sets of acceptance -sets a transition belongs to. In this case, there is only one -acceptance set, called =0=, containing a single transition. You may -have many transitions in the same acceptance set, and a transition may -also belong to multiple acceptance sets. An infinite path through -this automaton is accepting iff it visit each acceptance set -infinitely often. Therefore, in the above example, any accepted path -will /necessarily/ leave the initial state after a finite amount of -steps, and then it will verify the property =b= infinitely often. It -is also possible that an automaton do not use any acceptance set at -all, in which any run is accepting. +Characters like ⓿, ❶, etc. denotes the acceptance sets a transition +belongs to. In this case, there is only one acceptance set, called +=0=, containing a single transition. You may have many transitions in +the same acceptance set, and a transition may also belong to multiple +acceptance sets. An infinite path through this automaton is accepting +iff it visit each acceptance set infinitely often. Therefore, in the +above example, any accepted path will /necessarily/ leave the initial +state after a finite amount of steps, and then it will verify the +property =b= infinitely often. It is also possible that an automaton +do not use any acceptance set at all, in which any run is accepting. Here is a TGBA with multiple acceptance sets (we omit the call to =dot= to render the output of =ltl2tgba= from now on): -#+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba 'GFa & GFb' -#+END_SRC -#+RESULTS: -#+begin_example -digraph G { - rankdir=LR - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0"] - 0 -> 0 [label="a & b\n{0,1}"] - 0 -> 0 [label="!a & !b"] - 0 -> 0 [label="!a & b\n{1}"] - 0 -> 0 [label="a & !b\n{0}"] -} -#+end_example - #+NAME: dotex2 -#+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba "GFa & GFb" | sed 's/\\/\\\\/' +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba "GFa & GFb" #+END_SRC #+RESULTS: dotex2 #+begin_example digraph G { rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] I -> 0 0 [label="0"] - 0 -> 0 [label="a & b\\n{0,1}"] - 0 -> 0 [label="!a & !b"] - 0 -> 0 [label="!a & b\\n{1}"] - 0 -> 0 [label="a & !b\\n{0}"] + 0 -> 0 [label=⓿❶>] + 0 -> 0 [label=] + 0 -> 0 [label=❶>] + 0 -> 0 [label=⓿>] } #+end_example @@ -130,57 +125,38 @@ $txt #+RESULTS: [[file:dotex2.png]] -The above TGBA has two acceptance sets: =0= and =1=. The position of +The above TGBA has two acceptance sets: ⓿ and ❶. The position of these acceptance sets ensures that atomic propositions =a= and =b= must be true infinitely often. A Büchi automaton for the previous formula can be obtained with the =-B= option: +#+NAME: dotex2ba #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -B 'GFa & GFb' #+END_SRC -#+RESULTS: -#+begin_example -digraph G { - rankdir=LR - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0", peripheries=2] - 0 -> 0 [label="a & b"] - 0 -> 1 [label="!b"] - 0 -> 2 [label="!a & b"] - 1 [label="1"] - 1 -> 0 [label="a & b"] - 1 -> 1 [label="!b"] - 1 -> 2 [label="!a & b"] - 2 [label="2"] - 2 -> 0 [label="a"] - 2 -> 2 [label="!a"] -} -#+end_example - -#+NAME: dotex2ba -#+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba -B 'GFa & GFb' | sed 's/\\/\\\\/' -#+END_SRC #+RESULTS: dotex2ba #+begin_example digraph G { rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] I -> 0 0 [label="0", peripheries=2] - 0 -> 0 [label="a & b"] - 0 -> 1 [label="!b"] - 0 -> 2 [label="!a & b"] + 0 -> 0 [label=] + 0 -> 1 [label=] + 0 -> 2 [label=] 1 [label="1"] - 1 -> 0 [label="a & b"] - 1 -> 1 [label="!b"] - 1 -> 2 [label="!a & b"] + 1 -> 0 [label=] + 1 -> 1 [label=] + 1 -> 2 [label=] 2 [label="2"] - 2 -> 0 [label="a"] - 2 -> 2 [label="!a"] + 2 -> 0 [label=] + 2 -> 2 [label=] } #+end_example @@ -201,48 +177,33 @@ is done internally): #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba --dot=t -B 'GFa & GFb' #+END_SRC -#+RESULTS: -#+begin_example -digraph G { - rankdir=LR - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0"] - 0 -> 0 [label="a & b\n{0}"] - 0 -> 1 [label="!b\n{0}"] - 0 -> 2 [label="!a & b\n{0}"] - 1 [label="1"] - 1 -> 0 [label="a & b"] - 1 -> 1 [label="!b"] - 1 -> 2 [label="!a & b"] - 2 [label="2"] - 2 -> 0 [label="a"] - 2 -> 2 [label="!a"] -} -#+end_example #+NAME: dotex2ba-t #+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba --dot=t -B 'GFa & GFb' | sed 's/\\/\\\\/' +ltl2tgba --dot=.t -B 'GFa & GFb' #+END_SRC #+RESULTS: dotex2ba-t #+begin_example digraph G { rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] I -> 0 0 [label="0"] - 0 -> 0 [label="a & b\\n{0}"] - 0 -> 1 [label="!b\\n{0}"] - 0 -> 2 [label="!a & b\\n{0}"] + 0 -> 0 [label=⓿>] + 0 -> 1 [label=⓿>] + 0 -> 2 [label=⓿>] 1 [label="1"] - 1 -> 0 [label="a & b"] - 1 -> 1 [label="!b"] - 1 -> 2 [label="!a & b"] + 1 -> 0 [label=] + 1 -> 1 [label=] + 1 -> 2 [label=] 2 [label="2"] - 2 -> 0 [label="a"] - 2 -> 2 [label="!a"] + 2 -> 0 [label=] + 2 -> 2 [label=] } #+end_example @@ -262,18 +223,28 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' #+begin_example -8, --utf8 enable UTF-8 characters in output (ignored with --lbtt or --spin) - --dot[=c|h|n|N|s|t|v] GraphViz's format (default). Add letters to chose - (c) circular nodes, (h) horizontal layout, (v) - vertical layout, (n) with name, (N) without name, - (s) with SCCs, (t) always transition-based + --dot[=a|b|c|f(FONT)|h|n|N|r|R|s|t|v] + GraphViz's format (default). Add letters for (a) + acceptance display, (b) acceptance sets as + bullets,(c) circular nodes, (f(FONT)) use FONT, + (h) horizontal layout, (v) vertical layout, (n) + with name, (N) without name, (r) rainbow colors + for acceptance set, (R) color acceptance set by + Inf/Fin, (s) with SCCs, (t) force transition-based acceptance. - -H, --hoaf[=s|t|m|l] Output the automaton in HOA format. Add letters - to select (s) state-based acceptance, (t) - transition-based acceptance, (m) mixed acceptance, - (l) single-line output + -H, --hoaf[=i|s|t|m|l] Output the automaton in HOA format. Add letters + to select (i) use implicit labels for complete + deterministic automata, (s) prefer state-based + acceptance when possible [default], (t) force + transition-based acceptance, (m) mix state and + transition-based acceptance, (l) single-line + output --lbtt[=t] LBTT's format (add =t to force transition-based acceptance even on Büchi automata) --name=FORMAT set the name of the output automaton + -o, --output=FORMAT send output to a file named FORMAT instead of + standard output. The first automaton sent to a + file truncates it unless FORMAT starts with '>>'. -q, --quiet suppress all normal output -s, --spin[=6|c] Spin neverclaim (implies --ba). Add letters to select (6) Spin's 6.2.4 style, (c) comments on @@ -284,50 +255,31 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' Option =-8= can be used to improve the readability of the output if your system can display UTF-8 correctly. -#+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -B8 'GFa & GFb' -#+END_SRC -#+RESULTS: -#+begin_example -digraph G { - rankdir=LR - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0", peripheries=2] - 0 -> 0 [label="a∧b"] - 0 -> 1 [label="b̅"] - 0 -> 2 [label="a̅∧b"] - 1 [label="1"] - 1 -> 0 [label="a∧b"] - 1 -> 1 [label="b̅"] - 1 -> 2 [label="a̅∧b"] - 2 [label="2"] - 2 -> 0 [label="a"] - 2 -> 2 [label="a̅"] -} -#+end_example - #+NAME: dotex2ba8 -#+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba -B8 "GFa & GFb" | sed 's/\\/\\\\/' +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba -B8 "GFa & GFb" #+END_SRC #+RESULTS: dotex2ba8 #+begin_example digraph G { rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] I -> 0 0 [label="0", peripheries=2] - 0 -> 0 [label="a∧b"] - 0 -> 1 [label="b̅"] - 0 -> 2 [label="a̅∧b"] + 0 -> 0 [label=] + 0 -> 1 [label=] + 0 -> 2 [label=] 1 [label="1"] - 1 -> 0 [label="a∧b"] - 1 -> 1 [label="b̅"] - 1 -> 2 [label="a̅∧b"] + 1 -> 0 [label=] + 1 -> 1 [label=] + 1 -> 2 [label=] 2 [label="2"] - 2 -> 0 [label="a"] - 2 -> 2 [label="a̅"] + 2 -> 0 [label=] + 2 -> 2 [label=] } #+end_example @@ -423,48 +375,30 @@ automaton. An example formula where the difference between =-D= and =--small= is flagrant is =Ga|Gb|Gc=: -#+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba 'Ga|Gb|Gc' -#+END_SRC -#+RESULTS: -#+begin_example -digraph G { - rankdir=LR - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0", peripheries=2] - 0 -> 1 [label="a"] - 0 -> 2 [label="b"] - 0 -> 3 [label="c"] - 1 [label="1", peripheries=2] - 1 -> 1 [label="a"] - 2 [label="2", peripheries=2] - 2 -> 2 [label="b"] - 3 [label="3", peripheries=2] - 3 -> 3 [label="c"] -} -#+end_example - #+NAME: gagbgc1 -#+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba "Ga|Gb|Gc" | sed 's/\\/\\\\/' +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba "Ga|Gb|Gc" #+END_SRC #+RESULTS: gagbgc1 #+begin_example digraph G { rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] I -> 0 - 0 [label="0", peripheries=2] - 0 -> 1 [label="a"] - 0 -> 2 [label="b"] - 0 -> 3 [label="c"] - 1 [label="1", peripheries=2] - 1 -> 1 [label="a"] - 2 [label="2", peripheries=2] - 2 -> 2 [label="b"] - 3 [label="3", peripheries=2] - 3 -> 3 [label="c"] + 0 [label="0"] + 0 -> 1 [label=] + 0 -> 2 [label=] + 0 -> 3 [label=] + 1 [label="1"] + 1 -> 1 [label=] + 2 [label="2"] + 2 -> 2 [label=] + 3 [label="3"] + 3 -> 3 [label=] } #+end_example @@ -474,80 +408,46 @@ $txt #+RESULTS: [[file:gagbgc1.png]] +#+NAME: gagbgc2 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -D 'Ga|Gb|Gc' #+END_SRC -#+RESULTS: -#+begin_example -digraph G { - rankdir=LR - I [label="", style=invis, width=0] - I -> 6 - 0 [label="0", peripheries=2] - 0 -> 0 [label="c"] - 1 [label="1", peripheries=2] - 1 -> 0 [label="!b & c"] - 1 -> 1 [label="b & c"] - 1 -> 2 [label="b & !c"] - 2 [label="2", peripheries=2] - 2 -> 2 [label="b"] - 3 [label="3", peripheries=2] - 3 -> 2 [label="!a & b"] - 3 -> 3 [label="a & b"] - 3 -> 5 [label="a & !b"] - 4 [label="4", peripheries=2] - 4 -> 0 [label="!a & c"] - 4 -> 4 [label="a & c"] - 4 -> 5 [label="a & !c"] - 5 [label="5", peripheries=2] - 5 -> 5 [label="a"] - 6 [label="6", peripheries=2] - 6 -> 0 [label="!a & !b & c"] - 6 -> 1 [label="!a & b & c"] - 6 -> 2 [label="!a & b & !c"] - 6 -> 3 [label="a & b & !c"] - 6 -> 4 [label="a & !b & c"] - 6 -> 5 [label="a & !b & !c"] - 6 -> 6 [label="a & b & c"] -} -#+end_example - -#+NAME: gagbgc2 -#+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba -D 'Ga|Gb|Gc' | sed 's/\\/\\\\/' -#+END_SRC #+RESULTS: gagbgc2 #+begin_example digraph G { rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] I -> 6 0 [label="0", peripheries=2] - 0 -> 0 [label="c"] + 0 -> 0 [label=] 1 [label="1", peripheries=2] - 1 -> 0 [label="!b & c"] - 1 -> 1 [label="b & c"] - 1 -> 2 [label="b & !c"] + 1 -> 0 [label=] + 1 -> 1 [label=] + 1 -> 2 [label=] 2 [label="2", peripheries=2] - 2 -> 2 [label="b"] + 2 -> 2 [label=] 3 [label="3", peripheries=2] - 3 -> 2 [label="!a & b"] - 3 -> 3 [label="a & b"] - 3 -> 5 [label="a & !b"] + 3 -> 2 [label=] + 3 -> 3 [label=] + 3 -> 5 [label=] 4 [label="4", peripheries=2] - 4 -> 0 [label="!a & c"] - 4 -> 4 [label="a & c"] - 4 -> 5 [label="a & !c"] + 4 -> 0 [label=] + 4 -> 4 [label=] + 4 -> 5 [label=] 5 [label="5", peripheries=2] - 5 -> 5 [label="a"] + 5 -> 5 [label=] 6 [label="6", peripheries=2] - 6 -> 0 [label="!a & !b & c"] - 6 -> 1 [label="!a & b & c"] - 6 -> 2 [label="!a & b & !c"] - 6 -> 3 [label="a & b & !c"] - 6 -> 4 [label="a & !b & c"] - 6 -> 5 [label="a & !b & !c"] - 6 -> 6 [label="a & b & c"] + 6 -> 0 [label=] + 6 -> 1 [label=] + 6 -> 2 [label=] + 6 -> 3 [label=] + 6 -> 4 [label=] + 6 -> 5 [label=] + 6 -> 6 [label=] } #+end_example @@ -701,47 +601,30 @@ compatible outgoing transition exist. -MD= (short for =--monitor --deterministic=) will output the minimal deterministic monitor for the given formula. +#+NAME: monitor1 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -M '(Xa & Fb) | Gc' #+END_SRC -#+RESULTS: -#+begin_example -digraph G { - rankdir=LR - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0", peripheries=2] - 0 -> 1 [label="1"] - 0 -> 3 [label="c"] - 1 [label="1", peripheries=2] - 1 -> 2 [label="a"] - 2 [label="2", peripheries=2] - 2 -> 2 [label="1"] - 3 [label="3", peripheries=2] - 3 -> 3 [label="c"] -} -#+end_example - -#+NAME: monitor1 -#+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba -M '(Xa & Fb) | Gc' | sed 's/\\/\\\\/' -#+END_SRC #+RESULTS: monitor1 #+begin_example digraph G { rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] I -> 0 - 0 [label="0", peripheries=2] - 0 -> 1 [label="1"] - 0 -> 3 [label="c"] - 1 [label="1", peripheries=2] - 1 -> 2 [label="a"] - 2 [label="2", peripheries=2] - 2 -> 2 [label="1"] - 3 [label="3", peripheries=2] - 3 -> 3 [label="c"] + 0 [label="0"] + 0 -> 1 [label=<1>] + 0 -> 3 [label=] + 1 [label="1"] + 1 -> 2 [label=] + 2 [label="2"] + 2 -> 2 [label=<1>] + 3 [label="3"] + 3 -> 3 [label=] } #+end_example @@ -752,53 +635,33 @@ $txt #+RESULTS: [[file:monitor1.png]] +#+NAME: monitor2 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -MD '(Xa & Fb) | Gc' #+END_SRC -#+RESULTS: -#+begin_example -digraph G { - rankdir=LR - I [label="", style=invis, width=0] - I -> 3 - 0 [label="0", peripheries=2] - 0 -> 0 [label="1"] - 1 [label="1", peripheries=2] - 1 -> 0 [label="a"] - 2 [label="2", peripheries=2] - 2 -> 2 [label="c"] - 3 [label="3", peripheries=2] - 3 -> 1 [label="!c"] - 3 -> 4 [label="c"] - 4 [label="4", peripheries=2] - 4 -> 0 [label="a"] - 4 -> 2 [label="!a & c"] -} -#+end_example - -#+NAME: monitor2 -#+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba -MD '(Xa & Fb) | Gc' | sed 's/\\/\\\\/' -#+END_SRC #+RESULTS: monitor2 #+begin_example digraph G { rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] I -> 3 - 0 [label="0", peripheries=2] - 0 -> 0 [label="1"] - 1 [label="1", peripheries=2] - 1 -> 0 [label="a"] - 2 [label="2", peripheries=2] - 2 -> 2 [label="c"] - 3 [label="3", peripheries=2] - 3 -> 1 [label="!c"] - 3 -> 4 [label="c"] - 4 [label="4", peripheries=2] - 4 -> 0 [label="a"] - 4 -> 2 [label="!a & c"] + 0 [label="0"] + 0 -> 0 [label=<1>] + 1 [label="1"] + 1 -> 0 [label=] + 2 [label="2"] + 2 -> 2 [label=] + 3 [label="3"] + 3 -> 1 [label=] + 3 -> 4 [label=] + 4 [label="4"] + 4 -> 0 [label=] + 4 -> 2 [label=] } #+end_example @@ -811,7 +674,8 @@ $txt Because they accept all finite executions that could be extended to match the formula, monitor cannot be used to check for eventualities -such as =F(a)=. Any finite execution can be extended to match =F(a)=. +such as =F(a)=: indeed, any finite execution can be extended to match +=F(a)=. # LocalWords: ltl tgba num toc PSL Büchi automata SRC GFb invis Acc # LocalWords: ltlfilt filenames GraphViz vectorial pdf Tpdf dotex diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index dc5d6c428..1b69dff19 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -312,13 +312,16 @@ the following words, then the string on the right is appended. So for instance you can type just -#+BEGIN_SRC sh :results verbatim :exports both +#+BEGIN_SRC sh :results verbatim :exports code ltldo ltl2ba -f a #+END_SRC to obtain a Dot output (this is the default output format for =ltldo=) for the neverclaim produced by =ltl2ba -f a=. +#+BEGIN_SRC sh :results verbatim :exports result +SPOT_DOTEXTRA= ltldo ltl2ba -f a --dot= +#+END_SRC #+RESULTS: : digraph G { : rankdir=LR diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 6f8b3ce75..024ffdbec 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -1,4 +1,4 @@ -# -*- coding: utf-8 -*- +y# -*- coding: utf-8 -*- #+TITLE: Common output options for automata #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html @@ -18,16 +18,22 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' #+begin_example -8, --utf8 enable UTF-8 characters in output (ignored with --lbtt or --spin) - --dot[=c|h|n|N|s|t|v] GraphViz's format (default). Add letters for (a) - acceptance display, (c) circular nodes, (h) - horizontal layout, (v) vertical layout, (n) with - name, (N) without name, (s) with SCCs, (t) force - transition-based acceptance. - -H, --hoaf[=s|t|m|l] Output the automaton in HOA format. Add letters - to select (s) prefer state-based acceptance when - possible [default], (t) force transition-based - acceptance, (m) mix state and transition-based - acceptance, (l) single-line output + --dot[=a|b|c|f(FONT)|h|n|N|r|R|s|t|v] + GraphViz's format (default). Add letters for (a) + acceptance display, (b) acceptance sets as + bullets,(c) circular nodes, (f(FONT)) use FONT, + (h) horizontal layout, (v) vertical layout, (n) + with name, (N) without name, (r) rainbow colors + for acceptance set, (R) color acceptance set by + Inf/Fin, (s) with SCCs, (t) force transition-based + acceptance. + -H, --hoaf[=i|s|t|m|l] Output the automaton in HOA format. Add letters + to select (i) use implicit labels for complete + deterministic automata, (s) prefer state-based + acceptance when possible [default], (t) force + transition-based acceptance, (m) mix state and + transition-based acceptance, (l) single-line + output --lbtt[=t] LBTT's format (add =t to force transition-based acceptance even on Büchi automata) --name=FORMAT set the name of the output automaton @@ -118,148 +124,161 @@ represent. Here is a picture of these two automata: #+NAME: hoafex #+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba --dot=cn '(Ga -> Gb) W c' 'a U b' | dot | gvpack | +ltl2tgba --dot=.cn '(Ga -> Gb) W c' 'a U b' | dot | gvpack | perl -pe 's/\\\n//g;s/\\/\\\\/g;s/graph G/graph cluster/g' #+END_SRC #+RESULTS: hoafex #+begin_example digraph root { - graph [bb="0,0,425,231.06", + graph [bb="0,0,427,231.07", + fontname=Lato, labelloc=t, lheight=0.21, rankdir=LR ]; - node [label="\\N", - shape=circle + node [fillcolor="#ffffa0", + fontname=Lato, + label="\\N", + shape=circle, + style=filled ]; + edge [fontname=Lato]; subgraph cluster { graph [bb="", - label="(Gb | F!a) W c", + fontname=Lato, + label=<(Gb | F!a) W c>, labelloc=t, lheight=0.21, - lp="196.5,196.66", - lwidth=1.14, + lp="197.5,196.66", + lwidth=1.19, rankdir=LR ]; - node [height="", + node [fillcolor="#ffffa0", + fontname=Lato, + height="", label="\\N", pos="", shape=circle, - style="", + style=filled, width="" ]; - edge [label="", + edge [fontname=Lato, + label="", lp="", pos="" ]; I [height=0.013889, label="", - pos="1,49.162", + pos="1,49.168", style=invis, width=0.013889]; 1 [height=0.5, label=1, - pos="56,49.162", + pos="56,49.168", width=0.5]; I -> 1 [pos="e,37.942,49.324 1.1549,49.324 2.6725,49.324 15.097,49.324 27.628,49.324"]; - 1 -> 1 [label="!a & !c\\n{0}", + 1 -> 1 [label=⓿>, lp="56,100.32", - pos="e,62.379,66.361 49.621,66.361 48.319,76.181 50.445,85.324 56,85.324 59.472,85.324 61.604,81.752 62.398,76.677"]; + pos="e,62.379,66.362 49.621,66.362 48.319,76.182 50.445,85.324 56,85.324 59.472,85.324 61.604,81.753 62.398,76.677"]; 0 [height=0.5, label=0, - pos="189,121.16", + pos="190,121.17", width=0.5]; - 1 -> 0 [label="a & b & !c", - lp="122.5,113.82", - pos="e,171.82,115.02 70.135,60.558 76.501,65.71 84.4,71.688 92,76.324 114.85,90.263 142.72,102.89 162.53,111.19"]; + 1 -> 0 [label=, + lp="123,113.83", + pos="e,172.99,115.19 70.127,60.572 76.491,65.727 84.391,71.704 92,76.324 115.21,90.42 143.57,103.1 163.61,111.38"]; 2 [height=0.5, label=2, - pos="189,34.162", + pos="190,34.168", width=0.5]; - 1 -> 2 [label="a & !c", - lp="122.5,64.823", - pos="e,174.09,44.491 73.626,53.241 93.026,57.118 125.9,61.52 153,54.324 157.19,53.213 161.39,51.47 165.37,49.466"]; + 1 -> 2 [label=, + lp="123,64.824", + pos="e,175.09,44.492 73.8,53.268 93.402,57.17 126.62,61.596 154,54.324 158.19,53.213 162.39,51.47 166.37,49.467"]; 3 [height=0.5, label=3, - pos="375,34.162", + pos="377,34.168", width=0.5]; - 1 -> 3 [label=c, - lp="240.5,9.8235", - pos="e,359.03,25.984 66.028,34.328 72.163,25.634 81.128,15.425 92,10.324 114,0 275.42,0.3271 310,7.3235 323.76,10.107 338.24,15.942 349.94,21.478"]; - 0 -> 0 [label="b\\n{0}", - lp="189,172.32", - pos="e,197.63,137.24 180.37,137.24 178.11,147.47 180.99,157.32 189,157.32 194.26,157.32 197.3,153.08 198.14,147.27"]; - 2 -> 1 [label="!a & !c\\n{0}", - lp="122.5,35.324", - pos="e,68.596,36.184 172.36,26.591 166.44,24.064 159.55,21.586 153,20.324 126.38,15.197 117.5,11.13 92,20.324 86.432,22.331 81.123,25.651 76.398,29.343"]; - 2 -> 2 [label="a & !c", - lp="189,77.824", - pos="e,197.63,50.24 180.37,50.24 178.11,60.474 180.99,70.324 189,70.324 194.26,70.324 197.3,66.082 198.14,60.273"]; - 2 -> 3 [label="!a & c", - lp="292,105.82", - pos="e,363.94,48.712 202.25,46.94 217.46,61.618 244.99,85.026 274,94.324 289.24,99.207 295.12,100.21 310,94.324 329.12,86.764 345.87,70.495 357.43,56.803"]; + 1 -> 3 [label=, + lp="242,9.8246", + pos="e,361.03,25.984 66.027,34.327 72.161,25.632 81.127,15.423 92,10.325 114.02,0 277.48,0.3418 312,7.3246 325.76,10.108 340.24,15.943 351.94,21.478"]; + 0 -> 0 [label=⓿>, + lp="190,172.33", + pos="e,198.98,137.24 181.02,137.24 178.68,147.48 181.67,157.33 190,157.33 195.47,157.33 198.63,153.08 199.5,147.28"]; + 2 -> 1 [label=⓿>, + lp="123,35.324", + pos="e,68.596,36.186 173.36,26.591 167.44,24.066 160.55,21.587 154,20.324 126.94,15.113 117.92,10.98 92,20.324 86.432,22.331 81.123,25.651 76.398,29.343"]; + 2 -> 2 [label=, + lp="190,77.824", + pos="e,198.98,50.24 181.02,50.24 178.68,60.475 181.67,70.324 190,70.324 195.47,70.324 198.63,66.083 199.5,60.274"]; + 2 -> 3 [label=, + lp="294,105.83", + pos="e,365.94,48.712 203.15,46.686 218.52,61.348 246.56,84.98 276,94.324 291.25,99.165 297.12,100.21 312,94.324 331.12,86.764 347.87,70.495 359.43,56.803"]; 4 [height=0.5, label=4, - pos="292,34.162", + pos="294,34.168", width=0.5]; - 2 -> 4 [label="a & c", - lp="240.5,41.824", - pos="e,273.78,34.324 207.13,34.324 222.59,34.324 245.58,34.324 263.59,34.324"]; - 3 -> 3 [label="1\\n{0}", - lp="375,85.324", - pos="e,382.03,50.988 367.97,50.988 366.41,60.949 368.75,70.324 375,70.324 379,70.324 381.4,66.475 382.2,61.092"]; - 4 -> 3 [label="!a", - lp="333.5,41.824", - pos="e,356.85,34.324 310.18,34.324 320.81,34.324 334.69,34.324 346.8,34.324"]; - 4 -> 4 [label=a, - lp="292,77.824", - pos="e,299.03,50.988 284.97,50.988 283.41,60.949 285.75,70.324 292,70.324 296,70.324 298.4,66.475 299.2,61.092"]; + 2 -> 4 [label=, + lp="242,41.824", + pos="e,275.95,34.324 208.3,34.324 224.08,34.324 247.64,34.324 265.91,34.324"]; + 3 -> 3 [label=<1
⓿>, + lp="377,85.324", + pos="e,384.03,50.989 369.97,50.989 368.41,60.949 370.75,70.324 377,70.324 381,70.324 383.4,66.477 384.2,61.093"]; + 4 -> 3 [label=, + lp="335.5,41.824", + pos="e,358.85,34.324 312.18,34.324 322.81,34.324 336.69,34.324 348.8,34.324"]; + 4 -> 4 [label=, + lp="294,77.824", + pos="e,301.03,50.989 286.97,50.989 285.41,60.949 287.75,70.324 294,70.324 298,70.324 300.4,66.477 301.2,61.093"]; } subgraph cluster_gv1 { graph [bb="", - label="a U b", + fontname=Lato, + label=, labelloc=t, lheight=0.21, - lp="80.5,88.5", - lwidth=0.43, + lp="81.5,88.5", + lwidth=0.47, rankdir=LR ]; - node [height="", + node [fillcolor="#ffffa0", + fontname=Lato, + height="", label="\\N", peripheries="", pos="", shape=circle, - style="", + style=filled, width="" ]; - edge [label="", + edge [fontname=Lato, + label="", lp="", pos="" ]; I_gv1 [height=0.013889, label="", - pos="261,156.16", + pos="261,156.17", style=invis, width=0.013889]; "1_gv1" [height=0.5, label=1, - pos="316,156.16", + pos="316,156.17", width=0.5]; - I_gv1 -> "1_gv1" [pos="e,297.94,156.16 261.15,156.16 262.67,156.16 275.1,156.16 287.63,156.16"]; - "1_gv1" -> "1_gv1" [label="a & !b", - lp="316,199.66", - pos="e,322.38,173.2 309.62,173.2 308.32,183.02 310.44,192.16 316,192.16 319.47,192.16 321.6,188.59 322.4,183.51"]; + I_gv1 -> "1_gv1" [pos="e,297.94,156.17 261.15,156.17 262.67,156.17 275.1,156.17 287.63,156.17"]; + "1_gv1" -> "1_gv1" [label=, + lp="316,199.67", + pos="e,322.38,173.21 309.62,173.21 308.32,183.03 310.44,192.17 316,192.17 319.47,192.17 321.6,188.6 322.4,183.52"]; "0_gv1" [height=0.72222, label=0, peripheries=2, - pos="399,156.16", + pos="401,156.17", width=0.72222]; - "1_gv1" -> "0_gv1" [label=b, - lp="355.5,163.66", - pos="e,376.81,156.16 334.18,156.16 343.61,156.16 355.6,156.16 366.64,156.16"]; + "1_gv1" -> "0_gv1" [label=, + lp="356.5,163.67", + pos="e,379,156.17 334.2,156.17 344.16,156.17 357,156.17 368.7,156.17"]; "0_gv1" -> "0_gv1" [label=1, - lp="399,203.66", - pos="e,406.68,177.15 391.32,177.15 390.37,187.25 392.93,196.16 399,196.16 402.89,196.16 405.34,192.5 406.35,187.22"]; + lp="401,203.67", + pos="e,409.01,176.75 392.99,176.75 391.89,187.01 394.55,196.17 401,196.17 405.13,196.17 407.71,192.41 408.74,187.01"]; } } #+end_example @@ -457,10 +476,14 @@ of Promela syntax.) The =--dot= option (which usually is the default) causes automata to be output in GraphViz's format. -#+BEGIN_SRC sh :results verbatim :exports both +#+BEGIN_SRC sh :results verbatim :exports code ltl2tgba '(Ga -> Gb) W c' #+END_SRC +#+BEGIN_SRC sh :results verbatim :exports result +SPOT_DOTEXTRA= ltl2tgba '(Ga -> Gb) W c' --dot= +#+END_SRC + #+RESULTS: #+begin_example digraph G { @@ -492,7 +515,7 @@ picture. For instance use =dot -Tpng= or =dot -Tpdf=. #+NAME: oaut-dot1 #+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba '(Ga -> Gb) W c' | sed 's/\\/\\\\/' +SPOT_DOTEXTRA= ltl2tgba '(Ga -> Gb) W c' --dot= | sed 's/\\/\\\\/' #+END_SRC #+RESULTS: oaut-dot1 @@ -533,7 +556,14 @@ This output can be customized by passing optional characters to the of the default horizontal layout), =c= requests circle states, =s= causes strongly-connected components to be displayed, =n= causes the name (see below) of the automaton to be displayed, and =a= causes the -acceptance condition to be shown as well. +acceptance condition to be shown as well. Option =b= causes sets to +be ouput as bullets (e.g., ⓿ instead of ={0}=); option =r= (for +rainbow) causes sets to be displayed in different colors, while option +=R= also uses colors, but it chooses them depending on whether a set +is used with Fin-acceptance, Inf-acceptance, or both. Finally option +=f(FONT)= is used to select a fontname: is is often necessary when =b= +is used to ensure the characters ⓿, ❶, etc. are all selected from the +same font. #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba --dot=vcsna '(Ga -> Gb) W c' @@ -544,6 +574,7 @@ digraph G { label="(Gb | F!a) W c\nInf(0)" labelloc="t" node [shape="circle"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, height=0] I -> 1 subgraph cluster_0 { @@ -584,83 +615,50 @@ digraph G { #+NAME: oaut-dot2 #+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba --dot=vcsna '(Ga -> Gb) W c' | sed 's/\\/\\\\/' +SPOT_DOTEXTRA= ltl2tgba --dot=vcsna '(Ga -> Gb) W c' | sed 's/\\/\\\\/' #+END_SRC #+RESULTS: oaut-dot2 #+begin_example digraph G { - rankdir=LR - label="Fin(2) & (Inf(0)&Inf(1))" + label="(Gb | F!a) W c\\nInf(0)" labelloc="t" node [shape="circle"] - I [label="", style=invis, width=0] + I [label="", style=invis, height=0] I -> 1 subgraph cluster_0 { - color=grey - label="" - 5 [label="5"] - 6 [label="6"] - } - subgraph cluster_1 { - color=orange + color=green label="" 0 [label="0"] } + subgraph cluster_1 { + color=green + label="" + 3 [label="3"] + } subgraph cluster_2 { - color=orange - label="" - 9 [label="9"] - 10 [label="10"] - } - subgraph cluster_3 { - color=green - label="" - 8 [label="8"] - } - subgraph cluster_4 { - color=green - label="" - 7 [label="7"] - } - subgraph cluster_5 { - color=black - label="" - 2 [label="2"] - } - subgraph cluster_6 { color=red label="" 4 [label="4"] } - subgraph cluster_7 { + subgraph cluster_3 { color=green label="" 1 [label="1"] - 3 [label="3"] + 2 [label="2"] } - 0 -> 0 [label="a & b\\n{0,1,2}"] - 0 -> 0 [label="!a & !b\\n{2}"] - 0 -> 5 [label="a\\n{2}"] - 1 -> 4 [label="b"] - 1 -> 3 [label="a & !b"] - 2 -> 0 [label="a"] - 2 -> 7 [label="b"] - 3 -> 1 [label="a & b\\n{0,1}"] - 4 -> 4 [label="!b\\n{1,2}"] - 4 -> 2 [label="b"] - 5 -> 6 [label="1"] - 6 -> 5 [label="1"] - 7 -> 7 [label="!a & b\\n{0,1}"] - 7 -> 7 [label="a & b\\n{0,2}"] - 7 -> 8 [label="1"] - 8 -> 8 [label="!a & b\\n{0,2}"] - 8 -> 8 [label="a & b\\n{0,1}"] - 8 -> 9 [label="1"] - 9 -> 9 [label="!a & b\\n{0,2}"] - 9 -> 10 [label="a & b\\n{0,1}"] - 10 -> 9 [label="!a & b\\n{0,1}"] - 10 -> 10 [label="a & b\\n{0,2}"] + 0 -> 0 [label="b\\n{0}"] + 1 -> 0 [label="a & b & !c"] + 1 -> 1 [label="!a & !c\\n{0}"] + 1 -> 2 [label="a & !c"] + 1 -> 3 [label="c"] + 2 -> 1 [label="!a & !c\\n{0}"] + 2 -> 2 [label="a & !c"] + 2 -> 3 [label="!a & c"] + 2 -> 4 [label="a & c"] + 3 -> 3 [label="1\\n{0}"] + 4 -> 3 [label="!a"] + 4 -> 4 [label="a"] } #+end_example @@ -686,7 +684,7 @@ Here is an example involving all colors: #+NAME: oaut-dot3 #+BEGIN_SRC sh :results verbatim :exports none -autfilt --dot=cas < 1 - 0 [label="0", peripheries=2] - 0 -> 0 [label="1"] - 1 [label="1"] - 1 -> 0 [label="b"] - 1 -> 1 [label="a & !b"] -} -#+end_example - -#+NAME: oaut-name -#+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba --name='TGBA for %f' --dot=n 'a U b' | sed 's/\\/\\\\/' -#+END_SRC - #+RESULTS: oaut-name #+begin_example digraph G { rankdir=LR label="TGBA for a U b" labelloc="t" + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] I -> 1 0 [label="0", peripheries=2] diff --git a/doc/org/randaut.org b/doc/org/randaut.org index a6488de3c..cd6e0bb5d 100644 --- a/doc/org/randaut.org +++ b/doc/org/randaut.org @@ -9,56 +9,52 @@ By default, it will generate a random TGBA with 10 states, no acceptance sets, and using a set of atomic proposition you have to supply. +#+NAME: randaut1 #+BEGIN_SRC sh :results verbatim :exports code randaut a b #+END_SRC - -#+NAME: randaut1 -#+BEGIN_SRC sh :results verbatim :exports none -randaut a b | sed 's/\\/\\\\/' -#+END_SRC #+RESULTS: randaut1 #+begin_example digraph G { - 0 [label="", style=invis, height=0] - 0 -> 1 - 1 [label="0", peripheries=2] - 1 -> 2 [label="!a & !b"] - 1 -> 3 [label="!a & b"] - 2 [label="4", peripheries=2] - 2 -> 4 [label="a & b"] - 2 -> 5 [label="a & b"] - 2 -> 3 [label="a & b"] - 2 -> 6 [label="!a & b"] - 3 [label="2", peripheries=2] - 3 -> 3 [label="a & b"] - 3 -> 7 [label="!a & b"] - 3 -> 2 [label="!a & b"] - 3 -> 6 [label="!a & b"] - 4 [label="6", peripheries=2] - 4 -> 8 [label="!a & !b"] - 4 -> 6 [label="!a & !b"] - 4 -> 7 [label="a & b"] - 4 -> 9 [label="!a & b"] - 5 [label="5", peripheries=2] - 5 -> 2 [label="!a & b"] - 5 -> 10 [label="a & !b"] - 6 [label="3", peripheries=2] - 6 -> 3 [label="!a & !b"] - 6 -> 9 [label="!a & !b"] - 7 [label="7", peripheries=2] - 7 -> 9 [label="!a & b"] - 8 [label="1", peripheries=2] - 8 -> 1 [label="!a & b"] - 8 -> 6 [label="!a & !b"] - 9 [label="8", peripheries=2] - 9 -> 3 [label="a & b"] - 9 -> 10 [label="a & b"] - 9 -> 7 [label="a & !b"] - 9 -> 8 [label="!a & b"] - 10 [label="9", peripheries=2] - 10 -> 10 [label="a & !b"] - 10 -> 5 [label="a & !b"] + rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 8 [label=] + 0 -> 4 [label=] + 1 [label="1"] + 1 -> 2 [label=] + 1 -> 7 [label=] + 1 -> 4 [label=] + 2 [label="2"] + 2 -> 2 [label=] + 2 -> 0 [label=] + 2 -> 5 [label=] + 3 [label="3"] + 3 -> 6 [label=] + 4 [label="4"] + 4 -> 8 [label=] + 4 -> 2 [label=] + 4 -> 3 [label=] + 4 -> 7 [label=] + 5 [label="5"] + 5 -> 9 [label=] + 5 -> 3 [label=] + 5 -> 7 [label=] + 6 [label="6"] + 6 -> 7 [label=] + 6 -> 1 [label=] + 7 [label="7"] + 7 -> 3 [label=] + 8 [label="8"] + 8 -> 8 [label=] + 9 [label="9"] + 9 -> 0 [label=] + 9 -> 6 [label=] } #+end_example @@ -86,26 +82,27 @@ variance $(S-1)d(1-d)$. In particular =-d0= will cause all states to have 1 successors, and =-d1= will cause all states to be interconnected. +#+NAME: randaut2 #+BEGIN_SRC sh :results verbatim :exports code randaut -S3 -d0 2 #+END_SRC -#+NAME: randaut2 -#+BEGIN_SRC sh :results verbatim :exports none -randaut -S3 -d0 2 | sed 's/\\/\\\\/' -#+END_SRC - #+RESULTS: randaut2 #+begin_example digraph G { - 0 [label="", style=invis, height=0] - 0 -> 1 - 1 [label="0", peripheries=2] - 1 -> 2 [label="!p0 & !p1"] - 2 [label="2", peripheries=2] - 2 -> 3 [label="!p0 & p1"] - 3 [label="1", peripheries=2] - 3 -> 2 [label="p0 & p1"] + rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 2 [label=] + 1 [label="1"] + 1 -> 1 [label=] + 2 [label="2"] + 2 -> 1 [label=] } #+end_example @@ -115,32 +112,33 @@ $txt #+RESULTS: [[file:randaut2.png]] +#+NAME: randaut3 #+BEGIN_SRC sh :results verbatim :exports code randaut -S3 -d1 2 #+END_SRC -#+NAME: randaut3 -#+BEGIN_SRC sh :results verbatim :exports none -randaut -S3 -d1 2 | sed 's/\\/\\\\/' -#+END_SRC - #+RESULTS: randaut3 #+begin_example digraph G { - 0 [label="", style=invis, height=0] - 0 -> 1 - 1 [label="0", peripheries=2] - 1 -> 2 [label="!p0 & !p1"] - 1 -> 1 [label="!p0 & !p1"] - 1 -> 3 [label="p0 & p1"] - 2 [label="2", peripheries=2] - 2 -> 2 [label="p0 & !p1"] - 2 -> 3 [label="p0 & !p1"] - 2 -> 1 [label="!p0 & !p1"] - 3 [label="1", peripheries=2] - 3 -> 1 [label="!p0 & !p1"] - 3 -> 3 [label="!p0 & !p1"] - 3 -> 2 [label="p0 & p1"] + rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 2 [label=] + 0 -> 0 [label=] + 0 -> 1 [label=] + 1 [label="1"] + 1 -> 1 [label=] + 1 -> 2 [label=] + 1 -> 0 [label=] + 2 [label="2"] + 2 -> 1 [label=] + 2 -> 0 [label=] + 2 -> 2 [label=] } #+end_example @@ -171,29 +169,29 @@ The generation of acceptance sets is controlled with the following three paramet In addition, =-B= (or =--ba=) is a shorthand for =-A1 --state-acc=. -#+BEGIN_SRC sh :results verbatim :exports code -randaut -S3 -d0.5 -A2 -a0.2 2 -#+END_SRC - #+NAME: randaut4 -#+BEGIN_SRC sh :results verbatim :exports none -randaut -S3 -d0.5 -A2 -a0.2 2 | sed 's/\\/\\\\/' +#+BEGIN_SRC sh :results verbatim :exports code +randaut -S3 -d0.5 -A3 -a0.5 2 #+END_SRC #+RESULTS: randaut4 #+begin_example digraph G { - 0 [label="", style=invis, height=0] - 0 -> 1 - 1 [label="0"] - 1 -> 2 [label="!p0 & !p1\\n{1}"] - 1 -> 3 [label="!p0 & p1"] + rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 1 [label=] + 0 -> 0 [label=❷>] + 1 [label="1"] + 1 -> 2 [label=❶❷>] 2 [label="2"] - 2 -> 1 [label="!p0 & !p1\\n{0}"] - 2 -> 2 [label="!p0 & !p1"] - 3 [label="1"] - 3 -> 2 [label="!p0 & p1\\n{1}"] - 3 -> 3 [label="!p0 & p1"] + 2 -> 2 [label=⓿>] + 2 -> 1 [label=⓿❶>] } #+end_example @@ -204,29 +202,28 @@ $txt [[file:randaut4.png]] -#+BEGIN_SRC sh :results verbatim :exports code -randaut -S3 -d0.4 -B -a0.5 2 -#+END_SRC - #+NAME: randaut5 -#+BEGIN_SRC sh :results verbatim :exports none -randaut -S3 -d0.4 -B -a0.5 2 | sed 's/\\/\\\\/' +#+BEGIN_SRC sh :results verbatim :exports code +randaut -S3 -d0.4 -B -a0.7 2 #+END_SRC #+RESULTS: randaut5 #+begin_example digraph G { - 0 [label="", style=invis, height=0] - 0 -> 1 - 1 [label="0", peripheries=2] - 1 -> 2 [label="!p0 & !p1\\n{0}"] - 1 -> 1 [label="!p0 & p1\\n{0}"] + rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 2 [label=] + 1 [label="1"] + 1 -> 2 [label=] 2 [label="2", peripheries=2] - 2 -> 3 [label="!p0 & p1\\n{0}"] - 2 -> 1 [label="p0 & !p1\\n{0}"] - 3 [label="1"] - 3 -> 3 [label="p0 & !p1"] - 3 -> 1 [label="p0 & !p1"] + 2 -> 1 [label=] + 2 -> 0 [label=] } #+end_example @@ -250,31 +247,31 @@ Boolean formulas over the given atomic propositions, such that the sum of all these formulas is $\top$. The resulting automaton is therefore deterministic and complete. +#+NAME: randaut6 #+BEGIN_SRC sh :results verbatim :exports code randaut -D -S3 -d0.6 -A2 -a0.5 2 #+END_SRC -#+NAME: randaut6 -#+BEGIN_SRC sh :results verbatim :exports none -randaut -D -S3 -d0.6 -A2 -a0.5 2 | sed 's/\\/\\\\/' -#+END_SRC - #+RESULTS: randaut6 #+begin_example digraph G { - 0 [label="", style=invis, height=0] - 0 -> 1 - 1 [label="0"] - 1 -> 2 [label="p0\\n{1}"] - 1 -> 3 [label="!p0\\n{0,1}"] - 2 [label="1"] - 2 -> 3 [label="!p0 & p1"] - 2 -> 1 [label="!p0 & !p1\\n{0}"] - 2 -> 2 [label="p0\\n{0,1}"] - 3 [label="2"] - 3 -> 3 [label="p0 & p1\\n{1}"] - 3 -> 1 [label="p0 & !p1\\n{0}"] - 3 -> 2 [label="!p0"] + rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 1 [label=] + 0 -> 2 [label=] + 1 [label="1"] + 1 -> 2 [label=❶>] + 1 -> 0 [label=⓿>] + 2 [label="2"] + 2 -> 2 [label=⓿>] + 2 -> 0 [label=❶>] + 2 -> 1 [label=⓿>] } #+end_example diff --git a/doc/org/satmin.org b/doc/org/satmin.org index 143ecddd9..da9eedf25 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -96,6 +96,7 @@ ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" --stats='states=%s, det=%d' We can draw it: +#+NAME: gfaexxb3 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" #+END_SRC @@ -103,57 +104,32 @@ ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" #+begin_example digraph G { rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] I -> 0 0 [label="0"] - 0 -> 1 [label="!b\n{0}"] - 0 -> 1 [label="a & b"] - 0 -> 2 [label="!a & b"] + 0 -> 1 [label=⓿>] + 0 -> 2 [label=] + 0 -> 3 [label=] + 0 -> 3 [label=⓿>] 1 [label="1"] - 1 -> 1 [label="a & b\n{0}"] - 1 -> 1 [label="a & !b"] - 1 -> 2 [label="!a & !b"] - 1 -> 3 [label="!a & b\n{0}"] + 1 -> 0 [label=] + 1 -> 0 [label=⓿>] + 1 -> 1 [label=] + 1 -> 1 [label=⓿>] 2 [label="2"] - 2 -> 0 [label="a & !b"] - 2 -> 1 [label="b\n{0}"] - 2 -> 3 [label="!a & !b"] + 2 -> 0 [label=] + 2 -> 1 [label=⓿>] + 2 -> 1 [label=] + 2 -> 3 [label=⓿>] 3 [label="3"] - 3 -> 0 [label="a & b"] - 3 -> 0 [label="a & !b\n{0}"] - 3 -> 3 [label="!a & b"] - 3 -> 3 [label="!a & !b\n{0}"] -} -#+end_example - -#+NAME: gfaexxb3 -#+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" | sed 's/\\/\\\\/' -#+END_SRC -#+RESULTS: gfaexxb3 -#+begin_example -digraph G { - rankdir=LR - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0"] - 0 -> 1 [label="!b\\n{0}"] - 0 -> 1 [label="a & b"] - 0 -> 2 [label="!a & b"] - 1 [label="1"] - 1 -> 1 [label="a & b\\n{0}"] - 1 -> 1 [label="a & !b"] - 1 -> 2 [label="!a & !b"] - 1 -> 3 [label="!a & b\\n{0}"] - 2 [label="2"] - 2 -> 0 [label="a & !b"] - 2 -> 1 [label="b\\n{0}"] - 2 -> 3 [label="!a & !b"] - 3 [label="3"] - 3 -> 0 [label="a & b"] - 3 -> 0 [label="a & !b\\n{0}"] - 3 -> 3 [label="!a & b"] - 3 -> 3 [label="!a & !b\\n{0}"] + 3 -> 2 [label=⓿>] + 3 -> 2 [label=] + 3 -> 3 [label=⓿>] + 3 -> 3 [label=] } #+end_example @@ -168,82 +144,45 @@ acceptance. If we want a traditional Büchi automaton, with state-based acceptance, we only need to add the =-B= option. The result will of course be slightly bigger. +#+NAME: gfaexxb4 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" #+END_SRC -#+RESULTS: -#+begin_example -digraph G { - rankdir=LR - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0"] - 0 -> 0 [label="!a & b"] - 0 -> 1 [label="!a & !b"] - 0 -> 2 [label="a & !b"] - 0 -> 3 [label="a & b"] - 1 [label="1"] - 1 -> 0 [label="!a & b\n{0}"] - 1 -> 2 [label="a & !b\n{0}"] - 1 -> 3 [label="a & b\n{0}"] - 1 -> 4 [label="!a & !b\n{0}"] - 2 [label="2"] - 2 -> 4 [label="!a\n{0}"] - 2 -> 5 [label="a\n{0}"] - 3 [label="3"] - 3 -> 1 [label="!a & !b"] - 3 -> 2 [label="a & !b"] - 3 -> 4 [label="!a & b"] - 3 -> 5 [label="a & b"] - 4 [label="4"] - 4 -> 0 [label="!a & !b"] - 4 -> 1 [label="!a & b"] - 4 -> 2 [label="a & b"] - 4 -> 3 [label="a & !b"] - 5 [label="5"] - 5 -> 1 [label="b"] - 5 -> 4 [label="!a & !b"] - 5 -> 5 [label="a & !b"] -} -#+end_example - -#+NAME: gfaexxb4 -#+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" | sed 's/\\/\\\\/' -#+END_SRC #+RESULTS: gfaexxb4 #+begin_example digraph G { rankdir=LR + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] I [label="", style=invis, width=0] I -> 0 0 [label="0"] - 0 -> 0 [label="!a & b"] - 0 -> 1 [label="!a & !b"] - 0 -> 2 [label="a & !b"] - 0 -> 3 [label="a & b"] + 0 -> 0 [label=] + 0 -> 1 [label=] + 0 -> 2 [label=] 1 [label="1"] - 1 -> 0 [label="!a & b\\n{0}"] - 1 -> 2 [label="a & !b\\n{0}"] - 1 -> 3 [label="a & b\\n{0}"] - 1 -> 4 [label="!a & !b\\n{0}"] + 1 -> 4 [label=⓿>] + 1 -> 5 [label=⓿>] 2 [label="2"] - 2 -> 4 [label="!a\\n{0}"] - 2 -> 5 [label="a\\n{0}"] + 2 -> 1 [label=] + 2 -> 4 [label=] + 2 -> 5 [label=] 3 [label="3"] - 3 -> 1 [label="!a & !b"] - 3 -> 2 [label="a & !b"] - 3 -> 4 [label="!a & b"] - 3 -> 5 [label="a & b"] + 3 -> 0 [label=⓿>] + 3 -> 1 [label=⓿>] + 3 -> 2 [label=⓿>] 4 [label="4"] - 4 -> 0 [label="!a & !b"] - 4 -> 1 [label="!a & b"] - 4 -> 2 [label="a & b"] - 4 -> 3 [label="a & !b"] + 4 -> 0 [label=] + 4 -> 1 [label=] + 4 -> 2 [label=] + 4 -> 3 [label=] 5 [label="5"] - 5 -> 1 [label="b"] - 5 -> 4 [label="!a & !b"] - 5 -> 5 [label="a & !b"] + 5 -> 1 [label=] + 5 -> 3 [label=] + 5 -> 4 [label=] + 5 -> 5 [label=] } #+end_example diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 874923028..0560dd12b 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -51,10 +51,13 @@ static const argp_option options[] = { /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, - { "dot", OPT_DOT, "a|c|h|n|N|s|t|v", OPTION_ARG_OPTIONAL, + { "dot", OPT_DOT, "a|b|c|f(FONT)|h|n|N|r|R|s|t|v", OPTION_ARG_OPTIONAL, "GraphViz's format (default). Add letters for " - "(a) acceptance display, (c) circular nodes, (h) horizontal layout, " - "(v) vertical layout, (n) with name, (N) without name, (s) with SCCs, " + "(a) acceptance display, (b) acceptance sets as bullets," + "(c) circular nodes, (f(FONT)) use FONT, (h) horizontal layout, " + "(v) vertical layout, (n) with name, (N) without name, " + "(r) rainbow colors for acceptance set, " + "(R) color acceptance set by Inf/Fin, (s) with SCCs, " "(t) force transition-based acceptance.", 0 }, { "hoaf", 'H', "i|s|t|m|l", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 3669382ab..5df53f4d5 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -73,10 +73,13 @@ static const argp_option options[] = "of the given property)", 0 }, /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, - { "dot", OPT_DOT, "a|c|h|n|N|s|t|v", OPTION_ARG_OPTIONAL, - "GraphViz's format (default). Add letters for (a) acceptance display, " - "(c) circular nodes, (h) horizontal layout, (v) vertical layout, " - "(n) with name, (N) without name, (s) with SCCs, " + { "dot", OPT_DOT, "a|b|c|f(FONT)|h|n|N|r|R|s|t|v", OPTION_ARG_OPTIONAL, + "GraphViz's format (default). Add letters for " + "(a) acceptance display, (b) acceptance sets as bullets," + "(c) circular nodes, (f(FONT)) use FONT, (h) horizontal layout, " + "(v) vertical layout, (n) with name, (N) without name, " + "(r) rainbow colors for acceptance set, " + "(R) color acceptance set by Inf/Fin, (s) with SCCs, " "(t) force transition-based acceptance.", 0 }, { "hoaf", 'H', "i|s|t|m|l", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " diff --git a/src/bin/man/spot-x.x b/src/bin/man/spot-x.x index b8d673040..7677d9a5b 100644 --- a/src/bin/man/spot-x.x +++ b/src/bin/man/spot-x.x @@ -11,6 +11,15 @@ spot-x \- Common fine-tuning options. [ENVIRONMENT VARIABLES] +.TP +\fBSPOT_DOTDEFAULT\fR +Whenever the \f(CW--dot\fR option is used without argument (even +implicitely), the contents of this variable is used as default +argument. If you have some default setting in \fBSPOT_DOTDEFAULT\fR +but want to alter them temporarily for one call, use +\f(CW--dot=.yyy\fR: the dot character will be replaced by the contents +of the \f(CWSPOT_DOTDEFAULT\fR environment variable. + .TP \fBSPOT_DOTEXTRA\fR The contents of this variable is added to any dot output, immediately diff --git a/src/misc/escape.cc b/src/misc/escape.cc index e9ba8dd3c..3131f5621 100644 --- a/src/misc/escape.cc +++ b/src/misc/escape.cc @@ -77,6 +77,31 @@ namespace spot return os; } + std::ostream& + escape_html(std::ostream& os, const std::string& str) + { + for (auto i: str) + switch (i) + { + case '&': + os << "&"; + break; + case '"': + os << """; + break; + case '<': + os << "<"; + break; + case '>': + os << ">"; + break; + default: + os << i; + break; + } + return os; + } + std::ostream& escape_str(std::ostream& os, const std::string& str) { diff --git a/src/misc/escape.hh b/src/misc/escape.hh index 3b1bff613..d28c55639 100644 --- a/src/misc/escape.hh +++ b/src/misc/escape.hh @@ -46,6 +46,13 @@ namespace spot SPOT_API std::ostream& escape_latex(std::ostream& os, const std::string& str); + /// \brief Escape special HTML characters. + /// + /// The following characters are rewritten: + /// > < " & + SPOT_API std::ostream& + escape_html(std::ostream& os, const std::string& str); + /// \brief Escape characters ", \\, and /// \\n in \a str. SPOT_API std::ostream& diff --git a/src/tgba/acc.cc b/src/tgba/acc.cc index 6f7de2b68..6dbdff4af 100644 --- a/src/tgba/acc.cc +++ b/src/tgba/acc.cc @@ -48,9 +48,16 @@ namespace spot namespace { + void default_set_printer(std::ostream& os, int v) + { + os << v; + } + + template static void print_code(std::ostream& os, - const acc_cond::acc_code& code, unsigned pos) + const acc_cond::acc_code& code, unsigned pos, + std::function set_printer) { const char* op = " | "; auto& w = code[pos]; @@ -59,7 +66,7 @@ namespace spot switch (w.op) { case acc_cond::acc_op::And: - op = " & "; + op = html ? " & " : " & "; case acc_cond::acc_op::Or: { unsigned sub = pos - w.size; @@ -73,7 +80,7 @@ namespace spot first = false; else os << op; - print_code(os, code, pos); + print_code(os, code, pos, set_printer); pos -= code[pos].size; } if (!top) @@ -102,8 +109,10 @@ namespace spot { if (a & 1) { - os << and_ << "Inf(" << negated << level << ')'; - and_ = "&"; + os << and_ << "Inf(" << negated; + set_printer(os, level); + os << ')'; + and_ = html ? "&" : "&"; } a >>= 1; ++level; @@ -135,7 +144,9 @@ namespace spot { if (a & 1) { - os << or_ << "Fin(" << negated << level << ')'; + os << or_ << "Fin(" << negated; + set_printer(os, level); + os << ')'; or_ = "|"; } a >>= 1; @@ -746,13 +757,69 @@ namespace spot return used_in_cond; } + std::pair + acc_cond::acc_code::used_inf_fin_sets() const + { + if (is_true() || is_false()) + return {0U, 0U}; + + acc_cond::mark_t used_fin = 0U; + acc_cond::mark_t used_inf = 0U; + auto pos = &back(); + auto end = &front(); + while (pos > end) + { + switch (pos->op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::FinNeg: + used_fin |= pos[-1].mark; + pos -= 2; + break; + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + used_inf |= pos[-1].mark; + pos -= 2; + break; + } + } + return {used_inf, used_fin}; + } + + std::ostream& + acc_cond::acc_code::to_html(std::ostream& os, + std::function + set_printer) const + { + if (empty()) + os << 't'; + else + print_code(os, *this, size() - 1, + set_printer ? set_printer : default_set_printer); + return os; + } + + std::ostream& + acc_cond::acc_code::to_text(std::ostream& os, + std::function + set_printer) const + { + if (empty()) + os << 't'; + else + print_code(os, *this, size() - 1, + set_printer ? set_printer : default_set_printer); + return os; + } + + std::ostream& operator<<(std::ostream& os, const spot::acc_cond::acc_code& code) { - if (code.empty()) - os << 't'; - else - print_code(os, code, code.size() - 1); - return os; + return code.to_text(os); } } diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh index d9fbad119..70a576212 100644 --- a/src/tgba/acc.hh +++ b/src/tgba/acc.hh @@ -660,6 +660,24 @@ namespace spot // Return the set of sets appearing in the condition. acc_cond::mark_t used_sets() const; + // Return the sets used as Inf or Fin in the acceptance condition + std::pair used_inf_fin_sets() const; + + // Print the acceptance as HTML. The set_printer function can + // be used to implement customized output for set numbers. + std::ostream& + to_html(std::ostream& os, + std::function + set_printer = nullptr) const; + + // Print the acceptance as text. The set_printer function can + // be used to implement customized output for set numbers. + std::ostream& + to_text(std::ostream& os, + std::function + set_printer = nullptr) const; + + // Calls to_text SPOT_API friend std::ostream& operator<<(std::ostream& os, const acc_code& code); }; diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 702f4c726..1b7bf9d30 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -31,11 +31,16 @@ #include "tgba/formula2bdd.hh" #include "tgbaalgos/sccinfo.hh" #include +#include +#include + namespace spot { namespace { + constexpr int MAX_BULLET = 20; + class dotty_output { std::ostream& os_; @@ -46,74 +51,229 @@ namespace spot bool opt_show_acc_ = false; bool mark_states_ = false; bool opt_scc_ = false; + bool opt_html_labels_ = false; const_tgba_digraph_ptr aut_; std::vector* sn_; std::string* name_ = nullptr; + acc_cond::mark_t inf_sets_ = 0U; + acc_cond::mark_t fin_sets_ = 0U; + bool opt_rainbow = false; + bool opt_bullet = false; + bool opt_all_bullets = false; + std::string opt_font_; + + const char* const palette9[9] = + { + "#5DA5DA", /* blue */ + "#F17CB0", /* pink */ + "#FAA43A", /* orange */ + "#B276B2", /* purple */ + "#60BD68", /* green */ + "#F15854", /* red */ + "#B2912F", /* brown */ + "#4D4D4D", /* gray */ + "#DECF3F", /* yellow */ + }; + const char*const* palette = palette9; + int palette_mod = 9; public: + + void + parse_opts(const char* options) + { + const char* orig = options; + while (char c = *options++) + switch (c) + { + case '.': + { + static const char* def = getenv("SPOT_DOTDEFAULT"); + // Prevent infinite recursions... + if (orig == def) + throw std::runtime_error + (std::string("SPOT_DOTDEFAULT should not contain '.'")); + if (def) + parse_opts(def); + break; + } + case 'a': + opt_show_acc_ = true; + break; + case 'b': + opt_bullet = true; + break; + case 'c': + opt_circles_ = true; + break; + case 'h': + opt_horizontal_ = true; + break; + case 'f': + if (*options != '(') + throw std::runtime_error + (std::string("invalid font specification for dotty()")); + { + auto* end = strchr(++options, ')'); + if (!end) + throw std::runtime_error + (std::string("invalid font specification for dotty()")); + opt_font_ = std::string(options, end - options); + options = end + 1; + } + break; + case 'n': + opt_name_ = true; + break; + case 'N': + opt_name_ = false; + break; + case 'r': + opt_html_labels_ = true; + opt_rainbow = true; + break; + case 'R': + opt_html_labels_ = true; + opt_rainbow = false; + break; + case 's': + opt_scc_ = true; + break; + case 'v': + opt_horizontal_ = false; + break; + case 't': + opt_force_acc_trans_ = true; + break; + default: + throw std::runtime_error + (std::string("unknown option for dotty(): ") + c); + } + } + dotty_output(std::ostream& os, const char* options) : os_(os) { - if (options) - while (char c = *options++) - switch (c) - { - case 'a': - opt_show_acc_ = true; - break; - case 'c': - opt_circles_ = true; - break; - case 'h': - opt_horizontal_ = true; - break; - case 'n': - opt_name_ = true; - break; - case 'N': - opt_name_ = false; - break; - case 's': - opt_scc_ = true; - break; - case 'v': - opt_horizontal_ = false; - break; - case 't': - opt_force_acc_trans_ = true; - break; - default: - throw std::runtime_error - (std::string("unknown option for dotty(): ") + c); - } + parse_opts(options ? options : "."); + } + + void + output_set(std::ostream& os, int v) const + { + if (opt_bullet && (v >= 0) & (v <= MAX_BULLET)) + { + static const char* const tab[MAX_BULLET + 1] = { + "⓿", "❶", "❷", "❸", + "❹", "❺", "❻", "❼", + "❽", "❾", "❿", "⓫", + "⓬", "⓭", "⓮", "⓯", + "⓰", "⓱", "⓲", "⓳", + "⓴", + }; + os << tab[v]; + } + else + { + os << v; + } + } + + + const char* + html_set_color(int v) const + { + if (opt_rainbow) + return palette[v % palette_mod]; + // Color according to Fin/Inf + if (inf_sets_.has(v)) + { + if (fin_sets_.has(v)) + return palette[2]; + else + return palette[0]; + } + else + { + return palette[1]; + } + } + + void + output_html_set_aux(std::ostream& os, int v) const + { + os << ""; + output_set(os, v); + os << ""; + } + + void + output_html_set(int v) const + { + output_html_set_aux(os_, v); } void start() { + if (opt_html_labels_) + std::tie(inf_sets_, fin_sets_) = + aut_->get_acceptance().used_inf_fin_sets(); + if (opt_bullet && aut_->acc().num_sets() <= MAX_BULLET) + opt_all_bullets = true; + os_ << "digraph G {\n"; if (opt_horizontal_) os_ << " rankdir=LR\n"; if (name_ || opt_show_acc_) { - os_ << " label=\""; - if (name_) + if (!opt_html_labels_) { - escape_str(os_, *name_); + os_ << " label=\""; + if (name_) + { + escape_str(os_, *name_); + if (opt_show_acc_) + os_ << "\\n"; + } if (opt_show_acc_) - os_ << "\\n"; + aut_->get_acceptance().to_text + (os_, [this](std::ostream& os, int v) + { + this->output_set(os, v); + }); + os_ << "\"\n"; } - if (opt_show_acc_) - os_ << aut_->get_acceptance(); - os_ << "\"\n labelloc=\"t\"\n"; + else + { + os_ << " label=<"; + if (name_) + { + escape_html(os_, *name_); + if (opt_show_acc_) + os_ << "
"; + } + if (opt_show_acc_) + aut_->get_acceptance().to_html + (os_, [this](std::ostream& os, int v) + { + this->output_html_set_aux(os, v); + }); + os_ << ">\n"; + } + os_ << " labelloc=\"t\"\n"; } if (opt_circles_) os_ << " node [shape=\"circle\"]\n"; + if (!opt_font_.empty()) + os_ << " fontname=\"" << opt_font_ + << "\"\n node [fontname=\"" << opt_font_ + << "\"]\n edge [fontname=\"" << opt_font_ + << "\"]\n"; // Any extra text passed in the SPOT_DOTEXTRA environment // variable should be output at the end of the "header", so // that our setup can be overridden. static const char* extra = getenv("SPOT_DOTEXTRA"); - if (extra) + if (extra && *extra) os_ << " " << extra << '\n'; os_ << " I [label=\"\", style=invis, "; os_ << (opt_horizontal_ ? "width" : "height"); @@ -144,15 +304,53 @@ namespace spot process_link(const tgba_digraph::trans_storage_t& t) { std::string label = bdd_format_formula(aut_->get_dict(), t.cond); - label = escape_str(label); - if (!mark_states_) - if (auto a = t.acc) - { - label += "\\n"; - label += aut_->acc().format(a); - } - os_ << " " << t.src << " -> " << t.dst - << " [label=\"" + label + "\"]\n"; + os_ << " " << t.src << " -> " << t.dst; + if (!opt_html_labels_) + { + os_ << " [label=\""; + escape_str(os_, label); + if (!mark_states_) + if (auto a = t.acc) + { + os_ << "\\n"; + if (!opt_all_bullets) + os_ << '{'; + const char* space = ""; + for (auto v: a.sets()) + { + if (!opt_all_bullets) + os_ << space; + output_set(os_, v); + space = ","; + } + if (!opt_all_bullets) + os_ << '}'; + } + os_ << "\"]\n"; + } + else + { + os_ << " [label=<"; + escape_html(os_, label); + if (!mark_states_) + if (auto a = t.acc) + { + os_ << "
"; + if (!opt_all_bullets) + os_ << '{'; + const char* space = ""; + for (auto v: a.sets()) + { + if (!opt_all_bullets) + os_ << space; + output_html_set(v); + space = ","; + } + if (!opt_all_bullets) + os_ << '}'; + } + os_ << ">]\n"; + } } void print(const const_tgba_digraph_ptr& aut) diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 65e86c8bf..76be7bc02 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -308,7 +308,7 @@ State: 3 "s3" EOF $autfilt -H input | - SPOT_DOTEXTRA='/* hello world */' $autfilt --dot=vcsn >output + SPOT_DOTDEFAULT=vcsn SPOT_DOTEXTRA='/* hello world */' $autfilt >output cat >expected <output +$ltl2tgba --dot=ban 'GFa & GFb' >output cat output cat >expected < 0 0 [label="0"] - 0 -> 0 [label="a & b\n{0,1}"] + 0 -> 0 [label="a & b\n⓿❶"] 0 -> 0 [label="!a & !b"] - 0 -> 0 [label="!a & b\n{1}"] - 0 -> 0 [label="a & !b\n{0}"] + 0 -> 0 [label="!a & b\n❶"] + 0 -> 0 [label="a & !b\n⓿"] +} +EOF +diff output expected + + +SPOT_DOTDEFAULT=bra $ltl2tgba --dot='c.f(Lato)' 'GFa & GFb' >output +cat output + +zero='⓿' +one='❶' +cat >expected < + labelloc="t" + node [shape="circle"] + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 0 [label=$zero$one>] + 0 -> 0 [label=] + 0 -> 0 [label=$one>] + 0 -> 0 [label=$zero>] } EOF diff output expected diff --git a/wrap/python/spot.py b/wrap/python/spot.py index 808a50ade..25dc207bf 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -31,7 +31,7 @@ def _ostream_to_svg(ostr): res = dotty.communicate() return res[0].decode('utf-8') -def _render_automaton_as_svg(a, opt=""): +def _render_automaton_as_svg(a, opt=None): ostr = ostringstream() dotty_reachable(ostr, a, opt) return _ostream_to_svg(ostr) @@ -47,7 +47,7 @@ def _render_formula_as_svg(a): dotty(ostr, a) return SVG(_ostream_to_svg(ostr)) -def _render_tgba_as_svg(a, opt=""): +def _render_tgba_as_svg(a, opt=None): # Load the SVG function only if we need it. This way the bindings # can still be used outside of IPython if IPython is not # installed. diff --git a/wrap/python/tests/automata.ipynb b/wrap/python/tests/automata.ipynb index e7950ffe5..8c6c82c6a 100644 --- a/wrap/python/tests/automata.ipynb +++ b/wrap/python/tests/automata.ipynb @@ -1,7 +1,7 @@ { "metadata": { "name": "", - "signature": "sha256:5d2a4f77c6bcffce3121cc011949d340222f35788edaf95171ae9917ea3794d6" + "signature": "sha256:46e5472540261241876badd1678f26f98c6708247f2b22d92e76ec7d15136f5c" }, "nbformat": 3, "nbformat_minor": 0, @@ -14,7 +14,8 @@ "input": [ "import spot\n", "import os\n", - "os.environ['SPOT_DOTEXTRA'] = 'node[style=filled,fillcolor=\"#88ddff\"]'" + "os.environ['SPOT_DOTEXTRA'] = 'node[style=filled,fillcolor=\"#ffffaa\"]'\n", + "os.environ['SPOT_DOTDEFAULT'] = 'rbc'" ], "language": "python", "metadata": {}, @@ -33,7 +34,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 2, + "prompt_number": 3, "svg": [ "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fd82431b0f0> >" + " *' at 0x7f7be0d392d0> >" ] } ], - "prompt_number": 2 + "prompt_number": 3 }, { "cell_type": "code", "collapsed": false, "input": [ - "a.show(\"cs\")" + "a.show(\"\")" ], "language": "python", "metadata": {}, @@ -172,17 +173,152 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 3, + "prompt_number": 4, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "a.show(\".ast\")" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 5, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", "cluster_0\n", - "\n", + "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "cluster_2\n", "\n", @@ -190,7 +326,7 @@ "\n", "\n", "0\n", - "\n", + "\n", "0\n", "\n", "\n", @@ -202,104 +338,106 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "a & !b\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", + "\u24ff\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", + "\u24ff\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", + "\u24ff\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], - "prompt_number": 3 + "prompt_number": 5 }, { "cell_type": "code", @@ -316,159 +454,19 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 4, + "prompt_number": 6, "text": [ "a U b" ] } ], - "prompt_number": 4 - }, - { - "cell_type": "code", - "collapsed": false, - "input": [ - "spot.translate(f)" - ], - "language": "python", - "metadata": {}, - "outputs": [ - { - "metadata": {}, - "output_type": "pyout", - "prompt_number": 5, - "svg": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n" - ], - "text": [ - " *' at 0x7fd8242f2870> >" - ] - } - ], - "prompt_number": 5 - }, - { - "cell_type": "code", - "collapsed": false, - "input": [ - "f.translate()" - ], - "language": "python", - "metadata": {}, - "outputs": [ - { - "metadata": {}, - "output_type": "pyout", - "prompt_number": 6, - "svg": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n" - ], - "text": [ - " *' at 0x7fd8242f2ab0> >" - ] - } - ], "prompt_number": 6 }, { "cell_type": "code", "collapsed": false, "input": [ - "f.translate('mon')" + "spot.translate(f)" ], "language": "python", "metadata": {}, @@ -484,55 +482,195 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fd8242f2900> >" + " *' at 0x7f7be0d10930> >" ] } ], "prompt_number": 7 }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f.translate()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 8, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f7be0d10b70> >" + ] + } + ], + "prompt_number": 8 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f.translate('mon')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 9, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f7be0d10ae0> >" + ] + } + ], + "prompt_number": 9 + }, { "cell_type": "code", "collapsed": false, @@ -548,19 +686,19 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 8, + "prompt_number": 10, "text": [ "Ga | Gb | Gc" ] } ], - "prompt_number": 8 + "prompt_number": 10 }, { "cell_type": "code", "collapsed": false, "input": [ - "f.translate('ba', 'small').show('vc')" + "f.translate('ba', 'small').show('v')" ], "language": "python", "metadata": {}, @@ -568,92 +706,92 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 9, + "prompt_number": 11, "svg": [ - "\n", + "\n", "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], - "prompt_number": 9 + "prompt_number": 11 }, { "cell_type": "code", "collapsed": false, "input": [ - "f.translate('ba', 'det').show('vc')" + "f.translate('ba', 'det').show('v.')" ], "language": "python", "metadata": {}, @@ -661,7 +799,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 10, + "prompt_number": 12, "svg": [ "\n", "\n", @@ -670,7 +808,7 @@ "\n", "\n", "6\n", - "\n", + "\n", "\n", "6\n", "\n", @@ -683,11 +821,11 @@ "6->6\n", "\n", "\n", - "a & b & c\n", + "a & b & c\n", "\n", "\n", "0\n", - "\n", + "\n", "\n", "0\n", "\n", @@ -695,11 +833,11 @@ "6->0\n", "\n", "\n", - "!a & !b & c\n", + "!a & !b & c\n", "\n", "\n", "1\n", - "\n", + "\n", "\n", "1\n", "\n", @@ -707,11 +845,11 @@ "6->1\n", "\n", "\n", - "!a & b & !c\n", + "!a & b & !c\n", "\n", "\n", "2\n", - "\n", + "\n", "\n", "2\n", "\n", @@ -719,11 +857,11 @@ "6->2\n", "\n", "\n", - "a & !b & !c\n", + "a & !b & !c\n", "\n", "\n", "3\n", - "\n", + "\n", "\n", "3\n", "\n", @@ -731,11 +869,11 @@ "6->3\n", "\n", "\n", - "!a & b & c\n", + "!a & b & c\n", "\n", "\n", "4\n", - "\n", + "\n", "\n", "4\n", "\n", @@ -743,11 +881,11 @@ "6->4\n", "\n", "\n", - "a & b & !c\n", + "a & b & !c\n", "\n", "\n", "5\n", - "\n", + "\n", "\n", "5\n", "\n", @@ -755,89 +893,89 @@ "6->5\n", "\n", "\n", - "a & !b & c\n", + "a & !b & c\n", "\n", "\n", "0->0\n", "\n", "\n", - "c\n", + "c\n", "\n", "\n", "1->1\n", "\n", "\n", - "b\n", + "b\n", "\n", "\n", "2->2\n", "\n", "\n", - "a\n", + "a\n", "\n", "\n", "3->0\n", "\n", "\n", - "!b & c\n", + "!b & c\n", "\n", "\n", "3->1\n", "\n", "\n", - "b & !c\n", + "b & !c\n", "\n", "\n", "3->3\n", "\n", "\n", - "b & c\n", + "b & c\n", "\n", "\n", "4->1\n", "\n", "\n", - "!a & b\n", + "!a & b\n", "\n", "\n", "4->2\n", "\n", "\n", - "a & !b\n", + "a & !b\n", "\n", "\n", "4->4\n", "\n", "\n", - "a & b\n", + "a & b\n", "\n", "\n", "5->0\n", "\n", "\n", - "!a & c\n", + "!a & c\n", "\n", "\n", "5->2\n", "\n", "\n", - "a & !c\n", + "a & !c\n", "\n", "\n", "5->5\n", "\n", "\n", - "a & c\n", + "a & c\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], - "prompt_number": 10 + "prompt_number": 12 }, { "cell_type": "code",