autfilt.cc 45.1 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
// -*- coding: utf-8 -*-
2 3
// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
// et 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>
27 28
#include <sys/stat.h>
#include <unistd.h>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
29 30 31

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

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

43 44
#include <spot/misc/optionmap.hh>
#include <spot/misc/random.hh>
45
#include <spot/misc/timer.hh>
46 47 48 49
#include <spot/parseaut/public.hh>
#include <spot/tl/exclusive.hh>
#include <spot/twaalgos/are_isomorphic.hh>
#include <spot/twaalgos/canonicalize.hh>
50
#include <spot/twaalgos/cobuchi.hh>
51 52
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/dtwasat.hh>
53
#include <spot/twaalgos/dualize.hh>
54
#include <spot/twaalgos/gtec/gtec.hh>
55
#include <spot/twaalgos/hoa.hh>
56 57
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/isunamb.hh>
58
#include <spot/twaalgos/isweakscc.hh>
59
#include <spot/twaalgos/langmap.hh>
60 61 62 63 64 65 66 67 68 69 70 71 72
#include <spot/twaalgos/mask.hh>
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/randomize.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/remprop.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/sepsets.hh>
#include <spot/twaalgos/split.hh>
#include <spot/twaalgos/strength.hh>
#include <spot/twaalgos/stripacc.hh>
#include <spot/twaalgos/stutter.hh>
#include <spot/twaalgos/sum.hh>
#include <spot/twaalgos/totgba.hh>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
73

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
74
static const char argp_program_doc[] ="\
75
Convert, transform, and filter omega-automata.\v\
76 77 78 79
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
80

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

