From b321a410d57727d7b3606520fbe6824293e2dff0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Feb 2015 11:56:19 +0100 Subject: [PATCH] org: more documentation * doc/org/oaut.org: Mention --dot=a. * doc/org/autfilt.org: Update list of transformations. --- doc/org/autfilt.org | 33 ++++++++++++++++++++++++--------- doc/org/oaut.org | 42 ++++++++++++++++++++++++++---------------- 2 files changed, 50 insertions(+), 25 deletions(-) diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 5bb294b36..c7a712cf0 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -231,12 +231,27 @@ 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) +#+begin_example + --cleanup-acceptance remove unused acceptance sets from the automaton + --complement-acceptance complement the acceptance condition (without + touching the automaton) + --destut allow less stuttering + --dnf-acceptance put the acceptance condition in Disjunctive Normal + Form + --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 + --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) + --remove-fin rewrite the automaton without using Fin acceptance + + --state-based-acceptance, --sbacc + define the acceptance using states + --strip-acceptance remove the acceptance condition and all acceptance + sets +#+end_example diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 774d434ac..16a5e1338 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -18,17 +18,18 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' #+begin_example -8, --utf8 enable UTF-8 characters in output (ignored with --lbtt or --spin) - --dot[=c|h|n|N|s|t|v] GraphViz's format (default). Add letters to chose - (c) circular nodes, (h) horizontal layout, (v) - vertical layout, (n) with name, (N) without name, - (s) with SCCs, (t) always transition-based - acceptance. + --dot[=c|h|n|N|s|t|v] GraphViz's format (default). Add letters for (a) + acceptance display, (c) circular nodes, (h) + horizontal layout, (v) vertical layout, (n) with + name, (N) without name, (s) with SCCs, (t) force + transition-based acceptance. -H, --hoaf[=s|t|m|l] Output the automaton in HOA format. Add letters - to select (s) state-based acceptance, (t) - transition-based acceptance, (m) mixed acceptance, - (l) single-line output + to select (s) prefer state-based acceptance when + possible [default], (t) force transition-based + acceptance, (m) mix state and transition-based + acceptance, (l) single-line output --lbtt[=t] LBTT's format (add =t to force transition-based - acceptance even on Büchi automata) + acceptance even on Büchi automata) --name=FORMAT set the name of the output automaton -o, --output=FORMAT send output to a file named FORMAT instead of standard output. The first automaton sent to a @@ -270,7 +271,7 @@ $txt #+RESULTS: [[file:hoafex.png]] -The [[http://adl.github.io/hoaf/][HOA format]] support both state and transition-based acceptance. +The [[http://adl.github.io/hoaf/][HOA format]] supports both state and transition-based acceptance. Although Spot works only with transition-based acceptance, its output routines default to state-based acceptance whenever possible (this is the case in the first of these two automata) and use transition-based @@ -530,30 +531,35 @@ $txt This output can be customized by passing optional characters to the =--dot= option. For instance =v= requests a vertical layout (instead of the default horizontal layout), =c= requests circle states, =s= -causes strongly-connected components to be displayed, and =n= causes -the name (see below) of the automaton to be displayed. +causes strongly-connected components to be displayed, =n= causes the +name (see below) of the automaton to be displayed, and =a= causes the +acceptance condition to be shown as well. #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba --dot=vcsn '(Ga -> Gb) W c' +ltl2tgba --dot=vcsna '(Ga -> Gb) W c' #+END_SRC #+RESULTS: #+begin_example digraph G { - label="(Gb | F!a) W c" + label="(Gb | F!a) W c\nInf(0)" labelloc="t" node [shape="circle"] I [label="", style=invis, height=0] I -> 1 subgraph cluster_0 { + label="" 0 [label="0"] } subgraph cluster_1 { + label="" 3 [label="3"] } subgraph cluster_2 { + label="" 4 [label="4"] } subgraph cluster_3 { + label="" 1 [label="1"] 2 [label="2"] } @@ -574,13 +580,13 @@ digraph G { #+NAME: oaut-dot2 #+BEGIN_SRC sh :results verbatim :exports none -ltl2tgba --dot=vcsn '(Ga -> Gb) W c' | sed 's/\\/\\\\/' +ltl2tgba --dot=vcsna '(Ga -> Gb) W c' | sed 's/\\/\\\\/' #+END_SRC #+RESULTS: oaut-dot2 #+begin_example digraph G { - label="(Gb | F!a) W c" + label="(Gb | F!a) W c\\nInf(0)" labelloc="t" node [shape="circle"] I [label="", style=invis, height=0] @@ -624,6 +630,10 @@ $txt #+RESULTS: [[file:oaut-dot2.png]] +The acceptance condition is displayed in the same way as in the [[http://adl.github.io/hoaf/][HOA +format]]. Here =Inf(0)= means that runs are accepting if and only if +they visit some the transitions in the set #0 infinitely often. + * Statistics The =--stats= option takes format string parameter to specify what and