acc: add a to_dnf() method
* src/tgba/acc.cc, src/tgba/acc.hh: Implement a to_dnf() method. * src/bin/autfilt.cc: Add option --dnf-acceptance. * src/tgbatest/acc2.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz
parent
de586dd2f0
commit
1441c4fe34
4 changed files with 370 additions and 5 deletions
|
|
@ -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<bool> 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.
|
||||
|
||||
|
|
|
|||
|
|
@ -19,6 +19,7 @@
|
|||
|
||||
|
||||
#include <iostream>
|
||||
#include <set>
|
||||
#include "acc.hh"
|
||||
|
||||
namespace spot
|
||||
|
|
@ -232,6 +233,103 @@ namespace spot
|
|||
return false;
|
||||
}
|
||||
|
||||
namespace
|
||||
{
|
||||
std::set<acc_cond::acc_code> to_dnf_rec(const acc_cond::acc_word* c)
|
||||
{
|
||||
auto sz = c->size;
|
||||
auto start = c - sz - 1;
|
||||
auto op = c->op;
|
||||
std::set<acc_cond::acc_code> 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<acc_cond::acc_code> 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)
|
||||
{
|
||||
|
|
|
|||
226
src/tgba/acc.hh
226
src/tgba/acc.hh
|
|
@ -209,9 +209,9 @@ namespace spot
|
|||
};
|
||||
};
|
||||
|
||||
struct acc_code: public std::vector<acc_word>
|
||||
struct SPOT_API acc_code: public std::vector<acc_word>
|
||||
{
|
||||
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,7 @@ 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))
|
||||
|
|
@ -279,9 +340,162 @@ 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)
|
||||
{
|
||||
auto start = &(*this)[s] - (*this)[s].size;
|
||||
auto pos = &(*this)[s] - 1;
|
||||
pop_back();
|
||||
insert(this->end(), r.begin(), r.end());
|
||||
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))
|
||||
{
|
||||
(*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];
|
||||
}
|
||||
|
||||
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);
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
EOF
|
||||
|
||||
cat >body <<EOF
|
||||
--BODY--
|
||||
State: 0
|
||||
[0&1] 0 {0 1}
|
||||
[!0&!1] 0
|
||||
[!0&1] 0 {1}
|
||||
[0&!1] 0 {0}
|
||||
--END--
|
||||
EOF
|
||||
|
||||
|
||||
res="(Fin(2) & Fin(1) & Inf(0)) | (Fin(2) & (Inf(0)&Inf(3)))"
|
||||
res="$res | (Fin(1) & (Inf(0)&Inf(1))) | (Inf(0)&Inf(1)&Inf(3))"
|
||||
cat >acceptances<<EOF
|
||||
2 Inf(0)&Inf(1), 2 Inf(0)&Inf(1)
|
||||
2 Fin(0) & Inf(1), 2 Fin(0) & Inf(1)
|
||||
2 t, 2 t
|
||||
2 f, 2 f
|
||||
3 (Inf(1) | Fin(2)) & Inf(0), 3 (Fin(2) & Inf(0)) | (Inf(0)&Inf(1))
|
||||
4 (Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0), 4 $res
|
||||
4 $res, 4 $res
|
||||
3 (Fin(0)|Fin(1)) & Fin(2), 3 (Fin(1) & Fin(2)) | (Fin(0) & Fin(2))
|
||||
EOF
|
||||
|
||||
while IFS=, read a b
|
||||
do
|
||||
(cat header; echo 'Acceptance:' $a; cat body) |
|
||||
../../bin/autfilt -H --dnf-acc --stats '%A %G, %a %g'
|
||||
done < acceptances > output
|
||||
|
||||
diff acceptances output
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue