#######
#
# 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 <http://angg.twu.net/e/modelcheck.e>
#           or at <http://angg.twu.net/e/modelcheck.e.html>.
#        See also <http://angg.twu.net/emacs.html>,
#                 <http://angg.twu.net/.emacs[.html]>,
#                 <http://angg.twu.net/.zshrc[.html]>,
#                 <http://angg.twu.net/escripts.html>,
#             and <http://angg.twu.net/>.
#
#######




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: