1 # This program is free software; you can redistribute it and/or modify
2 # it under the terms of the GNU General Public License as published by
3 # the Free Software Foundation; either version 2 of the License, or
4 # (at your option) any later version.
6 # This program is distributed in the hope that it will be useful,
7 # but WITHOUT ANY WARRANTY; without even the implied warranty of
8 # MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
9 # GNU General Public License for more details.
11 # You should have received a copy of the GNU General Public License
12 # along with this program; if not, write to the Free Software
13 # Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
15 # Copyright (C) Mathieu Desnoyers, 2009
17 # Authors: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
25 make read_order | tee read_order.log
26 make read_order_no_wmb | tee read_order_no_wmb.log
27 make read_order_no_rmb | tee read_order_no_rmb.log
28 make asserts | tee asserts.log
31 #show trail : spin -v -t -N pan.ltl input.spin
32 # after each individual make.
36 @echo
"Verification summary"
40 cat DEFINES
> .input.spin
41 cat
${SPINFILE} >> .input.spin
42 rm -f .input.spin.trail
43 spin
-a
-X .input.spin
44 gcc
-w
${CFLAGS} -DSAFETY
-o pan pan.c
45 .
/pan
-v
-c1
-X
-m10000
-w19
46 cp .input.spin
$@.spin.input
47 -cp .input.spin.trail
$@.spin.input.trail
49 read_order
: clean read_order_ltl run
50 cp .input.spin
$@.spin.input
51 -cp .input.spin.trail
$@.spin.input.trail
53 read_order_no_rmb
: clean read_order_ltl read_order_no_rmb_define run
54 cp .input.spin
$@.spin.input
55 -cp .input.spin.trail
$@.spin.input.trail
57 read_order_no_rmb_define
:
58 cp read_order_no_rmb.
define .input.
define
60 read_order_no_wmb
: clean read_order_ltl read_order_no_wmb_define run
61 cp .input.spin
$@.spin.input
62 -cp .input.spin.trail
$@.spin.input.trail
64 read_order_no_wmb_define
:
65 cp read_order_no_wmb.
define .input.
define
70 cat .input.
define >> pan.ltl
71 spin
-f
"!(`cat read_order.ltl | grep -v ^//`)" >> pan.ltl
74 .
/pan
-a
-v
-c1
-X
-m10000
-w19
77 gcc
-w
${CFLAGS} -o pan pan.c
79 pan.c
: pan.ltl
${SPINFILE}
80 cat DEFINES
> .input.spin
81 cat .input.
define >> .input.spin
82 cat
${SPINFILE} >> .input.spin
83 rm -f .input.spin.trail
84 spin
-a
-X
-N pan.ltl .input.spin
86 .PHONY
: clean default
distclean summary
88 rm -f pan
* trail.out .input.spin
* *.spin.trail .input.
define
90 rm -f
*.trail
*.input
*.log