=Paper=
{{Paper
|id=Vol-1372/paper9
|storemode=property
|title=Reengineering the Editor of the GreatSPN Framework
|pdfUrl=https://ceur-ws.org/Vol-1372/paper9.pdf
|volume=Vol-1372
|dblpUrl=https://dblp.org/rec/conf/apn/Amparore15
}}
==Reengineering the Editor of the GreatSPN Framework==
https://ceur-ws.org/Vol-1372/paper9.pdf
Reengineering the Editor of the GreatSPN Framework
Elvio Gilberto Amparore
Università di Torino, Dipartimento di Informatica, Italy
amparore@di.unito.it
Abstract. This paper describes the technical challenges around the moderniza-
tion process of the GreatSPN framework[15], one of the first Petri net frame-
works started in the eighties, in particular in the reengineering of its Graphical
User Interface and in its general user-friendliness, to account for its large set of
functionalities1 .
Keywords: GreatSPN, GUI, Dataflow architecture.
1 Objectives and contributions
It is common opinion that formalisms like Petri nets or Timed Automata are very pow-
erful and yet simple to understand thanks to their graphical representation. A graphic
schema is usually simple to specify and grasp. However, graphical formalisms depends
on the availability of good graphical editors to be able to gain the full advantages.
Back in 1985, the University of Torino developed the (probably) first documented
software package for the analysis of stochastic Petri nets, under the name of Graphical
Editor and Analyzer for Timed and Stochastic Petri nets (GreatSPN) [15]. The frame-
work consisted in a set of tools for the analysis of Generalized Stochastic Petri nets
(GSPN) [1], and it was supported by a graphical editor, described in [16], for inter-
actively design, validate and evaluate GSPN models. The graphical editor, developed
initially on a Sun 3 machine with UNIX BSD 4.2, was based on the X11/Motif toolkit.
The simplicity of graphically designing models boosted the usage of GSPNs in vari-
ous fields, from performance evaluation, telecommunications, biology and more. Other
tools/GUIs have then followed, providing nowadays a large base of Petri net tools.
Today, the GreatSPN framework provides a vast collection of solvers developed in
a time span of 30 years, that includes solvers optimized for low memory consumption
(for the computers of the late ’80s), modern model checkers based on decision diagram
techniques [3], a stochastic model checker, ODE/SDE2 solvers, Markov decision pro-
cess optimizers, DSPN [23] solvers, simulators, and others. While the set of solvers of
GreatSPN is very large, the obsolescence of technologies like Motif hurt the usability
of the GUI over the years. After having evaluated other GUIs, the group arrived to the
decision of renewing the interface of GreatSPN. The modular nature of the framework
itself allows to easily replace solvers, modules and the GUI itself, while maintaining
1 This work has been funded by the Compagnia di San Paolo, as a part of the AMALFI (Ad-
vanced Methodologies for the Analysis and management of the Future Internet) project.
2 Ordinary and Stochastic Differential Equations.
154 PNSE’15 – Petri Nets and Software Engineering
the other modules fully working and unchanged. In the end, the modular framework
structure proved to be easy to maintain and to develop over such a long timeframe.
This paper describes the reengineered GUI of GreatSPN, with its recent enhance-
ments. The GUI is written in Java, and it is therefore portable to multiple platforms. En-
hancements include, among all, support for drawing colored Petri nets and hybrid Petri
nets, token game, batch measure specification and processing, and support for multiple
solvers/model checkers. The paper describes the overall tool workflow, from the mod-
eling and the verification phase, that allows to edit models, simulate their behaviors,
inspect their structural properties, up to the evaluation phase, where performance in-
dexes are computed with numerical solvers and/or simulators, and the computed results
are visualized interactively to the user. A prototype of the GUI was briefly described in
a short paper [5], centered around its use for stochastic model checking.
The GUI supports multiple formalisms: Generalized Stochastic Petri Nets (GSPN),
GSPN with colors (Stochastic Well-Formed net, or SWN), Hybrid Petri nets, and De-
terministic Timed Automata (DTA). In addition, the application presents a number of
unique features, like multipage projects, solution batches, support for template variables
in models, LATEX labels and high quality vector graphics. This new GUI is described
here with a focus on various recent additions: parametric measure specification, the
support for SWN and hybrid Petri nets, and the integration inside the framework.
The modernization process actually required a process of re-engineering of the GUI
around the workflow of GreatSPN. During this process, many limitations of the existing
GUI have been removed, like the absence of a SWN token game, the missing support
for model checkers, no capacity for drawing Timed Automata, and other. The main
contributions provided by the modernized GreatSPN GUI are its improved usability,
while keeping the compatibility with the large framework, and its support to multiple
formalisms and solvers, which expands the tool usability. Other formalisms and other
solvers may be added using the modular tool structure.
Section 2 describes the architecture of the GreatSPN framework. Section 3 and 4
introduce the application interface, and describe briefly the modeling capabilities of
the editor. Section 5 shows how the user can simulate the designed GSPNs with the
token game, and visualize their structural properties like the minimal P/T semi-flows.
Section 6 describes how the designed models can be verified quantitatively with the set
of supported solvers. Section 7 shows a simple use case of the tool that illustrates how
the GUI can help the user in the process of modeling and analysis. The paper concludes
with a comparison of other commonly used GUIs in section 8 and with the section 9
with a brief discussion on the future of GreatSPN.
2 Architecture of GreatSPN
GreatSPN is a large framework made by several interacting components, that has grown
over the time to incorporate various Petri net-related features. The framework itself is
not made by a large, monolithic tool. Instead, many independent tools interact by shar-
ing data through files in standardized formats, resulting in a dataflow architecture ap-
proach. Each tool is responsible for reading its own input, written in one or more files,
performing the computation, and writing the outputs in other files. The framework actu-
E. Amparore: Reengineering the Editor of the GreatSPN Framework 155
GreatSPN Editor
Property MC4CSLTA
WaitAction
NextOp
Queue
GSPNModel
2
FastQueue
Project
GSPN Sample
as DTA Stochastic model Model
UntilDTA
GSPN 3
(.dta)
CountArrivals
FastQueue
Measures
ExpPInv checker for CSL/CSLTA checking
complete
CSLTA
EXPTInvMeasures
¹ = 1:5
¸=2 ¹
results.
End N=3
Node properties K=3 timeout
Wait Release
ID: Packets2
Label: Default
arrivals
¸
T = 2:35
arrivals
CTL RGMEDD
2 im req N+1 start N+1
query CTL model checker with
Queue ¼=2
Packets1
¸=2
1 server End (.ctl)
Magnets: Center only norm req start 2 decision diagrams
Tags:
Place properties
LpQueue
K
Packets2
¸ Model checking.
Initial marking: K
Ok: object selected. 100 %
Bounds computed with
lpbound Linear programming
Graphical Editor of GreatSPN
Ok. 100 %
traps Deadlocks, traps
P/T-
pinvar/ invariants
gsol tinvar (.pin / .tin)
PNML
PNML rev.2009 -> Performance
model
(.pnml) Petri net (GSPN or Place bounds indexes
GSPN results.
SWN) translation model struct Conflict sets
(.bnd / .ecs)
(.net / .def)
Structural analysis.
UML ArgoSPE
schema Eclipse UML ->
(.uml) Performance
Petri net translation gst_prep gst_stndrd
indexes setup.
unfolding
SWN -> GSPN GSPNRG Steady-state
ggsc solution.
translation SWN GSPN only
model
(.net / .def) Reachability Transient
algebra WNRG graph ntrs solution.
Composition of multiple Ordinary RG
models by place/ Numerical solution.
transition superposition
WNSRG
Symbolic RG
Translation/Composition system. Reachability
RG computation and analysis. v_graph graph in PDF
MDWN* GSPNSIM
mdwnsolve MDP from Markov GSPN only
MDP solution Decision Petri net Estimated
formalism. results of the
WNSIM
Performance
Ordinary markings
Optimal indexes.
strategy
mdwn2Prism
WNSYMB
MDP in Prism format
Symbolic markings
Simulation engine.
MDP generation and optimization.
DSPN-Tool
Steady-state MRP
DSPN solution.
Fig. 1. (Partial) Architecture of the GreatSPN framework, as it is today.
ally contains more than 60 binaries. The advantage of this software architecture is that it
allows to easily modify/replace single components, while keeping the rest of the frame-
work unchanged, as long as the input/output formats are observed. While this software
architecture is not very modern, it has proven to be very solid and maintainable, such
that in the framework many software modules written in its 30 years of development
co-exists, without causing too many troubles.
A simplified schema of the GreatSPN framework is shown in Fig. 1, that reports a
selection of the various features of GreatSPN. Tools are written in bold, and are grouped
in logical modules, according to their function, that span from numerical solutions,
structural analysis, MDP support, conversion between multiple formalism, and so on.
The graphical editor is the center for drawing the models and their properties. It is
responsible for the invocation of various command line tools and for the visualization
of the results. Actually, many but not all the command line tools are available from the
GUI.
156 PNSE’15 – Petri Nets and Software Engineering
The workflow of GreatSPN was conceived, back in its original design, to be made
in three main phases: first the user (the “modeler”) designs the Petri net in a textual or
graphical way; secondly, structural properties are computed (minimal P/T semi-flows,
place bounds, conflict sets, ...) to understand if the model is designed properly and may
be solved under numerical analysis or simulation; then the user specifies the measures
of interest on the model and calls a command line solvers to do the computation. Several
solvers are provided, for different types of models and with different characteristics.
2.1 Reengineering requirements.
In order to create a new GUI that replaces the old one, it must satisfy a set of re-
quirements and constraints imposed by the framework itself. First of all, the GUI is
responsible of these tasks:
1. Help the user in the process of drawing Petri net models and other graphical models.
2. Allow the user to call the tools provided by the GreatSPN framework for the struc-
tural analysis of Petri net models, to discover potential structural mistakes made in
the drawn models.
3. Simplify the process of specifying and computing performance measures, by call-
ing the command-line solvers and providing an understandable visualization of the
computed results.
The design choices done to satisfy requirement 1 are explained in sections 3 and 4.
Requirements 2 and 3 involve the interaction between the GUI and the command line
tools. Command line tools expect precise file formats in input and produce other files as
output, since these tools are designed to be non-interactive. Therefore, the tool interac-
tion with the solvers require an explicit serialization of the data for the computation and
a deserialization of the results. Many different files are involved in any computation: a
partial list of these files is shown in Table 2.1.
Extension Content of the file
.PNPRO Petri net Project (XML format). Main format of the editor.
.net Input format of Petri net models for command line solves.
.def Input performance indexes.
.ctl Qualitative queries in CTL language.
.dta Deterministic timed automata for CSLTA model checker.
.pin, .tin P/T invariants.
.sta Computed statistics.
.throu Transition throughputs.
.tpd Token distributions in places.
.ecs Extended conflict sets.
.bnd Upper/lower bounds of tokens in places.
.grg Reachability graph.
Table 1. File extensions of the input/output files used by the editor and the solvers).
E. Amparore: Reengineering the Editor of the GreatSPN Framework 157
The complete solution process of a Petri net may require the invocation from one to
twelve different command line tools, depending on the target measures to be computed.
In addition, the reengineered workflow has been improved to support parametric mod-
els, i.e. models defined to depend on multiple integer/real parameters, whose values are
specified at solution time and not at design time. Parameters are passed as command
line arguments, and all command line tools have been modified to support them.
Another design requirement of the GUI is to support new modeling formalisms and
functionalities that are not present in the current toolchain. To represent and store these
informations, the tool uses a new XML file format for the models. This choice avoids
modifying the input file formats of the toolchain. Any command line tool invocation
serializes the drawn model in appropriate input formats when needed, leaving the main
file format just for the editor. In this way, it is easy to change the editor format without
breaking the compatibility with the command line tools of the GreatSPN framework.
Requirements 2 and 3 involve the reconstruction of the modeler workflow of Great-
SPN inside the GUI. Examples of how this workflow is implemented graphically are
given in sections 5–7.
2.2 Code structure of the new GUI.
The GUI consists of about 55K lines of code written in the JavaTM language, plus an
optional command line LATEX engine that runs in the background to format the text
labels of the models. The application is cross platform and runs on Windows, MacOSX
and Linux. Java package structure is shown in Table 2.2.
Packages Description
gui Core GUI structure, main window cycle.
gui.net Visualization/editing of abstract graphs (Petri nets, automata).
gui.play Interactive token game.
gui.semiflows Visualization of minimal P/T semi-flows.
gui.measures Editing of measures and visualization of computed results.
domain Data structures.
domain.project File management, undo/redo facility.
domain.grammar Unified ANTLRv4 grammar for expressions and measures.
domain.io Serialization/deserialization in net/def, XML and APNN formats.
domain.values Expression evaluation engine.
domain.elements.gspn GSPN elements.
domain.elements.dta DTA elements.
domain.play Token game logic.
domain.semiflows Computation of minimal P/T semi-flows.
domain.measures Measure specification and tool invocations.
domain.unfolding Unfolding of colored Petri nets into uncolored ones.
Table 2. Code structure of the Java application.
The core structure of the design view of the GUI is essentially an editor for abstract
graphs of nodes and edges. The version described in this paper supports two graph
158 PNSE’15 – Petri Nets and Software Engineering
formalisms: Petri nets and automata. New formalisms can be added by deriving the
corresponding base classes in the Java codebase. Adding a new formalism is done by
deriving the base classes for the model, the node elements and the edge elements, and
by providing the Java panels to edit properties. For instance, the DTA formalism, imple-
mented in the domain.elemens.dta package, involves about 2K lines of code: two Java
classes for the DTA locations and edges (the graph nodes), a class for the DTA model
in a project, and the property panels for the location and edges. Of course, other part of
the application that use DTAs also involve some additional logic. To abstract different
syntax of properties, measures, expressions, provided by various solvers, the GUI has
a uniform C-like language for expressions. When an expression needs to be passed to a
solver, it is converted to the specific syntax expected by the tool. Abstracting expression
languages of different solvers allows to support multiple solvers without having to re-
specify expressions and measures for different tools. Overall, the complete GreatSPN
framework amounts to about 500K lines of code, mostly made by C/C++ programs.
3 Drawing Petri net models
The core feature of the editor is the drawing of Petri net models, centered around the
GSPN, the SWN and the Hybrid Petri net formalisms. Figure 2 shows the main appli-
cation window, taken while editing a colored Petri net model. In the upper-left panel,
there is the list of open projects. The editor is designed around the idea of multi-page
projects. Each project correspond to a file, and is made by several pages. In the current
version of the editor, pages can be of three types: Petri net models, DTA models or table
of measures. In the lower-left panel of the main window there is the property panel, that
shows the editable properties of the selected objects. The central canvas contains the
editor of the selected project page, that is in this case a SWN model.
Petri nets are drawn with the usual graphical notation. Transitions may be immediate
(thin black bars), exponential (white rectangles) or general (black rectangles). Names,
arc multiplicities, transition delays, weights and priorities are drawn as small movable
labels near the corresponding Petri net elements. Arcs may be “broken”, meaning that
only the beginning and the end of the arrows are shown. Color definitions are drawn in
textual form, as in the upper right part of the window where two color classes, a com-
posite color domain and two color variables are declared. The editor also supports fluid
places and fluid transitions (not shown in the example of Fig. 2), and place partitions
for Kronecker-based solutions [11]. The editing process supports all the common oper-
ations of modern interactive editors, like undo/redo of every actions, cut/copy/paste of
objects, drag selection of objects with the mouse, single and multiple editing of selected
objects, etc. Great care has been put to the graphical quality of the resulting Petri net
models, to allow for high quality visualization of the net. The interface is designed to
avoid modal dialog windows as much as possible, to streamline the use of the GUI.
Figure 3 shows some of the extended features of the Petri net editor. Name labels for
elements (places, transitions, constants, etc) may appear in three user-selected modes:
– The label shown is the alphanumeric object identifier, as-is;
– A LATEX string is used, allowing for more readable models that better express their
meanings, like in the simple reaction network of Fig. 3(A) where alphanumeric
E. Amparore: Reengineering the Editor of the GreatSPN Framework 159
Fluid Line
FluidImmediate
ColorSemanticTest
ConcurrentGen
Database
NextOp
CPN Measures
NextOp PN wait mutex : S£F mutex : F class S = circular sf1::4g var s : S
hs; fi hfi class F = enum ff1::3g var f : F
hAlli
hs; fi hfi
Node properties domain S£F = S £ F
Start Acquire
ID: mutex 1:0
hs; fi hsi
hsi
Label: modify : S£F
hAlli all active : S hAlli all passive : S
message : S£F rec buf : S£F
hAll ¡ s; fi hs; fi hs; fi hs; fi
hs; fi hsi
hsi
1:0
Center only Change SendMessage Update
Magnets:
1:0
hs; fi
Tags: hs; fi
Place properties wait ack : S£F updating : S£F
Type: Discrete
hs; fi hs; fi
Initial marking:
Release EndUpdate
acknowledge : S£F reply buf : S£F 1:0
Kronecker partition: hAll ¡ s; fi hs; fi hs; fi hs; fi
1:0
Color domain SendReply
Color domain: F
Ok: object selected. 100 %
Fig. 2. The old and the new graphical user interfaces of GreatSPN. Screen-capture of the former
is taken during the interactive token-game, while the SVG capture of the latter shows the design
view with a colored Petri net model.
160 PNSE’15 – Petri Nets and Software Engineering
H2 ¸ synt = 0:7588
N load
2
2H2 + O2 ! 2H2O Machine
O2 start interm end
K ¸ synt 2 N
H2O stage 1 stage 2 Complete
Pallets
(A) Models can use LaTeX labels to fail repair
improve the visual presentation of the N=3
model elements. All labels (including Broken
arc multiplicities) are fully movable.
(B) Customizable magnetic points where arrows can attach.
Fig. 3. Some features of the Petri net editor.
transition names are replaced with the represented chemical reaction, and place
names represent the chemical species.
– The label is the object identifier automatically formatted in LATEX with a function
that tries to convert common patterns (like alpha → α, or stage1 → stage1 ).
Arc arrows point to the center of the attached transitions/places. If this behavior
is not satisfactory, the editor provides a set of customizable “magnetic points” drawn
on the element perimeters, where the arrows may attach. This behavior is shown in
Fig. 3(B), figure that has been taken while dragging the arc arrow with the mouse on
the “start” transition that has “3 magnets per side”. All elements in the model are vector
based, which result in high print quality. Printing and PDF exportation of the models
are also possible, using the printing facilities of the operating system.
Figure 4 shows a colored model, drawn using the SWN formalism, as it appears in
the editor window. Support for SWN has been recently added to the GUI. The model has
three objects, located in the upper left part, that represents object declarations. The hNi
objects declares a parametric integer constant, whose value is decided at verification
time. The ‘class’ declaration defines a color class for the places in the Petri net, as
usual in the SWN formalism. Places belonging to this color class are labeled with the
place name followed by a colon and the color class name. The third declaration is a
color variable named x of color class Philo. All expressions are parsed and verified
syntactically and semantically on-the-fly, and appear in red if there is some error.
4 Drawing CSLTA DTAs
The second type of models that can be drawn with the editor are Deterministic Timed
Automata (DTA), a type of timed automata for the CSLTA stochastic logic [19]. CSLTA
works by measuring stochastic GSPN behaviors using a DTA. A DTA is an automaton
that reads the language of GSPN firing sequences (also called paths), and separates
accepted and rejected paths. The formal semantic of the DTA can be found in [19]
(single clock), and in [14] (with multiple clocks). In few words, the logic provides a
stochastic operator: s0 |= P./λ (A) that is satisfied iff the overall probability of the set
of GSPN paths starting in state s0 and accepted by the DTA A, is ./ λ .
Figure 5 shows three CSLTA DTAs, drawn with the notation described in [4]. The
first DTA describes the CSL [7] path property: Φ 1 Until[α,β ] Φ 2 . Locations are drawn
E. Amparore: Reengineering the Editor of the GreatSPN Framework 161
hNi
class Philo = circular pf1::Ng
var x : Philo
Think : Philo
hxi
hAlli
hxi hxi hxi
hx++i
FF1a FF1b
hxi hxi
hAlli
Fork : Philo Catch1 : Philo Catch2 : Philo
hxi hxi
FF2a FF2b
hxi hxi hxi hx++i
hxi+hx++i
end
hxi
Eat : Philo
Fig. 4. Model of the N dining philosophers drawn in the SWN formalism.
as rounded rectangles, and the state proposition that the GSPN must satisfy while the
DTA is in a location is written below the location rectangle, in bold. Initial locations are
represented with an entering arrow, and final locations are drawn with a double border.
The editor also allows final rejecting locations, not included in the original definition,
but used in [2]. There are two kinds of edges, boundary, drawn dashed, and inner,
drawn solid. Boundary edges are triggered as soon as the clock condition is satisfied,
and are labeled with a ]. Inner edges specify the set of GSPN actions with which they
are synchronized. Each edge also specify a set of clock constraints, and an optional set
of clock resets.
h®i h¯i h©1i h©2i x 1 : clock h®i hBegihOki
Act x : clock h©0i hacti h®i
x<® x : clock x 2 : clock h¯i hMidi
Act n factg Act Act
] x<® factg x1 < ® x2 < ¯
l0 x=® lok l ok
x<®
©1 Act ©2 Act
®0
work1
work2 h©2i = #Finish1==#Finish2
Fork
Queue work 2
h®i = 3
l0 ‑> l1
Fork Wait2 Finish2 Join h¯i = 4
Time elapsed:
Token game is untimed. h®i h¯i h©1i h©2i
work 1 Act
Path trace: x<® x : clock
[l0] Spares=2, Queue=4 ¸ = 3:4
[l0] Spares=2, Queue=3, Wait2=1, Wait1=1 ¹ = 2:0 Wait1 Finish1 2
]
[l0] Spares=2, Queue=3, Wait2=1, Wait1=1 ½ = 0:6 l0 x=® lok
[l0] Spares=2, Queue=2, Wait2=2, Wait1=2 2 select T0 Act
©1 ©2
[l0] Spares=2, Queue=2, Wait2=2, Wait1=2
®