alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

org: more documentation

Browse source 
* doc/org/oaut.org: Mention --dot=a.
* doc/org/autfilt.org: Update list of transformations.
This commit is contained in:
Alexandre Duret-Lutz 2015-02-26 11:56:19 +01:00
parent af1d05fd13
commit b321a410d5
2 changed files with 50 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

33
doc/org/autfilt.org
View file

@ -231,12 +231,27 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: --destut allow less stuttering #+begin_example
: --instut[=1|2] allow more stuttering (two possible algorithms) --cleanup-acceptance remove unused acceptance sets from the automaton
: --mask-acc=NUM[,NUM...] remove all transitions in specified acceptance --complement-acceptance complement the acceptance condition (without
: sets touching the automaton)
: --merge-transitions merge transitions with same destination and --destut allow less stuttering
: acceptance --dnf-acceptance put the acceptance condition in Disjunctive Normal
: --product=FILENAME build the product with the automaton in FILENAME Form
: --randomize[=s|t] randomize states and transitions (specify 's' or --instut[=1|2] allow more stuttering (two possible algorithms)
: 't' to randomize only states or transitions) --keep-states=NUM[,NUM...] only keep specified states. The first state
will be the new initial state
--mask-acc=NUM[,NUM...] remove all transitions in specified acceptance
sets
--merge-transitions merge transitions with same destination and
acceptance
--product=FILENAME build the product with the automaton in FILENAME
--randomize[=s|t] randomize states and transitions (specify 's' or
't' to randomize only states or transitions)
--remove-fin rewrite the automaton without using Fin acceptance
--state-based-acceptance, --sbacc
define the acceptance using states
--strip-acceptance remove the acceptance condition and all acceptance
sets
#+end_example

42
doc/org/oaut.org
View file

@ -18,17 +18,18 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
#+begin_example #+begin_example
-8, --utf8 enable UTF-8 characters in output (ignored with -8, --utf8 enable UTF-8 characters in output (ignored with
--lbtt or --spin) --lbtt or --spin)
--dot[=c|h|n|N|s|t|v] GraphViz's format (default). Add letters to chose --dot[=c|h|n|N|s|t|v] GraphViz's format (default). Add letters for (a)
(c) circular nodes, (h) horizontal layout, (v) acceptance display, (c) circular nodes, (h)
vertical layout, (n) with name, (N) without name, horizontal layout, (v) vertical layout, (n) with
(s) with SCCs, (t) always transition-based name, (N) without name, (s) with SCCs, (t) force
acceptance. transition-based acceptance.
-H, --hoaf[=s|t|m|l] Output the automaton in HOA format. Add letters -H, --hoaf[=s|t|m|l] Output the automaton in HOA format. Add letters
to select (s) state-based acceptance, (t) to select (s) prefer state-based acceptance when
transition-based acceptance, (m) mixed acceptance, possible [default], (t) force transition-based
(l) single-line output acceptance, (m) mix state and transition-based
acceptance, (l) single-line output
--lbtt[=t] LBTT's format (add =t to force transition-based --lbtt[=t] LBTT's format (add =t to force transition-based
acceptance even on Büchi automata) acceptance even on Büchi automata)
--name=FORMAT set the name of the output automaton --name=FORMAT set the name of the output automaton
-o, --output=FORMAT send output to a file named FORMAT instead of -o, --output=FORMAT send output to a file named FORMAT instead of
standard output. The first automaton sent to a standard output. The first automaton sent to a
@ -270,7 +271,7 @@ $txt
#+RESULTS: #+RESULTS:
[[file:hoafex.png]] [[file:hoafex.png]]
The [[http://adl.github.io/hoaf/][HOA format]] support both state and transition-based acceptance. The [[http://adl.github.io/hoaf/][HOA format]] supports both state and transition-based acceptance.
Although Spot works only with transition-based acceptance, its output Although Spot works only with transition-based acceptance, its output
routines default to state-based acceptance whenever possible (this is routines default to state-based acceptance whenever possible (this is
the case in the first of these two automata) and use transition-based the case in the first of these two automata) and use transition-based
@ -530,30 +531,35 @@ $txt
This output can be customized by passing optional characters to the This output can be customized by passing optional characters to the
=--dot= option. For instance =v= requests a vertical layout (instead =--dot= option. For instance =v= requests a vertical layout (instead
of the default horizontal layout), =c= requests circle states, =s= of the default horizontal layout), =c= requests circle states, =s=
causes strongly-connected components to be displayed, and =n= causes causes strongly-connected components to be displayed, =n= causes the
the name (see below) of the automaton to be displayed. name (see below) of the automaton to be displayed, and =a= causes the
acceptance condition to be shown as well.
#+BEGIN_SRC sh :results verbatim :exports code #+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba --dot=vcsn '(Ga -> Gb) W c' ltl2tgba --dot=vcsna '(Ga -> Gb) W c'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
digraph G { digraph G {
label="(Gb | F!a) W c" label="(Gb | F!a) W c\nInf(0)"
labelloc="t" labelloc="t"
node [shape="circle"] node [shape="circle"]
I [label="", style=invis, height=0] I [label="", style=invis, height=0]
I -> 1 I -> 1
subgraph cluster_0 { subgraph cluster_0 {
label=""
0 [label="0"] 0 [label="0"]
} }
subgraph cluster_1 { subgraph cluster_1 {
label=""
3 [label="3"] 3 [label="3"]
} }
subgraph cluster_2 { subgraph cluster_2 {
label=""
4 [label="4"] 4 [label="4"]
} }
subgraph cluster_3 { subgraph cluster_3 {
label=""
1 [label="1"] 1 [label="1"]
2 [label="2"] 2 [label="2"]
} }
@ -574,13 +580,13 @@ digraph G {
#+NAME: oaut-dot2 #+NAME: oaut-dot2
#+BEGIN_SRC sh :results verbatim :exports none #+BEGIN_SRC sh :results verbatim :exports none
ltl2tgba --dot=vcsn '(Ga -> Gb) W c' | sed 's/\\/\\\\/' ltl2tgba --dot=vcsna '(Ga -> Gb) W c' | sed 's/\\/\\\\/'
#+END_SRC #+END_SRC
#+RESULTS: oaut-dot2 #+RESULTS: oaut-dot2
#+begin_example #+begin_example
digraph G { digraph G {
label="(Gb | F!a) W c" label="(Gb | F!a) W c\\nInf(0)"
labelloc="t" labelloc="t"
node [shape="circle"] node [shape="circle"]
I [label="", style=invis, height=0] I [label="", style=invis, height=0]
@ -624,6 +630,10 @@ $txt
#+RESULTS: #+RESULTS:
[[file:oaut-dot2.png]] [[file:oaut-dot2.png]]
The acceptance condition is displayed in the same way as in the [[http://adl.github.io/hoaf/][HOA
format]]. Here =Inf(0)= means that runs are accepting if and only if
they visit some the transitions in the set #0 infinitely often.
* Statistics * Statistics
The =--stats= option takes format string parameter to specify what and The =--stats= option takes format string parameter to specify what and