diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index b567e7c3e..096079508 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -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 < 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 diff --git a/doc/org/compile.org b/doc/org/compile.org index 5aa47111a..17c219a8c 100644 --- a/doc/org/compile.org +++ b/doc/org/compile.org @@ -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=. diff --git a/doc/org/concepts.org b/doc/org/concepts.org index bcf07b09d..d5d771642 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1044,14 +1044,14 @@ 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~ | A vector naming each state of the automaton, for display purpose. | -| ~highlight-edges~ | ~std::map~ | A map of (edge number, color number) for highlighting the output. | -| ~highlight-states~ | ~std::map~ | A map of (state number, color number) for highlighting the output. | -| ~incomplete-states~ | ~std::set~ | A set of states numbers that should be displayed as incomplete. Used internally by ~print_dot()~ when truncating large automata. | +| key name | (pointed) value type | description | +|---------------------+--------------------------------+---------------------------------------------------------------------------------------------------------------------------------| +| ~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~ | vector naming each state of the automaton, for display purpose | +| ~highlight-edges~ | ~std::map~ | map of (edge number, color number) for highlighting the output | +| ~highlight-states~ | ~std::map~ | map of (state number, color number) for highlighting the output | +| ~incomplete-states~ | ~std::set~ | 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 diff --git a/doc/org/csv.org b/doc/org/csv.org index 0cee75f18..bfdf7afd1 100644 --- a/doc/org/csv.org +++ b/doc/org/csv.org @@ -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 | diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 9552f7bc4..8381adc3f 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -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 diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 58d197eb4..d6bd1144d 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -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 diff --git a/tools/help2man b/tools/help2man index fb7c4da78..d8294a375 100755 --- a/tools/help2man +++ b/tools/help2man @@ -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;