Modelling Based on Petri Nets
Petri nets are often used for distributed systems and for systems with resource sharing.
Since there may be more than one transition in the Petri net active at a time and we don’t know which will fire first, they are non-deterministic.
There are certain additions to Petri nets which make them High-Level:
- Colour - For modelling attributes.
- Time - For performance analysis.
- Hierarchy - For the structuring of models, DFD’s.
Conditions
- A transition is only enabled if each of the input places contains tokens.
- Enabled transitions can fire.
- Firing consumes tokens from the inputs and produces tokens for the outputs according to the arcs.
Example Firing
This is a sequence of firings:
-
stateDiagram-v2 direction LR state T1 <<fork>> P1(•••) --> T1 T1 --> P2(•) T1 --> P3(•) P3(•) --> T1
-
stateDiagram-v2 direction LR state T1 <<fork>> P1(••) --> T1 T1 --> P2(••) T1 --> P3(•) P3(•) --> T1
-
stateDiagram-v2 direction LR state T1 <<fork>> P1(•) --> T1 T1 --> P2(•••) T1 --> P3(•) P3(•) --> T1
Creating & Consuming Tokens
A transitions without any input can fire at any time and produces tokens in all connected places:
-
stateDiagram-v2 direction LR state T1 <<fork>> T1 --> P1()
-
stateDiagram-v2 direction LR state T1 <<fork>> T1 --> P1(•)
-
stateDiagram-v2 direction LR state T1 <<fork>> T1 --> P1(••)
A transition without any output must be enabled to fire and deletes the incoming tokens:
-
stateDiagram-v2 direction LR state T1 <<fork>> P1(•••) --> T1
-
stateDiagram-v2 direction LR state T1 <<fork>> P1(••) --> T1
-
stateDiagram-v2 direction LR state T1 <<fork>> P1(•) --> T1
Non-Determinism
If two transitions fight for the same token there is a conflict. The next transition to fire $T1$ or $T2$ is non-deterministic:
stateDiagram-v2
direction LR
state T1 <<fork>>
state T2 <<fork>>
P1(•) --> T1
P1(•) --> T2
T1 --> P2
T2 --> P3
Even if there are two tokens, there is still conflict.
Modelling
- Tokens - Can represent resources, information, conditions, or states of objects.
- Places - Can represent buffers, channels, locations, conditions, or states.
- Transitions - Represent events, transformations or transportations.
Traffic Light Example
To begin we will model only one traffic light:
stateDiagram-v2
direction LR
state gy <<fork>>
state yr <<fork>>
state rg <<fork>>
Green --> gy
gy --> Amber
Amber --> yr
yr --> Red(•)
Red(•) --> rg
rg --> Green
Having two of this model would enable both sets of traffic lights to be green at the same time. To stop this we can make the following modification:
stateDiagram-v2
direction LR
state gy1 <<fork>>
state yr1 <<fork>>
state rg1 <<fork>>
Green1 --> gy1
gy1 --> Amber1
Amber1 --> yr1
yr1 --> Red1(•)
Red1(•) --> rg1
rg1 --> Green1
state gy2 <<fork>>
state yr2 <<fork>>
state rg2 <<fork>>
Green2 --> gy2
gy2 --> Amber2
Amber2 --> yr2
yr2 --> Red2(•)
Red2(•) --> rg2
rg2 --> Green2
yr1 --> Safe(•)
yr2 --> Safe(•)
Safe(•) --> rg2
Safe(•) --> rg1
This fires the two traffic lights in random order due to the conflict with Safe
. To make them change alternately we can use the following model:
stateDiagram-v2
direction LR
state gy1 <<fork>>
state yr1 <<fork>>
state rg1 <<fork>>
Green1 --> gy1
gy1 --> Amber1
Amber1 --> yr1
yr1 --> Red1(•)
Red1(•) --> rg1
rg1 --> Green1
state gy2 <<fork>>
state yr2 <<fork>>
state rg2 <<fork>>
Green2 --> gy2
gy2 --> Amber2
Amber2 --> yr2
yr2 --> Red2(•)
Red2(•) --> rg2
rg2 --> Green2
yr1 --> Safe1(•)
yr2 --> Safe2()
Safe1(•) --> rg2
Safe2() --> rg1
Definitions
- Current State (Marking) - The configuration of the tokens over the places.
- This is described by a tuple.
- Reachable State - A state reachable from the current state by firing a sequence of enabled transitions.
- Deadlock State - A state where no transition is enabled.
Examples
For the following graph:
stateDiagram-v2
direction LR
state br <<fork>>
state rr <<fork>>
state bb <<fork>>
Red(•••) --> rr:2
rr --> Black(••)
Black(••) --> bb:2
bb --> Black(••)
Black(••) --> br
br --> Red(•••)
Red(•••) --> br
State: (3,2)
This is because we are ordering the tuple (Red,Black)
and there are three tokens in Red
and two tokens in Black
.
We can also graph the reachable states and deadlock states in a tree:
flowchart LR
32["(3,2)"] -->|rr| 13
13["(1,3)"] -->|bb, br| 12["(1,2)"]
12 -->|bb, br| 11["(1,1)"]
11 -->|br| 10["(1,0)"]
32 -->|bb,br| 31["(3,1)"]
31 -->|rr| 12
31 -->|br| 30["(3,0)"]
30 -->|rr| 11
There are 7 reachable states and one deadlock state.
Reachable are those down stream from your current place and deadlock states are those with no transitions out.