#!/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