autfilt.cc 47.6 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
50
51
#include <spot/parseaut/public.hh>
#include <spot/tl/exclusive.hh>
#include <spot/twaalgos/are_isomorphic.hh>
#include <spot/twaalgos/canonicalize.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/dtwasat.hh>
52
#include <spot/twaalgos/dualize.hh>
53
#include <spot/twaalgos/gtec/gtec.hh>
54
#include <spot/twaalgos/hoa.hh>
55
56
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/isunamb.hh>
57
#include <spot/twaalgos/isweakscc.hh>
58
#include <spot/twaalgos/langmap.hh>
59
60
61
62
63
64
65
66
67
68
69
70
71
#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
72

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

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

154
155
#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
385
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
386
  {
387
    { &hoaread_argp, 0, nullptr, 0 },
388
389
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
390
    { &post_argp_disabled, 0, nullptr, 0 },
391
392
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
393
394
  };

395

396
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
397
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
398
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
399
400
401
402
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
403

404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
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);

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);

428
// We want all these variables to be destroyed when we exit main, to
429
430
431
432
433
434
// 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();
435
436
  spot::twa_graph_ptr product_and = nullptr;
  spot::twa_graph_ptr product_or = nullptr;
437
438
  spot::twa_graph_ptr sum_and = nullptr;
  spot::twa_graph_ptr sum_or = nullptr;
439
  spot::twa_graph_ptr intersect = nullptr;
440
  spot::twa_graph_ptr included_in = nullptr;
441
442
  spot::twa_graph_ptr equivalent_pos = nullptr;
  spot::twa_graph_ptr equivalent_neg = nullptr;
443
  spot::twa_graph_ptr are_isomorphic = nullptr;
444
445
446
  std::unique_ptr<spot::isomorphism_checker>
                         isomorphism_checker = nullptr;
  std::unique_ptr<unique_aut_t> uniq = nullptr;
447
448
  spot::exclusive_ap excl_ap;
  spot::remove_ap rem_ap;
449
  std::vector<spot::twa_graph_ptr> acc_words;
450
  std::vector<spot::twa_graph_ptr> rej_words;
451
  std::vector<std::pair<spot::twa_graph_ptr, unsigned>> hl_words;
452
453
}* opt;

454
static bool opt_merge = false;
455
static bool opt_is_alternating = false;
456
457
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
458
static bool opt_is_semi_deterministic = false;
459
static bool opt_is_unambiguous = false;
460
461
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
462
static bool opt_is_inherently_weak = false;
463
static bool opt_is_very_weak = false;
464
static bool opt_is_stutter_invariant = false;
465
static bool opt_invert = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
466
static range opt_states = { 0, std::numeric_limits<int>::max() };
467
468
static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() };
469
static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
470
471
472
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;
473
474
475
476
477
478
479
480
481
482
483
484
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;
485
486
static range opt_nondet_states = { 0, std::numeric_limits<int>::max() };
static bool opt_nondet_states_set = false;
487
static int opt_max_count = -1;
488
static bool opt_destut = false;
489
static char opt_instut = 0;
490
static bool opt_is_empty = false;
491
static bool opt_stripacc = false;
492
static bool opt_dnf_acc = false;
493
static bool opt_cnf_acc = false;
494
static bool opt_rem_fin = false;
495
static bool opt_clean_acc = false;
496
static bool opt_complement = false;
497
static bool opt_complement_acc = false;
498
static char* opt_decompose_strength = nullptr;
499
static int opt_decompose_scc = -1;
Thomas Medioni's avatar
Thomas Medioni committed
500
static bool opt_dualize = false;
501
static spot::acc_cond::mark_t opt_mask_acc = 0U;
502
503
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
504
static bool opt_simpl_acc = false;
505
static bool opt_simplify_exclusive_ap = false;
506
507
static bool opt_rem_dead = false;
static bool opt_rem_unreach = false;
508
static bool opt_rem_unused_ap = false;
509
static bool opt_sep_sets = false;
510
static bool opt_split_edges = false;
511
static const char* opt_sat_minimize = nullptr;
512
513
static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1;
514
static bool opt_highlight_languages = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
515

