autfilt.cc 36 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
92
93
  OPT_HIGHLIGHT_NONDET,
  OPT_HIGHLIGHT_NONDET_EDGES,
  OPT_HIGHLIGHT_NONDET_STATES,
94
  OPT_INSTUT,
95
  OPT_INCLUDED_IN,
96
  OPT_INHERENTLY_WEAK_SCCS,
97
98
99
100
  OPT_INTERSECT,
  OPT_IS_COMPLETE,
  OPT_IS_DETERMINISTIC,
  OPT_IS_EMPTY,
101
  OPT_IS_UNAMBIGUOUS,
102
103
  OPT_IS_TERMINAL,
  OPT_IS_WEAK,
104
  OPT_IS_INHERENTLY_WEAK,
105
106
107
  OPT_KEEP_STATES,
  OPT_MASK_ACC,
  OPT_MERGE,
108
109
  OPT_PRODUCT_AND,
  OPT_PRODUCT_OR,
110
  OPT_RANDOMIZE,
111
  OPT_REJ_SCCS,
112
  OPT_REJECT_WORD,
113
  OPT_REM_AP,
114
115
  OPT_REM_DEAD,
  OPT_REM_UNREACH,
116
  OPT_REM_UNUSED_AP,
117
  OPT_REM_FIN,
118
  OPT_SAT_MINIMIZE,
119
  OPT_SCCS,
120
  OPT_SEED,
121
  OPT_SEP_SETS,
122
  OPT_SIMPLIFY_EXCLUSIVE_AP,
123
124
  OPT_STATES,
  OPT_STRIPACC,
125
126
  OPT_TERMINAL_SCCS,
  OPT_TRIV_SCCS,
127
128
  OPT_USED_AP_N,
  OPT_UNUSED_AP_N,
129
  OPT_WEAK_SCCS,
130
};
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
131
132
133
134

