in cooperation with|
Dipartimento di Informatica - Università del Piemonte Orientale, Alessandria
GRaphical Editor and
for Timed and Stochastic Petri Nets
to download the book
Ansaldo Segnalamento Ferroviario, Napoli,
Telecom Italia Lab, Torino, Italy
Centro Elettrotecnico Sperimentale Italiano, Milano, Italy
- What is GreatSPN
GreatSPN2.0 is a software package for the modeling, validation, and performance
evaluation of distributed systems using Generalized Stochastic Petri Nets
and their colored extension: Stochastic Well-formed Nets. The tool provides
a friendly framework to experiment with timed Petri net based modeling
techniques. It implements efficient analysis algorithms to allow its use
on rather complex applications, not only toy examples.
GreatSPN2.0 is composed of many separate programs that cooperate in
the construction and analysis of PN models by sharing files. Using network
file system capabilities, different analysis modules can be run on different
machines in a distributed computing environment. The modular structure
of GreatSPN2.0 makes it open to the addition of new analysis modules
as new reserch results become available. All modules are written in
the C programming language to guarantee portability and efficiency on
different Unix machines. All solution modules use special storage techniques
to save memory both for intermediate result files and for program data
Several state-of-the-art analysis prototypes have been recently added
in the package: an algorithm for the fast computation of performance
bounds based on linear programming techniques, working at a purely structural
level (the computed bounds depend only on the average firing delay of
the transitions while they do not depend on the p.d.f. of such delays);
algorithms for the analysis of Stochastic Well-formed Nets providing
the user with the possibility of designing models of complex systems
in a more compact way, and allowing a more efficient state space analysis
that automatically exploits the model symmetries (through the Symbolic
Furthermore, the graphical interface has been recently ported under
OSF Motif achieving high portability under different hardware platforms.
Hardware and software required to run GreatSPN 2.0
This package has been compiled at our site using :
- Linux Fedora, Ubuntu (INTEL)
- Mac OS X 10.4 (PPC)
- Follows a (non exhaustive) list of people that contriuted to the
development and maintenance of GreatSPN and related tools:
- G. Chiola, R. Gaeta, A. Horvath, M. De Pierro, M. Beccuti, S. Baarir, D. Cerotti, Elvio Amparore.
- Collaborations with other Universities:
- New interesting developments on the solvers for the SWN formalism, based on some core functions of GreatSPN for the handling of SWN models, are in progress within a collaboration with the group MoVe (resp. Prof. F. Kordon) of the LIP6, Universite' Marie Curie, Paris and within a collaboration with the CReSTIC laboratory (resp. Prof. P. Moreaux) of the Universite' de Reims Champagne-Ardenne (URCA), Reims.
Back to the index
GreatSPN main features
The main functions of the tool can be outlined as follows:
- graphical interface running under OSF Motif 1.2 (or later) allows:
- graphical model editing including layering, cut and paste, selection,
rotation, rescaling, spline, zooming, improved printing in PostScript,
- graphical representation of structural properties
- interactive token game for PNs with priorities and inhibitor arcs
(not for colored nets for the moment)
- access to the model data base, with cut and paste options for submodels
- definition of timing and stochastic specifications, parameters,
and performance measures
- menu-driven interaction with analysis modules
- graphical representation of performance results
- graphical interactive simulation of timed and stochastic models
(not for colored nets for the moment)
- structural properties for nets with priorities and inhibitor
arcs (not for colored nets for the moment)
- Place- and Transition- invariants
- deadlocks and traps
- implicit places
- causal connection and structural conflict
- mutual exclusion
- Extended Conflict Set (ECS) and structural confusion
- structural boundedness and unbounded transition sequences
- linear programming performance bounds for timed P/T nets (not
for colored nets for the moment): upper and lower bounds for transition
throughputs and average place markings
- reachability graph generation and analysis programs
- home space, deadlocks, and livelocks
- transition liveness degree
- Markovian solvers for steady-state as well as transient performance
evaluation exploiting efficient, sparse matrix numerical techniques.
- simulation modules for interactive event-driven simulation (not
for colored nets for the moment). In cooperation with the graphical interface,
The simulation state is periodically saved on a file, so that previous
simulation runs can be resumed at any time. Several probability distributions
are allowed for transition timings (including uniform, discrete, Cox,
- interactive simulation, with graphical animation of the model and
movement of tokens, with step-by-step, and automatic run, forward
and backward time progression, real time update of performance figures,
arbitrary rescheduling of events.
- batch simulation, with periodic sampling and real time update of
performance figures on the graphical interface and computation of
- well-formed colored nets analysis prototypes
- construction of colored and symbolic reachability graph, conversion
into lumped Markov chain, steady state and transient Markovian analysis
- colored and symbolic simulation
- Nets composition through algebra
- Multiple experiments management through multisolve
The following items are Now Available!!
- unfolding an SWN model into a GSPN one
- graphical representation of the (S)RG in ps/eps format
- a VMware virtual machine running GreatSPN on top of Linux
- Extended SRG solver for SWN models (beta version)
- Dynamic SRG solver for SWN models (beta version)
- MDWN and MDPN formalism to model optimization problems (beta version)
- CTL Model checking with tree-like counterexamples exploiting decision diagram (beta version)
- CSLTA model checker exploiting recently solution methods for Markov Renewal Processes (beta version)
- New (Java-based) GUI for GSPN model (beta version)
Back to the index
How to obtain the package
The package is available for free for universities and non-profit organizations,
while it can be purchased from the Dipartimento di Informatica, Università
di Torino (Italy) by other organizations/companies. The procedure to obtain
it is the the following.
- Extract the licence agreement ( latex
file or postscript file ,
PDF file ), print it, and return
it signed by the responsible of your institution to
the greatSPN staff
Dipartimento di Informatica
Università di Torino
Fax Number: (+39)(011)(751603)
- Send either by electronic mail (firstname.lastname@example.org)
or by fax the name and the Internet address of the machine you will use
to connect to our server.
- Upon their receipt we will send you an e-mail message containing all
the necessary information to retrieve the source code of the package and
Back to the index
GreatSPN User Manual
Click here to get the NEW Getting Started manual of GreatSPN2.0
(either as PDF or PostScript).
The (almost) complete manual is HERE
Back to the index
Some examples of GSPN and
- Follows a list of GSPN and SWN model examples: for each example it is possible
to download a zip file containing a description of the modeled system (.pdf),
the model files in GreatSPN format (.net and .def),
some result files produced by GreatSPN (e.g. symbolic reachability
graph of SWN models - .srg* files - performance indices computed
by GreatSPN - .sta files -, etc.). A README file is included
to explain the content of each file in the package.
- Examples of GSPN nets:
- Readers-Writers Model
- Kanban System
- Randon Polling System
- Spooler System
- Mesh model with multitasking
- Examples of SWN nets:
Back to the index
- Papers on the Package
- G. Chiola, G. Franceschinis, R. Gaeta, and M. Ribaudo.
GreatSPN 1.7: Graphical Editor and Analyzer for Timed and Stochastic
Performance Evaluation, special issue on Performance Modeling
Tools, 24(1&2):47--68, November 1995.
- S.Bernardi, S.Donatelli, and A.Horvàth.
Compositionality in the GreatSPN tool and its use to the modelling
of industrial applications.
Software Tools for Technology Transfer
- S. Bernardi, C. Bertoncello, S. Donatelli, G. Franceschinis, G. Gaeta, M. Gribaudo and Horvàth.
GreatSPN in the new Millenium.
In Tools of Aachen 2001, International Multiconference on Measurement, Modelling and Evaluation
of Computer-Communication Systems, Research Report no.760/2001, Universitat Dortmund (Germany), September 2001, pages 17--23.
- J.M. Ilie, S. Baarir, M. Beccuti, C. Delamare, S.
Donatelli, C. Dutheillet, G. Franceschinis, R. Gaeta, P. Moreaux.
Extended SWN Solvers in GreatSPN.
1st International Conference on Quantitative Evaluation of Systems (QEST04), Enschede, Netherlands September 2004. IEEE Soc. Press: 324-325
- M. Beccuti, D. Codetta-Raiter, G. Franceschinis, and S. Haddad.
A framework to design and solve Markov Decision Well-formed Net models.
Proceeding of 4th International Conference on Quantitative Evaluation of SysTems (QEST07), Edinburgh, Scotland, 16-19 September 2007.IEEE Computer
- S. Baarir, M. Beccuti, G. Franceschinis.
New solvers for asymmetric systems in GreatSPN.
In 5th International Conference on the Quantitative Evaluation of SysTems (QEST) 2008 pages 235-236, St.
Malo, France, 14-17 September 2008. IEEE Computer Society Press
- S. Baarir, M. Beccuti, D. Cerotti, M. De Pierro, S. Donatelli and G. Franceschinis.
The GreatSPN Tool: Recent Enhancements.
ACM Performance Evaluation Review Special Issue on Tools for Performance Evalaluation, Volume 36, Issue 4, September 2009, Pages 4--9.
- J. Babar, M. Beccuti, S. Donatelli, and A. Miner.
GreatSPN Enhanced with Decision Diagram Data Structures.
In 31st International Conference on application and theory of Petri nets and other models of concurrency (ICATPN'10), volume 6128 of Springer LNCS, pages 308-317. June
21-25, 2010, Braga, Portugal
- M. Beccuti, S. Haddad, G. Franceschinis.
MDWNsolver: a framework to design and solve Markov Decision Petri Nets.
International Journal of Performability Engineering, Volume 7, Issue 5, September 2011, Pages 417-428. Ed. RAMS Consultants.
- Papers on the GSPN and SWN formalisms
- M. Ajmone Marsan, G. Balbo, and G. Conte.
A class of generalized stochastic Petri nets for the performance analysis
of multiprocessor systems.
ACM Transactions on Computer Systems, 2(1), May 1984.
- M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis.
Modelling with Generalized Stochastic Petri
Nets. J. Wiley, 1995.
- G. Chiola, J. Campos, J.M. Colom, M. Silva, and C. Anglano.
Operational analysis of timed Petri nets and applications to the computation
of performance bounds.
In Proc. 5th Intern. Workshop on Petri Nets and Performance Models,
Toulouse, France, October 1993. IEEE-CS Press.
- G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad.
Stochastic well-formed coloured nets for symmetric modelling applications.
IEEE Transactions on Computers, 42(11):1343--1360, November 1993.
- G. Chiola, M. Ajmone Marsan, G. Balbo, and G. Conte.
Generalized stochastic Petri nets: A definition at the net level and
IEEE Transactions on Software Engineering, 19(2):89--107, February
- R. Gaeta, and G. Chiola.
Efficient simulation of SWN models.
In Proc. 6th Intern. Workshop on Petri Nets and Performance Models,
Durham, U.S.A., October 1995. IEEE-CS Press.
- R. Gaeta, Efficient discrete-event simulation of colored Petri
IEEE Transactions on Software Engineering, 22(9), September
- ! [R9]> G.Chiola, C.Dutheillet, G.Franceschinis, and S.Haddad.
A Symbolic Reachability Graph for Coloured Petri Nets.
Theoretical Computer Science B (Logic, semantics and theory of
programming), 176 (1&2):39-65, April 1997, Elsevier.
- ![M3]> M.Ajmone Marsan, S.Donatelli, G.Franceschinis, and F.Neri.
Reductions in Generalized Stochastic Petri Nets and Stochastic Well-formed
Nets: An Overview and an Example of Application.
In The State-of-the-art in Performance Modeling and Simulation:
Network Theory, Tools and Tutorials, J. Walrand, K. Bagchi and G.
Zobrist (editors). Gordon and Breach Publishers INC., 1997
- L. Capra, C. Dutheillet, G. Franceschinis, J. M. Ilie.
Towards Performance Analysis with Partially Symmetrical SWN.
In Proc. 7th International Symposium on Modeling, Analysis and Simulation (MASCOTS 99), College Park, MD, USA. (1999)
- S. Baarir, C. Dutheillet, S. Haddad, and J-M. Ilie.
On the use of exact lumpability in partially symmetrical Well-formed Nets.
In Proc. of QEST, pages 23-32,Torino - Italy, September 2005.
- M. Beccuti, S. Baarir, G. Franceschinis, J-M. Ilie.
Efficient lumpability check in partially symmetric systems.
3rd International Conference on Quantitative Evaluation of Systems (QEST06), Riverside, CA, USA, September 2006. IEEE Soc. Press
- G. Balbo, M. Beccuti, M. De Pierro and G. Franceschinis.
First Passage Time Computation in Tagged GSPNs with Queue Places.
The Computer Journal, Oxford University Press., Volume 54, Issue 5, May 2010, Pages 653-673.
G. Balbo, M. Beccuti, M. De Pierro and G. Franceschinis.
importance of token scheduling policies in Stochastic Petri nets.
Proceedings of the International Conference on Operations research (OR2010), Springer LNCS, pages 181-187 September 1-3, 2010, Munich, Germany/EM>
- S. Baarir, M. Beccuti, C. Dutheillet, G. Franceschinis, S. Haddad.
Lumping partially symmetrical stochastic models.
International Journal of Performance Evaluation, Volume 68, Issue 1, January 2011, Pages 21-44.
- M. Beccuti and G. Franceschinis
Efficient simulation of Stochastic Well-Formed Nets through symmetry exploitation
Proceedings of Winter Simulation Conference (WSC12), pages 296-296, Berlin, Germany, 9-12 December, 2012.
- Case Studies with GSPN and SWNs
- C.Anglano, S. Donatelli, G.Franceschinis and O.Botti
Performance prediction of a reconfigurable high voltage substation
simulator: a case study using SWN
In Proc. 7th International Workshop on Petri Nets and Performance
M odels, St. Malo, France , june 1997.
- R.Gaeta and M.Ajmone Marsan,
SWN Analysis and Simulation of Large Knockout ATM Switches,
Volume 1420 of LNCS, Proc. of 19th International Conference on
Application and Theory of Petri Nets. Springer-Verlag, June 1998.
- G. Franceschinis, C. Bertoncello, G. Bruno, G. Lungo Vaschetti
and A. Pigozzi
SWN models of a contact center: a case study. In Proc. 9th International
Workshop on Petri Nets and Performance Mo dels, Aachen, Germany,
- A. Bobbio, G. Franceschinis, R. Gaeta and G. Portinale
Dependability Assessment of an Industrial Programmable Logic Controller
via Parametric Fault-Tree and High Level Petri Net In Proc. 9th
International Workshop on Petri Nets and Performance Mo dels,
Aachen, Germany, September 2001
- M. Beccuti, A. Bottrighi, G. Franceschinis, S. Montani and P. Terenziani.
Modeling clinical guidelines through Petri Nets.
In 12th International Conference on Artificial Intelligence in Medicine
(AIME'09), volume 5651 of Springer LNCS, pages 61-70. July 18-22, 2009,
Back to the index
[Group home page]