NIPS VM
A Virtual Machine for State Space Generation

Important Notice!

If you intend to use NIPS in new projects, please contact Michael Weber beforehand. For benchmarking purposes, we are working on alternatives, which compile PROMELA models to C code.

Download

NIPS Virtual Machine

NIPS PROMELA Compiler

SARN (Static Analysis and Reduction for NIPS)

Installation Instructions

  1. Preparations

    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.

  2. Virtual Machine

    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
make
    Run some example benchmarks to check if the VM works: 
    cd tests
make
make benchmark
  3. Compiler

    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
ant
    Compile some Promela programs into byte code, e.g. the already preprocessed (cpp -C -P) Spin example "eratosthenes": 
    ./CodeGen examples/eratosthenes.pr
  4. Some benchmarks against Spin 
    cd nips_vm/tests/spin
./benchmark-all.sh

Papers

Other Papers:

The following papers have draft status and are only available in German. They are also slightly outdated by now.