autfilt.cc 33 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
// -*- coding: utf-8 -*-
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
2
// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
3
// 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>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
27
28
29
30
31
32
33

#include <argp.h>
#include "error.h"

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

40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/stutter.hh>
#include <spot/twaalgos/isunamb.hh>
#include <spot/misc/optionmap.hh>
#include <spot/misc/timer.hh>
#include <spot/misc/random.hh>
#include <spot/parseaut/public.hh>
#include <spot/tl/exclusive.hh>
#include <spot/twaalgos/remprop.hh>
#include <spot/twaalgos/randomize.hh>
#include <spot/twaalgos/are_isomorphic.hh>
#include <spot/twaalgos/canonicalize.hh>
#include <spot/twaalgos/mask.hh>
#include <spot/twaalgos/sepsets.hh>
#include <spot/twaalgos/stripacc.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/dtwasat.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/strength.hh>
61
#include <spot/twaalgos/hoa.hh>
62
63
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isweakscc.hh>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
64

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
65
static const char argp_program_doc[] ="\
66
Convert, transform, and filter omega-automata.\v\
67
68
69
70
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
71

72
73
// Keep this list sorted
enum {
74
75
  OPT_ACC_SCCS = 256,
  OPT_ACC_SETS,
76
  OPT_ACCEPT_WORD,
77
  OPT_AP_N,
78
79
  OPT_ARE_ISOMORPHIC,
  OPT_CLEAN_ACC,
80
  OPT_CNF_ACC,
81
  OPT_COMPLEMENT,
82
83
  OPT_COMPLEMENT_ACC,
  OPT_COUNT,
84
  OPT_DECOMPOSE_STRENGTH,
85
86
87
  OPT_DESTUT,
  OPT_DNF_ACC,
  OPT_EDGES,
88
  OPT_EQUIVALENT_TO,
89
  OPT_EXCLUSIVE_AP,
90
  OPT_GENERIC,
91
  OPT_INSTUT,
92
  OPT_INCLUDED_IN,
93
  OPT_INHERENTLY_WEAK_SCCS,
94
95
96
97
  OPT_INTERSECT,
  OPT_IS_COMPLETE,
  OPT_IS_DETERMINISTIC,
  OPT_IS_EMPTY,
98
  OPT_IS_UNAMBIGUOUS,
99
100
  OPT_IS_TERMINAL,
  OPT_IS_WEAK,
101
  OPT_IS_INHERENTLY_WEAK,
102
103
104
  OPT_KEEP_STATES,
  OPT_MASK_ACC,
  OPT_MERGE,
105
106
  OPT_PRODUCT_AND,
  OPT_PRODUCT_OR,
107
  OPT_RANDOMIZE,
108
  OPT_REJ_SCCS,
109
  OPT_REJECT_WORD,
110
  OPT_REM_AP,
111
112
  OPT_REM_DEAD,
  OPT_REM_UNREACH,
113
  OPT_REM_FIN,
114
  OPT_SAT_MINIMIZE,
115
  OPT_SCCS,
116
  OPT_SEED,
117
  OPT_SEP_SETS,
118
  OPT_SIMPLIFY_EXCLUSIVE_AP,
119
120
  OPT_STATES,
  OPT_STRIPACC,
121
122
123
  OPT_TERMINAL_SCCS,
  OPT_TRIV_SCCS,
  OPT_WEAK_SCCS,
124
};
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
125
126
127
128

