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

simplify_acceptance: fix erroneous simplification

Browse source 
Reported by Florian Renkin.

* spot/twaalgos/cleanacc.cc: Do not rewrite
...Fin(0)&(Fin(1)|(Fin(3)&Inf(4)))... as Fin(0)&f when it appears that
{1,3} cannot receive {0}, because {1} is used elsewhere in the
acceptance.
* tests/python/simplacc.py: Add test case.
This commit is contained in:
Alexandre Duret-Lutz 2020-02-24 12:17:07 +01:00
parent b44daef42a
commit 8a4a4b9fff
2 changed files with 25 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

8
spot/twaalgos/cleanacc.cc
View file

@ -524,8 +524,8 @@ namespace spot
case acc_cond::acc_op::Or: case acc_cond::acc_op::Or:
// On // On
// Fin(a)&(Fin(b)&Inf(c)|Fin(d)) // Fin(a)&(Fin(b)&Inf(c)|Fin(d))
// where we'd like to return [{a}, // where we'd like to return [({a},...),
// {b,d}] and decide later that // ({b,d},...)] and decide later that
// {b,d} can receive {a} if they // {b,d} can receive {a} if they
// (b and d) are both used once. // (b and d) are both used once.
if (auto m = find_interm_rec(pos)) if (auto m = find_interm_rec(pos))
@ -553,7 +553,8 @@ namespace spot
if (!can_receive) if (!can_receive)
return; return;
for (auto p: singletons) for (auto p: singletons)
if (p.first != can_receive) if (p.first != can_receive &&
p.first.lowest() == p.first)
{ {
to_fuse.emplace_back(p.first, can_receive); to_fuse.emplace_back(p.first, can_receive);
if (p.second->sub.op == acc_cond::acc_op::Fin) if (p.second->sub.op == acc_cond::acc_op::Fin)
@ -592,6 +593,7 @@ namespace spot
for (auto pair: to_fuse) for (auto pair: to_fuse)
if (pair.first & once) // can we remove pair.first? if (pair.first & once) // can we remove pair.first?
{ {
assert(pair.first.count() == 1);
for (auto& e: aut->edges()) for (auto& e: aut->edges())
if (e.acc & pair.first) if (e.acc & pair.first)
e.acc = (e.acc - pair.first) | pair.second; e.acc = (e.acc - pair.first) | pair.second;

29
tests/python/simplacc.py
View file

@ -31,7 +31,14 @@ HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" Acceptance: 3 (Inf(0) | Inf(1)) &
HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" Acceptance: 4 (Inf(0) | HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" Acceptance: 4 (Inf(0) |
(Inf(1)&(Inf(3)|Fin(2)))) --BODY-- State: 0 [1] 0 {3} [0] 1 {0} State: 1 [0] 1 (Inf(1)&(Inf(3)|Fin(2)))) --BODY-- State: 0 [1] 0 {3} [0] 1 {0} State: 1 [0] 1
{2} [1] 0 {1} --END-- {2} [1] 0 {1} --END--
""")) /* The next automaton was incorrectly simplified. */
HOA: v1 States: 4 Start: 0 AP: 2 "p0" "p1" Acceptance: 6 ((Fin(1) | Inf(2)) &
Inf(5)) | (Fin(0) & (Fin(1) | (Fin(3) & Inf(4)))) properties: trans-labels
explicit-labels trans-acc complete properties: deterministic --BODY-- State: 0
[!0&!1] 0 {2} [0&1] 1 {0 5} [0&!1] 1 {0 2 5} [!0&1] 2 {1} State: 1 [0&1] 1 {0}
[!0&!1] 1 {2} [0&!1] 1 {0 2} [!0&1] 2 {1} State: 2 [!0&!1] 0 {2 3} [0&!1] 0 {0
2 3 5} [!0&1] 2 {1 4} [0&1] 3 {0 5} State: 3 [!0&!1] 0 {2 3} [0&!1] 0 {0 2 3 5}
[!0&1] 2 {1 4} [0&1] 3 {0} --END--"""))
res = [] res = []
for a in auts: for a in auts:
@ -44,11 +51,15 @@ for a in auts:
assert b.equivalent_to(a) assert b.equivalent_to(a)
res.append(str(b.get_acceptance())) res.append(str(b.get_acceptance()))
assert res == ['Inf(0)', assert res == [
'Fin(0)', 'Inf(0)',
'Inf(1) & Fin(0)', 'Fin(0)',
'Fin(1) | Inf(0)', 'Inf(1) & Fin(0)',
'Inf(1) & (Fin(0) | Inf(2))', 'Fin(1) | Inf(0)',
'Fin(1) | (Fin(2) & Inf(0))', 'Inf(1) & (Fin(0) | Inf(2))',
'(Fin(1) | Inf(2)) & Inf(0)', 'Fin(1) | (Fin(2) & Inf(0))',
'Fin(0) | (Fin(2) & Inf(1))'] '(Fin(1) | Inf(2)) & Inf(0)',
'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)))',
]