GreatSPN 3 is now open source! You can find the source code
and the documentation on https://github.com/greatspn/SOURCES.

GRaphical Editor and Analyzer for Timed and Stochastic Petri Nets

      
Telecom Italia Lab, Torino, Italy

    
Centro Elettrotecnico Sperimentale Italiano, Milano, Italy

Introducing GreatSPN

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 structures.

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 RG concept).

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)
  gcc
  Motif 2.0
  X11R6
  
• Mac OS X 10.4 (PPC)
  gcc
  Motif 2.0
  X11
  
  

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, etc.
  • 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, they provide
  • 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 confidence intervals
  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, Erlang, etc.).
• 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)
• CSL^TA 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.

1. 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)
2. Send either by electronic mail (greatspn@di.unito.it) or by fax the name and the Internet address of the machine you will use to connect to our server.
3. 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 its documentation.

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 SWN nets

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:

• Multiprocessor Architetture
• Polling System
• Multilevel Fat Tree

Back to the index

Bibliography

Papers on the Package

• G. Chiola, G. Franceschinis, R. Gaeta, and M. Ribaudo.
  GreatSPN 1.7: Graphical Editor and Analyzer for Timed and Stochastic Petri Nets.
  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 Society Press.
• 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 its implications.
  IEEE Transactions on Software Engineering, 19(2):89--107, February 1993.
• 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 nets,
  IEEE Transactions on Software Engineering, 22(9), September 1996
• 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.
• 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.
  On the 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, September 2001
• 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, Verona, Italy.