diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 0943f34bd..c4905c2e9 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -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