autfilt.cc 36.7 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
  OPT_NONDET_STATES,
109
110
  OPT_PRODUCT_AND,
  OPT_PRODUCT_OR,
111
  OPT_RANDOMIZE,
112
  OPT_REJ_SCCS,
113
  OPT_REJECT_WORD,
114
  OPT_REM_AP,
115
116
  OPT_REM_DEAD,
  OPT_REM_UNREACH,
117
  OPT_REM_UNUSED_AP,
118
  OPT_REM_FIN,
119
  OPT_SAT_MINIMIZE,
120
  OPT_SCCS,
121
  OPT_SEED,
122
  OPT_SEP_SETS,
123
  OPT_SIMPLIFY_EXCLUSIVE_AP,
124
125
  OPT_STATES,
  OPT_STRIPACC,
126
127
  OPT_TERMINAL_SCCS,
  OPT_TRIV_SCCS,
128
129
  OPT_USED_AP_N,
  OPT_UNUSED_AP_N,
130
  OPT_WEAK_SCCS,
131
};
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
132
133
134
135

static const argp_option options[] =
  {
    /**************************************************/
136
    { nullptr, 0, nullptr, 0, "Input:", 1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
137
138
139
    { "file", 'F', "FILENAME", 0,
      "process the automaton in FILENAME", 0 },
    /**************************************************/
140
    { "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
141
    { "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
142
    /**************************************************/
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
    { 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 },
    { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
      "keep only unambiguous automata", 0 },
    { "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
      "keep only terminal automata", 0 },
    { "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 },
186
187
    { "nondet-states", OPT_NONDET_STATES, "RANGE", 0,
      "keep automata whose number of nondeterministic states is in RANGE", 0 },
188
189
190
191
192
193
194
195
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
    { "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 },
222
    { "merge-transitions", OPT_MERGE, nullptr, 0,
223
      "merge transitions with same destination and acceptance", 0 },
224
225
226
    { "product", OPT_PRODUCT_AND, "FILENAME", 0,
      "build the product with the automaton in FILENAME "
      "to intersect languages", 0 },
227
    { "product-and", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
228
229
230
    { "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
231
    { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
232
      "randomize states and transitions (specify 's' or 't' to "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
233
      "randomize only states or transitions)", 0 },
234
235
    { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL,
      "allow more stuttering (two possible algorithms)", 0 },
236
    { "destut", OPT_DESTUT, nullptr, 0, "allow less stuttering", 0 },
237
238
    { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
      "remove all transitions in specified acceptance sets", 0 },
239
    { "strip-acceptance", OPT_STRIPACC, nullptr, 0,
240
      "remove the acceptance condition and all acceptance sets", 0 },
241
242
    { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
      "only keep specified states.  The first state will be the new "\
243
      "initial state.  Implies --remove-unreachable-states.", 0 },
244
    { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
245
      "put the acceptance condition in Disjunctive Normal Form", 0 },
246
    { "cnf-acceptance", OPT_CNF_ACC, nullptr, 0,
247
      "put the acceptance condition in Conjunctive Normal Form", 0 },
248
    { "remove-fin", OPT_REM_FIN, nullptr, 0,
249
      "rewrite the automaton without using Fin acceptance", 0 },
250
    { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
251
      "remove unused acceptance sets from the automaton", 0 },
252
253
254
    { "complement", OPT_COMPLEMENT, nullptr, 0,
      "complement each automaton (currently support only deterministic "
      "automata)", 0 },
255
    { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
256
257
      "complement the acceptance condition (without touching the automaton)",
      0 },
258
259
260
    { "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 },
261
262
263
264
265
    { "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 },
266
    { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, nullptr, 0,
267
268
269
      "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 },
270
271
272
    { "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 },
273
274
    { "remove-unused-ap", OPT_REM_UNUSED_AP, nullptr, 0,
      "remove declared atomic propositions that are not used", 0 },
275
    { "remove-unreachable-states", OPT_REM_UNREACH, nullptr, 0,
276
      "remove states that are unreachable from the initial state", 0 },
277
    { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
278
279
      "remove states that are unreachable, or that cannot belong to an "
      "infinite path", 0 },
280
    { "separate-sets", OPT_SEP_SETS, nullptr, 0,
281
282
      "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 },
283
    { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL,
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
284
      "minimize the automaton using a SAT solver (only works for deterministic"
285
      " automata)", 0 },
286
287
288
289
290
291
292
293
294
    { "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},
295
    /**************************************************/
296
297
    { nullptr, 0, nullptr, 0,
      "If any option among --small, --deterministic, or --any is given, "
298
      "then the simplification level defaults to --high unless specified "
299
      "otherwise.  If any option among --low, --medium, or --high is given, "
300
      "then the simplification goal defaults to --small unless specified "
301
302
303
      "otherwise.  If none of those options are specified, then autfilt "
      "acts as is --any --low were given: these actually disable the "
      "simplification routines.", 22 },
304
    /**************************************************/
305
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
306
307
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
308
309
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
310
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
311
312
  };

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

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

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

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

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

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
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
753
754
755

namespace
{
756
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
757
  {
758
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
759
    spot::postprocessor& post;
760
    automaton_printer printer;
761
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
762
763

    hoa_processor(spot::postprocessor& post)
764
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
765
766
767
768
    {
    }

    int
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
769
    process_formula(spot::formula, const char*, int)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
770
771
772
773
774
    {
      SPOT_UNREACHABLE();
    }

    int
775
    process_automaton(const spot::const_parsed_aut_ptr& haut,
776
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
777
778
779
    {
      spot::stopwatch sw;
      sw.start();
780

781
782
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
783
      // merge_edges()) and the statistics about it make sense.
784
      auto aut = ((automaton_format == Stats) || opt_name)
785
786
        ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
        : haut->aut;
787

788
789
      // Preprocessing.

790
      if (opt_stripacc)
791
        spot::strip_acceptance_here(aut);
792
      if (opt_merge)
793
        aut->merge_edges();
794
      if (opt_clean_acc || opt_rem_fin)
795
        cleanup_acceptance_here(aut);
796
      if (opt_sep_sets)
797
        separate_sets_here(aut);
798
      if (opt_complement_acc)
799
800
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
801
      if (opt_rem_fin)
802
        aut = remove_fin(aut);
803
      if (opt_dnf_acc)
804
805
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
806
      if (opt_cnf_acc)
807
808
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
809

810
811
812
813
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
814
      matched &= opt_states.contains(aut->num_states());
815
      matched &= opt_edges.contains(aut->num_edges());
816
      matched &= opt_accsets.contains(aut->acc().num_sets());
817
      matched &= opt_ap_n.contains(aut->ap().size());
818
819
820
821
822
823
824
      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)
825
        matched &= is_complete(aut);
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
858
859
860
861
862
863
864
865
866
867
      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);
            }
        }
868
869
      if (opt_nondet_states_set)
        matched &= opt_nondet_states.contains(spot::count_nondet_states(aut));
870
      if (opt_is_deterministic)
871
        matched &= is_deterministic(aut);
872
      else if (opt_is_unambiguous)
873
        matched &= is_unambiguous(aut);
874
      if (opt_is_terminal)
875
        matched &= is_terminal_automaton(aut);
876
      else if (opt_is_weak)
877
        matched &= is_weak_automaton(aut);
878
      else if (opt_is_inherently_weak)
879
        matched &= is_inherently_weak_automaton(aut);
880
881
      if (opt->are_isomorphic)
        matched &= opt->isomorphism_checker->is_isomorphic(aut);
882
      if (opt_is_empty)
883
        matched &= aut->is_empty();
884
      if (opt->intersect)
885
        matched &= !spot::product(aut, opt->intersect)->is_empty();
886
      if (opt->included_in)
887
        matched &= spot::product(aut, opt->included_in)->is_empty();
888
      if (opt->equivalent_pos)
889
890
891
        matched &= spot::product(aut, opt->equivalent_neg)->is_empty()
          && spot::product(dtwa_complement(ensure_deterministic(aut)),
                           opt->equivalent_pos)->is_empty();
892
893

      if (matched && !opt->acc_words.empty())
894
895
896
897
898
899
        for (auto& word_aut: opt->acc_words)
          if (spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
900
      if (matched && !opt->rej_words.empty())
901
902
903
904
905
906
        for (auto& word_aut: opt->rej_words)
          if (!spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
907

908
909
      // Drop or keep matched automata depending on the --invert option
      if (matched == opt_invert)
910
911
        return 0;

912
913
      // Postprocessing.

914
      if (opt_mask_acc)
915
        aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());
916

917
      if (!opt->rem_ap.empty())
918
        aut = opt->rem_ap.strip(aut);
919

920
921
922
923
924
      // opt_simplify_exclusive_ap is handled only after
      // post-processing.
      if (!opt->excl_ap.empty())
        aut = opt->excl_ap.constrain(aut, false);

925
      if (opt_destut)
926
        aut = spot::closure(std::move(aut));
927
      if (opt_instut == 1)
928
        aut = spot::sl(std::move(aut));
929
      else if (opt_instut == 2)
930
        aut = spot::sl2(std::move(aut));
931

932
      if (!opt_keep_states.empty())
933
        aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial);
934
      if (opt_rem_dead)
935
        aut->purge_dead_states();
936
      else if (opt_rem_unreach)
937
        aut->purge_unreachable_states();
938

939
      if (opt->product_and)
940
        aut = spot::product(std::move(aut), opt->product_and);
941
      if (opt->product_or)
942
        aut = spot::product_or(std::move(aut), opt->product_or);
943

944
      if (opt_decompose_strength)
945
946
947
948
949
        {
          aut = decompose_strength(aut, opt_decompose_strength);
          if (!aut)
            return 0;
        }
950

951
      if (opt_sat_minimize)
952
953
954
955
956
        {
          aut = spot::sat_minimize(aut, opt_sat_minimize, sbacc);
          if (!aut)
            return 0;
        }
957

958
      if (opt_complement)
959
        aut = spot::dtwa_complement(ensure_deterministic(aut));
960

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

963
      if (opt_simplify_exclusive_ap && !opt->excl_ap.empty())
964
965
966
        aut = opt->excl_ap.constrain(aut, true);
      else if (opt_rem_unused_ap) // constrain(aut, true) already does that
        aut->remove_unused_ap();
967

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
968
      if (randomize_st || randomize_tr)
969
        spot::randomize(aut, randomize_st, randomize_tr);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
970

971
972
973
974
975
      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);

976
977
      const double conversion_time = sw.stop();

978
      if (opt->uniq)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
979
980
        {
          auto tmp =
981
982
            spot::canonicalize(make_twa_graph(aut,
                                                 spot::twa::prop_set::all()));
983
          if (!opt->uniq->emplace(tmp->edge_vector().begin() + 1,
984
985
                                  tmp->edge_vector().end()).second)
            return 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
986
987
        }

988
989
      ++match_count;

990
      printer.print(aut, nullptr, filename, -1, conversion_time, haut);
991
992

      if (opt_max_count >= 0 && match_count >= opt_max_count)
993
        abort_run = true;
994

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
995
996
      return 0;
    }
997

998
    int
999
    aborted(const spot::const_parsed_aut_ptr& h, const char* filename)
1000
1001
1002
1003
    {
      std::cerr << filename << ':' << h->loc << ": aborted input automaton\n";
      return 2;
    }
1004
1005
1006
1007

    int
    process_file(const char* filename)
    {
1008
      auto hp = spot::automaton_stream_parser(filename, opt_parse);
1009
      int err = 0;
1010
      while (!abort_run)
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
        {
          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
1022
            process_automaton(haut, filename);