242 lines
8.3 KiB
Org Mode
242 lines
8.3 KiB
Org Mode
# -*- coding: utf-8 -*-
|
|
#+TITLE: =autfilt=
|
|
#+SETUPFILE: setup.org
|
|
#+HTML_LINK_UP: tools.html
|
|
|
|
The =autfilt= tool can filter, transform, and convert a stream of automata.
|
|
|
|
The tool operates a loop over 5 phases:
|
|
- input one automaton
|
|
- optionally preprocess the automaton
|
|
- optionally filter the automaton (i.e., decide whether to ignore the
|
|
automaton or continue with it)
|
|
- optionally postprocess the automaton
|
|
- output the automaton
|
|
|
|
The simplest way to use the tool is simply to use it for input and
|
|
output (i.e., format conversion) without any transformation and
|
|
filtering.
|
|
|
|
* Conversion between formats
|
|
|
|
=autfilt= can read automata written in the [[http://adl.github.io/hoaf/][Hanoi Omega Automata
|
|
Format]], as [[http://spinroot.com/spin/Man/never.html][Spin never claims]], or using [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT's format]]. Automata in
|
|
those formats (even a mix of those formats) can be concatenated in the
|
|
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
|
|
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.
|
|
|
|
|
|
* Filtering automata
|
|
|
|
=autfilt= supports multiple ways to filter automata based on different
|
|
characteristics of the automaton.
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports results
|
|
autfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d'
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
#+begin_example
|
|
--acc-sets=RANGE keep automata whose number of acceptance sets are
|
|
in RANGE
|
|
--are-isomorphic=FILENAME keep automata that are isomorphic to the
|
|
automaton in FILENAME
|
|
--edges=RANGE keep automata whose number of edges are in RANGE
|
|
--intersect=FILENAME keep automata whose languages have an non-empty
|
|
intersection with the automaton from FILENAME
|
|
--is-complete keep complete automata
|
|
--is-deterministic keep deterministic automata
|
|
--is-empty keep automata with an empty language
|
|
--states=RANGE keep automata whose number of states are in RANGE
|
|
-u, --unique do not output the same automaton twice (same in
|
|
the sense that they are isomorphic)
|
|
-v, --invert-match select non-matching automata
|
|
#+end_example
|
|
|
|
For instance =--states=2..5 --acc-sets=3= will /keep/ only automata that
|
|
use 3 acceptance sets, and that have between 2 and 5 states.
|
|
|
|
Except for =--unique=, all these filters can be inverted. Using
|
|
=--states=2..5 --acc-sets=3 -v= will /drop/ all automata that use 3
|
|
acceptance sets and that have between 2 and 5 states, and keep the
|
|
others.
|
|
|
|
* 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
|
|
|
|
|
|
By default, =--any --low= is used, which cause all simplifications to
|
|
be skipped. If you want to reduce the size of the automaton, try
|
|
=--small --high= and if you want to try to make it deterministic
|
|
(their is to guaranty of result, this is only a preference), try
|
|
=--deterministic --high=.
|
|
|
|
* Transformations
|
|
|
|
The following transformations are available:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports results
|
|
autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d'
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
: --destut allow less stuttering
|
|
: --instut[=1|2] allow more stuttering (two possible algorithms)
|
|
: --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)
|