1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2013-2021 Laboratoire de Recherche et Développement
3 // de l'Epita (LRDE).
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20 #include "common_sys.hh"
21
22 #include <string>
23 #include <iostream>
24 #include <limits>
25 #include <set>
26 #include <memory>
27 #include <sys/stat.h>
28 #include <unistd.h>
29
30 #include <argp.h>
31 #include "error.h"
32 #include "argmatch.h"
33
34 #include "common_setup.hh"
35 #include "common_finput.hh"
36 #include "common_cout.hh"
37 #include "common_aoutput.hh"
38 #include "common_range.hh"
39 #include "common_post.hh"
40 #include "common_conv.hh"
41 #include "common_hoaread.hh"
42
43 #include <spot/misc/optionmap.hh>
44 #include <spot/misc/random.hh>
45 #include <spot/misc/timer.hh>
46 #include <spot/parseaut/public.hh>
47 #include <spot/tl/exclusive.hh>
48 #include <spot/twaalgos/are_isomorphic.hh>
49 #include <spot/twaalgos/canonicalize.hh>
50 #include <spot/twaalgos/cobuchi.hh>
51 #include <spot/twaalgos/cleanacc.hh>
52 #include <spot/twaalgos/complement.hh>
53 #include <spot/twaalgos/contains.hh>
54 #include <spot/twaalgos/degen.hh>
55 #include <spot/twaalgos/dtwasat.hh>
56 #include <spot/twaalgos/dualize.hh>
57 #include <spot/twaalgos/gtec/gtec.hh>
58 #include <spot/twaalgos/hoa.hh>
59 #include <spot/twaalgos/iscolored.hh>
60 #include <spot/twaalgos/isdet.hh>
61 #include <spot/twaalgos/isunamb.hh>
62 #include <spot/twaalgos/isweakscc.hh>
63 #include <spot/twaalgos/langmap.hh>
64 #include <spot/twaalgos/mask.hh>
65 #include <spot/twaalgos/product.hh>
66 #include <spot/twaalgos/randomize.hh>
67 #include <spot/twaalgos/remfin.hh>
68 #include <spot/twaalgos/remprop.hh>
69 #include <spot/twaalgos/sccinfo.hh>
70 #include <spot/twaalgos/sepsets.hh>
71 #include <spot/twaalgos/split.hh>
72 #include <spot/twaalgos/strength.hh>
73 #include <spot/twaalgos/stripacc.hh>
74 #include <spot/twaalgos/stutter.hh>
75 #include <spot/twaalgos/sum.hh>
76 #include <spot/twaalgos/totgba.hh>
77
78 static const char argp_program_doc[] ="\
79 Convert, transform, and filter omega-automata.\v\
80 Exit status:\n\
81 0 if some automata were output\n\
82 1 if no automata were output (no match)\n\
83 2 if any error has been reported";
84
85 // Keep this list sorted
86 enum {
87 OPT_ACC_SCCS = 256,
88 OPT_ACC_SETS,
89 OPT_ACCEPT_WORD,
90 OPT_ACCEPTANCE_IS,
91 OPT_AP_N,
92 OPT_ARE_ISOMORPHIC,
93 OPT_CLEAN_ACC,
94 OPT_CNF_ACC,
95 OPT_COMPLEMENT,
96 OPT_COMPLEMENT_ACC,
97 OPT_COUNT,
98 OPT_DCA,
99 OPT_DECOMPOSE_SCC,
100 OPT_DESTUT,
101 OPT_DUALIZE,
102 OPT_DNF_ACC,
103 OPT_EDGES,
104 OPT_EQUIVALENT_TO,
105 OPT_EXCLUSIVE_AP,
106 OPT_GENERALIZED_RABIN,
107 OPT_GENERALIZED_STREETT,
108 OPT_HAS_EXIST_BRANCHING,
109 OPT_HAS_UNIV_BRANCHING,
110 OPT_HIGHLIGHT_NONDET,
111 OPT_HIGHLIGHT_NONDET_EDGES,
112 OPT_HIGHLIGHT_NONDET_STATES,
113 OPT_HIGHLIGHT_WORD,
114 OPT_HIGHLIGHT_ACCEPTING_RUN,
115 OPT_HIGHLIGHT_LANGUAGES,
116 OPT_INSTUT,
117 OPT_INCLUDED_IN,
118 OPT_INHERENTLY_WEAK_SCCS,
119 OPT_INTERSECT,
120 OPT_IS_ALTERNATING,
121 OPT_IS_COLORED,
122 OPT_IS_COMPLETE,
123 OPT_IS_DETERMINISTIC,
124 OPT_IS_EMPTY,
125 OPT_IS_INHERENTLY_WEAK,
126 OPT_IS_SEMI_DETERMINISTIC,
127 OPT_IS_STUTTER_INVARIANT,
128 OPT_IS_TERMINAL,
129 OPT_IS_UNAMBIGUOUS,
130 OPT_IS_VERY_WEAK,
131 OPT_IS_WEAK,
132 OPT_KEEP_STATES,
133 OPT_KILL_STATES,
134 OPT_MASK_ACC,
135 OPT_MERGE,
136 OPT_NONDET_STATES,
137 OPT_PARTIAL_DEGEN,
138 OPT_PRODUCT_AND,
139 OPT_PRODUCT_OR,
140 OPT_RANDOMIZE,
141 OPT_REJ_SCCS,
142 OPT_REJECT_WORD,
143 OPT_REM_AP,
144 OPT_REM_DEAD,
145 OPT_REM_UNREACH,
146 OPT_REM_UNUSED_AP,
147 OPT_REM_FIN,
148 OPT_SAT_MINIMIZE,
149 OPT_SCCS,
150 OPT_SEED,
151 OPT_SEP_SETS,
152 OPT_SIMPL_ACC,
153 OPT_SIMPLIFY_EXCLUSIVE_AP,
154 OPT_SPLIT_EDGES,
155 OPT_STATES,
156 OPT_STREETT_LIKE,
157 OPT_STRIPACC,
158 OPT_SUM_OR,
159 OPT_SUM_AND,
160 OPT_TERMINAL_SCCS,
161 OPT_TRIV_SCCS,
162 OPT_USED_AP_N,
163 OPT_UNUSED_AP_N,
164 OPT_WEAK_SCCS,
165 };
166
167 #define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0
168
169 static const argp_option options[] =
170 {
171 /**************************************************/
172 { nullptr, 0, nullptr, 0, "Input:", 1 },
173 { "file", 'F', "FILENAME", 0,
174 "process the automaton in FILENAME", 0 },
175 /**************************************************/
176 { "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
177 { "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
178 /**************************************************/
179 { nullptr, 0, nullptr, 0, "Filtering options:", 5 },
180 { "ap", OPT_AP_N, "RANGE", 0,
181 "match automata with a number of (declared) atomic propositions in RANGE",
182 0 },
183 { "used-ap", OPT_USED_AP_N, "RANGE", 0,
184 "match automata with a number of used atomic propositions in RANGE", 0 },
185 { "unused-ap", OPT_UNUSED_AP_N, "RANGE", 0,
186 "match automata with a number of declared, but unused atomic "
187 "propositions in RANGE", 0 },
188 { "acceptance-is", OPT_ACCEPTANCE_IS, "NAME|FORMULA", 0,
189 "match automata with given acceptance condition", 0 },
190 { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
191 "keep automata that are isomorphic to the automaton in FILENAME", 0 },
192 { "isomorphic", 0, nullptr, OPTION_ALIAS | OPTION_HIDDEN, nullptr, 0 },
193 { "unique", 'u', nullptr, 0,
194 "do not output the same automaton twice (same in the sense that they "
195 "are isomorphic)", 0 },
196 { "has-exist-branching", OPT_HAS_EXIST_BRANCHING, nullptr, 0,
197 "keep automata that use existential branching (i.e., make "
198 "non-deterministic choices)", 0 },
199 { "has-univ-branching", OPT_HAS_UNIV_BRANCHING, nullptr, 0,
200 "keep alternating automata that use universal branching", 0 },
201 { "is-colored", OPT_IS_COLORED, nullptr, 0,
202 "keep colored automata (i.e., exactly one acceptance mark per "
203 "transition or state)", 0 },
204 { "is-complete", OPT_IS_COMPLETE, nullptr, 0,
205 "keep complete automata", 0 },
206 { "is-deterministic", OPT_IS_DETERMINISTIC, nullptr, 0,
207 "keep deterministic automata", 0 },
208 { "is-semi-deterministic", OPT_IS_SEMI_DETERMINISTIC, nullptr, 0,
209 "keep semi-deterministic automata", 0 },
210 { "is-empty", OPT_IS_EMPTY, nullptr, 0,
211 "keep automata with an empty language", 0 },
212 { "is-stutter-invariant", OPT_IS_STUTTER_INVARIANT, nullptr, 0,
213 "keep automata representing stutter-invariant properties", 0 },
214 { "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
215 "keep only terminal automata", 0 },
216 { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
217 "keep only unambiguous automata", 0 },
218 { "is-weak", OPT_IS_WEAK, nullptr, 0,
219 "keep only weak automata", 0 },
220 { "is-inherently-weak", OPT_IS_INHERENTLY_WEAK, nullptr, 0,
221 "keep only inherently weak automata", 0 },
222 { "is-very-weak", OPT_IS_VERY_WEAK, nullptr, 0,
223 "keep only very-weak automata", 0 },
224 { "is-alternating", OPT_IS_ALTERNATING, nullptr, 0,
225 "keep only automata using universal branching", 0 },
226 { "intersect", OPT_INTERSECT, "FILENAME", 0,
227 "keep automata whose languages have an non-empty intersection with"
228 " the automaton from FILENAME", 0 },
229 { "included-in", OPT_INCLUDED_IN, "FILENAME", 0,
230 "keep automata whose languages are included in that of the "
231 "automaton from FILENAME", 0 },
232 { "equivalent-to", OPT_EQUIVALENT_TO, "FILENAME", 0,
233 "keep automata that are equivalent (language-wise) to the automaton "
234 "in FILENAME", 0 },
235 { "invert-match", 'v', nullptr, 0, "select non-matching automata", 0 },
236 { "states", OPT_STATES, "RANGE", 0,
237 "keep automata whose number of states is in RANGE", 0 },
238 { "edges", OPT_EDGES, "RANGE", 0,
239 "keep automata whose number of edges is in RANGE", 0 },
240 { "nondet-states", OPT_NONDET_STATES, "RANGE", 0,
241 "keep automata whose number of nondeterministic states is in RANGE", 0 },
242 { "acc-sets", OPT_ACC_SETS, "RANGE", 0,
243 "keep automata whose number of acceptance sets is in RANGE", 0 },
244 { "sccs", OPT_SCCS, "RANGE", 0,
245 "keep automata whose number of SCCs is in RANGE", 0 },
246 { "acc-sccs", OPT_ACC_SCCS, "RANGE", 0,
247 "keep automata whose number of non-trivial accepting SCCs is in RANGE",
248 0 },
249 { "accepting-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
250 { "rej-sccs", OPT_REJ_SCCS, "RANGE", 0,
251 "keep automata whose number of non-trivial rejecting SCCs is in RANGE",
252 0 },
253 { "rejecting-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
254 { "triv-sccs", OPT_TRIV_SCCS, "RANGE", 0,
255 "keep automata whose number of trivial SCCs is in RANGE", 0 },
256 { "trivial-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
257 { "inherently-weak-sccs", OPT_INHERENTLY_WEAK_SCCS, "RANGE", 0,
258 "keep automata whose number of accepting inherently-weak SCCs is in "
259 "RANGE. An accepting SCC is inherently weak if it does not have a "
260 "rejecting cycle.", 0 },
261 { "weak-sccs", OPT_WEAK_SCCS, "RANGE", 0,
262 "keep automata whose number of accepting weak SCCs is in RANGE. "
263 "In a weak SCC, all transitions belong to the same acceptance sets.", 0 },
264 { "terminal-sccs", OPT_TERMINAL_SCCS, "RANGE", 0,
265 "keep automata whose number of accepting terminal SCCs is in RANGE. "
266 "Terminal SCCs are weak and complete.", 0 },
267 { "accept-word", OPT_ACCEPT_WORD, "WORD", 0,
268 "keep automata that accept WORD", 0 },
269 { "reject-word", OPT_REJECT_WORD, "WORD", 0,
270 "keep automata that reject WORD", 0 },
271 { "nth", 'N', "RANGE", 0,
272 "assuming input automata are numbered from 1, keep only those in RANGE",
273 0 },
274 /**************************************************/
275 RANGE_DOC_FULL,
276 WORD_DOC,
277 /**************************************************/
278 { nullptr, 0, nullptr, 0, "Transformations:", 7 },
279 { "merge-transitions", OPT_MERGE, nullptr, 0,
280 "merge transitions with same destination and acceptance", 0 },
281 { "product", OPT_PRODUCT_AND, "FILENAME", 0,
282 "build the product with the automaton in FILENAME "
283 "to intersect languages", 0 },
284 { "product-and", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
285 { "product-or", OPT_PRODUCT_OR, "FILENAME", 0,
286 "build the product with the automaton in FILENAME "
287 "to sum languages", 0 },
288 { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
289 "randomize states and transitions (specify 's' or 't' to "
290 "randomize only states or transitions)", 0 },
291 { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL,
292 "allow more stuttering (two possible algorithms)", 0 },
293 { "destut", OPT_DESTUT, nullptr, 0, "allow less stuttering", 0 },
294 { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
295 "remove all transitions in specified acceptance sets", 0 },
296 { "strip-acceptance", OPT_STRIPACC, nullptr, 0,
297 "remove the acceptance condition and all acceptance sets", 0 },
298 { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
299 "only keep specified states. The first state will be the new "\
300 "initial state. Implies --remove-unreachable-states.", 0 },
301 { "kill-states", OPT_KILL_STATES, "NUM[,NUM...]", 0,
302 "mark the specified states as dead (no successor), and remove"
303 " them. Implies --remove-dead-states.", 0 },
304 { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
305 "put the acceptance condition in Disjunctive Normal Form", 0 },
306 { "streett-like", OPT_STREETT_LIKE, nullptr, 0,
307 "convert to an automaton with Streett-like acceptance. Works only with "
308 "acceptance condition in DNF", 0 },
309 { "cnf-acceptance", OPT_CNF_ACC, nullptr, 0,
310 "put the acceptance condition in Conjunctive Normal Form", 0 },
311 { "remove-fin", OPT_REM_FIN, nullptr, 0,
312 "rewrite the automaton without using Fin acceptance", 0 },
313 { "generalized-rabin", OPT_GENERALIZED_RABIN,
314 "unique-inf|share-inf", OPTION_ARG_OPTIONAL,
315 "rewrite the acceptance condition as generalized Rabin; the default "
316 "\"unique-inf\" option uses the generalized Rabin definition from the "
317 "HOA format; the \"share-inf\" option allows clauses to share Inf sets, "
318 "therefore reducing the number of sets", 0 },
319 { "gra", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
320 { "generalized-streett", OPT_GENERALIZED_STREETT,
321 "unique-fin|share-fin", OPTION_ARG_OPTIONAL,
322 "rewrite the acceptance condition as generalized Streett;"
323 " the \"share-fin\" option allows clauses to share Fin sets,"
324 " therefore reducing the number of sets; the default"
325 " \"unique-fin\" does not", 0 },
326 { "gsa", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
327 { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
328 "remove unused acceptance sets from the automaton", 0 },
329 { "complement", OPT_COMPLEMENT, nullptr, 0,
330 "complement each automaton (different strategies are used)", 0 },
331 { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
332 "complement the acceptance condition (without touching the automaton)",
333 0 },
334 { "decompose-scc", OPT_DECOMPOSE_SCC, "t|w|s|N|aN", 0,
335 "extract the (t) terminal, (w) weak, or (s) strong part of an automaton"
336 " or (N) the subautomaton leading to the Nth SCC, or (aN) to the Nth "
337 "accepting SCC (option can be combined with commas to extract multiple "
338 "parts)", 0 },
339 { "decompose-strength", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
340 { "dualize", OPT_DUALIZE, nullptr, 0,
341 "dualize each automaton", 0 },
342 { "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0,
343 "if any of those APs occur in the automaton, restrict all edges to "
344 "ensure two of them may not be true at the same time. Use this option "
345 "multiple times to declare independent groups of exclusive "
346 "propositions.", 0 },
347 { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, nullptr, 0,
348 "if --exclusive-ap is used, assume those AP groups are actually exclusive"
349 " in the system to simplify the expression of transition labels (implies "
350 "--merge-transitions)", 0 },
351 { "remove-ap", OPT_REM_AP, "AP[=0|=1][,AP...]", 0,
352 "remove atomic propositions either by existential quantification, or "
353 "by assigning them 0 or 1", 0 },
354 { "remove-unused-ap", OPT_REM_UNUSED_AP, nullptr, 0,
355 "remove declared atomic propositions that are not used", 0 },
356 { "remove-unreachable-states", OPT_REM_UNREACH, nullptr, 0,
357 "remove states that are unreachable from the initial state", 0 },
358 { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
359 "remove states that are unreachable, or that cannot belong to an "
360 "infinite path", 0 },
361 { "simplify-acceptance", OPT_SIMPL_ACC, nullptr, 0,
362 "simplify the acceptance condition by merging identical acceptance sets "
363 "and by simplifying some terms containing complementary sets", 0 },
364 { "split-edges", OPT_SPLIT_EDGES, nullptr, 0,
365 "split edges into transitions labeled by conjunctions of all atomic "
366 "propositions, so they can be read as letters", 0 },
367 { "sum", OPT_SUM_OR, "FILENAME", 0,
368 "build the sum with the automaton in FILENAME "
369 "to sum languages", 0 },
370 { "sum-or", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
371 { "sum-and", OPT_SUM_AND, "FILENAME", 0,
372 "build the sum with the automaton in FILENAME "
373 "to intersect languages", 0 },
374 { "partial-degeneralize", OPT_PARTIAL_DEGEN, "NUM1,NUM2,...",
375 OPTION_ARG_OPTIONAL, "Degeneralize automata according to sets "
376 "NUM1,NUM2,... If no sets are given, partial degeneralization "
377 "is performed for all conjunctions of Inf and disjunctions of Fin.", 0 },
378 { "separate-sets", OPT_SEP_SETS, nullptr, 0,
379 "if both Inf(x) and Fin(x) appear in the acceptance condition, replace "
380 "Fin(x) by a new Fin(y) and adjust the automaton", 0 },
381 { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL,
382 "minimize the automaton using a SAT solver (only works for deterministic"
383 " automata). Supported options are acc=STRING, states=N, max-states=N, "
384 "sat-incr=N, sat-incr-steps=N, sat-langmap, sat-naive, colored, preproc=N"
385 ". Spot uses by default its PicoSAT distribution but an external SAT"
386 "solver can be set thanks to the SPOT_SATSOLVER environment variable"
387 "(see spot-x)."
388 , 0 },
389 { nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 9 },
390 { "highlight-accepting-run", OPT_HIGHLIGHT_ACCEPTING_RUN, "NUM",
391 OPTION_ARG_OPTIONAL, "highlight one accepting run using color NUM", 0},
392 { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM",
393 OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM",
394 0 },
395 { "highlight-nondet-edges", OPT_HIGHLIGHT_NONDET_EDGES, "NUM",
396 OPTION_ARG_OPTIONAL, "highlight nondeterministic edges with color NUM",
397 0 },
398 { "highlight-nondet", OPT_HIGHLIGHT_NONDET, "NUM",
399 OPTION_ARG_OPTIONAL,
400 "highlight nondeterministic states and edges with color NUM", 0},
401 { "highlight-word", OPT_HIGHLIGHT_WORD, "[NUM,]WORD", 0,
402 "highlight one run matching WORD using color NUM", 0},
403 { "highlight-languages", OPT_HIGHLIGHT_LANGUAGES, nullptr, 0 ,
404 "highlight states that recognize identical languages", 0},
405 /**************************************************/
406 { nullptr, 0, nullptr, 0,
407 "If any option among --small, --deterministic, or --any is given, "
408 "then the simplification level defaults to --high unless specified "
409 "otherwise. If any option among --low, --medium, or --high is given, "
410 "then the simplification goal defaults to --small unless specified "
411 "otherwise. If none of those options are specified, then autfilt "
412 "acts as is --any --low were given: these actually disable the "
413 "simplification routines.", 22 },
414 /**************************************************/
415 { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
416 { "extra-options", 'x', "OPTS", 0,
417 "fine-tuning options (see spot-x (7))", 0 },
418 { "seed", OPT_SEED, "INT", 0,
419 "seed for the random number generator (0)", 0 },
420 { nullptr, 0, nullptr, 0, nullptr, 0 }
421 };
422
423 static const struct argp_child children[] =
424 {
425 { &hoaread_argp, 0, nullptr, 0 },
426 { &aoutput_argp, 0, nullptr, 0 },
427 { &aoutput_io_format_argp, 0, nullptr, 4 },
428 { &post_argp_disabled, 0, nullptr, 0 },
429 { &misc_argp, 0, nullptr, -1 },
430 { nullptr, 0, nullptr, 0 }
431 };
432
433
434 struct canon_aut
435 {
436 typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
437 unsigned num_states;
438 std::vector<tr_t> edges;
439 std::string acc;
440
canon_autcanon_aut441 canon_aut(const spot::const_twa_graph_ptr& aut)
442 : num_states(aut->num_states())
443 , edges(aut->edge_vector().begin() + 1,
444 aut->edge_vector().end())
445 {
446 std::ostringstream os;
447 aut->get_acceptance().to_text(os);
448 acc = os.str();
449 }
450
operator <canon_aut451 bool operator<(const canon_aut& o) const
452 {
453 return std::tie(num_states, edges, acc)
454 < std::tie(o.num_states, o.edges, o.acc);
455 };
456 };
457
458 typedef std::set<canon_aut> unique_aut_t;
459 static long int match_count = 0;
460 static spot::option_map extra_options;
461 static bool randomize_st = false;
462 static bool randomize_tr = false;
463 static int opt_seed = 0;
464
465 enum gra_type { GRA_NO = 0, GRA_SHARE_INF = 1, GRA_UNIQUE_INF = 2 };
466 static gra_type opt_gra = GRA_NO;
467 static char const *const gra_args[] =
468 {
469 "default", "share-inf", "hoa", "unique-inf", nullptr
470 };
471 static gra_type const gra_types[] =
472 {
473 GRA_UNIQUE_INF, GRA_SHARE_INF, GRA_UNIQUE_INF, GRA_UNIQUE_INF
474 };
475 ARGMATCH_VERIFY(gra_args, gra_types);
476
477 enum acc_type {
478 ACC_Any = 0,
479 ACC_Given,
480 ACC_tt,
481 ACC_ff,
482 ACC_Buchi,
483 ACC_GenBuchi,
484 ACC_CoBuchi,
485 ACC_GenCoBuchi,
486 ACC_Rabin,
487 ACC_Streett,
488 ACC_GenRabin,
489 ACC_GenStreett,
490 ACC_RabinLike,
491 ACC_StreettLike,
492 ACC_Parity,
493 ACC_ParityMin,
494 ACC_ParityMax,
495 ACC_ParityOdd,
496 ACC_ParityEven,
497 ACC_ParityMinOdd,
498 ACC_ParityMaxOdd,
499 ACC_ParityMinEven,
500 ACC_ParityMaxEven,
501 ACC_FinLess,
502 };
503 static acc_type opt_acceptance_is = ACC_Any;
504 spot::acc_cond opt_acceptance_is_given;
505 static char const *const acc_is_args[] =
506 {
507 "any",
508 "t", "all",
509 "f", "none",
510 "Buchi", "Büchi",
511 "generalized-Buchi", "generalized-Büchi",
512 "genBuchi", "genBüchi", "gen-Buchi", "gen-Büchi",
513 "coBuchi", "coBüchi", "co-Buchi", "co-Büchi",
514 "generalized-coBuchi", "generalized-coBüchi",
515 "generalized-co-Buchi", "generalized-co-Büchi",
516 "gen-coBuchi", "gen-coBüchi",
517 "gen-co-Buchi", "gen-co-Büchi",
518 "gencoBuchi", "gencoBüchi",
519 "Rabin",
520 "Streett",
521 "generalized-Rabin", "gen-Rabin", "genRabin",
522 "generalized-Streett", "gen-Streett", "genStreett",
523 "Streett-like",
524 "Rabin-like",
525 "parity",
526 "parity min", "parity-min",
527 "parity max", "parity-max",
528 "parity odd", "parity-odd",
529 "parity even", "parity-even",
530 "parity min even", "parity-min-even",
531 "parity min odd", "parity-min-odd",
532 "parity max even", "parity-max-even",
533 "parity max odd", "parity-max-odd",
534 "Fin-less", "Finless",
535 nullptr,
536 };
537 static acc_type const acc_is_types[] =
538 {
539 ACC_Any,
540 ACC_tt, ACC_tt,
541 ACC_ff, ACC_ff,
542 ACC_Buchi, ACC_Buchi,
543 ACC_GenBuchi, ACC_GenBuchi,
544 ACC_GenBuchi, ACC_GenBuchi, ACC_GenBuchi, ACC_GenBuchi,
545 ACC_CoBuchi, ACC_CoBuchi, ACC_CoBuchi, ACC_CoBuchi,
546 ACC_GenCoBuchi, ACC_GenCoBuchi,
547 ACC_GenCoBuchi, ACC_GenCoBuchi,
548 ACC_GenCoBuchi, ACC_GenCoBuchi,
549 ACC_GenCoBuchi, ACC_GenCoBuchi,
550 ACC_GenCoBuchi, ACC_GenCoBuchi,
551 ACC_Rabin,
552 ACC_Streett,
553 ACC_GenRabin, ACC_GenRabin, ACC_GenRabin,
554 ACC_GenStreett, ACC_GenStreett, ACC_GenStreett,
555 ACC_StreettLike,
556 ACC_RabinLike,
557 ACC_Parity,
558 ACC_ParityMin, ACC_ParityMin,
559 ACC_ParityMax, ACC_ParityMax,
560 ACC_ParityOdd, ACC_ParityOdd,
561 ACC_ParityEven, ACC_ParityEven,
562 ACC_ParityMinEven, ACC_ParityMinEven,
563 ACC_ParityMinOdd, ACC_ParityMinOdd,
564 ACC_ParityMaxEven, ACC_ParityMaxEven,
565 ACC_ParityMaxOdd, ACC_ParityMaxOdd,
566 ACC_FinLess, ACC_FinLess,
567 };
568 ARGMATCH_VERIFY(acc_is_args, acc_is_types);
569
570 enum gsa_type { GSA_NO = 0, GSA_SHARE_FIN = 1, GSA_UNIQUE_FIN = 2 };
571 static gsa_type opt_gsa = GSA_NO;
572 static char const *const gsa_args[] =
573 {
574 "default", "share-fin", "unique-fin", nullptr
575 };
576 static gsa_type const gsa_types[] =
577 {
578 GSA_UNIQUE_FIN, GSA_SHARE_FIN, GSA_UNIQUE_FIN
579 };
580 ARGMATCH_VERIFY(gsa_args, gsa_types);
581
582 // We want all these variables to be destroyed when we exit main, to
583 // make sure it happens before all other global variables (like the
584 // atomic propositions maps) are destroyed. Otherwise we risk
585 // accessing deleted stuff.
586 static struct opt_t
587 {
588 spot::bdd_dict_ptr dict = spot::make_bdd_dict();
589 spot::twa_graph_ptr product_and = nullptr;
590 spot::twa_graph_ptr product_or = nullptr;
591 spot::twa_graph_ptr sum_and = nullptr;
592 spot::twa_graph_ptr sum_or = nullptr;
593 spot::twa_graph_ptr intersect = nullptr;
594 spot::twa_graph_ptr included_in = nullptr;
595 spot::twa_graph_ptr equivalent_pos = nullptr;
596 spot::twa_graph_ptr equivalent_neg = nullptr;
597 spot::twa_graph_ptr are_isomorphic = nullptr;
598 std::unique_ptr<spot::isomorphism_checker>
599 isomorphism_checker = nullptr;
600 std::unique_ptr<unique_aut_t> uniq = nullptr;
601 spot::exclusive_ap excl_ap;
602 spot::remove_ap rem_ap;
603 std::vector<spot::twa_graph_ptr> acc_words;
604 std::vector<spot::twa_graph_ptr> rej_words;
605 std::vector<std::pair<spot::twa_graph_ptr, unsigned>> hl_words;
606 }* opt;
607
608 static bool opt_merge = false;
609 static bool opt_has_univ_branching = false;
610 static bool opt_has_exist_branching = false;
611 static bool opt_is_alternating = false;
612 static bool opt_is_colored = false;
613 static bool opt_is_complete = false;
614 static bool opt_is_deterministic = false;
615 static bool opt_is_semi_deterministic = false;
616 static bool opt_is_unambiguous = false;
617 static bool opt_is_terminal = false;
618 static bool opt_is_weak = false;
619 static bool opt_is_inherently_weak = false;
620 static bool opt_is_very_weak = false;
621 static bool opt_is_stutter_invariant = false;
622 static bool opt_invert = false;
623 static range opt_states = { 0, std::numeric_limits<int>::max() };
624 static range opt_edges = { 0, std::numeric_limits<int>::max() };
625 static range opt_accsets = { 0, std::numeric_limits<int>::max() };
626 static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
627 static range opt_used_ap_n = { 0, std::numeric_limits<int>::max() };
628 static range opt_unused_ap_n = { 0, std::numeric_limits<int>::max() };
629 static bool need_unused_ap_count = false;
630 static range opt_sccs = { 0, std::numeric_limits<int>::max() };
631 static range opt_acc_sccs = { 0, std::numeric_limits<int>::max() };
632 static range opt_rej_sccs = { 0, std::numeric_limits<int>::max() };
633 static range opt_triv_sccs = { 0, std::numeric_limits<int>::max() };
634 static bool opt_sccs_set = false;
635 static bool opt_art_sccs_set = false; // need to classify SCCs as Acc/Rej/Triv.
636 static range opt_inhweak_sccs = { 0, std::numeric_limits<int>::max() };
637 static bool opt_inhweak_sccs_set = false;
638 static range opt_weak_sccs = { 0, std::numeric_limits<int>::max() };
639 static bool opt_weak_sccs_set = false;
640 static range opt_terminal_sccs = { 0, std::numeric_limits<int>::max() };
641 static bool opt_terminal_sccs_set = false;
642 static range opt_nondet_states = { 0, std::numeric_limits<int>::max() };
643 static bool opt_nondet_states_set = false;
644 static int opt_max_count = -1;
645 static range opt_nth = { 0, std::numeric_limits<int>::max() };
646 static bool opt_destut = false;
647 static char opt_instut = 0;
648 static bool opt_is_empty = false;
649 static bool opt_stripacc = false;
650 static bool opt_dnf_acc = false;
651 static bool opt_cnf_acc = false;
652 static bool opt_rem_fin = false;
653 static bool opt_clean_acc = false;
654 static bool opt_complement = false;
655 static bool opt_complement_acc = false;
656 static char* opt_decompose_scc = nullptr;
657 static bool opt_dualize = false;
658 static bool opt_partial_degen_set = false;
659 static spot::acc_cond::mark_t opt_partial_degen = {};
660 static spot::acc_cond::mark_t opt_mask_acc = {};
661 static std::vector<bool> opt_keep_states = {};
662 static unsigned int opt_keep_states_initial = 0;
663 static std::vector<unsigned> opt_kill_states = {};
664 static bool opt_simpl_acc = false;
665 static bool opt_simplify_exclusive_ap = false;
666 static bool opt_rem_dead = false;
667 static bool opt_rem_unreach = false;
668 static bool opt_rem_unused_ap = false;
669 static bool opt_sep_sets = false;
670 static bool opt_split_edges = false;
671 static const char* opt_sat_minimize = nullptr;
672 static int opt_highlight_nondet_states = -1;
673 static int opt_highlight_nondet_edges = -1;
674 static int opt_highlight_accepting_run = -1;
675 static bool opt_highlight_languages = false;
676 static bool opt_dca = false;
677 static bool opt_streett_like = false;
678
679 static spot::twa_graph_ptr
ensure_deterministic(const spot::twa_graph_ptr & aut,bool nonalt=false)680 ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
681 {
682 if ((!nonalt || aut->is_existential()) && spot::is_universal(aut))
683 return aut;
684 spot::postprocessor p;
685 p.set_type(spot::postprocessor::Generic);
686 p.set_pref(spot::postprocessor::Deterministic);
687 p.set_level(level);
688 return p.run(aut);
689 }
690
ensure_tba(spot::twa_graph_ptr aut)691 static spot::twa_graph_ptr ensure_tba(spot::twa_graph_ptr aut)
692 {
693 spot::postprocessor p;
694 p.set_type(spot::postprocessor::Buchi);
695 p.set_pref(spot::postprocessor::Any);
696 p.set_level(spot::postprocessor::Low);
697 return p.run(aut);
698
699 }
700
701 static spot::twa_graph_ptr
product(spot::twa_graph_ptr left,spot::twa_graph_ptr right)702 product(spot::twa_graph_ptr left, spot::twa_graph_ptr right)
703 {
704 if ((type == spot::postprocessor::Buchi)
705 && (left->num_sets() + right->num_sets() >
706 spot::acc_cond::mark_t::max_accsets()))
707 {
708 left = ensure_tba(left);
709 right = ensure_tba(right);
710 }
711 return spot::product(left, right);
712 }
713
714 static spot::twa_graph_ptr
product_or(spot::twa_graph_ptr left,spot::twa_graph_ptr right)715 product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right)
716 {
717 if ((type == spot::postprocessor::Buchi)
718 && (left->num_sets() + right->num_sets() >
719 spot::acc_cond::mark_t::max_accsets()))
720 {
721 left = ensure_tba(left);
722 right = ensure_tba(right);
723 }
724 return spot::product_or(left, right);
725 }
726
727 static int
parse_opt(int key,char * arg,struct argp_state *)728 parse_opt(int key, char* arg, struct argp_state*)
729 {
730 // Called from C code, so should not raise any exception.
731 BEGIN_EXCEPTION_PROTECT;
732 // This switch is alphabetically-ordered.
733 switch (key)
734 {
735 case 'c':
736 automaton_format = Count;
737 break;
738 case 'F':
739 jobs.emplace_back(arg, true);
740 break;
741 case 'n':
742 opt_max_count = to_pos_int(arg, "-n/--max-count");
743 break;
744 case 'N':
745 opt_nth = parse_range(arg, 0, std::numeric_limits<int>::max());
746 break;
747 case 'u':
748 opt->uniq = std::unique_ptr<unique_aut_t>(new std::set<canon_aut>());
749 break;
750 case 'v':
751 opt_invert = true;
752 break;
753 case 'x':
754 {
755 const char* opt = extra_options.parse_options(arg);
756 if (opt)
757 error(2, 0, "failed to parse --options near '%s'", opt);
758 }
759 break;
760 case OPT_AP_N:
761 opt_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
762 break;
763 case OPT_ACC_SETS:
764 opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
765 break;
766 case OPT_ACC_SCCS:
767 opt_acc_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
768 opt_art_sccs_set = true;
769 break;
770 case OPT_ACCEPT_WORD:
771 try
772 {
773 opt->acc_words.push_back(spot::parse_word(arg, opt->dict)
774 ->as_automaton());
775 }
776 catch (const spot::parse_error& e)
777 {
778 error(2, 0, "failed to parse the argument of --accept-word:\n%s",
779 e.what());
780 }
781 break;
782 case OPT_ACCEPTANCE_IS:
783 {
784 auto res = argmatch(arg, acc_is_args,
785 (char const*) acc_is_types, sizeof(acc_type));
786 if (res >= 0)
787 opt_acceptance_is = acc_is_types[res];
788 else
789 {
790 try
791 {
792 opt_acceptance_is_given =
793 spot::acc_cond(spot::acc_cond::acc_code(arg));
794 opt_acceptance_is = ACC_Given;
795 }
796 catch (const spot::parse_error& err)
797 {
798 std::cerr << program_name << ": failed to parse '" << arg
799 << ("' as an acceptance formula for "
800 "--acceptance-is\n\t")
801 << err.what()
802 << ("\nIf you do not want to supply a formula, the "
803 "following names are recognized:");
804 acc_type last_val = ACC_Any;
805 for (int i = 0; acc_is_args[i]; i++)
806 if ((i == 0) || last_val != acc_is_types[i])
807 {
808 std::cerr << "\n - '" << acc_is_args[i] << '\'';
809 last_val = acc_is_types[i];
810 }
811 else
812 {
813 std::cerr << ", '" << acc_is_args[i] << '\'';
814 }
815 std::cerr << '\n';
816 exit(2);
817 }
818 }
819 }
820 break;
821 case OPT_ARE_ISOMORPHIC:
822 opt->are_isomorphic = read_automaton(arg, opt->dict);
823 break;
824 case OPT_CLEAN_ACC:
825 opt_clean_acc = true;
826 break;
827 case OPT_CNF_ACC:
828 opt_dnf_acc = false;
829 opt_cnf_acc = true;
830 break;
831 case OPT_COMPLEMENT:
832 if (opt_dualize)
833 error(2, 0, "either --complement or --dualize options"
834 " can be given, not both");
835 opt_complement = true;
836 break;
837 case OPT_COMPLEMENT_ACC:
838 opt_complement_acc = true;
839 break;
840 case OPT_DCA:
841 opt_dca = true;
842 break;
843 case OPT_DECOMPOSE_SCC:
844 opt_decompose_scc = arg;
845 break;
846 case OPT_DESTUT:
847 opt_destut = true;
848 break;
849 case OPT_DUALIZE:
850 if (opt_complement)
851 error(2, 0, "either --complement or --dualize options"
852 " can be given, not both");
853 opt_dualize = true;
854 break;
855 case OPT_DNF_ACC:
856 opt_dnf_acc = true;
857 opt_cnf_acc = false;
858 break;
859 case OPT_STREETT_LIKE:
860 opt_streett_like = true;
861 break;
862 case OPT_EDGES:
863 opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
864 break;
865 case OPT_EXCLUSIVE_AP:
866 opt->excl_ap.add_group(arg);
867 break;
868 case OPT_EQUIVALENT_TO:
869 if (opt->equivalent_pos)
870 error(2, 0, "only one --equivalent-to option can be given");
871 opt->equivalent_pos = read_automaton(arg, opt->dict);
872 opt->equivalent_neg =
873 spot::dualize(ensure_deterministic(opt->equivalent_pos, true));
874 break;
875 case OPT_GENERALIZED_RABIN:
876 if (arg)
877 opt_gra = XARGMATCH("--generalized-rabin", arg, gra_args, gra_types);
878 else
879 opt_gra = GRA_UNIQUE_INF;
880 opt_gsa = GSA_NO;
881 break;
882 case OPT_GENERALIZED_STREETT:
883 if (arg)
884 opt_gsa = XARGMATCH("--generalized-streett", arg, gsa_args, gsa_types);
885 else
886 opt_gsa = GSA_UNIQUE_FIN;
887 opt_gra = GRA_NO;
888 break;
889 case OPT_HAS_EXIST_BRANCHING:
890 opt_has_exist_branching = true;
891 break;
892 case OPT_HAS_UNIV_BRANCHING:
893 opt_has_univ_branching = true;
894 break;
895 case OPT_HIGHLIGHT_ACCEPTING_RUN:
896 opt_highlight_accepting_run =
897 arg ? to_pos_int(arg, "--highlight-accepting-run") : 1;
898 break;
899 case OPT_HIGHLIGHT_NONDET:
900 {
901 int v = arg ? to_pos_int(arg, "--highlight-nondet") : 1;
902 opt_highlight_nondet_edges = opt_highlight_nondet_states = v;
903 break;
904 }
905 case OPT_HIGHLIGHT_NONDET_STATES:
906 opt_highlight_nondet_states =
907 arg ? to_pos_int(arg, "--highlight-nondet-states") : 1;
908 break;
909 case OPT_HIGHLIGHT_NONDET_EDGES:
910 opt_highlight_nondet_edges =
911 arg ? to_pos_int(arg, "--highlight-nondet-edges") : 1;
912 break;
913 case OPT_HIGHLIGHT_WORD:
914 {
915 char* endptr;
916 int res = strtol(arg, &endptr, 10);
917 if (endptr == arg)
918 {
919 res = 1;
920 }
921 else
922 {
923 if (res < 0)
924 error(2, 0, "failed to parse the argument of --highlight-word: "
925 "%d is not positive", res);
926 while (std::isspace(*endptr))
927 ++endptr;
928 if (*endptr != ',')
929 error(2, 0, "failed to parse the argument of --highlight-word: "
930 "%d should be followed by a comma and WORD", res);
931 arg = endptr + 1;
932 }
933 try
934 {
935 opt->hl_words.emplace_back(spot::parse_word(arg, opt->dict)
936 ->as_automaton(), res);
937 }
938 catch (const spot::parse_error& e)
939 {
940 error(2, 0, "failed to parse the argument of --highlight-word:\n%s",
941 e.what());
942 }
943 }
944 break;
945 case OPT_HIGHLIGHT_LANGUAGES:
946 opt_highlight_languages = true;
947 break;
948 case OPT_INSTUT:
949 if (!arg || (arg[0] == '1' && arg[1] == 0))
950 opt_instut = 1;
951 else if (arg[0] == '2' && arg[1] == 0)
952 opt_instut = 2;
953 else
954 error(2, 0, "unknown argument for --instut: %s", arg);
955 break;
956 case OPT_INCLUDED_IN:
957 {
958 auto aut = ensure_deterministic(read_automaton(arg, opt->dict), true);
959 aut = spot::dualize(aut);
960 if (!opt->included_in)
961 opt->included_in = aut;
962 else
963 opt->included_in = spot::product_or(opt->included_in, aut);
964 }
965 break;
966 case OPT_INHERENTLY_WEAK_SCCS:
967 opt_inhweak_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
968 opt_inhweak_sccs_set = true;
969 opt_art_sccs_set = true;
970 break;
971 case OPT_INTERSECT:
972 opt->intersect = read_automaton(arg, opt->dict);
973 break;
974 case OPT_IS_ALTERNATING:
975 opt_is_alternating = true;
976 break;
977 case OPT_IS_COLORED:
978 opt_is_colored = true;
979 break;
980 case OPT_IS_COMPLETE:
981 opt_is_complete = true;
982 break;
983 case OPT_IS_DETERMINISTIC:
984 opt_is_deterministic = true;
985 break;
986 case OPT_IS_EMPTY:
987 opt_is_empty = true;
988 break;
989 case OPT_IS_INHERENTLY_WEAK:
990 opt_is_inherently_weak = true;
991 break;
992 case OPT_IS_VERY_WEAK:
993 opt_is_very_weak = true;
994 break;
995 case OPT_IS_SEMI_DETERMINISTIC:
996 opt_is_semi_deterministic = true;
997 break;
998 case OPT_IS_STUTTER_INVARIANT:
999 opt_is_stutter_invariant = true;
1000 break;
1001 case OPT_IS_TERMINAL:
1002 opt_is_terminal = true;
1003 break;
1004 case OPT_IS_UNAMBIGUOUS:
1005 opt_is_unambiguous = true;
1006 break;
1007 case OPT_IS_WEAK:
1008 opt_is_weak = true;
1009 break;
1010 case OPT_KEEP_STATES:
1011 {
1012 std::vector<long> values = to_longs(arg);
1013 if (!values.empty())
1014 opt_keep_states_initial = values[0];
1015 for (auto res : values)
1016 {
1017 if (res < 0)
1018 error(2, 0, "state ids should be non-negative:"
1019 " --keep-states=%ld", res);
1020 // We don't know yet how many states the automata contain.
1021 if (opt_keep_states.size() <= static_cast<unsigned long>(res))
1022 opt_keep_states.resize(res + 1, false);
1023 opt_keep_states[res] = true;
1024 }
1025 break;
1026 }
1027 case OPT_KILL_STATES:
1028 {
1029 std::vector<long> values = to_longs(arg);
1030 for (auto res : values)
1031 {
1032 if (res < 0)
1033 error(2, 0, "state ids should be non-negative:"
1034 " --kill-states=%ld", res);
1035 opt_kill_states.push_back(res);
1036 }
1037 opt_rem_dead = true;
1038 break;
1039 }
1040 case OPT_MERGE:
1041 opt_merge = true;
1042 break;
1043 case OPT_MASK_ACC:
1044 {
1045 for (auto res : to_longs(arg))
1046 {
1047 if (res < 0)
1048 error(2, 0, "acceptance sets should be non-negative:"
1049 " --mask-acc=%ld", res);
1050 if (static_cast<unsigned long>(res) >=
1051 spot::acc_cond::mark_t::max_accsets())
1052 error(2, 0, "this implementation does not support that many"
1053 " acceptance sets: --mask-acc=%ld", res);
1054 opt_mask_acc.set(res);
1055 }
1056 break;
1057 }
1058 case OPT_NONDET_STATES:
1059 opt_nondet_states = parse_range(arg, 0, std::numeric_limits<int>::max());
1060 opt_nondet_states_set = true;
1061 break;
1062 case OPT_PARTIAL_DEGEN:
1063 {
1064 opt_partial_degen_set = true;
1065 if (arg)
1066 for (auto res : to_longs(arg))
1067 {
1068 if (res < 0)
1069 error(2, 0, "acceptance sets should be non-negative:"
1070 " --partial-degeneralize=%ld", res);
1071 if (static_cast<unsigned long>(res) >=
1072 spot::acc_cond::mark_t::max_accsets())
1073 error(2, 0, "this implementation does not support that many"
1074 " acceptance sets: --partial-degeneralize=%ld", res);
1075 opt_partial_degen.set(res);
1076 }
1077 break;
1078 }
1079 case OPT_PRODUCT_AND:
1080 {
1081 auto a = read_automaton(arg, opt->dict);
1082 if (!opt->product_and)
1083 opt->product_and = std::move(a);
1084 else
1085 opt->product_and = ::product(std::move(opt->product_and),
1086 std::move(a));
1087 }
1088 break;
1089 case OPT_PRODUCT_OR:
1090 {
1091 auto a = read_automaton(arg, opt->dict);
1092 if (!opt->product_or)
1093 opt->product_or = std::move(a);
1094 else
1095 opt->product_or = ::product_or(std::move(opt->product_or),
1096 std::move(a));
1097 }
1098 break;
1099 case OPT_RANDOMIZE:
1100 if (arg)
1101 {
1102 for (auto p = arg; *p; ++p)
1103 switch (*p)
1104 {
1105 case 's':
1106 randomize_st = true;
1107 break;
1108 case 't':
1109 randomize_tr = true;
1110 break;
1111 default:
1112 error(2, 0, "unknown argument for --randomize: '%c'", *p);
1113 }
1114 }
1115 else
1116 {
1117 randomize_tr = true;
1118 randomize_st = true;
1119 }
1120 break;
1121 case OPT_REJ_SCCS:
1122 opt_rej_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
1123 opt_art_sccs_set = true;
1124 break;
1125 case OPT_REJECT_WORD:
1126 try
1127 {
1128 opt->rej_words.push_back(spot::parse_word(arg, opt->dict)
1129 ->as_automaton());
1130 }
1131 catch (const spot::parse_error& e)
1132 {
1133 error(2, 0, "failed to parse the argument of --reject-word:\n%s",
1134 e.what());
1135 }
1136 break;
1137 case OPT_REM_AP:
1138 opt->rem_ap.add_ap(arg);
1139 break;
1140 case OPT_REM_DEAD:
1141 opt_rem_dead = true;
1142 break;
1143 case OPT_REM_FIN:
1144 opt_rem_fin = true;
1145 break;
1146 case OPT_REM_UNREACH:
1147 opt_rem_unreach = true;
1148 break;
1149 case OPT_REM_UNUSED_AP:
1150 opt_rem_unused_ap = true;
1151 break;
1152 case OPT_SAT_MINIMIZE:
1153 opt_sat_minimize = arg ? arg : "";
1154 break;
1155 case OPT_SCCS:
1156 opt_sccs_set = true;
1157 opt_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
1158 break;
1159 case OPT_SEED:
1160 opt_seed = to_int(arg, "--seed");
1161 break;
1162 case OPT_SEP_SETS:
1163 opt_sep_sets = true;
1164 break;
1165 case OPT_SIMPL_ACC:
1166 opt_simpl_acc = true;
1167 break;
1168 case OPT_SIMPLIFY_EXCLUSIVE_AP:
1169 opt_simplify_exclusive_ap = true;
1170 opt_merge = true;
1171 break;
1172 case OPT_SPLIT_EDGES:
1173 opt_split_edges = true;
1174 break;
1175 case OPT_STATES:
1176 opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
1177 break;
1178 case OPT_STRIPACC:
1179 opt_stripacc = true;
1180 break;
1181 case OPT_SUM_OR:
1182 {
1183 auto a = read_automaton(arg, opt->dict);
1184 if (!opt->sum_or)
1185 opt->sum_or = std::move(a);
1186 else
1187 opt->sum_or = spot::sum(std::move(opt->sum_or),
1188 std::move(a));
1189 }
1190 break;
1191 case OPT_SUM_AND:
1192 {
1193 auto a = read_automaton(arg, opt->dict);
1194 if (!opt->sum_and)
1195 opt->sum_and = std::move(a);
1196 else
1197 opt->sum_and = spot::sum_and(std::move(opt->sum_and),
1198 std::move(a));
1199 }
1200 break;
1201 case OPT_TERMINAL_SCCS:
1202 opt_terminal_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
1203 opt_terminal_sccs_set = true;
1204 opt_art_sccs_set = true;
1205 break;
1206 case OPT_TRIV_SCCS:
1207 opt_triv_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
1208 opt_art_sccs_set = true;
1209 break;
1210 case OPT_USED_AP_N:
1211 opt_used_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
1212 need_unused_ap_count = true;
1213 break;
1214 case OPT_UNUSED_AP_N:
1215 opt_unused_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
1216 need_unused_ap_count = true;
1217 break;
1218 case OPT_WEAK_SCCS:
1219 opt_weak_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
1220 opt_weak_sccs_set = true;
1221 opt_art_sccs_set = true;
1222 break;
1223 case ARGP_KEY_ARG:
1224 jobs.emplace_back(arg, true);
1225 break;
1226
1227 default:
1228 return ARGP_ERR_UNKNOWN;
1229 }
1230 END_EXCEPTION_PROTECT;
1231 return 0;
1232 }
1233
unused_ap(const spot::const_twa_graph_ptr & aut)1234 static int unused_ap(const spot::const_twa_graph_ptr& aut)
1235 {
1236 bdd all = aut->ap_vars();
1237 for (auto& e: aut->edges())
1238 {
1239 all = bdd_exist(all, bdd_support(e.cond));
1240 if (all == bddtrue) // All APs are used.
1241 return 0;
1242 }
1243 int count = 0;
1244 while (all != bddtrue)
1245 {
1246 ++count;
1247 all = bdd_high(all);
1248 }
1249 return count;
1250 }
1251
1252 namespace
1253 {
1254 static
match_acceptance(spot::twa_graph_ptr aut)1255 bool match_acceptance(spot::twa_graph_ptr aut)
1256 {
1257 auto& acc = aut->acc();
1258 switch (opt_acceptance_is)
1259 {
1260 case ACC_Any:
1261 return true;
1262 case ACC_Given:
1263 return acc == opt_acceptance_is_given;
1264 case ACC_tt:
1265 return acc.is_t();
1266 case ACC_ff:
1267 return acc.is_f();
1268 case ACC_Buchi:
1269 return acc.is_buchi();
1270 case ACC_GenBuchi:
1271 return acc.is_generalized_buchi();
1272 case ACC_CoBuchi:
1273 return acc.is_co_buchi();
1274 case ACC_GenCoBuchi:
1275 return acc.is_generalized_co_buchi();
1276 case ACC_Rabin:
1277 return acc.is_rabin() >= 0;
1278 case ACC_Streett:
1279 return acc.is_streett() >= 0;
1280 case ACC_GenRabin:
1281 {
1282 std::vector<unsigned> p;
1283 return acc.is_generalized_rabin(p);
1284 }
1285 case ACC_GenStreett:
1286 {
1287 std::vector<unsigned> p;
1288 return acc.is_generalized_streett(p);
1289 }
1290 case ACC_RabinLike:
1291 {
1292 std::vector<spot::acc_cond::rs_pair> p;
1293 return acc.is_rabin_like(p);
1294 }
1295 case ACC_StreettLike:
1296 {
1297 std::vector<spot::acc_cond::rs_pair> p;
1298 return acc.is_streett_like(p);
1299 }
1300 case ACC_Parity:
1301 case ACC_ParityMin:
1302 case ACC_ParityMax:
1303 case ACC_ParityOdd:
1304 case ACC_ParityEven:
1305 case ACC_ParityMinOdd:
1306 case ACC_ParityMaxOdd:
1307 case ACC_ParityMinEven:
1308 case ACC_ParityMaxEven:
1309 {
1310 bool max;
1311 bool odd;
1312 bool is_p = acc.is_parity(max, odd, true);
1313 if (!is_p)
1314 return false;
1315 switch (opt_acceptance_is)
1316 {
1317 case ACC_Parity:
1318 return true;
1319 case ACC_ParityMin:
1320 return !max;
1321 case ACC_ParityMax:
1322 return max;
1323 case ACC_ParityOdd:
1324 return odd;
1325 case ACC_ParityEven:
1326 return !odd;
1327 case ACC_ParityMinOdd:
1328 return !max && odd;
1329 case ACC_ParityMaxOdd:
1330 return max && odd;
1331 case ACC_ParityMinEven:
1332 return !max && !odd;
1333 case ACC_ParityMaxEven:
1334 return max && !odd;
1335 default:
1336 SPOT_UNREACHABLE();
1337 }
1338 }
1339 case ACC_FinLess:
1340 return !acc.uses_fin_acceptance() && !acc.is_f();
1341 }
1342 SPOT_UNREACHABLE();
1343 }
1344
1345
1346 struct autfilt_processor: hoa_processor
1347 {
1348 private:
1349 spot::postprocessor& post;
1350 automaton_printer printer;
1351 public:
autfilt_processor__anondcbaebf00211::autfilt_processor1352 autfilt_processor(spot::postprocessor& post, spot::bdd_dict_ptr dict)
1353 : hoa_processor(dict), post(post), printer(aut_input)
1354 {
1355 }
1356
1357 int
process_automaton__anondcbaebf00211::autfilt_processor1358 process_automaton(const spot::const_parsed_aut_ptr& haut) override
1359 {
1360 static unsigned order = 0;
1361 ++order;
1362
1363 spot::process_timer timer;
1364 timer.start();
1365
1366 // If --stats or --name is used, duplicate the automaton so we
1367 // never modify the original automaton (e.g. with
1368 // merge_edges()) and the statistics about it make sense.
1369 auto aut = ((automaton_format == Stats) || opt_name)
1370 ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
1371 : haut->aut;
1372
1373 // Preprocessing.
1374
1375 if (opt_stripacc)
1376 spot::strip_acceptance_here(aut);
1377 if (opt_merge)
1378 aut->merge_edges();
1379
1380 if (opt_simpl_acc)
1381 simplify_acceptance_here(aut);
1382 else if (opt_clean_acc)
1383 cleanup_acceptance_here(aut);
1384
1385 if (opt_sep_sets)
1386 separate_sets_here(aut);
1387 if (opt_complement_acc)
1388 aut->set_acceptance(aut->acc().num_sets(),
1389 aut->get_acceptance().complement());
1390 if (opt_rem_fin)
1391 aut = remove_fin(aut);
1392 if (opt_dnf_acc)
1393 aut->set_acceptance(aut->acc().num_sets(),
1394 aut->get_acceptance().to_dnf());
1395 if (opt_cnf_acc)
1396 aut->set_acceptance(aut->acc().num_sets(),
1397 aut->get_acceptance().to_cnf());
1398
1399 // Filters.
1400
1401 bool matched = true;
1402
1403 matched &= opt_nth.contains(order);
1404 matched &= opt_states.contains(aut->num_states());
1405 matched &= opt_edges.contains(aut->num_edges());
1406 matched &= opt_accsets.contains(aut->acc().num_sets());
1407 matched &= opt_ap_n.contains(aut->ap().size());
1408 if (matched && need_unused_ap_count)
1409 {
1410 int unused = unused_ap(aut);
1411 matched &= opt_unused_ap_n.contains(unused);
1412 matched &= opt_used_ap_n.contains(aut->ap().size() - unused);
1413 }
1414 if (matched && opt_is_alternating)
1415 matched &= !aut->is_existential();
1416 if (matched && opt_is_colored)
1417 matched &= is_colored(aut);
1418 if (matched && opt_is_complete)
1419 matched &= is_complete(aut);
1420
1421 if (matched && opt_acceptance_is)
1422 matched = match_acceptance(aut);
1423
1424 if (matched && (opt_sccs_set | opt_art_sccs_set))
1425 {
1426 spot::scc_info si(aut);
1427 unsigned n = si.scc_count();
1428 matched = opt_sccs.contains(n);
1429
1430 if (opt_art_sccs_set && matched)
1431 {
1432 si.determine_unknown_acceptance();
1433 unsigned triv = 0;
1434 unsigned acc = 0;
1435 unsigned rej = 0;
1436 unsigned inhweak = 0;
1437 unsigned weak = 0;
1438 unsigned terminal = 0;
1439 for (unsigned s = 0; s < n; ++s)
1440 if (si.is_trivial(s))
1441 {
1442 ++triv;
1443 }
1444 else if (si.is_rejecting_scc(s))
1445 {
1446 ++rej;
1447 }
1448 else
1449 {
1450 ++acc;
1451 if (opt_inhweak_sccs_set)
1452 inhweak += is_inherently_weak_scc(si, s);
1453 if (opt_weak_sccs_set)
1454 weak += is_weak_scc(si, s);
1455 if (opt_terminal_sccs_set)
1456 terminal += is_terminal_scc(si, s);
1457 }
1458 matched &= opt_acc_sccs.contains(acc);
1459 matched &= opt_rej_sccs.contains(rej);
1460 matched &= opt_triv_sccs.contains(triv);
1461 matched &= opt_inhweak_sccs.contains(inhweak);
1462 matched &= opt_weak_sccs.contains(weak);
1463 matched &= opt_terminal_sccs.contains(terminal);
1464 }
1465 }
1466 if (opt_nondet_states_set)
1467 matched &= opt_nondet_states.contains(spot::count_nondet_states(aut));
1468 if (opt_has_univ_branching)
1469 matched &= !aut->is_existential();
1470 if (opt_has_exist_branching)
1471 matched &= !is_universal(aut);
1472 if (opt_is_deterministic)
1473 {
1474 matched &= is_deterministic(aut);
1475 }
1476 else
1477 {
1478 if (opt_is_unambiguous)
1479 matched &= is_unambiguous(aut);
1480 if (opt_is_semi_deterministic)
1481 matched &= is_semi_deterministic(aut);
1482 }
1483 if (opt_is_terminal)
1484 matched &= is_terminal_automaton(aut);
1485 else if (opt_is_very_weak)
1486 matched &= is_very_weak_automaton(aut);
1487 else if (opt_is_weak)
1488 matched &= is_weak_automaton(aut);
1489 else if (opt_is_inherently_weak)
1490 matched &= is_inherently_weak_automaton(aut);
1491 if (opt->are_isomorphic)
1492 matched &= opt->isomorphism_checker->is_isomorphic(aut);
1493 if (opt_is_empty)
1494 matched &= aut->is_empty();
1495 if (opt->intersect)
1496 matched &= aut->intersects(opt->intersect);
1497 if (opt->included_in)
1498 matched &= !aut->intersects(opt->included_in);
1499 if (opt->equivalent_pos)
1500 matched &= !aut->intersects(opt->equivalent_neg)
1501 && spot::contains(aut, opt->equivalent_pos);
1502
1503 if (matched && !opt->acc_words.empty())
1504 for (auto& word_aut: opt->acc_words)
1505 if (spot::product(aut, word_aut)->is_empty())
1506 {
1507 matched = false;
1508 break;
1509 }
1510 if (matched && !opt->rej_words.empty())
1511 for (auto& word_aut: opt->rej_words)
1512 if (!spot::product(aut, word_aut)->is_empty())
1513 {
1514 matched = false;
1515 break;
1516 }
1517 if (opt_is_stutter_invariant)
1518 {
1519 check_stutter_invariance(aut);
1520 assert(aut->prop_stutter_invariant().is_known());
1521 matched &= aut->prop_stutter_invariant().is_true();
1522 }
1523
1524 // Drop or keep matched automata depending on the --invert option
1525 if (matched == opt_invert)
1526 return 0;
1527
1528 // Postprocessing.
1529
1530 if (opt_mask_acc)
1531 aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());
1532
1533 if (!opt->rem_ap.empty())
1534 aut = opt->rem_ap.strip(aut);
1535
1536 // opt_simplify_exclusive_ap is handled only after
1537 // post-processing.
1538 if (!opt->excl_ap.empty())
1539 aut = opt->excl_ap.constrain(aut, false);
1540
1541 if (opt_destut)
1542 aut = spot::closure_inplace(std::move(aut));
1543 if (opt_instut == 1)
1544 aut = spot::sl(std::move(aut));
1545 else if (opt_instut == 2)
1546 aut = spot::sl2_inplace(std::move(aut));
1547
1548 if (!opt_kill_states.empty())
1549 {
1550 unsigned ns = aut->num_states();
1551 for (unsigned s: opt_kill_states)
1552 if (s < ns)
1553 aut->kill_state(s);
1554 }
1555 if (!opt_keep_states.empty())
1556 aut = mask_keep_accessible_states(aut, opt_keep_states,
1557 opt_keep_states_initial);
1558 if (opt_rem_dead)
1559 aut->purge_dead_states();
1560 else if (opt_rem_unreach)
1561 aut->purge_unreachable_states();
1562
1563 if (opt_partial_degen_set)
1564 {
1565 if (opt_partial_degen)
1566 {
1567 auto sets = opt_partial_degen & aut->acc().all_sets();
1568 aut = spot::partial_degeneralize(aut, sets);
1569 }
1570 else
1571 {
1572 aut = spot::partial_degeneralize(aut);
1573 }
1574 }
1575
1576 if (opt->product_and)
1577 aut = ::product(std::move(aut), opt->product_and);
1578 if (opt->product_or)
1579 aut = ::product_or(std::move(aut), opt->product_or);
1580
1581 if (opt->sum_or)
1582 aut = spot::sum(std::move(aut), opt->sum_or);
1583 if (opt->sum_and)
1584 aut = spot::sum_and(std::move(aut), opt->sum_and);
1585
1586 if (opt_decompose_scc)
1587 {
1588 aut = decompose_scc(aut, opt_decompose_scc);
1589 if (!aut)
1590 return 0;
1591 }
1592
1593 if (opt_sat_minimize)
1594 {
1595 aut = spot::sat_minimize(aut, opt_sat_minimize, sbacc);
1596 if (!aut)
1597 return 0;
1598 }
1599
1600 if (opt_complement)
1601 {
1602 aut = spot::complement(aut);
1603 aut->merge_edges();
1604 }
1605
1606 if (opt_dualize)
1607 aut = spot::dualize(aut);
1608
1609 aut = post.run(aut, nullptr);
1610
1611 if (opt_gra)
1612 aut = spot::to_generalized_rabin(aut, opt_gra == GRA_SHARE_INF);
1613 if (opt_gsa)
1614 aut = spot::to_generalized_streett(aut, opt_gsa == GSA_SHARE_FIN);
1615
1616 if (opt_streett_like)
1617 aut = spot::dnf_to_streett(aut);
1618
1619 if (opt_simplify_exclusive_ap && !opt->excl_ap.empty())
1620 aut = opt->excl_ap.constrain(aut, true);
1621 else if (opt_rem_unused_ap) // constrain(aut, true) already does that
1622 aut->remove_unused_ap();
1623
1624 if (opt_split_edges)
1625 aut = spot::split_edges(aut);
1626
1627 if (randomize_st || randomize_tr)
1628 spot::randomize(aut, randomize_st, randomize_tr);
1629
1630 if (opt_highlight_nondet_states >= 0)
1631 spot::highlight_nondet_states(aut, opt_highlight_nondet_states);
1632 if (opt_highlight_nondet_edges >= 0)
1633 spot::highlight_nondet_edges(aut, opt_highlight_nondet_edges);
1634
1635 if (opt_highlight_languages)
1636 spot::highlight_languages(aut);
1637
1638 if (opt_highlight_accepting_run >= 0)
1639 aut->accepting_run()->highlight(opt_highlight_accepting_run);
1640
1641 if (!opt->hl_words.empty())
1642 for (auto& word_aut: opt->hl_words)
1643 {
1644 if (aut->acc().uses_fin_acceptance())
1645 error(2, 0,
1646 "--highlight-word does not yet work with Fin acceptance");
1647 if (auto run = spot::product(aut, word_aut.first)->accepting_run())
1648 run->project(aut)->highlight(word_aut.second);
1649 }
1650
1651 timer.stop();
1652 if (opt->uniq)
1653 {
1654 auto tmp =
1655 spot::canonicalize(make_twa_graph(aut,
1656 spot::twa::prop_set::all()));
1657 if (!opt->uniq->emplace(tmp).second)
1658 return 0;
1659 }
1660
1661 ++match_count;
1662
1663 printer.print(aut, timer, nullptr, haut->filename.c_str(), -1,
1664 haut, prefix, suffix);
1665
1666 if (opt_max_count >= 0 && match_count >= opt_max_count)
1667 abort_run = true;
1668
1669 return 0;
1670 }
1671 };
1672 }
1673
1674 int
main(int argc,char ** argv)1675 main(int argc, char** argv)
1676 {
1677 return protected_main(argv, [&] {
1678 const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
1679 argp_program_doc, children, nullptr, nullptr };
1680
1681 // This will ensure that all objects stored in this struct are
1682 // destroyed before global variables.
1683 opt_t o;
1684 opt = &o;
1685
1686 // Disable post-processing as much as possible by default.
1687 level = spot::postprocessor::Low;
1688 pref = spot::postprocessor::Any;
1689 type = spot::postprocessor::Generic;
1690 if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
1691 exit(err);
1692
1693 if (level_set && !pref_set)
1694 pref = spot::postprocessor::Small;
1695 if (pref_set && !level_set)
1696 level = spot::postprocessor::High;
1697
1698 check_no_automaton();
1699
1700 if (opt->are_isomorphic)
1701 {
1702 if (opt_merge)
1703 opt->are_isomorphic->merge_edges();
1704 opt->isomorphism_checker = std::unique_ptr<spot::isomorphism_checker>
1705 (new spot::isomorphism_checker(opt->are_isomorphic));
1706 }
1707
1708
1709 spot::srand(opt_seed);
1710
1711 spot::postprocessor post(&extra_options);
1712 post.set_type(type);
1713 post.set_pref(pref | comp | sbacc | colored);
1714 post.set_level(level);
1715
1716 autfilt_processor processor(post, o.dict);
1717 if (processor.run())
1718 return 2;
1719
1720 // Diagnose unused -x options
1721 extra_options.report_unused_options();
1722
1723 if (automaton_format == Count)
1724 std::cout << match_count << std::endl;
1725
1726 check_cout();
1727 return match_count ? 0 : 1;
1728 });
1729 }
1730