Last modified

June 28, 2016

Displayed

Aug 17, 2018

June 28, 2016

Displayed

Aug 17, 2018

Symmetric Nets with Bags - Some Examples

Navigation

Grammars

Examples

Services

P/T Nets

Symmetric Nets

Stochastic Nets

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

- The "Referendum" example,
- The "Global Resource Allocation Algorithm" 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.

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

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.