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

cleanacc: keep acceptance order when removing complementary colors

Browse source 
* spot/twaalgos/cleanacc.cc (remove_compl_rec): Rewrite to preserve
the original order of the acceptance condition while rewriting it.
* tests/core/sccdot.test, tests/python/merge.py,
tests/python/simplacc.py, tests/python/toparity.py: Adjust test cases.
This commit is contained in:
Alexandre Duret-Lutz 2020-04-18 22:05:43 +02:00
parent 262b24e6d7
commit c0e1b3e52a
5 changed files with 109 additions and 108 deletions
Download patch file Download diff file Expand all files Collapse all files

140
spot/twaalgos/cleanacc.cc
View file

@ -157,101 +157,99 @@ namespace spot
return aut;
}
// Eventually remove complementary marks from the acceptance condition.
// Remove complementary marks from the acceptance condition.
acc_cond::acc_code remove_compl_rec(const acc_cond::acc_word* pos,
const std::vector<acc_cond::mark_t>&
complement)
{
auto start = pos - pos->sub.size;
switch (pos->sub.op)
{
case acc_cond::acc_op::And:
auto boolop =
[&](acc_cond::acc_op opand, acc_cond::acc_op opfin,
acc_cond::acc_op opinf,
acc_cond::acc_code&& truecode,
acc_cond::acc_code&& falsecode)
{
--pos;
auto res = acc_cond::acc_code::t();
acc_cond::acc_code res = truecode;
acc_cond::mark_t seen_fin = {};
auto inf = acc_cond::acc_code::inf({});
do
{
auto tmp = remove_compl_rec(pos, complement);
if (!tmp.empty())
{
if (tmp.back().sub.op == acc_cond::acc_op::Fin
&& tmp.front().mark.count() == 1)
if (!tmp.empty() && (tmp.back().sub.op == opfin
&& tmp.front().mark.count() == 1))
seen_fin |= tmp.front().mark;
if (tmp.back().sub.op == acc_cond::acc_op::Inf)
{
inf &= std::move(tmp);
pos -= pos->sub.size + 1;
continue;
}
}
if (opand == acc_cond::acc_op::And)
tmp &= std::move(res);
std::swap(tmp, res);
pos -= pos->sub.size + 1;
}
while (pos > start);
// Fin(i) & Inf(i) = f;
if (inf.front().mark & seen_fin)
return acc_cond::acc_code::f();
for (auto m: seen_fin.sets())
{
acc_cond::mark_t cm = complement[m];
// Fin(i) & Fin(!i) = f;
if (cm & seen_fin)
return acc_cond::acc_code::f();
// Inf({!i}) & Fin({i}) = Fin({i})
inf.front().mark -= complement[m];
}
return inf & res;
}
case acc_cond::acc_op::Or:
{
--pos;
auto res = acc_cond::acc_code::f();
acc_cond::mark_t seen_inf = {};
auto fin = acc_cond::acc_code::f();
do
{
auto tmp = remove_compl_rec(pos, complement);
if (!tmp.empty())
{
if (tmp.back().sub.op == acc_cond::acc_op::Inf
&& tmp.front().mark.count() == 1)
seen_inf |= tmp.front().mark;
if (tmp.back().sub.op == acc_cond::acc_op::Fin)
{
fin |= std::move(tmp);
pos -= pos->sub.size + 1;
continue;
}
}
else
tmp |= std::move(res);
std::swap(tmp, res);
pos -= pos->sub.size + 1;
}
while (pos > start);
// Fin(i) | Inf(i) = t;
if (fin.front().mark & seen_inf)
return acc_cond::acc_code::t();
for (auto m: seen_inf.sets())
if (res.empty() || res.back().sub.op != opand)
return res;
// Locate the position of any Inf element.
// A property of the &= operator is that there
// is only one Inf in a conjunction.
auto rbegin = &res.back();
auto rend = rbegin - rbegin->sub.size;
--rbegin;
do
{
if (rbegin->sub.op == opinf)
break;
rbegin -= rbegin->sub.size + 1;
}
while (rbegin > rend);
if (rbegin <= rend)
return res;
// Fin(i) & Inf(i) = f;
if (rbegin[-1].mark & seen_fin)
return std::move(falsecode);
for (auto m: seen_fin.sets())
{
acc_cond::mark_t cm = complement[m];
// Inf({i}) | Inf({!i}) = t;
if (cm & seen_inf)
return acc_cond::acc_code::t();
// Fin({!i}) | Inf({i}) = Inf({i})
fin.front().mark -= complement[m];
// Fin(i) & Fin(!i) = f;
if (cm & seen_fin)
return std::move(falsecode);
// Inf({!i}) & Fin({i}) = Fin({i})
rbegin[-1].mark -= complement[m];
}
return res | fin;
if (rbegin[-1].mark)
return res;
// Inf(i) has been rewritten as t, we need to remove it. Sigh!
acc_cond::acc_code res2 = std::move(truecode);
rbegin = &res.back() - 1;
do
{
acc_cond::acc_code tmp(rbegin);
if (opand == acc_cond::acc_op::And)
tmp &= std::move(res);
else
tmp |= std::move(res);
std::swap(tmp, res2);
rbegin -= rbegin->sub.size + 1;
}
while (rbegin > rend);
return res2;
};
switch (pos->sub.op)
{
case acc_cond::acc_op::And:
return boolop(acc_cond::acc_op::And,
acc_cond::acc_op::Fin,
acc_cond::acc_op::Inf,
acc_cond::acc_code::t(),
acc_cond::acc_code::f());
case acc_cond::acc_op::Or:
return boolop(acc_cond::acc_op::Or,
acc_cond::acc_op::Inf,
acc_cond::acc_op::Fin,
acc_cond::acc_code::f(),
acc_cond::acc_code::t());
case acc_cond::acc_op::Fin:
return acc_cond::acc_code::fin(pos[-1].mark);
case acc_cond::acc_op::Inf:

4
tests/core/sccdot.test
View file

@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et
# Copyright (C) 2015, 2017, 2018, 2020 Laboratoire de Recherche et
# Développement de l'Epita
#
# This file is part of Spot, a model checking library.
@ -156,7 +156,7 @@ HOA: v1
States: 8
Start: 0
AP: 2 "a" "b"
Acceptance: 3 Fin(2) & (Inf(0)&Inf(1))
Acceptance: 3 (Inf(0)&Inf(1)) & Fin(2)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0

11
tests/python/merge.py
View file

@ -43,7 +43,8 @@ assert hoa == """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Fin(1) | Inf(0)
acc-name: parity min even 2
Acceptance: 2 Inf(0) | Fin(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
@ -78,7 +79,8 @@ assert hoa == """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Fin(1) | Inf(0)
acc-name: parity min even 2
Acceptance: 2 Inf(0) | Fin(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
@ -149,7 +151,8 @@ assert hoa == """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Fin(1) | Inf(0)
acc-name: parity min even 2
Acceptance: 2 Inf(0) | Fin(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
@ -289,7 +292,7 @@ assert hoa == """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 2 (Fin(1) & Inf(0)) | (Fin(1) & Inf(0))
Acceptance: 2 (Inf(0) & Fin(1)) | (Inf(0) & Fin(1))
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0 {0}

11
tests/python/simplacc.py
View file

@ -67,18 +67,17 @@ for a in auts:
c = spot.simplify_acceptance(b)
assert b.get_acceptance() == c.get_acceptance()
assert res == [
'Inf(0)',
'Fin(0)',
'Fin(0) & Inf(1)',
'Inf(1) & Fin(0)',
'Fin(1) | Inf(0)',
'(Fin(0) | Inf(2)) & Inf(1)',
'Fin(1) | (Fin(2) & Inf(0))',
'(Fin(1) | Inf(2)) & Inf(0)',
'Inf(1) & (Fin(0) | Inf(2))',
'Fin(1) | (Inf(0) & Fin(2))',
'Inf(0) & (Inf(2) | Fin(1))',
'Fin(0) | (Fin(2) & Inf(1))',
'((Fin(1) | Inf(2)) & Inf(5)) | (Fin(0) & (Fin(1) | (Fin(3) & Inf(4))))',
'(Fin(5) | (Fin(2) & Inf(1))) & (Inf(0) | ((Fin(4) | Inf(3)) & Inf(1)))',
'((Inf(1) & Fin(2)) | Fin(5)) & (Inf(0) | (Inf(1) & (Inf(3) | Fin(4))))',
'Inf(0)',
'Fin(0)',
]

3
tests/python/toparity.py
View file

@ -112,6 +112,7 @@ def test(aut, expected_num_states=[], full=True):
spot.reduce_parity_here(p1)
assert spot.are_equivalent(aut, p1)
if expected_num is not None:
# print(p1.num_states(), expected_num)
assert p1.num_states() == expected_num
if full:
# Make sure passing opt is the same as setting
@ -292,7 +293,7 @@ State: 4
[0&!1] 4
[0&1] 4 {1 2 4}
--END--
"""), [9, 6, 6, 6, 7, 6, 6])
"""), [9, 6, 7, 7, 6, 6, 6])
test(spot.automaton("""
HOA: v1