spot-x.cc 8.61 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
3
// Développement de l'Epita (LRDE).
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

#include "common_sys.hh"
#include <string>
#include <iostream>
#include <cstdlib>
#include <argp.h>
#include "common_setup.hh"

const char argp_program_doc[] ="\
Common fine-tuning options for binaries built 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 \
value) is a shorthand for KEY=1, while !KEY is a shorthand for KEY=0.";

36
#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0
37
38
39

static const argp_option options[] =
  {
40
    { nullptr, 0, nullptr, 0, "Translation options:", 0 },
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
    { 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.") },
    { 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 \
comp-susp=1.") },
    { DOC("skel-simul", "Default to 1.  Set to 0 to disable simulation \
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 \
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.") },
58
    { nullptr, 0, nullptr, 0, "Postprocessing options:", 0 },
59
60
61
62
63
64
65
66
67
    { 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 \
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 \
simpification pass.") },
    { DOC("degen-reset", "If non-zero (the default), the \
degeneralization algorithm will reset its level any time it exits \
68
69
an SCC.") },
    { DOC("degen-lcache", "If non-zero (the default is 1), whenever the \
70
71
degeneralization algorithm enters an SCC on a state that has already \
been associated to a level elsewhere, it should reuse that level. \
72
Different values can be used to select which level to reuse: 1 always \
73
uses the first level created, 2 uses the minimum level seen so far, and \
74
75
3 uses the maximum level seen so far. The \"lcache\" stands for \
\"level cache\".") },
76
    { DOC("degen-order", "If non-zero, the degeneralization algorithm \
77
78
will compute an independent degeneralization order for each SCC it \
processes.  This is currently disabled by default.") },
79
80
81
82
83
84
85
    { DOC("degen-lskip", "If non-zero (the default), the degeneralization \
algorithm will skip as much levels as possible for each transition.  This \
is enabled by default as it very often reduce the number of resulting \
states.  A consequence of skipping levels is that the degeneralized \
automaton tends to have smaller cycles around the accepting states.  \
Disabling skipping will produce automata with large cycles, and often \
with more states.") },
86
    { DOC("degen-lowinit", "Whenever the degeneralization algorihm enters \
87
a new SCC (or starts from the initial state), it starts on some level L that \
88
89
is compatible with all outgoing transitions.  If degen-lowinit is zero \
(the default) and the corresponding state (in the generalized automaton) \
90
91
92
93
has an accepting self-loop, then level L is replaced by the accepting \
level, as it might favor finding accepting cycles earlier.  If \
degen-lowinit is non-zero, then level L is always used without looking \
for the presence of an accepting self-loop.") },
94
95
96
97
98
99
    { DOC("det-scc", "Set to 0 to disable scc-based optimizations in \
the determinization algorithm.") },
    { DOC("det-simul", "Set to 0 to disable simulation-based optimizations in \
the determinization algorithm.") },
    { DOC("det-stutter", "Set to 0 to disable optimizations based on \
the stutter-invariance in the determinization algorithm.") },
100
101
102
    { 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. \
103
104
The default is 3, except when option --low is specified, in which case \
the default is 1.") },
105
106
107
108
109
    { DOC("ba-simul", "Set to 0 to disable simulation-based reductions \
on the Büchi automaton (i.e., after degeneralization has been performed). \
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 in --high mode, and 0 otherwise.") },
110
111
    { DOC("wdba-minimize", "Set to 0 to disable WDBA-minimization.  \
Enabled by default.") },
112
113
114
115
    { DOC("tba-det", "Set to 1 to attempt a powerset determinization \
if the TGBA is not already deterministic.  Doing so will degeneralize \
the automaton.  This is disabled by default, unless sat-minimize is set.") },
    { DOC("sat-minimize",
116
117
118
119
120
121
122
123
124
125
126
127
128
129
          "Set it to enable SAT-based minimization of deterministic \
TGBA. Depending on its value (from 1 to 4) it changes the algorithm \
to perform. The default value is (1) and it proves to be the most effective \
method. SAT-based minimization uses PicoSAT (distributed with Spot), but \
another installed SAT-solver can be set thanks to the SPOT_SATSOLVER \
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 \
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 \
is at least equal to the total number of different languages recognized by \
the automaton's states.") },
130
    { DOC("sat-states",
131
          "When this is set to some positive integer, the SAT-based \
132
133
134
135
136
137
138
minimization will attempt to construct a TGBA with the given number of \
states.  It may however return an automaton with less states if some of \
these are unreachable or useless.  Setting sat-states automatically \
enables sat-minimize, but no iteration is performed.  If no equivalent \
automaton could be constructed with the given number of states, the original \
automaton is returned.") },
    { DOC("sat-acc",
139
          "When this is set to some positive integer, the SAT-based will \
140
141
142
143
144
attempt to construct a TGBA with the given number of acceptance sets. \
states.  It may however return an automaton with less acceptance sets if \
some of these are useless.  Setting sat-acc automatically \
sets sat-minimize to 1 if not set differently.") },
    { DOC("state-based",
145
          "Set to 1 to instruct the SAT-minimization procedure to produce \
146
147
a TGBA where all outgoing transition of a state have the same acceptance \
sets.  By default this is only enabled when option -B is used.") },
148
    { nullptr, 0, nullptr, 0, nullptr, 0 }
149
150
151
152
  };

const struct argp_child children[] =
  {
153
154
    { &misc_argp_hidden, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
155
156
157
158
159
160
161
  };

int
main(int argc, char** argv)
{
  setup(argv);

162
  const argp ap = { options, nullptr, nullptr, argp_program_doc, children,
163
                    nullptr, nullptr };
164

165
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
166
167
168
    exit(err);

  std::cerr << "This binary serves no purpose other than generating"
169
            << " the spot-x.7 manpage.\n";
170
171
172

  return 1;
}