autfilt.cc 56.4 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2013-2020 Laboratoire de Recherche et Développement
3
// de l'Epita (LRDE).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
//
// 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>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
24
#include <limits>
25 26
#include <set>
#include <memory>
27 28
#include <sys/stat.h>
#include <unistd.h>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
29 30 31

#include <argp.h>
#include "error.h"
32
#include "argmatch.h"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
33 34 35 36

#include "common_setup.hh"
#include "common_finput.hh"
#include "common_cout.hh"
37
#include "common_aoutput.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
38
#include "common_range.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
39
#include "common_post.hh"
40
#include "common_conv.hh"
41
#include "common_hoaread.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
42

43 44
#include <spot/misc/optionmap.hh>
#include <spot/misc/random.hh>
45
#include <spot/misc/timer.hh>
46 47 48 49
#include <spot/parseaut/public.hh>
#include <spot/tl/exclusive.hh>
#include <spot/twaalgos/are_isomorphic.hh>
#include <spot/twaalgos/canonicalize.hh>
50
#include <spot/twaalgos/cobuchi.hh>
51
#include <spot/twaalgos/cleanacc.hh>
52
#include <spot/twaalgos/complement.hh>
53
#include <spot/twaalgos/contains.hh>
54
#include <spot/twaalgos/degen.hh>
55
#include <spot/twaalgos/dtwasat.hh>
56
#include <spot/twaalgos/dualize.hh>
57
#include <spot/twaalgos/gtec/gtec.hh>
58
#include <spot/twaalgos/hoa.hh>
59
#include <spot/twaalgos/iscolored.hh>
60 61
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/isunamb.hh>
62
#include <spot/twaalgos/isweakscc.hh>
63
#include <spot/twaalgos/langmap.hh>
64 65 66 67 68 69 70 71 72 73 74 75 76
#include <spot/twaalgos/mask.hh>
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/randomize.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/remprop.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/sepsets.hh>
#include <spot/twaalgos/split.hh>
#include <spot/twaalgos/strength.hh>
#include <spot/twaalgos/stripacc.hh>
#include <spot/twaalgos/stutter.hh>
#include <spot/twaalgos/sum.hh>
#include <spot/twaalgos/totgba.hh>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
77

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
78
static const char argp_program_doc[] ="\
79
Convert, transform, and filter omega-automata.\v\
80 81 82 83
Exit status:\n\
  0  if some automata were output\n\
  1  if no automata were output (no match)\n\
  2  if any error has been reported";
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
84

85 86
// Keep this list sorted
enum {
87 88
  OPT_ACC_SCCS = 256,
  OPT_ACC_SETS,
89
  OPT_ACCEPT_WORD,
90
  OPT_ACCEPTANCE_IS,
91
  OPT_AP_N,
92 93
  OPT_ARE_ISOMORPHIC,
  OPT_CLEAN_ACC,
94
  OPT_CNF_ACC,
95
  OPT_COMPLEMENT,
96 97
  OPT_COMPLEMENT_ACC,
  OPT_COUNT,
98
  OPT_DCA,
99
  OPT_DECOMPOSE_SCC,
100
  OPT_DESTUT,
Thomas Medioni's avatar
Thomas Medioni committed
101
  OPT_DUALIZE,
102 103
  OPT_DNF_ACC,
  OPT_EDGES,
104
  OPT_EQUIVALENT_TO,
105
  OPT_EXCLUSIVE_AP,
106 107
  OPT_GENERALIZED_RABIN,
  OPT_GENERALIZED_STREETT,
108 109
  OPT_HAS_EXIST_BRANCHING,
  OPT_HAS_UNIV_BRANCHING,
110 111 112
  OPT_HIGHLIGHT_NONDET,
  OPT_HIGHLIGHT_NONDET_EDGES,
  OPT_HIGHLIGHT_NONDET_STATES,
113
  OPT_HIGHLIGHT_WORD,
114
  OPT_HIGHLIGHT_ACCEPTING_RUN,
115
  OPT_HIGHLIGHT_LANGUAGES,
116
  OPT_INSTUT,
117
  OPT_INCLUDED_IN,
118
  OPT_INHERENTLY_WEAK_SCCS,
119
  OPT_INTERSECT,
120
  OPT_IS_ALTERNATING,
121
  OPT_IS_COLORED,
122 123 124
  OPT_IS_COMPLETE,
  OPT_IS_DETERMINISTIC,
  OPT_IS_EMPTY,
125
  OPT_IS_INHERENTLY_WEAK,
126
  OPT_IS_SEMI_DETERMINISTIC,
127
  OPT_IS_STUTTER_INVARIANT,
128
  OPT_IS_TERMINAL,
129
  OPT_IS_UNAMBIGUOUS,
130
  OPT_IS_VERY_WEAK,
131
  OPT_IS_WEAK,
132 133 134
  OPT_KEEP_STATES,
  OPT_MASK_ACC,
  OPT_MERGE,
135
  OPT_NONDET_STATES,
136
  OPT_PARTIAL_DEGEN,
137 138
  OPT_PRODUCT_AND,
  OPT_PRODUCT_OR,
139
  OPT_RANDOMIZE,
140
  OPT_REJ_SCCS,
141
  OPT_REJECT_WORD,
142
  OPT_REM_AP,
143 144
  OPT_REM_DEAD,
  OPT_REM_UNREACH,
145
  OPT_REM_UNUSED_AP,
146
  OPT_REM_FIN,
147
  OPT_SAT_MINIMIZE,
148
  OPT_SCCS,
149
  OPT_SEED,
150
  OPT_SEP_SETS,
151
  OPT_SIMPL_ACC,
152
  OPT_SIMPLIFY_EXCLUSIVE_AP,
153
  OPT_SPLIT_EDGES,
154
  OPT_STATES,
155
  OPT_STREETT_LIKE,
156
  OPT_STRIPACC,
157 158
  OPT_SUM_OR,
  OPT_SUM_AND,
159 160
  OPT_TERMINAL_SCCS,
  OPT_TRIV_SCCS,
161 162
  OPT_USED_AP_N,
  OPT_UNUSED_AP_N,
163
  OPT_WEAK_SCCS,
164
};
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
165

