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

bitset: fix implementation of operator-()

Browse source 
This fixes #469.

* spot/misc/bitset.hh (bitset::operator-): Rewrite.
I cannot follow the logic of the old implementation.
* tests/python/setacc.py: Add a test case, inspired from #469.
This commit is contained in:
Alexandre Duret-Lutz 2021-07-05 14:12:58 +02:00
parent bb7426c0b9
commit c0c76904da
2 changed files with 19 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

11
spot/misc/bitset.hh
View file

@ -318,15 +318,12 @@ namespace spot
bitset operator-() const bitset operator-() const
{ {
bitset res = *this; bitset res = *this;
unsigned carry = 0; unsigned carry = 1;
for (auto& v : res.data) for (auto& v : res.data)
{ {
v += carry; word_t old = v;
if (v < carry) v = ~v + carry;
carry = 2; carry = old == 0;
else
carry = 1;
v = -v;
} }
return res; return res;
} }

16
tests/python/setacc.py
View file

@ -1,6 +1,6 @@
#!/usr/bin/python3 #!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*- # -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement de # Copyright (C) 2016, 2018, 2021 Laboratoire de Recherche et Développement de
# l'EPITA. # l'EPITA.
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -82,3 +82,17 @@ assert v == ()
# FIXME: We should have a way to disable the following output, as it is not # FIXME: We should have a way to disable the following output, as it is not
# part of HOA v1. # part of HOA v1.
assert acc.name() == "generalized-Streett 1 2" assert acc.name() == "generalized-Streett 1 2"
# issue #469. This test is meaningful only if Spot is compiled with
# --enable-max-accsets=64 or more.
try:
m = spot.mark_t([33])
assert m.lowest() == m
n = spot.mark_t([33,34])
assert n.lowest() == m
except RuntimeError as e:
if "Too many acceptance sets used." in str(e):
pass
else:
raise e