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

tests: add tests for parallel algorithms

Browse source 
* tests/ltsmin/check.test: here.
This commit is contained in:
Etienne Renault 2017-11-22 09:49:30 +01:00
parent 63a4b4085a
commit f397def03e
1 changed files with 14 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

14
tests/ltsmin/check.test
View file

@ -77,3 +77,17 @@ cat stderr
grep 'No variable' stderr
grep 'No state' stderr
grep 'Unexpected' stderr
# Test parallel algorithms
# Test Deadlock
run 0 ../modelcheck --model beem-peterson.4.dve2C \
--csv --has-deadlock -p 3 >stdout
test `grep "#" stdout | awk -F',' '{print $4}'` = "NO-DEADLOCK"
# Test Bloemen
run 0 ../modelcheck --model beem-peterson.4.dve2C \
--csv --bloemen -p 3 >stdout
test `grep "#" stdout | awk -F',' '{print $7}'` -eq 29115