autfilt.cc 47.2 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 50 51
#include <spot/parseaut/public.hh>
#include <spot/tl/exclusive.hh>
#include <spot/twaalgos/are_isomorphic.hh>
#include <spot/twaalgos/canonicalize.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/dtwasat.hh>
52
#include <spot/twaalgos/dualize.hh>
53
#include <spot/twaalgos/gtec/gtec.hh>
54
#include <spot/twaalgos/hoa.hh>
55 56
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/isunamb.hh>
57
#include <spot/twaalgos/isweakscc.hh>
58
#include <spot/twaalgos/langmap.hh>
59 60 61 62 63 64 65 66 67 68 69 70 71
#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
72

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

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

153 154
#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
155 156 157
static const argp_option options[] =
  {
    /**************************************************/
158
    { nullptr, 0, nullptr, 0, "Input:", 1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
159 160 161
    { "file", 'F', "FILENAME", 0,
      "process the automaton in FILENAME", 0 },
    /**************************************************/
162
    { "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
163
    { "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
164
    /**************************************************/
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183
    { 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 },
184 185
    { "is-semi-deterministic", OPT_IS_SEMI_DETERMINISTIC, nullptr, 0,
      "keep semi-deterministic automata", 0 },
186 187
    { "is-empty", OPT_IS_EMPTY, nullptr, 0,
      "keep automata with an empty language", 0 },
188 189
    { "is-stutter-invariant", OPT_IS_STUTTER_INVARIANT, nullptr, 0,
      "keep automata representing stutter-invariant properties", 0 },
190 191
    { "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
      "keep only terminal automata", 0 },
192 193
    { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
      "keep only unambiguous automata", 0 },
194 195 196 197
    { "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 },
198 199
    { "is-very-weak", OPT_IS_VERY_WEAK, nullptr, 0,
      "keep only very-weak automata", 0 },
200 201
    { "is-alternating", OPT_IS_ALTERNATING, nullptr, 0,
      "keep only automata using universal branching", 0 },
202 203 204 205 206 207 208 209 210 211 212 213 214 215
    { "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 },
216 217
    { "nondet-states", OPT_NONDET_STATES, "RANGE", 0,
      "keep automata whose number of nondeterministic states is in RANGE", 0 },
218 219 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
    { "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 },
252
    { "merge-transitions", OPT_MERGE, nullptr, 0,
253
      "merge transitions with same destination and acceptance", 0 },
254 255 256
    { "product", OPT_PRODUCT_AND, "FILENAME", 0,
      "build the product with the automaton in FILENAME "
      "to intersect languages", 0 },
257
    { "product-and", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
258 259 260
    { "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
261
    { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
262
      "randomize states and transitions (specify 's' or 't' to "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
263
      "randomize only states or transitions)", 0 },
264 265
    { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL,
      "allow more stuttering (two possible algorithms)", 0 },
266
    { "destut", OPT_DESTUT, nullptr, 0, "allow less stuttering", 0 },
267 268
    { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
      "remove all transitions in specified acceptance sets", 0 },
269
    { "strip-acceptance", OPT_STRIPACC, nullptr, 0,
270
      "remove the acceptance condition and all acceptance sets", 0 },
271 272
    { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
      "only keep specified states.  The first state will be the new "\
273
      "initial state.  Implies --remove-unreachable-states.", 0 },
274
    { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
275
      "put the acceptance condition in Disjunctive Normal Form", 0 },
276
    { "cnf-acceptance", OPT_CNF_ACC, nullptr, 0,
277
      "put the acceptance condition in Conjunctive Normal Form", 0 },
278
    { "remove-fin", OPT_REM_FIN, nullptr, 0,
279
      "rewrite the automaton without using Fin acceptance", 0 },
280 281 282 283 284 285 286 287 288 289 290 291 292 293
    { "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 },
294
    { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
295
      "remove unused acceptance sets from the automaton", 0 },
296 297 298
    { "complement", OPT_COMPLEMENT, nullptr, 0,
      "complement each automaton (currently support only deterministic "
      "automata)", 0 },
299
    { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
300 301
      "complement the acceptance condition (without touching the automaton)",
      0 },
302 303 304
    { "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 },
305 306
    { "decompose-scc", OPT_DECOMPOSE_SCC, "N", 0, "keep only the Nth accepting"
      " SCC as accepting", 0 },
Thomas Medioni's avatar
Thomas Medioni committed
307 308
    { "dualize", OPT_DUALIZE, nullptr, 0,
      "dualize each automaton", 0 },
309 310 311 312 313
    { "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 },
314
    { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, nullptr, 0,
315 316 317
      "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 },
318 319 320
    { "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 },
321 322
    { "remove-unused-ap", OPT_REM_UNUSED_AP, nullptr, 0,
      "remove declared atomic propositions that are not used", 0 },
323
    { "remove-unreachable-states", OPT_REM_UNREACH, nullptr, 0,
324
      "remove states that are unreachable from the initial state", 0 },
325
    { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
326 327
      "remove states that are unreachable, or that cannot belong to an "
      "infinite path", 0 },
328 329 330
    { "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 },
331 332 333 334 335 336 337
    { "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 },
338
    { "separate-sets", OPT_SEP_SETS, nullptr, 0,
339 340
      "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 },
341
    { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL,
Alexandre Duret-Lutz's avatar
typos  
Alexandre Duret-Lutz committed
342
      "minimize the automaton using a SAT solver (only works for deterministic"
343 344 345 346 347 348 349
      " 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 },
    { nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 9 },
350 351
    { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM",
352
      0 },
353 354
    { "highlight-nondet-edges", OPT_HIGHLIGHT_NONDET_EDGES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic edges with color NUM",
355
      0 },
356 357 358
    { "highlight-nondet", OPT_HIGHLIGHT_NONDET, "NUM",
      OPTION_ARG_OPTIONAL,
      "highlight nondeterministic states and edges with color NUM", 0},
359 360
    { "highlight-word", OPT_HIGHLIGHT_WORD, "[NUM,]WORD", 0,
      "highlight one run matching WORD using color NUM", 0},
361
    { "highlight-languages", OPT_HIGHLIGHT_LANGUAGES, nullptr, 0 ,
362
      "highlight states that recognize identical languages", 0},
363
    /**************************************************/
364 365
    { nullptr, 0, nullptr, 0,
      "If any option among --small, --deterministic, or --any is given, "
366
      "then the simplification level defaults to --high unless specified "
367
      "otherwise.  If any option among --low, --medium, or --high is given, "
368
      "then the simplification goal defaults to --small unless specified "
369 370 371
      "otherwise.  If none of those options are specified, then autfilt "
      "acts as is --any --low were given: these actually disable the "
      "simplification routines.", 22 },
372
    /**************************************************/
373
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
374 375
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
376 377
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
378
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
379 380
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
381
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
382
  {
383
    { &hoaread_argp, 0, nullptr, 0 },
384 385
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
386
    { &post_argp_disabled, 0, nullptr, 0 },
387 388
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
389 390
  };

391

392
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
393
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
394
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
395 396 397 398
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
399

400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423
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);

424
// We want all these variables to be destroyed when we exit main, to
425 426 427 428 429 430
// 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();
431 432
  spot::twa_graph_ptr product_and = nullptr;
  spot::twa_graph_ptr product_or = nullptr;
433 434
  spot::twa_graph_ptr sum_and = nullptr;
  spot::twa_graph_ptr sum_or = nullptr;
435
  spot::twa_graph_ptr intersect = nullptr;
436
  spot::twa_graph_ptr included_in = nullptr;
437 438
  spot::twa_graph_ptr equivalent_pos = nullptr;
  spot::twa_graph_ptr equivalent_neg = nullptr;
439
  spot::twa_graph_ptr are_isomorphic = nullptr;
440 441 442
  std::unique_ptr<spot::isomorphism_checker>
                         isomorphism_checker = nullptr;
  std::unique_ptr<unique_aut_t> uniq = nullptr;
443 444
  spot::exclusive_ap excl_ap;
  spot::remove_ap rem_ap;
445
  std::vector<spot::twa_graph_ptr> acc_words;
446
  std::vector<spot::twa_graph_ptr> rej_words;
447
  std::vector<std::pair<spot::twa_graph_ptr, unsigned>> hl_words;
448 449
}* opt;

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

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