[lttv.git] / trunk / verif / md / run

#!/bin/bash

#avail. mem
MEM=15360

#spin -a model.spin
#cc -DMEMLIM=${MEM} -DSAFETY -o pan pan.c
#./pan

#first LTL formula
cat defines > pan.ltl
/usr/local/bin/spin -f "!($(cat model_03_write_read_off.spin.ltl | grep -v ^//))" >> pan.ltl
/usr/local/bin/spin -a -X -N pan.ltl  model.spin

gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=1850 -DXUSAFE -DNOFAIR  pan.c
time ./pan -v -X -m10000 -w19  -a -c1

#second LTL formula
cat defines > pan.ltl
/usr/local/bin/spin -f "!($(cat model_03_write_commit_sum.spin.ltl | grep -v ^//))" >> pan.ltl
/usr/local/bin/spin -a -X -N pan.ltl  model.spin

gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=1850 -DXUSAFE -DNOFAIR  pan.c
time ./pan -v -X -m10000 -w19  -a -c1

#3rd
cat defines > pan.ltl
/usr/local/bin/spin -f "!($(cat model_03_events_lost.spin.ltl | grep -v ^//))" >> pan.ltl
/usr/local/bin/spin -a -X -N pan.ltl  model.spin

gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=1850 -DXUSAFE -DNOFAIR  pan.c
time ./pan -v -X -m10000 -w19  -a -c1

#4th
cat defines > pan.ltl
/usr/local/bin/spin -f "!($(cat model_03_no_events_lost.spin.ltl | grep -v ^//))" >> pan.ltl
/usr/local/bin/spin -a -X -N pan.ltl  model.spin

gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=1850 -DXUSAFE -DNOFAIR  pan.c
time ./pan -v -X -m10000 -w19  -a -c1
Commit	Line	Data
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