The home of the New GreatSPN Graphical Editor.

A new graphical editor for drawing GSPNs and DTAs for the GreatSPN framework

New GreatSPN Editor is a Graphical User Interface for the GreatSPN framework and for the MC4CSL^TA command line model checker (that can be found here). It is an interactive editor, written in the Java language, that can be used to draw Generalized Stochastic Petri Nets (GSPN) and Deterministic Timed Automata (DTA).

Installation

The standalone GreatSPN editor has been discontinued, and has been replaced with a portable self-installing version of the GreatSPN framework. Go to the GreatSPN repository to have all the information on how to download and install the Editor and the pre-compiled solvers, or on how to compile everything from sources.

Go to the GreatSPN page to download the Editor!

The (very old) MC4CSL^TA command line solver can be downloaded from here.

The interface of the editor

The tool shows a SDI interface with multiple open projects, and multiple schemas. It supports most of the capabilities expected from a modern editor, like cut/copy/paste of elements, editing with undo/redo support, interactive editing and high quality drawings.

The structure of the main window is the following:

Features

Projects with multiple pages:

The editor works on multi-page projects, saved in a readable XML format (pnpro format). Each page can be:

a GSPN model
a DTA for CSL^TA queries
or a list of performance queries.

Multipage projects allow for an easier management of complex models, in particular when multiple DTAs are defined for a given set of GSPN models.

Flexible language for GSPNs:

GSPN models can be described and drawn with a rich set of graphical elements, that include general/immediate/exponential transitions, labels with expressions, named constants and template constants, support to N-servers policies, and more. The editor supports also colored Petri net, using the SWN formalism, and hybrid Petri nets.

In addition, GSPNs can be exported in the GreatSPN file format, and can interoperate with the GreatSPN toolchain.

Flexible language for DTAs:

DTAs can be described in a purely graphical form, using locations, edges, state propositions, action names, etc... Template Ids allow to specify model-indepentent DTAs, that can be reused across multiple GSPNs.

DTAs can be exported in the MC4CSL^TA model checker format, and can then be used to compute the probability of GSPN paths accepted by the exported DTA.

High-quality schemas with LaTeX labels:

GSPNs and DTAs are drawn with an high-quality vector based renderer, with LaTeX labels and full support to LaTeX strings for object names. Schemas can be printed to a PDF/PS printer and exporting in vector format for publications, preserving the vector quality in print. Formulas, expressions and labels of places, transitions, DTA locations and so on, are all drawn with the LaTeX engine that allows for precise representation of mathematical formulas and objects.

The editor uses the excellent open-source Java-based LaTeX engine JLaTeXMath as external typesetting engine. The source code of the command-line LaTeX engine is under GPL license and can be downloaded here .

WYSISWYG editing:

Full support to modern WYSIWYG editing, including automatic grid alignment of elements, double click on labels to change their value, editing gizmos for resizing and rotating objects, etc.

Alternatively, the editor supports multi-selection of nodes and arcs of the schema with editing of the common properties from the property editor.

Vast selection of objects:

GSPNs and DTAs can be drawn with a vast selection of nodes, locations, transitions, clocks, expression objects, that allows for a simple and coincise representation of the model. Each of these elements is drawn with an appropriate representation, easing the readability of the diagrams.

Interactive token game and model checking:

The editor supports an interactive token game for GSPN nets, and an interactive CSL^TA model checking simulation of path trajectories of a GSPN controlled by a DTA. Interactive simulation makes it easier to understand the behaviour of GSPN models. DTA behaviour is shown by running the automaton side-by-side with the checked GSPN.

Developers

The current developer and mantainer of New GreatSPN editor is Elvio G. Amparore, who have worked on it under the supervision of Susanna Donatelli. If you want more informations on the tool, please write an e-mail to amparore (at) di.unito.it or to susi (at) di.unito.it.