acc: fix maybe_accepting() on Fin(x)|Fin(y)|Fin(z)

Fixes #271, reported by Henrich Lauko.

* spot/twa/acc.cc (maybe_accepting): Fix handling in case
of disjunction of Fin.
* tests/core/scc.test, tests/python/accparse2.py: Add more
tests.
This commit is contained in:
Alexandre Duret-Lutz 2017-06-21 16:03:17 +02:00
parent fc609057d6
commit 20df3b4e98
3 changed files with 42 additions and 4 deletions

View file

@ -255,12 +255,12 @@ namespace spot
case acc_cond::acc_op::Inf: case acc_cond::acc_op::Inf:
return (pos[-1].mark & infinitely_often) == pos[-1].mark; return (pos[-1].mark & infinitely_often) == pos[-1].mark;
case acc_cond::acc_op::Fin: case acc_cond::acc_op::Fin:
if (pos[-1].mark & always_present) if ((pos[-1].mark & always_present) == pos[-1].mark)
return false; return false;
else if (pos[-1].mark & infinitely_often) else if ((pos[-1].mark & infinitely_often) != pos[-1].mark)
return trival::maybe();
else
return true; return true;
else
return trival::maybe();
case acc_cond::acc_op::FinNeg: case acc_cond::acc_op::FinNeg:
case acc_cond::acc_op::InfNeg: case acc_cond::acc_op::InfNeg:
SPOT_UNREACHABLE(); SPOT_UNREACHABLE();

View file

@ -103,3 +103,35 @@ EOF
run 0 autfilt --decompose-scc=1 -F aut> out run 0 autfilt --decompose-scc=1 -F aut> out
cat out cat out
diff out ref diff out ref
# From issue #271, reported by Henrich Lauko.
cat >in.hoa <<EOF
HOA: v1
States: 4
Start: 2
AP: 2 "p1" "p0"
acc-name: generalized-co-Buchi 2
Acceptance: 2 Fin(0)|Fin(1)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0 {0}
[1] 0
[!1] 1
State: 1 {0 1}
[1] 0
[!1] 1
State: 2
[0&1] 0
[0&!1] 1
[!0&1] 2
[!0&!1] 3
State: 3 {1}
[0&1] 0
[0&!1] 1
[!0&1] 2
[!0&!1] 3
--END--
EOF
test 2 = `autfilt --stats=%[a]c in.hoa`

View file

@ -41,6 +41,12 @@ assert a.maybe_accepting([2], []).is_true()
assert a.maybe_accepting([0, 1], []).is_maybe() assert a.maybe_accepting([0, 1], []).is_maybe()
assert a.maybe_accepting([0, 1], [1]).is_false() assert a.maybe_accepting([0, 1], [1]).is_false()
a.set_acceptance('Fin(0)|Fin(1)')
assert a.maybe_accepting([0, 1], [1]).is_maybe()
assert a.maybe_accepting([0, 1], [0, 1]).is_false()
assert a.maybe_accepting([0], []).is_true()
assert a.maybe_accepting([], [0]).is_true()
a = spot.acc_cond(0) a = spot.acc_cond(0)
a.set_acceptance('all') a.set_acceptance('all')
assert(a.is_rabin() == -1) assert(a.is_rabin() == -1)