K-Machinations: Testing and Repairing Machinations Diagrams
摘要
Machinations is a visual design language widely used in the computer game development industry to model and analyze game economy rules. The models created are graphical diagrams that can be executed similarly to a program. Execution is done in different scenarios to analyze the behavior of the modeled game. However, the lack of formal semantics makes it difficult to ascertain the correctness of the execution of graphical diagrams. In this work, we develop K-Machinations, a formal high-level executable semantics for Machinations in the K framework. We apply K-Machination to validate the implementation of Machination commercial platform, comparing the executions of several graphical diagrams to uncover six types of defects that can lead to wrong decisions in games design. Our tool can also provide solutions to repair incorrect diagrams.