static const argp_option options[] =
  {
    /**************************************************/
135
    { nullptr, 0, nullptr, 0, "Input:", 1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
136
137
138
    { "file", 'F', "FILENAME", 0,
      "process the automaton in FILENAME", 0 },
    /**************************************************/
139
    { "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
140
    { "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
141
    /**************************************************/
142
143
    { nullptr, 0, nullptr, 0, "Transformations:", 5 },
    { "merge-transitions", OPT_MERGE, nullptr, 0,
144
      "merge transitions with same destination and acceptance", 0 },
145
146
147
    { "product", OPT_PRODUCT_AND, "FILENAME", 0,
      "build the product with the automaton in FILENAME "
      "to intersect languages", 0 },
148
    { "product-and", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
149
150
151
    { "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
152
    { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
153
      "randomize states and transitions (specify 's' or 't' to "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
154
      "randomize only states or transitions)", 0 },
155
156
    { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL,
      "allow more stuttering (two possible algorithms)", 0 },
157
    { "destut", OPT_DESTUT, nullptr, 0, "allow less stuttering", 0 },
158
159
    { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
      "remove all transitions in specified acceptance sets", 0 },
160
    { "strip-acceptance", OPT_STRIPACC, nullptr, 0,
161
      "remove the acceptance condition and all acceptance sets", 0 },
162
163
    { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
      "only keep specified states.  The first state will be the new "\
164
      "initial state.  Implies --remove-unreachable-states.", 0 },
165
    { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
166
      "put the acceptance condition in Disjunctive Normal Form", 0 },
167
    { "cnf-acceptance", OPT_CNF_ACC, nullptr, 0,
168
      "put the acceptance condition in Conjunctive Normal Form", 0 },
169
    { "remove-fin", OPT_REM_FIN, nullptr, 0,
170
      "rewrite the automaton without using Fin acceptance", 0 },
171
    { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
172
      "remove unused acceptance sets from the automaton", 0 },
173
174
175
    { "complement", OPT_COMPLEMENT, nullptr, 0,
      "complement each automaton (currently support only deterministic "
      "automata)", 0 },
176
    { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
177
178
      "complement the acceptance condition (without touching the automaton)",
      0 },
179
180
181
    { "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 },
182
183
184
185
186
    { "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 },
187
    { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, nullptr, 0,
188
189
190
      "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 },
191
192
193
    { "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 },
194
195
    { "remove-unused-ap", OPT_REM_UNUSED_AP, nullptr, 0,
      "remove declared atomic propositions that are not used", 0 },
196
    { "remove-unreachable-states", OPT_REM_UNREACH, nullptr, 0,
197
      "remove states that are unreachable from the initial state", 0 },
198
    { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
199
200
      "remove states that are unreachable, or that cannot belong to an "
      "infinite path", 0 },
201
    { "separate-sets", OPT_SEP_SETS, nullptr, 0,
202
203
      "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 },
204
    { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL,
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
205
      "minimize the automaton using a SAT solver (only works for deterministic"
206
      " automata)", 0 },
207
208
209
210
211
212
213
214
215
216
    { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM",
      0},
    { "highlight-nondet-edges", OPT_HIGHLIGHT_NONDET_EDGES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic edges with color NUM",
      0},
    { "highlight-nondet", OPT_HIGHLIGHT_NONDET, "NUM",
      OPTION_ARG_OPTIONAL,
      "highlight nondeterministic states and edges with color NUM", 0},

217
    /**************************************************/
218
    { nullptr, 0, nullptr, 0, "Filtering options:", 6 },
219
    { "ap", OPT_AP_N, "RANGE", 0,
220
221
222
223
224
225
226
      "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 },
227
    { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
228
      "keep automata that are isomorphic to the automaton in FILENAME", 0 },
229
230
    { "isomorphic", 0, nullptr, OPTION_ALIAS | OPTION_HIDDEN, nullptr, 0 },
    { "unique", 'u', nullptr, 0,
231
232
      "do not output the same automaton twice (same in the sense that they "\
      "are isomorphic)", 0 },
233
    { "is-complete", OPT_IS_COMPLETE, nullptr, 0,
234
      "keep complete automata", 0 },
235
    { "is-deterministic", OPT_IS_DETERMINISTIC, nullptr, 0,
236
      "keep deterministic automata", 0 },
237
    { "is-empty", OPT_IS_EMPTY, nullptr, 0,
238
      "keep automata with an empty language", 0 },
239
    { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
240
      "keep only unambiguous automata", 0 },
241
242
243
244
    { "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
      "keep only terminal automata", 0 },
    { "is-weak", OPT_IS_WEAK, nullptr, 0,
      "keep only weak automata", 0 },
245
246
    { "is-inherently-weak", OPT_IS_INHERENTLY_WEAK, nullptr, 0,
      "keep only inherently weak automata", 0 },
247
248
249
    { "intersect", OPT_INTERSECT, "FILENAME", 0,
      "keep automata whose languages have an non-empty intersection with"
      " the automaton from FILENAME", 0 },
250
251
252
    { "included-in", OPT_INCLUDED_IN, "FILENAME", 0,
      "keep automata whose languages are included in that of the "
      "automaton from FILENAME", 0 },
253
254
255
    { "equivalent-to", OPT_EQUIVALENT_TO, "FILENAME", 0,
      "keep automata thare are equivalent (language-wise) to the automaton "
      "in FILENAME", 0 },
256
    { "invert-match", 'v', nullptr, 0, "select non-matching automata", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
257
    { "states", OPT_STATES, "RANGE", 0,
258
      "keep automata whose number of states is in RANGE", 0 },
259
    { "edges", OPT_EDGES, "RANGE", 0,
260
      "keep automata whose number of edges is in RANGE", 0 },
261
    { "acc-sets", OPT_ACC_SETS, "RANGE", 0,
262
      "keep automata whose number of acceptance sets is in RANGE", 0 },
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
    { "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 },
286
287
288
289
    { "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
290
    RANGE_DOC_FULL,
291
    WORD_DOC,
292
293
    { nullptr, 0, nullptr, 0,
      "If any option among --small, --deterministic, or --any is given, "
294
      "then the simplification level defaults to --high unless specified "
295
      "otherwise.  If any option among --low, --medium, or --high is given, "
296
      "then the simplification goal defaults to --small unless specified "
297
298
299
      "otherwise.  If none of those options are specified, then autfilt "
      "acts as is --any --low were given: these actually disable the "
      "simplification routines.", 22 },
300
    /**************************************************/
301
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
302
303
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
304
305
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
306
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
307
308
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
309
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
310
  {
311
    { &hoaread_argp, 0, nullptr, 0 },
312
313
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
314
    { &post_argp_disabled, 0, nullptr, 0 },
315
316
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
317
318
  };

319
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
320
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
321
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
322
323
324
325
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
326

327
// We want all these variables to be destroyed when we exit main, to
328
329
330
331
332
333
// 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();
334
335
  spot::twa_graph_ptr product_and = nullptr;
  spot::twa_graph_ptr product_or = nullptr;
336
  spot::twa_graph_ptr intersect = nullptr;
337
  spot::twa_graph_ptr included_in = nullptr;
338
339
  spot::twa_graph_ptr equivalent_pos = nullptr;
  spot::twa_graph_ptr equivalent_neg = nullptr;
340
  spot::twa_graph_ptr are_isomorphic = nullptr;
341
342
343
  std::unique_ptr<spot::isomorphism_checker>
                         isomorphism_checker = nullptr;
  std::unique_ptr<unique_aut_t> uniq = nullptr;
344
345
  spot::exclusive_ap excl_ap;
  spot::remove_ap rem_ap;
346
  std::vector<spot::twa_graph_ptr> acc_words;
347
  std::vector<spot::twa_graph_ptr> rej_words;
348
349
}* opt;

350
static bool opt_merge = false;
351
352
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
353
static bool opt_is_unambiguous = false;
354
355
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
356
static bool opt_is_inherently_weak = false;
357
static bool opt_invert = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
358
static range opt_states = { 0, std::numeric_limits<int>::max() };
359
360
static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() };
361
static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
362
363
364
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;
365
366
367
368
369
370
371
372
373
374
375
376
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;
377
static int opt_max_count = -1;
378
static bool opt_destut = false;
379
static char opt_instut = 0;
380
static bool opt_is_empty = false;
381
static bool opt_stripacc = false;
382
static bool opt_dnf_acc = false;
383
static bool opt_cnf_acc = false;
384
static bool opt_rem_fin = false;
385
static bool opt_clean_acc = false;
386
static bool opt_complement = false;
387
static bool opt_complement_acc = false;
388
static char* opt_decompose_strength = nullptr;
389
static spot::acc_cond::mark_t opt_mask_acc = 0U;
390
391
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
392
static bool opt_simplify_exclusive_ap = false;
393
394
static bool opt_rem_dead = false;
static bool opt_rem_unreach = false;
395
static bool opt_rem_unused_ap = false;
396
static bool opt_sep_sets = false;
397
static const char* opt_sat_minimize = nullptr;
398
399
static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
400

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

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
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
743
744
745

namespace
{
746
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
747
  {
748
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
749
    spot::postprocessor& post;
750
    automaton_printer printer;
751
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
752
753

    hoa_processor(spot::postprocessor& post)
754
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
755
756
757
758
    {
    }

    int
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
759
    process_formula(spot::formula, const char*, int)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
760
761
762
763
764
    {
      SPOT_UNREACHABLE();
    }

    int
765
    process_automaton(const spot::const_parsed_aut_ptr& haut,
766
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
767
768
769
    {
      spot::stopwatch sw;
      sw.start();
770

771
772
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
773
      // merge_edges()) and the statistics about it make sense.
774
      auto aut = ((automaton_format == Stats) || opt_name)
775
776
        ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
        : haut->aut;
777

778
779
      // Preprocessing.

780
      if (opt_stripacc)
781
        spot::strip_acceptance_here(aut);
782
      if (opt_merge)
783
        aut->merge_edges();
784
      if (opt_clean_acc || opt_rem_fin)
785
        cleanup_acceptance_here(aut);
786
      if (opt_sep_sets)
787
        separate_sets_here(aut);
788
      if (opt_complement_acc)
789
790
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
791
      if (opt_rem_fin)
792
        aut = remove_fin(aut);
793
      if (opt_dnf_acc)
794
795
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
796
      if (opt_cnf_acc)
797
798
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
799

800
801
802
803
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
804
      matched &= opt_states.contains(aut->num_states());
805
      matched &= opt_edges.contains(aut->num_edges());
806
      matched &= opt_accsets.contains(aut->acc().num_sets());
807
      matched &= opt_ap_n.contains(aut->ap().size());
808
809
810
811
812
813
814
      if (matched && need_unused_ap_count)
        {
          int unused = unused_ap(aut);
          matched &= opt_unused_ap_n.contains(unused);
          matched &= opt_used_ap_n.contains(aut->ap().size() - unused);
        }
      if (matched && opt_is_complete)
815
        matched &= is_complete(aut);
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
      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);
            }
        }
858
      if (opt_is_deterministic)
859
        matched &= is_deterministic(aut);
860
      else if (opt_is_unambiguous)
861
        matched &= is_unambiguous(aut);
862
      if (opt_is_terminal)
863
        matched &= is_terminal_automaton(aut);
864
      else if (opt_is_weak)
865
        matched &= is_weak_automaton(aut);
866
      else if (opt_is_inherently_weak)
867
        matched &= is_inherently_weak_automaton(aut);
868
869
      if (opt->are_isomorphic)
        matched &= opt->isomorphism_checker->is_isomorphic(aut);
870
      if (opt_is_empty)
871
        matched &= aut->is_empty();
872
      if (opt->intersect)
873
        matched &= !spot::product(aut, opt->intersect)->is_empty();
874
      if (opt->included_in)
875
        matched &= spot::product(aut, opt->included_in)->is_empty();
876
      if (opt->equivalent_pos)
877
878
879
        matched &= spot::product(aut, opt->equivalent_neg)->is_empty()
          && spot::product(dtwa_complement(ensure_deterministic(aut)),
                           opt->equivalent_pos)->is_empty();
880
881

      if (matched && !opt->acc_words.empty())
882
883
884
885
886
887
        for (auto& word_aut: opt->acc_words)
          if (spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
888
      if (matched && !opt->rej_words.empty())
889
890
891
892
893
894
        for (auto& word_aut: opt->rej_words)
          if (!spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
895

896
897
      // Drop or keep matched automata depending on the --invert option
      if (matched == opt_invert)
898
899
        return 0;

900
901
      // Postprocessing.

902
      if (opt_mask_acc)
903
        aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());
904

905
      if (!opt->rem_ap.empty())
906
        aut = opt->rem_ap.strip(aut);
907

908
909
910
911
912
      // opt_simplify_exclusive_ap is handled only after
      // post-processing.
      if (!opt->excl_ap.empty())
        aut = opt->excl_ap.constrain(aut, false);

913
      if (opt_destut)
914
        aut = spot::closure(std::move(aut));
915
      if (opt_instut == 1)
916
        aut = spot::sl(std::move(aut));
917
      else if (opt_instut == 2)
918
        aut = spot::sl2(std::move(aut));
919

920
      if (!opt_keep_states.empty())
921
        aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial);
922
      if (opt_rem_dead)
923
        aut->purge_dead_states();
924
      else if (opt_rem_unreach)
925
        aut->purge_unreachable_states();
926

927
      if (opt->product_and)
928
        aut = spot::product(std::move(aut), opt->product_and);
929
      if (opt->product_or)
930
        aut = spot::product_or(std::move(aut), opt->product_or);
931

932
      if (opt_decompose_strength)
933
934
935
936
937
        {
          aut = decompose_strength(aut, opt_decompose_strength);
          if (!aut)
            return 0;
        }
938

939
      if (opt_sat_minimize)
940
941
942
943
944
        {
          aut = spot::sat_minimize(aut, opt_sat_minimize, sbacc);
          if (!aut)
            return 0;
        }
945

946
      if (opt_complement)
947
        aut = spot::dtwa_complement(ensure_deterministic(aut));
948

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

951
      if (opt_simplify_exclusive_ap && !opt->excl_ap.empty())
952
953
954
        aut = opt->excl_ap.constrain(aut, true);
      else if (opt_rem_unused_ap) // constrain(aut, true) already does that
        aut->remove_unused_ap();
955

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
956
      if (randomize_st || randomize_tr)
957
        spot::randomize(aut, randomize_st, randomize_tr);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
958

959
960
961
962
963
      if (opt_highlight_nondet_states >= 0)
        spot::highlight_nondet_states(aut, opt_highlight_nondet_states);
      if (opt_highlight_nondet_edges >= 0)
        spot::highlight_nondet_edges(aut, opt_highlight_nondet_edges);

964
965
      const double conversion_time = sw.stop();

966
      if (opt->uniq)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
967
968
        {
          auto tmp =
969
970
            spot::canonicalize(make_twa_graph(aut,
                                                 spot::twa::prop_set::all()));
971
          if (!opt->uniq->emplace(tmp->edge_vector().begin() + 1,
972
973
                                  tmp->edge_vector().end()).second)
            return 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
974
975
        }

976
977
      ++match_count;