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.