From b7e77743dbd399cbc23d3c456a2dcaa9fd7b00dd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 19 Jun 2018 22:03:48 +0200 Subject: [PATCH] org: fix lists of escape sequences * doc/org/autfilt.org, doc/org/ltl2tgba.org, doc/org/ltlfilt.org: Here. --- doc/org/autfilt.org | 52 ++++++++++++++++++++++++++++++++++++-------- doc/org/ltl2tgba.org | 47 +++++++++++++++++++++++++++++++++------ doc/org/ltlfilt.org | 24 ++++++++++++++++---- 3 files changed, 103 insertions(+), 20 deletions(-) diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index cbf1ab75f..85a35dce4 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -127,25 +127,59 @@ autfilt --stats='%s states, %e edges, %a acc-sets, %c SCCs, det=%d' The following =%= sequences are available: #+BEGIN_SRC sh :results verbatim :exports results -autfilt --help | sed -n '/^ %%/,/^$/p' | sed '$d' +ltl2tgba --help | sed -n '/ sequences:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: #+begin_example + %< the part of the line before the formula if it + comes from a column extracted from a CSV file + %> the part of the line after the formula if it comes + from a column extracted from a CSV file %% a single % - %A, %a number of acceptance sets - %C, %c number of SCCs + %a number of acceptance sets + %c, %[LETTERS]c number of SCCs; you may filter the SCCs to count + using the following LETTERS, possibly + concatenated: (a) accepting, (r) rejecting, (c) + complete, (v) trivial, (t) terminal, (w) weak, + (iw) inherently weak. Use uppercase letters to + negate them. %d 1 if the output is deterministic, 0 otherwise - %E, %e number of edges + %e number of reachable edges + %f the formula, in Spot's syntax %F name of the input file - %G, %g acceptance condition (in HOA syntax) + %g, %[LETTERS]g acceptance condition (in HOA syntax); add brackets + to print an acceptance name instead and LETTERS to + tweak the format: (0) no parameters, (a) + accentuated, (b) abbreviated, (d) style used in + dot output, (g) no generalized parameter, (l) + recognize Street-like and Rabin-like, (m) no main + parameter, (p) no parity parameter, (o) name + unknown acceptance as 'other', (s) shorthand for + 'lo0'. + %h the automaton in HOA format on a single line (use + %[opt]h to specify additional options as in + --hoa=opt) %L location in the input file - %M, %m name of the automaton + %m name of the automaton %n number of nondeterministic states in output %p 1 if the output is complete, 0 otherwise - %r processing time (excluding parsing) in seconds - %S, %s number of states - %T, %t number of transitions + %r wall-clock time elapsed in seconds (excluding + parsing) + %R, %[LETTERS]R CPU time (excluding parsing), in seconds; Add + LETTERS to restrict to(u) user time, (s) system + time, (p) parent process, or (c) children + processes. + %s number of reachable states + %t number of reachable transitions %w one word accepted by the output automaton + %x, %[LETTERS]x number of atomic propositions declared in the + automaton; add LETTERS to list atomic + propositions with (n) no quoting, (s) occasional + double-quotes with C-style escape, (d) + double-quotes with C-style escape, (c) + double-quotes with CSV-style escape, (p) between + parentheses, any extra non-alphanumeric character + will be used to separate propositions #+end_example When a letter is available both as uppercase and lowercase, the diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 5b510864d..d3eeae2ec 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -981,26 +981,59 @@ statistics should be output, and how they should be output using the following sequence of characters (other characters are output as-is): #+BEGIN_SRC sh :results verbatim :exports results -ltl2tgba --help | sed -n '/^ *%/p' +ltl2tgba --help | sed -n '/ sequences:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: #+begin_example + %< the part of the line before the formula if it + comes from a column extracted from a CSV file + %> the part of the line after the formula if it comes + from a column extracted from a CSV file %% a single % %a number of acceptance sets - %c number of SCCs + %c, %[LETTERS]c number of SCCs; you may filter the SCCs to count + using the following LETTERS, possibly + concatenated: (a) accepting, (r) rejecting, (c) + complete, (v) trivial, (t) terminal, (w) weak, + (iw) inherently weak. Use uppercase letters to + negate them. %d 1 if the output is deterministic, 0 otherwise - %e number of edges + %e number of reachable edges %f the formula, in Spot's syntax %F name of the input file - %g acceptance condition (in HOA syntax) + %g, %[LETTERS]g acceptance condition (in HOA syntax); add brackets + to print an acceptance name instead and LETTERS to + tweak the format: (0) no parameters, (a) + accentuated, (b) abbreviated, (d) style used in + dot output, (g) no generalized parameter, (l) + recognize Street-like and Rabin-like, (m) no main + parameter, (p) no parity parameter, (o) name + unknown acceptance as 'other', (s) shorthand for + 'lo0'. + %h the automaton in HOA format on a single line (use + %[opt]h to specify additional options as in + --hoa=opt) %L location in the input file %m name of the automaton %n number of nondeterministic states in output %p 1 if the output is complete, 0 otherwise - %r processing time (excluding parsing) in seconds - %s number of states - %t number of transitions + %r wall-clock time elapsed in seconds (excluding + parsing) + %R, %[LETTERS]R CPU time (excluding parsing), in seconds; Add + LETTERS to restrict to(u) user time, (s) system + time, (p) parent process, or (c) children + processes. + %s number of reachable states + %t number of reachable transitions %w one word accepted by the output automaton + %x, %[LETTERS]x number of atomic propositions declared in the + automaton; add LETTERS to list atomic + propositions with (n) no quoting, (s) occasional + double-quotes with C-style escape, (d) + double-quotes with C-style escape, (c) + double-quotes with CSV-style escape, (p) between + parentheses, any extra non-alphanumeric character + will be used to separate propositions #+end_example For instance we can study the size of the automata generated for the diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 5698e099e..d4bd5d06d 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -493,18 +493,15 @@ GF(1 U b) The =--format= option can be used the alter the way formulas are output. The list of supported =%=-escape sequences are recalled in the =--help= output: #+BEGIN_SRC sh :results verbatim :exports results -ltlfilt --help | sed -n '/The FORMAT/,/^$/p' | sed '$d' +ltlfilt --help | sed -n '/ sequences:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: #+begin_example - The FORMAT string passed to --format may use the following interpreted - sequences: %< the part of the line before the formula if it comes from a column extracted from a CSV file %> the part of the line after the formula if it comes from a column extracted from a CSV file %% a single % - %a number of atomic propositions used in the formula %b the Boolean-length of the formula (i.e., all Boolean subformulas count as 1) %f the formula (in the selected syntax) @@ -513,7 +510,26 @@ ltlfilt --help | sed -n '/The FORMAT/,/^$/p' | sed '$d' hierarchy ([v] replaces abbreviations by class names, [w] for all compatible classes) %L the original line number in the input file + %[OP]n the nesting depth of operator OP. OP should be a + single letter denoting the operator to count, or + multiple letters to fuse several operators during + depth evaluation. Add '~' to rewrite the formula + in negative normal form before counting. + %r wall-clock time elapsed in seconds (excluding + parsing) + %R, %[LETTERS]R CPU time (excluding parsing), in seconds; Add + LETTERS to restrict to(u) user time, (s) system + time, (p) parent process, or (c) children + processes. %s the length (or size) of the formula + %x, %[LETTERS]X, %[LETTERS]x number of atomic propositions used in the + formula; add LETTERS to list atomic propositions + with (n) no quoting, (s) occasional double-quotes + with C-style escape, (d) double-quotes with + C-style escape, (c) double-quotes with CSV-style + escape, (p) between parentheses, any extra + non-alphanumeric character will be used to + separate propositions #+end_example As a trivial example, use