autfilt.cc 33.3 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_UNUSED_AP,
114
  OPT_REM_FIN,
115
  OPT_SAT_MINIMIZE,
116
  OPT_SCCS,
117
  OPT_SEED,
118
  OPT_SEP_SETS,
119
  OPT_SIMPLIFY_EXCLUSIVE_AP,
120
121
  OPT_STATES,
  OPT_STRIPACC,
122
123
124
  OPT_TERMINAL_SCCS,
  OPT_TRIV_SCCS,
  OPT_WEAK_SCCS,
125
};
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
126
127
128
129

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

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

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

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

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

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

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}


namespace
{
683
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
684
  {
685
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
686
    spot::postprocessor& post;
687
    automaton_printer printer;
688
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
689
690

    hoa_processor(spot::postprocessor& post)
691
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
692
693
694
695
    {
    }

    int
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
696
    process_formula(spot::formula, const char*, int)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
697
698
699
700
701
    {
      SPOT_UNREACHABLE();
    }

    int
702
    process_automaton(const spot::const_parsed_aut_ptr& haut,
703
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
704
705
706
    {
      spot::stopwatch sw;
      sw.start();
707

708
709
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
710
      // merge_edges()) and the statistics about it make sense.
711
      auto aut = ((automaton_format == Stats) || opt_name)
712
713
        ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
        : haut->aut;
714

715
716
      // Preprocessing.

717
      if (opt_stripacc)
718
        spot::strip_acceptance_here(aut);
719
      if (opt_merge)
720
        aut->merge_edges();
721
      if (opt_clean_acc || opt_rem_fin)
722
        cleanup_acceptance_here(aut);
723
      if (opt_sep_sets)
724
        separate_sets_here(aut);
725
      if (opt_complement_acc)
726
727
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
728
      if (opt_rem_fin)
729
        aut = remove_fin(aut);
730
      if (opt_dnf_acc)
731
732
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
733
      if (opt_cnf_acc)
734
735
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
736

737
738
739
740
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
741
      matched &= opt_states.contains(aut->num_states());
742
      matched &= opt_edges.contains(aut->num_edges());
743
      matched &= opt_accsets.contains(aut->acc().num_sets());
744
      matched &= opt_ap_n.contains(aut->ap().size());
745
      if (opt_is_complete)
746
        matched &= is_complete(aut);
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
782
783
784
785
786
787
788
      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);
            }
        }
789
      if (opt_is_deterministic)
790
        matched &= is_deterministic(aut);
791
      else if (opt_is_unambiguous)
792
        matched &= is_unambiguous(aut);
793
      if (opt_is_terminal)
794
        matched &= is_terminal_automaton(aut);
795
      else if (opt_is_weak)
796
        matched &= is_weak_automaton(aut);
797
      else if (opt_is_inherently_weak)
798
        matched &= is_inherently_weak_automaton(aut);
799
800
      if (opt->are_isomorphic)
        matched &= opt->isomorphism_checker->is_isomorphic(aut);
801
      if (opt_is_empty)
802
        matched &= aut->is_empty();
803
      if (opt->intersect)
804
        matched &= !spot::product(aut, opt->intersect)->is_empty();
805
      if (opt->included_in)
806
        matched &= spot::product(aut, opt->included_in)->is_empty();
807
      if (opt->equivalent_pos)
808
809
810
        matched &= spot::product(aut, opt->equivalent_neg)->is_empty()
          && spot::product(dtwa_complement(ensure_deterministic(aut)),
                           opt->equivalent_pos)->is_empty();
811
812

      if (matched && !opt->acc_words.empty())
813
814
815
816
817
818
        for (auto& word_aut: opt->acc_words)
          if (spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
819
      if (matched && !opt->rej_words.empty())
820
821
822
823
824
825
        for (auto& word_aut: opt->rej_words)
          if (!spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
826

827
828
      // Drop or keep matched automata depending on the --invert option
      if (matched == opt_invert)
829
830
        return 0;

831
832
      // Postprocessing.

833
      if (opt_mask_acc)
834
        aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());
835

836
      if (!opt->rem_ap.empty())
837
        aut = opt->rem_ap.strip(aut);
838

839
840
841
842
843
      // opt_simplify_exclusive_ap is handled only after
      // post-processing.
      if (!opt->excl_ap.empty())
        aut = opt->excl_ap.constrain(aut, false);

844
      if (opt_destut)
845
        aut = spot::closure(std::move(aut));
846
      if (opt_instut == 1)
847
        aut = spot::sl(std::move(aut));
848
      else if (opt_instut == 2)
849
        aut = spot::sl2(std::move(aut));
850

851
      if (!opt_keep_states.empty())
852
        aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial);
853
      if (opt_rem_dead)
854
        aut->purge_dead_states();
855
      else if (opt_rem_unreach)
856
        aut->purge_unreachable_states();
857

858
      if (opt->product_and)
859
        aut = spot::product(std::move(aut), opt->product_and);
860
      if (opt->product_or)
861
        aut = spot::product_or(std::move(aut), opt->product_or);
862

863
      if (opt_decompose_strength)
864
865
866
867
868
        {
          aut = decompose_strength(aut, opt_decompose_strength);
          if (!aut)
            return 0;
        }
869

870
      if (opt_sat_minimize)
871
872
873
874
875
        {
          aut = spot::sat_minimize(aut, opt_sat_minimize, sbacc);
          if (!aut)
            return 0;
        }
876

877
      if (opt_complement)
878
        aut = spot::dtwa_complement(ensure_deterministic(aut));
879

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

882
      if (opt_simplify_exclusive_ap && !opt->excl_ap.empty())
883
884
885
        aut = opt->excl_ap.constrain(aut, true);
      else if (opt_rem_unused_ap) // constrain(aut, true) already does that
        aut->remove_unused_ap();
886

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
887
      if (randomize_st || randomize_tr)
888
        spot::randomize(aut, randomize_st, randomize_tr);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
889

890
891
      const double conversion_time = sw.stop();

892
      if (opt->uniq)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
893
894
        {
          auto tmp =
895
896
            spot::canonicalize(make_twa_graph(aut,
                                                 spot::twa::prop_set::all()));
897
          if (!opt->uniq->emplace(tmp->edge_vector().begin() + 1,
898
899
                                  tmp->edge_vector().end()).second)
            return 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
900
901
        }

902
903
      ++match_count;

904
      printer.print(aut, nullptr, filename, -1, conversion_time, haut);
905
906

      if (opt_max_count >= 0 && match_count >= opt_max_count)
907
        abort_run = true;
908

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
909
910
      return 0;
    }
911

912
    int
913
    aborted(const spot::const_parsed_aut_ptr& h, const char* filename)
914
915
916
917
    {
      std::cerr << filename << ':' << h->loc << ": aborted input automaton\n";
      return 2;
    }
918
919
920
921

    int
    process_file(const char* filename)
    {
922
      auto hp = spot::automaton_stream_parser(filename, opt_parse);
923
      int err = 0;
924
      while (!abort_run)
925
926
927
928
929
930
931
932
933
934
935
        {
          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
936
            process_automaton(haut, filename);
937
        }
938
939
      return err;
    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
940
941
942
943
944
945
946
947
948
  };
}

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

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

951
952
953
954
955
956
  try
    {