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.

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.

• Binaries
  • hhypernets-bin-linux-i386-1.2.84.tar.gz (2006-11-09) - Haskell component
  • jhypernets-1.2.123.tar.gz (2006-11-09)- Java component
• Sources
  • hhypernets-src-1.2.84.tar.gz (2006-11-09) - Haskell component (sources)
  • jhypernets-src-1.2.123.tar.gz (2006-11-09)- Java component (sources)

Minimal setup allowing to use the tool consist of:

• uDrawGraph
• Graphviz package
• JRE (Java Runtime Environment), version 1.5 or later

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:

• GHC (Glasgow Haskell Compiler)
• HaXml 1.15 (Haskell XML library)

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.

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.

• New in hhypernets version 1.2.80, compared to 1.1.71
  • Data structures are ADT now
  • Optimization of most data structures
  • Server now works through TCP/IP
• New in jhypernets version 1.2.116, compared to 1.0.94
  • Much of the internal structure has been refactored: new packages have been added, some method's names have been changed
  • XML serializing works now, with cooperation with hhypernets server configured to use XML
  • New functionality: hiding modules (facilitates cleaner presentation of hypernets)
• New in hhypernets version 1.1.71, compared to 1.0.62
  • XML format support for exchanging information between the Haskell component and the Java component. HaXml is a XML library we use.
  • Parameterizing exchange format usage. Now the new XML format can be used, as well as an old, based on Haskell lists representation.
  • General clenaup and removal of obsoloted code.

Programming:

• Artur Siekielski (Haskell component, except the Parser module, XML format in the Java module)
• Jakub Sławiński (Java component, TCL scripts and Haskell Parser module)

Supervision and theoretical support:

• Marek A. Bednarczyk
• Wiesław Pawłowski