166 167
#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
168 169 170
static const argp_option options[] =
  {
    /**************************************************/
171
    { nullptr, 0, nullptr, 0, "Input:", 1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
172 173 174
    { "file", 'F', "FILENAME", 0,
      "process the automaton in FILENAME", 0 },
    /**************************************************/
175
    { "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
176
    { "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
177
    /**************************************************/
178 179 180 181 182 183 184 185 186
    { nullptr, 0, nullptr, 0, "Filtering options:", 5 },
    { "ap", OPT_AP_N, "RANGE", 0,
      "match automata with a number of (declared) atomic propositions in RANGE",
      0 },
    { "used-ap", OPT_USED_AP_N, "RANGE", 0,
      "match automata with a number of used atomic propositions in RANGE", 0 },
    { "unused-ap", OPT_UNUSED_AP_N, "RANGE", 0,
      "match automata with a number of declared, but unused atomic "
      "propositions in RANGE", 0 },
187 188
    { "acceptance-is", OPT_ACCEPTANCE_IS, "NAME|FORMULA", 0,
      "match automata with given accetance condition", 0 },
189 190 191 192
    { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
      "keep automata that are isomorphic to the automaton in FILENAME", 0 },
    { "isomorphic", 0, nullptr, OPTION_ALIAS | OPTION_HIDDEN, nullptr, 0 },
    { "unique", 'u', nullptr, 0,
193
      "do not output the same automaton twice (same in the sense that they "
194
      "are isomorphic)", 0 },
195 196 197 198 199
    { "has-exist-branching", OPT_HAS_EXIST_BRANCHING, nullptr, 0,
      "keep automata that use existential branching (i.e., make "
      "non-deterministic choices)", 0 },
    { "has-univ-branching", OPT_HAS_UNIV_BRANCHING, nullptr, 0,
      "keep alternating automata that use universal branching", 0 },
200 201 202
    { "is-colored", OPT_IS_COLORED, nullptr, 0,
      "keep colored automata (i.e., exactly one acceptance mark per "
      "transition or state)", 0 },
203 204 205 206
    { "is-complete", OPT_IS_COMPLETE, nullptr, 0,
      "keep complete automata", 0 },
    { "is-deterministic", OPT_IS_DETERMINISTIC, nullptr, 0,
      "keep deterministic automata", 0 },
207 208
    { "is-semi-deterministic", OPT_IS_SEMI_DETERMINISTIC, nullptr, 0,
      "keep semi-deterministic automata", 0 },
209 210
    { "is-empty", OPT_IS_EMPTY, nullptr, 0,
      "keep automata with an empty language", 0 },
211 212
    { "is-stutter-invariant", OPT_IS_STUTTER_INVARIANT, nullptr, 0,
      "keep automata representing stutter-invariant properties", 0 },
213 214
    { "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
      "keep only terminal automata", 0 },
215 216
    { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
      "keep only unambiguous automata", 0 },
217 218 219 220
    { "is-weak", OPT_IS_WEAK, nullptr, 0,
      "keep only weak automata", 0 },
    { "is-inherently-weak", OPT_IS_INHERENTLY_WEAK, nullptr, 0,
      "keep only inherently weak automata", 0 },
221 222
    { "is-very-weak", OPT_IS_VERY_WEAK, nullptr, 0,
      "keep only very-weak automata", 0 },
223 224
    { "is-alternating", OPT_IS_ALTERNATING, nullptr, 0,
      "keep only automata using universal branching", 0 },
225 226 227 228 229 230 231
    { "intersect", OPT_INTERSECT, "FILENAME", 0,
      "keep automata whose languages have an non-empty intersection with"
      " the automaton from FILENAME", 0 },
    { "included-in", OPT_INCLUDED_IN, "FILENAME", 0,
      "keep automata whose languages are included in that of the "
      "automaton from FILENAME", 0 },
    { "equivalent-to", OPT_EQUIVALENT_TO, "FILENAME", 0,
Maximilien Colange's avatar
Maximilien Colange committed
232
      "keep automata that are equivalent (language-wise) to the automaton "
233 234 235 236 237 238
      "in FILENAME", 0 },
    { "invert-match", 'v', nullptr, 0, "select non-matching automata", 0 },
    { "states", OPT_STATES, "RANGE", 0,
      "keep automata whose number of states is in RANGE", 0 },
    { "edges", OPT_EDGES, "RANGE", 0,
      "keep automata whose number of edges is in RANGE", 0 },
239 240
    { "nondet-states", OPT_NONDET_STATES, "RANGE", 0,
      "keep automata whose number of nondeterministic states is in RANGE", 0 },
241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269
    { "acc-sets", OPT_ACC_SETS, "RANGE", 0,
      "keep automata whose number of acceptance sets is in RANGE", 0 },
    { "sccs", OPT_SCCS, "RANGE", 0,
      "keep automata whose number of SCCs is in RANGE", 0 },
    { "acc-sccs", OPT_ACC_SCCS, "RANGE", 0,
      "keep automata whose number of non-trivial accepting SCCs is in RANGE",
      0 },
    { "accepting-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "rej-sccs", OPT_REJ_SCCS, "RANGE", 0,
      "keep automata whose number of non-trivial rejecting SCCs is in RANGE",
      0 },
    { "rejecting-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "triv-sccs", OPT_TRIV_SCCS, "RANGE", 0,
      "keep automata whose number of trivial SCCs is in RANGE", 0 },
    { "trivial-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "inherently-weak-sccs", OPT_INHERENTLY_WEAK_SCCS, "RANGE", 0,
      "keep automata whose number of accepting inherently-weak SCCs is in "
      "RANGE.  An accepting SCC is inherently weak if it does not have a "
      "rejecting cycle.", 0 },
    { "weak-sccs", OPT_WEAK_SCCS, "RANGE", 0,
      "keep automata whose number of accepting weak SCCs is in RANGE.  "
      "In a weak SCC, all transitions belong to the same acceptance sets.", 0 },
    { "terminal-sccs", OPT_TERMINAL_SCCS, "RANGE", 0,
      "keep automata whose number of accepting terminal SCCs is in RANGE.  "
      "Terminal SCCs are weak and complete.", 0 },
    { "accept-word", OPT_ACCEPT_WORD, "WORD", 0,
      "keep automata that accept WORD", 0 },
    { "reject-word", OPT_REJECT_WORD, "WORD", 0,
      "keep automata that reject WORD", 0 },
270 271 272
    { "nth", 'N', "RANGE", 0,
      "assuming input automata are numbered from 1, keep only those in RANGE",
      0 },
273 274 275 276 277
    /**************************************************/
    RANGE_DOC_FULL,
    WORD_DOC,
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Transformations:", 7 },
278
    { "merge-transitions", OPT_MERGE, nullptr, 0,
279
      "merge transitions with same destination and acceptance", 0 },
280 281 282
    { "product", OPT_PRODUCT_AND, "FILENAME", 0,
      "build the product with the automaton in FILENAME "
      "to intersect languages", 0 },
283
    { "product-and", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
284 285 286
    { "product-or", OPT_PRODUCT_OR, "FILENAME", 0,
      "build the product with the automaton in FILENAME "
      "to sum languages", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
287
    { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
288
      "randomize states and transitions (specify 's' or 't' to "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
289
      "randomize only states or transitions)", 0 },
290 291
    { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL,
      "allow more stuttering (two possible algorithms)", 0 },
292
    { "destut", OPT_DESTUT, nullptr, 0, "allow less stuttering", 0 },
293 294
    { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
      "remove all transitions in specified acceptance sets", 0 },
295
    { "strip-acceptance", OPT_STRIPACC, nullptr, 0,
296
      "remove the acceptance condition and all acceptance sets", 0 },
297 298
    { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
      "only keep specified states.  The first state will be the new "\
299
      "initial state.  Implies --remove-unreachable-states.", 0 },
300
    { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
301
      "put the acceptance condition in Disjunctive Normal Form", 0 },
302 303 304
    { "streett-like", OPT_STREETT_LIKE, nullptr, 0,
      "convert to an automaton with Streett-like acceptance. Works only with "
      "acceptance condition in DNF", 0 },
305
    { "cnf-acceptance", OPT_CNF_ACC, nullptr, 0,
306
      "put the acceptance condition in Conjunctive Normal Form", 0 },
307
    { "remove-fin", OPT_REM_FIN, nullptr, 0,
308
      "rewrite the automaton without using Fin acceptance", 0 },
309 310 311 312 313 314 315 316 317 318 319 320 321 322
    { "generalized-rabin", OPT_GENERALIZED_RABIN,
      "unique-inf|share-inf", OPTION_ARG_OPTIONAL,
      "rewrite the acceptance condition as generalized Rabin; the default "
      "\"unique-inf\" option uses the generalized Rabin definition from the "
      "HOA format; the \"share-inf\" option allows clauses to share Inf sets, "
      "therefore reducing the number of sets", 0 },
    { "gra", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "generalized-streett", OPT_GENERALIZED_STREETT,
      "unique-fin|share-fin", OPTION_ARG_OPTIONAL,
      "rewrite the acceptance condition as generalized Streett;"
      " the \"share-fin\" option allows clauses to share Fin sets,"
      " therefore reducing the number of sets; the default"
      " \"unique-fin\" does not", 0 },
    { "gsa", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
323
    { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
324
      "remove unused acceptance sets from the automaton", 0 },
325
    { "complement", OPT_COMPLEMENT, nullptr, 0,
326
      "complement each automaton (different strategies are used)", 0 },
327
    { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
328 329
      "complement the acceptance condition (without touching the automaton)",
      0 },
330
    { "decompose-scc", OPT_DECOMPOSE_SCC, "t|w|s|N|aN", 0,
331
      "extract the (t) terminal, (w) weak, or (s) strong part of an automaton"
332
      " or (N) the subautomaton leading to the Nth SCC, or (aN) to the Nth "
Clément Gillard's avatar
Clément Gillard committed
333
      "accepting SCC (option can be combined with commas to extract multiple "
334 335
      "parts)", 0 },
    { "decompose-strength", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
Thomas Medioni's avatar
Thomas Medioni committed
336 337
    { "dualize", OPT_DUALIZE, nullptr, 0,
      "dualize each automaton", 0 },
338 339 340 341 342
    { "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0,
      "if any of those APs occur in the automaton, restrict all edges to "
      "ensure two of them may not be true at the same time.  Use this option "
      "multiple times to declare independent groups of exclusive "
      "propositions.", 0 },
343
    { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, nullptr, 0,
344 345 346
      "if --exclusive-ap is used, assume those AP groups are actually exclusive"
      " in the system to simplify the expression of transition labels (implies "
      "--merge-transitions)", 0 },
347 348 349
    { "remove-ap", OPT_REM_AP, "AP[=0|=1][,AP...]", 0,
      "remove atomic propositions either by existential quantification, or "
      "by assigning them 0 or 1", 0 },
350 351
    { "remove-unused-ap", OPT_REM_UNUSED_AP, nullptr, 0,
      "remove declared atomic propositions that are not used", 0 },
352
    { "remove-unreachable-states", OPT_REM_UNREACH, nullptr, 0,
353
      "remove states that are unreachable from the initial state", 0 },
354
    { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
355 356
      "remove states that are unreachable, or that cannot belong to an "
      "infinite path", 0 },
357 358 359
    { "simplify-acceptance", OPT_SIMPL_ACC, nullptr, 0,
      "simplify the acceptance condition by merging identical acceptance sets "
      "and by simplifying some terms containing complementary sets", 0 },
360 361 362
    { "split-edges", OPT_SPLIT_EDGES, nullptr, 0,
      "split edges into transitions labeled by conjunctions of all atomic "
      "propositions, so they can be read as letters", 0 },
363 364 365 366 367 368 369
    { "sum", OPT_SUM_OR, "FILENAME", 0,
      "build the sum with the automaton in FILENAME "
      "to sum languages", 0 },
    { "sum-or", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "sum-and", OPT_SUM_AND, "FILENAME", 0,
      "build the sum with the automaton in FILENAME "
      "to intersect languages", 0 },
370 371 372 373
    { "partial-degeneralize", OPT_PARTIAL_DEGEN, "NUM1,NUM2,...",
      OPTION_ARG_OPTIONAL, "Degeneralize automata according to sets "
      "NUM1,NUM2,... If no sets are given, partial degeneralization "
      "is performed for all conjunctions of Inf and disjunctions of Fin.", 0 },
374
    { "separate-sets", OPT_SEP_SETS, nullptr, 0,
375 376
      "if both Inf(x) and Fin(x) appear in the acceptance condition, replace "
      "Fin(x) by a new Fin(y) and adjust the automaton", 0 },
377
    { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL,
Alexandre Duret-Lutz's avatar
typos  
Alexandre Duret-Lutz committed
378
      "minimize the automaton using a SAT solver (only works for deterministic"
379 380 381 382 383 384 385
      " automata). Supported options are acc=STRING, states=N, max-states=N, "
      "sat-incr=N, sat-incr-steps=N, sat-langmap, sat-naive, colored, preproc=N"
      ". Spot uses by default its PicoSAT distribution but an external SAT"
      "solver can be set thanks to the SPOT_SATSOLVER environment variable"
      "(see spot-x)."
      , 0 },
    { nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 9 },
386 387
    { "highlight-accepting-run", OPT_HIGHLIGHT_ACCEPTING_RUN, "NUM",
      OPTION_ARG_OPTIONAL, "highlight one accepting run using color NUM", 0},
388 389
    { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM",
390
      0 },
391 392
    { "highlight-nondet-edges", OPT_HIGHLIGHT_NONDET_EDGES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic edges with color NUM",
393
      0 },
394 395 396
    { "highlight-nondet", OPT_HIGHLIGHT_NONDET, "NUM",
      OPTION_ARG_OPTIONAL,
      "highlight nondeterministic states and edges with color NUM", 0},
397 398
    { "highlight-word", OPT_HIGHLIGHT_WORD, "[NUM,]WORD", 0,
      "highlight one run matching WORD using color NUM", 0},
399
    { "highlight-languages", OPT_HIGHLIGHT_LANGUAGES, nullptr, 0 ,
400
      "highlight states that recognize identical languages", 0},
401
    /**************************************************/
402 403
    { nullptr, 0, nullptr, 0,
      "If any option among --small, --deterministic, or --any is given, "
404
      "then the simplification level defaults to --high unless specified "
405
      "otherwise.  If any option among --low, --medium, or --high is given, "
406
      "then the simplification goal defaults to --small unless specified "
407 408 409
      "otherwise.  If none of those options are specified, then autfilt "
      "acts as is --any --low were given: these actually disable the "
      "simplification routines.", 22 },
410
    /**************************************************/
411
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
412 413
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
414 415
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
416
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
417 418
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
419
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
420
  {
421
    { &hoaread_argp, 0, nullptr, 0 },
422 423
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
424
    { &post_argp_disabled, 0, nullptr, 0 },
425 426
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
427 428
  };

429

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454
struct canon_aut
{
  typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
  unsigned num_states;
  std::vector<tr_t> edges;
  std::string acc;

  canon_aut(const spot::const_twa_graph_ptr& aut)
    : num_states(aut->num_states())
    , edges(aut->edge_vector().begin() + 1,
            aut->edge_vector().end())
  {
    std::ostringstream os;
    aut->get_acceptance().to_text(os);
    acc = os.str();
  }

  bool operator<(const canon_aut& o) const
  {
    return std::tie(num_states, edges, acc)
      < std::tie(o.num_states, o.edges, o.acc);
  };
};

typedef std::set<canon_aut> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
455
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
456 457 458 459
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
460

461 462 463 464 465 466 467 468 469 470 471 472
enum gra_type { GRA_NO = 0, GRA_SHARE_INF = 1, GRA_UNIQUE_INF = 2 };
static gra_type opt_gra = GRA_NO;
static char const *const gra_args[] =
{
  "default", "share-inf", "hoa", "unique-inf", nullptr
};
static gra_type const gra_types[] =
{
  GRA_UNIQUE_INF, GRA_SHARE_INF, GRA_UNIQUE_INF, GRA_UNIQUE_INF
};
ARGMATCH_VERIFY(gra_args, gra_types);

473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565
enum acc_type {
  ACC_Any = 0,
  ACC_Given,
  ACC_tt,
  ACC_ff,
  ACC_Buchi,
  ACC_GenBuchi,
  ACC_CoBuchi,
  ACC_GenCoBuchi,
  ACC_Rabin,
  ACC_Streett,
  ACC_GenRabin,
  ACC_GenStreett,
  ACC_RabinLike,
  ACC_StreettLike,
  ACC_Parity,
  ACC_ParityMin,
  ACC_ParityMax,
  ACC_ParityOdd,
  ACC_ParityEven,
  ACC_ParityMinOdd,
  ACC_ParityMaxOdd,
  ACC_ParityMinEven,
  ACC_ParityMaxEven,
  ACC_FinLess,
};
static acc_type opt_acceptance_is = ACC_Any;
spot::acc_cond opt_acceptance_is_given;
static char const *const acc_is_args[] =
  {
    "any",
    "t", "all",
    "f", "none",
    "Buchi", "Büchi",
    "generalized-Buchi", "generalized-Büchi",
    "genBuchi", "genBüchi", "gen-Buchi", "gen-Büchi",
    "coBuchi", "coBüchi", "co-Buchi", "co-Büchi",
    "generalized-coBuchi", "generalized-coBüchi",
    "generalized-co-Buchi", "generalized-co-Büchi",
    "gen-coBuchi", "gen-coBüchi",
    "gen-co-Buchi", "gen-co-Büchi",
    "gencoBuchi", "gencoBüchi",
    "Rabin",
    "Streett",
    "generalized-Rabin", "gen-Rabin", "genRabin",
    "generalized-Streett", "gen-Streett", "genStreett",
    "Streett-like",
    "Rabin-like",
    "parity",
    "parity min", "parity-min",
    "parity max", "parity-max",
    "parity odd", "parity-odd",
    "parity even", "parity-even",
    "parity min even", "parity-min-even",
    "parity min odd", "parity-min-odd",
    "parity max even", "parity-max-even",
    "parity max odd", "parity-max-odd",
    "Fin-less", "Finless",
    nullptr,
  };
static acc_type const acc_is_types[] =
  {
    ACC_Any,
    ACC_tt, ACC_tt,
    ACC_ff, ACC_ff,
    ACC_Buchi, ACC_Buchi,
    ACC_GenBuchi, ACC_GenBuchi,
    ACC_GenBuchi, ACC_GenBuchi, ACC_GenBuchi, ACC_GenBuchi,
    ACC_CoBuchi, ACC_CoBuchi, ACC_CoBuchi, ACC_CoBuchi,
    ACC_GenCoBuchi, ACC_GenCoBuchi,
    ACC_GenCoBuchi, ACC_GenCoBuchi,
    ACC_GenCoBuchi, ACC_GenCoBuchi,
    ACC_GenCoBuchi, ACC_GenCoBuchi,
    ACC_GenCoBuchi, ACC_GenCoBuchi,
    ACC_Rabin,
    ACC_Streett,
    ACC_GenRabin, ACC_GenRabin, ACC_GenRabin,
    ACC_GenStreett, ACC_GenStreett, ACC_GenStreett,
    ACC_StreettLike,
    ACC_RabinLike,
    ACC_Parity,
    ACC_ParityMin, ACC_ParityMin,
    ACC_ParityMax, ACC_ParityMax,
    ACC_ParityOdd, ACC_ParityOdd,
    ACC_ParityEven, ACC_ParityEven,
    ACC_ParityMinEven, ACC_ParityMinEven,
    ACC_ParityMinOdd, ACC_ParityMinOdd,
    ACC_ParityMaxEven, ACC_ParityMaxEven,
    ACC_ParityMaxOdd, ACC_ParityMaxOdd,
    ACC_FinLess, ACC_FinLess,
  };
ARGMATCH_VERIFY(acc_is_args, acc_is_types);

566 567 568 569 570 571 572 573 574 575 576 577
enum gsa_type { GSA_NO = 0, GSA_SHARE_FIN = 1, GSA_UNIQUE_FIN = 2 };
static gsa_type opt_gsa = GSA_NO;
static char const *const gsa_args[] =
{
  "default", "share-fin", "unique-fin", nullptr
};
static gsa_type const gsa_types[] =
{
  GSA_UNIQUE_FIN, GSA_SHARE_FIN, GSA_UNIQUE_FIN
};
ARGMATCH_VERIFY(gsa_args, gsa_types);

578
// We want all these variables to be destroyed when we exit main, to
579 580 581 582 583 584
// make sure it happens before all other global variables (like the
// atomic propositions maps) are destroyed.  Otherwise we risk
// accessing deleted stuff.
static struct opt_t
{
  spot::bdd_dict_ptr dict = spot::make_bdd_dict();
585 586
  spot::twa_graph_ptr product_and = nullptr;
  spot::twa_graph_ptr product_or = nullptr;
587 588
  spot::twa_graph_ptr sum_and = nullptr;
  spot::twa_graph_ptr sum_or = nullptr;
589
  spot::twa_graph_ptr intersect = nullptr;
590
  spot::twa_graph_ptr included_in = nullptr;
591 592
  spot::twa_graph_ptr equivalent_pos = nullptr;
  spot::twa_graph_ptr equivalent_neg = nullptr;
593
  spot::twa_graph_ptr are_isomorphic = nullptr;
594 595 596
  std::unique_ptr<spot::isomorphism_checker>
                         isomorphism_checker = nullptr;
  std::unique_ptr<unique_aut_t> uniq = nullptr;
597 598
  spot::exclusive_ap excl_ap;
  spot::remove_ap rem_ap;
599
  std::vector<spot::twa_graph_ptr> acc_words;
600
  std::vector<spot::twa_graph_ptr> rej_words;
601
  std::vector<std::pair<spot::twa_graph_ptr, unsigned>> hl_words;
602 603
}* opt;

604
static bool opt_merge = false;
605 606
static bool opt_has_univ_branching = false;
static bool opt_has_exist_branching = false;
607
static bool opt_is_alternating = false;
608
static bool opt_is_colored = false;
609 610
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
611
static bool opt_is_semi_deterministic = false;
612
static bool opt_is_unambiguous = false;
613 614
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
615
static bool opt_is_inherently_weak = false;
616
static bool opt_is_very_weak = false;
617
static bool opt_is_stutter_invariant = false;
618
static bool opt_invert = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
619
static range opt_states = { 0, std::numeric_limits<int>::max() };
620 621
static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() };
622
static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
623 624 625
static range opt_used_ap_n = { 0, std::numeric_limits<int>::max() };
static range opt_unused_ap_n = { 0, std::numeric_limits<int>::max() };
static bool need_unused_ap_count = false;
626 627 628 629 630 631 632 633 634 635 636 637
static range opt_sccs = { 0, std::numeric_limits<int>::max() };
static range opt_acc_sccs = { 0, std::numeric_limits<int>::max() };
static range opt_rej_sccs = { 0, std::numeric_limits<int>::max() };
static range opt_triv_sccs = { 0, std::numeric_limits<int>::max() };
static bool opt_sccs_set = false;
static bool opt_art_sccs_set = false; // need to classify SCCs as Acc/Rej/Triv.
static range opt_inhweak_sccs = { 0, std::numeric_limits<int>::max() };
static bool opt_inhweak_sccs_set = false;
static range opt_weak_sccs = { 0, std::numeric_limits<int>::max() };
static bool opt_weak_sccs_set = false;
static range opt_terminal_sccs = { 0, std::numeric_limits<int>::max() };
static bool opt_terminal_sccs_set = false;
638 639
static range opt_nondet_states = { 0, std::numeric_limits<int>::max() };
static bool opt_nondet_states_set = false;
640
static int opt_max_count = -1;
641
static range opt_nth = { 0, std::numeric_limits<int>::max() };
642
static bool opt_destut = false;
643
static char opt_instut = 0;
644
static bool opt_is_empty = false;
645
static bool opt_stripacc = false;
646
static bool opt_dnf_acc = false;
647
static bool opt_cnf_acc = false;
648
static bool opt_rem_fin = false;
649
static bool opt_clean_acc = false;
650
static bool opt_complement = false;
651
static bool opt_complement_acc = false;
652
static char* opt_decompose_scc = nullptr;
Thomas Medioni's avatar
Thomas Medioni committed
653
static bool opt_dualize = false;
654 655
static bool opt_partial_degen_set = false;
static spot::acc_cond::mark_t opt_partial_degen = {};
656
static spot::acc_cond::mark_t opt_mask_acc = {};
657 658
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
659
static bool opt_simpl_acc = false;
660
static bool opt_simplify_exclusive_ap = false;
661 662
static bool opt_rem_dead = false;
static bool opt_rem_unreach = false;
663
static bool opt_rem_unused_ap = false;
664
static bool opt_sep_sets = false;
665
static bool opt_split_edges = false;
666
static const char* opt_sat_minimize = nullptr;
667 668
static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1;
669
static int opt_highlight_accepting_run = -1;
670
static bool opt_highlight_languages = false;
671
static bool opt_dca = false;
672
static bool opt_streett_like = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
673

674
static spot::twa_graph_ptr
675
ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
676
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
677
  if ((!nonalt || aut->is_existential()) && spot::is_universal(aut))
678 679 680 681 682 683 684 685
    return aut;
  spot::postprocessor p;
  p.set_type(spot::postprocessor::Generic);
  p.set_pref(spot::postprocessor::Deterministic);
  p.set_level(level);
  return p.run(aut);
}

686 687 688 689 690 691 692 693 694 695 696 697 698 699
static spot::twa_graph_ptr ensure_tba(spot::twa_graph_ptr aut)
{
  spot::postprocessor p;
  p.set_type(spot::postprocessor::TGBA);
  p.set_pref(spot::postprocessor::Any);
  p.set_level(spot::postprocessor::Low);
  return spot::degeneralize_tba(p.run(aut));

}

static spot::twa_graph_ptr
product(spot::twa_graph_ptr left, spot::twa_graph_ptr right)
{
  if ((type == spot::postprocessor::BA)
700 701
      && (left->num_sets() + right->num_sets() >
          spot::acc_cond::mark_t::max_accsets()))
702 703 704 705 706 707 708 709 710 711 712
    {
      left = ensure_tba(left);
      right = ensure_tba(right);
    }
  return spot::product(left, right);
}

static spot::twa_graph_ptr
product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right)
{
  if ((type == spot::postprocessor::BA)
713 714
      && (left->num_sets() + right->num_sets() >
          spot::acc_cond::mark_t::max_accsets()))
715 716 717 718 719 720 721
    {
      left = ensure_tba(left);
      right = ensure_tba(right);
    }
  return spot::product_or(left, right);
}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
722 723 724
static int
parse_opt(int key, char* arg, struct argp_state*)
{
725 726
  // Called from C code, so should not raise any exception.
  BEGIN_EXCEPTION_PROTECT;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
727 728 729
  // This switch is alphabetically-ordered.
  switch (key)
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
730
    case 'c':
731
      automaton_format = Count;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
732
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
733 734 735
    case 'F':
      jobs.emplace_back(arg, true);
      break;
736
    case 'n':
737
      opt_max_count = to_pos_int(arg, "-n/--max-count");
738
      break;
739 740 741
    case 'N':
      opt_nth = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
742
    case 'u':
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
743
      opt->uniq = std::unique_ptr<unique_aut_t>(new std::set<canon_aut>());
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
744
      break;
745 746 747
    case 'v':
      opt_invert = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
748 749
    case 'x':
      {
750 751 752
        const char* opt = extra_options.parse_options(arg);
        if (opt)
          error(2, 0, "failed to parse --options near '%s'", opt);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
753 754
      }
      break;
755 756 757
    case OPT_AP_N:
      opt_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
758 759 760
    case OPT_ACC_SETS:
      opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
761 762 763 764
    case OPT_ACC_SCCS:
      opt_acc_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
765
    case OPT_ACCEPT_WORD:
766
      try
767 768 769 770
        {
          opt->acc_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
771
      catch (const spot::parse_error& e)
772 773 774 775
        {
          error(2, 0, "failed to parse the argument of --accept-word:\n%s",
                e.what());
        }
776
      break;
777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807
    case OPT_ACCEPTANCE_IS:
      {
        auto res = argmatch(arg, acc_is_args,
                            (char const*) acc_is_types, sizeof(acc_type));
        if (res >= 0)
          opt_acceptance_is = acc_is_types[res];
        else
          {
            try
              {
                opt_acceptance_is_given =
                  spot::acc_cond(spot::acc_cond::acc_code(arg));
                opt_acceptance_is = ACC_Given;
              }
            catch (const spot::parse_error& err)
              {
                std::cerr << program_name << ": failed to parse '" << arg
                          << ("' as an acceptance formula for "
                              "--acceptance-is\n\t")
                          << err.what()
                          << ("\nIf you do not want to supply a formula, the "
                              "following names are recognized:");
                acc_type last_val = ACC_Any;
                for (int i = 0; acc_is_args[i]; i++)
                  if ((i == 0) || last_val != acc_is_types[i])
                    {
                      std::cerr << "\n  - '" << acc_is_args[i] << '\'';
                      last_val = acc_is_types[i];
                    }
                  else
                    {
808
                      std::cerr << ", '" << acc_is_args[i] << '\'';
809
                    }
810
                std::cerr << '\n';
811 812 813 814 815
                exit(2);
              }
          }
      }
      break;
816
    case OPT_ARE_ISOMORPHIC:
817
      opt->are_isomorphic = read_automaton(arg, opt->dict);
818
      break;
819 820 821
    case OPT_CLEAN_ACC:
      opt_clean_acc = true;
      break;
822 823 824 825
    case OPT_CNF_ACC:
      opt_dnf_acc = false;
      opt_cnf_acc = true;
      break;
826
    case OPT_COMPLEMENT:
Thomas Medioni's avatar
Thomas Medioni committed
827 828 829
      if (opt_dualize)
        error(2, 0, "either --complement or --dualize options"
                    " can be given, not both");
830 831
      opt_complement = true;
      break;
832 833 834
    case OPT_COMPLEMENT_ACC:
      opt_complement_acc = true;
      break;
835 836 837
     case OPT_DCA:
      opt_dca = true;
      break;
838
    case OPT_DECOMPOSE_SCC:
839
      opt_decompose_scc = arg;
840
      break;
841 842 843
    case OPT_DESTUT:
      opt_destut = true;
      break;
Thomas Medioni's avatar
Thomas Medioni committed
844 845 846 847 848 849
    case OPT_DUALIZE:
      if (opt_complement)
        error(2, 0, "either --complement or --dualize options"
                    " can be given, not both");
      opt_dualize = true;
      break;
850 851
    case OPT_DNF_ACC:
      opt_dnf_acc = true;
852
      opt_cnf_acc = false;
853
      break;
854 855 856
    case OPT_STREETT_LIKE:
      opt_streett_like = true;
      break;
857 858 859
    case OPT_EDGES:
      opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
860
    case OPT_EXCLUSIVE_AP:
861
      opt->excl_ap.add_group(arg);
862
      break;
863 864
    case OPT_EQUIVALENT_TO:
      if (opt->equivalent_pos)
865
        error(2, 0, "only one --equivalent-to option can be given");
866 867
      opt->equivalent_pos = read_automaton(arg, opt->dict);
      opt->equivalent_neg =
868
        spot::dualize(ensure_deterministic(opt->equivalent_pos, true));
869
      break;
870 871 872 873 874 875 876 877 878 879 880 881 882 883
    case OPT_GENERALIZED_RABIN:
      if (arg)
        opt_gra = XARGMATCH("--generalized-rabin", arg, gra_args, gra_types);
      else
        opt_gra = GRA_UNIQUE_INF;
      opt_gsa = GSA_NO;
      break;
    case OPT_GENERALIZED_STREETT:
      if (arg)
        opt_gsa = XARGMATCH("--generalized-streett", arg, gsa_args, gsa_types);
      else
        opt_gsa = GSA_UNIQUE_FIN;
      opt_gra = GRA_NO;
      break;
884 885 886 887 888 889
    case OPT_HAS_EXIST_BRANCHING:
      opt_has_exist_branching = true;
      break;
    case OPT_HAS_UNIV_BRANCHING:
      opt_has_univ_branching = true;
      break;
890 891 892 893
    case OPT_HIGHLIGHT_ACCEPTING_RUN:
      opt_highlight_accepting_run =
        arg ? to_pos_int(arg, "--highlight-accepting-run") : 1;
      break;
894 895
    case OPT_HIGHLIGHT_NONDET:
      {
896
        int v = arg ? to_pos_int(arg, "--highlight-nondet") : 1;
897 898 899 900
        opt_highlight_nondet_edges = opt_highlight_nondet_states = v;
        break;
      }
    case OPT_HIGHLIGHT_NONDET_STATES:
901 902
      opt_highlight_nondet_states =
        arg ? to_pos_int(arg, "--highlight-nondet-states") : 1;
903 904
      break;
    case OPT_HIGHLIGHT_NONDET_EDGES:
905 906
      opt_highlight_nondet_edges =
        arg ? to_pos_int(arg, "--highlight-nondet-edges") : 1;
907
      break;
908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939
    case OPT_HIGHLIGHT_WORD:
      {
        char* endptr;
        int res = strtol(arg, &endptr, 10);
        if (endptr == arg)
          {
            res = 1;
          }
        else
          {
            if (res < 0)
              error(2, 0, "failed to parse the argument of --highlight-word: "
                    "%d is not positive", res);
            while (std::isspace(*endptr))
              ++endptr;
            if (*endptr != ',')
              error(2, 0, "failed to parse the argument of --highlight-word: "
                    "%d should be followed by a comma and WORD", res);
            arg = endptr + 1;
          }
        try
          {
            opt->hl_words.emplace_back(spot::parse_word(arg, opt->dict)
                                       ->as_automaton(), res);
          }
        catch (const spot::parse_error& e)
          {
            error(2, 0, "failed to parse the argument of --highlight-word:\n%s",
                  e.what());
          }
      }
      break;
940 941 942
    case OPT_HIGHLIGHT_LANGUAGES:
      opt_highlight_languages = true;
      break;
943
    case OPT_INSTUT:
944
      if (!arg || (arg[0] == '1' && arg[1] == 0))
945
        opt_instut = 1;
946
      else if (arg[0] == '2' && arg[1] == 0)
947
        opt_instut = 2;
948
      else
949
        error(2, 0, "unknown argument for --instut: %s", arg);
950
      break;
951 952
    case OPT_INCLUDED_IN:
      {
953
        auto aut = ensure_deterministic(read_automaton(arg, opt->dict), true);
954
        aut = spot::dualize(aut);
955 956 957 958
        if (!opt->included_in)
          opt->included_in = aut;
        else
          opt->included_in = spot::product_or(opt->included_in, aut);
959 960
      }
      break;
961 962 963 964 965
    case OPT_INHERENTLY_WEAK_SCCS:
      opt_inhweak_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_inhweak_sccs_set = true;
      opt_art_sccs_set = true;
      break;
966
    case OPT_INTERSECT:
967
      opt->intersect = read_automaton(arg, opt->dict);
968
      break;
969 970 971
    case OPT_IS_ALTERNATING:
      opt_is_alternating = true;
      break;
972 973 974
    case OPT_IS_COLORED:
      opt_is_colored = true;
      break;
975 976 977 978 979 980
    case OPT_IS_COMPLETE:
      opt_is_complete = true;
      break;
    case OPT_IS_DETERMINISTIC:
      opt_is_deterministic = true;
      break;
981 982 983
    case OPT_IS_EMPTY:
      opt_is_empty = true;
      break;
984 985 986
    case OPT_IS_INHERENTLY_WEAK:
      opt_is_inherently_weak = true;
      break;
987 988 989
    case OPT_IS_VERY_WEAK:
      opt_is_very_weak = true;
      break;
990 991 992
    case OPT_IS_SEMI_DETERMINISTIC:
      opt_is_semi_deterministic = true;
      break;
993 994
    case OPT_IS_STUTTER_INVARIANT:
      opt_is_stutter_invariant = true;
995
      break;
996 997 998
    case OPT_IS_TERMINAL:
      opt_is_terminal = true;
      break;
999 1000 1001
    case OPT_IS_UNAMBIGUOUS:
      opt_is_unambiguous = true;
      break;
1002 1003 1004
    case OPT_IS_WEAK:
      opt_is_weak = true;
      break;
1005 1006 1007 1008 1009 1010
    case OPT_KEEP_STATES:
      {
        std::vector<long> values = to_longs(arg);
        if (!values.empty())
          opt_keep_states_initial = values[0];
        for (auto res : values)
1011 1012 1013 1014
          {
            if (res < 0)
              error(2, 0, "state ids should be non-negative:"
                    " --mask-acc=%ld", res);
1015 1016 1017
            // We don't know yet how many states the automata contain.
            if (opt_keep_states.size() <= static_cast<unsigned long>(res))
              opt_keep_states.resize(res + 1, false);
1018 1019 1020
            opt_keep_states[res] = true;
          }
        break;
1021
      }
1022 1023 1024 1025 1026 1027 1028 1029 1030 1031
    case OPT_MERGE:
      opt_merge = true;
      break;
    case OPT_MASK_ACC:
      {
        for (auto res : to_longs(arg))
          {
            if (res < 0)
              error(2, 0, "acceptance sets should be non-negative:"
                    " --mask-acc=%ld", res);
1032 1033
            if (static_cast<unsigned long>(res) >=
                spot::acc_cond::mark_t::max_accsets())
1034 1035 1036 1037 1038 1039 1040 1041 1042 1043
              error(2, 0, "this implementation does not support that many"
                    " acceptance sets: --mask-acc=%ld", res);
            opt_mask_acc.set(res);
          }
        break;
      }
    case OPT_NONDET_STATES:
      opt_nondet_states = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_nondet_states_set = true;
      break;
1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060
    case OPT_PARTIAL_DEGEN:
      {
        opt_partial_degen_set = true;
        if (arg)
          for (auto res : to_longs(arg))
            {
              if (res < 0)
                error(2, 0, "acceptance sets should be non-negative:"
                      " --partial-degeneralize=%ld", res);
              if (static_cast<unsigned long>(res) >=
                  spot::acc_cond::mark_t::max_accsets())
                error(2, 0, "this implementation does not support that many"
                      " acceptance sets: --partial-degeneralize=%ld", res);
              opt_partial_degen.set(res);
            }
        break;
      }
1061
    case OPT_PRODUCT_AND:
1062
      {
1063 1064 1065 1066
        auto a = read_automaton(arg, opt->dict);
        if (!opt->product_and)
          opt->product_and = std::move(a);
        else
1067 1068
          opt->product_and = ::product(std::move(opt->product_and),
                                       std::move(a));
1069 1070 1071 1072
      }
      break;
    case OPT_PRODUCT_OR:
      {
1073 1074 1075 1076
        auto a = read_automaton(arg, opt->dict);
        if (!opt->product_or)
          opt->product_or = std::move(a);
        else
1077 1078
          opt->product_or = ::product_or(std::move(opt->product_or),
                                         std::move(a));
1079 1080
      }
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1081 1082
    case OPT_RANDOMIZE:
      if (arg)
1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096
        {
          for (auto p = arg; *p; ++p)
            switch (*p)
              {
              case 's':
                randomize_st = true;
                break;
              case 't':
                randomize_tr = true;
                break;
              default:
                error(2, 0, "unknown argument for --randomize: '%c'", *p);
              }
        }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1097
      else
1098 1099 1100 1101
        {
          randomize_tr = true;
          randomize_st = true;
        }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1102
      break;
1103 1104 1105 1106
    case OPT_REJ_SCCS:
      opt_rej_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
1107 1108
    case OPT_REJECT_WORD:
      try
1109 1110 1111 1112
        {
          opt->rej_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
1113
      catch (const spot::parse_error& e)
1114 1115 1116 1117
        {
          error(2, 0, "failed to parse the argument of --reject-word:\n%s",
                e.what());
        }
1118
      break;
1119
    case OPT_REM_AP:
1120
      opt->rem_ap.add_ap(arg);
1121
      break;
1122 1123 1124
    case OPT_REM_DEAD:
      opt_rem_dead = true;
      break;
1125 1126 1127
    case OPT_REM_FIN:
      opt_rem_fin = true;
      break;
1128 1129 1130
    case OPT_REM_UNREACH:
      opt_rem_unreach = true;
      break;
1131 1132 1133
    case OPT_REM_UNUSED_AP:
      opt_rem_unused_ap = true;
      break;
1134 1135 1136
    case OPT_SAT_MINIMIZE:
      opt_sat_minimize = arg ? arg : "";
      break;
1137 1138 1139 1140
    case OPT_SCCS:
      opt_sccs_set = true;
      opt_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1141
    case OPT_SEED:
1142
      opt_seed = to_int(arg, "--seed");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1143
      break;
1144 1145 1146
    case OPT_SEP_SETS:
      opt_sep_sets = true;
      break;
1147 1148 1149
    case OPT_SIMPL_ACC:
      opt_simpl_acc = true;
      break;
1150 1151 1152 1153
    case OPT_SIMPLIFY_EXCLUSIVE_AP:
      opt_simplify_exclusive_ap = true;
      opt_merge = true;
      break;
1154 1155 1156
    case OPT_SPLIT_EDGES:
      opt_split_edges = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1157 1158 1159
    case OPT_STATES:
      opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
1160 1161 1162
    case OPT_STRIPACC:
      opt_stripacc = true;
      break;
1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182
    case OPT_SUM_OR:
      {
        auto a = read_automaton(arg, opt->dict);
        if (!opt->sum_or)
          opt->sum_or = std::move(a);
        else
          opt->sum_or = spot::sum(std::move(opt->sum_or),
                                  std::move(a));
      }
      break;
    case OPT_SUM_AND:
      {
        auto a = read_automaton(arg, opt->dict);
        if