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., [1,2] ) and are often a way to introduce students to programming (e.g., [3]). Furthermore, games offer domains that are well-known by most students.
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 offer the following advantages: 1. Game domain, which should foster student engagement; 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 differentiation 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 " [4]. It is a single-player tile-based board game with simple rules. However, it can quickly become highly challenging. It is played on a "map" made of adjoining tiles. Each tile can be seen as a cell in a grid. The player moves in one of four directions: left to right, right to left, top to bottom, and bottom to top. The objective is for the player to push all the boxes around the grid to put them in the final marked locations. If a box is adjacent, the player can push the box to the next cell in the same direction. However, for that to happen, the ending box position must be free, which means no (other) box or "wall" can be in that cell. Each tile can be from one of three types:
Free cell A cell that can also contain the player or a box;
End cell A free cell that is marked as a final destination of any one box;
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 [5]. Numerous Sokoban implementations and levels are readily available on the Internet. As a specially significant example, the website https://sokoban.info/ provides "more than 7500 levels". Fig. 1 illustrates one of the smallest and simplest levels available. 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 [6]. More precisely, the game domain has been proven NP-Hard [7], and PSPACE-complete [8]. Sokoban has also been the object of several studies regarding possible algorithms (e.g., [9]). Here, our object is to use the modeling of the level (board) and movement rules as motivating exercises for model construction using Place/Transition Petri nets. The Petri net reachability graph can then be used to explore the existence of solutions and the respective paths to them.
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. 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.
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: 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 difficulty 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.
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.
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.
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 effectively 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.
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 offers 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 [10] and reference nets [11,12,13]. The presented exercise sequence can be adapted to the modeling of other tile-based games by P/T nets, high-level nets, or even non-autonomous 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.