fix some typos in the spot-x man page
* bin/spot-x.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz
parent
08c2424e2e
commit
b8c7eb7f2b
1 changed files with 28 additions and 27 deletions
|
|
@ -25,12 +25,12 @@
|
|||
#include "common_setup.hh"
|
||||
|
||||
const char argp_program_doc[] ="\
|
||||
Common fine-tuning options for binaries built with Spot.\n\
|
||||
Common fine-tuning options for programs installed with Spot.\n\
|
||||
\n\
|
||||
The argument of -x or --extra-options is a comma-separated list of KEY=INT \
|
||||
assignments that are passed to the post-processing routines (they may \
|
||||
be passed to other algorithms in the future). These options are \
|
||||
mostly used for benchmarking and debugging purpose. KEYR (without any \
|
||||
assignments that are passed to the post-processing or translation routines \
|
||||
(they may be passed to other algorithms in the future). These options are \
|
||||
mostly used for benchmarking and debugging purpose. KEY (without any \
|
||||
value) is a shorthand for KEY=1, while !KEY is a shorthand for KEY=0.";
|
||||
|
||||
#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0
|
||||
|
|
@ -39,7 +39,7 @@ static const argp_option options[] =
|
|||
{
|
||||
{ nullptr, 0, nullptr, 0, "Temporal logic simplification options:", 0 },
|
||||
{ DOC("tls-impl",
|
||||
"Control usage of implication-based rewriting. \
|
||||
"Control usage of implication-based rewriting. \
|
||||
(0) disables it, (1) enables rules based on syntactic implications, \
|
||||
(2) additionally allows automata-based implication checks, (3) enables \
|
||||
more rules based on automata-based implication checks. The default value \
|
||||
|
|
@ -53,7 +53,8 @@ as product or sum of subformulas.") },
|
|||
{ DOC("comp-susp", "Set to 1 to enable compositional suspension, \
|
||||
as described in our SPIN'13 paper (see Bibliography below). Set to 2, \
|
||||
to build only the skeleton TGBA without composing it. Set to 0 (the \
|
||||
default) to disable.") },
|
||||
default) to disable. Nowadays, ltl-split already takes care of that for \
|
||||
suspendable subformulas at the top level.") },
|
||||
{ DOC("early-susp", "When set to 1, start compositional suspension on \
|
||||
the transitions that enter accepting SCCs, and not only on the transitions \
|
||||
inside accepting SCCs. This option defaults to 0, and is only used when \
|
||||
|
|
@ -63,33 +64,33 @@ explicitly iterate over all possible valuations of atomic propositions when \
|
|||
considering the successors of a BDD-encoded state, instead of discovering \
|
||||
possible successors by rewriting the BDD as a sum of product. This is enabled \
|
||||
by default for --high, and disabled by default otherwise. When unambiguous \
|
||||
automata are required, this option forced and cannot be disabled.") },
|
||||
automata are required, this option is forced and cannot be disabled.") },
|
||||
{ DOC("skel-simul", "Default to 1. Set to 0 to disable simulation \
|
||||
on the skeleton automaton during compositional suspension. Only used when \
|
||||
on the skeleton automaton during compositional suspension. Only used when \
|
||||
comp-susp=1.") },
|
||||
{ DOC("skel-wdba", "Set to 0 to disable WDBA \
|
||||
minimization on the skeleton automaton during compositional suspension. \
|
||||
Set to 1 always WDBA-minimize the skeleton . Set to 2 to keep the WDBA \
|
||||
minimization on the skeleton automaton during compositional suspension. \
|
||||
Set to 1 always WDBA-minimize the skeleton. Set to 2 to keep the WDBA \
|
||||
only if it is smaller than the original skeleton. This option is only \
|
||||
used when comp-susp=1 and default to 1 or 2 depending on whether --small \
|
||||
or --deterministic is specified.") },
|
||||
{ nullptr, 0, nullptr, 0, "Postprocessing options:", 0 },
|
||||
{ DOC("scc-filter", "Set to 1 (the default) to enable \
|
||||
SCC-pruning and acceptance simplification at the beginning of \
|
||||
post-processing. Transitions that are outside of accepting SCC are \
|
||||
post-processing. Transitions that are outside of accepting SCC are \
|
||||
removed from accepting sets, except those that enter into an accepting \
|
||||
SCC. Set to 2 to remove even these entering transition from the \
|
||||
accepting sets. Set to 0 to disable this SCC-pruning and acceptance \
|
||||
SCC. Set to 2 to remove even these entering transition from the \
|
||||
accepting sets. Set to 0 to disable this SCC-pruning and acceptance \
|
||||
simpification pass.") },
|
||||
{ DOC("degen-reset", "If non-zero (the default), the \
|
||||
degeneralization algorithm will reset its level any time it exits \
|
||||
an SCC.") },
|
||||
{ DOC("degen-lcache", "If non-zero (the default is 1), whenever the \
|
||||
degeneralization algorithm enters an SCC on a state that has already \
|
||||
been associated to a level elsewhere, it should reuse that level. \
|
||||
been associated to a level elsewhere, it should reuse that level. \
|
||||
Different values can be used to select which level to reuse: 1 always \
|
||||
uses the first level created, 2 uses the minimum level seen so far, and \
|
||||
3 uses the maximum level seen so far. The \"lcache\" stands for \
|
||||
3 uses the maximum level seen so far. The \"lcache\" stands for \
|
||||
\"level cache\".") },
|
||||
{ DOC("degen-order", "If non-zero, the degeneralization algorithm \
|
||||
will compute an independent degeneralization order for each SCC it \
|
||||
|
|
@ -149,9 +150,9 @@ This is enabled by default for medium and high optimization \
|
|||
levels. Unless we are building deterministic automata, the \
|
||||
resulting automata are compared to the automata built using the \
|
||||
more traditional pipeline, and only kept if they are better.") },
|
||||
{ DOC("simul", "Set to 0 to disable simulation-based reductions. \
|
||||
Set to 1 to use only direct simulation. Set to 2 to use only reverse \
|
||||
simulation. Set to 3 to iterate both direct and reverse simulations. \
|
||||
{ DOC("simul", "Set to 0 to disable simulation-based reductions. \
|
||||
Set to 1 to use only direct simulation. Set to 2 to use only reverse \
|
||||
simulation. Set to 3 to iterate both direct and reverse simulations. \
|
||||
The default is 3, except when option --low is specified, in which case \
|
||||
the default is 1.") },
|
||||
{ DOC("ba-simul", "Set to 0 to disable simulation-based reductions \
|
||||
|
|
@ -189,8 +190,8 @@ that are weak and deterministic. The default is 1 in --high mode, else 2 in \
|
|||
{ DOC("wdba-det-max", "Maximum number of additional states allowed \
|
||||
in intermediate steps of WDBA-minimization. If the number of additional \
|
||||
states reached in the powerset construction or in the followup products \
|
||||
exceeds this value, WDBA-minimization is aborted. \
|
||||
Defaults to 4096. Set to 0 to disable. This limit is ignored when -D used \
|
||||
exceeds this value, WDBA-minimization is aborted. \
|
||||
Defaults to 4096. Set to 0 to disable. This limit is ignored when -D used \
|
||||
or when det-max-states is set.") },
|
||||
{ DOC("tba-det", "Set to 1 to attempt a powerset determinization \
|
||||
if the TGBA is not already deterministic. Doing so will degeneralize \
|
||||
|
|
@ -203,15 +204,15 @@ is disabled at low level or if parameter \"simul\" is set to 0.") },
|
|||
of deterministic ω-automata. If the input has n states, a SAT solver is \
|
||||
used to find an equivalent automaton with 1≤m<n states. The value between \
|
||||
1 and 4 selects how the lowest possible m is searched, see the SAT-MINIMIZE \
|
||||
VALUE section. SAT-based minimization uses PicoSAT (distributed with Spot), \
|
||||
VALUE section. SAT-based minimization uses PicoSAT (embedded in Spot), \
|
||||
but another installed SAT-solver can be set thanks to the SPOT_SATSOLVER \
|
||||
environment variable. Enabling SAT-based minimization will also enable \
|
||||
environment variable. Enabling SAT-based minimization will also enable \
|
||||
tba-det.") },
|
||||
{ DOC("sat-incr-steps", "Set the value of sat-incr-steps. This variable \
|
||||
is used by two SAT-based minimization algorithms: (2) and (3). They are both \
|
||||
{ DOC("sat-incr-steps", "Set the value of sat-incr-steps. This variable \
|
||||
is used by two SAT-based minimization algorithms: (2) and (3). They are both \
|
||||
described below.") },
|
||||
{ DOC("sat-langmap", "Find the lower bound of default sat-minimize \
|
||||
procedure (1). This relies on the fact that the size of the minimal automaton \
|
||||
procedure (1). This relies on the fact that the size of the minimal automaton \
|
||||
is at least equal to the total number of different languages recognized by \
|
||||
the automaton's states.") },
|
||||
{ DOC("sat-states",
|
||||
|
|
@ -224,8 +225,8 @@ automaton could be constructed with the given number of states, the original \
|
|||
automaton is returned.") },
|
||||
{ DOC("sat-acc",
|
||||
"When this is set to some positive integer, the SAT-based will \
|
||||
attempt to construct a TGBA with the given number of acceptance sets. \
|
||||
states. It may however return an automaton with fewer acceptance sets if \
|
||||
attempt to construct a TGBA with the given number of acceptance sets. \
|
||||
It may however return an automaton with fewer acceptance sets if \
|
||||
some of these are useless. Setting sat-acc automatically \
|
||||
sets sat-minimize to 1 if not set differently.") },
|
||||
{ DOC("state-based",
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue