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

modelcheck: more relevant information for --csv

Browse source 
* tests/ltsmin/check.test,
tests/ltsmin/modelcheck.cc: Here.
This commit is contained in:
Etienne Renault 2020-05-14 16:00:53 +02:00
parent bdb95dcde9
commit 070dc4880a
2 changed files with 21 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

5
tests/ltsmin/check.test
View file

@ -90,6 +90,11 @@ run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
--csv --bloemen -p 1 >stdout
test `grep "#" stdout | awk -F',' '{print $8}'` -eq 29115
# Test Bloemen
run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
--csv --bloemen -p 3 >stdout
test `grep "#" stdout | awk -F',' '{print $8}'` -eq 29115
run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
--formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv --bloemen-ec -p 3 >stdout