From e50ff35d0f0e1996585dea60d18d3b0fe3515126 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Apr 2016 16:44:24 +0200 Subject: [PATCH] autfilt: add options to filter by SCC count and types * bin/autfilt.cc: Implement those options. * NEWS: Mention them. * doc/org/randaut.org: Add a quick example. * tests/core/strength.test: Add some basic tests. * tests/core/acc_word.test: Adjust options abbreviations. --- NEWS | 5 ++ bin/autfilt.cc | 121 ++++++++++++++++++++++++++++++++++++++- doc/org/randaut.org | 30 ++++++++++ tests/core/acc_word.test | 4 +- tests/core/strength.test | 10 ++++ 5 files changed, 165 insertions(+), 5 deletions(-) diff --git a/NEWS b/NEWS index 853fa4ecb..b89c16983 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,11 @@ New in spot 2.0a (not yet released) * ltldo has a new option --errors=... to specify how to deal with errors from executed tools. + * autfilt has several new options to filter automata by count of + SCCs (--sccs=RANGE) or by type of SCCs (--accepting-sccs=RANGE, + --rejecting-sccs=RANGE, trivial-sccs=RANGE, --terminal-sccs=RANGE, + --weak-sccs=RANGE, --inherently-weak-sccs=RANGE). + Library: * The print_hoa() function will now output version 1.1 of the HOA diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 54c9128cf..5924bf642 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -59,6 +59,8 @@ #include #include #include +#include +#include static const char argp_program_doc[] ="\ Convert, transform, and filter omega-automata.\v\ @@ -69,7 +71,8 @@ Exit status:\n\ // Keep this list sorted enum { - OPT_ACC_SETS = 256, + OPT_ACC_SCCS = 256, + OPT_ACC_SETS, OPT_ACCEPT_WORD, OPT_AP_N, OPT_ARE_ISOMORPHIC, @@ -87,6 +90,7 @@ enum { OPT_GENERIC, OPT_INSTUT, OPT_INCLUDED_IN, + OPT_INHERENTLY_WEAK_SCCS, OPT_INTERSECT, OPT_IS_COMPLETE, OPT_IS_DETERMINISTIC, @@ -101,17 +105,22 @@ enum { OPT_PRODUCT_AND, OPT_PRODUCT_OR, OPT_RANDOMIZE, + OPT_REJ_SCCS, OPT_REJECT_WORD, OPT_REM_AP, OPT_REM_DEAD, OPT_REM_UNREACH, OPT_REM_FIN, OPT_SAT_MINIMIZE, + OPT_SCCS, OPT_SEED, OPT_SEP_SETS, OPT_SIMPLIFY_EXCLUSIVE_AP, OPT_STATES, OPT_STRIPACC, + OPT_TERMINAL_SCCS, + OPT_TRIV_SCCS, + OPT_WEAK_SCCS, }; static const argp_option options[] = @@ -227,6 +236,29 @@ static const argp_option options[] = "keep automata whose number of edges is in RANGE", 0 }, { "acc-sets", OPT_ACC_SETS, "RANGE", 0, "keep automata whose number of acceptance sets is in RANGE", 0 }, + { "sccs", OPT_SCCS, "RANGE", 0, + "keep automata whose number of SCCs is in RANGE", 0 }, + { "acc-sccs", OPT_ACC_SCCS, "RANGE", 0, + "keep automata whose number of non-trivial accepting SCCs is in RANGE", + 0 }, + { "accepting-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "rej-sccs", OPT_REJ_SCCS, "RANGE", 0, + "keep automata whose number of non-trivial rejecting SCCs is in RANGE", + 0 }, + { "rejecting-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "triv-sccs", OPT_TRIV_SCCS, "RANGE", 0, + "keep automata whose number of trivial SCCs is in RANGE", 0 }, + { "trivial-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "inherently-weak-sccs", OPT_INHERENTLY_WEAK_SCCS, "RANGE", 0, + "keep automata whose number of accepting inherently-weak SCCs is in " + "RANGE. An accepting SCC is inherently weak if it does not have a " + "rejecting cycle.", 0 }, + { "weak-sccs", OPT_WEAK_SCCS, "RANGE", 0, + "keep automata whose number of accepting weak SCCs is in RANGE. " + "In a weak SCC, all transitions belong to the same acceptance sets.", 0 }, + { "terminal-sccs", OPT_TERMINAL_SCCS, "RANGE", 0, + "keep automata whose number of accepting terminal SCCs is in RANGE. " + "Terminal SCCs are weak and complete.", 0 }, { "accept-word", OPT_ACCEPT_WORD, "WORD", 0, "keep automata that accept WORD", 0 }, { "reject-word", OPT_REJECT_WORD, "WORD", 0, @@ -303,6 +335,18 @@ static range opt_states = { 0, std::numeric_limits::max() }; static range opt_edges = { 0, std::numeric_limits::max() }; static range opt_accsets = { 0, std::numeric_limits::max() }; static range opt_ap_n = { 0, std::numeric_limits::max() }; +static range opt_sccs = { 0, std::numeric_limits::max() }; +static range opt_acc_sccs = { 0, std::numeric_limits::max() }; +static range opt_rej_sccs = { 0, std::numeric_limits::max() }; +static range opt_triv_sccs = { 0, std::numeric_limits::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::max() }; +static bool opt_inhweak_sccs_set = false; +static range opt_weak_sccs = { 0, std::numeric_limits::max() }; +static bool opt_weak_sccs_set = false; +static range opt_terminal_sccs = { 0, std::numeric_limits::max() }; +static bool opt_terminal_sccs_set = false; static int opt_max_count = -1; static bool opt_destut = false; static char opt_instut = 0; @@ -371,6 +415,10 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_ACC_SETS: opt_accsets = parse_range(arg, 0, std::numeric_limits::max()); break; + case OPT_ACC_SCCS: + opt_acc_sccs = parse_range(arg, 0, std::numeric_limits::max()); + opt_art_sccs_set = true; + break; case OPT_ACCEPT_WORD: try { @@ -440,6 +488,11 @@ parse_opt(int key, char* arg, struct argp_state*) opt->included_in = spot::product_or(opt->included_in, aut); } break; + case OPT_INHERENTLY_WEAK_SCCS: + opt_inhweak_sccs = parse_range(arg, 0, std::numeric_limits::max()); + opt_inhweak_sccs_set = true; + opt_art_sccs_set = true; + break; case OPT_INTERSECT: opt->intersect = read_automaton(arg, opt->dict); break; @@ -542,6 +595,10 @@ parse_opt(int key, char* arg, struct argp_state*) randomize_st = true; } break; + case OPT_REJ_SCCS: + opt_rej_sccs = parse_range(arg, 0, std::numeric_limits::max()); + opt_art_sccs_set = true; + break; case OPT_REJECT_WORD: try { @@ -569,6 +626,10 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_SAT_MINIMIZE: opt_sat_minimize = arg ? arg : ""; break; + case OPT_SCCS: + opt_sccs_set = true; + opt_sccs = parse_range(arg, 0, std::numeric_limits::max()); + break; case OPT_SEED: opt_seed = to_int(arg); break; @@ -585,6 +646,20 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_STRIPACC: opt_stripacc = true; break; + case OPT_TERMINAL_SCCS: + opt_terminal_sccs = parse_range(arg, 0, std::numeric_limits::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::max()); + opt_art_sccs_set = true; + break; + case OPT_WEAK_SCCS: + opt_weak_sccs = parse_range(arg, 0, std::numeric_limits::max()); + opt_weak_sccs_set = true; + opt_art_sccs_set = true; + break; case ARGP_KEY_ARG: jobs.emplace_back(arg, true); break; @@ -662,8 +737,48 @@ namespace matched &= opt_ap_n.contains(aut->ap().size()); if (opt_is_complete) matched &= is_complete(aut); - if (opt_is_deterministic) - matched &= is_deterministic(aut); + if (matched && (opt_sccs_set | opt_art_sccs_set)) + { + spot::scc_info si(aut); + unsigned n = si.scc_count(); + matched = opt_sccs.contains(n); + + if (opt_art_sccs_set && matched) + { + si.determine_unknown_acceptance(); + unsigned triv = 0; + unsigned acc = 0; + unsigned rej = 0; + unsigned inhweak = 0; + unsigned weak = 0; + unsigned terminal = 0; + for (unsigned s = 0; s < n; ++s) + if (si.is_trivial(s)) + { + ++triv; + } + else if (si.is_rejecting_scc(s)) + { + ++rej; + } + else + { + ++acc; + if (opt_inhweak_sccs_set) + inhweak += is_inherently_weak_scc(si, s); + if (opt_weak_sccs_set) + weak += is_weak_scc(si, s); + if (opt_terminal_sccs_set) + terminal += is_terminal_scc(si, s); + } + matched &= opt_acc_sccs.contains(acc); + matched &= opt_rej_sccs.contains(rej); + matched &= opt_triv_sccs.contains(triv); + matched &= opt_inhweak_sccs.contains(inhweak); + matched &= opt_weak_sccs.contains(weak); + matched &= opt_terminal_sccs.contains(terminal); + } + } if (opt_is_deterministic) matched &= is_deterministic(aut); else if (opt_is_unambiguous) diff --git a/doc/org/randaut.org b/doc/org/randaut.org index e2064a432..f51f63a04 100644 --- a/doc/org/randaut.org +++ b/doc/org/randaut.org @@ -476,3 +476,33 @@ Use option =-n= to specify a number of automata to build. A negative value will cause an infinite number of automata to be produced. This generation of multiple automata is useful when piped to another tool that can process automata in batches. + +Here is an example were we use [[file:autfilt.org][=autfilt=]] to scan an infinite stream +(=-n -1=) of random parity automata for the first automaton (=-n 1=) +that have exactly 5 SCCs of particular natures: we want 1 trivial SCC +(i.e. an SCC with no cycle), 1 rejecting SCC (an SCC without any +accepting SCCs), 2 inherently weak SCCs (SCCs contains only rejecting +cycles) among which one should be weak (all transitions should belong +to the same sets). This leaves us with one extra SCC that should +necessarily mix accepting and rejecting cycles. + +(Note: the '=.=' argument passed to =--dot= below hides default +options discussed [[file:oaut.org::#default-dot][on another page]], while '=a=' causes the acceptance +condition to be displayed and'=s=' shows SCCs.) + +#+NAME: randaut7 +#+BEGIN_SRC sh :results verbatim :exports code +randaut -n -1 --colored -A'parity min odd 4' a b | +autfilt --sccs=5 --trivial-sccs=1 --rejecting-sccs=1 \ + --inherently-weak-sccs=2 --weak-sccs=1 -n 1 --dot=.as +#+END_SRC + +#+BEGIN_SRC dot :file randaut7.png :cmdline -Tpng :var txt=randaut7 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:randaut7.png]] + +You should be able to find each of the expected type of SCCs in the above picture. +The green rectangles mark the three SCCs that contain some accepting cycles. diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test index d66e07834..d80d0183c 100644 --- a/tests/core/acc_word.test +++ b/tests/core/acc_word.test @@ -49,8 +49,8 @@ randltl -n -1 a b | ltlfilt --simplify --uniq \ diff out expect # Test syntax errors -autfilt --reject='foobar' error && exit 1 -autfilt --accept='cycle{foo' >error && exit 1 +autfilt --reject-w='foobar' error && exit 1 +autfilt --accept-w='cycle{foo' >error && exit 1 cat error cat >expect < out3 diff out3 expected2 + + +test 2 = `autfilt -c --sccs=4 out` +test 5 = `autfilt -c --sccs=2 out` +test 1 = `autfilt -c -v --inherently-weak-sccs=1.. out` +test 2 = `autfilt -c --weak-sccs=2 out` +test 14 = `autfilt -c --terminal-sccs=1 out` +test 2 = `autfilt -c --terminal-sccs=1 --inherently-weak-sccs=2 out` +test 4 = `autfilt -c --rejecting-sccs=1 --accepting-sccs=1 out` +test 0 = `autfilt -c --trivial-sccs=1.. out`