NIPS is currently in use at several academic sites, among them:
I've found nips_c / nips_vm a very useful tool, thanks a lot for writing it! During last few weeks I've used it with many existing promela models that were originally written for spin.
Create a new empty directory and download the above tarballs into it:
mkdir vmssg cd vmssg wget "http://www.ewi.utwente.nl/~michaelw/nips/nips_vm-1.2.4-2006-03-14.tar.bz2" wget "http://www.ewi.utwente.nl/~michaelw/nips/nips_c-1.2.3-20060203-source.tar.bz2"
Ensure a recent C-compiler (e.g. gcc 3.x) and Java-SDK (e.g. JDK 1.5.0) are installed.
First, unpack the tarball. If needed, adapt the programs (compiler, ...) and flags in the header of "Makefile". Then compile:
tar jxf nips_vm-1.2.4-2006-03-14.tar.bz2 ln -s nips_vm-1.2.4-2006-03-14 nips_vm cd nips_vm makeRun some example benchmarks to check if the VM works:
cd tests make make benchmark
Unpack the tarball, then compile:
tar jxf nips_c-1.2.3-20060203-source.tar.bz2 ln -s nips_c-1.2.3-20060203-source nips_c cd nips_c antCompile some Promela programs into byte code, e.g. the already preprocessed (cpp -C -P) Spin example "eratosthenes":
./CodeGen examples/eratosthenes.pr
cd nips_vm/tests/spin ./benchmark-all.sh
To Store or Not to StoreReloaded: Reclaiming Memory on Demand
Other Papers:
Vergleich von Algorithmen für den Leerheitstest von Büchiautomaten, in german)
The following papers have draft status and are only available in German. They are also slightly outdated by now.