New GreatSPN Editor is a Graphical User Interface for the GreatSPN framework and for the MC4CSLTA 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).
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.
The (very old) MC4CSLTA command line solver can be downloaded from here.
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:
The editor works on multi-page projects, saved in a readable XML format (pnpro format). Each page can be:
Multipage projects allow for an easier management of complex models, in particular when multiple DTAs are defined for a given set of GSPN models.
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.
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 MC4CSLTA model checker format, and can then be used to compute the probability of GSPN paths accepted by the exported DTA.
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.
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.
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.
The editor supports an interactive token game for GSPN nets, and an interactive CSLTA 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.
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.