diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index dc6db1648..b40b07de0 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -79,6 +79,7 @@ Exit status:\n\ #define OPT_SBACC 18 #define OPT_STRIPACC 19 #define OPT_KEEP_STATES 20 +#define OPT_DNF_ACC 21 static const argp_option options[] = { @@ -118,6 +119,8 @@ static const argp_option options[] = { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0, "only keep specified states. The first state will be the new "\ "initial state", 0 }, + { "dnf-acceptance", OPT_DNF_ACC, 0, 0, + "put the acceptance condition in Disjunctive Normal Form", 0 }, /**************************************************/ { 0, 0, 0, 0, "Filtering options:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, @@ -197,6 +200,7 @@ static char opt_instut = 0; static bool opt_is_empty = false; static bool opt_sbacc = false; static bool opt_stripacc = false; +static bool opt_dnf_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 +263,9 @@ parse_opt(int key, char* arg, struct argp_state*) 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; @@ -403,6 +410,9 @@ namespace spot::strip_acceptance_here(aut); if (opt_merge) aut->merge_transitions(); + if (opt_dnf_acc) + aut->set_acceptance(aut->acc().num_sets(), + aut->get_acceptance().to_dnf()); // Filters. diff --git a/src/tgba/acc.cc b/src/tgba/acc.cc index eded9e16c..4bf52a504 100644 --- a/src/tgba/acc.cc +++ b/src/tgba/acc.cc @@ -19,6 +19,7 @@ #include +#include #include "acc.hh" namespace spot @@ -232,6 +233,103 @@ namespace spot return false; } + namespace + { + std::set to_dnf_rec(const acc_cond::acc_word* c) + { + auto sz = c->size; + auto start = c - sz - 1; + auto op = c->op; + std::set res; + switch (op) + { + case acc_cond::acc_op::Or: + { + --c; + do + { + for (auto& i: to_dnf_rec(c)) + res.emplace(std::move(i)); + c -= c->size + 1; + } + while (c > start); + return res; + } + case acc_cond::acc_op::And: + { + std::set old; + // Add true to the set. + res.emplace(acc_cond::acc_code()); + --c; + do + { + old.clear(); + std::swap(res, old); + // AND any element in the set with the DNF of c. + for (auto& i: to_dnf_rec(c)) + for (auto& j: old) + { + auto ac = i; + ac.append_and(j); + res.insert(ac); + } + c -= c->size + 1; + } + while (c > start); + return res; + } + case acc_cond::acc_op::Fin: + { + acc_cond::acc_code w; + w.resize(2); + w[1].op = acc_cond::acc_op::Fin; + w[1].size = 1; + for (auto i: c[-1].mark.sets()) + { + w[0].mark = 0U; + w[0].mark.set(i); + res.insert(w); + } + if (!res.empty()) + return res; + /* fall through to handle false */; + } + case acc_cond::acc_op::Inf: + { + acc_cond::acc_code w; + w.insert(w.begin(), c - 1, c + 1); + return { w }; + } + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::FinNeg: + SPOT_UNREACHABLE(); + return {}; + } + SPOT_UNREACHABLE(); + return {}; + } + } + + acc_cond::acc_code acc_cond::acc_code::to_dnf() const + { + if (empty()) + return *this; + acc_cond::acc_code res; + unsigned count = 0; + for (auto&i : to_dnf_rec(&back())) + { + res.insert(res.end(), i.begin(), i.end()); + ++count; + } + if (count <= 1) + return res; + acc_cond::acc_word w; + w.op = acc_op::Or; + w.size = res.size(); + res.push_back(w); + return res; + } + 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 b00f300b9..8f7a70858 100644 --- a/src/tgba/acc.hh +++ b/src/tgba/acc.hh @@ -209,9 +209,9 @@ namespace spot }; }; - struct acc_code: public std::vector + struct SPOT_API acc_code: public std::vector { - bool operator==(const acc_code& other) + bool operator==(const acc_code& other) const { unsigned pos = size(); if (other.size() != pos) @@ -242,7 +242,67 @@ namespace spot return true; }; - bool operator!=(const acc_code& other) + bool operator<(const acc_code& other) const + { + unsigned pos = size(); + auto osize = other.size(); + if (pos < osize) + return true; + if (pos > osize) + return false; + while (pos > 0) + { + auto op = (*this)[pos - 1].op; + auto oop = other[pos - 1].op; + if (op < oop) + return true; + if (op > oop) + return false; + auto sz = (*this)[pos - 1].size; + auto osz = other[pos - 1].size; + if (sz < osz) + return true; + if (sz > osz) + return false; + switch (op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::FinNeg: + pos -= 2; + auto m = (*this)[pos].mark; + auto om = other[pos].mark; + if (m < om) + return true; + if (m > om) + return false; + break; + } + } + return false; + } + + bool operator>(const acc_code& other) const + { + return other < *this; + } + + bool operator<=(const acc_code& other) const + { + return !(other < *this); + } + + bool operator>=(const acc_code& other) const + { + return !(*this < other); + } + + bool operator!=(const acc_code& other) const { return !(*this == other); } @@ -272,6 +332,97 @@ namespace spot return; unsigned s = size() - 1; unsigned rs = r.size() - 1; + // We want to group all Inf(x) operators: + // Inf(a) & Inf(b) = Inf(a & b) + if (((*this)[s].op == acc_op::Inf && r[rs].op == acc_op::Inf) + || ((*this)[s].op == acc_op::InfNeg && r[rs].op == acc_op::InfNeg)) + { + (*this)[s - 1].mark |= r[rs - 1].mark; + return; + } + + // In the more complex scenarios, left and right may both + // be conjunctions, and Inf(x) might be a member of each + // side. Find it if it exists. + // left_inf points to the left Inf mark if any. + // right_inf points to the right Inf mark if any. + acc_word* left_inf = nullptr; + if ((*this)[s].op == acc_op::And) + { + auto start = &(*this)[s] - (*this)[s].size; + auto pos = &(*this)[s] - 1; + pop_back(); + while (pos > start) + { + if (pos->op == acc_op::Inf) + { + left_inf = pos - 1; + break; + } + pos -= pos->size + 1; + } + } + else if ((*this)[s].op == acc_op::Inf) + { + left_inf = &(*this)[s - 1]; + } + + acc_word* right_inf = nullptr; + auto right_end = &r.back(); + if (right_end->op == acc_op::And) + { + auto start = &r[0]; + auto pos = --right_end; + while (pos > start) + { + if (pos->op == acc_op::Inf) + { + right_inf = pos - 1; + break; + } + pos -= pos->size + 1; + } + } + else if (right_end->op == acc_op::Inf) + { + right_inf = right_end - 1; + } + + if (left_inf && right_inf) + { + left_inf->mark |= right_inf->mark; + insert(this->end(), &r[0], right_inf); + insert(this->end(), right_inf + 2, right_end + 1); + } + else if (right_inf) + { + // Always insert Inf() at the very first entry. + insert(this->begin(), right_inf, right_inf + 2); + insert(this->end(), &r[0], right_inf); + insert(this->end(), right_inf + 2, right_end + 1); + } + else + { + insert(this->end(), &r[0], right_end + 1); + } + + acc_word w; + w.op = acc_op::And; + w.size = size(); + push_back(w); + } + + void append_and(const acc_code& r) + { + if (is_true() || r.is_false()) + { + *this = r; + return; + } + if (is_false() || r.is_true()) + return; + unsigned s = size() - 1; + unsigned rs = r.size() - 1; // Inf(a) & Inf(b) = Inf(a & b) if (((*this)[s].op == acc_op::Inf && r[rs].op == acc_op::Inf) || ((*this)[s].op == acc_op::InfNeg && r[rs].op == acc_op::InfNeg)) @@ -279,9 +430,72 @@ namespace spot (*this)[s - 1].mark |= r[rs - 1].mark; return; } + + // In the more complex scenarios, left and right may both + // be conjunctions, and Inf(x) might be a member of each + // side. Find it if it exists. + // left_inf points to the left Inf mark if any. + // right_inf points to the right Inf mark if any. + acc_word* left_inf = nullptr; if ((*this)[s].op == acc_op::And) - pop_back(); - insert(this->end(), r.begin(), r.end()); + { + auto start = &(*this)[s] - (*this)[s].size; + auto pos = &(*this)[s] - 1; + pop_back(); + while (pos > start) + { + if (pos->op == acc_op::Inf) + { + left_inf = pos - 1; + break; + } + pos -= pos->size + 1; + } + } + else if ((*this)[s].op == acc_op::Inf) + { + left_inf = &(*this)[s - 1]; + } + + const acc_word* right_inf = nullptr; + auto right_end = &r.back(); + if (right_end->op == acc_op::And) + { + auto start = &r[0]; + auto pos = --right_end; + while (pos > start) + { + if (pos->op == acc_op::Inf) + { + right_inf = pos - 1; + break; + } + pos -= pos->size + 1; + } + } + else if (right_end->op == acc_op::Inf) + { + right_inf = right_end - 1; + } + + if (left_inf && right_inf) + { + left_inf->mark |= right_inf->mark; + insert(this->end(), &r[0], right_inf); + insert(this->end(), right_inf + 2, right_end + 1); + } + else if (right_inf) + { + // Always insert Inf() at the very first entry. + insert(this->begin(), right_inf, right_inf + 2); + insert(this->end(), &r[0], right_inf); + insert(this->end(), right_inf + 2, right_end + 1); + } + else + { + insert(this->end(), &r[0], right_end + 1); + } + acc_word w; w.op = acc_op::And; w.size = size(); @@ -308,6 +522,8 @@ namespace spot } if ((*this)[s].op == acc_op::Or) pop_back(); + if (r.back().op == acc_op::Or) + r.pop_back(); insert(this->end(), r.begin(), r.end()); acc_word w; w.op = acc_op::Or; @@ -340,6 +556,8 @@ namespace spot while (pos > 0); } + acc_code to_dnf() 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 e367882d1..af6505ff6 100755 --- a/src/tgbatest/acc2.test +++ b/src/tgbatest/acc2.test @@ -29,3 +29,42 @@ grep 'Acceptance:' in > expected ../../bin/autfilt -H in --stats='Acceptance: %A %G' > out2 diff out1 expected diff out2 expected + +cat >header <body <acceptances< output + +diff acceptances output