From d597050f6d1301678f6e79b53aba90df11857f0d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 24 Feb 2015 21:50:00 +0100 Subject: [PATCH] Make it easy to complement an acceptance condition * src/tgba/acc.cc, src/tgba/acc.hh (complement): New method. * src/bin/autfilt.cc: Add a --complement-acceptance option. * src/tgbatest/acc2.test: Test it. --- src/bin/autfilt.cc | 33 ++++++++++++------ src/tgba/acc.cc | 78 ++++++++++++++++++++++++++++++++++++++++++ src/tgba/acc.hh | 2 ++ src/tgbatest/acc2.test | 21 ++++++++++++ 4 files changed, 123 insertions(+), 11 deletions(-) diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 336d66828..c0cceb70d 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -84,6 +84,7 @@ Exit status:\n\ #define OPT_DNF_ACC 21 #define OPT_REM_FIN 22 #define OPT_CLEAN_ACC 23 +#define OPT_COMPLEMENT_ACC 24 static const argp_option options[] = { @@ -119,7 +120,7 @@ static const argp_option options[] = "define the acceptance using states", 0 }, { "sbacc", 0, 0, OPTION_ALIAS, 0, 0 }, { "strip-acceptance", OPT_STRIPACC, 0, 0, - "remove the acceptance conditions and all acceptance sets", 0 }, + "remove the acceptance condition and all acceptance sets", 0 }, { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0, "only keep specified states. The first state will be the new "\ "initial state", 0 }, @@ -129,6 +130,9 @@ static const argp_option options[] = "rewrite the automaton without using Fin acceptance", 0 }, { "cleanup-acceptance", OPT_CLEAN_ACC, 0, 0, "remove unused acceptance sets from the automaton", 0 }, + { "complement-acceptance", OPT_COMPLEMENT_ACC, 0, 0, + "complement the acceptance condition (without touching the automaton)", + 0 }, /**************************************************/ { 0, 0, 0, 0, "Filtering options:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, @@ -211,6 +215,7 @@ static bool opt_stripacc = false; static bool opt_dnf_acc = false; static bool opt_rem_fin = false; static bool opt_clean_acc = false; +static bool opt_complement_acc = false; static spot::acc_cond::mark_t opt_mask_acc = 0U; static std::vector opt_keep_states = {}; static unsigned int opt_keep_states_initial = 0; @@ -259,6 +264,15 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_CLEAN_ACC: opt_clean_acc = true; break; + case OPT_COMPLEMENT_ACC: + opt_complement_acc = true; + break; + case OPT_DESTUT: + opt_destut = true; + break; + case OPT_DNF_ACC: + opt_dnf_acc = true; + break; case OPT_EDGES: opt_edges = parse_range(arg, 0, std::numeric_limits::max()); break; @@ -273,12 +287,6 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_INTERSECT: opt->intersect = read_automaton(arg, opt->dict); break; - case OPT_DESTUT: - opt_destut = true; - break; - case OPT_DNF_ACC: - opt_dnf_acc = true; - break; case OPT_IS_COMPLETE: opt_is_complete = true; break; @@ -426,13 +434,16 @@ namespace spot::strip_acceptance_here(aut); if (opt_merge) aut->merge_transitions(); + if (opt_clean_acc || opt_rem_fin) + cleanup_acceptance(aut); + if (opt_complement_acc) + aut->set_acceptance(aut->acc().num_sets(), + aut->get_acceptance().complement()); + if (opt_rem_fin) + aut = remove_fin(aut); if (opt_dnf_acc) aut->set_acceptance(aut->acc().num_sets(), aut->get_acceptance().to_dnf()); - if (opt_clean_acc && !opt_rem_fin) - cleanup_acceptance(aut); - if (opt_rem_fin) - aut = remove_fin(aut); // Filters. diff --git a/src/tgba/acc.cc b/src/tgba/acc.cc index 54a8060f3..c33591a1f 100644 --- a/src/tgba/acc.cc +++ b/src/tgba/acc.cc @@ -353,6 +353,84 @@ namespace spot return true; } + namespace + { + acc_cond::acc_code complement_rec(const acc_cond::acc_word* pos) + { + auto start = pos - pos->size; + + acc_cond::acc_code res; + res.resize(2); + res[0].mark = 0U; + res[1].size = 1; + + switch (pos->op) + { + case acc_cond::acc_op::And: + { + --pos; + res[1].op = acc_cond::acc_op::Fin; // f + do + { + auto tmp = complement_rec(pos); + tmp.append_or(std::move(res)); + std::swap(tmp, res); + pos -= pos->size + 1; + } + while (pos > start); + return res; + } + case acc_cond::acc_op::Or: + { + --pos; + res[1].op = acc_cond::acc_op::Inf; // t + do + { + auto tmp = complement_rec(pos); + tmp.append_and(std::move(res)); + std::swap(tmp, res); + pos -= pos->size + 1; + } + while (pos > start); + return res; + } + case acc_cond::acc_op::Fin: + res[0].mark = pos[-1].mark; + res[1].op = acc_cond::acc_op::Inf; + return res; + case acc_cond::acc_op::Inf: + res[0].mark = pos[-1].mark; + res[1].op = acc_cond::acc_op::Fin; + return res; + case acc_cond::acc_op::FinNeg: + res[0].mark = pos[-1].mark; + res[1].op = acc_cond::acc_op::InfNeg; + return res; + case acc_cond::acc_op::InfNeg: + res[0].mark = pos[-1].mark; + res[1].op = acc_cond::acc_op::FinNeg; + return res; + } + SPOT_UNREACHABLE(); + return acc_cond::acc_code{}; + } + + } + + + acc_cond::acc_code acc_cond::acc_code::complement() const + { + if (empty()) + { + acc_cond::acc_code res; + res.resize(2); + res[0].mark = 0U; + res[1].op = acc_cond::acc_op::Fin; + res[1].size = 1; + return res; + } + return complement_rec(&back()); + } std::ostream& operator<<(std::ostream& os, const spot::acc_cond::acc_code& code) diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh index 596fa8de0..4a6f3fc3a 100644 --- a/src/tgba/acc.hh +++ b/src/tgba/acc.hh @@ -560,6 +560,8 @@ namespace spot acc_code to_dnf() const; + acc_code complement() const; + SPOT_API friend std::ostream& operator<<(std::ostream& os, const acc_code& code); }; diff --git a/src/tgbatest/acc2.test b/src/tgbatest/acc2.test index af6505ff6..a2e7e9ff5 100755 --- a/src/tgbatest/acc2.test +++ b/src/tgbatest/acc2.test @@ -68,3 +68,24 @@ do done < acceptances > output diff acceptances output + +a="(Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0)" +b="(Fin(1) & Inf(2)) | (Fin(3) & Inf(1)) | Fin(0)" +cat >acceptances< output + +diff acceptances output