static const argp_option options[] =
  {
    /**************************************************/
129
    { nullptr, 0, nullptr, 0, "Input:", 1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
130
131
132
    { "file", 'F', "FILENAME", 0,
      "process the automaton in FILENAME", 0 },
    /**************************************************/
133
    { "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
134
    { "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
135
    /**************************************************/
136
137
    { nullptr, 0, nullptr, 0, "Transformations:", 5 },
    { "merge-transitions", OPT_MERGE, nullptr, 0,
138
      "merge transitions with same destination and acceptance", 0 },
139
140
141
    { "product", OPT_PRODUCT_AND, "FILENAME", 0,
      "build the product with the automaton in FILENAME "
      "to intersect languages", 0 },
142
    { "product-and", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
143
144
145
    { "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
146
    { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
147
      "randomize states and transitions (specify 's' or 't' to "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
148
      "randomize only states or transitions)", 0 },
149
150
    { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL,
      "allow more stuttering (two possible algorithms)", 0 },
151
    { "destut", OPT_DESTUT, nullptr, 0, "allow less stuttering", 0 },
152
153
    { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
      "remove all transitions in specified acceptance sets", 0 },
154
    { "strip-acceptance", OPT_STRIPACC, nullptr, 0,
155
      "remove the acceptance condition and all acceptance sets", 0 },
156
157
    { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
      "only keep specified states.  The first state will be the new "\
158
      "initial state.  Implies --remove-unreachable-states.", 0 },
159
    { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
160
      "put the acceptance condition in Disjunctive Normal Form", 0 },
161
    { "cnf-acceptance", OPT_CNF_ACC, nullptr, 0,
162
      "put the acceptance condition in Conjunctive Normal Form", 0 },
163
    { "remove-fin", OPT_REM_FIN, nullptr, 0,
164
      "rewrite the automaton without using Fin acceptance", 0 },
165
    { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
166
      "remove unused acceptance sets from the automaton", 0 },
167
168
169
    { "complement", OPT_COMPLEMENT, nullptr, 0,
      "complement each automaton (currently support only deterministic "
      "automata)", 0 },
170
    { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
171
172
      "complement the acceptance condition (without touching the automaton)",
      0 },
173
174
175
    { "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 },
176
177
178
179
180
    { "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 },
181
    { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, nullptr, 0,
182
183
184
      "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 },
185
186
187
    { "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 },
188
    { "remove-unreachable-states", OPT_REM_UNREACH, nullptr, 0,
189
      "remove states that are unreachable from the initial state", 0 },
190
    { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
191
192
      "remove states that are unreachable, or that cannot belong to an "
      "infinite path", 0 },
193
    { "separate-sets", OPT_SEP_SETS, nullptr, 0,
194
195
      "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 },
196
    { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL,
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
197
      "minimize the automaton using a SAT solver (only works for deterministic"
198
199
      " automata)", 0 },
    /**************************************************/
200
    { nullptr, 0, nullptr, 0, "Filtering options:", 6 },
201
202
    { "ap", OPT_AP_N, "RANGE", 0,
      "match automata with a number of atomic propositions in RANGE", 0 },
203
    { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
204
      "keep automata that are isomorphic to the automaton in FILENAME", 0 },
205
206
    { "isomorphic", 0, nullptr, OPTION_ALIAS | OPTION_HIDDEN, nullptr, 0 },
    { "unique", 'u', nullptr, 0,
207
208
      "do not output the same automaton twice (same in the sense that they "\
      "are isomorphic)", 0 },
209
    { "is-complete", OPT_IS_COMPLETE, nullptr, 0,
210
      "keep complete automata", 0 },
211
    { "is-deterministic", OPT_IS_DETERMINISTIC, nullptr, 0,
212
      "keep deterministic automata", 0 },
213
    { "is-empty", OPT_IS_EMPTY, nullptr, 0,
214
      "keep automata with an empty language", 0 },
215
    { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
216
      "keep only unambiguous automata", 0 },
217
218
219
220
    { "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
      "keep only terminal automata", 0 },
    { "is-weak", OPT_IS_WEAK, nullptr, 0,
      "keep only weak automata", 0 },
221
222
    { "is-inherently-weak", OPT_IS_INHERENTLY_WEAK, nullptr, 0,
      "keep only inherently weak automata", 0 },
223
224
225
    { "intersect", OPT_INTERSECT, "FILENAME", 0,
      "keep automata whose languages have an non-empty intersection with"
      " the automaton from FILENAME", 0 },
226
227
228
    { "included-in", OPT_INCLUDED_IN, "FILENAME", 0,
      "keep automata whose languages are included in that of the "
      "automaton from FILENAME", 0 },
229
230
231
    { "equivalent-to", OPT_EQUIVALENT_TO, "FILENAME", 0,
      "keep automata thare are equivalent (language-wise) to the automaton "
      "in FILENAME", 0 },
232
    { "invert-match", 'v', nullptr, 0, "select non-matching automata", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
233
    { "states", OPT_STATES, "RANGE", 0,
234
      "keep automata whose number of states is in RANGE", 0 },
235
    { "edges", OPT_EDGES, "RANGE", 0,
236
      "keep automata whose number of edges is in RANGE", 0 },
237
    { "acc-sets", OPT_ACC_SETS, "RANGE", 0,
238
      "keep automata whose number of acceptance sets is in RANGE", 0 },
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
    { "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 },
262
263
264
265
    { "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 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
266
    RANGE_DOC_FULL,
267
    WORD_DOC,
268
269
    { nullptr, 0, nullptr, 0,
      "If any option among --small, --deterministic, or --any is given, "
270
      "then the simplification level defaults to --high unless specified "
271
      "otherwise.  If any option among --low, --medium, or --high is given, "
272
      "then the simplification goal defaults to --small unless specified "
273
274
275
      "otherwise.  If none of those options are specified, then autfilt "
      "acts as is --any --low were given: these actually disable the "
      "simplification routines.", 22 },
276
    /**************************************************/
277
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
278
279
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
280
281
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
282
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
283
284
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
285
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
286
  {
287
    { &hoaread_argp, 0, nullptr, 0 },
288
289
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
290
    { &post_argp_disabled, 0, nullptr, 0 },
291
292
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
293
294
  };

295
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
296
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
297
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
298
299
300
301
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
302

303
// We want all these variables to be destroyed when we exit main, to
304
305
306
307
308
309
// 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();
310
311
  spot::twa_graph_ptr product_and = nullptr;
  spot::twa_graph_ptr product_or = nullptr;
312
  spot::twa_graph_ptr intersect = nullptr;
313
  spot::twa_graph_ptr included_in = nullptr;
314
315
  spot::twa_graph_ptr equivalent_pos = nullptr;
  spot::twa_graph_ptr equivalent_neg = nullptr;
316
  spot::twa_graph_ptr are_isomorphic = nullptr;
317
318
319
  std::unique_ptr<spot::isomorphism_checker>
                         isomorphism_checker = nullptr;
  std::unique_ptr<unique_aut_t> uniq = nullptr;
320
321
  spot::exclusive_ap excl_ap;
  spot::remove_ap rem_ap;
322
  std::vector<spot::twa_graph_ptr> acc_words;
323
  std::vector<spot::twa_graph_ptr> rej_words;
324
325
}* opt;

326
static bool opt_merge = false;
327
328
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
329
static bool opt_is_unambiguous = false;
330
331
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
332
static bool opt_is_inherently_weak = false;
333
static bool opt_invert = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
334
static range opt_states = { 0, std::numeric_limits<int>::max() };
335
336
static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() };
337
static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
338
339
340
341
342
343
344
345
346
347
348
349
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;
350
static int opt_max_count = -1;
351
static bool opt_destut = false;
352
static char opt_instut = 0;
353
static bool opt_is_empty = false;
354
static bool opt_stripacc = false;
355
static bool opt_dnf_acc = false;
356
static bool opt_cnf_acc = false;
357
static bool opt_rem_fin = false;
358
static bool opt_clean_acc = false;
359
static bool opt_complement = false;
360
static bool opt_complement_acc = false;
361
static char* opt_decompose_strength = nullptr;
362
static spot::acc_cond::mark_t opt_mask_acc = 0U;
363
364
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
365
static bool opt_simplify_exclusive_ap = false;
366
367
static bool opt_rem_dead = false;
static bool opt_rem_unreach = false;
368
static bool opt_sep_sets = false;
369
static const char* opt_sat_minimize = nullptr;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
370

371
372
373
374
375
376
377
378
379
380
381
382
static spot::twa_graph_ptr
ensure_deterministic(const spot::twa_graph_ptr& aut)
{
  if (spot::is_deterministic(aut))
    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
383
384
385
386
387
388
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
389
    case 'c':
390
      automaton_format = Count;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
391
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
392
393
394
    case 'F':
      jobs.emplace_back(arg, true);
      break;
395
396
397
    case 'n':
      opt_max_count = to_pos_int(arg);
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
398
    case 'u':
399
      opt->uniq =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
400
401
        std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
      break;
402
403
404
    case 'v':
      opt_invert = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
405
406
    case 'x':
      {
407
408
409
        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
410
411
      }
      break;
412
413
414
    case OPT_AP_N:
      opt_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
415
416
417
    case OPT_ACC_SETS:
      opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
418
419
420
421
    case OPT_ACC_SCCS:
      opt_acc_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
422
    case OPT_ACCEPT_WORD:
423
      try
424
425
426
427
        {
          opt->acc_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
428
      catch (const spot::parse_error& e)
429
430
431
432
        {
          error(2, 0, "failed to parse the argument of --accept-word:\n%s",
                e.what());
        }
433
      break;
434
    case OPT_ARE_ISOMORPHIC:
435
      opt->are_isomorphic = read_automaton(arg, opt->dict);
436
      break;
437
438
439
    case OPT_CLEAN_ACC:
      opt_clean_acc = true;
      break;
440
441
442
443
    case OPT_CNF_ACC:
      opt_dnf_acc = false;
      opt_cnf_acc = true;
      break;
444
445
446
    case OPT_COMPLEMENT:
      opt_complement = true;
      break;
447
448
449
    case OPT_COMPLEMENT_ACC:
      opt_complement_acc = true;
      break;
450
451
452
    case OPT_DECOMPOSE_STRENGTH:
      opt_decompose_strength = arg;
      break;
453
454
455
456
457
    case OPT_DESTUT:
      opt_destut = true;
      break;
    case OPT_DNF_ACC:
      opt_dnf_acc = true;
458
      opt_cnf_acc = false;
459
      break;
460
461
462
    case OPT_EDGES:
      opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
463
    case OPT_EXCLUSIVE_AP:
464
      opt->excl_ap.add_group(arg);
465
      break;
466
467
    case OPT_EQUIVALENT_TO:
      if (opt->equivalent_pos)
468
        error(2, 0, "only one --equivalent-to option can be given");
469
470
      opt->equivalent_pos = read_automaton(arg, opt->dict);
      opt->equivalent_neg =
471
        spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos));
472
      break;
473
    case OPT_INSTUT:
474
      if (!arg || (arg[0] == '1' && arg[1] == 0))
475
        opt_instut = 1;
476
      else if (arg[0] == '2' && arg[1] == 0)
477
        opt_instut = 2;
478
      else
479
        error(2, 0, "unknown argument for --instut: %s", arg);
480
      break;
481
482
    case OPT_INCLUDED_IN:
      {
483
484
485
486
487
488
        auto aut = ensure_deterministic(read_automaton(arg, opt->dict));
        aut = spot::dtwa_complement(aut);
        if (!opt->included_in)
          opt->included_in = aut;
        else
          opt->included_in = spot::product_or(opt->included_in, aut);
489
490
      }
      break;
491
492
493
494
495
    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;
496
    case OPT_INTERSECT:
497
      opt->intersect = read_automaton(arg, opt->dict);
498
      break;
499
500
501
502
503
504
    case OPT_IS_COMPLETE:
      opt_is_complete = true;
      break;
    case OPT_IS_DETERMINISTIC:
      opt_is_deterministic = true;
      break;
505
506
507
    case OPT_IS_EMPTY:
      opt_is_empty = true;
      break;
508
509
510
    case OPT_IS_INHERENTLY_WEAK:
      opt_is_inherently_weak = true;
      break;
511
512
513
    case OPT_IS_UNAMBIGUOUS:
      opt_is_unambiguous = true;
      break;
514
515
516
517
518
519
    case OPT_IS_TERMINAL:
      opt_is_terminal = true;
      break;
    case OPT_IS_WEAK:
      opt_is_weak = true;
      break;
520
521
522
    case OPT_MERGE:
      opt_merge = true;
      break;
523
524
    case OPT_MASK_ACC:
      {
525
526
527
528
529
530
531
532
533
534
535
536
        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;
537
538
539
540
541
542
543
      }
    case OPT_KEEP_STATES:
      {
        std::vector<long> values = to_longs(arg);
        if (!values.empty())
          opt_keep_states_initial = values[0];
        for (auto res : values)
544
545
546
547
          {
            if (res < 0)
              error(2, 0, "state ids should be non-negative:"
                    " --mask-acc=%ld", res);
548
549
550
            // 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);
551
552
553
554
            opt_keep_states[res] = true;
          }
        opt_rem_unreach = true;
        break;
555
      }
556
    case OPT_PRODUCT_AND:
557
      {
558
559
560
561
562
563
        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));
564
565
566
567
      }
      break;
    case OPT_PRODUCT_OR:
      {
568
569
570
571
572
573
        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));
574
575
      }
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
576
577
    case OPT_RANDOMIZE:
      if (arg)
578
579
580
581
582
583
584
585
586
587
588
589
590
591
        {
          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
592
      else
593
594
595
596
        {
          randomize_tr = true;
          randomize_st = true;
        }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
597
      break;
598
599
600
601
    case OPT_REJ_SCCS:
      opt_rej_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
602
603
    case OPT_REJECT_WORD:
      try
604
605
606
607
        {
          opt->rej_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
608
      catch (const spot::parse_error& e)
609
610
611
612
        {
          error(2, 0, "failed to parse the argument of --reject-word:\n%s",
                e.what());
        }
613
      break;
614
    case OPT_REM_AP:
615
      opt->rem_ap.add_ap(arg);
616
      break;
617
618
619
    case OPT_REM_DEAD:
      opt_rem_dead = true;
      break;
620
621
622
    case OPT_REM_FIN:
      opt_rem_fin = true;
      break;
623
624
625
    case OPT_REM_UNREACH:
      opt_rem_unreach = true;
      break;
626
627
628
    case OPT_SAT_MINIMIZE:
      opt_sat_minimize = arg ? arg : "";
      break;
629
630
631
632
    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
633
634
635
    case OPT_SEED:
      opt_seed = to_int(arg);
      break;
636
637
638
    case OPT_SEP_SETS:
      opt_sep_sets = true;
      break;
639
640
641
642
    case OPT_SIMPLIFY_EXCLUSIVE_AP:
      opt_simplify_exclusive_ap = true;
      opt_merge = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
643
644
645
    case OPT_STATES:
      opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
646
647
648
    case OPT_STRIPACC:
      opt_stripacc = true;
      break;
649
650
651
652
653
654
655
656
657
658
659
660
661
662
    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;
    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
663
664
665
666
667
668
669
670
671
672
673
674
675
    case ARGP_KEY_ARG:
      jobs.emplace_back(arg, true);
      break;

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}


namespace
{
676
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
677
  {
678
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
679
    spot::postprocessor& post;
680
    automaton_printer printer;
681
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
682
683

    hoa_processor(spot::postprocessor& post)
684
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
685
686
687
688
    {
    }

    int
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
689
    process_formula(spot::formula, const char*, int)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
690
691
692
693
694
    {
      SPOT_UNREACHABLE();
    }

    int
695
    process_automaton(const spot::const_parsed_aut_ptr& haut,
696
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
697
698
699
    {
      spot::stopwatch sw;
      sw.start();
700

701
702
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
703
      // merge_edges()) and the statistics about it make sense.
704
      auto aut = ((automaton_format == Stats) || opt_name)
705
706
        ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
        : haut->aut;
707

708
709
      // Preprocessing.

710
      if (opt_stripacc)
711
        spot::strip_acceptance_here(aut);
712
      if (opt_merge)
713
        aut->merge_edges();
714
      if (opt_clean_acc || opt_rem_fin)
715
        cleanup_acceptance_here(aut);
716
      if (opt_sep_sets)
717
        separate_sets_here(aut);
718
      if (opt_complement_acc)
719
720
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
721
      if (opt_rem_fin)
722
        aut = remove_fin(aut);
723
      if (opt_dnf_acc)
724
725
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
726
      if (opt_cnf_acc)
727
728
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
729

730
731
732
733
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
734
      matched &= opt_states.contains(aut->num_states());
735
      matched &= opt_edges.contains(aut->num_edges());
736
      matched &= opt_accsets.contains(aut->acc().num_sets());
737
      matched &= opt_ap_n.contains(aut->ap().size());
738
      if (opt_is_complete)
739
        matched &= is_complete(aut);
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
      if (matched && (opt_sccs_set | opt_art_sccs_set))
        {
          spot::scc_info si(aut);
          unsigned n = si.scc_count();
          matched = opt_sccs.contains(n);

          if (opt_art_sccs_set && matched)
            {
              si.determine_unknown_acceptance();
              unsigned triv = 0;
              unsigned acc = 0;
              unsigned rej = 0;
              unsigned inhweak = 0;
              unsigned weak = 0;
              unsigned terminal = 0;
              for (unsigned s = 0; s < n; ++s)
                if (si.is_trivial(s))
                  {
                    ++triv;
                  }
                else if (si.is_rejecting_scc(s))
                  {
                    ++rej;
                  }
                else
                  {
                    ++acc;
                    if (opt_inhweak_sccs_set)
                      inhweak += is_inherently_weak_scc(si, s);
                    if (opt_weak_sccs_set)
                      weak += is_weak_scc(si, s);
                    if (opt_terminal_sccs_set)
                      terminal += is_terminal_scc(si, s);
                  }
              matched &= opt_acc_sccs.contains(acc);
              matched &= opt_rej_sccs.contains(rej);
              matched &= opt_triv_sccs.contains(triv);
              matched &= opt_inhweak_sccs.contains(inhweak);
              matched &= opt_weak_sccs.contains(weak);
              matched &= opt_terminal_sccs.contains(terminal);
            }
        }
782
      if (opt_is_deterministic)
783
        matched &= is_deterministic(aut);
784
      else if (opt_is_unambiguous)
785
        matched &= is_unambiguous(aut);
786
      if (opt_is_terminal)
787
        matched &= is_terminal_automaton(aut);
788
      else if (opt_is_weak)
789
        matched &= is_weak_automaton(aut);
790
      else if (opt_is_inherently_weak)
791
        matched &= is_inherently_weak_automaton(aut);
792
793
      if (opt->are_isomorphic)
        matched &= opt->isomorphism_checker->is_isomorphic(aut);
794
      if (opt_is_empty)
795
        matched &= aut->is_empty();
796
      if (opt->intersect)
797
        matched &= !spot::product(aut, opt->intersect)->is_empty();
798
      if (opt->included_in)
799
        matched &= spot::product(aut, opt->included_in)->is_empty();
800
      if (opt->equivalent_pos)
801
802
803
        matched &= spot::product(aut, opt->equivalent_neg)->is_empty()
          && spot::product(dtwa_complement(ensure_deterministic(aut)),
                           opt->equivalent_pos)->is_empty();
804
805

      if (matched && !opt->acc_words.empty())
806
807
808
809
810
811
        for (auto& word_aut: opt->acc_words)
          if (spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
812
      if (matched && !opt->rej_words.empty())
813
814
815
816
817
818
        for (auto& word_aut: opt->rej_words)
          if (!spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
819

820
821
      // Drop or keep matched automata depending on the --invert option
      if (matched == opt_invert)
822
823
        return 0;

824
825
      // Postprocessing.

826
      if (opt_mask_acc)
827
        aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());
828

829
      if (!opt->rem_ap.empty())
830
        aut = opt->rem_ap.strip(aut);
831

832
833
834
835
836
      // opt_simplify_exclusive_ap is handled only after
      // post-processing.
      if (!opt->excl_ap.empty())
        aut = opt->excl_ap.constrain(aut, false);

837
      if (opt_destut)
838
        aut = spot::closure(std::move(aut));
839
      if (opt_instut == 1)
840
        aut = spot::sl(std::move(aut));
841
      else if (opt_instut == 2)
842
        aut = spot::sl2(std::move(aut));
843

844
      if (!opt_keep_states.empty())
845
        aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial);
846
      if (opt_rem_dead)
847
        aut->purge_dead_states();
848
      else if (opt_rem_unreach)
849
        aut->purge_unreachable_states();
850

851
      if (opt->product_and)
852
        aut = spot::product(std::move(aut), opt->product_and);
853
      if (opt->product_or)
854
        aut = spot::product_or(std::move(aut), opt->product_or);
855

856
      if (opt_decompose_strength)
857
858
859
860
861
        {
          aut = decompose_strength(aut, opt_decompose_strength);
          if (!aut)
            return 0;
        }
862

863
      if (opt_sat_minimize)
864
865
866
867
868
        {
          aut = spot::sat_minimize(aut, opt_sat_minimize, sbacc);
          if (!aut)
            return 0;
        }
869

870
      if (opt_complement)
871
        aut = spot::dtwa_complement(ensure_deterministic(aut));
872

873
      aut = post.run(aut, nullptr);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
874

875
876
877
      if (opt_simplify_exclusive_ap && !opt->excl_ap.empty())
        aut = opt->excl_ap.constrain(aut, opt_simplify_exclusive_ap);

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
878
      if (randomize_st || randomize_tr)
879
        spot::randomize(aut, randomize_st, randomize_tr);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
880

881
882
      const double conversion_time = sw.stop();

883
      if (opt->uniq)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
884
885
        {
          auto tmp =
886
887
            spot::canonicalize(make_twa_graph(aut,
                                                 spot::twa::prop_set::all()));
888
          if (!opt->uniq->emplace(tmp->edge_vector().begin() + 1,
889
890
                                  tmp->edge_vector().end()).second)
            return 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
891
892
        }

893
894
      ++match_count;

895
      printer.print(aut, nullptr, filename, -1, conversion_time, haut);
896
897

      if (opt_max_count >= 0 && match_count >= opt_max_count)
898
        abort_run = true;
899

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
900
901
      return 0;
    }
902

903
    int
904
    aborted(const spot::const_parsed_aut_ptr& h, const char* filename)
905
906
907
908
    {
      std::cerr << filename << ':' << h->loc << ": aborted input automaton\n";
      return 2;
    }
909
910
911
912

    int
    process_file(const char* filename)
    {
913
      auto hp = spot::automaton_stream_parser(filename, opt_parse);
914
      int err = 0;
915
      while (!abort_run)
916
917
918
919
920
921
922
923
924
925
926
        {
          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
927
            process_automaton(haut, filename);
928
        }
929
930
      return err;
    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
931
932
933
934
935
936
937
938
939
  };
}

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

  const argp ap = { options, parse_opt, "[FILENAMES...]",
940
                    argp_program_doc, children, nullptr, nullptr };
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
941

942
943
944
945
946
947
  try
    {
      // This will ensure that all objects stored in this struct are
      // destroyed before global variables.
      opt_t o;
      opt = &o;
948

949
950
951
      // Disable post-processing as much as possible by default.
      level = spot::postprocessor::Low;
      pref = spot::postprocessor::Any;
952
      type = spot::postprocessor::Generic;
953
      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
954
        exit(err);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
955