Model kontrolcüsü SPIN ile labirent benzeri oyun seviyelerini doğrulamak

In this thesis, we present a new methodology that includes procedural generation and verification of maze-like game levels. The methodology employs a model checker, called SPIN, in order to both produce a winning sequence of actions and to formally verify custom game design properties. In order to verify a game level, we propose automated tailoring on template game models, considering the level-in-test, specifically designed according to the game rules. By leveraging the counterexample generation feature of SPIN, we find one or more solutions to the level-in-test, and use PyVGDL to animate the solutions. In order to show this methodology's effectiveness, we conducted five different experiments. These experiments include performance comparisons in level solving between the proposed and existing methodologies, A-star search Monte Carlo tree search, and demonstrations of the proposed approach's usage to verify a game level with respect to existing requirements. The work also includes a pipeline for the generation of maze-like puzzle levels that includes two levels of cellular automata.