We provide here two simple examples to illustrate modelling concurrent systems with Symmetric Nets with Bags:
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.
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 into 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.