Paper | |
---|---|
edit | |
description | |
id | Vol-3170/short1 |
wikidataid | Q117351473→Q117351473 |
title | The Chameleon Game |
pdfUrl | https://ceur-ws.org/Vol-3170/short1.pdf |
dblpUrl | https://dblp.org/rec/conf/apn/Desel22 |
volume | Vol-3170→Vol-3170 |
session | → |
Paper | |
---|---|
edit | |
description | |
id | Vol-3170/short1 |
wikidataid | Q117351473→Q117351473 |
title | The Chameleon Game |
pdfUrl | https://ceur-ws.org/Vol-3170/short1.pdf |
dblpUrl | https://dblp.org/rec/conf/apn/Desel22 |
volume | Vol-3170→Vol-3170 |
session | → |
The Chameleon Game Jörg Desel FernUniversität in Hagen, Germany Abstract A little puzzle is presented, together with a corresponding Petri net model. Conditions for deadlock- freedom and for the termination property are proven necessary and sufficient. This example might be helpful for education issues w.r.t. modeling of systems, modeling of properties, techniques for decid- ing deadlock-freedom and for termination such as siphons and invariants and, more generally, proof techniques. Keywords Petri Net Examples, Education, Deadlock-Freedom, Termination, Proof Techniques, Chameleons 1. Introduction 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 different, 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 PNSE’22, International Workshop on Petri Nets and Software Engineering, Bergen, Norway, 2022 " joerg.desel@fernuni-hagen.de (J. Desel) ~ https://www.fernuni-hagen.de/sttp/team/joerg.desel.shtml (J. Desel) © 2022 Copyright for this paper by its author. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) 202 �Jörg Desel CEUR Workshop Proceedings 202–210 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 sufficient in most application examples. My personal motivation for this work is that I found the task statement completely inde- pendent 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. 2. The Chameleon Game 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 different 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. 203 �Jörg Desel CEUR Workshop Proceedings 202–210 bgr 2 red 2 2 Figure 1: Petri net model of the Chameleon Game 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 different 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 firing 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 sufficient 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. 3. Deadlock-Freedom As long as there are chameleons with different 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 204 �Jörg Desel CEUR Workshop Proceedings 202–210 not enable any transition and therefore is a deadlock. We consider the following three questions: 1. Is there a finite occurrence sequence from marking (4, 2, 1) to a deadlock? 2. Is there a finite occurrence sequence from marking (5, 2, 1) to a deadlock? 3. Is there a finite occurrence sequence from marking (6, 2, 1) to a deadlock? In the positive case, the answer is simple: a suitable occurrence sequence leading to a deadlock is a sufficient answer. In the negative case, however, we are looking for a proof that no such occurrence sequence exists. 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 −1 −1 A = ⎝ −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 (1, 1, 1) (and its multiples), which states that the overall number of tokens (chameleons) never changes. 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 (1, −1, 0), (1, 0, −1), (0, 1, −1) and (1, 1, 1) (every place invariant is also a modulo-𝑛-invariant for every 𝑛), as well as sums and differences of these vectors. For example, (1, −1, 0) states that the difference between the respective numbers of red 205 �Jörg Desel CEUR Workshop Proceedings 202–210 and blue chameleons will always differ from the initial difference by a multiple of 3. In the exam- ple shown in Figure 1, for every reachable marking 𝑚 we have 𝑟 − 𝑏 ∈ {. . . , −4, −1, 2, 5, . . .} because 𝑟0 − 𝑏0 = 2. 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. Proof. =⇒ Assume that (𝑟0 + 𝑏0 + 𝑔0 , 0, 0) is reachable from (𝑟0 , 𝑏0 , 𝑔0 ). 𝑏0 ≡ 𝑔0 (mod 3) follows by the mod-3 invariant (0, 1, −1) and because 0 = 𝑏 = 𝑔 = 0 ≡ 0 (mod 3) . 𝑟0 +𝑏0 > 0 since otherwise the initial marking is a deadlock (0, 0, 𝑔0 ) with 𝑔0 = 𝑟0 +𝑏0 +𝑔0 > 0, contradicting reachability of (𝑟0 + 𝑏0 + 𝑔0 , 0, 0). 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 (0, 1, −1) is a modulo-3-invariant of the chameleon net. Moreover, we have 𝑟 + 𝑏 + 𝑔 = 𝑟0 + 𝑏0 + 𝑔0 because (1, 1, 1) is a place invariant. 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 fire 𝑔𝑟𝑏. 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 𝑟𝑏𝑔. 206 �Jörg Desel CEUR Workshop Proceedings 202–210 Corollary 1. A deadlock is reachable if and only if 𝑏0 ≡ 𝑔0 (mod 3) or 𝑔0 ≡ 𝑟0 (mod 3) or 𝑟0 ≡ 𝑏0 (mod 3). In other words, no deadlock is reachable if and only if {(𝑏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 (0, 1, −1) we have 𝑏0 ≡ 𝑔0 (mod 3). For the other two cases, the same argument applies to the respective other pairs of places. 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 ini- tial markings of the chameleon net. From the initial marking (4, 2, 1) a deadlock can be reached because 4 ≡ 1 (mod 3). From the marking (5, 2, 1) a deadlock can be reached because 5 ≡ 2 (mod 3). From the marking (6, 2, 1) no deadlock can be reached because {6, 2, 1} ≡ {0, 1, 2} (mod 3), i.e., the numbers 6, 2 and 1 represent all three equivalence classes modulo 3. 4. Termination 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 207 �Jörg Desel CEUR Workshop Proceedings 202–210 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 fire 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 sufficient for non-termination, i.e., for the existence of an infinite occurrence sequence. Lemma 2. The chameleon has an infinite occurrence sequence if and only if initially one of its places carries at least two tokens and another place carries at least one token. 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 different 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: 1. Two places are unmarked (all chameleons have the same color) 2. The overall number of tokens is less than three (there are less than three chameleons) 3. All three places carry exactly one token initially (there is one red, one blue and one green chameleon) 208 �Jörg Desel CEUR Workshop Proceedings 202–210 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 different colors appear. For three chameleons, the net moreover terminates if all chameleons have different 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 (different color), whereas one chameleon will stay lonely forever anyway and zero chameleons do not have to be considered. 5. Conclusion 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 difficulty 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. References [1] W. Reisig, Elements of distributed algorithms: modeling and analysis with Petri nets, Springer, 1998. [2] H. Dambeck, M. Niestedt, Verwirrspiel im Terrarium, https://www.spiegel.de/karriere/ 209 �Jörg Desel CEUR Workshop Proceedings 202–210 verwirrspiel-im-terrarium-raetsel-der-woche-a-404e0560-ca83-418c-a5f3-8acfa3167d3d, 2021. Accessed: 2022-03-01. [3] A. Beutelspacher, Das Geheimnis der zwölften Münze: Neue mathematische Knobeleien, C.H.Beck, 2021. [4] W. Reisig, Petri Nets: An Introduction, volume 4 of EATCS Monographs on Theoretical Computer Science, Springer, 1985. [5] J. Desel, J. Esparza, Free Choice Petri Nets, Cambridge University Press, USA, 1995. [6] J. Desel, K.-P. Neuendorf, M.-D. Radola, Proving nonreachability by modulo-invariants, Theoretical Computer Science 153 (1996) 49–64. 210 �
The Chameleon Game Jörg Desel FernUniversität in Hagen, Germany Abstract A little puzzle is presented, together with a corresponding Petri net model. Conditions for deadlock- freedom and for the termination property are proven necessary and sufficient. This example might be helpful for education issues w.r.t. modeling of systems, modeling of properties, techniques for decid- ing deadlock-freedom and for termination such as siphons and invariants and, more generally, proof techniques. Keywords Petri Net Examples, Education, Deadlock-Freedom, Termination, Proof Techniques, Chameleons 1. Introduction 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 different, 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 PNSE’22, International Workshop on Petri Nets and Software Engineering, Bergen, Norway, 2022 " joerg.desel@fernuni-hagen.de (J. Desel) ~ https://www.fernuni-hagen.de/sttp/team/joerg.desel.shtml (J. Desel) © 2022 Copyright for this paper by its author. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) 202 �Jörg Desel CEUR Workshop Proceedings 202–210 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 sufficient in most application examples. My personal motivation for this work is that I found the task statement completely inde- pendent 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. 2. The Chameleon Game 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 different 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. 203 �Jörg Desel CEUR Workshop Proceedings 202–210 bgr 2 red 2 2 Figure 1: Petri net model of the Chameleon Game 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 different 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 firing 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 sufficient 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. 3. Deadlock-Freedom As long as there are chameleons with different 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 204 �Jörg Desel CEUR Workshop Proceedings 202–210 not enable any transition and therefore is a deadlock. We consider the following three questions: 1. Is there a finite occurrence sequence from marking (4, 2, 1) to a deadlock? 2. Is there a finite occurrence sequence from marking (5, 2, 1) to a deadlock? 3. Is there a finite occurrence sequence from marking (6, 2, 1) to a deadlock? In the positive case, the answer is simple: a suitable occurrence sequence leading to a deadlock is a sufficient answer. In the negative case, however, we are looking for a proof that no such occurrence sequence exists. 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 −1 −1 A = ⎝ −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 (1, 1, 1) (and its multiples), which states that the overall number of tokens (chameleons) never changes. 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 (1, −1, 0), (1, 0, −1), (0, 1, −1) and (1, 1, 1) (every place invariant is also a modulo-𝑛-invariant for every 𝑛), as well as sums and differences of these vectors. For example, (1, −1, 0) states that the difference between the respective numbers of red 205 �Jörg Desel CEUR Workshop Proceedings 202–210 and blue chameleons will always differ from the initial difference by a multiple of 3. In the exam- ple shown in Figure 1, for every reachable marking 𝑚 we have 𝑟 − 𝑏 ∈ {. . . , −4, −1, 2, 5, . . .} because 𝑟0 − 𝑏0 = 2. 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. Proof. =⇒ Assume that (𝑟0 + 𝑏0 + 𝑔0 , 0, 0) is reachable from (𝑟0 , 𝑏0 , 𝑔0 ). 𝑏0 ≡ 𝑔0 (mod 3) follows by the mod-3 invariant (0, 1, −1) and because 0 = 𝑏 = 𝑔 = 0 ≡ 0 (mod 3) . 𝑟0 +𝑏0 > 0 since otherwise the initial marking is a deadlock (0, 0, 𝑔0 ) with 𝑔0 = 𝑟0 +𝑏0 +𝑔0 > 0, contradicting reachability of (𝑟0 + 𝑏0 + 𝑔0 , 0, 0). 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 (0, 1, −1) is a modulo-3-invariant of the chameleon net. Moreover, we have 𝑟 + 𝑏 + 𝑔 = 𝑟0 + 𝑏0 + 𝑔0 because (1, 1, 1) is a place invariant. 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 fire 𝑔𝑟𝑏. 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 𝑟𝑏𝑔. 206 �Jörg Desel CEUR Workshop Proceedings 202–210 Corollary 1. A deadlock is reachable if and only if 𝑏0 ≡ 𝑔0 (mod 3) or 𝑔0 ≡ 𝑟0 (mod 3) or 𝑟0 ≡ 𝑏0 (mod 3). In other words, no deadlock is reachable if and only if {(𝑏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 (0, 1, −1) we have 𝑏0 ≡ 𝑔0 (mod 3). For the other two cases, the same argument applies to the respective other pairs of places. 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 ini- tial markings of the chameleon net. From the initial marking (4, 2, 1) a deadlock can be reached because 4 ≡ 1 (mod 3). From the marking (5, 2, 1) a deadlock can be reached because 5 ≡ 2 (mod 3). From the marking (6, 2, 1) no deadlock can be reached because {6, 2, 1} ≡ {0, 1, 2} (mod 3), i.e., the numbers 6, 2 and 1 represent all three equivalence classes modulo 3. 4. Termination 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 207 �Jörg Desel CEUR Workshop Proceedings 202–210 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 fire 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 sufficient for non-termination, i.e., for the existence of an infinite occurrence sequence. Lemma 2. The chameleon has an infinite occurrence sequence if and only if initially one of its places carries at least two tokens and another place carries at least one token. 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 different 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: 1. Two places are unmarked (all chameleons have the same color) 2. The overall number of tokens is less than three (there are less than three chameleons) 3. All three places carry exactly one token initially (there is one red, one blue and one green chameleon) 208 �Jörg Desel CEUR Workshop Proceedings 202–210 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 different colors appear. For three chameleons, the net moreover terminates if all chameleons have different 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 (different color), whereas one chameleon will stay lonely forever anyway and zero chameleons do not have to be considered. 5. Conclusion 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 difficulty 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. References [1] W. Reisig, Elements of distributed algorithms: modeling and analysis with Petri nets, Springer, 1998. [2] H. Dambeck, M. Niestedt, Verwirrspiel im Terrarium, https://www.spiegel.de/karriere/ 209 �Jörg Desel CEUR Workshop Proceedings 202–210 verwirrspiel-im-terrarium-raetsel-der-woche-a-404e0560-ca83-418c-a5f3-8acfa3167d3d, 2021. Accessed: 2022-03-01. [3] A. Beutelspacher, Das Geheimnis der zwölften Münze: Neue mathematische Knobeleien, C.H.Beck, 2021. [4] W. Reisig, Petri Nets: An Introduction, volume 4 of EATCS Monographs on Theoretical Computer Science, Springer, 1985. [5] J. Desel, J. Esparza, Free Choice Petri Nets, Cambridge University Press, USA, 1995. [6] J. Desel, K.-P. Neuendorf, M.-D. Radola, Proving nonreachability by modulo-invariants, Theoretical Computer Science 153 (1996) 49–64. 210 