autfilt.cc 36.2 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
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
186
187
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
    { 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 },
    { "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 },
219
    { "merge-transitions", OPT_MERGE, nullptr, 0,
220
      "merge transitions with same destination and acceptance", 0 },
221
222
223
    { "product", OPT_PRODUCT_AND, "FILENAME", 0,
      "build the product with the automaton in FILENAME "
      "to intersect languages", 0 },
224
    { "product-and", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
225
226
227
    { "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
228
    { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
229
      "randomize states and transitions (specify 's' or 't' to "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
230
      "randomize only states or transitions)", 0 },
231
232
    { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL,
      "allow more stuttering (two possible algorithms)", 0 },
233
    { "destut", OPT_DESTUT, nullptr, 0, "allow less stuttering", 0 },
234
235
    { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
      "remove all transitions in specified acceptance sets", 0 },
236
    { "strip-acceptance", OPT_STRIPACC, nullptr, 0,
237
      "remove the acceptance condition and all acceptance sets", 0 },
238
239
    { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
      "only keep specified states.  The first state will be the new "\
240
      "initial state.  Implies --remove-unreachable-states.", 0 },
241
    { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
242
      "put the acceptance condition in Disjunctive Normal Form", 0 },
243
    { "cnf-acceptance", OPT_CNF_ACC, nullptr, 0,
244
      "put the acceptance condition in Conjunctive Normal Form", 0 },
245
    { "remove-fin", OPT_REM_FIN, nullptr, 0,
246
      "rewrite the automaton without using Fin acceptance", 0 },
247
    { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
248
      "remove unused acceptance sets from the automaton", 0 },
249
250
251
    { "complement", OPT_COMPLEMENT, nullptr, 0,
      "complement each automaton (currently support only deterministic "
      "automata)", 0 },
252
    { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
253
254
      "complement the acceptance condition (without touching the automaton)",
      0 },
255
256
257
    { "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 },
258
259
260
261
262
    { "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 },
263
    { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, nullptr, 0,
264
265
266
      "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 },
267
268
269
    { "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 },
270
271
    { "remove-unused-ap", OPT_REM_UNUSED_AP, nullptr, 0,
      "remove declared atomic propositions that are not used", 0 },
272
    { "remove-unreachable-states", OPT_REM_UNREACH, nullptr, 0,
273
      "remove states that are unreachable from the initial state", 0 },
274
    { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
275
276
      "remove states that are unreachable, or that cannot belong to an "
      "infinite path", 0 },
277
    { "separate-sets", OPT_SEP_SETS, nullptr, 0,
278
279
      "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 },
280
    { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL,
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
281
      "minimize the automaton using a SAT solver (only works for deterministic"
282
      " automata)", 0 },
283
284
285
286
287
288
289
290
291
    { "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},
292
    /**************************************************/
293
294
    { nullptr, 0, nullptr, 0,
      "If any option among --small, --deterministic, or --any is given, "
295
      "then the simplification level defaults to --high unless specified "
296
      "otherwise.  If any option among --low, --medium, or --high is given, "
297
      "then the simplification goal defaults to --small unless specified "
298
299
300
      "otherwise.  If none of those options are specified, then autfilt "
      "acts as is --any --low were given: these actually disable the "
      "simplification routines.", 22 },
301
    /**************************************************/
302
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
303
304
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
305
306
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
307
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
308
309
  };

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

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

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

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

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

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

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

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

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

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

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

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

779
780
      // Preprocessing.

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

801
802
803
804
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
805
      matched &= opt_states.contains(aut->num_states());
806
      matched &= opt_edges.contains(aut->num_edges());
807
      matched &= opt_accsets.contains(aut->acc().num_sets());
808
      matched &= opt_ap_n.contains(aut->ap().size());
809
810
811
812
813
814
815
      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)
816
        matched &= is_complete(aut);
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
858
      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);
            }
        }
859
      if (opt_is_deterministic)
860
        matched &= is_deterministic(aut);
861
      else if (opt_is_unambiguous)
862
        matched &= is_unambiguous(aut);
863
      if (opt_is_terminal)
864
        matched &= is_terminal_automaton(aut);
865
      else if (opt_is_weak)
866
        matched &= is_weak_automaton(aut);
867
      else if (opt_is_inherently_weak)
868
        matched &= is_inherently_weak_automaton(aut);
869
870
      if (opt->are_isomorphic)
        matched &= opt->isomorphism_checker->is_isomorphic(aut);
871
      if (opt_is_empty)
872
        matched &= aut->is_empty();
873
      if (opt->intersect)
874
        matched &= !spot::product(aut, opt->intersect)->is_empty();
875
      if (opt->included_in)
876
        matched &= spot::product(aut, opt->included_in)->is_empty();
877
      if (opt->equivalent_pos)
878
879
880
        matched &= spot::product(aut, opt->equivalent_neg)->is_empty()
          && spot::product(dtwa_complement(ensure_deterministic(aut)),
                           opt->equivalent_pos)->is_empty();
881
882

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

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

901
902
      // Postprocessing.

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

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

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

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

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

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

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

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

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

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

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

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

960
961
962
963
964
      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);

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

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

977
978
      ++match_count;

979
      printer.print(aut, nullptr, filename, -1, conversion_time, haut);
980
981

      if (opt_max_count >= 0 && match_count >= opt_max_count)
982
        abort_run = true;
983

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
984
985
      return 0;
    }
986

987
    int
988
    aborted(const spot::const_parsed_aut_ptr& h, const char* filename)
989
990
991
992
    {
      std::cerr << filename << ':' << h->loc << ": aborted input automaton\n";
      return 2;
    }
993
994
995
996

    int
    process_file(const char* filename)
    {
997
      auto hp = spot::automaton_stream_parser(filename, opt_parse);
998
      int err = 0;
999
      while (!abort_run)
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
        {
          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
1011
            process_automaton(haut, filename);
1012
        }
1013
1014
      return err;
    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1015
1016
1017
1018
1019
1020
1021
1022
1023
  };
}

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

  const argp ap = { options, parse_opt, "[FILENAMES...]",
1024
                    argp_program_doc, children, nullptr, nullptr };