516
static spot::twa_graph_ptr
517
ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
518
{
519
  if ((!nonalt || aut->is_existential()) && spot::is_deterministic(aut))
520
521
522
523
524
525
526
527
    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
528
529
530
531
532
533
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
534
    case 'c':
535
      automaton_format = Count;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
536
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
537
538
539
    case 'F':
      jobs.emplace_back(arg, true);
      break;
540
541
542
    case 'n':
      opt_max_count = to_pos_int(arg);
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
543
    case 'u':
544
      opt->uniq =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
545
546
        std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
      break;
547
548
549
    case 'v':
      opt_invert = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
550
551
    case 'x':
      {
552
553
554
        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
555
556
      }
      break;
557
558
559
    case OPT_AP_N:
      opt_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
560
561
562
    case OPT_ACC_SETS:
      opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
563
564
565
566
    case OPT_ACC_SCCS:
      opt_acc_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
567
    case OPT_ACCEPT_WORD:
568
      try
569
570
571
572
        {
          opt->acc_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
573
      catch (const spot::parse_error& e)
574
575
576
577
        {
          error(2, 0, "failed to parse the argument of --accept-word:\n%s",
                e.what());
        }
578
      break;
579
    case OPT_ARE_ISOMORPHIC:
580
      opt->are_isomorphic = read_automaton(arg, opt->dict);
581
      break;
582
583
584
    case OPT_CLEAN_ACC:
      opt_clean_acc = true;
      break;
585
586
587
588
    case OPT_CNF_ACC:
      opt_dnf_acc = false;
      opt_cnf_acc = true;
      break;
589
    case OPT_COMPLEMENT:
Thomas Medioni's avatar
Thomas Medioni committed
590
591
592
      if (opt_dualize)
        error(2, 0, "either --complement or --dualize options"
                    " can be given, not both");
593
594
      opt_complement = true;
      break;
595
596
597
    case OPT_COMPLEMENT_ACC:
      opt_complement_acc = true;
      break;
598
599
600
    case OPT_DECOMPOSE_STRENGTH:
      opt_decompose_strength = arg;
      break;
601
602
603
    case OPT_DECOMPOSE_SCC:
      opt_decompose_scc = to_pos_int(arg);
      break;
604
605
606
    case OPT_DESTUT:
      opt_destut = true;
      break;
Thomas Medioni's avatar
Thomas Medioni committed
607
608
609
610
611
612
    case OPT_DUALIZE:
      if (opt_complement)
        error(2, 0, "either --complement or --dualize options"
                    " can be given, not both");
      opt_dualize = true;
      break;
613
614
    case OPT_DNF_ACC:
      opt_dnf_acc = true;
615
      opt_cnf_acc = false;
616
      break;
617
618
619
    case OPT_EDGES:
      opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
620
    case OPT_EXCLUSIVE_AP:
621
      opt->excl_ap.add_group(arg);
622
      break;
623
624
    case OPT_EQUIVALENT_TO:
      if (opt->equivalent_pos)
625
        error(2, 0, "only one --equivalent-to option can be given");
626
627
      opt->equivalent_pos = read_automaton(arg, opt->dict);
      opt->equivalent_neg =
628
        spot::dualize(ensure_deterministic(opt->equivalent_pos, true));
629
      break;
630
631
632
633
634
635
636
637
638
639
640
641
642
643
    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;
644
645
646
647
648
649
650
651
652
653
654
655
    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;
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
    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;
688
689
690
    case OPT_HIGHLIGHT_LANGUAGES:
      opt_highlight_languages = true;
      break;
691
    case OPT_INSTUT:
692
      if (!arg || (arg[0] == '1' && arg[1] == 0))
693
        opt_instut = 1;
694
      else if (arg[0] == '2' && arg[1] == 0)
695
        opt_instut = 2;
696
      else
697
        error(2, 0, "unknown argument for --instut: %s", arg);
698
      break;
699
700
    case OPT_INCLUDED_IN:
      {
701
        auto aut = ensure_deterministic(read_automaton(arg, opt->dict), true);
702
        aut = spot::dualize(aut);
703
704
705
706
        if (!opt->included_in)
          opt->included_in = aut;
        else
          opt->included_in = spot::product_or(opt->included_in, aut);
707
708
      }
      break;
709
710
711
712
713
    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;
714
    case OPT_INTERSECT:
715
      opt->intersect = read_automaton(arg, opt->dict);
716
      break;
717
718
719
    case OPT_IS_ALTERNATING:
      opt_is_alternating = true;
      break;
720
721
722
723
724
725
    case OPT_IS_COMPLETE:
      opt_is_complete = true;
      break;
    case OPT_IS_DETERMINISTIC:
      opt_is_deterministic = true;
      break;
726
727
728
    case OPT_IS_EMPTY:
      opt_is_empty = true;
      break;
729
730
731
    case OPT_IS_INHERENTLY_WEAK:
      opt_is_inherently_weak = true;
      break;
732
733
734
    case OPT_IS_VERY_WEAK:
      opt_is_very_weak = true;
      break;
735
736
737
    case OPT_IS_SEMI_DETERMINISTIC:
      opt_is_semi_deterministic = true;
      break;
738
739
    case OPT_IS_STUTTER_INVARIANT:
      opt_is_stutter_invariant = true;
740
      break;
741
742
743
    case OPT_IS_TERMINAL:
      opt_is_terminal = true;
      break;
744
745
746
    case OPT_IS_UNAMBIGUOUS:
      opt_is_unambiguous = true;
      break;
747
748
749
    case OPT_IS_WEAK:
      opt_is_weak = true;
      break;
750
751
752
753
754
755
    case OPT_KEEP_STATES:
      {
        std::vector<long> values = to_longs(arg);
        if (!values.empty())
          opt_keep_states_initial = values[0];
        for (auto res : values)
756
757
758
759
          {
            if (res < 0)
              error(2, 0, "state ids should be non-negative:"
                    " --mask-acc=%ld", res);
760
761
762
            // 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);
763
764
765
            opt_keep_states[res] = true;
          }
        break;
766
      }
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
    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;
789
    case OPT_PRODUCT_AND:
790
      {
791
792
793
794
795
796
        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));
797
798
799
800
      }
      break;
    case OPT_PRODUCT_OR:
      {
801
802
803
804
805
806
        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));
