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

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
296
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
297
  {
298
    { &hoaread_argp, 0, nullptr, 0 },
299
300
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
301
    { &post_argp_disabled, 0, nullptr, 0 },
302
303
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
304
305
  };

306
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
307
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
308
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
309
310
311
312
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
313

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

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

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

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
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
716
717
718

namespace
{
719
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
720
  {
721
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
722
    spot::postprocessor& post;
723
    automaton_printer printer;
724
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
725
726

    hoa_processor(spot::postprocessor& post)
727
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
728
729
730
731
    {
    }

    int
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
732
    process_formula(spot::formula, const char*, int)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
733
734
735
736
737
    {
      SPOT_UNREACHABLE();
    }

    int
738
    process_automaton(const spot::const_parsed_aut_ptr& haut,
739
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
740
741
742
    {
      spot::stopwatch sw;
      sw.start();
743

744
745
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
746
      // merge_edges()) and the statistics about it make sense.
747
      auto aut = ((automaton_format == Stats) || opt_name)
748
749
        ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
        : haut->aut;
750

751
752
      // Preprocessing.

753
      if (opt_stripacc)
754
        spot::strip_acceptance_here(aut);
755
      if (opt_merge)
756
        aut->merge_edges();
757
      if (opt_clean_acc || opt_rem_fin)
758
        cleanup_acceptance_here(aut);
759
      if (opt_sep_sets)
760
        separate_sets_here(aut);
761
      if (opt_complement_acc)
762
763
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
764
      if (opt_rem_fin)
765
        aut = remove_fin(aut);
766
      if (opt_dnf_acc)
767
768
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
769
      if (opt_cnf_acc)
770
771
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
772

773
774
775
776
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
777
      matched &= opt_states.contains(aut->num_states());
778
      matched &= opt_edges.contains(aut->num_edges());
779
      matched &= opt_accsets.contains(aut->acc().num_sets());
780
      matched &= opt_ap_n.contains(aut->ap().size());
781
782
783
784
785
786
787
      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)
788
        matched &= is_complete(aut);
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
      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);
            }
        }
831
      if (opt_is_deterministic)
832
        matched &= is_deterministic(aut);
833
      else if (opt_is_unambiguous)
834
        matched &= is_unambiguous(aut);
835
      if (opt_is_terminal)
836
        matched &= is_terminal_automaton(aut);
837
      else if (opt_is_weak)
838
        matched &= is_weak_automaton(aut);
839
      else if (opt_is_inherently_weak)
840
        matched &= is_inherently_weak_automaton(aut);
841
842
      if (opt->are_isomorphic)
        matched &= opt->isomorphism_checker->is_isomorphic(aut);
843
      if (opt_is_empty)
844
        matched &= aut->is_empty();
845
      if (opt->intersect)
846
        matched &= !spot::product(aut, opt->intersect)->is_empty();
847
      if (opt->included_in)
848
        matched &= spot::product(aut, opt->included_in)->is_empty();
849
      if (opt->equivalent_pos)
850
851
852
        matched &= spot::product(aut, opt->equivalent_neg)->is_empty()
          && spot::product(dtwa_complement(ensure_deterministic(aut)),
                           opt->equivalent_pos)->is_empty();
853
854

      if (matched && !opt->acc_words.empty())
855
856
857
858
859
860
        for (auto& word_aut: opt->acc_words)
          if (spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
861
      if (matched && !opt->rej_words.empty())
862
863
864
865
866
867
        for (auto& word_aut: opt->rej_words)
          if (!spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
868

869
870
      // Drop or keep matched automata depending on the --invert option
      if (matched == opt_invert)
871
872
        return 0;

873
874
      // Postprocessing.

875
      if (opt_mask_acc)
876
        aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());
877

878
      if (!opt->rem_ap.empty())
879
        aut = opt->rem_ap.strip(aut);
880

881
882
883
884
885
      // opt_simplify_exclusive_ap is handled only after
      // post-processing.
      if (!opt->excl_ap.empty())
        aut = opt->excl_ap.constrain(aut, false);

886
      if (opt_destut)
887
        aut = spot::closure(std::move(aut));
888
      if (opt_instut == 1)
889
        aut = spot::sl(std::move(aut));
890
      else if (opt_instut == 2)
891
        aut = spot::sl2(std::move(aut));
892

893
      if (!opt_keep_states.empty())
894
        aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial);
895
      if (opt_rem_dead)
896
        aut->purge_dead_states();
897
      else if (opt_rem_unreach)
898
        aut->purge_unreachable_states();
899

900
      if (opt->product_and)
901
        aut = spot::product(std::move(aut), opt->product_and);
902
      if (opt->product_or)
903
        aut = spot::product_or(std::move(aut), opt->product_or);
904

905
      if (opt_decompose_strength)
906
907
908
909
910
        {
          aut = decompose_strength(aut, opt_decompose_strength);
          if (!aut)
            return 0;
        }
911

912
      if (opt_sat_minimize)
913
914
915
916
917
        {
          aut = spot::sat_minimize(aut, opt_sat_minimize, sbacc);
          if (!aut)
            return 0;
        }
918

919
      if (opt_complement)
920
        aut = spot::dtwa_complement(ensure_deterministic(aut));
921

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

924
      if (opt_simplify_exclusive_ap && !opt->excl_ap.empty())
925
926
927
        aut = opt->excl_ap.constrain(aut, true);
      else if (opt_rem_unused_ap) // constrain(aut, true) already does that
        aut->remove_unused_ap();
928

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
929
      if (randomize_st || randomize_tr)
930
        spot::randomize(aut, randomize_st, randomize_tr);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
931

932
933
      const double conversion_time = sw.stop();

934
      if (opt->uniq)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
935
936
        {
          auto tmp =
937
938
            spot::canonicalize(make_twa_graph(aut,
                                                 spot::twa::prop_set::all()));
939
          if (!opt->uniq->emplace(tmp->edge_vector().begin() + 1,
940
941
                                  tmp->edge_vector().end()).second)
            return 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
942
943
        }

944
945
      ++match_count;

946
      printer.print(aut, nullptr, filename, -1, conversion_time, haut);
947
948

      if (opt_max_count >= 0 && match_count >= opt_max_count)
949
        abort_run = true;
950

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
951
952
      return 0;
    }
953

954
    int
955
    aborted(const spot::const_parsed_aut_ptr& h, const char* filename)
956
957
958
959
    {
      std::cerr << filename << ':' << h->loc << ": aborted input automaton\n";
      return 2;
    }
960
961
962
963

    int
    process_file(const char* filename)
    {