Commit 7dfeda8e authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

org: simplify babel blocks using #+PROPERTY: header-args

This feature is in Org 9, which is already required.

* doc/org/autcross.org, doc/org/autfilt.org, doc/org/compile.org,
doc/org/concepts.org, doc/org/csv.org, doc/org/dstar2tgba.org,
doc/org/genaut.org, doc/org/genltl.org, doc/org/hierarchy.org,
doc/org/hoa.org, doc/org/ioltl.org, doc/org/ltl2tgba.org,
doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltldo.org,
doc/org/ltlfilt.org, doc/org/ltlgrind.org, doc/org/ltlsynt.org,
doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org,
doc/org/satmin.org, doc/org/setup.org, doc/org/tools.org,
doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut04.org, doc/org/tut10.org, doc/org/tut11.org,
doc/org/tut12.org, doc/org/tut20.org, doc/org/tut21.org,
doc/org/tut22.org, doc/org/tut23.org, doc/org/tut24.org,
doc/org/tut30.org, doc/org/tut31.org, doc/org/tut50.org,
doc/org/upgrade2.org: Simplify SRC block setups for sh, python and
C++.  Also fix a few typos and examples along the way.
parent 8c99cffa
This diff is collapsed.
This diff is collapsed.
......@@ -3,6 +3,7 @@
#+DESCRIPTION: How to compile C++14 programs using Spot
#+INCLUDE: setup.org
#+HTML_LINK_UP: tut.html
#+PROPERTY: header-args:C+++ :results verbatim :exports both
This page is not about compiling Spot itself (for this, please refer
to the [[file:install.org][installation instructions]]), but about how to compile and
......@@ -14,7 +15,7 @@ As an example we will take the following simple program, stored in a
file called =hello.cc=:
#+NAME: hello-word
#+BEGIN_SRC C++ :results verbatim :exports both
#+BEGIN_SRC C++
#include <iostream>
#include <spot/misc/version.hh>
......@@ -30,7 +31,7 @@ greetings and the Spot version:
#+RESULTS: hello-word
: Hello world!
: This is Spot 1.99.6a.
: This is Spot 2.7.2.dev.
To successfully compile this example program, we need a C++ compiler,
......
......@@ -3,6 +3,7 @@
#+DESCRIPTION: Informal explanation of various concepts used in Spot.
#+INCLUDE: setup.org
#+HTML_LINK_UP: index.html
#+PROPERTY: header-args:sh :results verbatim :exports none
This page documents some of the concepts used in Spot, and whose
knowledge is usually assumed throughout the documentation. The
......@@ -128,7 +129,7 @@ For instance here is a Büchi automaton that accepts only words in
which $a$ is always true, and $b$ is true infinitely often.
#+NAME: buchi-example1
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
ltl2tgba 'G(a) & GF(b)' -B -d
#+END_SRC
......@@ -149,7 +150,7 @@ the [[#ltl][LTL formula]] =G(door_open -> light_on)= that specifies that
=light_on= should be true whenever =door_open= is true.
#+NAME: buchi-example2
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
ltl2tgba 'G(door_open -> light_on)' -d -C
#+END_SRC
......@@ -183,7 +184,7 @@ all runs in which at all point $a$ is true iff $b$ is true at the next
instant.
#+NAME: buchi-example3
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
ltl2tgba 'G(a <-> Xb)' -B -d
#+END_SRC
#+BEGIN_SRC dot :file concept-buchi3.svg :var txt=buchi-example3 :exports results
......@@ -210,7 +211,7 @@ have been aggregated in an edge.
Here is a simple example:
#+NAME: te1
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
cat >concept-te.hoa <<EOF
HOA: v1
Acceptance: 0 t
......@@ -232,7 +233,7 @@ $txt
[[file:concept-te1.svg]]
#+NAME: size
#+BEGIN_SRC sh :exports none
#+BEGIN_SRC sh
autfilt --merge --stats=$arg concept-te.hoa
#+END_SRC
......@@ -243,7 +244,7 @@ This is because those formula-labeled edges actually simplify the
following transition structure:
#+NAME: te2
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
autfilt concept-te.hoa -d.A
#+END_SRC
#+BEGIN_SRC dot :file concept-te2.svg :var txt=te2 :exports results
......@@ -296,7 +297,7 @@ states labeled with ❶ belong to set 1. Here each acceptance set
contains a single state.
#+NAME: gen-buchi-example1
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
ltl2tgba 'GFa & GFb' | autfilt -S --sat-minimize -d
#+END_SRC
......@@ -317,7 +318,7 @@ following automaton has the same language as the previous one (despite
its more complex look).
#+NAME: gen-buchi-example2
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
ltl2tgba 'GFa & GFb' -S -d
#+END_SRC
......@@ -337,7 +338,7 @@ with a 2-state generalized-Büchi automaton, but the smallest
equivalent Büchi automaton has three state:
#+NAME: gen-buchi-example-ba
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
ltl2tgba 'GFa & GFb' -B -d
#+END_SRC
......@@ -356,7 +357,7 @@ acceptance sets (as below). Spot's output routines have options for
both.
#+NAME: gen-buchi-example-ba2
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
ltl2tgba 'GFa & GFb' -B -d.b
#+END_SRC
......@@ -384,7 +385,7 @@ Here is an example of Transition-based Generalized Büchi Automaton
(TGBA).
#+NAME: tgba-example1
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
ltl2tgba 'GF(a & X(a U b))' -d
#+END_SRC
#+BEGIN_SRC dot :file concept-tgba1.svg :var txt=tgba-example1 :exports results
......@@ -403,7 +404,7 @@ The typical example is the LTL formula =GFa= (infinitely often $a$)
that can be represented using a one-state transition-based Büchi
automaton:
#+NAME: tgba-example2
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
ltl2tgba 'GFa' -d
#+END_SRC
#+BEGIN_SRC dot :file concept-tgba2.svg :var txt=tgba-example2 :exports results
......@@ -417,7 +418,7 @@ While the same property require a 2-state Büchi automaton using
state-based acceptance:
#+NAME: tgba-example3
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
ltl2tgba 'GFa' -B -d
#+END_SRC
#+BEGIN_SRC dot :file concept-tba-vs-ba.svg :var txt=tgba-example3 :exports results
......@@ -544,7 +545,7 @@ produced by =ltl2dstar= for the LTL formula =GFa | FGb=, but displayed
by Spot:
#+NAME: twa-example1
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
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
......@@ -572,7 +573,7 @@ For instance the following alternating co-Büchi ω-automaton was
generated by [[https://sourceforge.net/projects/ltl3ba/][=ltl3ba 1.1.3=]] for the LTL formula =GF(a <-> Xb)=.
#+NAME: concepts-alt
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
autfilt -d.ba <<EOF
HOA: v1
States: 5
......@@ -635,7 +636,7 @@ alternating automata is the [[#hoa][HOA format, introduced below]].
infinitely often $p_1$). The graphical representation of that
automaton follows.
#+BEGIN_SRC sh :results verbatim :exports results
#+BEGIN_SRC sh :exports results
ltl2tgba -s 'p0 | GFp1' > tmp.$$
ltl2tgba -s6 'p0 | GFp1' | pr -w80 -m -t tmp.$$ -
rm tmp.$$
......@@ -665,7 +666,7 @@ accept_all: accept_all:
#+end_example
#+NAME: never-ex1
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
ltl2tgba -Bd 'p0 | GFp1'
#+END_SRC
#+BEGIN_SRC dot :file concept-never1.svg :var txt=never-ex1 :exports results
......@@ -697,7 +698,7 @@ LTL to (state-based) generalized Büchi automata, and then used by
For instance the Büchi automaton we used as an example for never
claims can be encoded as follows:
#+BEGIN_SRC sh :results verbatim :exports results
#+BEGIN_SRC sh :exports results
ltl2tgba --ba --lbtt 'p0 | GFp1'
#+END_SRC
......@@ -727,7 +728,7 @@ The format has been extended in two ways. First, LBTT extended it to
support transition-based acceptance. This is indicated by a =t= on
the first line:
#+BEGIN_SRC sh :results verbatim :exports results
#+BEGIN_SRC sh :exports results
ltl2tgba --lbtt 'p0 | GFp1'
#+END_SRC
......@@ -748,7 +749,7 @@ ltl2tgba --lbtt 'p0 | GFp1'
#+end_example
#+NAME: lbtt-ex2
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
ltl2tgba -d 'p0 | GFp1'
#+END_SRC
#+BEGIN_SRC dot :file concept-lbtt2.svg :var txt=lbtt-ex2 :exports results
......@@ -781,7 +782,7 @@ preferred. =ltl2dstar= can now also output HOA directly.
Here is one Rabin automaton in the DSTAR format:
#+BEGIN_SRC sh :results verbatim :exports results
#+BEGIN_SRC sh :exports results
echo '| F G p0 G F p1' | ltl2dstar --output-format=native - -
#+END_SRC
......@@ -821,7 +822,7 @@ Acc-Sig: +0 +1
#+end_example
#+NAME: dstar-example1
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
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
......@@ -840,7 +841,7 @@ The [[http://adl.github.io/hoaf/][HOA format]] inherits several features from th
extends it in many ways, including support for non-deterministic
automata, alternating automata, and for arbitrary acceptance conditions.
#+BEGIN_SRC sh :results verbatim :exports results
#+BEGIN_SRC sh :exports results
ltldo ltl2dstar -f 'FGp0 | GFp1' --name=%f
#+END_SRC
......@@ -880,7 +881,7 @@ State: 3 {1 3}
#+end_example
#+NAME: hoa1
#+BEGIN_SRC sh :results verbatim :exports none
#+BEGIN_SRC sh
ltldo ltl2dstar -f 'FGp0 | GFp1' -d
#+END_SRC
#+BEGIN_SRC dot :file concept-hoa.svg :var txt=hoa1 :exports results
......@@ -994,7 +995,7 @@ automaton can then be simplified using several algorithms depending on what opti
Here is for instance a translation of ={(1;1)[*]}[]->a= discussed [[#psl][above]].
#+NAME: ltl2tgba1
#+BEGIN_SRC sh :results verbatim :exports code
#+BEGIN_SRC sh :exports code
ltl2tgba '{(1;1)[*]}[]->a' -d
#+END_SRC
#+BEGIN_SRC dot :file concept-ltl2tgba.svg :var txt=ltl2tgba1 :exports results
......
......@@ -3,6 +3,7 @@
#+DESCRIPTION: Examples showing how to read and write CSV files using Spot's command-line tools.
#+INCLUDE: setup.org
#+HTML_LINK_UP: tools.html
#+PROPERTY: header-args:sh :results verbatim :exports both
This page discusses features available in Spot's command-line
tools to produce an consume CSV files.
......@@ -17,7 +18,7 @@ For instance here is how we could use =genltl= to generate a CSV file
with three columns: the family name of the formula, its parameter, and
the formula itself.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
genltl --and-gf=1..5 --u-left=1..5 --format='%F,%L,%f' > gen.csv
cat gen.csv
#+END_SRC
......@@ -45,7 +46,7 @@ For instance, the following command will translate all the previous
formulas, and show the resulting number of states (=%s=) and edges
(=%e=) of the automaton constructed for each formula.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
genltl --and-gf=1..5 --u-left=1..5 | ltl2tgba --stats '%f,%s,%e'
#+END_SRC
#+RESULTS:
......@@ -66,7 +67,7 @@ If the translated formulas may contain commas, or double quotes, this
simple output may prove difficult to process by other tools. For
instance consider the translation of the following two formulas:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
ltl2tgba -f Xa -f 'G("switch == on" -> F"tab[3,5] < 12")' --stats '%f,%s,%e'
#+END_SRC
#+RESULTS:
......@@ -77,7 +78,7 @@ The second line of this input does no conform to [[https://www.rfc-editor.org/rf
non-escaped fields are not allowed to contain comma or double quotes.
To fix this, simply double-quote the =%f= in the argument to =--stats=:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
ltl2tgba -f Xa -f 'G("switch == on" -> F"tab[3,5] < 12")' --stats '"%f",%s,%e'
#+END_SRC
......@@ -102,7 +103,7 @@ to support the specification of a CSV column. The notation
For instance let's consider the file =gen.csv= built with the first command of
this page. It contains:
#+BEGIN_SRC sh :results verbatim :exports results
#+BEGIN_SRC sh :exports results
cat gen.csv
#+END_SRC
#+RESULTS:
......@@ -122,7 +123,7 @@ u-left,5,(((p1 U p2) U p3) U p4) U p5
We can run =ltl2tgba= on the third column to produce
the same output as in a previous example:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
ltl2tgba -F gen.csv/3 --stats '%f,%s,%e'
#+END_SRC
#+RESULTS:
......@@ -143,7 +144,7 @@ When =ltlfilt= is used on a CSV file, it will preserve the
text before and after the matched formula in the CSV file.
For instance:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
ltlfilt -F gen.csv/3 --size-min=8 --relabel=abc
#+END_SRC
#+RESULTS:
......@@ -162,7 +163,7 @@ string.
For instance this moves the first two columns after the formulas.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
ltlfilt -F gen.csv/3 --size-min=8 --format='"%f",%<'
#+END_SRC
#+RESULTS:
......@@ -190,7 +191,7 @@ Typical uses of =ltlfilt= on CSV file include:
Some CSV files contain a header lines that should not be processed.
For instance the CSV files produced by =ltlcross= have such a line:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
randltl -n 2 a b | ltlfilt --remove-wm |
ltlcross --csv=results.csv 'ltl2tgba -s %f >%N' 'ltl3ba -f %s >%N'
cat results.csv
......@@ -209,7 +210,7 @@ cat results.csv
If we run =ltlfilt= on the first column, it will process the =formula=
header as if it was an LTL formula.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
ltlfilt -F results.csv/1 --format='%f' --unique
#+END_SRC
......@@ -223,7 +224,7 @@ ltlfilt -F results.csv/1 --format='%f' --unique
In such case, the syntax =FILENAME/-COL= (with a minus sign before the
column number) can be used to discard the first line of a CSV file.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
ltlfilt -F results.csv/-1 --format='%f' --unique
#+END_SRC
......@@ -238,7 +239,7 @@ ltlfilt -F results.csv/-1 --format='%f' --unique
The =--stats= option of tools that generate automata can be used to
generate CSV files that embed automata. For instance
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
genltl --dac=1..3 | ltl2tgba --stats='"%f","%e edges","%h"' > csv-aut.csv
cat csv-aut.csv
#+END_SRC
......@@ -258,7 +259,7 @@ syntax we used previously, but by default it will just output the
automata. If you want to preserve the entire line, you should use
=%<= and =%>= in the =--stats= format.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
autfilt csv-aut.csv/3 --states=2..3 --stats='%<,"%h"'
#+END_SRC
......@@ -271,7 +272,7 @@ Another source of automata in CSV format is =ltlcross=. Using options
=--automata= it will record the automata produced by each tool into
the CSV file:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
genltl --dac=1..3 | ltlcross --csv=result.csv --automata ltl2tgba
cat result.csv
#+END_SRC
......
......@@ -3,6 +3,7 @@
#+DESCRIPTION: Spot command-line tool for converting automata into Transition-based Generalized Büchi Automata.
#+INCLUDE: setup.org
#+HTML_LINK_UP: tools.html
#+PROPERTY: header-args:sh :results verbatim :exports both
This tool converts automata into transition-based generalized Büchi
automata, a.k.a., TGBA. It can also produce Büchi automata on request
......@@ -35,85 +36,57 @@ The following command instructs =ltl2dstar= to:
Additionally we use =ltlfilt= to convert our formula to the
prefix format used by =ltl2dstar=.
#+BEGIN_SRC sh :results silent :exports both
#+BEGIN_SRC sh :results silent
ltlfilt -f '(a U b) & GFb' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - fagfb
#+END_SRC
By looking at the file =fagfb= you can see the =ltl2dsar= actually
produced a 4-state DRA:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
cat fagfb
#+END_SRC
#+RESULTS:
#+begin_example
DRA v2 explicit
Comment: "Safra[NBA=3]"
Comment: "DBA2DRA[NBA=3]"
States: 4
Acceptance-Pairs: 1
Start: 2
Start: 1
AP: 2 "a" "b"
---
State: 0
Acc-Sig: +0
3
3
Acc-Sig:
0
0
0
0
State: 1
Acc-Sig: -0
1
1
1
Acc-Sig:
0
1
3
3
State: 2
Acc-Sig:
1
2
0
0
2
3
3
State: 3
Acc-Sig:
Acc-Sig: +0
2
2
3
3
0
0
#+end_example
Let's display this automaton with =autfilt=:
#+NAME: fagfb
#+BEGIN_SRC sh :results verbatim :exports code
#+BEGIN_SRC sh :exports code
autfilt fagfb --dot
#+END_SRC
#+RESULTS: fagfb
#+begin_example
digraph G {
rankdir=LR
label=<Fin(<font color="#5DA5DA">⓿</font>) &amp; Inf(<font color="#F17CB0">❶</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 -> 2
0 [label=<0<br/><font color="#F17CB0">❶</font>>]
0 -> 0 [label=<b>]
0 -> 3 [label=<!b>]
1 [label=<1<br/><font color="#5DA5DA">⓿</font>>]
1 -> 1 [label=<1>]
2 [label=<2>]
2 -> 0 [label=<b>]
2 -> 1 [label=<!a &amp; !b>]
2 -> 2 [label=<a &amp; !b>]
3 [label=<3>]
3 -> 0 [label=<b>]
3 -> 3 [label=<!b>]
}
#+end_example
#+BEGIN_SRC dot :file fagfb.svg :var txt=fagfb :exports results
$txt
#+END_SRC
......@@ -127,31 +100,9 @@ a Monitor, using the same options as [[file:ltl2tgba.org][=ltl2tgba=]].
For instance here is the conversion to a Büchi automaton (=-B=):
#+NAME: fagfb2ba
#+BEGIN_SRC sh :results verbatim :exports code
#+BEGIN_SRC sh :exports code
dstar2tgba -B fagfb -d
#+END_SRC
#+RESULTS: fagfb2ba
#+begin_example
digraph G {
rankdir=LR
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 -> 1
0 [label="0", peripheries=2]
0 -> 0 [label=<b>]
0 -> 2 [label=<!b>]
1 [label="1"]
1 -> 0 [label=<b>]
1 -> 1 [label=<a &amp; !b>]
2 [label="2"]
2 -> 0 [label=<b>]
2 -> 2 [label=<!b>]
}
#+end_example
#+BEGIN_SRC dot :file fagfb2ba.svg :var txt=fagfb2ba :exports results
$txt
......@@ -165,7 +116,7 @@ a complete automaton.
But we could as well require the output as a never claim for Spin (option =-s=):
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
dstar2tgba -s fagfb
#+END_SRC
#+RESULTS:
......@@ -173,18 +124,18 @@ dstar2tgba -s fagfb
never {
T0_init:
if
:: (b) -> goto accept_S0
:: ((a) && (!(b))) -> goto T0_init
:: (b) -> goto accept_S2
fi;
accept_S0:
T0_S1:
if
:: (b) -> goto accept_S0
:: (!(b)) -> goto T0_S2
:: (!(b)) -> goto T0_S1
:: (b) -> goto accept_S2
fi;
T0_S2:
accept_S2:
if
:: (b) -> goto accept_S0
:: (!(b)) -> goto T0_S2
:: (!(b)) -> goto T0_S1
:: (b) -> goto accept_S2
fi;
}
#+end_example
......@@ -197,7 +148,7 @@ T0_S2:
Here is the translation of =GFa | GFb= to a 4-state Streett automaton:
#+NAME: gfafgb
#+BEGIN_SRC sh :results verbatim :exports code
#+BEGIN_SRC sh :exports code
ltlfilt -f 'GFa & GFb' -l | ltl2dstar --automata=streett --ltl2nba=spin:ltl2tgba@-Ds - gfagfb
autfilt --dot gfagfb
#+END_SRC
......@@ -216,42 +167,9 @@ We don't pass any option to =dstar2tgba= because converting to TGBA is
the default:
#+NAME: gfagfb2ba
#+BEGIN_SRC sh :results verbatim :exports code
#+BEGIN_SRC sh :exports code
dstar2tgba gfagfb -d
#+END_SRC
#+RESULTS: gfagfb2ba
#+begin_example
digraph G {
rankdir=LR
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 &amp; b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
0 -> 1 [label=<!a &amp; b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
0 -> 2 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
0 -> 3 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
1 [label="1"]
1 -> 0 [label=<a &amp; b<br/><font color="#F17CB0">❶</font>>]
1 -> 1 [label=<!a &amp; b<br/><font color="#F17CB0">❶</font>>]
1 -> 2 [label=<a &amp; !b<br/><font color="#F17CB0">❶</font>>]
1 -> 3 [label=<!a &amp; !b<br/><font color="#F17CB0">❶</font>>]
2 [label="2"]
2 -> 0 [label=<a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
2 -> 1 [label=<!a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
2 -> 2 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
2 -> 3 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
3 [label="3"]
3 -> 0 [label=<a &amp; b>]
3 -> 1 [label=<!a &amp; b>]
3 -> 2 [label=<a &amp; !b>]
3 -> 3 [label=<!a &amp; !b>]
}
#+end_example
#+BEGIN_SRC dot :file gfagfb2ba.svg :var txt=gfagfb2ba :exports results
$txt
......@@ -260,8 +178,8 @@ $txt
[[file:gfagfb2ba.svg]]
Obviously the resulting automaton could be simplified further, as the
minimal TGBA for this formula has a single state. (Patches
welcome...)
minimal TGBA for this formula has a single state. (This will be fixed
in Spot 2.8.)
* Details
......@@ -285,7 +203,7 @@ The last two steps are shared with =ltl2tgba= and use the same options.
The type of automaton to produce can be selected using the =-B= or =-M=
switches:
#+BEGIN_SRC sh :results verbatim :exports results
#+BEGIN_SRC sh :exports results
dstar2tgba --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d'
#+END_SRC
......@@ -301,7 +219,7 @@ dstar2tgba --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d'
And these may be refined by a simplification goal, should the
post-processor routine had a choice to make:
#+BEGIN_SRC sh :results verbatim :exports results
#+BEGIN_SRC sh :exports results
dstar2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
......@@ -313,7 +231,7 @@ dstar2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d'
The effort put into post-processing can be limited with the =--low= or
=--medium= options:
#+BEGIN_SRC sh :results verbatim :exports results
#+BEGIN_SRC sh :exports results
dstar2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
......@@ -326,7 +244,7 @@ should you find =dstar2tgba= too slow.
Finally, the output format can be changed with the following
[[file:oaut.org][common ouput options]]:
#+BEGIN_SRC sh :results verbatim :exports results
#+BEGIN_SRC sh :exports results
dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
......@@ -395,7 +313,7 @@ of the input (Rabin) automaton, =%s=, the number of states of the
output (Büchi) automaton, =%d=, whether the output automaton is
deterministic, and =%p= whether the automaton is complete.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh
randltl -n -1 --tree-size=10..14 a b c |
ltlfilt --remove-wm -r -u --size-min=3 -n 10 |
while read f; do
......@@ -410,20 +328,20 @@ done
#+begin_example
(b | Fa) R Fc
DRA: 9st.; BA: 9st.; det.? 1; complete? 1
Ga U (Gc R (!a | Gc))
Ga U G(!a | Gc)
DRA: 7st.; BA: 7st.; det.? 0; complete? 0
GFc
DRA: 3st.; BA: 3st.; det.? 1; complete? 1
DRA: 2st.; BA: 2st.; 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
Xc R G(b | G!c)
DRA: 3st.; BA: 2st.; det.? 1; complete? 0
c & G(b | F(a & c))
DRA: 4st.; 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
DRA: 4st.; 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
......
......@@ -3,13 +3,14 @@
#+DESCRIPTION: Spot command-line tool that generates ω-automata from known patterns
#+INCLUDE: setup.org
#+HTML_LINK_UP: tools.html
#+PROPERTY: header-args:sh :results verbatim :exports both
This tool outputs ω-automata generated from scalable patterns.
These patterns are usually taken from the literature (see the
[[./man/genaut.1.html][=genaut=]](1) man page for references).
#+BEGIN_SRC sh :results verbatim :exports results
#+BEGIN_SRC sh :exports results
genaut --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d'
#+END_SRC
......@@ -19,9 +20,9 @@ genaut --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d'
: has at least 2^N/(2N+1) states.
: --l-dsa=RANGE A deterministic Streett automaton with 4N states
: with no equivalent deterministic Rabin automaton
: of less than n! states.
: of less than N! states.
: --l-nba=RANGE A Büchi automaton with 3N+1 states whose
: complementary Streett automaton needs at least n!
: complementary Streett automaton needs at least N!
: states.
......@@ -30,7 +31,7 @@ By default, the output format is [[file:hoa.org][HOA]], but this can be controll
For instance:
#+NAME: kscobuchi2
#+BEGIN_SRC sh :results verbatim :exports code
#+BEGIN_SRC sh :exports code
genaut --ks-nca=2 --dot
#+END_SRC
......
This diff is collapsed.
This diff is collapsed.
......@@ -2,6 +2,7 @@
#+DESCRIPTION: Details about support of the HOA format in Spot
#+INCLUDE: setup.org
#+HTML_LINK_UP: tools.html
#+PROPERTY: header-args:sh :results verbatim :exports both
The [[http://adl.github.io/hoaf/][Hanoi Omega-Automa format]] is a textual representation of
......@@ -150,7 +151,7 @@ EOF
#+RESULTS:
#+BEGIN_SRC sh :results verbatim :exports results :wrap SRC hoa
#+BEGIN_SRC sh :exports results :wrap SRC hoa
sed -n '/--BODY/,/--END/p' stvstracc.hoa | grep -v -- --
#+END_SRC
......@@ -173,7 +174,7 @@ State: 2
will always be stored as a TωA with this transition structure:
#+BEGIN_SRC sh :results verbatim :exports results :wrap SRC hoa
#+BEGIN_SRC sh :exports results :wrap SRC hoa
autfilt -Ht stvstracc.hoa | sed -n '/--BODY/,/--END/p' | grep -v -- --
#+END_SRC
......@@ -208,7 +209,7 @@ For instance in the following automaton, the outgoing transitions of
each states belong to the same sets:
#+NAME: state-based-example
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
#+BEGIN_SRC sh :wrap SRC hoa
cat >sba.hoa <<EOF_HOA
HOA: v1
States: 3
......@@ -272,7 +273,7 @@ Nevertheless, should you really insist on having an output with
transition-based acceptance, you can do so by passing the option =t=
to the HOA printer:
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
#+BEGIN_SRC sh :wrap SRC hoa
autfilt -Ht sba.hoa
#+END_SRC
......@@ -305,7 +306,7 @@ format to prevents mixing the two: if you use =-Hm=, the decision of
using state or transition-based acceptance will be made for each state
separately. For instance:
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
#+BEGIN_SRC sh :wrap SRC hoa
ltl2tgba -Hm 'GFa | Fb'
#+END_SRC
......@@ -345,7 +346,7 @@ when necessary. Most tools have a =-S= option (or
=--state-based-acceptance=) for this purpose. Compare the following
output with the previous one.
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
#+BEGIN_SRC sh :wrap SRC hoa
ltl2tgba -S -Hm 'GFa | Fb'
#+END_SRC
......@@ -434,7 +435,7 @@ In the following example, you can see =autfilt= removing the duplicate
Rabin pair, and reordering the remaining pair to fit the syntax
corresponding to =Rabin 1=.
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
#+BEGIN_SRC sh :wrap SRC hoa
autfilt <<EOF
HOA: v1
States: 3
......@@ -501,7 +502,7 @@ When you look at an acceptance condition output by Spot, you can
actually spot the terms that have been grouped together internally by
looking at the spacing around operators =&= and =|=. For instance:
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa