diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index be3837658..9bd502d0a 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -255,12 +255,12 @@ namespace spot case acc_cond::acc_op::Inf: return (pos[-1].mark & infinitely_often) == pos[-1].mark; case acc_cond::acc_op::Fin: - if (pos[-1].mark & always_present) + if ((pos[-1].mark & always_present) == pos[-1].mark) return false; - else if (pos[-1].mark & infinitely_often) - return trival::maybe(); - else + else if ((pos[-1].mark & infinitely_often) != pos[-1].mark) return true; + else + return trival::maybe(); case acc_cond::acc_op::FinNeg: case acc_cond::acc_op::InfNeg: SPOT_UNREACHABLE(); diff --git a/tests/core/scc.test b/tests/core/scc.test index ec1388787..ba9232f6a 100755 --- a/tests/core/scc.test +++ b/tests/core/scc.test @@ -103,3 +103,35 @@ EOF run 0 autfilt --decompose-scc=1 -F aut> out cat out diff out ref + + +# From issue #271, reported by Henrich Lauko. +cat >in.hoa <