org: more typos and small fixups
* doc/org/autfilt.org, doc/org/compile.org, doc/org/concepts.org, doc/org/csv.org, doc/org/ltl2tgba.org, doc/org/oaut.org: Here. * tools/help2man: Adjust regex for optional arguments.
This commit is contained in:
Alexandre Duret-Lutz
parent
ce7b9c5161
commit
2b4cf8e7cb
7 changed files with 106 additions and 57 deletions
|
|
@ -30,7 +30,7 @@ automaton in LBTT's format may not follow an automaton in
|
|||
|
||||
By default the output uses the HOA format. This can be changed using
|
||||
[[file:oaut.org][the common output options]] like =--spin=, =--lbtt=, =--dot=,
|
||||
=--hoaf=...
|
||||
=--stats=...
|
||||
|
||||
#+BEGIN_SRC sh :results silent :exports both
|
||||
cat >example.hoa <<EOF
|
||||
|
|
@ -63,7 +63,7 @@ SPOT_DOTEXTRA= autfilt example.hoa --dot=
|
|||
: 0 -> 0 [label="!p0"]
|
||||
: }
|
||||
|
||||
The =--spin= options implicitly requires a degeneralization:
|
||||
The =--spin= option implicitly requires a degeneralization:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
autfilt example.hoa --spin
|
||||
|
|
@ -85,6 +85,8 @@ T0_S2:
|
|||
}
|
||||
#+end_example
|
||||
|
||||
Option =--lbtt= only works for Büchi or generalized Büchi acceptance.
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
autfilt example.hoa --lbtt
|
||||
#+END_SRC
|
||||
|
|
@ -154,49 +156,78 @@ automaton.
|
|||
|
||||
* Filtering automata
|
||||
|
||||
=autfilt= supports multiple ways to filter automata based on different
|
||||
characteristics of the automaton.
|
||||
=autfilt= offers multiple options 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
|
||||
--acc-sccs=RANGE, --accepting-sccs=RANGE
|
||||
keep automata whose number of non-trivial
|
||||
accepting SCCs is in RANGE
|
||||
--acc-sets=RANGE keep automata whose number of acceptance sets is
|
||||
in RANGE
|
||||
--accept-word=WORD keep automata that accept WORD
|
||||
--ap=RANGE match automata with a number of atomic
|
||||
--ap=RANGE match automata with a number of (declared) atomic
|
||||
propositions 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
|
||||
--edges=RANGE keep automata whose number of edges is in RANGE
|
||||
--equivalent-to=FILENAME keep automata thare are equivalent
|
||||
(language-wise) to the automaton in FILENAME
|
||||
--included-in=FILENAME keep automata whose languages are included in that
|
||||
of the automaton from FILENAME
|
||||
--inherently-weak-sccs=RANGE
|
||||
keep automata whose number of accepting
|
||||
inherently-weak SCCs is in RANGE. An accepting
|
||||
SCC is inherently weak if it does not have a
|
||||
rejecting cycle.
|
||||
--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
|
||||
--is-inherently-weak keep only inherently weak automata
|
||||
--is-stutter-invariant keep automata representing stutter-invariant
|
||||
properties
|
||||
--is-terminal keep only terminal automata
|
||||
--is-unambiguous keep only unambiguous automata
|
||||
--is-weak keep only weak automata
|
||||
--nondet-states=RANGE keep automata whose number of nondeterministic
|
||||
states is in RANGE
|
||||
--rej-sccs=RANGE, --rejecting-sccs=RANGE
|
||||
keep automata whose number of non-trivial
|
||||
rejecting SCCs is in RANGE
|
||||
--reject-word=WORD keep automata that reject WORD
|
||||
--states=RANGE keep automata whose number of states are in RANGE
|
||||
--sccs=RANGE keep automata whose number of SCCs is in RANGE
|
||||
--states=RANGE keep automata whose number of states is in RANGE
|
||||
--terminal-sccs=RANGE keep automata whose number of accepting terminal
|
||||
SCCs is in RANGE. Terminal SCCs are weak and
|
||||
complete.
|
||||
--triv-sccs=RANGE, --trivial-sccs=RANGE
|
||||
keep automata whose number of trivial SCCs is in
|
||||
RANGE
|
||||
--unused-ap=RANGE match automata with a number of declared, but
|
||||
unused atomic propositions in RANGE
|
||||
--used-ap=RANGE match automata with a number of used atomic
|
||||
propositions 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
|
||||
--weak-sccs=RANGE keep automata whose number of accepting weak SCCs
|
||||
is in RANGE. In a weak SCC, all transitions
|
||||
belong to the same acceptance sets.
|
||||
#+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.
|
||||
Except for =--unique=, all these filters can be inverted using option
|
||||
=-v=. 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
|
||||
|
||||
|
|
@ -321,6 +352,17 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d'
|
|||
be true at the same time. Use this option
|
||||
multiple times to declare independent groups of
|
||||
exclusive propositions.
|
||||
--generalized-rabin[=unique-inf|share-inf], --gra[=unique-inf|share-inf]
|
||||
rewrite the acceptance condition as generalized
|
||||
Rabin; the default "unique-inf" option uses the
|
||||
generalized Rabin definition from the HOA format;
|
||||
the "share-inf" option allows clauses to share Inf
|
||||
sets, therefore reducing the number of sets
|
||||
--generalized-streett[=unique-fin|share-fin], --gsa[=unique-fin|share-fin] rewrite the
|
||||
acceptance condition as generalized Streett; the
|
||||
"share-fin" option allows clauses to share Fin
|
||||
sets, therefore reducing the number of sets; the
|
||||
default "unique-fin" does not
|
||||
--instut[=1|2] allow more stuttering (two possible algorithms)
|
||||
--keep-states=NUM[,NUM...] only keep specified states. The first state
|
||||
will be the new initial state. Implies
|
||||
|
|
@ -346,8 +388,10 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d'
|
|||
--remove-unreachable-states
|
||||
remove states that are unreachable from the
|
||||
initial state
|
||||
--remove-unused-ap remove declared atomic propositions that are not
|
||||
used
|
||||
--sat-minimize[=options] minimize the automaton using a SAT solver
|
||||
(only work for deterministic automata)
|
||||
(only works for deterministic automata)
|
||||
--separate-sets if both Inf(x) and Fin(x) appear in the acceptance
|
||||
condition, replace Fin(x) by a new Fin(y) and
|
||||
adjust the automaton
|
||||
|
|
|
|||
|
|
@ -39,8 +39,10 @@ obvisously. On this page, we are going to assume that you use =g++=
|
|||
same user interface. To successfully build the =hello= program, we
|
||||
might need to tell the compiler several things:
|
||||
|
||||
1. The language that we use is C++11 (or C++14). This usually requires
|
||||
passing an option like =-std=c++11=.
|
||||
1. The language that we use is C++11 (or C++14). This usually
|
||||
requires passing an option like =-std=c++11=. Note that with
|
||||
version 6 of =g++= the default is now to compile C++14, so this
|
||||
option is not necessary.
|
||||
2. The C++ preprocessor should be able to find =spot/misc/version.hh=.
|
||||
This might require appending another directory to the include
|
||||
search path with =-I location=.
|
||||
|
|
|
|||
|
|
@ -1045,13 +1045,13 @@ method.
|
|||
Here is a list of named properties currently used inside Spot:
|
||||
|
||||
| key name | (pointed) value type | description |
|
||||
|---------------------+--------------------------------+-----------------------------------------------------------------------------------------------------------------------------------|
|
||||
| ~automaton-name~ | ~std::string~ | A name for the automaton, for instance to display in the HOA format. |
|
||||
| ~product-states~ | ~const spot::product_states~ | A vector of pair of states giving the left and right operand of each state in a product automaton. |
|
||||
| ~state-names~ | ~std::vector<std::string>~ | A vector naming each state of the automaton, for display purpose. |
|
||||
| ~highlight-edges~ | ~std::map<unsigned, unsigned>~ | A map of (edge number, color number) for highlighting the output. |
|
||||
| ~highlight-states~ | ~std::map<unsigned, unsigned>~ | A map of (state number, color number) for highlighting the output. |
|
||||
| ~incomplete-states~ | ~std::set<unsigned>~ | A set of states numbers that should be displayed as incomplete. Used internally by ~print_dot()~ when truncating large automata. |
|
||||
|---------------------+--------------------------------+---------------------------------------------------------------------------------------------------------------------------------|
|
||||
| ~automaton-name~ | ~std::string~ | name for the automaton, for instance to display in the HOA format |
|
||||
| ~product-states~ | ~const spot::product_states~ | vector of pairs of states giving the left and right operands of each state in a product automaton |
|
||||
| ~state-names~ | ~std::vector<std::string>~ | vector naming each state of the automaton, for display purpose |
|
||||
| ~highlight-edges~ | ~std::map<unsigned, unsigned>~ | map of (edge number, color number) for highlighting the output |
|
||||
| ~highlight-states~ | ~std::map<unsigned, unsigned>~ | map of (state number, color number) for highlighting the output |
|
||||
| ~incomplete-states~ | ~std::set<unsigned>~ | set of states numbers that should be displayed as incomplete (used internally by ~print_dot()~ when truncating large automata) |
|
||||
|
||||
Objects referenced via named properties are automatically destroyed
|
||||
when the automaton is destroyed, but this can be altered by passing a
|
||||
|
|
|
|||
|
|
@ -35,10 +35,10 @@ u-left,4,((p1 U p2) U p3) U p4
|
|||
u-left,5,(((p1 U p2) U p3) U p4) U p5
|
||||
#+end_example
|
||||
|
||||
Tools that produce automata (like [[file:ltl2tgba.org][=ltl2tgba=]], or [[file:dstar2tgba.org][=dstar2tgba=]]) have a
|
||||
=--stats= option that can be used to output various statistics about
|
||||
the constructed automaton (these statistics are shown *instead* of
|
||||
printing the automaton).
|
||||
Tools that produce automata (like [[file:ltl2tgba.org][=ltl2tgba=]], [[file:dstar2tgba.org][=dstar2tgba=]], [[file:autfilt.org][=autfilt=]],
|
||||
or [[file:randaut.org][=randaut=]]) have a =--stats= option that can be used to output
|
||||
various statistics about the constructed automaton (these statistics
|
||||
are shown *instead* of printing the automaton).
|
||||
|
||||
For instance, the following command will translate all the previous
|
||||
formulas, and show the resulting number of states (=%s=) and edges
|
||||
|
|
@ -192,8 +192,8 @@ Typical uses of =ltlfilt= on CSV file include:
|
|||
|
||||
* Dealing with header lines
|
||||
|
||||
Some CSV contain a header lines that should not be processed.
|
||||
The CSV file produced by =ltlcross= have such a line:
|
||||
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
|
||||
randltl -n 2 a b | ltlfilt --remove-wm |
|
||||
|
|
|
|||
|
|
@ -13,8 +13,8 @@ now offers several options to adjust the type of automaton output.
|
|||
Those options will be covered in more detail below, but here is
|
||||
a quick summary:
|
||||
|
||||
- =--tgba= (the default) outputs Transition-based Generalized
|
||||
Büchi Automata
|
||||
- =--tgba= (the default) outputs Transition-based Generalized Büchi
|
||||
Automata
|
||||
- =--ba= (or =-B=) outputs state-based Büchi automata
|
||||
- =--monitor= (or =-M=) outputs Monitors
|
||||
- =--generic --deterministic= (or =-GD=) will do whatever it takes to
|
||||
|
|
@ -70,7 +70,7 @@ ltl2tgba "Fa & GFb" -d | dot -Tpdf > tgba.pdf
|
|||
#+RESULTS:
|
||||
|
||||
The result would look like this (note that in this documentation
|
||||
we use some [[file:oaut.org][environment variables]] to produce a more colorful
|
||||
we use some [[file:oaut.org::#default-dot][environment variables]] to produce a more colorful
|
||||
output by default)
|
||||
#+NAME: dotex
|
||||
#+BEGIN_SRC sh :results verbatim :exports none
|
||||
|
|
@ -723,8 +723,8 @@ expectations.
|
|||
|
||||
The =--generic= (or =-G=) option allows =ltl2tgba= to use more
|
||||
complex acceptance. Combined with =--deterministic= (or =-D=) this
|
||||
allows the use of a determinization algorithm that produce automata
|
||||
with parity acceptance.
|
||||
allows the use of a determinization algorithm that produces
|
||||
automata with parity acceptance.
|
||||
|
||||
For instance =FGa= is the typical formula for which not
|
||||
deterministic TGBA exists.
|
||||
|
|
@ -762,7 +762,7 @@ parity acceptance, but =Fin(0)&Inf(1)= can be interpreted either as
|
|||
|
||||
The [[./man/spot-x.7.html][=spot-x=]](7) man page lists a few =-x= options (=det-scc=,
|
||||
=det-simul=, =det-stutter=) of the determinization algorithm that are
|
||||
enable by default, but that you may want to disable for experimental
|
||||
enabled by default, but that you may want to disable for experimental
|
||||
purpose.
|
||||
|
||||
For instance the following deterministic automaton
|
||||
|
|
@ -796,13 +796,13 @@ ltl2tgba "F(a W FGb)" -x '!det-scc' -G -D -d.a
|
|||
* Translating multiple formulas for statistics
|
||||
|
||||
If multiple formulas are given to =ltl2tgba=, the corresponding
|
||||
automata will be output one after the other. This is not very
|
||||
convenient, since most of these output formats are not designed to
|
||||
represent multiple automata, and tools like =dot= will only display
|
||||
the first one.
|
||||
automata will be output one after the other. The default output
|
||||
format HOA is designed to allow streaming automata this way to build
|
||||
processing pipelines, but Spot's automaton parser can also read a
|
||||
stream of automata in other formats.
|
||||
|
||||
One situation where passing many formulas to =ltl2tgba= is useful is
|
||||
in combination with the =--stats=FORMAT= option. This option will
|
||||
Another situation where passing many formulas to =ltl2tgba= is useful
|
||||
is in combination with the =--stats=FORMAT= option. This option will
|
||||
output statistics about the translated automata instead of the
|
||||
automata themselves. The =FORMAT= string should indicate which
|
||||
statistics should be output, and how they should be output using the
|
||||
|
|
@ -858,9 +858,9 @@ and /edges/. An edge between two states is labeled by a Boolean
|
|||
formula and may in fact represent several transitions labeled by
|
||||
compatible Boolean assignment.
|
||||
|
||||
For instance if the atomic propositions are =x= and =y=, an edge labeled
|
||||
by the formula =!x= actually represents two transitions labeled respectively
|
||||
with =!x&y= and =!x&!y=.
|
||||
For instance if the atomic propositions are =x= and =y=, an edge
|
||||
labeled by the formula =!x= actually represents two transitions
|
||||
labeled respectively with =!x&y= and =!x&!y=.
|
||||
|
||||
Two automata with the same structures (states and edges) but differing
|
||||
labels, may have a different count of transitions, e.g., if one has
|
||||
|
|
|
|||
|
|
@ -872,9 +872,9 @@ export SPOT_DOTEXTRA='edge[arrowhead=vee, arrowsize=.7]'
|
|||
The =--stats= option takes format string parameter to specify what and
|
||||
how statistics should be output.
|
||||
|
||||
Most tool support a common set of statistics about the output
|
||||
Most tools support a common set of statistics about the output
|
||||
automaton (like =%s= for the number of states, =%t= for transitions,
|
||||
=%e= for edges, etc.) Additional statistics might be available
|
||||
=%e= for edges, etc.). Additional statistics might be available
|
||||
depending on what the tool does (for instance [[file:autfilt.org][=autfilt=]] also has =%S=,
|
||||
=%T=, and =%E= to display the same statistics about the input
|
||||
automaton). All the available statistics are displayed when a tool is
|
||||
|
|
@ -1056,13 +1056,12 @@ autfilt -c out-det1.hoa # Count of deterministic automata
|
|||
: 14
|
||||
: 6
|
||||
|
||||
If you use this feature, beware that the output filename
|
||||
is only truncated by the first file that is output to it: so
|
||||
if no automaton generate some filename, the existing file
|
||||
will be left untouched. For instance we we run the above
|
||||
commands, again, but forcing [[file:randaut.org][=randaut=]] to output 20
|
||||
deterministic automata, it may look like we produced more
|
||||
than 20 automata:
|
||||
If you use this feature, beware that the output filename is only
|
||||
truncated once a first automaton is output to it: so if no automaton
|
||||
is output for a given filename, the existing file will be left
|
||||
untouched. For instance if we run the above commands again, but
|
||||
forcing [[file:randaut.org][=randaut=]] to output 20 *deterministic* automata, it may look
|
||||
like we produced more than 20 automata:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
randaut -D -n 20 -Q2 -e1 1 -o out-det%d.hoa
|
||||
|
|
@ -1082,4 +1081,8 @@ it, prefix the output filename with =>>= as in
|
|||
|
||||
: randaut -D -n 20 -Q2 1 -o '>>out-det%d.hoa'
|
||||
|
||||
(You need the quotes so that the shell does not interpret '>>'.)
|
||||
(You need the quotes so that the shell does not interpret =>>=.)
|
||||
|
||||
#+BEGIN_SRC sh :results silent :exports results
|
||||
rm -f out-det0.hoa out-det1.hoa
|
||||
#+END_SRC
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
|
||||
# Generate a short man page from --help and --version output.
|
||||
# Copyright (C) 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005, 2009,
|
||||
# 2010, 2011, 2012, 2015 Free Software Foundation, Inc.
|
||||
# 2010, 2011, 2012, 2015, 2016 Free Software Foundation, Inc.
|
||||
|
||||
# This program is free software; you can redistribute it and/or modify
|
||||
# it under the terms of the GNU General Public License as published by
|
||||
|
|
@ -555,8 +555,8 @@ while (length)
|
|||
s/\x84//g;
|
||||
|
||||
# Convert options.
|
||||
s/(^| )(-[][\w-]+(?:=[][\w=\/|()'"-]*)?)/$1 . convert_option $2/mge;
|
||||
s/\((-[][\w-]+(?:=[][\w=\/|()'"-]*)?)\)/"(" . convert_option $1 . ")"/mge;
|
||||
s/(^| )(-[][\w-]+(?:=[][\w=\/|()+<#.'"-]*)?)/$1 . convert_option $2/mge;
|
||||
s/\((-[][\w-]+(?:=[][\w=\/|()+<#.'"-]*)?)\)/"(" . convert_option $1 . ")"/mge;
|
||||
|
||||
# Escape remaining hyphens
|
||||
s/-/\x83/g;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue