VMSSG Statespace Converter v1.0

1. Introduction

The purpose of the VMSSG statespace converter is to process statespace graphes produced by a modified version of the VMSSG virtual machine (but the input format is so simple, any graph-generating program will work), analyze it, and then display the graph in some understandable manner.

2. Software dependencies

The VMSSG virtual machine by Schuermans and Weber can be found here:
http://www-i2.informatik.rwth-aachen.de/Research/vmssg/
It needs to be compiled with a special output file, graphout.c, which is supplied in the "external" directory.

The Walrus graph visualization tool can be found here:
http://www.caida.org/tools/visualization/walrus/
Walrus uses the Java3D API, which can be found here:
http://java.sun.com/products/java-media/3D/
A Linux implementation of the native interface of Java3D is provided by the Blackdown Java implementation:
http://www.blackdown.org/java-linux/java2-status/java-3d-status.html

POVRay is included in most standard Linux distributions. It can be obtained (for other OS) at:
http://www.povray.org

For partitioning, a tool called METIS is employed. It can be found here:
http://www-users.cs.umn.edu/~karypis/metis/metis/

For viewing 2D graphs, the ZGRViewer is recommended:
http://zvtm.sourceforge.net/zgrviewer.html
Also, there exists an output handler for the GUESS viewer:
http://graphexploration.cond.org

(It should be mentioned that all this tools are open source, and are among the finest I've encountered so far.)

Finally, the converter itself is written in Java 1.5, with the obvious dependency. For betweenness centrality calculation, a JNI interface has been implemented, which is currently only available for Linux. However, the sources are provided in the "external" directory and can be compiled for any system.

3. Usage

Basically, the (recommended) usage of the converter goes like this:

java -Xmx700m -Xms300m -Djava.library.path=./lib -cp bin:lib/mp.jar:lib/vecmath.jar GraphConverter <input.graph> <preparator> <handler> <preparator-parameter> <handler-parameter>

The -Djava.library.path=./lib option is required only if betweenness centrality is used. <input.graph> is the input file, as provided by the VMSSG extension, in the format given below. <preparator> is the (prefix of a) Java class name of some preparation handler. Currently implemented preparation handler are:

SCC : Use Tarjan's algorithm to identify strongly connected components. Nodes are colored accordingly to the SCC membership. No parameter.
Partition : Uses the METIS tool for partitioning the statespace in k partitions, with minimal cut. As a parameter, the number of partitions is required.
BC : Use the Brandes algorithm for calculating betweenness centrality values for the node. Two parameter are required: treshold and mode, described below.
NodeWeight : Simply calculates the weight of the node, i.e. the number of all incoming and outgoing transitions. Two parameter required: treshold and mode.
NodeIncoming/NodeOutgoing: Count the number of incoming/outgoing transitions. Requires treshold and mode.

For the latter preparators, the parameter treshold and mode are required. mode is either "absolute", "absolutenormal" or "relative". For "absolute", treshold gives the value of the node, and nodes with a higher value are marked. "absolutenormal" works just the same, but first normalizes the nodes value to fit within [0..1]. "relative" requires a treshold in [0..1] and marks the top treshold*100 percent of the nodes.

The output handler then exports the graph in some format, that can be processed by graph viewers or other tools. Currently implemented are:

DotLight/DotFull : Output the graph in DOT format. DotLight just adds the node number as node label, DotFull the full description.
POV : Output the graph in POV format. The output itself consists of macro invocations, so it needs to be included in the main.pov file provided in the "external" directory. Note that currently the camera in the main.pov file needs to be set manually.
Walrus : Output the graph in the Walrus format. For displaying the node color in Walrus, select the node color to be "RBG" prior to "Start Rendering" (or use "Update Rendering"). Add a parameter "moves" to the converter invocation to have the edges colored according to the process that is about to move.
Statistics : Outputs some statistics on the graph
PartitionEdge : Outputs the edges between partitions (or SCCs, or generally all nodes given different values in the preparation phase).
GUESS: Outputs the graph for the GUESS graph viewer, which is capable of displaying smaller (approx. 200 nodes) graphs.

4. Input format

Basically, the input format is a log of the interation of states.
A state is given by a header line, consisting of "<stateid> : <depth_in_spantree>". This line is followed by an arbitrary number of lines giving the state description, which are terminated by a line consisting of four dashes: "----".
After this line, the transitions are given like this: "<src_id> -> <target_id>". They are independent of the state given before, so src_id can be any value. We treat the spanning tree differently (as it is required by the Walrus tool), so spanning tree transitions should be marked as "<src_id> => <target_id>". Each transition may be succeeded by a ": <processId>" suffix, which indicates the process that moved, with the following preselected IDs:

-2 : No process moves
-1 : The never claim moves
0 : A process is instantiated or removed
i > 0: The normal process with id i moves

The block of transitions is ended by the status line of a new state, or by the end of the file.

5. A quick walkthrough

(We assume that we are using Linux.)
Given a SPIN model named <model>, first use the cpp preprocessor:

cpp -C -P -o <model>.pr <model>

Then build the bytecode (with nips_c referring to the directory where the VMSSG compiler is installed, and nips_vm the installation directory of the VM)

nips_c/CodeGen <model>.pr
nips_vm/nips_asm.pl <model>.pr.s

Applying path reduction is recommended:

java -Xmx800m -cp ../pathreduct/bin proposal.PathReduction <model.pr.b $1.red.b

You may try the model checker

nips_vm/nips_vm -D 10000 <model>.pr.b

We then use the graphout.c-compiled version of the VM to extract the statespace:

nips_vm/graphout <model>.pr.b

Then we convert the statespace to walrus and POV format, using SCC markings:

java -Xmx800m -cp bin GraphConverter <model>.pr.b.graph SCC Walrus
java -Xmx800m -cp bin GraphConverter <model>.pr.b.graph SCC POV

Finally, we run POVRay to generate the state space visualization (note that the camera perspective is not yet calculated automatically)

cp <model>.pov main.inc
povray +D00 +FN8 +W640 +H480 +A0.3 +O<model>.png  main.pov

6. Further notice

I took some code from the Walrus viewer to layout the graph for the POV output. Walrus is published under the GPL, therefore this program is published under the GPL as well (and would have been even if I had the skills to write a hyperbolic graph layout on my own).

GPL Copyleft License

A gallery of state space rendered with the POVRay raytracer can be found at my state space visualization gallery.

Contact me at hammer "at" pst.ifi.lmu.de.