Petri nets with data – PART 2
If you want to run a workflow net for multiple instances/tokens, you add a start and end
transition to the net. The start-transition is always enabled and can always fire a token.
This results in new methods to check if the net is sound:
K-sound: a net is k-sound if:
• Weak termination: if you have k tokens in the initial marking, then you should
end up with k tokens in the final marking (and: it should always be possible to
reach a marking where only the final place is marked)
• Proper completion: once the final place has k tokens, there are no other tokens
pending in the net
• All transitions are reachable
Up-to-k sound: a net is up-to-k-sound if:
- If a net is sound for every amount of tokens up till k tokens. So: if k = 4, then it
needs to be 1/2/3/4 sound. 1 sound
PS: 1-sound means that the net is sound when having 1 token. The
net below has a livelock (2 tokens are needed in order to fire D) so
it’s not 1-sound. However, the net is 2-sound, which means that in
any situation/marking, the tokens can follow a route to end up in
the final state. PS: the different tokens don’t have to be fired at the same time.
Generalized soundness:
- If a free choice net is 1-sound, then it’s generalized sound
- If a Jackson net is 1-sound, then it’s generalized sound
Colored tokens
In the model on the right, the tokens in p and s are from instance 1 and the tokens
in q and r are from instance 2. However, D doesn’t see the difference and just fires.
What to do about this? → give the tokens a color. A transition is now enabled if the
color of the tokens are the same.
In order to make sure that only one color tokens at a time goes through the split
part of the process, we add a place of some resource. It’s consumed at the
beginning of the split processes and produced back at the end, after which a new
color can go through the split thing in the model. If you need 1+ tokens in the resource
place, for example if you need the resource in another part of the model too, then you
should use (different) colors for the resource-tokens as well.
, Read token as:
agent(a1)
Another way to work with multiple tokens is to use identifiers. A token
often represents multiple real-life entities/elements. They are then
called ‘vectors of identifiers’. The size of the vector is defined by the
amount of elements that the place that the token is in represents. You
can see the place as the relation type. The tokens are the actual relations.
All the different place-identifiers are the entity types . PS: you can give
the arcs the token-names, for example call the arcs going towards
transition A ‘a’ from agent and ‘c’ from case, and call the tokens that A
produces in places p and q ‘c,a’ and ‘c,a’.
Remember: a start event generates a new identifier/case/instance, and
so does an arrow that has a variable which isn’t on one of the ingoing
arcs.
a1,c1 How can you check whether a transition can fire
or not? → you construct a mode by linking the
a1,c3 variables on the arcs with the token identifiers,
and then you check if the transition can fire for
that mode.
A mode is all possible identifiers that the
different variables on the arcs can represent. So,
in this case is this the mode:
a1,b1,c1
a2,b1,c3
Since ‘w’ is not on an ingoing arc, you create a
new identifier for that, in this case ‘d’. So now you just check if there is a possible
combination for which the transition can fire. And there is: x:a1 / y:b1 / z:c1 / w:d1.
So this basically says that if all x’s are a1, all y’s are b1 etc, that the transition can fire
since every input place has at least 1 token that matches this mode. Token a1,c1 in place
1 matches this mode, and token a1,b1,c1 in place 3 matches this mode too. So, yes: this
transition can fire. PS: place 2 has no identifiers and thus doesn’t need to match the
mode or something.
In a model or net, you check per transition what the modes are and which one works.
If you want to run a workflow net for multiple instances/tokens, you add a start and end
transition to the net. The start-transition is always enabled and can always fire a token.
This results in new methods to check if the net is sound:
K-sound: a net is k-sound if:
• Weak termination: if you have k tokens in the initial marking, then you should
end up with k tokens in the final marking (and: it should always be possible to
reach a marking where only the final place is marked)
• Proper completion: once the final place has k tokens, there are no other tokens
pending in the net
• All transitions are reachable
Up-to-k sound: a net is up-to-k-sound if:
- If a net is sound for every amount of tokens up till k tokens. So: if k = 4, then it
needs to be 1/2/3/4 sound. 1 sound
PS: 1-sound means that the net is sound when having 1 token. The
net below has a livelock (2 tokens are needed in order to fire D) so
it’s not 1-sound. However, the net is 2-sound, which means that in
any situation/marking, the tokens can follow a route to end up in
the final state. PS: the different tokens don’t have to be fired at the same time.
Generalized soundness:
- If a free choice net is 1-sound, then it’s generalized sound
- If a Jackson net is 1-sound, then it’s generalized sound
Colored tokens
In the model on the right, the tokens in p and s are from instance 1 and the tokens
in q and r are from instance 2. However, D doesn’t see the difference and just fires.
What to do about this? → give the tokens a color. A transition is now enabled if the
color of the tokens are the same.
In order to make sure that only one color tokens at a time goes through the split
part of the process, we add a place of some resource. It’s consumed at the
beginning of the split processes and produced back at the end, after which a new
color can go through the split thing in the model. If you need 1+ tokens in the resource
place, for example if you need the resource in another part of the model too, then you
should use (different) colors for the resource-tokens as well.
, Read token as:
agent(a1)
Another way to work with multiple tokens is to use identifiers. A token
often represents multiple real-life entities/elements. They are then
called ‘vectors of identifiers’. The size of the vector is defined by the
amount of elements that the place that the token is in represents. You
can see the place as the relation type. The tokens are the actual relations.
All the different place-identifiers are the entity types . PS: you can give
the arcs the token-names, for example call the arcs going towards
transition A ‘a’ from agent and ‘c’ from case, and call the tokens that A
produces in places p and q ‘c,a’ and ‘c,a’.
Remember: a start event generates a new identifier/case/instance, and
so does an arrow that has a variable which isn’t on one of the ingoing
arcs.
a1,c1 How can you check whether a transition can fire
or not? → you construct a mode by linking the
a1,c3 variables on the arcs with the token identifiers,
and then you check if the transition can fire for
that mode.
A mode is all possible identifiers that the
different variables on the arcs can represent. So,
in this case is this the mode:
a1,b1,c1
a2,b1,c3
Since ‘w’ is not on an ingoing arc, you create a
new identifier for that, in this case ‘d’. So now you just check if there is a possible
combination for which the transition can fire. And there is: x:a1 / y:b1 / z:c1 / w:d1.
So this basically says that if all x’s are a1, all y’s are b1 etc, that the transition can fire
since every input place has at least 1 token that matches this mode. Token a1,c1 in place
1 matches this mode, and token a1,b1,c1 in place 3 matches this mode too. So, yes: this
transition can fire. PS: place 2 has no identifiers and thus doesn’t need to match the
mode or something.
In a model or net, you check per transition what the modes are and which one works.
