From a0ac8dc512e69b338f8c6af0dbb4a9d0ba0bb080 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 Mar 2015 09:13:08 +0100 Subject: [PATCH] acc: add a to_cnf() function * src/tgba/acc.cc, src/tgba/acc.hh (to_cnf, is_cnf): New functions. * src/bin/autfilt.cc: Add a --cnf-acceptance option. * src/tgbatest/acc2.test: Test it. --- src/bin/autfilt.cc | 12 +++++ src/tgba/acc.cc | 105 ++++++++++++++++++++++++++++++++++++++++- src/tgba/acc.hh | 2 + src/tgbatest/acc2.test | 25 ++++++++++ 4 files changed, 143 insertions(+), 1 deletion(-) diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index d889a347c..59aa408cd 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -65,6 +65,7 @@ enum { OPT_ACC_SETS = 256, OPT_ARE_ISOMORPHIC, OPT_CLEAN_ACC, + OPT_CNF_ACC, OPT_COMPLEMENT_ACC, OPT_COUNT, OPT_DESTUT, @@ -128,6 +129,8 @@ static const argp_option options[] = "initial state", 0 }, { "dnf-acceptance", OPT_DNF_ACC, 0, 0, "put the acceptance condition in Disjunctive Normal Form", 0 }, + { "cnf-acceptance", OPT_CNF_ACC, 0, 0, + "put the acceptance condition in Conjunctive Normal Form", 0 }, { "remove-fin", OPT_REM_FIN, 0, 0, "rewrite the automaton without using Fin acceptance", 0 }, { "cleanup-acceptance", OPT_CLEAN_ACC, 0, 0, @@ -215,6 +218,7 @@ static bool opt_is_empty = false; static bool opt_sbacc = false; static bool opt_stripacc = false; static bool opt_dnf_acc = false; +static bool opt_cnf_acc = false; static bool opt_rem_fin = false; static bool opt_clean_acc = false; static bool opt_complement_acc = false; @@ -266,6 +270,10 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_CLEAN_ACC: opt_clean_acc = true; break; + case OPT_CNF_ACC: + opt_dnf_acc = false; + opt_cnf_acc = true; + break; case OPT_COMPLEMENT_ACC: opt_complement_acc = true; break; @@ -274,6 +282,7 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_DNF_ACC: opt_dnf_acc = true; + opt_cnf_acc = false; break; case OPT_EDGES: opt_edges = parse_range(arg, 0, std::numeric_limits::max()); @@ -446,6 +455,9 @@ namespace if (opt_dnf_acc) aut->set_acceptance(aut->acc().num_sets(), aut->get_acceptance().to_dnf()); + if (opt_cnf_acc) + aut->set_acceptance(aut->acc().num_sets(), + aut->get_acceptance().to_cnf()); // Filters. diff --git a/src/tgba/acc.cc b/src/tgba/acc.cc index 1382e8ec4..6f7de2b68 100644 --- a/src/tgba/acc.cc +++ b/src/tgba/acc.cc @@ -394,7 +394,7 @@ namespace spot acc_cond::acc_code acc_cond::acc_code::to_dnf() const { - if (empty()) + if (empty() || size() == 2) return *this; auto used = acc_cond::acc_code::used_sets(); @@ -462,6 +462,76 @@ namespace spot return rescode; } + acc_cond::acc_code acc_cond::acc_code::to_cnf() const + { + if (empty() || size() == 2) + return *this; + + auto used = acc_cond::acc_code::used_sets(); + unsigned c = used.count(); + + bdd_allocator ba; + int base = ba.allocate_variables(c); + std::vector r; + std::vector sets(c); + for (unsigned i = 0; r.size() < c; ++i) + { + if (used.has(i)) + { + sets[base] = i; + r.push_back(bdd_ithvar(base++)); + } + else + { + r.push_back(bddfalse); + } + } + + bdd res = to_bdd_rec(&back(), &r[0]); + + if (res == bddtrue) + return t(); + if (res == bddfalse) + return f(); + + minato_isop isop(!res); + bdd cube; + acc_code rescode; + while ((cube = isop.next()) != bddfalse) + { + mark_t m = 0U; + acc_code c = f(); + while (cube != bddtrue) + { + // The acceptance set associated to this BDD variable + mark_t s = 0U; + s.set(sets[bdd_var(cube)]); + + bdd h = bdd_high(cube); + if (h == bddfalse) // Negative variable? -> Inf + { + cube = bdd_low(cube); + // The strange order here make sure we can smaller set + // numbers at the end of the acceptance code, i.e., at + // the front of the output. + auto a = inf(s); + a.append_or(std::move(c)); + std::swap(a, c); + } + else // Positive variable? -> Fin + { + m |= s; + cube = h; + } + } + c.append_or(fin(m)); + // See comment above for the order. + c.append_and(std::move(rescode)); + std::swap(c, rescode); + } + return rescode; + } + bool acc_cond::acc_code::is_dnf() const { if (empty() || size() == 2) @@ -495,6 +565,39 @@ namespace spot return true; } + bool acc_cond::acc_code::is_cnf() const + { + if (empty() || size() == 2) + return true; + auto pos = &back(); + auto start = &front(); + auto or_scope = pos + 1; + if (pos->op == acc_cond::acc_op::And) + --pos; + while (pos > start) + { + switch (pos->op) + { + case acc_cond::acc_op::And: + return false; + case acc_cond::acc_op::Or: + or_scope = std::min(or_scope, pos - pos->size); + --pos; + break; + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + if (pos[-1].mark.count() > 1 && pos > or_scope) + return false; + /* fall through */ + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::FinNeg: + pos -= 2; + break; + } + } + return true; + } + namespace { acc_cond::acc_code complement_rec(const acc_cond::acc_word* pos) diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh index 3e6734b64..d9fbad119 100644 --- a/src/tgba/acc.hh +++ b/src/tgba/acc.hh @@ -635,8 +635,10 @@ namespace spot } bool is_dnf() const; + bool is_cnf() const; acc_code to_dnf() const; + acc_code to_cnf() const; acc_code complement() const; diff --git a/src/tgbatest/acc2.test b/src/tgbatest/acc2.test index af3d559d7..42b7a008d 100755 --- a/src/tgbatest/acc2.test +++ b/src/tgbatest/acc2.test @@ -47,6 +47,7 @@ State: 0 --END-- EOF +#------------- DNF ------------- res="(Fin(1) & Fin(2) & Inf(0)) | (Inf(0)&Inf(1)&Inf(3))" cat >acceptances< output diff acceptances output +#------------- CNF ------------- + +res="(Fin(2) | Inf(1)) & (Fin(1) | Inf(3)) & Inf(0)" +cat >acceptances< output + +diff acceptances output + +#------------- COMP ------------- + a="(Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0)" b="(Fin(1) & Inf(2)) | (Fin(3) & Inf(1)) | Fin(0)" cat >acceptances<