155 156
#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
157 158 159
static const argp_option options[] =
  {
    /**************************************************/
160
    { nullptr, 0, nullptr, 0, "Input:", 1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
161 162 163
    { "file", 'F', "FILENAME", 0,
      "process the automaton in FILENAME", 0 },
    /**************************************************/
164
    { "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
165
    { "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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 },
186 187
    { "is-semi-deterministic", OPT_IS_SEMI_DETERMINISTIC, nullptr, 0,
      "keep semi-deterministic automata", 0 },
188 189
    { "is-empty", OPT_IS_EMPTY, nullptr, 0,
      "keep automata with an empty language", 0 },
190 191
    { "is-stutter-invariant", OPT_IS_STUTTER_INVARIANT, nullptr, 0,
      "keep automata representing stutter-invariant properties", 0 },
192 193
    { "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
      "keep only terminal automata", 0 },
194 195
    { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
      "keep only unambiguous automata", 0 },
196 197 198 199
    { "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 },
200 201
    { "is-very-weak", OPT_IS_VERY_WEAK, nullptr, 0,
      "keep only very-weak automata", 0 },
202 203
    { "is-alternating", OPT_IS_ALTERNATING, nullptr, 0,
      "keep only automata using universal branching", 0 },
204 205 206 207 208 209 210 211 212 213 214 215 216 217
    { "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 },
218 219
    { "nondet-states", OPT_NONDET_STATES, "RANGE", 0,
      "keep automata whose number of nondeterministic states is in RANGE", 0 },
220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253
    { "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 },
254
    { "merge-transitions", OPT_MERGE, nullptr, 0,
255
      "merge transitions with same destination and acceptance", 0 },
256 257 258
    { "product", OPT_PRODUCT_AND, "FILENAME", 0,
      "build the product with the automaton in FILENAME "
      "to intersect languages", 0 },
259
    { "product-and", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
260 261 262
    { "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
263
    { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
264
      "randomize states and transitions (specify 's' or 't' to "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
265
      "randomize only states or transitions)", 0 },
266 267
    { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL,
      "allow more stuttering (two possible algorithms)", 0 },
268
    { "destut", OPT_DESTUT, nullptr, 0, "allow less stuttering", 0 },
269 270
    { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
      "remove all transitions in specified acceptance sets", 0 },
271
    { "strip-acceptance", OPT_STRIPACC, nullptr, 0,
272
      "remove the acceptance condition and all acceptance sets", 0 },
273 274
    { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
      "only keep specified states.  The first state will be the new "\
275
      "initial state.  Implies --remove-unreachable-states.", 0 },
276
    { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
277
      "put the acceptance condition in Disjunctive Normal Form", 0 },
278
    { "cnf-acceptance", OPT_CNF_ACC, nullptr, 0,
279
      "put the acceptance condition in Conjunctive Normal Form", 0 },
280
    { "remove-fin", OPT_REM_FIN, nullptr, 0,
281
      "rewrite the automaton without using Fin acceptance", 0 },
282 283 284 285 286 287 288 289 290 291 292 293 294 295
    { "generalized-rabin", OPT_GENERALIZED_RABIN,
      "unique-inf|share-inf", OPTION_ARG_OPTIONAL,
      "rewrite the acceptance condition as generalized Rabin; the default "
      "\"unique-inf\" option uses the generalized Rabin definition from the "
      "HOA format; the \"share-inf\" option allows clauses to share Inf sets, "
      "therefore reducing the number of sets", 0 },
    { "gra", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "generalized-streett", OPT_GENERALIZED_STREETT,
      "unique-fin|share-fin", OPTION_ARG_OPTIONAL,
      "rewrite the acceptance condition as generalized Streett;"
      " the \"share-fin\" option allows clauses to share Fin sets,"
      " therefore reducing the number of sets; the default"
      " \"unique-fin\" does not", 0 },
    { "gsa", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
296
    { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
297
      "remove unused acceptance sets from the automaton", 0 },
298 299 300
    { "complement", OPT_COMPLEMENT, nullptr, 0,
      "complement each automaton (currently support only deterministic "
      "automata)", 0 },
301
    { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
302 303
      "complement the acceptance condition (without touching the automaton)",
      0 },
304
    { "decompose-scc", OPT_DECOMPOSE_SCC, "t|w|s|N|aN", 0,
305
      "extract the (t) terminal, (w) weak, or (s) strong part of an automaton"
306
      " or (N) the subautomaton leading to the Nth SCC, or (aN) to the Nth "
Clément Gillard's avatar
Clément Gillard committed
307
      "accepting SCC (option can be combined with commas to extract multiple "
308 309
      "parts)", 0 },
    { "decompose-strength", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
Thomas Medioni's avatar
Thomas Medioni committed
310 311
    { "dualize", OPT_DUALIZE, nullptr, 0,
      "dualize each automaton", 0 },
312 313 314 315 316
    { "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 },
317
    { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, nullptr, 0,
318 319 320
      "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 },
321 322 323
    { "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 },
324 325
    { "remove-unused-ap", OPT_REM_UNUSED_AP, nullptr, 0,
      "remove declared atomic propositions that are not used", 0 },
326
    { "remove-unreachable-states", OPT_REM_UNREACH, nullptr, 0,
327
      "remove states that are unreachable from the initial state", 0 },
328
    { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
329 330
      "remove states that are unreachable, or that cannot belong to an "
      "infinite path", 0 },
331 332 333
    { "simplify-acceptance", OPT_SIMPL_ACC, nullptr, 0,
      "simplify the acceptance condition by merging identical acceptance sets "
      "and by simplifying some terms containing complementary sets", 0 },
334 335 336
    { "split-edges", OPT_SPLIT_EDGES, nullptr, 0,
      "split edges into transitions labeled by conjunctions of all atomic "
      "propositions, so they can be read as letters", 0 },
337 338 339 340 341 342 343
    { "sum", OPT_SUM_OR, "FILENAME", 0,
      "build the sum with the automaton in FILENAME "
      "to sum languages", 0 },
    { "sum-or", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "sum-and", OPT_SUM_AND, "FILENAME", 0,
      "build the sum with the automaton in FILENAME "
      "to intersect languages", 0 },
344
    { "separate-sets", OPT_SEP_SETS, nullptr, 0,
345 346
      "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 },
347
    { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL,
Alexandre Duret-Lutz's avatar
typos  
Alexandre Duret-Lutz committed
348
      "minimize the automaton using a SAT solver (only works for deterministic"
349 350 351 352 353 354
      " automata). Supported options are acc=STRING, states=N, max-states=N, "
      "sat-incr=N, sat-incr-steps=N, sat-langmap, sat-naive, colored, preproc=N"
      ". Spot uses by default its PicoSAT distribution but an external SAT"
      "solver can be set thanks to the SPOT_SATSOLVER environment variable"
      "(see spot-x)."
      , 0 },
355 356 357 358 359 360
    { "dca", OPT_DCA, nullptr, 0,
      "convert to deterministic co-Büchi. The resulting automaton will always "
      "recognize at least the same language. Actually, it can recognize "
      "more if the original language can not be expressed using a co-Büchi "
      "acceptance condition."
      , 0 },
361
    { nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 9 },
362 363
    { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM",
364
      0 },
365 366
    { "highlight-nondet-edges", OPT_HIGHLIGHT_NONDET_EDGES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic edges with color NUM",
367
      0 },
368 369 370
    { "highlight-nondet", OPT_HIGHLIGHT_NONDET, "NUM",
      OPTION_ARG_OPTIONAL,
      "highlight nondeterministic states and edges with color NUM", 0},
371 372
    { "highlight-word", OPT_HIGHLIGHT_WORD, "[NUM,]WORD", 0,
      "highlight one run matching WORD using color NUM", 0},
373
    { "highlight-languages", OPT_HIGHLIGHT_LANGUAGES, nullptr, 0 ,
374
      "highlight states that recognize identical languages", 0},
375
    /**************************************************/
376 377
    { nullptr, 0, nullptr, 0,
      "If any option among --small, --deterministic, or --any is given, "
378
      "then the simplification level defaults to --high unless specified "
379
      "otherwise.  If any option among --low, --medium, or --high is given, "
380
      "then the simplification goal defaults to --small unless specified "
381 382 383
      "otherwise.  If none of those options are specified, then autfilt "
      "acts as is --any --low were given: these actually disable the "
      "simplification routines.", 22 },
384
    /**************************************************/
385
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
386 387
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
388 389
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
390
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
391 392
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
393
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
394
  {
395
    { &hoaread_argp, 0, nullptr, 0 },
396 397
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
398
    { &post_argp_disabled, 0, nullptr, 0 },
399 400
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
401 402
  };

403

404
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
405
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
406
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
407 408 409 410
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
411

412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435
enum gra_type { GRA_NO = 0, GRA_SHARE_INF = 1, GRA_UNIQUE_INF = 2 };
static gra_type opt_gra = GRA_NO;
static char const *const gra_args[] =
{
  "default", "share-inf", "hoa", "unique-inf", nullptr
};
static gra_type const gra_types[] =
{
  GRA_UNIQUE_INF, GRA_SHARE_INF, GRA_UNIQUE_INF, GRA_UNIQUE_INF
};
ARGMATCH_VERIFY(gra_args, gra_types);

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

436
// We want all these variables to be destroyed when we exit main, to
437 438 439 440 441 442
// 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();
443 444
  spot::twa_graph_ptr product_and = nullptr;
  spot::twa_graph_ptr product_or = nullptr;
445 446
  spot::twa_graph_ptr sum_and = nullptr;
  spot::twa_graph_ptr sum_or = nullptr;
447
  spot::twa_graph_ptr intersect = nullptr;
448
  spot::twa_graph_ptr included_in = nullptr;
449 450
  spot::twa_graph_ptr equivalent_pos = nullptr;
  spot::twa_graph_ptr equivalent_neg = nullptr;
451
  spot::twa_graph_ptr are_isomorphic = nullptr;
452 453 454
  std::unique_ptr<spot::isomorphism_checker>
                         isomorphism_checker = nullptr;
  std::unique_ptr<unique_aut_t> uniq = nullptr;
455 456
  spot::exclusive_ap excl_ap;
  spot::remove_ap rem_ap;
457
  std::vector<spot::twa_graph_ptr> acc_words;
458
  std::vector<spot::twa_graph_ptr> rej_words;
459
  std::vector<std::pair<spot::twa_graph_ptr, unsigned>> hl_words;
460 461
}* opt;

462
static bool opt_merge = false;
463
static bool opt_is_alternating = false;
464 465
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
466
static bool opt_is_semi_deterministic = false;
467
static bool opt_is_unambiguous = false;
468 469
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
470
static bool opt_is_inherently_weak = false;
471
static bool opt_is_very_weak = false;
472
static bool opt_is_stutter_invariant = false;
473
static bool opt_invert = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
474
static range opt_states = { 0, std::numeric_limits<int>::max() };
475 476
static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() };
477
static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
478 479 480
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;
481 482 483 484 485 486 487 488 489 490 491 492
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;
493 494
static range opt_nondet_states = { 0, std::numeric_limits<int>::max() };
static bool opt_nondet_states_set = false;
495
static int opt_max_count = -1;
496
static bool opt_destut = false;
497
static char opt_instut = 0;
498
static bool opt_is_empty = false;
499
static bool opt_stripacc = false;
500
static bool opt_dnf_acc = false;
501
static bool opt_cnf_acc = false;
502
static bool opt_rem_fin = false;
503
static bool opt_clean_acc = false;
504
static bool opt_complement = false;
505
static bool opt_complement_acc = false;
506
static char* opt_decompose_scc = nullptr;
Thomas Medioni's avatar
Thomas Medioni committed
507
static bool opt_dualize = false;
508
static spot::acc_cond::mark_t opt_mask_acc = 0U;
509 510
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
511
static bool opt_simpl_acc = false;
512
static bool opt_simplify_exclusive_ap = false;
513 514
static bool opt_rem_dead = false;
static bool opt_rem_unreach = false;
515
static bool opt_rem_unused_ap = false;
516
static bool opt_sep_sets = false;
517
static bool opt_split_edges = false;
518
static const char* opt_sat_minimize = nullptr;
519 520
static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1;
521
static bool opt_highlight_languages = false;
522
static bool opt_dca = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
523

524
static spot::twa_graph_ptr
525
ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
526
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
527
  if ((!nonalt || aut->is_existential()) && spot::is_universal(aut))
528 529 530 531 532 533 534 535
    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
536 537 538 539 540 541
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
542
    case 'c':
543
      automaton_format = Count;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
544
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
545 546 547
    case 'F':
      jobs.emplace_back(arg, true);
      break;
548 549 550
    case 'n':
      opt_max_count = to_pos_int(arg);
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
551
    case 'u':
552
      opt->uniq =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
553 554
        std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
      break;
555 556 557
    case 'v':
      opt_invert = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
558 559
    case 'x':
      {
560 561 562
        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
563 564
      }
      break;
565 566 567
    case OPT_AP_N:
      opt_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
568 569 570
    case OPT_ACC_SETS:
      opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
571 572 573 574
    case OPT_ACC_SCCS:
      opt_acc_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
575
    case OPT_ACCEPT_WORD:
576
      try
577 578 579 580
        {
          opt->acc_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
581
      catch (const spot::parse_error& e)
582 583 584 585
        {
          error(2, 0, "failed to parse the argument of --accept-word:\n%s",
                e.what());
        }
586
      break;
587
    case OPT_ARE_ISOMORPHIC:
588
      opt->are_isomorphic = read_automaton(arg, opt->dict);
589
      break;
590 591 592
    case OPT_CLEAN_ACC:
      opt_clean_acc = true;
      break;
593 594 595 596
    case OPT_CNF_ACC:
      opt_dnf_acc = false;
      opt_cnf_acc = true;
      break;
597
    case OPT_COMPLEMENT:
Thomas Medioni's avatar
Thomas Medioni committed
598 599 600
      if (opt_dualize)
        error(2, 0, "either --complement or --dualize options"
                    " can be given, not both");
601 602
      opt_complement = true;
      break;
603 604 605
    case OPT_COMPLEMENT_ACC:
      opt_complement_acc = true;
      break;
606 607 608
     case OPT_DCA:
      opt_dca = true;
      break;
609
    case OPT_DECOMPOSE_SCC:
610
      opt_decompose_scc = arg;
611
      break;
612 613 614
    case OPT_DESTUT:
      opt_destut = true;
      break;
Thomas Medioni's avatar
Thomas Medioni committed
615 616 617 618 619 620
    case OPT_DUALIZE:
      if (opt_complement)
        error(2, 0, "either --complement or --dualize options"
                    " can be given, not both");
      opt_dualize = true;
      break;
621 622
    case OPT_DNF_ACC:
      opt_dnf_acc = true;
623
      opt_cnf_acc = false;
624
      break;
625 626 627
    case OPT_EDGES:
      opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
628
    case OPT_EXCLUSIVE_AP:
629
      opt->excl_ap.add_group(arg);
630
      break;
631 632
    case OPT_EQUIVALENT_TO:
      if (opt->equivalent_pos)
633
        error(2, 0, "only one --equivalent-to option can be given");
634 635
      opt->equivalent_pos = read_automaton(arg, opt->dict);
      opt->equivalent_neg =
636
        spot::dualize(ensure_deterministic(opt->equivalent_pos, true));
637
      break;
638 639 640 641 642 643 644 645 646 647 648 649 650 651
    case OPT_GENERALIZED_RABIN:
      if (arg)
        opt_gra = XARGMATCH("--generalized-rabin", arg, gra_args, gra_types);
      else
        opt_gra = GRA_UNIQUE_INF;
      opt_gsa = GSA_NO;
      break;
    case OPT_GENERALIZED_STREETT:
      if (arg)
        opt_gsa = XARGMATCH("--generalized-streett", arg, gsa_args, gsa_types);
      else
        opt_gsa = GSA_UNIQUE_FIN;
      opt_gra = GRA_NO;
      break;
652 653 654 655 656 657 658 659 660 661 662 663
    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;
664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695
    case OPT_HIGHLIGHT_WORD:
      {
        char* endptr;
        int res = strtol(arg, &endptr, 10);
        if (endptr == arg)
          {
            res = 1;
          }
        else
          {
            if (res < 0)
              error(2, 0, "failed to parse the argument of --highlight-word: "
                    "%d is not positive", res);
            while (std::isspace(*endptr))
              ++endptr;
            if (*endptr != ',')
              error(2, 0, "failed to parse the argument of --highlight-word: "
                    "%d should be followed by a comma and WORD", res);
            arg = endptr + 1;
          }
        try
          {
            opt->hl_words.emplace_back(spot::parse_word(arg, opt->dict)
                                       ->as_automaton(), res);
          }
        catch (const spot::parse_error& e)
          {
            error(2, 0, "failed to parse the argument of --highlight-word:\n%s",
                  e.what());
          }
      }
      break;
696 697 698
    case OPT_HIGHLIGHT_LANGUAGES:
      opt_highlight_languages = true;
      break;
699
    case OPT_INSTUT:
700
      if (!arg || (arg[0] == '1' && arg[1] == 0))
701
        opt_instut = 1;
702
      else if (arg[0] == '2' && arg[1] == 0)
703
        opt_instut = 2;
704
      else
705
        error(2, 0, "unknown argument for --instut: %s", arg);
706
      break;
707 708
    case OPT_INCLUDED_IN:
      {
709
        auto aut = ensure_deterministic(read_automaton(arg, opt->dict), true);
710
        aut = spot::dualize(aut);
711 712 713 714
        if (!opt->included_in)
          opt->included_in = aut;
        else
          opt->included_in = spot::product_or(opt->included_in, aut);
715 716
      }
      break;
717 718 719 720 721
    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;
722
    case OPT_INTERSECT:
723
      opt->intersect = read_automaton(arg, opt->dict);
724
      break;
725 726 727
    case OPT_IS_ALTERNATING:
      opt_is_alternating = true;
      break;
728 729 730 731 732 733
    case OPT_IS_COMPLETE:
      opt_is_complete = true;
      break;
    case OPT_IS_DETERMINISTIC:
      opt_is_deterministic = true;
      break;
734 735 736
    case OPT_IS_EMPTY:
      opt_is_empty = true;
      break;
737 738 739
    case OPT_IS_INHERENTLY_WEAK:
      opt_is_inherently_weak = true;
      break;
740 741 742
    case OPT_IS_VERY_WEAK:
      opt_is_very_weak = true;
      break;
743 744 745
    case OPT_IS_SEMI_DETERMINISTIC:
      opt_is_semi_deterministic = true;
      break;
746 747
    case OPT_IS_STUTTER_INVARIANT:
      opt_is_stutter_invariant = true;
748
      break;
749 750 751
    case OPT_IS_TERMINAL:
      opt_is_terminal = true;
      break;
752 753 754
    case OPT_IS_UNAMBIGUOUS:
      opt_is_unambiguous = true;
      break;
755 756 757
    case OPT_IS_WEAK:
      opt_is_weak = true;
      break;
758 759 760 761 762 763
    case OPT_KEEP_STATES:
      {
        std::vector<long> values = to_longs(arg);
        if (!values.empty())
          opt_keep_states_initial = values[0];
        for (auto res : values)
764 765 766 767
          {
            if (res < 0)
              error(2, 0, "state ids should be non-negative:"
                    " --mask-acc=%ld", res);
768 769 770
            // 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);
771 772 773
            opt_keep_states[res] = true;
          }
        break;
774
      }
775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796
    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;
797
    case OPT_PRODUCT_AND:
798
      {
799 800 801 802 803 804
        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));
805 806 807 808
      }
      break;
    case OPT_PRODUCT_OR:
      {
809 810 811 812 813 814
        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));
815 816
      }
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
817 818
    case OPT_RANDOMIZE:
      if (arg)
819 820 821 822 823 824 825 826 827 828 829 830 831 832
        {
          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
833
      else
834 835 836 837
        {
          randomize_tr = true;
          randomize_st = true;
        }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
838
      break;
839 840 841 842
    case OPT_REJ_SCCS:
      opt_rej_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
843 844
    case OPT_REJECT_WORD:
      try
845 846 847 848
        {
          opt->rej_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
849
      catch (const spot::parse_error& e)
850 851 852 853
        {
          error(2, 0, "failed to parse the argument of --reject-word:\n%s",
                e.what());
        }
854
      break;
855
    case OPT_REM_AP:
856
      opt->rem_ap.add_ap(arg);
857
      break;
858 859 860
    case OPT_REM_DEAD:
      opt_rem_dead = true;
      break;
861 862 863
    case OPT_REM_FIN:
      opt_rem_fin = true;
      break;
864 865 866
    case OPT_REM_UNREACH:
      opt_rem_unreach = true;
      break;
867 868 869
    case OPT_REM_UNUSED_AP:
      opt_rem_unused_ap = true;
      break;
870 871 872
    case OPT_SAT_MINIMIZE:
      opt_sat_minimize = arg ? arg : "";
      break;
873 874 875 876
    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
877 878 879
    case OPT_SEED:
      opt_seed = to_int(arg);
      break;
880 881 882
    case OPT_SEP_SETS:
      opt_sep_sets = true;
      break;
883 884 885
    case OPT_SIMPL_ACC:
      opt_simpl_acc = true;
      break;
886 887 888 889
    case OPT_SIMPLIFY_EXCLUSIVE_AP:
      opt_simplify_exclusive_ap = true;
      opt_merge = true;
      break;
890 891 892
    case OPT_SPLIT_EDGES:
      opt_split_edges = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
893 894 895
    case OPT_STATES:
      opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
896 897 898
    case OPT_STRIPACC:
      opt_stripacc = true;
      break;
899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918
    case OPT_SUM_OR:
      {
        auto a = read_automaton(arg, opt->dict);
        if (!opt->sum_or)
          opt->sum_or = std::move(a);
        else
          opt->sum_or = spot::sum(std::move(opt->sum_or),
                                  std::move(a));
      }
      break;
    case OPT_SUM_AND:
      {
        auto a = read_automaton(arg, opt->dict);
        if (!opt->sum_and)
          opt->sum_and = std::move(a);
        else
          opt->sum_and = spot::sum_and(std::move(opt->sum_and),
                                       std::move(a));
      }
      break;
919 920 921 922 923 924 925 926 927
    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;
928 929 930 931 932 933 934 935
    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;
936 937 938 939 940
    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
941 942 943 944 945 946 947 948 949 950
    case ARGP_KEY_ARG:
      jobs.emplace_back(arg, true);
      break;

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967
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
968 969 970

namespace
{
971 972

  struct autfilt_processor: hoa_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
973
  {
974
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
975
    spot::postprocessor& post;