Students face unfamiliar abstract concepts when learning about formal methods and Petri net modeling. These concepts are challenging for students to understand fully and for teachers to design captivating modeling exercises that align with the intended learning outcomes. The proposed exercises should provide significant opportunities to apply abstract concepts in familiar domains, bridging the gap between the concrete and the abstract. Board games ofer a range of modeling problems in an area that many students know. This paper introduces a model for Sokoban, a classic computer-based, one-player puzzle game. After, a sequence of possible Petri net modeling exercises focused on the game movement rules and model composition are proposed. The complete model is created by composing multiple instances of the previously defined models acting as modules. The complete model can then be used to verify game termination and obtain the net step sequence leading to the intended final net marking.
Exercises are a core component of learning and assessment and must fulfill a dual role: they must align with the intended learning outcomes and be perceived by students as interesting and motivating.
Due to the well-known capacity to engage students, games are frequently used for pedagogical
purposes (e.g., [
We propose using simple tile-based games, sometimes called grid-based games, as an adequate basis for teaching and learning Petri net modeling. More specifically, we argue that many of those games ofer the following advantages:
2. Huge variety, from very simple to very complex ones; 3. Graphical representations allowing a visual mapping between the physical board and the Petri net model structure; 4. A clear diferentiation between the passive part (the board) and the active part (moving pieces and their movement rules, including restraints).
We present the Sokoban game as an illustrative example. This game, with its grid-based structure and movement rules, is a concrete application that exemplifies the above-listed advantages.
The paper is structured as follows. In the next section, we present the game Sokoban. In Section 3, we present a sequence of proposed exercises and the respective possible solutions focusing on the movement rules of the game and the subsequent composition that yields the complete model amenable to simulation or state-based exploration. Finally, we conclude with some proposals for future work.
Sokoban has been named "the quintessential “block pushing” game " [
Wall A cell that cannot be occupied by the player or a box; these cells also serve to delimit the level board.
The Wikipedia webpage provides a simple and short introduction to the Sokoban game, illustrated
with an animated gif [
Even Sokoban basic levels necessitate significant computational resources, as there are many branches
and possible deadlocks, and a vast number of steps can quickly be needed to reach a solution [
The following section presents a sequence of possible student exercises. It corresponds to a step-wise and module-based approach for constructing a complete Sokoban level.
Here, we present six sequential exercises toward a complete model for a Sokoban game level and its analysis using Place/Transition nets. First, we focus on the player movement, either by simply moving to an adjacent position or by pushing a box; secondly, we present how that model can be split into a passive and an active part; finally, using a textual description, we show how multiple instances of these two small modules can be composed to generate a level with all the possible movements in that level.
When presenting the game to the students, the obvious challenge is to model the player’s movements. Here, we split the player movement into two cases: (1) the end position is free; (2) the end position has a box. 3.1.1. Free movement
2. How do we know where the player is; 3. How the model moves the player from one position to the other; 4. How the model checks if the end position is free.
The student’s first solution does not need to distinguish between an end position with a box or a wall. This distinction can be required for a second solution, as it should be clear that it will be needed for the case where the player has to move a box. Fig. 2b illustrates a solution with two places, for the begin and end positions, respectively, that need the end position to be free for the transition freeMove to be enabled. The transition firing models the player’s movement. 3.1.2. Movement pushing a box The cases to be presented to students in a second exercise are shown in Fig. 3a. The player moves to a position where a box is. The students have to consider the following aspects that are to be expressed in the model: 1. How the initial and end box position are modeled; 2. How to know where the player is; 3. How the model moves the player from one position to the other; 4. How the model moves the pushed box from one position to the other; 5. How the model moves the player and the pushed box synchronously; 6. How the model checks if the end position has a box; 7. How the model checks if the box’s intended end position is free (from a box or a wall).
In this second exercise, it should be apparent from the beginning that the box and the player must change their positions. An additional complication is that a total of three positions must be considered, as the position after the box is also a possible restriction to the player’s (and the box’s) movement. The need to test and update the presence and the absence of a box presents a new dificulty that provides an opportunity to discuss the use of complementary places. In addition, it is helpful to discuss whether we need a complementary place for the wall and what information we need in each position.
Fig. 3b illustrates a solution. It is centered on the "push box" action, which is modeled by transition pushBox. It uses complementary places for boxes in the initial box position and in the position where the box is going to be pushed. It also checks whether or not there is a wall in the box end position. The chosen layout has all places related to the same cell (position) in the same row to highlight the number of positions involved and the data needed for each position state. 3.1.3. Movement composition A third, more straightforward exercise is to compose both movements into a single one. The solution is presented in Fig. 4.
A fourth exercise is identifying all the state information needed for each position as a step toward modeling movement in both directions. Fig. 5a presents the solution presented in Fig. 4 with all the places needed to store each position’s state. Their use in the two-way movement is illustrated in Fig. 5b.
The complete model, for a whole level, requires multiple compositions. A two-step approach can be presented to students: (1) identify the modules to be composed; (2) express the multiple compositions. 3.3.1. Modules identification The modeling of the two movements in two opposite directions can be seen as the modeling of the "passage" between those two positions. The following exercise can be the identification of the model for each position (each cell in the grid). Next, both the "passage" and the "cell" should be transformed into composable modules by identifying the "interface" nodes. The "interface" nodes are the ones that will be fused (merged) with nodes in other modules. It seems worth discussing the dual nature of "passages," which encapsulate the actions (moving from one position to another), and "cells," which encapsulate the game state. This duality is analogous to the one between Petri nets transitions and places. Hence, the module composition is particularly interesting when allowing and exhibiting this duality.
Figures 6a and 6b allow the composition of cell module instances with passages modules in between. Fig. 7 shows a high-level view of the whole game level of Fig. 1 as the composition of juxtaposed cell and passage instance modules. 3.3.2. Complete model The last modeling exercise can be the specification of all the necessary compositions. This exercise relies heavily on a tool that comprehensively supports model composition. Some textual language is probably the preferable approach. We present a possible pseudo-code for such composition (see Algorithm 1). The procedure receives four-cell module instances and one passage module instance. A set of place fusions connects the five instances. The whole level is built by the procedure. This procedure calls the procedure for each pair of positions (cells) with a passage between them. The function returns the positions with a passage between them, thus efectively defining the game-level structure but not the initial state (marking). The function receives those two positions’ coordinates and returns the four module instances needed for the composition. Functions . and . create new instances of module and module (identified by the respective parameters) if not yet created, and return the respective instance if already created.
If suitable tools are available to obtain the model for the complete level, using it for simulation or state-space analysis should be interesting. The state-space analysis is especially interesting for checking the reachability of the intended final marking (all boxes in the end cells) and the shortest path (step sequence) to reach it.
Algorithm 1 Create board (complete Petri net model) 1: procedure createBoard((1, 1), (2, 2)) 2: for all ((1, 1), (2, 2)) ∈ () do 3: Connect( FourCells( (x1, y1), (x2, y2) ), passage.create((x1, y1), (x2, y2)) ) 4: end for 5: end procedure 6: function connectionsList( ) 7: ◁ Position pairs with a passage in between 8: return ( ▷
Using the Sokoban game as an example, we have shown how a classic tile-based game can be used as a
basis for engaging P/T net modeling exercises. Considering low-level nets, the model also ofers good
opportunities to discuss and use test arcs, inhibitor arcs, or both to simplify the model. The game also
provides a suitable ground for high-level Petri net modeling, including coloured Petri nets [
In our future work, we recognize the necessity for a straightforward method to define and implement multiple module compositions. Specifically, this method should enable the composition of modular models in a declarative manner, utilizing a textual language.
This work was financed by Portuguese Agency FCT – Fundação para a Ciência e Tecnologia, in the framework of project UIDB/00066/2020.