otf_product: fix deletion of iter_cache_
Fixes #152, reported by Valentin Iovene. * spot/twa/twaproduct.cc (~twa_product): Delete iter_cache_. * tests/python/otfcrash.py: New file. * tests/Makefile.am: Add it. * NEWS: Mention the bug.
This commit is contained in:
parent
e86370f894
commit
3a3913cf50
4 changed files with 46 additions and 0 deletions
39
tests/python/otfcrash.py
Normal file
39
tests/python/otfcrash.py
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
import spot
|
||||
import spot.ltsmin
|
||||
import tempfile
|
||||
import shutil
|
||||
import sys
|
||||
|
||||
# this test requires divine with --ltsmin support
|
||||
if shutil.which("divine") == None:
|
||||
sys.exit(77)
|
||||
import subprocess
|
||||
out = subprocess.check_output(['divine', 'compile',
|
||||
'--help'], stderr=subprocess.STDOUT)
|
||||
if b'LTSmin' not in out:
|
||||
sys.exit(77)
|
||||
|
||||
# the test case actually starts here
|
||||
with tempfile.NamedTemporaryFile(dir='.', suffix='.dve') as fp:
|
||||
fp.write(b"""int f = 3;
|
||||
process R {
|
||||
int p = 1, found = 0;
|
||||
state i, e;
|
||||
init i;
|
||||
trans
|
||||
i -> i {guard p != f; effect p = p + 1;},
|
||||
i -> e {guard p == f; effect found = 1;},
|
||||
e -> e {};
|
||||
}
|
||||
system async;
|
||||
""")
|
||||
fp.flush()
|
||||
m = spot.ltsmin.load(fp.name)
|
||||
|
||||
def modelcheck(formula, model):
|
||||
a = spot.translate(formula)
|
||||
k = m.kripke([ap.ap_name() for ap in a.ap()])
|
||||
p = spot.otf_product(k, a)
|
||||
return p.is_empty()
|
||||
|
||||
assert(modelcheck('X "R.found"', m) == True)
|
||||
Loading…
Add table
Add a link
Reference in a new issue