| 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 | spin -f "!(`cat no_events_lost.ltl | grep -v ^//`)" >> pan.ltl |
| 18 | |
| 19 | |
| 20 | |
| 21 | events_lost: clean events_lost_ltl run |
| 22 | |
| 23 | events_lost_ltl: |
| 24 | cat DEFINES > pan.ltl |
| 25 | spin -f "!(`cat events_lost.ltl`)" >> pan.ltl |
| 26 | |
| 27 | |
| 28 | |
| 29 | read_write: clean read_write_ltl run |
| 30 | |
| 31 | read_write_ltl: |
| 32 | cat DEFINES > pan.ltl |
| 33 | spin -f "!(`cat read_write.ltl`)" >> pan.ltl |
| 34 | |
| 35 | |
| 36 | |
| 37 | commit_sum: clean commit_sum_ltl run |
| 38 | |
| 39 | commit_sum_ltl: |
| 40 | cat DEFINES > pan.ltl |
| 41 | spin -f "!(`cat commit_sum.ltl`)" >> pan.ltl |
| 42 | |
| 43 | |
| 44 | |
| 45 | run: pan |
| 46 | ./pan -v -X -m100000 -w21 -a -c1 |
| 47 | |
| 48 | pan: pan.c |
| 49 | gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=750 -DXUSAFE -DNOFAIR pan.c |
| 50 | |
| 51 | pan.c: pan.ltl model.spin |
| 52 | spin -a -X -N pan.ltl model.spin |
| 53 | |
| 54 | |
| 55 | |
| 56 | clean: |
| 57 | rm -f pan* trail.out |