####### # # E-scripts for model checkers. # # Note 1: use the eev command (defined in eev.el) and the # ee alias (in my .zshrc) to execute parts of this file. # Executing this file as a whole makes no sense. # An introduction to eev can be found here: # # (find-eev-quick-intro) # http://angg.twu.net/eev-intros/find-eev-quick-intro.html # # Note 2: be VERY careful and make sure you understand what # you're doing. # # Note 3: If you use a shell other than zsh things like |& # and the for loops may not work. # # Note 4: I always run as root. # # Note 5: some parts are too old and don't work anymore. Some # never worked. # # Note 6: the definitions for the find-xxxfile commands are on my # .emacs. # # Note 7: if you see a strange command check my .zshrc -- it may # be defined there as a function or an alias. # # Note 8: the sections without dates are always older than the # sections with dates. # # This file is at # or at . # See also , # , # , # , # and . # ####### lynx /usr/src/spin-3.3.6/HTML/ltl.html spin -f '[] place' spin -f '<> picked' spin -f '[] (place -> <> picked)' s = 1; do :: s == 1 -> s = 1 :: s == 1 -> s = 2 :: s == 2 -> break cd ~/SPIN/ cat > foo <<'---' byte s; init { s = 1; progress_1: do :: s == 1 -> s = 1 :: s == 1 -> s = 2 :: s == 2 -> break od; progress_2: skip; do :: s == 1 -> break od; progress_3: skip; } --- spin -a -v foo gcc -DNP -o pan pan.c pan -l -f -v |& tee ol # (find-fline "~/SPIN/pan.t") # (find-fline "~/SPIN/pan.t") pan |& tee o #pan -a |& tee oa pan -l |& tee ol ##### # # spin docs (2 pages per sheet) # ##### # (find-vldifile "psutils.list") # (find-fline "/usr/doc/psutils/") # (find-fline "$ES/print.e" "pstops") # pstops -d 4:0@$S($H0,$V0)+1@$S($H1,$V0)+2@$S($H0,$V2)+3@$S($H1,$V2) # psresize -Pletter -pA4 function prom () { SPEC="2:0@$2R($3,$4)+1@$2R($5,$6)" echo $SPEC OUTFILE=/tmp/$1_$2_$3_$4_$5_$6.ps OUTFILE=/tmp/$1.ps pstops $SPEC < ~edrx/$1.ps > $OUTFILE gv $OUTFILE & } function prom2 () { prom $1 0.6 50 750 50 430 } prom2 manual #prom intro 0.6 50 430 50 450 prom2 intro prom2 concise cd /tmp/ make -f ~/LATEX/Makefile manual.p01 ##### # # smv # 99nov24 # ##### rm -Rv /usr/src/smv/ cd /usr/src/ tar -xvzf $S/http/www.cs.cmu.edu/~modelcheck/smv/smv.r2.5.3.1d.tar.gz cd /usr/src/smv/ # (find-fline "/usr/src/smv/") ##### # # spin # 99dec01 # ##### rm -Rv /usr/src/spin-3.3.6/ mkdir /usr/src/spin-3.3.6/ cd /usr/src/spin-3.3.6/ tar -xvzf $S/http/netlib.bell-labs.com/netlib/spin/spin336.tar.gz tar -xvzf $S/http/netlib.bell-labs.com/netlib/spin/html.tar.gz chmod 644 $(find * -type f) cd /usr/src/spin-3.3.6/Src3.3/ make |& tee om ln -sf /usr/src/spin-3.3.6/Src3.3/spin /usr/bin/spin cat > /usr/bin/xspin <<'---' #!/bin/sh wish /usr/src/spin-3.3.6/Xspin3.3/xspin333.tcl $* --- chmod 755 /usr/bin/xspin # (code-c-d "spin" "/usr/src/spin-3.3.6/") # (find-spinfile "") # (find-spinfile "Test/") # (find-spinfile "Test/README.tests") # (find-spinfile "Test/README.tests" "test 5") cd /usr/src/spin-3.3.6/Test/ sh examples rm examples # 1 spin hello # 2 spin -a loops gcc -DNOREDUCE -o pan pan.c ./pan # 3 ./pan -a # 4 spin -t -p loops # 5 gcc -DNP -DNOREDUCE -o pan pan.c ./pan -l # 6 for i in leader snoopy pftp sort; do echo "\n\n $i:\n" spin -a $i gcc -DSAFETY -DNOREDUCE -DNOCLAIM -o pan pan.c ./pan -c0 -n done # 6b gcc -DSAFETY -DNOCLAIM -o pan pan.c ./pan -c0 -n # 7 (does not terminate) spin -p -g priorities |& head -n 200 # 8 spin -f "[] ( p U ( <> q ))" # 9 spin -a -N leader.ltl leader gcc -o pan pan.c pan -a edrxnetscape /usr/src/spin-3.3.6/HTML/index.html & # Local Variables: # coding: utf-8-unix # End: