
This directory contains the Promela source files for the models
discussed in the paper "Modeling Wildcard-Free MPI Programs for
Verification", by Stephen F. Siegel and George S. Avrunin, PPoPP '05,
June 15--17, 2005, Chicago, IL, USA.

There are 8 data referred to in the paper, each corresponding to a
file, as follows:


               Filename               number of states

1. laplace-deadlock-nobar-buf.prom      1.39834e+06
2. laplace-deadlock-nobar-nobuf.prom         26,686
3. laplace-partial-deadlock-buf.prom    9.04759e+06 (1.65726e+07 visited)
4. laplace-partial-deadlock-nobuf.prom      242,956 (443,098 visited)
5. laplace-deadlock-bar-buf.prom            441,010
6. laplace-deadlock-bar-nobuf.prom           12,402
7. laplace-ghost.prom                       527,036
8. laplace-ghost-flag.prom                   35,391

The additional files

laplace-deadlock-main.prom
laplace-partial-deadlock-main.prom

contain material that is shared by other files.

Spin version 4.1.0 of 6 Dec 2003 was used.  The exact sequence of
commands to arrive at the data is as follows:


spin -a laplace-deadlock-nobar-buf.prom
cc -o pan pan.c -DSAFETY
./pan -n

spin -a laplace-deadlock-nobar-nobuf.prom
cc -o pan pan.c -DSAFETY
./pan -n

spin -a laplace-partial-deadlock-buf.prom
cc -o pan pan.c -DCOLLAPSE
./pan -n -a

spin -a laplace-partial-deadlock-nobuf.prom
cc -o pan pan.c
./pan -n -a

spin -a laplace-deadlock-bar-buf.prom
cc -o pan pan.c -DSAFETY
./pan -n

spin -a laplace-deadlock-bar-nobuf.prom
cc -o pan pan.c -DSAFETY
./pan -n

spin -a laplace-ghost.prom
cc -o pan pan.c -DSAFETY
./pan -n

spin -a laplace-ghost-flag.prom
cc -o pan pan.c -DSAFETY
./pan -n

