A little puzzle is presented, together with a corresponding Petri net model. Conditions for deadlockfreedom and for the termination property are proven necessary and suficient. This example might be helpful for education issues w.r.t. modeling of systems, modeling of properties, techniques for deciding deadlock-freedom and for termination such as siphons and invariants and, more generally, proof techniques.
A usual way to teach programming is to explain the programming language syntax, a number of example programs, and its runs, and then expect that students can construct their own programs independently for a given requirement. The same holds respectively for teaching modeling and for teaching model analysis. In fact, good students survive this impertinence, but many other students do not get the feeling of how to model, analyze, or prove properly. In particular, they might be able to reproduce very small and trivial examples but fail to make the transfer to application. This is not surprising: Imagine that in music classes students would first learn the syntax for the language of music, i.e., the interpretation of notes, clefs, keys etc. Later they hear concerts from Mozart and Beethoven and then are expected to be able to compose their own music. Instead, what is absolutely necessary for learning music, programming, or modeling is training by examples of diferent, increasing complexity and size, where training means independent work on related tasks.
This article presents an example that is claimed to be useful for learning modeling with Petri nets, model analysis, and proofs based on models. In fact, existing textbook literature on modeling intentionally starts with very simple examples, because students are not supposed to spend time on understanding the example, but on the concepts being taught. More application oriented literature uses more complex models, but often the emphasis or the learning goal is within the application domain and not on modeling. However, some good examples of medium sized modeling tasks and sample solutions can be found. Yet, to the best of my knowledge, there is no systematic collection of them. One exception is the collection of example in Wolfgang Reisig’s book on distributed algorithms [1], which provides lots of modeling and model analysis examples for high-level Petri nets, but I doubt that many students would be ready to independently create models on that level.
This short paper just provides a modeling example on a much lower level, suitable for beginners like graduates of the Petri Net Course of the annual Petri Net Conference or of the Petri Net Advanced Course series. It only applies elementary concepts of low-level Petri nets, but also typical proof techniques, recognizing that simple application of invariants, siphons, and such things are not suficient in most application examples.
My personal motivation for this work is that I found the task statement completely independent from the typical Petri net modeling world, that the problems mentioned are neither completely trivial nor unsolvable, and that this example is beautiful in two ways: it is a beautiful problem, and Petri nets can provide a beautiful solution.
I recently found the following puzzle in the German online magazin SPIEGEL online [2], based on [3]:
Some chameleons live quite happily in a large terrarium. There are six in all: four red, two blue, and a green one. These chameleons have a strange property: whenever two chameleons of diferent colors meet, both take on the third color. For example, when a blue and a green chameleon meet, they both turn red. And when a red and a green chameleon meet, they both turn blue.
Question: Can it happen that at some point in time all the chameleons have the same color? Additional questions: What is the answer if at the beginning five chameleons are red, two are blue and one is green? What if six chameleons are red, two are blue and one is green?
The solutions to two of the questions are given and proven without any formal model in [2]. In this contribution, we aim to show that the puzzle is very well suited to train Petri net modeling, and that the above questions, as well as related questions, can be solved using Petri net methods.
It is easily seen that the property “all chameleons have the same color" of this example coincides with the deadlock property of a Petri net model, as long as only the behavior mentioned above is modeled. Generally, a deadlock is a state in which no (further) action is possible – in Petri net models it is a marking which enables no transition. A system or an initially marked Petri net is said to be deadlock-free, if no reachable state or marking is a deadlock.
So, for a Petri net model of the Chameleon game, the above questions translate to the questions whether the net with respective initial markings is deadlock-free or not.
Figure 1 shows a Petri net model of the chameleon game, which we shall call chameleon net in this paper (for educational issues, students should be asked to provide the model!).
The initial marking of the chameleon net depends on the initial numbers of chameleons and their colors. The figure shows the initial situation with four red chameleons, two blue ones, and one green one, as in the first question above. bgr 2 red 2 2
In this contribution, we will only consider this chameleon Petri net and will use the following notations: The initial marking 0 of the net will be denoted by (0, 0, 0) where 0 = 0(), 0 = 0(), and 0 = 0(). Similarly, we describe general markings by (, , ).
We assume that the readers know the concepts of occurrence rule for Petri nets (with arc weights) and occurrence sequences (finite and infinite ones). Moreover, we assume the incidence matrix of a net to be known. We will also mention marking graphs, place invariants and siphons. For definitions, see any textbook on Petri nets like [4] or see [5].
The following section presents a deadlock-freedom analysis of the chameleon net, providing answers to the above questions. We will characterize deadlock-free initial markings, i.e., initial markings that make the marked chameleon net deadlock-free. For initial markings which are not deadlock-free we will provide a strategy how to fire transitions in such a way that a deadlock will be reached eventually.
Section four considers a similar, but diferent question: Will the chameleon net inevitably reach a deadlock, provided that in each non-deadlocked marking a transition occurs? We call this property termination property and say that the net with a given initial marking satisfying the termination property terminates. If a net does not terminate, then it is possible to keep on ifring transitions forever, which means that infinite occurrence sequences exist. Note that a non-terminating net may run into a deadlock, but does not necessarily do so. We will analyze the chameleon net w.r.t. termination and provide a suficient and necessary condition for this property in terms of the initial marking. We will provide a strategy how to avoid deadlocks for non-terminating initial markings of the chameleon net.
As long as there are chameleons with diferent colors, they might meet and change colors. That
is, a transition can occur in the chameleon net. When, conversely, all chameleons are of the
same color, nothing can happen anymore and the corresponding marking of the Petri net does
not enable any transition and therefore is a deadlock. We consider the following three questions:
1. Is there a finite occurrence sequence from marking (
Question 1 is easily answered by
(4, 2, 1→)−− (3, 1, 3→)−− (2, 3, 2→)−− (1, 5, 1→)−− (0, 7, 0) and Question 2 by
(5, 2, 1→)−− (4, 4, 0→)−− (3, 3, 2→)−− (2, 2, 4→)−− (1, 1, 6→)−− (0, 0, 8).
The reader is invited to find a respective occurrence sequence that leads to a deadlock for Question 3 ... but will inevitably fail because no such sequence exists. To prove this fact, the simplest way is to construct the marking graph of the net and verify that each of its nodes has at least one successor and therefore does not represent a deadlock. But imagine that the initial marking was (1006, 1002, 1001) – then this procedure was no longer feasible. Instead, both [2] and [3] present a proof that, for this particular initial marking, no reachable deadlock exists. In the sequel, we will translate this proof into Petri net jargon.
For analysis of the chameleon net we consider its incidence matrix ⎛
2 A = ⎝ − 1 − 1 − 1
2
− 1
− 1 ⎞
− 1 ⎠
2
where the rows corresponds to the places , and and the columns to the transitions
, and . It is well known that, if a transition occurs at marking and leads to marking
′, then ′ is obtained by adding the corresponding column of the incidence matrix to . A
place invariant is a vector satisfying · A = (0, 0, 0). The most important property of a place
invariant is that each reachable marking satisfies · = · 0. In the chameleon example,
there is only one relevant place invariant, namely (
The concept of place invariants was generalized in [6] to modulo-invariants. A vector is a modulo--invariant, if · A ≡ 0 (mod ), i.e., if all entries of · A are multiples of . Similar to place invariants, we have for a modulo--invariant that · ≡ · 0 (mod ) for each marking reachable from 0, i.e., · − · 0 is a multiple of .
Modulo-3-invariants of the chameleon net will be used in the proof of the following lemma.
The net has the modulo-3-invariants (
The following lemma considers the case that a deadlock is reachable where all chameleons are red. The other two options of deadlocks (all chameleons blue or all chameleons green) are similar. For technical reasons, the case that there are no chameleons at all is excluded. Lemma 1. Assume 0 + 0 + 0 > 0.
The marking (0 + 0 + 0, 0, 0) is reachable from 0 if and only if
0 ≡ 0 (mod 3) and 0 + 0 > 0 and 0 + 0 > 0.
=⇒
Assume that (0 + 0 + 0, 0, 0) is reachable from (0, 0, 0).
0 ≡ 0 (mod 3) follows by the mod-3 invariant (
Similarly, 0 + 0 > 0 since otherwise the initial marking is a deadlock (0, 0, 0) with 0 > 0. ⇐= Assume 0 ≡ 0 (mod 3), 0 + 0 > 0, 0 + 0 > 0. We proceed by induction on max(0, 0). Base. If max(0, 0) = 0 then 0 = (0, 0, 0) and we are finished.
Step. Assume that max(0, 0) > 0. We show that we can reach a marking (, , ) from (0, 0, 0) such that
≡ (mod 3), + > 0, + > 0, max(, ) < max(0, 0).
Then, by the induction hypothesis, (0 + 0 + 0, 0, 0) can be reached from (, , ) and thus from (0, 0, 0), too.
In the cases considered below we use (− ) ≡ (0 − 0) ≡ 0 (mod 3). This is because (
If 0 > 0 and 0 > 0, then we fire , yielding the marking ( = 0 + 2, = 0 − 1, = 0 − 1). Then + = 0 + 0 + 1 > 1, + = 0 + 0 + 1 > 1 and max(, ) = max(0, 0) − 1. If 0 = 0 then, by assumptions, 0 > 0 and 0 > 0. Since 0 ≡ 0 (mod 3) we obtain 0 ≥ 3. We ifre . Then = 0 − 1, = 2, = 0 − 1 ≥ 2. So max(, ) = = 0 − 1 = max(0, 0) − 1. Since = 2 and ≥ 2 we have + > 0 and + > 0.
The case 0 = 0 is similar by symmetry; we fire .
0 ≡ 0 (mod 3) or 0 ≡ 0 (mod 3) or 0 ≡ 0 (mod 3).
{(0 − 0), (0 − 0), (0 − 0)} ≡ { 0, 1, 2} (mod 3) where equivalence modulo is defined on sets elementwise.
Proof. The only possible reachable deadlocks are (0 + 0 + 0, 0, 0), (0, 0 + 0 + 0, 0) and
(0, 0, 0 + 0 + 0). In the first case, = and therefore, by the modulo-3-invariant (
Conversely, assume that one of the conditions, say 0 ≡ 0 (mod 3) holds true. If 0 + 0 > 0 and 0 + 0 > 0, then the result follows from Lemma 1. Otherwise, either 0 = 0 = 0 or 0 = 0 = 0 and thus the initial marking is already a deadlock. This is in particular the case if all places are initially unmarked.
By symmetry, Lemma 1 can be applied for the other conditions in the same way.
The proof of Lemma 1 also shows a strategy to reach a deadlock, if possible. When we assume that 0 ≡ 0 ≡ 0 (mod 3) ( ̸= ), which has to be the case for some places and by the lemma, then we give priority to the transition which has both and in its pre-set, until one (or both) of these places are unmarked. In case both are unmarked, a deadlock is reached. In case only one of these places is unmarked, we fire the transition that adds two tokens to this place (and takes away a token from the other place) and then continue with the prioritized transition.
Now let‘s come back to the three questions asked initially regarding three particular
initial markings of the chameleon net. From the initial marking (
In the previous section we aimed at characterizing initial markings of the chameleon net with the property that a deadlock is reachable. Moreover, we provided a strategy to reach a deadlock, if possible.
Now we take the opposite view and try to avoid deadlocks. So our first question is whether the net with a given initial marking necessarily reaches a deadlock eventually or if the initial marking enables an infinite occurrence sequence. Again, we aim at a characterization of those initial markings that allow for infinite occurrence sequences, and in turn of initial markings that make the net terminating eventually.
As seen in the previous section, deadlock states of the chameleon game are easily characterized: A state of the chameleon game is a deadlock if and only if all chameleons have the same color and hence no color change is possible any more. In terms of markings of the chameleon net, a marking is a deadlock marking, if and only if (at least) two of the places , and are unmarked. So the question from above translates to the question whether it is possible to ifre transitions in such a way that always at most one place is unmarked.
An analysis of the chameleon net shows that the net has three minimal siphons: {, }, {, } and {, }. So the deadlocks are exactly those markings where a siphon is unmarked. Remember that, in general, whenever a marking is a deadlock, some siphon is unmarked. In our example net, the converse holds as well.
If the initial marking is already a deadlock, then the answer to the above question is simple and negative. Otherwise we look at the last marking before reaching a deadlock. It is easily seen that at this marking two places must carry exactly one token each, and that the transition removing these two tokens leads to the deadlock. So we can avoid reaching a deadlock immediately if at least one of the input places of the according transition carries at least two tokens. The following lemma states that this condition is also suficient for non-termination, i.e., for the existence of an infinite occurrence sequence.
Proof. Assume that 0() ≥ 2 and 0() ≥ 1, where and are distinct places (and is the remaining place). Then the transition in the pre-set of is enabled. Its occurrence leads to a marking with () = 0() + 2 ≥ 2 and () = 0() − 1 ≥ 1. So we have the same situation as initially: one place carries at least two tokens (now it is ) and a distinct place (now ) carries at least one token. This argument can be repeated arbitrarily, and a deadlock is never reached. In other words: Applying this strategy, the condition is invariant.
Conversely, assume that there is an infinite occurrence sequence from the initial marking (0, 0, 0). Consider the first two transition occurrences and in this sequence, i.e., the sequence starts with . If = , then both places in the pre-set of this transition carry initially at least two tokens. If ̸= then the place which is neither in the post-set of nor in the post-set of is in both pre-sets. Hence it initially carries at least two tokens, because is enabled at 0. The other place in the pre-set of carries initially at least one token, because is enabled at 0.
In terms of chameleons, Lemma 2 states that the game does not terminate if and only if at least two chameleons have the same color and two chameleons have diferent color. The following corollary provides a characterization of the negated property: Corollary 2. The chameleon game terminates if and only if at least one of the following conditions holds:
chameleon)
It might be worth mentioning that for four or more chameleons, the net inevitably terminates if and only if the initial marking is already a deadlock, because otherwise at least one of the three colors must appear twice and also diferent colors appear. For three chameleons, the net moreover terminates if all chameleons have diferent colors, because after one (arbitrary) step, they all will have the same color. For two chameleons, either the initial marking is a deadlock (same color) or a deadlock is reached after one step (diferent color), whereas one chameleon will stay lonely forever anyway and zero chameleons do not have to be considered.
We have presented a puzzle, translated it into Petri nets and used Petri net analysis techniques for finding answers to the puzzle and other relevant information. None of this constitutes results to scientific problems nor to real world applications. However, the chameleon net presented in this paper can be used in many ways to explain how to model systems with Petri nets (in the small) and how to provide answers to questions about a system using Petri net techniques. The chameleon example can be used for motivation and explanation of Petri net analysis techniques as well as for various student exercises, where students are asked to find solutions based on learned Petri net techniques and general proof techniques. For example, the example can be used as a motivating example for the introduction of modulo-invariants. In this case, students are asked to find the particular invariant property that holds for this net, and then modulo-invariants are introduced as a general concept that formalizes this invariant. If modulo-invariants are already known, then the example can be used as an exercise of finding an appropriate modulo-invariant.
A particular importance of examples like this one is that students get a feeling for when which modeling construct and which analysis method can be used and/or is promising, also in a bigger setting.
The Petri net community lacks a systematic collection of nontrivial examples, although small examples can be found in many scientific papers and textbooks on Petri nets. For explaining a new technique, the examples are just big enough to understand the new idea, but often the same results could easily be obtained without the technique. On the other hand, industrial examples are here and there published, but in general they can hardly be used for educational purpose – too many aspects are relevant in practice, the examples are too large to be used in classes, and students can only take the role of recipients, where no active engagement is possible.
I hope that this and existing or new examples of medium complexity and dificulty will be collected in future to serve as an example collection for the community, as a pool for educational purposes, but also as a source to test new techniques and compare with existing ones.