This paper explores the use of Coloured Petri Nets (CPNs) as a formal modeling tool for solving combinatorial problems. Focusing on a book distribution problem, we demonstrate how CPNs help visualize and systematically verify various proposed solutions. By constructing CPN models and generating the corresponding state spaces, we identify the correct solution and diagnose reasoning errors in alternative approaches. The study highlights the similarities between combinatorial problem-solving and system modeling, particularly in addressing hidden constraints and managing state space explosion. Our findings underscore the potential of formal methods like CPNs as educational tools for enhancing understanding in combinatorics and improving students' problem-solving skills.
Such uncertainties can be efectively addressed through formal specification techniques, which help to make assumptions more explicit. In combinatorial analysis, enumerating all possible configurations quickly leads to an exponential growth of the solution space. The phenomenon closely mirrors the state space explosion encountered in formal methods. In both contexts, abstraction, through simplification or reduction, becomes crucial to making problems tractable. Furthermore, the systematic exploration of state spaces serves not only to identify correct solutions but also to provide critical insights into why alternative methods fail. This diagnostic process reveals underlying reasoning errors and uncovers overlooked constraints.
This paper investigates the relationship between combinatorial problem-solving and formal methods. In particular, we use Coloured Petri Nets (CPNs) to systematically model and analyze such problems. The remainder of the paper is organized as follows: Section 2 discusses the CPN models for the book distribution problem, identifying the correct methods and analyzing the reasoning errors in incorrect approaches. Section 3 reviews related work, and Section 4 concludes the paper. 2. The CPN Model of the Book Distribution Problem To solve the book distribution problem, we divide the problem into two distinct stages: first, the distribution of 10 distinct books, and second, the distribution of 8 identical balls. According to the Multiplication Principle2, the total number of possible outcomes is the product of the number of ways each event can occur. Since the distribution of identical balls can be addressed separately using the Stars and Bars3 technique, this section focuses primarily on modeling the distribution of the distinct books. Without loss of generality, we reduce the number of books to 6 to avoid state space explosion.
Figure 1 presents the Coloured Petri Nets (CPNs) model, a simplified version of the original problem, which captures the distribution of 6 distinct books among 3 students. The goal is to ensure that each student receives at least one book. 2The Multiplication Principle: If one event can occur in m ways and a second event can occur in n ways, then the sequence of these two events can occur in × ways. 3Stars and bars is a combinatorial technique for counting ways to divide identical items into distinct groups. To find positive integer solutions to 1 + 2 + · · · + = , we place − 1 bars among stars. The number of ways is (︀ − 1)︀ . − 1 A n C1 n
n 1`1++1`2++1`3++BOOKS 1`4++1`5++1`6
n INT 20
Alice
Depicted as an oval, the place BOOKS initially contains tokens representing the 6 distinct books (1 through 6), each treated as a unique value of type INT. The places Alice, Bob, Chalee represent where books are assigned to the respective students. Transitions shown as rectangles, represent the possible actions of assigning books from the place BOOKS to each of the students. Transitions labeled A1, B1, and C1 are used in conjunction with inhibitor arcs, which prevent firing unless the respective student’s place is empty. These three transitions have higher priorities (10, 20 and 30 respectively) than transitions A, B, and C to ensure that each student receives one book in the first round. The total state space consists of 2,137 states. There are 540 terminal markings. Each represents a valid distribution where all books are assigned and every student has at least one book.
To compute the number of valid distributions using the inclusion-exclusion principle4 , note that each book has 3 possible recipients, giving a total of 36 = 729 ways. However, this count includes cases where one or two children receive no books. To correct this overlap: • Subtract the number of distributions where only 2 children receive books: 3 × 26 ways, • Add back the cases where only 1 child receives all books: 3 ways.
Thus, the total number of valid distributions where each child receives at least one book is: 36 − 3 × 26 + 3 = 540 4The inclusion-exclusion principle is used to count elements in the union of overlapping sets. For two sets, the formula is: | ∪ | = || + || − | ∩ | It corrects for elements counted twice in the overlap. This idea extends to three or more sets by alternately subtracting and adding intersections.
1: fun ev1(n) = if (Mark.BOOK’Alice 1 n)<>empty andalso (Mark.BOOK’Bob 1 n)<>empty 2: andalso (Mark.BOOK’Chalee 1 n)<>empty then true else false; 3: fun ev2(n) = if (Mark.BOOK’Alice 1 n) = empty then true else false; 4: fun ev3(n) = if (Mark.BOOK’Alice 1 n) = empty 5: andalso (Mark.BOOK’Bob 1 n)= empty then true else false; 6: val _ = print("Satifies Some students have not received any books.:");7: length(ListDeadMarkings()); 8: val _ = print("Satifies Alice has not received any books.:"); 9: length(PredNodes(ListDeadMarkings(), ev2, NoLimit)); 10: val _ = print("Satifies Neither Alice nor Bob has received any books.:");11: length( PredNodes(ListDeadMarkings(), ev3, NoLimit)); 12: val _ = print("Satifies Each student receives at least one book.:");13: length (PredNodes(ListDeadMarkings(), ev1, NoLimit));
The second approach organizes the arrangement in two steps. First, arrange the six distinct books in a row, which can be done in 6!= 720 ways. Then, in each case, use the Stars and Bars method to divide the six books into three distinct groups, which can be done in (︀ 6−− 11)︀ = 10 ways. Thus, the total number 3 of possible arrangements by this method is 720 × 10 = 7, 200 ways.
The second method leads to an incorrect answer because it allows the books within each group to be permuted, whereas in the actual problem, the books held by each child are not reordered. In fact, the second method models a scenario where books are arranged onto three shelves, with the order of books on each shelf being significant.
Figure 5 illustrates the CPN model for the case where books are arranged onto three shelves with internal permutations allowed. The model closely resembles that in Fig. 1 but to capture the ordering of books, tokens are represented by the List type instead of a multi-set. Transitions A1, B1, C1 play the same purpose as the corresponding transitions in Fig. 1. However, rather than using inhibitor arcs, a guard [length(ln) = 0] is employed to check whether the token is a null list. The generated state space contains 12,757 states and 7,200 terminal markings.
This method divides the distribution process into three stages. First, select a group of three distinct books from the six available, which can be done in (︀ 6)︀ =20 ways. Second, distribute these three books in 3 order among the three children, which can be done in 3! = 6 ways. Finally, assign each of the remaining [length(ln) = 0]
A1 10 1`1++1`2++1`3n++ 1`4++1`5++1`6 [length(ln) = 0] 30
C1 ln n ln ln^^[n]
n BOOKS
INT Chalee 1`[] L_INT
L_INT ln n ln n n
A C n n ln^^[n]
B ln^^[n] ln ln ln^^[n]
B1 20 [length(ln) = 0]
Bob L_INT three books independently to any of the three children, giving 33 =27 possible distributions. Thus, the total number of arrangements according to this method is 20 × 6 × 27 = 3, 240 ways.
Figure 6 shows the CPN diagram representing the distribution process in three stages. The resulting state space comprises 2,322 states and 540 terminal markings, which correspond to the correct number of valid distributions. When transitions in the second and third stages are disabled, the state space yields 20 terminal markings matching the number of combinations from the first stage. Disabling only the third stage results in 120 terminal markings, consistent with the product of the first two stages. When all three stages are active, the number of terminal markings is 540, indicating that the original 3,240 configurations have been folded together due to equivalence in the final distributions.
A counterexample is taken from the generated state space. This confirms that the method overcounts distinct arrangements. Consider the following two cases: • Case I: Alice selects Book No.1 .
• Case II: Alice selects Book No.4
Both cases then proceed with identical actions. In the final step, Case I: Alice selects Book No.4, and Case II: Alice selects Book No.1. This leads to the same final distribution. However, the multiplication principle treats them as distinct due to diferent initial choices, even though the outcomes are equivalent. Therefore, this method results in overcounting and produces an incorrect answer.
This final approach presumes that the final distribution of books among the three children falls into one
of the following patterns: (
Thus, the total number of possible arrangements is: 90+360+90 = 540 ways.
Figure 7 illustrates the CPN model for the configuartion (
Combinatorics education has been widely discussed in research, particularly with regard to the dificulties when the students learn the subject. A recurring theme in the literature is the over-reliance on formulas and a lack of conceptual understanding among students, which hinders their ability to grasp the principles of counting and combinatorial reasoning.
Syahputra [4] investigates students’ dificulties in solving combinatorics problems and their strategies. The study involving 36 high school students and 67 first-year college mathematics education students revealed very poor combinatorial ability. Given five problems, only 35% answered the first correctly, 10.68% the second, none got the third right, 1.9% solved the fourth, and only 0.97% solved the fifth. The analysis suggests that most students did not understand the problems, rarely used enumeration, and generally avoided building mathematical models but relying on memorized formulas. Intensive practice using enumeration, pattern recognition, and trial-and-error methods is recommended to improve their skills.
Lockwood [5] shows students struggle with counting problems due to incorrect understanding of combinatorics. Lockwood developed a model to analyze students thinking, focusing on relationships among counting processes, outcomes, and formulas. The model describes how students conceptualize counting tasks and explains common dificulties. It also ofers a framework for teachers designing experiments and identifying sources of student errors. Finally, the model provides a foundation for better instructional strategies in combinatorics education.
Sriraman and English [6] explains that students often struggle with combinatorics due to confusion between permutations and combinations. It defines combinatorics as the art of counting arrangements of finite sets and emphasizes its role in flexible and independent thinking. Researchers use multiple representations for students to build structural understanding. Collaborative problem-solving and problem-posing activities can further enhance creativity, and conceptual understanding.
This paper explored the application of Coloured Petri Nets to model a combinatorial problem and evaluate potential solutions. Using CPNs to visualize and analyze the problem, we can identify the correct solution and diagnose the reasoning errors such as overcounting and unintended permutations. Through abstraction and model simplification, we can reduce the complexity and make the problem tractable. Using formal methods like CPNs provides better understanding and teaching combinatorial concepts. Finally, this study underscores the value of formal tools in both system modeling and mathematical problem-solving education.
During the preparation of this work, the author used GPT-4 in order to: Grammar and spelling check. After using this tool/service, the author reviewed and edited the content as needed and takes full responsibility for the publication’s content.