dc45444e |
1 | #!/bin/bash |
2 | |
3 | #avail. mem |
4 | MEM=15360 |
5 | |
6 | #spin -a model.spin |
7 | #cc -DMEMLIM=${MEM} -DSAFETY -o pan pan.c |
8 | #./pan |
9 | |
10 | #first LTL formula |
11 | cat defines > pan.ltl |
12 | /usr/local/bin/spin -f "!($(cat model_03_write_read_off.spin.ltl | grep -v ^//))" >> pan.ltl |
13 | /usr/local/bin/spin -a -X -N pan.ltl model.spin |
14 | |
15 | gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=1850 -DXUSAFE -DNOFAIR pan.c |
16 | time ./pan -v -X -m10000 -w19 -a -c1 |
17 | |
18 | #second LTL formula |
19 | cat defines > pan.ltl |
20 | /usr/local/bin/spin -f "!($(cat model_03_write_commit_sum.spin.ltl | grep -v ^//))" >> pan.ltl |
21 | /usr/local/bin/spin -a -X -N pan.ltl model.spin |
22 | |
23 | gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=1850 -DXUSAFE -DNOFAIR pan.c |
24 | time ./pan -v -X -m10000 -w19 -a -c1 |
25 | |
26 | #3rd |
27 | cat defines > pan.ltl |
28 | /usr/local/bin/spin -f "!($(cat model_03_events_lost.spin.ltl | grep -v ^//))" >> pan.ltl |
29 | /usr/local/bin/spin -a -X -N pan.ltl model.spin |
30 | |
31 | gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=1850 -DXUSAFE -DNOFAIR pan.c |
32 | time ./pan -v -X -m10000 -w19 -a -c1 |
33 | |
34 | #4th |
35 | cat defines > pan.ltl |
36 | /usr/local/bin/spin -f "!($(cat model_03_no_events_lost.spin.ltl | grep -v ^//))" >> pan.ltl |
37 | /usr/local/bin/spin -a -X -N pan.ltl model.spin |
38 | |
39 | gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=1850 -DXUSAFE -DNOFAIR pan.c |
40 | time ./pan -v -X -m10000 -w19 -a -c1 |
41 | |
42 | |
43 | |
44 | |