CUI LSV LIPN LIP6
MeFoSyLoMa CNRS Iniria
QR Code
Last modified
June 28, 2016

Displayed
Jun 25, 2017
Symmetric Nets with Bags - Some Examples

Introduction

We provide here two simple examples to illustrate modelling concurrent systems with SNB:

The "Referendum" Example

This is the SNB version of the model presented for SN (see there).

It models a referendum where each participant votes either yes or no. The final result is stored in places voted_yes and voted_no. Once again, the expression "<Voters.all>" denotes the constant function that generates one token per value in the Voters colour class.

This system can be modelled by the symmetric net with bags shown in the figure below for a configuration involving 10 voters.

referendum

In this model, transition vote removes all voters from place voting, generates a bag of tokens in place voted_yes and its complementary in place voted_no. The unicity of the tokens is guaranteed by the [unique Y] guard that specifies that each element in Y occurs only once. ~Y corresponds to the complement set function applied to variable Y.

In this model, all possible votes are generated by a single transition firing only. This solution is simpler but also suppresses (in the reachability graph) the useless interleaving generated by firing the no and yes transitions in the SN model, i.e. all intermediate steps representing the individual votes

The "Global Resource Allocation Algorithm" Example

Let us consider the "Global Allocation" algorithm that allows to block resources for an exclusive use by processes before entering a critical section. When process p enters a critical section (transition enter) it locks all the resources required to be used in the critical section. Then, it can release a subset of these resources (and then stay in the critical section) or exit the critical section, thus releasing all the remaining resources it locks.

philsosopher