jHypernets

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.


Design of the tool
design picture

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.


Downloads

Installation

Minimal setup allowing to use the tool consist of:

After downloading the binary package with jhypernets, unzip it, edit JH.sh script 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

Compliation

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

$ make

To compile Java component's sources, please see Ant's build.xml file contained in the package and see available compile/run targets.


Usage

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.


Implementation notes

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.


Changes

Authors

Programming:

Supervision and theoretical support:


License
This software is licensed under GPL v.2.

Contact
If you have comments, ideas or problems with the tool, please write to  asiekiel at manta.univ.gda.pl  or  jslawins at manta.univ.gda.pl