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

simplify_acc: fix an infinite loop

Browse source 
* spot/twaalgos/cleanacc.cc (fuse_mark_here): Fix incorrect cancelling
of n-ary subterms, causing an invalid acceptance condition, and then
an infinite loop.
* tests/python/simplacc.py: Add test case.
This commit is contained in:
Alexandre Duret-Lutz 2020-04-16 22:40:49 +02:00
parent 68012e6a85
commit b62e1bb13c
2 changed files with 28 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

21
spot/twaalgos/cleanacc.cc
View file

@ -367,7 +367,7 @@ namespace spot
return {};
}
acc_cond::mark_t find_interm_rec(acc_cond::acc_word* pos)
acc_cond::mark_t find_interm_rec(const acc_cond::acc_word* pos)
{
acc_cond::acc_op wanted;
auto topop = pos->sub.op;
@ -489,13 +489,13 @@ namespace spot
assert(topop == acc_cond::acc_op::Or);
}
// Return a vector of "singleton-sets" of
// Build a vector of "singleton-sets" of
// the wanted type in the operand of the
// pointed Or/And operator. For instance,
// assuming wanted=Inf and pos points to
//
// Inf({1})|Inf({2,3})|Fin({4})
// |Inf({5})|Inf({5})|Inf({6})
// |Inf({5})|Inf({5,6})
//
// This returns [({1}, Inf({1})),
// ({5}, Inf({5}))]].
@ -522,9 +522,8 @@ namespace spot
break;
case acc_cond::acc_op::And:
case acc_cond::acc_op::Or:
// On
// Fin(a)&(Fin(b)&Inf(c)|Fin(d))
// where we'd like to return [({a},...),
// On Fin(a)&(Fin(b)&Inf(c)|Fin(d))
// we'd like to build [({a},...),
// ({b,d},...)] and decide later that
// {b,d} can receive {a} if they
// (b and d) are both used once.
@ -556,12 +555,18 @@ namespace spot
if (p.first != can_receive &&
p.first.lowest() == p.first)
{
to_fuse.emplace_back(p.first, can_receive);
// Mark fused singletons as false,
// so that a future call to
// find_fusable() ignores them.
if (p.second->sub.op == acc_cond::acc_op::Fin)
p.second->sub.op = acc_cond::acc_op::Inf;
else
else if (p.second->sub.op ==
acc_cond::acc_op::Inf)
p.second->sub.op = acc_cond::acc_op::Fin;
else
continue;
p.second[-1].mark = {};
to_fuse.emplace_back(p.first, can_receive);
}
};

16
tests/python/simplacc.py
View file

@ -38,7 +38,19 @@ 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--"""))
[!0&1] 2 {1 4} [0&1] 3 {0} --END--
/* This one caused an infinite loop in the simplification code. */
HOA: v1 States: 10 Start: 0 AP: 2 "p0" "p1" Acceptance: 6 (((Fin(4) &
(Fin(3) | (Fin(3) & Inf(1))) & (Inf(0)&Inf(5))) | (Fin(5) & Fin(2)))
& Inf(5)) | Inf(5) | Inf(0) properties: trans-labels explicit-labels
trans-acc --BODY-- State: 0 [!0&!1] 2 [!0&!1] 7 {1} [!0&!1] 6 State:
1 [!0&!1] 5 {1 5} [0&!1] 9 {3} [!0&1] 1 {0} [!0&!1] 4 {0 3} State: 2
[0&1] 1 {1} State: 3 [!0&1] 8 {4} State: 4 [!0&!1] 0 {5} [!0&1] 3 {4}
State: 5 [!0&1] 4 {3 5} [!0&1] 3 {2 4} [!0&1] 2 {2 3} [!0&!1] 0 {0}
[!0&1] 7 {0 4 5} [0&1] 5 {2} State: 6 [0&!1] 7 [0&!1] 1 {1 4} [0&1]
4 {1 4} State: 7 [0&1] 3 {2 3} [0&1] 0 [!0&!1] 6 [0&1] 1 State: 8 [0&1]
3 [!0&!1] 0 [0&1] 9 State: 9 [0&!1] 7 {4 5} [!0&1] 8 {0} [0&1] 9 --END--
"""))
res = []
for a in auts:
@ -62,4 +74,6 @@ assert res == [
'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) | Inf(0)',
'Fin(1) & Fin(0)',
]