Case Studies and Example Models for the APNN-Toolbox
Examples of Mutual Exclusion Algorithms modeled with ordinary and untimed Petri Nets
The following set of examples are taken from W. Reisig, "Elements of Distributed Algorithms Modeling and Analysis with Petri Nets", Chapter 13, Springer Verlag,
for educational and illustrative purposes. For each model, we provide a brief description, a screen shot and the APNN net description which can be loaded and worked with in the APNN Toolbox.
Since those Petri nets are purely functional models, they
may be analyzed by help of the token game, invariant analysis,
lifeness checks and model checking.
All models do NOT use the notion of color as supported by the APNN Toolbox.
All models do NOT use the stochastic notion of time for their semantics, however within the APNN Toolbox, this results in transitions of priority 0, i.e., timed transitions, in order to make state based analysis algorithms work properly.
The Token-Passing mutex Algorithm
The Round-Based mutex Algorithm
Peterson's mutex Algorithm
Dekker's mutex Algorithm
Owicki/Lamport's mutex Algorithm
The Asymmetrical mutex Algorithm
Case Studies
The following Petri net models are mainly taken from literature and have been served
as benchmark examples several times in our own and in external papers.
Each example has its own Web-page including a short description and a
reference where it appeared first, if the example has been taken from literature.
Observe that most of the following examples are part of the APNN-toolbox
distribution and need not downloaded separately.
For each example we have an APNN-specification and one or several representations
as hierarchical stochastic automata networks.
The APNN-specification can be read and modified by the editor APNNed
and can used as input for the simulator APNNsim.
The file format for hierarchical automata networks can be found in the
Nsolve documentation . State spaces and matrices
can be stored as flat stochastic automata networks (SANs) which are hierarchical
networks with one state for the high level model or as true hierarchical models
with several states in the high level model. Flat automata networks are the
input format for the tools SupGSPN and CSLModelChecking. The
hierarchical description is used in the tools Nsolve and Parallel.
Case studies of Communication Systems
Case studies of Computer Systems
Case studies of Manufacturing and Logistic Systems
Miscellaneous other topics