This paper describes the technical challenges around the modernization process of the GreatSPN framework[15], one of the first Petri net frameworks 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. It is common opinion that formalisms like Petri nets or Timed Automata are very powerful 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 framework 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 interactively 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 various 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 process 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 (Advanced Methodologies for the Analysis and management of the Future Internet) project. 2 Ordinary and Stochastic Differential Equations.
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
enhancements. The GUI is written in Java, and it is therefore portable to multiple platforms.
Enhancements 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
modeling and the verification phase, that allows to edit models, simulate their behaviors,
inspect their structural properties, up to the evaluation phase, where performance
indexes 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 [
The GUI supports multiple formalisms: Generalized Stochastic Petri Nets (GSPN), GSPN with colors (Stochastic Well-Formed net, or SWN), Hybrid Petri nets, and Deterministic 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
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 sharing data through files in standardized formats, resulting in a dataflow architecture approach. 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 actuPerformance indexes results.
gst_stndrd ggsc ntrs v_graph
Steady-state solution.
Transient solution.
Reachability graph in PDF Estimated results of the Performance indexes.
Model checking results.
Bounds computed with Linear programming Deadlocks, traps
P/Tinvariants (.pin / .tin) Place bounds Conflict sets (.bnd / .ecs)
Performance indexes setup.
Stochastic model checker for CSL/CSLTA
CTL model checker with decision diagrams lpbound traps pinvar/ tinvar struct gst_prep
GSPN only
GSPN only
Ordinary markings
Symbolic markings
Steady-state MRP
Ordinary RG
Symbolic RG
Reachability graph 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 framework 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.
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 requirements 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 structural 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 calling 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 interaction 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.
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 models, 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 GreatSPN 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.
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 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, implemented 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 respecify 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
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 application 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
composite 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 [
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 Fluid Line FluidImmediate ColorSemanticTest ConcurrentGen Database NextOp CPN Measures
NextOp PN Node properties ID: mutex
Label:
Center only Magnets: Tags: Place properties Type: Discrete Initial marking:
<All> Kronecker partition: Color domain Color domain: F Ok: object selected. is taken during the interactive token-game, while the SVG capture of the latter shows the design view with a colored Petri net model.
wait mutex:S£F
hs;fi hfi hs;fi
Start 1:0 hsi hsi hAlli all active:S mutex :F hAlli
hfi Acquire hs;fi modify :S£F hs;fi hAll ¡ s;fi
message :S£F Change 1:0 hs;fi
wait ack :S£F hs;fi Release
acknowledge:S£F hAll ¡ s;fi hs;fi reply buf:S£hsF;fi hs;fi 1:0
SendReply hs;fi hs;fi 1:0 SendMessage class S = circular sf1::4g class F = enum ff1::3g domain S£F = S £ F var s : S var f : F hs;fi rec buf :S£F hAlli all passive :S
hsi Update hsi hs;fi hs;fi updating :S£F EndUpdate 1:0 100 % O2 K
H2 N 2 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 [
Figure 5 shows three CSLTA DTAs, drawn with the notation described in [
hxi hx++i hxi hxi hAlli
hxi end hxi+hx++i hxi
Think :Philo
hAlli hxi FF1a FF2a hxi hxi
hxi hxi hxi hxi hx++i
FF1b
FF2b Fork :Philo
Catch1 :Philo
Catch2 :Philo
Eat :Philo
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 [
Fig. 5. Some example of DTA models drawn with the editor.
DTAs are parametric, and are not bound a priori to a specific GSPN model. Instead, all state propositions, real clock boundaries and action names are declared as template variables (depicted as hvari). When the DTA is used for computating measures of a GSPN, these parameters are instantiated to boolean conditions, real values and transition names of the GSPN, as we shall see in section 5.1.
Clocks are declared as part of the DTA. The DTAs (A) and (B) of Fig. 5 have a single clock, while the DTA (C) has two clocks. Currently, only single-clock DTAs can be verified numerically. The DTA (B) accepts all the GSPN where a transitionact fires before time α, while remaining in states that satisfy the condition Φ0. 5 Interactive simulation and inspection of structural properties The behavior of Petri nets can be experimented interactively inside the GUI. This is known as the “token game” or “interactive simulation”, and works as follows. The editor shows thCelosien. itial maChraknginebgindoinfgsthe GSPN, and highlights the set of enable transitions of the model. By click on one of the enabled transitions, the editor responds by firing the tokens fPr-‐‑osmemiflthowes:input to the outputGpSPlNac1es, showing the behavior of the model. The reachMeindimmalasrukppionrgtsiesmitflhoewns: shown, andNth=e5user can continue firing new transitions.
Queue + 2*Wait1 + 2*Finish1 ¹ = 1:5
Queue + 2*Wait2 + 2*Finish2 ¸ = 3:4 P0 t0
T0 T1 1:0 1:0
P1 P2 D0
t1
P3 (A) Token simulation screenshot taken while firing immediate transition t1.
N
T = 1:0
N
1 Queue
2 2
Fork
2 Wait1 Wait2 work1 work2
2 Finish1 Finish2
Join (B) Interactive visualization of a P-semiflow of a GSPN.
P-semiflow multiplicities are written on the places.
Figure 6(A) shows this interactive simulation on a GSPN model, taken during the firing of transition t1. Tokens removed from input places and added to output places are drawn with a short animation. Token game works in untimed and timed mode. In untimOke.d mode, no age/duration of the events is considered, and no track is kept for the advance of time. In timed mode instead, a time is present, and the time for the transition fire is taken into account. For DSPN models with non-ex1p0o0n%ential transitions, timing constraints are resolved. The user may also enable a semi-automatic firingmode, where interaction is required only if there is a choice between multiple concurrently enabled transitions, or a random firingmode where the editor picks the next transition randomly (and the next time in timed simulation), thus simulating without the user interaction. SWN models are supported in interactive mode: instead of black dots, colored tokens are shown as color names. When firing a colored transitions, a list of enabling bounds of the color variables is shown to the user, who can pick the one to fire.
Additionally, the user may visualize the minimal P and T semi-flows that covers a
GSPN model, as shown in Fig. 6(B). The user selects the minimal semi-flow that wants
to visualize from a list, and the editor highlights the involved places and transitions.
Semi-flows are computed with the modified Farkas method of Martinez and Silva [
An interactive simulation of the path probability operator of the CSLTA logic is, roughly speaking, a system where GSPN firings are checked by the DTA. Each GSPN transition firing has to be matched by a corresponding DTA edge, otherwise the path is rejected. In addition, boundary edges of the DTA (labeled with a ] and drawn as dashed arrows) are autonomous and are taken as soon as their timing conditions are met. Before starting the simulation, the template variables of the models are shown as a list of text boxes, that must be filled by the user with appropriate values. Values assigned to the parametric variables of the DTA are shown above the DTA. In the central panel of the window, the GSPN and the DTA are shown side by side.
Close. Switch to Timed Semi‑automatic firing.
Random automatic firing.
Enabled Transitions: work1 work2 Fork l0 ‑> l1 Time elapsed:
Token game is untimed.
Path[l0t]raScpea:res=2, Queue=4 ¸ = 3:4 [l0] Spares=2, Queue=3, Wait2=1, Wait1=1¹ = 2:0 [l0] Spares=2, Queue=3, Wait2=1, Wait1=1 ½ = 0:6 [l0] Spares=2, Queue=2, Wait2=2, Wait1=2 [l0] Spares=2, Queue=2, Wait2=2, Wait1=2 [[ll00]]SSppaarreess==22,,QQuueeuuee==22,,WWaiati2t=2=2,2F,iFniinsihs1h=11=,1W,SaWpitaa1ir=te11s=1 Speed: Ok.
Start!
Figure 7 shows the GUI window for the joint simulation of a GSPN model and a DTA. The list of enabled GSPN transitions and autonomous DTA edges is shown in the upper-left corner. In the lower left corner there is the state of the path trace chosen interactively by the user, starting from the initial marking. Values assigned to the parametric variables are validated while typing, and their correctness is signaled with a green tick mark on the right of the corresponding text boxes. When all values are assigned, the user may press the play button and the joint simulation starts in the initial state of the GSPN and in the initial location of the DTA. Each time the user selects a GSPN transition to fire, a DTA inner edge has to be chosen afterwards to match the GSPN firing. Boundary edges of the DTA may also be independently enabled (clock condition is evaluated in a timed simulation, and ignored in an untimed one). The simulation ends when the DTA reaches a final location, or when no DTA edge can match a GSPN firing.
Solver: GreatSPN
Assigned Value: to: 8
step: 1
Max iterations: 10000 Add measure
Comment Target model: Database CPN Template parameters: Name: hni ranges
from: 1 Solver parameters:
Epsilon: 1.0e‑7 Solver mode: SWN Ordinary Measures: Pos: 1° 2° 3° CTMC solution is computed in:
Steady state
Simulation
Transient
at: 1.0
Measure: All place distributions and transition throughputs.
Plot of the Reachability Graph with vanishing markings.
E{ #Queue } The GUI integrates an interface for specifying, computing and visualizing measures on Petri net models. A project may contain multiple measure pages, and each page specifies: – The target Petri net model; – The selected numerical solver, from a list of supported solvers; – The instantiation of the parameters of model, if any; – Solver-specific parameters and flags; – A table of target measures that will be computed.
The GUI is currently integrated with three solvers. The first is the GreatSPN toolchain,
that can evaluate standard performance measures (mean number of tokens in a place,
transition throughputs, etc...) on GSPN/SWN models using an extensively tested
implementation. Index can be computed in steady-state or in transient with a numerical solver,
or by using a simulator. The second solver is the MC4CSLTA stochastic model checker,
that can evaluate standard performance measures for GSPN and DSPN models [
Figure 8 shows a measure page editor for a GSPN model with one parametric marking parameter hni and with three measures (at the bottom). The GSPN model is evaluated multiple times for different values of n, from 1 to 10 (template parameters section), with increments of 1. The numerical solution is computed by invoking the commandline solvers with the specified solver parameters (solution in steady-state, maximum number of iterations, use the ordinary SWN solution, etc..). The table of measures lists what will be computed. Entry ALL specifies that all basic GSPN measures will be computed, which are the distributions of tokens in each place, and the transition throughputs. RG and TRG specify that the (Tangible) Reachability Graph will be generated by the GreatSPN tools, and a graphical representation will be drawn. Queries in a given language (CTL, CSL, CSLTA, Performance measures) can be specified textually. A PERF query expresses a performance measure on places and transitions, using the syntax of the measure language of GreatSPN.
Close.
Variables binding:
Fork-‐‑ Join
When the user clicks on the “Compute” button, the GUI calls the command-line
numerical solvers, and shows the output to the user. To use the command line tools
directly, the user can export the GSPN/DTA models as separate files. Currently supported
formats are the GreatSPN format and the APNN format [
Computed solutions are shown interactively to the user. Figure 9 shows the interface that is used to show the results of the ALL measure, computed with parameter hni that ranges from 1 to 10. Places and transitions show their expected number of tokens and throughputs, respectively, for the value selected by the user (in this case n = 6). When the user selects a place, its token distribution is shown in the bottom-left corner.
Template parameters can be bound to a single value, a list of values or a range of values. If the performance measures are computed in transient, it is possible to specify that the transient time t is template variable, thus computing a sequence of solutions at different time steps. This allows the user to setup a batch of parametric tests with a certain degree of flexibility. 7
We now present a simple use case to show how the tool functionalities can be used to support model analysis with standard performance measures as well as with CSLTA queries.
StartM1
M1
N Pallets
M2 sw1
M1on ew1
M2bu® sw2
M2on ew2
M3bu® sw3
M3on ew3 hNi hti ¸1 = 1:2 ¸2 = 1:8 ¸3 = 1:9 ½2 = 0:02 ½3 = 0:07 load 0:4 ¸1
Spares repM2
M2ko failM2
½2 SpareBroken repSpares
¼=2 SpareRepairing
M2go goIdle
¸2 goReady2 EndRep
Idle Ready goReady
0:5 repSpareE
repM3E 0:1 0:15 restart 0:2
M3 0:6
Completed
¸3 M3go failM3 ½3 M3ko repM3 ¼=3 M3repairing
Figure 10 shows an instance of a Flexible Manufacturing System (FMS) taken
from [
Figure 11 depicts two DTAs drawn with the GUI that express two path properties on the FMS model. The first accepts the system behaviors where three completion events 0 E-07 5258 9917 3185 0038 5273 5563 8281 4577 7381 7587 8253 1348 6384 2258 3908 5032 2998 5352 7264
0 0685 0368 8322 5596 1036 3105 7591 4371 8061 9543 5a1g3e4* 5408 6844 2146 8224 7213 4701 8408 9713 9824 38% 40%
N=2% N=4% N=6%
N=8% N=10
N=12 ew3 are observed before time α , having not seen any failure of the machines M2 and M3. The second DTA accepts the paths where at least two repairs have been completed in t time units.
To carry on the analysis from the editor, it is sufficient to create a new set of measures for the FMS model, that are parametric in the number N of pallets and on the time t of the DTA. Figure 12 shows the results of the analysis of the FMS model by computing the steady state solution and the model checking of the two DTAs. Datas are computed using the GUI, and then exported from the GUI in Excel Open XML format to plot the diagrams.
! N 2 4 6 8 10 12 14 16 18 *t 1.2% * e *3m 1% e r feo 0.8% sb * ire 0.6% ap *reX 0.4% *f o *ty 0.2% ili b ab 0% o r P
States 259 1460 4858 12225 25861 48594 83780 135303 207575
Visited Transitions Vanishings Iterations 734 324 161 5565 21280 58047 129426 252369 447220 737715 1150982 2414 9246 25420 57168 112354 200474 332656 521660
GMRES 258 325 380 501 634 793 1297 1854
Time 0,01 0,08 0,34 1,04 2,67 6,25 15,02 41,91 122,34 State space of the FMS net and time/iterations required to achieve convergence of the steady-state solution.
Plot*2:*Probability*of*X*repairs*in*total*before* 3me*t=5*
N=2% N=4% N=6% N=8% N=10% N=12% 1% 0.8% *y 0.6% liit ab 0.4% b o r P 0.2% 0% !0.2% *t 1.2% * e *3m 1% e r fo 0.8% eb * irs 0.6% ap *re2 0.4% *f *tyo 0.2% iil abb 0% o r P
Plot*1:*X*comple3ons*without*breakages*
(N=6)* 0% 1% 2% 3% 4% 5% 6% 7% 8% 9% 10% 11% 12% 13% 14% 15% 16% 17% 18% 19% 20%
Time* units.* Plot*3:*Observing*at*least*2*repairs*in*t*3me*
X=1% X=2% X=3% X=4% N=1% N=2% N=3% N=4% N=6% N=8% N=10% 0% 1% 2% 3%
4% Number*of*repairs*(X)* %0 %02 %40 %60 %80 %001 %120 %140 %160 %180 %200 %220 %240 %260 %280 %300 %320 %340 %360 %380 %400
Time*
Fig. 12. Results of the FMS model analysis, visualized in Excel.
The table in the upper-left corner shows the size of the FMS model state space, the number of transitions, the number of vanishing states visited by the numerical solver, and the iterations/time needed to compute the steady state solution on a 2.4Ghz Intel machine with accuracy of 10−7.
Plot 1 represents the result of DTA 1 on the FMS with N=6 pallets for 1,2,3,4 completions (the DTA of Figure 11 represents the case X =3). The plot shows the probability of having enough time to do X completions, and for large values of t converges to the probability of observing a failure. Plot 2 shows the results of DTA 1 by variating the number of circulating pallets N with a fixed time t = 5. The x-axis plots the number of completions, while the y-axis shows the overall probability of completing X tasks before time t. A larger number of pallets increases the throughput of the system, resulting in an increased probability. Finally, Plot 3 shows the results of DTA 2, i.e. the probability of observing two repairs in t time units. Time is plotted on the x-axis and probability on the y-axis, for various numbers of circulating pallets. Since the machine may break when it is under usage, the probability increases for higher values of N. 8
While the GreatSPN framework with the new interface provides a solid base for editing, verifying and computing quantitative/qualitative measures of GSPN/SWN models, there are other tools that provide similar features. Before reimplementing a new GUI, we have explored various alternatives. An (incomplete) list is given.
Möbius : The aims of the Möbius tool [
Snoopy : The tool Snoopy [
Coloane : Coloane [
The specific characteristic of the GreatSPN models, and the vast number of solvers lead to the decision of designing a specific GUI for it. Additionally, some features like the DTA specification and the support to the CSLTA stochastic logic are, to the best of our knowledge, a unique feature of the GreatSPN GUI, and are not found on other tools. The tool is available at http://www.di.unito.it/~greatspn/index.html, in the “New Java GUI” section, either as a part of GreatSPN or as a standalone version. A virtual machine with all the tools installed is also available, at request. 9
This paper presents an in-depth analysis of a new graphical user interface for the GreatSPN framework. The GUI is designed around a complete workflow for the modeling of Petri nets and DTAs, and includes graphical interactive analysis, specification of measures, computation and interactive visualization of the results, and an integration with multiple solvers/simulators/model checkers/optimizer/translators including a CSLTA stochastic model checker and GreatSPN. A small use case has been also presented, to show the effectiveness of the GUI modeling capabilities and analysis with measures from the user point of view.
Since the tool architecture is scalable and customizable, we plan to extend the tool in
various directions. First of all, the Petri net formalism can be augmented to support other
extensions, like compositional formalism. Similarly, DTAs can be extended to cover
more complete statistical control automata, like Linear Hybrid Automata [