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.
This commit is contained in:
Alexandre Duret-Lutz
parent
3334d37bb5
commit
62302b6046
5 changed files with 388 additions and 2 deletions
5
NEWS
5
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
|
||||
|
|
|
|||
230
bin/autfilt.cc
230
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<unsigned> p;
|
||||
return acc.is_generalized_rabin(p);
|
||||
}
|
||||
case ACC_GenStreett:
|
||||
{
|
||||
std::vector<unsigned> p;
|
||||
return acc.is_generalized_streett(p);
|
||||
}
|
||||
case ACC_RabinLike:
|
||||
{
|
||||
std::vector<spot::acc_cond::rs_pair> p;
|
||||
return acc.is_rabin_like(p);
|
||||
}
|
||||
case ACC_StreettLike:
|
||||
{
|
||||
std::vector<spot::acc_cond::rs_pair> 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);
|
||||
|
|
|
|||
|
|
@ -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<unsigned>& 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<unsigned>& 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<unsigned, unsigned> 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)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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<unsigned>& pairs) const;
|
||||
|
||||
// Return the number of Inf in each pair.
|
||||
bool is_generalized_streett(std::vector<unsigned>& 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
|
||||
|
|
|
|||
|
|
@ -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 <input
|
||||
cat >expected <<EOF
|
||||
Inf(0)&Inf(1)&Inf(2)&Inf(3),generalized-Buchi
|
||||
Inf(0)&Inf(1)&Inf(2)&Inf(3),generalized-Buchi
|
||||
EOF
|
||||
diff stdout expected
|
||||
autfilt --acceptance-is=Fin-less --stats='%g,%[s]g' >stdout <input
|
||||
diff stdout expected
|
||||
|
||||
autfilt --acceptance-is=generalized-Rabin --stats='%[sb]g' >stdout <input
|
||||
cat >expected <<EOF
|
||||
gen. Rabin
|
||||
gen. Rabin
|
||||
gen. Rabin
|
||||
EOF
|
||||
diff stdout expected
|
||||
|
||||
autfilt --acceptance-is=parity --stats='%g,%[sb]g' >stdout <input
|
||||
cat >expected <<EOF
|
||||
Inf(0) | (Fin(1) & (Inf(2) | Fin(3))),parity
|
||||
Fin(1) & Inf(0),parity
|
||||
Inf(3) | (Fin(2) & (Inf(1) | Fin(0))),parity
|
||||
EOF
|
||||
diff stdout expected
|
||||
|
||||
autfilt --acceptance-is=parity-odd --stats='%g,%[m]g' >stdout <input
|
||||
cat >expected <<EOF
|
||||
Inf(3) | (Fin(2) & (Inf(1) | Fin(0))),parity max odd
|
||||
EOF
|
||||
diff stdout expected
|
||||
|
||||
autfilt --acceptance-is=parity-min --stats='%g,%[m]g' >stdout <input
|
||||
cat >expected <<EOF
|
||||
Inf(0) | (Fin(1) & (Inf(2) | Fin(3))),parity min even
|
||||
EOF
|
||||
diff stdout expected
|
||||
|
||||
autfilt --acceptance-is=parity-max-even --stats='%g,%[m]g' >stdout <input
|
||||
cat >expected <<EOF
|
||||
Fin(1) & Inf(0),parity max even
|
||||
EOF
|
||||
diff stdout expected
|
||||
|
||||
autfilt --acceptance-is=Streett <input && exit 1
|
||||
|
||||
autfilt --acceptance-is='Fin(1)|Fin(2)&Fin(3)&Fin(0)' --stats='%g,%[s]g' \
|
||||
>stdout <input
|
||||
cat >expected <<EOF
|
||||
Fin(1) | (Fin(2) & Fin(3) & Fin(0)),other
|
||||
EOF
|
||||
diff stdout expected
|
||||
|
||||
autfilt --acceptance-is='Fin(1)|' <input 2>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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue