From 62302b6046b3ed4d13c41b016b6b80f62e6b4f51 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 4 Nov 2017 20:53:57 +0100 Subject: [PATCH] autfilt: introduce --acceptance-is Fixes #288. * bin/autfilt.cc: Implement it. * spot/twa/acc.cc, spot/twa/acc.hh: Add acc_cond::is_generalized_streett, acc_cond::operator==, and acc_cond::operator!=. * tests/core/randaut.test: Add some tests. * NEWS: Mention it. --- NEWS | 5 + bin/autfilt.cc | 230 ++++++++++++++++++++++++++++++++++++++++ spot/twa/acc.cc | 81 ++++++++++++++ spot/twa/acc.hh | 13 +++ tests/core/randaut.test | 61 ++++++++++- 5 files changed, 388 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 1663d6ccc..15c1aba2d 100644 --- a/NEWS +++ b/NEWS @@ -22,6 +22,11 @@ New in spot 2.4.1.dev (not yet released) deterministic co-Büchi automaton using the new functions [nsa-dnf]_to_dca() described below. + - autfilt learned --acceptance-is=ACC to filter automata by + acceptance condition. ACC can be the name of some acceptance + class (e.g. Büchi, Fin-less, Streett-like) or a precise acceptance + formula in the HOA syntax. + - ltlfilt learned to measure wall-time using --format=%r. - ltlfilt learned to measure cpu-time (as opposed to wall-time) using diff --git a/bin/autfilt.cc b/bin/autfilt.cc index d261c4af0..06a809f03 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -83,6 +83,7 @@ enum { OPT_ACC_SCCS = 256, OPT_ACC_SETS, OPT_ACCEPT_WORD, + OPT_ACCEPTANCE_IS, OPT_AP_N, OPT_ARE_ISOMORPHIC, OPT_CLEAN_ACC, @@ -174,6 +175,8 @@ static const argp_option options[] = { "unused-ap", OPT_UNUSED_AP_N, "RANGE", 0, "match automata with a number of declared, but unused atomic " "propositions in RANGE", 0 }, + { "acceptance-is", OPT_ACCEPTANCE_IS, "NAME|FORMULA", 0, + "match automata with given accetance condition", 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 }, @@ -425,6 +428,99 @@ static gra_type const gra_types[] = }; ARGMATCH_VERIFY(gra_args, gra_types); +enum acc_type { + ACC_Any = 0, + ACC_Given, + ACC_tt, + ACC_ff, + ACC_Buchi, + ACC_GenBuchi, + ACC_CoBuchi, + ACC_GenCoBuchi, + ACC_Rabin, + ACC_Streett, + ACC_GenRabin, + ACC_GenStreett, + ACC_RabinLike, + ACC_StreettLike, + ACC_Parity, + ACC_ParityMin, + ACC_ParityMax, + ACC_ParityOdd, + ACC_ParityEven, + ACC_ParityMinOdd, + ACC_ParityMaxOdd, + ACC_ParityMinEven, + ACC_ParityMaxEven, + ACC_FinLess, +}; +static acc_type opt_acceptance_is = ACC_Any; +spot::acc_cond opt_acceptance_is_given; +static char const *const acc_is_args[] = + { + "any", + "t", "all", + "f", "none", + "Buchi", "Büchi", + "generalized-Buchi", "generalized-Büchi", + "genBuchi", "genBüchi", "gen-Buchi", "gen-Büchi", + "coBuchi", "coBüchi", "co-Buchi", "co-Büchi", + "generalized-coBuchi", "generalized-coBüchi", + "generalized-co-Buchi", "generalized-co-Büchi", + "gen-coBuchi", "gen-coBüchi", + "gen-co-Buchi", "gen-co-Büchi", + "gencoBuchi", "gencoBüchi", + "Rabin", + "Streett", + "generalized-Rabin", "gen-Rabin", "genRabin", + "generalized-Streett", "gen-Streett", "genStreett", + "Streett-like", + "Rabin-like", + "parity", + "parity min", "parity-min", + "parity max", "parity-max", + "parity odd", "parity-odd", + "parity even", "parity-even", + "parity min even", "parity-min-even", + "parity min odd", "parity-min-odd", + "parity max even", "parity-max-even", + "parity max odd", "parity-max-odd", + "Fin-less", "Finless", + nullptr, + }; +static acc_type const acc_is_types[] = + { + ACC_Any, + ACC_tt, ACC_tt, + ACC_ff, ACC_ff, + ACC_Buchi, ACC_Buchi, + ACC_GenBuchi, ACC_GenBuchi, + ACC_GenBuchi, ACC_GenBuchi, ACC_GenBuchi, ACC_GenBuchi, + ACC_CoBuchi, ACC_CoBuchi, ACC_CoBuchi, ACC_CoBuchi, + ACC_GenCoBuchi, ACC_GenCoBuchi, + ACC_GenCoBuchi, ACC_GenCoBuchi, + ACC_GenCoBuchi, ACC_GenCoBuchi, + ACC_GenCoBuchi, ACC_GenCoBuchi, + ACC_GenCoBuchi, ACC_GenCoBuchi, + ACC_Rabin, + ACC_Streett, + ACC_GenRabin, ACC_GenRabin, ACC_GenRabin, + ACC_GenStreett, ACC_GenStreett, ACC_GenStreett, + ACC_StreettLike, + ACC_RabinLike, + ACC_Parity, + ACC_ParityMin, ACC_ParityMin, + ACC_ParityMax, ACC_ParityMax, + ACC_ParityOdd, ACC_ParityOdd, + ACC_ParityEven, ACC_ParityEven, + ACC_ParityMinEven, ACC_ParityMinEven, + ACC_ParityMinOdd, ACC_ParityMinOdd, + ACC_ParityMaxEven, ACC_ParityMaxEven, + ACC_ParityMaxOdd, ACC_ParityMaxOdd, + ACC_FinLess, ACC_FinLess, + }; +ARGMATCH_VERIFY(acc_is_args, acc_is_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[] = @@ -589,6 +685,45 @@ parse_opt(int key, char* arg, struct argp_state*) e.what()); } break; + case OPT_ACCEPTANCE_IS: + { + auto res = argmatch(arg, acc_is_args, + (char const*) acc_is_types, sizeof(acc_type)); + if (res >= 0) + opt_acceptance_is = acc_is_types[res]; + else + { + try + { + opt_acceptance_is_given = + spot::acc_cond(spot::acc_cond::acc_code(arg)); + opt_acceptance_is = ACC_Given; + } + catch (const spot::parse_error& err) + { + std::cerr << program_name << ": failed to parse '" << arg + << ("' as an acceptance formula for " + "--acceptance-is\n\t") + << err.what() + << ("\nIf you do not want to supply a formula, the " + "following names are recognized:"); + acc_type last_val = ACC_Any; + for (int i = 0; acc_is_args[i]; i++) + if ((i == 0) || last_val != acc_is_types[i]) + { + std::cerr << "\n - '" << acc_is_args[i] << '\''; + last_val = acc_is_types[i]; + } + else + { + std::cerr << ", '" << acc_is_args[i] << '"'; + } + std::cerr << std::flush; + exit(2); + } + } + } + break; case OPT_ARE_ISOMORPHIC: opt->are_isomorphic = read_automaton(arg, opt->dict); break; @@ -976,6 +1111,97 @@ static int unused_ap(const spot::const_twa_graph_ptr& aut) namespace { + static + bool match_acceptance(spot::twa_graph_ptr aut) + { + auto& acc = aut->acc(); + switch (opt_acceptance_is) + { + case ACC_Any: + return true; + case ACC_Given: + return acc == opt_acceptance_is_given; + case ACC_tt: + return acc.is_t(); + case ACC_ff: + return acc.is_f(); + case ACC_Buchi: + return acc.is_buchi(); + case ACC_GenBuchi: + return acc.is_generalized_buchi(); + case ACC_CoBuchi: + return acc.is_co_buchi(); + case ACC_GenCoBuchi: + return acc.is_generalized_co_buchi(); + case ACC_Rabin: + return acc.is_rabin() >= 0; + case ACC_Streett: + return acc.is_streett() >= 0; + case ACC_GenRabin: + { + std::vector p; + return acc.is_generalized_rabin(p); + } + case ACC_GenStreett: + { + std::vector p; + return acc.is_generalized_streett(p); + } + case ACC_RabinLike: + { + std::vector p; + return acc.is_rabin_like(p); + } + case ACC_StreettLike: + { + std::vector p; + return acc.is_streett_like(p); + } + case ACC_Parity: + case ACC_ParityMin: + case ACC_ParityMax: + case ACC_ParityOdd: + case ACC_ParityEven: + case ACC_ParityMinOdd: + case ACC_ParityMaxOdd: + case ACC_ParityMinEven: + case ACC_ParityMaxEven: + { + bool max; + bool odd; + bool is_p = acc.is_parity(max, odd, true); + if (!is_p) + return false; + switch (opt_acceptance_is) + { + case ACC_Parity: + return true; + case ACC_ParityMin: + return !max; + case ACC_ParityMax: + return max; + case ACC_ParityOdd: + return odd; + case ACC_ParityEven: + return !odd; + case ACC_ParityMinOdd: + return !max && odd; + case ACC_ParityMaxOdd: + return max && odd; + case ACC_ParityMinEven: + return !max && !odd; + case ACC_ParityMaxEven: + return max && !odd; + default: + SPOT_UNREACHABLE(); + } + } + case ACC_FinLess: + return !acc.uses_fin_acceptance(); + } + SPOT_UNREACHABLE(); + } + struct autfilt_processor: hoa_processor { @@ -1045,6 +1271,10 @@ namespace matched &= !aut->is_existential(); if (matched && opt_is_complete) matched &= is_complete(aut); + + if (matched && opt_acceptance_is) + matched = match_acceptance(aut); + if (matched && (opt_sccs_set | opt_art_sccs_set)) { spot::scc_info si(aut); diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 72005e475..119f81ce9 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -649,6 +649,7 @@ namespace spot return is_rs_like(code_, acc_op::Or, acc_op::And, acc_op::Inf, pairs); } + // PAIRS contains the number of Inf in each pair. bool acc_cond::is_generalized_rabin(std::vector& pairs) const { @@ -729,6 +730,86 @@ namespace spot && (seen_fin | seen_inf) == all_sets()); } + // PAIRS contains the number of Inf in each pair. + bool acc_cond::is_generalized_streett(std::vector& pairs) const + { + pairs.clear(); + if (is_generalized_buchi()) + { + pairs.resize(num_); + return true; + } + if (code_.is_f() + || code_.back().sub.op != acc_op::And) + return false; + + auto s = code_.back().sub.size; + acc_cond::mark_t seen_fin = 0U; + acc_cond::mark_t seen_inf = 0U; + // Each pairs is the position of a Inf followed + // by the number of Fin. + std::map p; + while (s) + { + --s; + if (code_[s].sub.op == acc_op::Or) + { + auto o1 = code_[--s].sub.op; + auto m1 = code_[--s].mark; + auto o2 = code_[--s].sub.op; + auto m2 = code_[--s].mark; + + // We assume + // Inf(n) | Fin({n+1,n+2,...,n+i}) + // o1 (m1) o2 (m2) + // swap if it is the converse + if (o2 == acc_cond::acc_op::Inf) + { + std::swap(o1, o2); + std::swap(m1, m2); + } + + if (o1 != acc_cond::acc_op::Inf + || o2 != acc_cond::acc_op::Fin + || m1.count() != 1) + return false; + + unsigned i = m2.count(); + // If we have seen this pair already, it must have the + // same size. + if (p.emplace(m1.max_set(), i).first->second != i) + return false; + assert(i > 0); + unsigned j = m1.max_set(); // == n+1 + do + if (!m2.has(j++)) + return false; + while (--i); + + seen_inf |= m1; + seen_fin |= m2; + } + else if (code_[s].sub.op == acc_op::Inf) + { + auto m1 = code_[--s].mark; + for (auto s: m1.sets()) + // If we have seen this pair already, it must have the + // same size. + if (p.emplace(s, 0U).first->second != 0U) + return false; + seen_inf |= m1; + } + else + { + return false; + } + } + for (auto i: p) + pairs.emplace_back(i.second); + return (!(seen_inf & seen_fin) + && (seen_inf | seen_fin) == all_sets()); + } + acc_cond::acc_code acc_cond::acc_code::parity(bool max, bool odd, unsigned sets) { diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 26fb9a5e4..a1ffa4ee4 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -985,6 +985,16 @@ namespace spot return code_; } + bool operator==(const acc_cond& other) const + { + return other.num_sets() == num_ && other.get_acceptance() == code_; + } + + bool operator!=(const acc_cond& other) const + { + return !(*this == other); + } + bool uses_fin_acceptance() const { return uses_fin_acceptance_; @@ -1124,6 +1134,9 @@ namespace spot // Return the number of Inf in each pair. bool is_generalized_rabin(std::vector& pairs) const; + // Return the number of Inf in each pair. + bool is_generalized_streett(std::vector& pairs) const; + // If EQUIV is false, this return true iff the acceptance // condition is a parity condition written in the canonical way // given in the HOA specifications. If EQUIV is true, then we diff --git a/tests/core/randaut.test b/tests/core/randaut.test index 5769f14e0..0951d2742 100755 --- a/tests/core/randaut.test +++ b/tests/core/randaut.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +# Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -84,7 +84,7 @@ grep 'autfilt: options --output and --count are incompatible' stderr randaut -A 'random 4' -n 2 -Q5 -H 2 randaut -A 'parity rand rand 2..4' -n3 -Q5 -H 2 randaut -A 'generalized-Rabin 3 1..2 2..3 0' -n3 -Q5 -H 2 -) | grep -E '(acc-name:|Acceptance:)' > output +) | tee input | grep -E '(acc-name:|Acceptance:)' > output cat output a=Acceptance @@ -110,6 +110,63 @@ $a: 8 (Fin(0) & (Inf(1)&Inf(2))) | (Fin(3) & (Inf(4)&Inf(5)&Inf(6))) | Fin(7) EOF diff output expected +autfilt --acceptance-is=generalized-Buchi --stats='%g,%[s]g' >stdout expected <stdout stdout expected <stdout expected <stdout expected <stdout expected <stdout expected <stdout expected <err && exit 1 +grep acceptance-is err +grep 'syntax error at end of acceptance' err +grep " - 'generalized-Streett'" err + randaut --spin -A 'random 2' 2 2>stderr && exit 1 grep 'randaut: --spin.*--acceptance' stderr randaut --ba --acceptance='random 2' 2 2>stderr && exit 1