jHypernets is a simulation and model checking tool for Petri Hypernets - a formal model of mobile computations. There are several papers available on the subject, including a gentle introduction to hypernets and a presentation the logic which jHypernets provides a model-checker for.
The tool consists of three components, as shown in the picture. uDrawGraph is a standalone application for graph visualization which can be used from external applications. It draws the model and is responsible for user interactions. TCL scripts can be used to extend functionality.
The Haskell server is a component implementing the semantics of the model. A state of the model can be queried and changed by means of some formally specified operations.
The Java mediator is a component that glues two other components. It is responsible for answering to user requests, which are passed by the uDrawGraph component, and translating them into commands that are understandable by the Haskell server.
Minimal setup allowing to use the tool consist of:
JH.shscript and adjust a path to uDrawGraph. Next, set JHYPERNETS_CONFIG environment variable to path where config.xml file is (it is provided in the jhypernets package).
You don't have to run Haskell component by yourself. A default one is running on our server. Provided config.xml file is set up to use it. If you want, you can download a binary version of the component (which consists of one executable file) and run it on your machine, then configure config.xml to reflect that fact.
Finally, please run the tool by the command:
$ java -jar jhypernets.jar
If you want to compile the Haskell component by yourself, install the following additionally:
After downloading and unpacking the Haskell component's sources, you must compile the server by running
To compile Java component's sources, please see Ant's build.xml file contained in the package and see available compile/run targets.
When the tool starts, a uDrawGraph window will pop up. A hypernet can be opened by choosing File->Open from menu. Editing/viewing instructions are shown after clicking Help->Mini-Help.
Please note that although we have used cross-platfrom programming languages and tools, jHypernets has mainly been used and tested uder Linux operating system.
In the current state, the tool must be regarder as a prototype rather than a final product. The model checking algorithm is a naive one, so model checking will work in reasonable time for very small models only.
We have implemented a (very) experimental simulator version that is capable of being used through WWW. It operates on hypernets written in XML and uses XSLT to transform them into description understandable by Graphviz tool, which generates pictures. Simple CGI scripts glueing together all that operations are written in Python. Implementation of this experimental version is provided in the jhypernets package in subdirectory script_sim.
Parsermodule, XML format in the Java module)
Supervision and theoretical support:
asiekiel at manta.univ.gda.plor
jslawins at manta.univ.gda.pl