Commit bdf65191 authored by Etienne Renault's avatar Etienne Renault

tests: add tests for parallel algorithms

* tests/ltsmin/check.test: here.
parent 6c7a8499
......@@ -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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment