alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

acc: refactor strip() routines

Browse source 
* src/tgba/acc.cc, src/tgba/acc.hh: Move the strip() routine from
acc_cond into acc_cond::mark_t, and the strip() routine from
cleanacc.cc into acc_cond::acc_code.  Introduce helper functions
to create inf()/fin()/t()/f() at the acc_code level.
* src/tgbaalgos/cleanacc.cc: Simplify, using the strip() function
from acc_code.
* src/tgbaalgos/mask.cc (mask_acc_sets): Use the strip() function
from acc_code so that it work on non-Buchi acceptance.
* src/tgbatest/maskacc.test: Add a test for the latter change.
* src/tgbaalgos/sccfilter.cc, src/tgbatest/acc.cc: Adjust the
use mark_t::strip().
This commit is contained in:
Alexandre Duret-Lutz 2015-02-25 22:36:13 +01:00
parent 717c857794
commit 5b2c7b55ed
7 changed files with 267 additions and 165 deletions
Download patch file Download diff file Expand all files Collapse all files

129
src/tgba/acc.cc
View file

@ -414,18 +414,12 @@ namespace spot
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
auto res = acc_cond::acc_code::f();
do
{
auto tmp = complement_rec(pos);
@ -439,7 +433,7 @@ namespace spot
case acc_cond::acc_op::Or:
{
--pos;
res[1].op = acc_cond::acc_op::Inf; // t
auto res = acc_cond::acc_code::t();
do
{
auto tmp = complement_rec(pos);
@ -451,24 +445,16 @@ namespace spot
return res;
}
case acc_cond::acc_op::Fin:
res[0].mark = pos[-1].mark;
res[1].op = acc_cond::acc_op::Inf;
return res;
return acc_cond::acc_code::inf(pos[-1].mark);
case acc_cond::acc_op::Inf:
res[0].mark = pos[-1].mark;
res[1].op = acc_cond::acc_op::Fin;
return res;
return acc_cond::acc_code::fin(pos[-1].mark);
case acc_cond::acc_op::FinNeg:
res[0].mark = pos[-1].mark;
res[1].op = acc_cond::acc_op::InfNeg;
return res;
return acc_cond::acc_code::inf_neg(pos[-1].mark);
case acc_cond::acc_op::InfNeg:
res[0].mark = pos[-1].mark;
res[1].op = acc_cond::acc_op::FinNeg;
return res;
return acc_cond::acc_code::fin_neg(pos[-1].mark);
}
SPOT_UNREACHABLE();
return acc_cond::acc_code{};
return {};
}
}
@ -476,18 +462,101 @@ namespace spot
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;
}
if (is_true())
return acc_cond::acc_code::f();
return complement_rec(&back());
}
namespace
{
static acc_cond::acc_code
strip_rec(const acc_cond::acc_word* pos, acc_cond::mark_t rem, bool missing)
{
auto start = pos - pos->size;
switch (pos->op)
{
case acc_cond::acc_op::And:
{
--pos;
auto res = acc_cond::acc_code::t();
do
{
auto tmp = strip_rec(pos, rem, missing);
tmp.append_and(std::move(res));
std::swap(tmp, res);
pos -= pos->size + 1;
}
while (pos > start);
return res;
}
case acc_cond::acc_op::Or:
{
--pos;
auto res = acc_cond::acc_code::f();
do
{
auto tmp = strip_rec(pos, rem, missing);
tmp.append_or(std::move(res));
std::swap(tmp, res);
pos -= pos->size + 1;
}
while (pos > start);
return res;
}
case acc_cond::acc_op::Fin:
if (missing && (pos[-1].mark & rem))
return acc_cond::acc_code::t();
return acc_cond::acc_code::fin(pos[-1].mark.strip(rem));
case acc_cond::acc_op::Inf:
if (missing && (pos[-1].mark & rem))
return acc_cond::acc_code::f();
return acc_cond::acc_code::inf(pos[-1].mark.strip(rem));
case acc_cond::acc_op::FinNeg:
case acc_cond::acc_op::InfNeg:
SPOT_UNREACHABLE();
return {};
}
SPOT_UNREACHABLE();
return {};
}
}
acc_cond::acc_code
acc_cond::acc_code::strip(acc_cond::mark_t rem, bool missing) const
{
if (is_true() || is_false())
return *this;
return strip_rec(&back(), rem, missing);
}
acc_cond::mark_t
acc_cond::acc_code::used_sets() const
{
if (is_true() || is_false())
return 0U;
acc_cond::mark_t used_in_cond = 0U;
auto pos = &back();
auto end = &front();
while (pos > end)
{
switch (pos->op)
{
case acc_cond::acc_op::And:
case acc_cond::acc_op::Or:
--pos;
break;
case acc_cond::acc_op::Fin:
case acc_cond::acc_op::Inf:
case acc_cond::acc_op::FinNeg:
case acc_cond::acc_op::InfNeg:
used_in_cond |= pos[-1].mark;
pos -= 2;
break;
}
}
return used_in_cond;
}
std::ostream& operator<<(std::ostream& os,
const spot::acc_cond::acc_code& code)
{

153
src/tgba/acc.hh
View file

@ -145,6 +145,29 @@ namespace spot
return id ^ r.id;
}
mark_t strip(mark_t y) const
{
// strip every bit of id that is marked in y
// 100101110100.strip(
// 001011001000)
// == 10 1 11 100
// == 10111100
auto xv = id; // 100101110100
auto yv = y.id; // 001011001000
while (yv && xv)
{
// Mask for everything after the last 1 in y
auto rm = (~yv) & (yv - 1); // 000000000111
// Mask for everything before the last 1 in y
auto lm = ~(yv ^ (yv - 1)); // 111111110000
xv = ((xv & lm) >> 1) | (xv & rm);
yv = (yv & lm) >> 1;
}
return xv;
}
// Number of bits sets.
unsigned count() const
{
@ -321,6 +344,61 @@ namespace spot
&& (*this)[s - 1].op == acc_op::Fin && (*this)[s - 2].mark == 0U;
}
static acc_code f()
{
acc_code res;
res.resize(2);
res[0].mark = 0U;
res[1].op = acc_op::Fin;
res[1].size = 1;
return res;
}
static acc_code t()
{
return {};
}
static acc_code fin(mark_t m)
{
acc_code res;
res.resize(2);
res[0].mark = m;
res[1].op = acc_op::Fin;
res[1].size = 1;
return res;
}
static acc_code fin_neg(mark_t m)
{
acc_code res;
res.resize(2);
res[0].mark = m;
res[1].op = acc_op::FinNeg;
res[1].size = 1;
return res;
}
static acc_code inf(mark_t m)
{
acc_code res;
res.resize(2);
res[0].mark = m;
res[1].op = acc_op::Inf;
res[1].size = 1;
return res;
}
static acc_code inf_neg(mark_t m)
{
acc_code res;
res.resize(2);
res[0].mark = m;
res[1].op = acc_op::InfNeg;
res[1].size = 1;
return res;
}
void append_and(acc_code&& r)
{
if (is_true() || r.is_false())
@ -562,6 +640,24 @@ namespace spot
acc_code complement() const;
// Remove all the acceptance sets in rem.
//
// If MISSING is set, the acceptance sets are assumed to be
// missing from the automaton, and the acceptance is updated to
// reflect this. For instance (Inf(1)&Inf(2))|Fin(3) will
// become Fin(3) if we remove 2 because it is missing from this
// automaton, because there is no way to fulfill Inf(1)&Inf(2)
// in this case. So essentially MISSING causes Inf(rem) to
// become f, and Fin(rem) to become t.
//
// If MISSING is unset, Inf(rem) become t while Fin(rem) become
// f. Removing 2 from (Inf(1)&Inf(2))|Fin(3) would then give
// Inf(1)|Fin(3).
acc_code strip(acc_cond::mark_t rem, bool missing) const;
// Return the set of sets appearing in the condition.
acc_cond::mark_t used_sets() const;
SPOT_API
friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
};
@ -609,26 +705,25 @@ namespace spot
(s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets());
}
bool is_buchi() const
{
unsigned s = code_.size();
return num_ == 1 &&
s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets();
}
bool is_true() const
{
return code_.is_true();
}
protected:
bool check_fin_acceptance() const;
acc_code primitive(mark_t mark, acc_op op) const
{
acc_word w1;
w1.mark = mark;
acc_word w2;
w2.op = op;
w2.size = 1;
acc_code c;
c.push_back(w1);
c.push_back(w2);
return c;
}
public:
acc_code inf(mark_t mark) const
{
return primitive(mark, acc_op::Inf);
return acc_code::inf(mark);
}
acc_code inf(std::initializer_list<unsigned> vals) const
@ -638,7 +733,7 @@ namespace spot
acc_code inf_neg(mark_t mark) const
{
return primitive(mark, acc_op::InfNeg);
return acc_code::inf_neg(mark);
}
acc_code inf_neg(std::initializer_list<unsigned> vals) const
@ -648,7 +743,7 @@ namespace spot
acc_code fin(mark_t mark) const
{
return primitive(mark, acc_op::Fin);
return acc_code::fin(mark);
}
acc_code fin(std::initializer_list<unsigned> vals) const
@ -658,7 +753,7 @@ namespace spot
acc_code fin_neg(mark_t mark) const
{
return primitive(mark, acc_op::FinNeg);
return acc_code::fin_neg(mark);
}
acc_code fin_neg(std::initializer_list<unsigned> vals) const
@ -795,30 +890,6 @@ namespace spot
return u;
}
mark_t strip(mark_t x, mark_t y) const
{
// strip every bit of x that is marked in y
// strip(100101110100,
// 001011001000)
// == 10 1 11 100
// == 10111100
auto xv = x.id; // 100101110100
auto yv = y.id; // 001011001000
while (yv && xv)
{
// Mask for everything after the last 1 in y
auto rm = (~yv) & (yv - 1); // 000000000111
// Mask for everything before the last 1 in y
auto lm = ~(yv ^ (yv - 1)); // 111111110000
xv = ((xv & lm) >> 1) | (xv & rm);
yv = (yv & lm) >> 1;
}
return xv;
}
protected:
mark_t::value_t mark_(unsigned u) const
{

89
src/tgbaalgos/cleanacc.cc
View file

@ -21,61 +21,6 @@
namespace spot
{
namespace
{
acc_cond::acc_code strip(const acc_cond& acc,
const acc_cond::acc_word* pos,
acc_cond::mark_t useless)
{
auto start = pos - pos->size;
switch (pos->op)
{
case acc_cond::acc_op::And:
{
--pos;
acc_cond::acc_code res;
do
{
auto tmp = strip(acc, pos, useless);
tmp.append_and(std::move(res));
std::swap(tmp, res);
pos -= pos->size + 1;
}
while (pos > start);
return res;
}
case acc_cond::acc_op::Or:
{
--pos;
acc_cond::acc_code res = acc.fin(0); // f
do
{
auto tmp = strip(acc, pos, useless);
tmp.append_or(std::move(res));
std::swap(tmp, res);
pos -= pos->size + 1;
}
while (pos > start);
return res;
}
case acc_cond::acc_op::Fin:
if (pos[-1].mark & useless)
return acc.inf(0U); // t
return acc.fin(acc.strip(pos[-1].mark, useless));
case acc_cond::acc_op::Inf:
if (pos[-1].mark & useless)
return acc.fin(0U); // f
return acc.inf(acc.strip(pos[-1].mark, useless));
case acc_cond::acc_op::FinNeg:
case acc_cond::acc_op::InfNeg:
SPOT_UNREACHABLE();
return acc_cond::acc_code{};
}
SPOT_UNREACHABLE();
return acc_cond::acc_code{};
}
}
void cleanup_acceptance(tgba_digraph_ptr& aut)
{
auto& acc = aut->acc();
@ -83,29 +28,7 @@ namespace spot
return;
auto& c = aut->get_acceptance();
acc_cond::mark_t used_in_cond = 0U;
if (!c.is_true())
{
auto pos = &c.back();
auto end = &c.front();
while (pos > end)
{
switch (pos->op)
{
case acc_cond::acc_op::And:
case acc_cond::acc_op::Or:
--pos;
break;
case acc_cond::acc_op::Fin:
case acc_cond::acc_op::Inf:
case acc_cond::acc_op::FinNeg:
case acc_cond::acc_op::InfNeg:
used_in_cond |= pos[-1].mark;
pos -= 2;
break;
}
}
}
acc_cond::mark_t used_in_cond = c.used_sets();
acc_cond::mark_t used_in_aut = 0U;
for (auto& t: aut->transitions())
@ -120,16 +43,10 @@ namespace spot
// Remove useless marks from the automaton
for (auto& t: aut->transitions())
t.acc = acc.strip(t.acc, useless);
t.acc = t.acc.strip(useless);
// Remove useless marks from the acceptance condition
acc_cond::acc_code newc;
if (c.is_true() || c.is_false())
newc = c;
else
newc = strip(acc, &c.back(), useless);
aut->set_acceptance(useful.count(), newc);
aut->set_acceptance(useful.count(), c.strip(useless, true));
}
}

8
src/tgbaalgos/mask.cc
View file

@ -24,14 +24,14 @@ namespace spot
tgba_digraph_ptr mask_acc_sets(const const_tgba_digraph_ptr& in,
acc_cond::mark_t to_remove)
{
auto& inacc = in->acc();
auto res = make_tgba_digraph(in->get_dict());
res->copy_ap_of(in);
res->prop_copy(in, { true, false, true, true });
unsigned na = inacc.num_sets();
unsigned na = in->acc().num_sets();
unsigned tr = to_remove.count();
assert(tr <= na);
res->set_generalized_buchi(na - tr);
res->set_acceptance(na - tr,
in->get_acceptance().strip(to_remove, false));
transform_accessible(in, res, [&](unsigned,
bdd& cond,
acc_cond::mark_t& acc,
@ -40,7 +40,7 @@ namespace spot
if (acc & to_remove)
cond = bddfalse;
else
acc = inacc.strip(acc, to_remove);
acc = acc.strip(to_remove);
});
return res;
}

6
src/tgbaalgos/sccfilter.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
// de Recherche et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -240,7 +240,7 @@ namespace spot
if (!this->si->is_accepting_scc(u))
acc = 0U;
else
acc = this->si->get_aut()->acc().strip(acc, strip_[u]);
acc = acc.strip(strip_[u]);
}
return filtered_trans{keep, cond, acc};
}

2
src/tgbatest/acc.cc
View file

@ -103,7 +103,7 @@ int main()
for (auto& v: s)
{
check(ac, v);
check(ac, ac.strip(v, u));
check(ac, v.strip(u));
}

45
src/tgbatest/maskacc.test
View file

@ -111,6 +111,51 @@ diff output expect3
run 0 ../../bin/autfilt --mask-acc=0 --mask-acc=1 input1 -H >output
diff output expect3
cat >input4 <<EOF
HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
Acceptance: 3 Inf(1)|Fin(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 1 {0}
[1] 2 {1}
State: 1
[0] 2
[0] 3 {1}
State: 2
[1] 1
[1] 3 {0}
State: 3
[0] 3 {0 1}
--END--
EOF
cat >expect4 <<EOF
HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[1] 1 {0}
State: 1
[1] 2
State: 2
[0] 1
[0] 3 {0}
State: 3
--END--
EOF
run 0 ../../bin/autfilt --mask-acc=0 input4 -H >output
diff output expect4
# Errors
run 2 ../../bin/autfilt --mask-acc=a3 input1
run 2 ../../bin/autfilt --mask-acc=3-2 input1