Description of the «Peterson» model
This is a model of the Peterson's algorithm for the mutual exclusion problem, in its generalized version for N processes (see reference there) . This algorithm is based on shared memory communication and uses a loop with N-1 iterations, each iteration is in charge of stopping one of the competing processes.
The figure above shows this model and is set up for value N.
Scale factor
The scale factor is the number of processes involved in the system. This has an influence on some color domains definition, some arc valuations and some transition guards. Proposed instances of this models contain the following values: 2, 3, 4, 5, 6.
Model files
PNML files and a set of properties respecting the BNF we propose are available in the submission kit.
