autfilt.cc 41.1 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

#include <argp.h>
#include "error.h"
30
#include "argmatch.h"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
31
32
33
34

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

41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
#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>
62
#include <spot/twaalgos/hoa.hh>
63
64
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isweakscc.hh>
65
#include <spot/twaalgos/gtec/gtec.hh>
66
#include <spot/twaalgos/totgba.hh>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
67

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

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

static const argp_option options[] =
  {
    /**************************************************/
142
    { nullptr, 0, nullptr, 0, "Input:", 1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
143
144
145
    { "file", 'F', "FILENAME", 0,
      "process the automaton in FILENAME", 0 },
    /**************************************************/
146
    { "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
147
    { "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
148
    /**************************************************/
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
    { nullptr, 0, nullptr, 0, "Filtering options:", 5 },
    { "ap", OPT_AP_N, "RANGE", 0,
      "match automata with a number of (declared) atomic propositions in RANGE",
      0 },
    { "used-ap", OPT_USED_AP_N, "RANGE", 0,
      "match automata with a number of used atomic propositions in RANGE", 0 },
    { "unused-ap", OPT_UNUSED_AP_N, "RANGE", 0,
      "match automata with a number of declared, but unused atomic "
      "propositions in RANGE", 0 },
    { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
      "keep automata that are isomorphic to the automaton in FILENAME", 0 },
    { "isomorphic", 0, nullptr, OPTION_ALIAS | OPTION_HIDDEN, nullptr, 0 },
    { "unique", 'u', nullptr, 0,
      "do not output the same automaton twice (same in the sense that they "\
      "are isomorphic)", 0 },
    { "is-complete", OPT_IS_COMPLETE, nullptr, 0,
      "keep complete automata", 0 },
    { "is-deterministic", OPT_IS_DETERMINISTIC, nullptr, 0,
      "keep deterministic automata", 0 },
    { "is-empty", OPT_IS_EMPTY, nullptr, 0,
      "keep automata with an empty language", 0 },
170
171
    { "is-stutter-invariant", OPT_IS_STUTTER_INVARIANT, nullptr, 0,
      "keep automata representing stutter-invariant properties", 0 },
172
173
    { "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
      "keep only terminal automata", 0 },
174
175
    { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
      "keep only unambiguous automata", 0 },
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
    { "is-weak", OPT_IS_WEAK, nullptr, 0,
      "keep only weak automata", 0 },
    { "is-inherently-weak", OPT_IS_INHERENTLY_WEAK, nullptr, 0,
      "keep only inherently weak automata", 0 },
    { "intersect", OPT_INTERSECT, "FILENAME", 0,
      "keep automata whose languages have an non-empty intersection with"
      " the automaton from FILENAME", 0 },
    { "included-in", OPT_INCLUDED_IN, "FILENAME", 0,
      "keep automata whose languages are included in that of the "
      "automaton from FILENAME", 0 },
    { "equivalent-to", OPT_EQUIVALENT_TO, "FILENAME", 0,
      "keep automata thare are equivalent (language-wise) to the automaton "
      "in FILENAME", 0 },
    { "invert-match", 'v', nullptr, 0, "select non-matching automata", 0 },
    { "states", OPT_STATES, "RANGE", 0,
      "keep automata whose number of states is in RANGE", 0 },
    { "edges", OPT_EDGES, "RANGE", 0,
      "keep automata whose number of edges is in RANGE", 0 },
194
195
    { "nondet-states", OPT_NONDET_STATES, "RANGE", 0,
      "keep automata whose number of nondeterministic states is in RANGE", 0 },
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
    { "acc-sets", OPT_ACC_SETS, "RANGE", 0,
      "keep automata whose number of acceptance sets is in RANGE", 0 },
    { "sccs", OPT_SCCS, "RANGE", 0,
      "keep automata whose number of SCCs is in RANGE", 0 },
    { "acc-sccs", OPT_ACC_SCCS, "RANGE", 0,
      "keep automata whose number of non-trivial accepting SCCs is in RANGE",
      0 },
    { "accepting-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "rej-sccs", OPT_REJ_SCCS, "RANGE", 0,
      "keep automata whose number of non-trivial rejecting SCCs is in RANGE",
      0 },
    { "rejecting-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "triv-sccs", OPT_TRIV_SCCS, "RANGE", 0,
      "keep automata whose number of trivial SCCs is in RANGE", 0 },
    { "trivial-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "inherently-weak-sccs", OPT_INHERENTLY_WEAK_SCCS, "RANGE", 0,
      "keep automata whose number of accepting inherently-weak SCCs is in "
      "RANGE.  An accepting SCC is inherently weak if it does not have a "
      "rejecting cycle.", 0 },
    { "weak-sccs", OPT_WEAK_SCCS, "RANGE", 0,
      "keep automata whose number of accepting weak SCCs is in RANGE.  "
      "In a weak SCC, all transitions belong to the same acceptance sets.", 0 },
    { "terminal-sccs", OPT_TERMINAL_SCCS, "RANGE", 0,
      "keep automata whose number of accepting terminal SCCs is in RANGE.  "
      "Terminal SCCs are weak and complete.", 0 },
    { "accept-word", OPT_ACCEPT_WORD, "WORD", 0,
      "keep automata that accept WORD", 0 },
    { "reject-word", OPT_REJECT_WORD, "WORD", 0,
      "keep automata that reject WORD", 0 },
    /**************************************************/
    RANGE_DOC_FULL,
    WORD_DOC,
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Transformations:", 7 },
230
    { "merge-transitions", OPT_MERGE, nullptr, 0,
231
      "merge transitions with same destination and acceptance", 0 },
232
233
234
    { "product", OPT_PRODUCT_AND, "FILENAME", 0,
      "build the product with the automaton in FILENAME "
      "to intersect languages", 0 },
235
    { "product-and", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
236
237
238
    { "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
239
    { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
240
      "randomize states and transitions (specify 's' or 't' to "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
241
      "randomize only states or transitions)", 0 },
242
243
    { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL,
      "allow more stuttering (two possible algorithms)", 0 },
244
    { "destut", OPT_DESTUT, nullptr, 0, "allow less stuttering", 0 },
245
246
    { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
      "remove all transitions in specified acceptance sets", 0 },
247
    { "strip-acceptance", OPT_STRIPACC, nullptr, 0,
248
      "remove the acceptance condition and all acceptance sets", 0 },
249
250
    { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
      "only keep specified states.  The first state will be the new "\
251
      "initial state.  Implies --remove-unreachable-states.", 0 },
252
    { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
253
      "put the acceptance condition in Disjunctive Normal Form", 0 },
254
    { "cnf-acceptance", OPT_CNF_ACC, nullptr, 0,
255
      "put the acceptance condition in Conjunctive Normal Form", 0 },
256
    { "remove-fin", OPT_REM_FIN, nullptr, 0,
257
      "rewrite the automaton without using Fin acceptance", 0 },
258
259
260
261
262
263
264
265
266
267
268
269
270
271
    { "generalized-rabin", OPT_GENERALIZED_RABIN,
      "unique-inf|share-inf", OPTION_ARG_OPTIONAL,
      "rewrite the acceptance condition as generalized Rabin; the default "
      "\"unique-inf\" option uses the generalized Rabin definition from the "
      "HOA format; the \"share-inf\" option allows clauses to share Inf sets, "
      "therefore reducing the number of sets", 0 },
    { "gra", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "generalized-streett", OPT_GENERALIZED_STREETT,
      "unique-fin|share-fin", OPTION_ARG_OPTIONAL,
      "rewrite the acceptance condition as generalized Streett;"
      " the \"share-fin\" option allows clauses to share Fin sets,"
      " therefore reducing the number of sets; the default"
      " \"unique-fin\" does not", 0 },
    { "gsa", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
272
    { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
273
      "remove unused acceptance sets from the automaton", 0 },
274
275
276
    { "complement", OPT_COMPLEMENT, nullptr, 0,
      "complement each automaton (currently support only deterministic "
      "automata)", 0 },
277
    { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
278
279
      "complement the acceptance condition (without touching the automaton)",
      0 },
280
281
282
    { "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 },
283
284
285
286
287
    { "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 },
288
    { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, nullptr, 0,
289
290
291
      "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 },
292
293
294
    { "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 },
295
296
    { "remove-unused-ap", OPT_REM_UNUSED_AP, nullptr, 0,
      "remove declared atomic propositions that are not used", 0 },
297
    { "remove-unreachable-states", OPT_REM_UNREACH, nullptr, 0,
298
      "remove states that are unreachable from the initial state", 0 },
299
    { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
300
301
      "remove states that are unreachable, or that cannot belong to an "
      "infinite path", 0 },
302
    { "separate-sets", OPT_SEP_SETS, nullptr, 0,
303
304
      "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 },
305
    { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL,
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
306
      "minimize the automaton using a SAT solver (only works for deterministic"
307
      " automata)", 0 },
308
    /**************************************************/
309
    { nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 8 },
310
311
    { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM",
312
      0 },
313
314
    { "highlight-nondet-edges", OPT_HIGHLIGHT_NONDET_EDGES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic edges with color NUM",
315
      0 },
316
317
318
    { "highlight-nondet", OPT_HIGHLIGHT_NONDET, "NUM",
      OPTION_ARG_OPTIONAL,
      "highlight nondeterministic states and edges with color NUM", 0},
319
320
    { "highlight-word", OPT_HIGHLIGHT_WORD, "[NUM,]WORD", 0,
      "highlight one run matching WORD using color NUM", 0},
321
    /**************************************************/
322
323
    { nullptr, 0, nullptr, 0,
      "If any option among --small, --deterministic, or --any is given, "
324
      "then the simplification level defaults to --high unless specified "
325
      "otherwise.  If any option among --low, --medium, or --high is given, "
326
      "then the simplification goal defaults to --small unless specified "
327
328
329
      "otherwise.  If none of those options are specified, then autfilt "
      "acts as is --any --low were given: these actually disable the "
      "simplification routines.", 22 },
330
    /**************************************************/
331
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
332
333
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
334
335
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
336
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
337
338
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
339
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
340
  {
341
    { &hoaread_argp, 0, nullptr, 0 },
342
343
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
344
    { &post_argp_disabled, 0, nullptr, 0 },
345
346
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
347
348
  };

349

350
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
351
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
352
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
353
354
355
356
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
357

358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
enum gra_type { GRA_NO = 0, GRA_SHARE_INF = 1, GRA_UNIQUE_INF = 2 };
static gra_type opt_gra = GRA_NO;
static char const *const gra_args[] =
{
  "default", "share-inf", "hoa", "unique-inf", nullptr
};
static gra_type const gra_types[] =
{
  GRA_UNIQUE_INF, GRA_SHARE_INF, GRA_UNIQUE_INF, GRA_UNIQUE_INF
};
ARGMATCH_VERIFY(gra_args, gra_types);

enum gsa_type { GSA_NO = 0, GSA_SHARE_FIN = 1, GSA_UNIQUE_FIN = 2 };
static gsa_type opt_gsa = GSA_NO;
static char const *const gsa_args[] =
{
  "default", "share-fin", "unique-fin", nullptr
};
static gsa_type const gsa_types[] =
{
  GSA_UNIQUE_FIN, GSA_SHARE_FIN, GSA_UNIQUE_FIN
};
ARGMATCH_VERIFY(gsa_args, gsa_types);

382
// We want all these variables to be destroyed when we exit main, to
383
384
385
386
387
388
// 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();
389
390
  spot::twa_graph_ptr product_and = nullptr;
  spot::twa_graph_ptr product_or = nullptr;
391
  spot::twa_graph_ptr intersect = nullptr;
392
  spot::twa_graph_ptr included_in = nullptr;
393
394
  spot::twa_graph_ptr equivalent_pos = nullptr;
  spot::twa_graph_ptr equivalent_neg = nullptr;
395
  spot::twa_graph_ptr are_isomorphic = nullptr;
396
397
398
  std::unique_ptr<spot::isomorphism_checker>
                         isomorphism_checker = nullptr;
  std::unique_ptr<unique_aut_t> uniq = nullptr;
399
400
  spot::exclusive_ap excl_ap;
  spot::remove_ap rem_ap;
401
  std::vector<spot::twa_graph_ptr> acc_words;
402
  std::vector<spot::twa_graph_ptr> rej_words;
403
  std::vector<std::pair<spot::twa_graph_ptr, unsigned>> hl_words;
404
405
}* opt;

406
static bool opt_merge = false;
407
408
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
409
static bool opt_is_unambiguous = false;
410
411
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
412
static bool opt_is_inherently_weak = false;
413
static bool opt_is_stutter_invariant = false;
414
static bool opt_invert = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
415
static range opt_states = { 0, std::numeric_limits<int>::max() };
416
417
static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() };
418
static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
419
420
421
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;
422
423
424
425
426
427
428
429
430
431
432
433
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;
434
435
static range opt_nondet_states = { 0, std::numeric_limits<int>::max() };
static bool opt_nondet_states_set = false;
436
static int opt_max_count = -1;
437
static bool opt_destut = false;
438
static char opt_instut = 0;
439
static bool opt_is_empty = false;
440
static bool opt_stripacc = false;
441
static bool opt_dnf_acc = false;
442
static bool opt_cnf_acc = false;
443
static bool opt_rem_fin = false;
444
static bool opt_clean_acc = false;
445
static bool opt_complement = false;
446
static bool opt_complement_acc = false;
447
static char* opt_decompose_strength = nullptr;
448
static spot::acc_cond::mark_t opt_mask_acc = 0U;
449
450
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
451
static bool opt_simplify_exclusive_ap = false;
452
453
static bool opt_rem_dead = false;
static bool opt_rem_unreach = false;
454
static bool opt_rem_unused_ap = false;
455
static bool opt_sep_sets = false;
456
static const char* opt_sat_minimize = nullptr;
457
458
static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
459

460
461
462
463
464
465
466
467
468
469
470
471
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
472
473
474
475
476
477
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
478
    case 'c':
479
      automaton_format = Count;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
480
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
481
482
483
    case 'F':
      jobs.emplace_back(arg, true);
      break;
484
485
486
    case 'n':
      opt_max_count = to_pos_int(arg);
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
487
    case 'u':
488
      opt->uniq =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
489
490
        std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
      break;
491
492
493
    case 'v':
      opt_invert = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
494
495
    case 'x':
      {
496
497
498
        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
499
500
      }
      break;
501
502
503
    case OPT_AP_N:
      opt_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
504
505
506
    case OPT_ACC_SETS:
      opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
507
508
509
510
    case OPT_ACC_SCCS:
      opt_acc_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
511
    case OPT_ACCEPT_WORD:
512
      try
513
514
515
516
        {
          opt->acc_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
517
      catch (const spot::parse_error& e)
518
519
520
521
        {
          error(2, 0, "failed to parse the argument of --accept-word:\n%s",
                e.what());
        }
522
      break;
523
    case OPT_ARE_ISOMORPHIC:
524
      opt->are_isomorphic = read_automaton(arg, opt->dict);
525
      break;
526
527
528
    case OPT_CLEAN_ACC:
      opt_clean_acc = true;
      break;
529
530
531
532
    case OPT_CNF_ACC:
      opt_dnf_acc = false;
      opt_cnf_acc = true;
      break;
533
534
535
    case OPT_COMPLEMENT:
      opt_complement = true;
      break;
536
537
538
    case OPT_COMPLEMENT_ACC:
      opt_complement_acc = true;
      break;
539
540
541
    case OPT_DECOMPOSE_STRENGTH:
      opt_decompose_strength = arg;
      break;
542
543
544
545
546
    case OPT_DESTUT:
      opt_destut = true;
      break;
    case OPT_DNF_ACC:
      opt_dnf_acc = true;
547
      opt_cnf_acc = false;
548
      break;
549
550
551
    case OPT_EDGES:
      opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
552
    case OPT_EXCLUSIVE_AP:
553
      opt->excl_ap.add_group(arg);
554
      break;
555
556
    case OPT_EQUIVALENT_TO:
      if (opt->equivalent_pos)
557
        error(2, 0, "only one --equivalent-to option can be given");
558
559
      opt->equivalent_pos = read_automaton(arg, opt->dict);
      opt->equivalent_neg =
560
        spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos));
561
      break;
562
563
564
565
566
567
568
569
570
571
572
573
574
575
    case OPT_GENERALIZED_RABIN:
      if (arg)
        opt_gra = XARGMATCH("--generalized-rabin", arg, gra_args, gra_types);
      else
        opt_gra = GRA_UNIQUE_INF;
      opt_gsa = GSA_NO;
      break;
    case OPT_GENERALIZED_STREETT:
      if (arg)
        opt_gsa = XARGMATCH("--generalized-streett", arg, gsa_args, gsa_types);
      else
        opt_gsa = GSA_UNIQUE_FIN;
      opt_gra = GRA_NO;
      break;
576
577
578
579
580
581
582
583
584
585
586
587
    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;
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
    case OPT_HIGHLIGHT_WORD:
      {
        char* endptr;
        int res = strtol(arg, &endptr, 10);
        if (endptr == arg)
          {
            res = 1;
          }
        else
          {
            if (res < 0)
              error(2, 0, "failed to parse the argument of --highlight-word: "
                    "%d is not positive", res);
            while (std::isspace(*endptr))
              ++endptr;
            if (*endptr != ',')
              error(2, 0, "failed to parse the argument of --highlight-word: "
                    "%d should be followed by a comma and WORD", res);
            arg = endptr + 1;
          }
        try
          {
            opt->hl_words.emplace_back(spot::parse_word(arg, opt->dict)
                                       ->as_automaton(), res);
          }
        catch (const spot::parse_error& e)
          {
            error(2, 0, "failed to parse the argument of --highlight-word:\n%s",
                  e.what());
          }
      }
      break;

621
    case OPT_INSTUT:
622
      if (!arg || (arg[0] == '1' && arg[1] == 0))
623
        opt_instut = 1;
624
      else if (arg[0] == '2' && arg[1] == 0)
625
        opt_instut = 2;
626
      else
627
        error(2, 0, "unknown argument for --instut: %s", arg);
628
      break;
629
630
    case OPT_INCLUDED_IN:
      {
631
632
633
634
635
636
        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);
637
638
      }
      break;
639
640
641
642
643
    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;
644
    case OPT_INTERSECT:
645
      opt->intersect = read_automaton(arg, opt->dict);
646
      break;
647
648
649
650
651
652
    case OPT_IS_COMPLETE:
      opt_is_complete = true;
      break;
    case OPT_IS_DETERMINISTIC:
      opt_is_deterministic = true;
      break;
653
654
655
    case OPT_IS_EMPTY:
      opt_is_empty = true;
      break;
656
657
658
    case OPT_IS_INHERENTLY_WEAK:
      opt_is_inherently_weak = true;
      break;
659
660
    case OPT_IS_STUTTER_INVARIANT:
      opt_is_stutter_invariant = true;
661
      break;
662
663
664
    case OPT_IS_TERMINAL:
      opt_is_terminal = true;
      break;
665
666
667
    case OPT_IS_UNAMBIGUOUS:
      opt_is_unambiguous = true;
      break;
668
669
670
    case OPT_IS_WEAK:
      opt_is_weak = true;
      break;
671
672
673
674
675
676
    case OPT_KEEP_STATES:
      {
        std::vector<long> values = to_longs(arg);
        if (!values.empty())
          opt_keep_states_initial = values[0];
        for (auto res : values)
677
678
679
680
          {
            if (res < 0)
              error(2, 0, "state ids should be non-negative:"
                    " --mask-acc=%ld", res);
681
682
683
            // 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);
684
685
686
687
            opt_keep_states[res] = true;
          }
        opt_rem_unreach = true;
        break;
688
      }
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
    case OPT_MERGE:
      opt_merge = true;
      break;
    case OPT_MASK_ACC:
      {
        for (auto res : to_longs(arg))
          {
            if (res < 0)
              error(2, 0, "acceptance sets should be non-negative:"
                    " --mask-acc=%ld", res);
            if (static_cast<unsigned long>(res)
                > sizeof(spot::acc_cond::mark_t::value_t))
              error(2, 0, "this implementation does not support that many"
                    " acceptance sets: --mask-acc=%ld", res);
            opt_mask_acc.set(res);
          }
        break;
      }
    case OPT_NONDET_STATES:
      opt_nondet_states = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_nondet_states_set = true;
      break;
711
    case OPT_PRODUCT_AND:
712
      {
713
714
715
716
717
718
        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));
719
720
721
722
      }
      break;
    case OPT_PRODUCT_OR:
      {
723
724
725
726
727
728
        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));
729
730
      }
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
731
732
    case OPT_RANDOMIZE:
      if (arg)
733
734
735
736
737
738
739
740
741
742
743
744
745
746
        {
          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
747
      else
748
749
750
751
        {
          randomize_tr = true;
          randomize_st = true;
        }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
752
      break;
753
754
755
756
    case OPT_REJ_SCCS:
      opt_rej_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
757
758
    case OPT_REJECT_WORD:
      try
759
760
761
762
        {
          opt->rej_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
763
      catch (const spot::parse_error& e)
764
765
766
767
        {
          error(2, 0, "failed to parse the argument of --reject-word:\n%s",
                e.what());
        }
768
      break;
769
    case OPT_REM_AP:
770
      opt->rem_ap.add_ap(arg);
771
      break;
772
773
774
    case OPT_REM_DEAD:
      opt_rem_dead = true;
      break;
775
776
777
    case OPT_REM_FIN:
      opt_rem_fin = true;
      break;
778
779
780
    case OPT_REM_UNREACH:
      opt_rem_unreach = true;
      break;
781
782
783
    case OPT_REM_UNUSED_AP:
      opt_rem_unused_ap = true;
      break;
784
785
786
    case OPT_SAT_MINIMIZE:
      opt_sat_minimize = arg ? arg : "";
      break;
787
788
789
790
    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
791
792
793
    case OPT_SEED:
      opt_seed = to_int(arg);
      break;
794
795
796
    case OPT_SEP_SETS:
      opt_sep_sets = true;
      break;
797
798
799
800
    case OPT_SIMPLIFY_EXCLUSIVE_AP:
      opt_simplify_exclusive_ap = true;
      opt_merge = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
801
802
803
    case OPT_STATES:
      opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
804
805
806
    case OPT_STRIPACC:
      opt_stripacc = true;
      break;
807
808
809
810
811
812
813
814
815
    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;
816
817
818
819
820
821
822
823
    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;
824
825
826
827
828
    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
829
830
831
832
833
834
835
836
837
838
    case ARGP_KEY_ARG:
      jobs.emplace_back(arg, true);
      break;

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
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
856
857
858

namespace
{
859
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
860
  {
861
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
862
    spot::postprocessor& post;
863
    automaton_printer printer;
864
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
865
866

    hoa_processor(spot::postprocessor& post)
867
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
868
869
870
871
    {
    }

    int
872
    process_formula(spot::formula, const char*, int) override
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
873
874
875
876
877
    {
      SPOT_UNREACHABLE();
    }

    int
878
    process_automaton(const spot::const_parsed_aut_ptr& haut,
879
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
880
881
882
    {
      spot::stopwatch sw;
      sw.start();
883

884
885
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
886
      // merge_edges()) and the statistics about it make sense.
887
      auto aut = ((automaton_format == Stats) || opt_name)
888
889
        ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
        : haut->aut;
890

891
892
      // Preprocessing.

893
      if (opt_stripacc)
894
        spot::strip_acceptance_here(aut);
895
      if (opt_merge)
896
        aut->merge_edges();
897
      if (opt_clean_acc || opt_rem_fin)
898
        cleanup_acceptance_here(aut);
899
      if (opt_sep_sets)
900
        separate_sets_here(aut);
901
      if (opt_complement_acc)
902
903
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
904
      if (opt_rem_fin)
905
        aut = remove_fin(aut);
906
      if (opt_dnf_acc)
907
908
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
909
      if (opt_cnf_acc)
910
911
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
912

913
914
915
916
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
917
      matched &= opt_states.contains(aut->num_states());
918
      matched &= opt_edges.contains(aut->num_edges());
919
      matched &= opt_accsets.contains(aut->acc().num_sets());
920
      matched &= opt_ap_n.contains(aut->ap().size());
921
922
923
924
925
926
927
      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)
928
        matched &= is_complete(aut);
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
      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);
            }
        }
971
972
      if (opt_nondet_states_set)
        matched &= opt_nondet_states.contains(spot::count_nondet_states(aut));
973
      if (opt_is_deterministic)
974
        matched &= is_deterministic(aut);
975
      else if (opt_is_unambiguous)
976
        matched &= is_unambiguous(aut);
977
      if (opt_is_terminal)
978
        matched &= is_terminal_automaton(aut);
979
      else if (opt_is_weak)
980
        matched &= is_weak_automaton(aut);
981
      else if (opt_is_inherently_weak)
982
        matched &= is_inherently_weak_automaton(aut);
983
984
      if (opt->are_isomorphic)
        matched &= opt->isomorphism_checker->is_isomorphic(aut);
985
      if (opt_is_empty)
986
        matched &= aut->is_empty();
987
      if (opt->intersect)
988
        matched &= !spot::product(aut, opt->intersect)->is_empty();
989
      if (opt->included_in)
990
        matched &= spot::product(aut, opt->included_in)->is_empty();
991
      if (opt->equivalent_pos)
992
993
994
        matched &= spot::product(aut, opt->equivalent_neg)->is_empty()
          && spot::product(dtwa_complement(ensure_deterministic(aut)),
                           opt->equivalent_pos)->is_empty();
995
996

      if (matched && !opt->acc_words.empty())
997
998
999
1000
1001
1002
        for (auto& word_aut: opt->acc_words)
          if (spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
1003
      if (matched && !opt->rej_words.empty())
1004
1005
1006
1007
1008
1009
        for (auto& word_aut: opt->rej_words)
          if (!spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
1010
1011
1012
1013
1014
1015
      if (opt_is_stutter_invariant)
        {
          check_stutter_invariance(aut);
          assert(aut->prop_stutter_invariant().is_known());
          matched &= aut->prop_stutter_invariant().is_true();
        }
1016

1017
1018
      // Drop or keep matched automata depending on the --invert option
      if (matched == opt_invert)
1019
1020
        return 0;

1021
1022
      // Postprocessing.

1023
      if (opt_mask_acc)
1024
        aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());
1025

1026
      if (!opt->rem_ap.empty())
1027
        aut = opt->rem_ap.strip(aut);
1028

1029
1030
1031
1032
1033
      // opt_simplify_exclusive_ap is handled only after
      // post-processing.
      if (!opt->excl_ap.empty())
        aut = opt->excl_ap.constrain(aut, false);

1034
      if (opt_destut)
1035
        aut = spot::closure(std::move(aut));
1036
      if (opt_instut == 1)
1037
        aut = spot::sl(std::move(aut));
1038
      else if (opt_instut == 2)
1039
        aut = spot::sl2(std::move(aut));
1040

1041
      if (!opt_keep_states.empty())
1042
        aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial);
1043
      if (opt_rem_dead)
1044
        aut->purge_dead_states();
1045
      else if (opt_rem_unreach)
1046
        aut->purge_unreachable_states();
1047

1048
      if (opt->product_and)
1049
        aut = spot::product(std::move(aut), opt->product_and);
1050
      if (opt->product_or)
1051
        aut = spot::product_or(std::move(aut), opt->product_or);
1052

1053
      if (opt_decompose_strength)
1054
1055
1056
1057
1058
        {
          aut = decompose_strength(aut, opt_decompose_strength);
          if (!aut)
            return 0;
        }
1059

1060
      if (opt_sat_minimize)