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 latest version (1.5) of the New GreatSPN Editor can be downloaded here:
New GreatSPN Editor runs on Windows, MacOSX and Linux, including 64-bits variants of these platforms. Download and extract the application package for your platform, and double click on the application executable (exe file, application bundle, jar file). New GreatSPN Editor requires Java version 1.6 or higher to run. Linux version requires the sharutils package for the installation process. The editor is built using a command line LaTeX provider, whose source code is available here (GPL version 2 license with linking exception).
NOTE: on MacOSX it could trigger an error that says "GreatSPN Editor cannot be opened because it is from an unidentified developer". In that case, open the System Preferences > Security & Privacy > General, and allow the application to run on your Mac (see this guide for additional help).
The 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.