807
808
      }
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
809
810
    case OPT_RANDOMIZE:
      if (arg)
811
812
813
814
815
816
817
818
819
820
821
822
823
824
        {
          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
825
      else
826
827
828
829
        {
          randomize_tr = true;
          randomize_st = true;
        }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
830
      break;
831
832
833
834
    case OPT_REJ_SCCS:
      opt_rej_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
835
836
    case OPT_REJECT_WORD:
      try
837
838
839
840
        {
          opt->rej_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
841
      catch (const spot::parse_error& e)
842
843
844
845
        {
          error(2, 0, "failed to parse the argument of --reject-word:\n%s",
                e.what());
        }
846
      break;
847
    case OPT_REM_AP:
848
      opt->rem_ap.add_ap(arg);
849
      break;
850
851
852
    case OPT_REM_DEAD:
      opt_rem_dead = true;
      break;
853
854
855
    case OPT_REM_FIN:
      opt_rem_fin = true;
      break;
856
857
858
    case OPT_REM_UNREACH:
      opt_rem_unreach = true;
      break;
859
860
861
    case OPT_REM_UNUSED_AP:
      opt_rem_unused_ap = true;
      break;
862
863
864
    case OPT_SAT_MINIMIZE:
      opt_sat_minimize = arg ? arg : "";
      break;
865
866
867
868
    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
869
870
871
    case OPT_SEED:
      opt_seed = to_int(arg);
      break;
872
873
874
    case OPT_SEP_SETS:
      opt_sep_sets = true;
      break;
875
876
877
    case OPT_SIMPL_ACC:
      opt_simpl_acc = true;
      break;
878
879
880
881
    case OPT_SIMPLIFY_EXCLUSIVE_AP:
      opt_simplify_exclusive_ap = true;
      opt_merge = true;
      break;
882
883
884
    case OPT_SPLIT_EDGES:
      opt_split_edges = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
885
886
887
    case OPT_STATES:
      opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
888
889
890
    case OPT_STRIPACC:
      opt_stripacc = true;
      break;
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
    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;
911
912
913
914
915
916
917
918
919
    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;
920
921
922
923
924
925
926
927
    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;
928
929
930
931
932
    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
933
934
935
936
937
938
939
940
941
942
    case ARGP_KEY_ARG:
      jobs.emplace_back(arg, true);
      break;

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
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
960
961
962

namespace
{
963
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
964
  {
965
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
966
    spot::postprocessor& post;
967
    automaton_printer printer;
968
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
969
970

    hoa_processor(spot::postprocessor& post)
971
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
972
973
974
975
    {
    }

    int
976
    process_formula(spot::formula, const char*, int) override
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
977
978
979
980
    {
      SPOT_UNREACHABLE();
    }

981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
    int process_string(const std::string& input, const char* filename,
                       int linenum) override
    {
      std::ostringstream loc;
      loc << filename << ':' << linenum;
      std::string locstr = loc.str();
      return process_automaton_stream
        (spot::automaton_stream_parser(input.c_str(), locstr, opt_parse),
         locstr.c_str());
    }

    int
    aborted(const spot::const_parsed_aut_ptr& h, const char* filename)
    {
      std::cerr << filename << ':' << h->loc << ": aborted input automaton\n";
      return 2;
    }

    int
    process_file(const char* filename) override
    {
      // If we have a filename like "foo/NN" such
      // that:
      // ① foo/NN is not a file,
      // ② NN is a number,
      // ③ foo is a file,
      // then it means we want to open foo as
      // a CSV file and process column NN.
      if (const char* slash = strrchr(filename, '/'))
        {
          char* end;
          errno = 0;
          long int col = strtol(slash + 1, &end, 10);
          if (errno == 0 && !*end && col != 0)
            {
              struct stat buf;
              if (stat(filename, &buf) != 0)
                {
                  col_to_read = col;
                  if (real_filename)
                    free(real_filename);
                  real_filename = strndup(filename, slash - filename);

                  // Special case for stdin.
                  if (real_filename[0] == '-' && real_filename[1] == 0)
                    return process_stream(std::cin, real_filename);

                  std::ifstream input(real_filename);
                  if (input)
                    return process_stream(input, real_filename);

                  error(2, errno, "cannot open '%s' nor '%s'",
                        filename, real_filename);
                }
            }
        }

      return process_automaton_stream(spot::automaton_stream_parser(filename,
                                                                    opt_parse),
                                      filename);
    }

    int process_automaton_stream(spot::automaton_stream_parser&& hp,
                                 const char* filename)
    {
      int err = 0;
      while (!abort_run)
        {
          auto haut = hp.parse(opt->dict);
          if (!haut->aut && haut->errors.empty())
            break;
          if (haut->format_errors(std::cerr))
            err = 2;
          if (!haut->aut)
            error(2, 0, "failed to read automaton from %s", filename);
          else if (haut->aborted)
            err = std::max(err, aborted(haut, filename));
          else
            process_automaton(haut, filename);
        }
      return err;
    }


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1065
    int
1066
    process_automaton(const spot::const_parsed_aut_ptr& haut,
1067
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1068
    {
1069
1070
      process_timer timer;
      timer.start();
1071

1072
1073
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
1074
      // merge_edges()) and the statistics about it make sense.
1075
      auto aut = ((automaton_format == Stats) || opt_name)
1076
1077
        ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
        : haut->aut;
1078

1079
1080
      // Preprocessing.

1081
      if (opt_stripacc)
1082
        spot::strip_acceptance_here(aut);
1083
      if (opt_merge)
1084
        aut->merge_edges();
1085
1086
1087
1088

      if (opt_simpl_acc)
        simplify_acceptance_here(aut);
      else if (opt_clean_acc)
1089
        cleanup_acceptance_here(aut);
1090

1091
      if (opt_sep_sets)
1092
        separate_sets_here(aut);
1093
      if (opt_complement_acc)
1094
1095
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
1096
      if (opt_rem_fin)
1097
        aut = remove_fin(aut);
1098
      if (opt_dnf_acc)
1099
1100
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
1101
      if (opt_cnf_acc)
1102
1103
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
1104

1105
1106
1107
1108
      // Filters.

      bool