From de935d40ca62a8c163102b436d4ec999580d8c6a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 1 Feb 2015 20:31:21 +0100 Subject: [PATCH] autfilt: improve documentation * src/bin/autfilt.cc: Tweak --help. * doc/org/autfilt.org: More documentation. --- doc/org/autfilt.org | 74 ++++++++++++++++++++++++++++++++++++++++++++- src/bin/autfilt.cc | 12 ++++---- 2 files changed, 79 insertions(+), 7 deletions(-) diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index c62de09ca..5bb294b36 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -5,6 +5,18 @@ 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 @@ -73,7 +85,6 @@ autfilt example.hoa --lbtt : 0 -1 ! p0 : -1 - * Displaying statistics One special output format of =autfilt= is the statistic output. For @@ -127,6 +138,41 @@ 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 @@ -168,3 +214,29 @@ autfilt --help | sed -n '/Optimization level:/,/^$/p' | sed '1d;$d' : --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) diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 4f0a11d42..5d4f5adc7 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -96,15 +96,17 @@ static const argp_option options[] = { "merge-transitions", OPT_MERGE, 0, 0, "merge transitions with same destination and acceptance", 0 }, { "product", OPT_PRODUCT, "FILENAME", 0, - "build the product with FILENAME", 0 }, + "build the product with the automaton in FILENAME", 0 }, { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL, "randomize states and transitions (specify 's' or 't' to " "randomize only states or transitions)", 0 }, { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL, "allow more stuttering (two possible algorithms)", 0 }, { "destut", OPT_DESTUT, 0, 0, "allow less stuttering", 0 }, + { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0, + "remove all transitions in specified acceptance sets", 0 }, /**************************************************/ - { 0, 0, 0, 0, "Filters:", 6 }, + { 0, 0, 0, 0, "Filtering options:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, "keep automata that are isomorphic to the automaton in FILENAME", 0 }, { "isomorphic", 0, 0, OPTION_ALIAS | OPTION_HIDDEN, 0, 0 }, @@ -112,9 +114,9 @@ static const argp_option options[] = "do not output the same automaton twice (same in the sense that they "\ "are isomorphic)", 0 }, { "is-complete", OPT_IS_COMPLETE, 0, 0, - "the automaton is complete", 0 }, + "keep complete automata", 0 }, { "is-deterministic", OPT_IS_DETERMINISTIC, 0, 0, - "the automaton is deterministic", 0 }, + "keep deterministic automata", 0 }, { "is-empty", OPT_IS_EMPTY, 0, 0, "keep automata with an empty language", 0 }, { "intersect", OPT_INTERSECT, "FILENAME", 0, @@ -127,8 +129,6 @@ static const argp_option options[] = "keep automata whose number of edges are in RANGE", 0 }, { "acc-sets", OPT_ACC_SETS, "RANGE", 0, "keep automata whose number of acceptance sets are in RANGE", 0 }, - { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0, - "remove all transitions in specified acceptance sets", 0 }, RANGE_DOC_FULL, /**************************************************/ { 0, 0, 0, 0, "Miscellaneous options:", -1 },