dc45444e |
1 | # makefile |
2 | |
3 | COPTIONS=-DSAFETY |
4 | |
5 | |
6 | default: |
7 | make commit_sum | tee commit_sum.log |
8 | make read_write | tee read_write.log |
9 | make events_lost | tee events_lost.log |
10 | make no_events_lost | tee no_events_lost.log |
11 | |
12 | |
13 | no_events_lost: clean no_events_lost_ltl run |
14 | |
15 | no_events_lost_ltl: |
16 | cat defines > pan.ltl |
17 | cat no_events_lost.def > pan.spin |
18 | spin -f "!(`cat no_events_lost.ltl | grep -v ^//`)" >> pan.ltl |
19 | |
20 | |
21 | |
22 | events_lost: clean events_lost_ltl run |
23 | |
24 | events_lost_ltl: |
25 | cat defines > pan.ltl |
26 | spin -f "!(`cat events_lost.ltl | grep -v ^//`)" >> pan.ltl |
27 | |
28 | |
29 | |
30 | read_write: clean read_write_ltl run |
31 | |
32 | read_write_ltl: |
33 | cat defines > pan.ltl |
34 | spin -f "!(`cat read_write.ltl | grep -v ^//`)" >> pan.ltl |
35 | |
36 | |
37 | |
38 | commit_sum: clean commit_sum_ltl run |
39 | |
40 | commit_sum_ltl: |
41 | cat defines > pan.ltl |
42 | spin -f "!(`cat commit_sum.ltl | grep -v ^//`)" >> pan.ltl |
43 | |
44 | |
45 | |
46 | run: pan |
47 | ./pan -v -X -m100000 -w21 -a -c1 |
48 | |
49 | pan: pan.c |
50 | gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=750 -DXUSAFE -DNOFAIR pan.c |
51 | |
52 | pan.c: pan.ltl model.spin |
53 | cat model.spin >> pan.spin |
54 | spin -a -X -N pan.ltl pan.spin |
55 | |
56 | |
57 | |
58 | clean: |
59 | rm -f pan* trail.out |