Commit e6e416e1 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

document autfilt and randaut

* NEWS: Mention these tools.
* doc/org/autfilt.org, doc/org/randaut.org: New files.
* doc/org/tools.org, doc/Makefile.am: Add them.
parent c5842c3a
......@@ -7,7 +7,7 @@ New in spot 1.99a (not yet released)
already installed on the system.
- ltlgrind is a new tool that mutates LTL or PSL formulas. If you
have a tool that is bogus on some formula that is tool large to
have a tool that is bogus on some formula that is too large to
debug, you can use ltlgrind to generate smaller derived formulas
and see if you can reproduce the bug on those.
......@@ -15,6 +15,11 @@ New in spot 1.99a (not yet released)
size of any bogus formula it discovers, while still exhibiting
the bug.
- randaut is a new tool that generates random automata.
- autfilt is a new tool that converts/filters/transforms a
stream of automata.
- "ltlfilt --stutter-invariant" will now work with PSL formula.
The implementation is actually much more efficient
than the previous implementation that was only for LTL.
......
## -*- coding: utf-8 -*-
## Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et
## Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et
## Développement de l'Epita (LRDE).
## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
......@@ -60,6 +60,7 @@ ORG_FILES = \
org/.dir-locals.el \
org/init.el.in \
org/syntax.css \
org/autfilt.org \
org/csv.org \
org/dstar2tgba.org \
org/genltl.org \
......@@ -68,6 +69,8 @@ ORG_FILES = \
org/ltl2tgta.org \
org/ltlcross.org \
org/ltlfilt.org \
org/ltlgrind.org \
org/randaut.org \
org/randltl.org \
org/tools.org \
org/satmin.org \
......
#+TITLE: =autfilt=
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
The =autfilt= tool can filter, transform, and convert a stream of automata.
* Conversion between formats
=autfilt= reads automata in the [[http://adl.github.io/hoaf/][Hanoi Omega Automata Format]]. The
output format can be controlled using the =--spin=, =--lbtt=, =--dot=,
or =--hoaf= options.
#+BEGIN_SRC sh :results verbatim :exports both
cat >example.hoa <<EOF
HOA: v1
States: 1
Start: 0
AP: 1 "p0"
Acceptance: 1 Inf(0)
--BODY--
State: 0
[0] 0 {0}
[!0] 0
--END--
EOF
autfilt example.hoa --dot
#+END_SRC
#+RESULTS:
: digraph G {
: 0 [label="", style=invis, height=0]
: 0 -> 1
: 1 [label="0"]
: 1 -> 1 [label="p0\n{0}"]
: 1 -> 1 [label="!p0"]
: }
The =--spin= options implicitly requires a degeneralization:
#+BEGIN_SRC sh :results verbatim :exports both
autfilt example.hoa --spin
#+END_SRC
#+RESULTS:
#+begin_example
never {
accept_init:
if
:: ((p0)) -> goto accept_init
:: ((!(p0))) -> goto T0_S2
fi;
T0_S2:
if
:: ((p0)) -> goto accept_init
:: ((!(p0))) -> goto T0_S2
fi;
}
#+end_example
#+BEGIN_SRC sh :results verbatim :exports both
autfilt example.hoa --lbtt
#+END_SRC
#+RESULTS:
: 1 1t
: 0 1
: 0 0 -1 p0
: 0 -1 ! p0
: -1
* Displaying statistics
One special output format of =autfilt= is the statistic output. For
instance the following command calls [[file:randaut.org][=randaut=]] to generate 10 random
automata, and pipe the result into =autfilt= to display various
statistics.
#+BEGIN_SRC sh :results verbatim :exports both
randaut --hoa -n 10 -A0..2 -S10..20 -d0.05 2 |
autfilt --stats='%s states, %e edges, %a acc-sets, %c SCCs, det=%d'
#+END_SRC
#+RESULTS:
#+begin_example
16 states, 27 edges, 1 acc-sets, 2 SCCs, det=0
12 states, 20 edges, 1 acc-sets, 2 SCCs, det=0
11 states, 15 edges, 0 acc-sets, 4 SCCs, det=1
16 states, 29 edges, 0 acc-sets, 2 SCCs, det=0
15 states, 30 edges, 2 acc-sets, 1 SCCs, det=0
11 states, 17 edges, 1 acc-sets, 2 SCCs, det=0
11 states, 16 edges, 1 acc-sets, 1 SCCs, det=1
17 states, 28 edges, 1 acc-sets, 1 SCCs, det=0
19 states, 36 edges, 0 acc-sets, 3 SCCs, det=0
11 states, 16 edges, 2 acc-sets, 6 SCCs, det=0
#+end_example
The following =%= sequences are available:
#+BEGIN_SRC sh :results verbatim :exports results
autfilt --help | sed -n '/^ %%/,/^$/p' | sed '$d'
#+END_SRC
#+RESULTS:
#+begin_example
%% a single %
%A, %a number of acceptance pairs or sets
%C, %c number of SCCs
%d 1 if the output is deterministic, 0 otherwise
%E, %e number of edges
%F name of the input file
%n number of nondeterministic states in output
%p 1 if the output is complete, 0 otherwise
%r conversion time (including post-processings, but
not parsing) in seconds
%S, %s number of states
%T, %t number of transitions
#+end_example
When a letter is available both as uppercase and lowercase, the
uppercase version refer to the input automaton, while the lowercase
refer to the output automaton. Of course this distinction makes sense
only if =autfilt= was instructed to perform an operation on the input
automaton.
* Simplifying automata
The standard set of automata simplification routines (these are often
referred to as the "post-processing" routines, because these are the
procedures performed by [[file:ltl2tgba.org][=ltl2tgba=]] after translating a formula into a
TGBA) are available through the following options.
This set of options controls the desired type of output automaton:
#+BEGIN_SRC sh :results verbatim :exports results
autfilt --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
: -B, --ba Büchi Automaton
: -M, --monitor Monitor (accepts all finite prefixes of the given
: property)
: --tgba Transition-based Generalized Büchi Automaton
: (default)
These options specifies desired properties:
#+BEGIN_SRC sh :results verbatim :exports results
autfilt --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
: -a, --any no preference (default)
: -C, --complete output a complete automaton (combine with other
: intents)
: -D, --deterministic prefer deterministic automata
: --small prefer small automata
Finally, the following switches control the amount of effort applied
to reach the desired properties:
#+BEGIN_SRC sh :results verbatim :exports results
autfilt --help | sed -n '/Optimization level:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
: --high all available optimizations (slow)
: --low minimal optimizations (fast, default)
: --medium moderate optimizations
#+TITLE: =randaut=
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
The =randaut= tool generates random (connected) automata.
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.
#+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"]
}
#+end_example
#+BEGIN_SRC dot :file randaut1.png :cmdline -Tpng :var txt=randaut1 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:randaut1.png]]
As for [[file:randltl.org][=randltl=]], you can supply a number of atomic propositions
instead of giving a list of atomic propositions.
* States and density
The numbers of states can be controlled using the =-S= option. This
option will accept a range as argument, so for instance =-S3..6= will
generate an automaton with 3 to 6 states.
The number of edges can be controlled using the =-d= (or
=--density=) option. The argument should be a number between 0 and 1.
In an automaton with $S$ states and density $d$, the degree of each
state will follow a normal distribution with mean $1+(S-1)d$ and
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.
#+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"]
}
#+end_example
#+BEGIN_SRC dot :file randaut2.png :cmdline -Tpng :var txt=randaut2 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:randaut2.png]]
#+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"]
}
#+end_example
#+BEGIN_SRC dot :file randaut3.png :cmdline -Tpng :var txt=randaut3 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:randaut3.png]]
* Acceptance sets
The generation of acceptance sets is controlled with the following three parameters:
- =-A= (or =--acc-sets=) controls the number of acceptance sets.
This can be given as a range (e.g. =-A1..3=) in case you want this
number to be picked at random in the range.
- =-a= (or =--acc-probability=) controls the probability that any
transition belong to a given acceptance set.
- =--state-acc= requests that the automaton use state-based
acceptance. In this case, =-a= is the probability that a /state/
belong to the acceptance set. (Because Spot only deals with
transition-based acceptance internally, this options force all
transitions leaving a state to belong to the same acceptance sets.
But if the output format allows state-acceptance, it will be used.)
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/\\/\\\\/'
#+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"]
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"]
}
#+end_example
#+BEGIN_SRC dot :file randaut4.png :cmdline -Tpng :var txt=randaut4 :exports results
$txt
#+END_SRC
#+RESULTS:
[[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/\\/\\\\/'
#+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}"]
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"]
}
#+end_example
#+BEGIN_SRC dot :file randaut5.png :cmdline -Tpng :var txt=randaut5 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:randaut5.png]]
* Determinism
The output can only contain a single edge between two given states.
By default, the label of this edge is a random assignment of all
atomic propositions. Two edges leaving the same state may therefore
have the same label.
If the =-D= (or =--deterministic=) option is supplied, the labels
are generated differently: once the degree $m$ of a state has been
decided, the algorithm will compute a set of $m$ disjoint
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.
#+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"]
}
#+end_example
#+BEGIN_SRC dot :file randaut6.png :cmdline -Tpng :var txt=randaut6 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:randaut6.png]]
Note that in a deterministic automaton with $a$ atomic propositions,
it is not possible to have states with more than $2^a$ successors. If
the combination of =-d= and =-S= allows the situation where a state
can have more than $2^a$ successors, the degree will be clipped to
$2^a$. When working with random deterministic automata over $a$
atomic propositions, we suggest you always request more than $2^a$
states.
* Output formats
The output format can be controlled using =--hoaf=, =--dot==,
=--lbtt=, and =--spin=. Note that =--spin= automatically implies
=--ba=.
* Generating a stream of automata
Use option =-n= to specify a number of automata to build. A negative
value will cause an infinite number of automata to be produced. This
generation of multiple automata is probably useful only with =--hoaf=,
when piped to another tool that can read this format and process
automata in batches.
......@@ -36,7 +36,7 @@ corresponding commands are hidden.
* Command-line tools
- [[file:randltl.org][=randltl=]] Generate random LTL/PSL formulas.
- [[file:ltlfilt.org][=ltlfilt=]] Filter LTL/PSL formulas.
- [[file:ltlfilt.org][=ltlfilt=]] Filter and convert LTL/PSL formulas.
- [[file:genltl.org][=genltl=]] Generate LTL formulas from scalable patterns.
- [[file:ltl2tgba.org][=ltl2tgba=]] Translate LTL/PSL formulas into Büchi automata.
- [[file:ltl2tgta.org][=ltl2tgta=]] Translate LTL/PSL formulas into Testing automata.
......@@ -45,8 +45,10 @@ corresponding commands are hidden.
Büchi automata.
- [[file:ltlgrind.org][=ltlgrind=]] List formulas similar to but simpler than a given LTL/PSL
formula
- [[file:randaut.org][=randaut=]] Generate random automata.
- [[file:autfilt.org][=autfilt=]] Filter and convert automata.
* Advanced uses
* Advanced use-cases
- [[file:csv.org][Reading and writing CSV files]]
- [[file:satmin.org][SAT-based minimization of Deterministic (Generalized) Büchi automata]]
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment