autfilt.cc 51.9 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
// et Développement 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
52
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/dtwasat.hh>
53
#include <spot/twaalgos/dualize.hh>
54
#include <spot/twaalgos/gtec/gtec.hh>
55
#include <spot/twaalgos/hoa.hh>
56
57
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/isunamb.hh>
58
#include <spot/twaalgos/isweakscc.hh>
59
#include <spot/twaalgos/langmap.hh>
60
61
62
63
64
65
66
67
68
69
70
71
72
#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
73

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
74
static const char argp_program_doc[] ="\
75
Convert, transform, and filter omega-automata.\v\
76
77
78
79
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
80

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

157
158
#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
159
160
161
static const argp_option options[] =
  {
    /**************************************************/
162
    { nullptr, 0, nullptr, 0, "Input:", 1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
163
164
165
    { "file", 'F', "FILENAME", 0,
      "process the automaton in FILENAME", 0 },
    /**************************************************/
166
    { "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
167
    { "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
168
    /**************************************************/
169
170
171
172
173
174
175
176
177
    { 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 },
178
179
    { "acceptance-is", OPT_ACCEPTANCE_IS, "NAME|FORMULA", 0,
      "match automata with given accetance condition", 0 },
180
181
182
183
184
185
186
187
188
189
    { "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,
      "do not output the same automaton twice (same in the sense that they "\
      "are isomorphic)", 0 },
    { "is-complete", OPT_IS_COMPLETE, nullptr, 0,
      "keep complete automata", 0 },
    { "is-deterministic", OPT_IS_DETERMINISTIC, nullptr, 0,
      "keep deterministic automata", 0 },
190
191
    { "is-semi-deterministic", OPT_IS_SEMI_DETERMINISTIC, nullptr, 0,
      "keep semi-deterministic automata", 0 },
192
193
    { "is-empty", OPT_IS_EMPTY, nullptr, 0,
      "keep automata with an empty language", 0 },
194
195
    { "is-stutter-invariant", OPT_IS_STUTTER_INVARIANT, nullptr, 0,
      "keep automata representing stutter-invariant properties", 0 },
196
197
    { "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
      "keep only terminal automata", 0 },
198
199
    { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
      "keep only unambiguous automata", 0 },
200
201
202
203
    { "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 },
204
205
    { "is-very-weak", OPT_IS_VERY_WEAK, nullptr, 0,
      "keep only very-weak automata", 0 },
206
207
    { "is-alternating", OPT_IS_ALTERNATING, nullptr, 0,
      "keep only automata using universal branching", 0 },
208
209
210
211
212
213
214
215
216
217
218
219
220
221
    { "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,
      "keep automata thare are equivalent (language-wise) to the automaton "
      "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 },
222
223
    { "nondet-states", OPT_NONDET_STATES, "RANGE", 0,
      "keep automata whose number of nondeterministic states is in RANGE", 0 },
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
    { "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 },
    /**************************************************/
    RANGE_DOC_FULL,
    WORD_DOC,
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Transformations:", 7 },
258
    { "merge-transitions", OPT_MERGE, nullptr, 0,
259
      "merge transitions with same destination and acceptance", 0 },
260
261
262
    { "product", OPT_PRODUCT_AND, "FILENAME", 0,
      "build the product with the automaton in FILENAME "
      "to intersect languages", 0 },
263
    { "product-and", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
264
265
266
    { "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
267
    { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
268
      "randomize states and transitions (specify 's' or 't' to "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
269
      "randomize only states or transitions)", 0 },
270
271
    { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL,
      "allow more stuttering (two possible algorithms)", 0 },
272
    { "destut", OPT_DESTUT, nullptr, 0, "allow less stuttering", 0 },
273
274
    { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
      "remove all transitions in specified acceptance sets", 0 },
275
    { "strip-acceptance", OPT_STRIPACC, nullptr, 0,
276
      "remove the acceptance condition and all acceptance sets", 0 },
277
278
    { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
      "only keep specified states.  The first state will be the new "\
279
      "initial state.  Implies --remove-unreachable-states.", 0 },
280
    { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
281
      "put the acceptance condition in Disjunctive Normal Form", 0 },
282
283
284
    { "streett-like", OPT_STREETT_LIKE, nullptr, 0,
      "convert to an automaton with Streett-like acceptance. Works only with "
      "acceptance condition in DNF", 0 },
285
    { "cnf-acceptance", OPT_CNF_ACC, nullptr, 0,
286
      "put the acceptance condition in Conjunctive Normal Form", 0 },
287
    { "remove-fin", OPT_REM_FIN, nullptr, 0,
288
      "rewrite the automaton without using Fin acceptance", 0 },
289
290
291
292
293
294
295
296
297
298
299
300
301
302
    { "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 },
303
    { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
304
      "remove unused acceptance sets from the automaton", 0 },
305
306
307
    { "complement", OPT_COMPLEMENT, nullptr, 0,
      "complement each automaton (currently support only deterministic "
      "automata)", 0 },
308
    { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
309
310
      "complement the acceptance condition (without touching the automaton)",
      0 },
311
    { "decompose-scc", OPT_DECOMPOSE_SCC, "t|w|s|N|aN", 0,
312
      "extract the (t) terminal, (w) weak, or (s) strong part of an automaton"
313
      " or (N) the subautomaton leading to the Nth SCC, or (aN) to the Nth "
Clément Gillard's avatar
Clément Gillard committed
314
      "accepting SCC (option can be combined with commas to extract multiple "
315
316
      "parts)", 0 },
    { "decompose-strength", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
Thomas Medioni's avatar
Thomas Medioni committed
317
318
    { "dualize", OPT_DUALIZE, nullptr, 0,
      "dualize each automaton", 0 },
319
320
321
322
323
    { "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 },
324
    { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, nullptr, 0,
325
326
327
      "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 },
328
329
330
    { "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 },
331
332
    { "remove-unused-ap", OPT_REM_UNUSED_AP, nullptr, 0,
      "remove declared atomic propositions that are not used", 0 },
333
    { "remove-unreachable-states", OPT_REM_UNREACH, nullptr, 0,
334
      "remove states that are unreachable from the initial state", 0 },
335
    { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
336
337
      "remove states that are unreachable, or that cannot belong to an "
      "infinite path", 0 },
338
339
340
    { "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 },
341
342
343
    { "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 },
344
345
346
347
348
349
350
    { "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 },
351
    { "separate-sets", OPT_SEP_SETS, nullptr, 0,
352
353
      "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 },
354
    { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL,
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
355
      "minimize the automaton using a SAT solver (only works for deterministic"
356
357
358
359
360
361
      " 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 },
362
363
364
365
366
367
    { "dca", OPT_DCA, nullptr, 0,
      "convert to deterministic co-Büchi. The resulting automaton will always "
      "recognize at least the same language. Actually, it can recognize "
      "more if the original language can not be expressed using a co-Büchi "
      "acceptance condition."
      , 0 },
368
    { nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 9 },
369
370
    { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM",
371
      0 },
372
373
    { "highlight-nondet-edges", OPT_HIGHLIGHT_NONDET_EDGES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic edges with color NUM",
374
      0 },
375
376
377
    { "highlight-nondet", OPT_HIGHLIGHT_NONDET, "NUM",
      OPTION_ARG_OPTIONAL,
      "highlight nondeterministic states and edges with color NUM", 0},
378
379
    { "highlight-word", OPT_HIGHLIGHT_WORD, "[NUM,]WORD", 0,
      "highlight one run matching WORD using color NUM", 0},
380
    { "highlight-languages", OPT_HIGHLIGHT_LANGUAGES, nullptr, 0 ,
381
      "highlight states that recognize identical languages", 0},
382
    /**************************************************/
383
384
    { nullptr, 0, nullptr, 0,
      "If any option among --small, --deterministic, or --any is given, "
385
      "then the simplification level defaults to --high unless specified "
386
      "otherwise.  If any option among --low, --medium, or --high is given, "
387
      "then the simplification goal defaults to --small unless specified "
388
389
390
      "otherwise.  If none of those options are specified, then autfilt "
      "acts as is --any --low were given: these actually disable the "
      "simplification routines.", 22 },
391
    /**************************************************/
392
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
393
394
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
395
396
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
397
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
398
399
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
400
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
401
  {
402
    { &hoaread_argp, 0, nullptr, 0 },
403
404
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
405
    { &post_argp_disabled, 0, nullptr, 0 },
406
407
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
408
409
  };

410

411
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
412
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
413
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
414
415
416
417
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
418

419
420
421
422
423
424
425
426
427
428
429
430
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);

431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
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
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);

524
525
526
527
528
529
530
531
532
533
534
535
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);

536
// We want all these variables to be destroyed when we exit main, to
537
538
539
540
541
542
// 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();
543
544
  spot::twa_graph_ptr product_and = nullptr;
  spot::twa_graph_ptr product_or = nullptr;
545
546
  spot::twa_graph_ptr sum_and = nullptr;
  spot::twa_graph_ptr sum_or = nullptr;
547
  spot::twa_graph_ptr intersect = nullptr;
548
  spot::twa_graph_ptr included_in = nullptr;
549
550
  spot::twa_graph_ptr equivalent_pos = nullptr;
  spot::twa_graph_ptr equivalent_neg = nullptr;
551
  spot::twa_graph_ptr are_isomorphic = nullptr;
552
553
554
  std::unique_ptr<spot::isomorphism_checker>
                         isomorphism_checker = nullptr;
  std::unique_ptr<unique_aut_t> uniq = nullptr;
555
556
  spot::exclusive_ap excl_ap;
  spot::remove_ap rem_ap;
557
  std::vector<spot::twa_graph_ptr> acc_words;
558
  std::vector<spot::twa_graph_ptr> rej_words;
559
  std::vector<std::pair<spot::twa_graph_ptr, unsigned>> hl_words;
560
561
}* opt;

562
static bool opt_merge = false;
563
static bool opt_is_alternating = false;
564
565
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
566
static bool opt_is_semi_deterministic = false;
567
static bool opt_is_unambiguous = false;
568
569
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
570
static bool opt_is_inherently_weak = false;
571
static bool opt_is_very_weak = false;
572
static bool opt_is_stutter_invariant = false;
573
static bool opt_invert = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
574
static range opt_states = { 0, std::numeric_limits<int>::max() };
575
576
static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() };
577
static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
578
579
580
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;
581
582
583
584
585
586
587
588
589
590
591
592
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;
593
594
static range opt_nondet_states = { 0, std::numeric_limits<int>::max() };
static bool opt_nondet_states_set = false;
595
static int opt_max_count = -1;
596
static bool opt_destut = false;
597
static char opt_instut = 0;
598
static bool opt_is_empty = false;
599
static bool opt_stripacc = false;
600
static bool opt_dnf_acc = false;
601
static bool opt_cnf_acc = false;
602
static bool opt_rem_fin = false;
603
static bool opt_clean_acc = false;
604
static bool opt_complement = false;
605
static bool opt_complement_acc = false;
606
static char* opt_decompose_scc = nullptr;
Thomas Medioni's avatar
Thomas Medioni committed
607
static bool opt_dualize = false;
608
static spot::acc_cond::mark_t opt_mask_acc = 0U;
609
610
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
611
static bool opt_simpl_acc = false;
612
static bool opt_simplify_exclusive_ap = false;
613
614
static bool opt_rem_dead = false;
static bool opt_rem_unreach = false;
615
static bool opt_rem_unused_ap = false;
616
static bool opt_sep_sets = false;
617
static bool opt_split_edges = false;
618
static const char* opt_sat_minimize = nullptr;
619
620
static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1;
621
static bool opt_highlight_languages = false;
622
static bool opt_dca = false;
623
static bool opt_streett_like = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
624

625
static spot::twa_graph_ptr
626
ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
627
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
628
  if ((!nonalt || aut->is_existential()) && spot::is_universal(aut))
629
630
631
632
633
634
635
636
    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);
}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
637
638
639
640
641
642
static int
parse_opt(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
643
    case 'c':
644
      automaton_format = Count;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
645
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
646
647
648
    case 'F':
      jobs.emplace_back(arg, true);
      break;
649
650
651
    case 'n':
      opt_max_count = to_pos_int(arg);
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
652
    case 'u':
653
      opt->uniq =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
654
655
        std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
      break;
656
657
658
    case 'v':
      opt_invert = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
659
660
    case 'x':
      {
661
662
663
        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
664
665
      }
      break;
666
667
668
    case OPT_AP_N:
      opt_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
669
670
671
    case OPT_ACC_SETS:
      opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
672
673
674
675
    case OPT_ACC_SCCS:
      opt_acc_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
676
    case OPT_ACCEPT_WORD:
677
      try
678
679
680
681
        {
          opt->acc_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
682
      catch (const spot::parse_error& e)
683
684
685
686
        {
          error(2, 0, "failed to parse the argument of --accept-word:\n%s",
                e.what());
        }
687
      break;
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
    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
                    {
                      std::cerr << ", '" << acc_is_args[i] << '"';
                    }
                std::cerr << std::flush;
                exit(2);
              }
          }
      }
      break;
727
    case OPT_ARE_ISOMORPHIC:
728
      opt->are_isomorphic = read_automaton(arg, opt->dict);
729
      break;
730
731
732
    case OPT_CLEAN_ACC:
      opt_clean_acc = true;
      break;
733
734
735
736
    case OPT_CNF_ACC:
      opt_dnf_acc = false;
      opt_cnf_acc = true;
      break;
737
    case OPT_COMPLEMENT:
Thomas Medioni's avatar
Thomas Medioni committed
738
739
740
      if (opt_dualize)
        error(2, 0, "either --complement or --dualize options"
                    " can be given, not both");
741
742
      opt_complement = true;
      break;
743
744
745
    case OPT_COMPLEMENT_ACC:
      opt_complement_acc = true;
      break;
746
747
748
     case OPT_DCA:
      opt_dca = true;
      break;
749
    case OPT_DECOMPOSE_SCC:
750
      opt_decompose_scc = arg;
751
      break;
752
753
754
    case OPT_DESTUT:
      opt_destut = true;
      break;
Thomas Medioni's avatar
Thomas Medioni committed
755
756
757
758
759
760
    case OPT_DUALIZE:
      if (opt_complement)
        error(2, 0, "either --complement or --dualize options"
                    " can be given, not both");
      opt_dualize = true;
      break;
761
762
    case OPT_DNF_ACC:
      opt_dnf_acc = true;
763
      opt_cnf_acc = false;
764
      break;
765
766
767
    case OPT_STREETT_LIKE:
      opt_streett_like = true;
      break;
768
769
770
    case OPT_EDGES:
      opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
771
    case OPT_EXCLUSIVE_AP:
772
      opt->excl_ap.add_group(arg);
773
      break;
774
775
    case OPT_EQUIVALENT_TO:
      if (opt->equivalent_pos)
776
        error(2, 0, "only one --equivalent-to option can be given");
777
778
      opt->equivalent_pos = read_automaton(arg, opt->dict);
      opt->equivalent_neg =
779
        spot::dualize(ensure_deterministic(opt->equivalent_pos, true));
780
      break;
781
782
783
784
785
786
787
788
789
790
791
792
793
794
    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;
795
796
797
798
799
800
801
802
803
804
805
806
    case OPT_HIGHLIGHT_NONDET:
      {
        int v = arg ? to_pos_int(arg) : 1;
        opt_highlight_nondet_edges = opt_highlight_nondet_states = v;
        break;
      }
    case OPT_HIGHLIGHT_NONDET_STATES:
      opt_highlight_nondet_states = arg ? to_pos_int(arg) : 1;
      break;
    case OPT_HIGHLIGHT_NONDET_EDGES:
      opt_highlight_nondet_edges = arg ? to_pos_int(arg) : 1;
      break;
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
    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;
839
840
841
    case OPT_HIGHLIGHT_LANGUAGES:
      opt_highlight_languages = true;
      break;
842
    case OPT_INSTUT:
843
      if (!arg || (arg[0] == '1' && arg[1] == 0))
844
        opt_instut = 1;
845
      else if (arg[0] == '2' && arg[1] == 0)
846
        opt_instut = 2;
847
      else
848
        error(2, 0, "unknown argument for --instut: %s", arg);
849
      break;
850
851
    case OPT_INCLUDED_IN:
      {
852
        auto aut = ensure_deterministic(read_automaton(arg, opt->dict), true);
853
        aut = spot::dualize(aut);
854
855
856
857
        if (!opt->included_in)
          opt->included_in = aut;
        else
          opt->included_in = spot::product_or(opt->included_in, aut);
858
859
      }
      break;
860
861
862
863
864
    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;
865
    case OPT_INTERSECT:
866
      opt->intersect = read_automaton(arg, opt->dict);
867
      break;
868
869
870
    case OPT_IS_ALTERNATING:
      opt_is_alternating = true;
      break;
871
872
873
874
875
876
    case OPT_IS_COMPLETE:
      opt_is_complete = true;
      break;
    case OPT_IS_DETERMINISTIC:
      opt_is_deterministic = true;
      break;
877
878
879
    case OPT_IS_EMPTY:
      opt_is_empty = true;
      break;
880
881
882
    case OPT_IS_INHERENTLY_WEAK:
      opt_is_inherently_weak = true;
      break;
883
884
885
    case OPT_IS_VERY_WEAK:
      opt_is_very_weak = true;
      break;
886
887
888
    case OPT_IS_SEMI_DETERMINISTIC:
      opt_is_semi_deterministic = true;
      break;
889
890
    case OPT_IS_STUTTER_INVARIANT:
      opt_is_stutter_invariant = true;
891
      break;
892
893
894
    case OPT_IS_TERMINAL:
      opt_is_terminal = true;
      break;
895
896
897
    case OPT_IS_UNAMBIGUOUS:
      opt_is_unambiguous = true;
      break;
898
899
900
    case OPT_IS_WEAK:
      opt_is_weak = true;
      break;
901
902
903
904
905
906
    case OPT_KEEP_STATES:
      {
        std::vector<long> values = to_longs(arg);
        if (!values.empty())
          opt_keep_states_initial = values[0];
        for (auto res : values)
907
908
909
910
          {
            if (res < 0)
              error(2, 0, "state ids should be non-negative:"
                    " --mask-acc=%ld", res);
911
912
913
            // 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);
914
915
916
            opt_keep_states[res] = true;
          }
        break;
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_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);
            if (static_cast<unsigned long>(res)
                > sizeof(spot::acc_cond::mark_t::value_t))
              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;
940
    case OPT_PRODUCT_AND:
941
      {
942
943
944
945
946
947
        auto a = read_automaton(arg, opt->dict);
        if (!opt->product_and)
          opt->product_and = std::move(a);
        else
          opt->product_and = spot::product(std::move(opt->product_and),
                                           std::move(a));
948
949
950
951
      }
      break;
    case OPT_PRODUCT_OR:
      {
952
953
954
955
956
957
        auto a = read_automaton(arg, opt->dict);
        if (!opt->product_or)
          opt->product_or = std::move(a);
        else
          opt->product_or = spot::product_or(std::move(opt->product_or),
                                             std::move(a));
958
959
      }
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
960
961
    case OPT_RANDOMIZE:
      if (arg)
962
963
964
965
966
967
968
969
970
971
972
973
974
975
        {
          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
976
      else
977
978
979
980
        {
          randomize_tr = true;
          randomize_st = true;
        }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
981
      break;
982
983
984
985
    case OPT_REJ_SCCS:
      opt_rej_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
986
987
    case OPT_REJECT_WORD:
      try
988
989
990
991
        {
          opt->rej_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
992
      catch (const spot::parse_error& e)
993
994
995
996
        {
          error(2, 0, "failed to parse the argument of --reject-word:\n%s",
                e.what());
        }
997
      break;
998
    case OPT_REM_AP:
999
      opt->rem_ap.add_ap(arg);
1000
      break;
1001
1002
1003
    case OPT_REM_DEAD:
      opt_rem_dead = true;
      break;
1004
1005
1006
    case OPT_REM_FIN:
      opt_rem_fin = true;
      break;
1007
1008
1009
    case OPT_REM_UNREACH:
      opt_rem_unreach = true;
      break;
1010
1011
1012
    case OPT_REM_UNUSED_AP:
      opt_rem_unused_ap = true;
      break;
1013
1014
1015
    case OPT_SAT_MINIMIZE:
      opt_sat_minimize = arg ? arg : "";
      break;
1016
1017
1018
1019
    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
1020
1021
1022
    case OPT_SEED:
      opt_seed = to_int(arg);
      break;
1023
1024
1025
    case OPT_SEP_SETS:
      opt_sep_sets = true;
      break;
1026
1027
1028
    case OPT_SIMPL_ACC:
      opt_simpl_acc = true;
      break;
1029
1030
1031
1032
    case OPT_SIMPLIFY_EXCLUSIVE_AP:
      opt_simplify_exclusive_ap = true;
      opt_merge = true;
      break;
1033
1034
1035
    case OPT_SPLIT_EDGES:
      opt_split_edges = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1036
1037
1038
    case OPT_STATES:
      opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
1039
1040
1041
    case OPT_STRIPACC:
      opt_stripacc = true;
      break;
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
    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 (!opt->sum_and)
          opt->sum_and = std::move(a);
        else
          opt->sum_and = spot::sum_and(std::move(opt->sum_and),
                                       std::move(a));
      }
      break;
1062
1063
1064
1065
1066
1067
1068
1069
1070
    case OPT_TERMINAL_SCCS:
      opt_terminal_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_terminal_sccs_set = true;
      opt_art_sccs_set = true;
      break;
    case OPT_TRIV_SCCS:
      opt_triv_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
1071
1072
1073
1074
1075
1076
1077
1078
    case OPT_USED_AP_N:
      opt_used_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
      need_unused_ap_count = true;
      break;
    case OPT_UNUSED_AP_N:
      opt_unused_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
      need_unused_ap_count = true;
      break;
1079
1080
1081
1082
1083
    case OPT_WEAK_SCCS:
      opt_weak_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_weak_sccs_set = true;
      opt_art_sccs_set = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
    case ARGP_KEY_ARG:
      jobs.emplace_back(arg, true);
      break;

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
static int unused_ap(const spot::const_twa_graph_ptr& aut)
{
  bdd all = aut->ap_vars();
  for (auto& e: aut->edges())
    {
      all = bdd_exist(all, bdd_support(e.cond));
      if (all == bddtrue)    // All APs are used.
        return 0;
    }
  int count = 0;
  while (all != bddtrue)
    {
      ++count;
      all = bdd_high(all);
    }
  return count;
}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1111
1112
1113

namespace
{
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
  static
  bool match_acceptance(spot::twa_graph_ptr aut)
  {
    auto& acc = aut->acc();
    switch (opt_acceptance_is)
      {
      case ACC_Any:
        return true;
      case ACC_Given:
        return acc == opt_acceptance_is_given;
      case ACC_tt:
        return acc.is_t();
      case ACC_ff:
        return acc.is_f();
      case ACC_Buchi:
        return acc.is_buchi();
      case ACC_GenBuchi:
        return acc.is_generalized_buchi();
      case ACC_CoBuchi:
        return acc.is_co_buchi();
      case ACC_GenCoBuchi:
        return acc.is_generalized_co_buchi();
      case ACC_Rabin:
        return acc.is_rabin() >= 0;
      case ACC_Streett:
        return acc.is_streett() >= 0;
      case ACC_GenRabin:
        {
          std::vector<unsigned> p;
          return acc.is_generalized_rabin(p);
        }
      case ACC_GenStreett:
        {
          std::vector<unsigned> p;
          return acc.is_generalized_streett(p);
        }
      case ACC_RabinLike:
        {
          std::vector<spot::acc_cond::rs_pair> p;
          return acc.is_rabin_like(p);
        }
      case ACC_StreettLike:
        {
          std::vector<spot::acc_cond::rs_pair> p;
          return acc.is_streett_like(p);
        }
      case ACC_Parity:
      case ACC_ParityMin:
      case ACC_ParityMax:
      case ACC_ParityOdd:
      case ACC_ParityEven:
      case ACC_ParityMinOdd:
      case ACC_ParityMaxOdd:
      case ACC_ParityMinEven:
      case ACC_ParityMaxEven:
        {
          bool max;
          bool odd;
          bool is_p = acc.is_parity(max, odd, true);
          if (!is_p)
            return false;
          switch (opt_acceptance_is)
            {
            case ACC_Parity:
              return true;
            case ACC_ParityMin:
              return !max;
            case ACC_ParityMax:
              return max;
            case ACC_ParityOdd:
              return odd;
            case ACC_ParityEven:
              return !odd;
            case ACC_ParityMinOdd:
              return !max && odd;
            case ACC_ParityMaxOdd:
              return max && odd;
            case ACC_ParityMinEven:
              return !max && !odd;
            case ACC_ParityMaxEven:
              return max && !odd;
            default:
              SPOT_UNREACHABLE();
            }
        }
      case ACC_FinLess:
        return !acc.uses_fin_acceptance();
      }