verif/md/run

   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