Debugging Non-Determinism: a Petrinets Modelling, Analysis, and Debugging Tool (Tool Demonstration) Simon Van Mierlo Hans Vangheluwe University of Antwerp University of Antwerp Email: simon.vanmierlo@uantwerpen.be Flanders Make vzw McGill University Email: hv@cs.mcgill.ca Abstract—Non-deterministic formalisms are used to model to manually check how that invalid state was reached. Tools for systems whose runtime behaviour is inherently non-deterministic analysing Petrinet models offer limited debugging capabilities. (its runtime execution might be different in consecutive runs, As an example, TINA [5] allows to step through a model’s even for the same inputs). To analyse these systems, the full state space is explored to check whether an unwanted state (for firing sequence manually, but does not offer more advanced example: deadlock, unsafe) can be reached. Debugging support capabilities such as breakpoints. for such formalisms is currently limited. This paper presents We extend the set of existing analysis operations with inter- a prototype tool which allows to interactively construct the active debugging operations that allow to steer the reachability reachability graph (by manually stepping). The construction can analysis in a direction deemed most useful by the modeller. In be automatically paused at the moment a state of interest is reached (breakpointing). This should lead to earlier detection a sense, we envision to combine the existing formal analysis of errors and easier resolution, since the user can observe and techniques with debugging operations to get the best of both control the reachability analysis. worlds: the reachability graph is constructed up to a point deemed interesting by the modeller (and paused automatically I. I NTRODUCTION using a breakpoint), after which they are free to step through Non-deterministic formalisms, such as Petrinets [1] provide the rest of the reachability analysis by hand. While our tool abstractions for natively modelling systems whose (inherent) is built for the Petrinets formalism, the techniques are general runtime behaviour can differ from one execution to the next, and can be applied to other non-deterministic formalisms. even for the same inputs. Examples include, amongst others, distributed systems, safety-critical embedded systems that can II. T OOL OVERVIEW be interrupted by its environment, and programs executing This section describes the Petrinets debugger. We first look on multiple threads accessing shared resources. By modelling at its architecture, which is based on the Modelverse [6], their inherent non-determinism, it becomes possible to ex- our (meta)modelling kernel and repository. Then, we describe haustively explore the state space of the system and infer the visual interface used for modelling Petrinet models and properties concerning its safety and liveness. A full state space debugging their reachability graphs. exploration might, however, take a long time to complete for non-trivial systems. A. Architecture Recently, multiple works have introduced debugging opera- Our architecture is based on the Modelverse, our modelling tions for a number of modelling formalisms [2], [3], [4]. Often, framework and repository [6]. In the Modelverse, we model these techniques deal with deterministic formalisms whose the abstract syntax of the Petrinets language: a model in the semantics result in an execution trace that evolves the state of language consists of a number of Places and Transitions. the system over time. Common operations, transposed from Places can have a number of (initial) tokens (an integer code debugging, include pausing, stepping (at several levels number) and can be connected to transitions; transitions can of granularity), (scaled) real-time simulation and breakpoints be connected to places as well. (automatic pauses on state conditions). The semantics of the language is defined in the Modelverse Debugging operations for non-deterministic formalisms in the form of an action language model (an analyser). The have not been thoroughly researched. This paper presents analyser produces a reachability graph, which consists of a a prototype debugging tool for Petrinets, which is a basic, set of reachable markings. A marking contains a number of but representative example of a non-deterministic formalism. tokens for each place. These markings are connected: a link Usually, to analyse a Petrinets model, its reachability graph is denotes that the destination marking can be reached from the constructed and subsequently queried: if an undesirable state source marking when a transition is triggered. A transition can be reached (for example, a deadlock state), the user needs can be triggered when all of its input places contain at least Modelverse 2) When the user has chosen one of the unexplored ClassDiagrams ActionLanguage ClassDiagrams markings, the marking is loaded into the Petrinet model and the analyser communicates which transi- <> <> tions are enabled (and unexplored) in that particular Petrinets PetrinetsAnalyser ReachabilityGraph marking. These transitions are highlighted in green <> and the user can choose one of them by clicking on produce_consume aReachabilityGraph it. 3) The analyser executes the transition and updates the <> (XMLHTTP)>> Python This mode is most interesting to go back to a (partially) unexplored node in the reachability graph and continue its construction from that point interactively. • Breakpoints allow the user to automatically pause the analysis when a certain condition on the state (i.e., the structure of the reachability graph) is reached. From there, the user can use one of the above operations to resume construction. C. Interface Fig. 1. The architecture of our solution. The visual modelling, analysis, and debugging interface is shown in Figure 2. At the top, the modelling interface for Petrinets is shown with a loaded model that describes a one token; it then subtracts one token from all its input places producer-consumer system (1). A toolbar allows to edit the and adds a token in all its output places (resulting in a new model (2). Below, the (partial) reachability graph is shown reachable marking). (3). A toolbar allows the user to control the analysis using Figure 1 visualises the architecture of our solution: the the operations defined in the previous subsection (4). In the Modelverse provides all modelling operations and allows screenshot, the user is manually controlling the analysis algo- to define an analyser in action code. It is deployed on a rithm and has selected the bottom-most marking (highlighted server which provides an API that is called using XMLHTTP in yellow). In the Petrinets model, the marking is loaded in requests. For visualization purposes, we implement a Python the places, and the enabled transitions are highlighted in green. Tkinter application which allows to visually model Petrinets in By clicking one of them, a new (unexplored) marking will be one window and analyse/debug them, showing the reachability added to the reachability graph. graph in a separate frame and allowing the user to interact with it. The following subsection explains which debugging III. C ONCLUSION operations we added to the reachability graph construction This paper presents a prototype visual modelling, analysis algorithm. Details on the visual modelling and debugging and debugging interface for Petrinets, chosen as a represen- interface are provided in the last subsection. tative non-deterministic formalism. The interface allows to model Petrinets and analyse them, visualising its reachability B. Debugging Operations graph as it is constructed. Additional control is given to the user in the form of debugging operations: the user can We define the following debugging operations: step through the reachability graph construction and manually • Continuous Operation executes the reachability graph control which marking is generated next. This allows users to construction algorithm until the full reachability graph interactively explore the reachability graph. In future work, has been generated (this is equivalent to running the these techniques can be used to build debuggers for more analyser without debugging support). advanced non-deterministic formalisms (such as model trans- • Step executes one analysis “step”: it generates one addi- formations [7], process modelling formalisms, etc.). tional reachable node in the reachability graph. • Manual allows the user to fully control the analyser ACKNOWLEDGMENT through the visual interface. The debuggable analyser will This work was funded by Flanders Make vzw, the strategic expose these phases in the algorithm and allow the user research centre for the manufacturing industry, and with a PhD to control them: fellowship from the Agency for Innovation by Science and 1) The analyser communicates all markings that are Technology in Flanders (IWT). We thank Yentl Van Tendeloo “unexplored”. An unexplored marking has at least for his support of and with the Modelverse. one enabled, non-explored transition. Unexplored markings are highlighted in the interface, and the user can choose on of them. R EFERENCES Parallel DEVS,” SIMULATION, vol. 93, no. 4, pp. 285–306, 2017. [Online]. Available: http://dx.doi.org/10.1177/0037549716658360 [5] B. Berthomieu and F. Vernadat, “Time petri nets analysis with [1] T. Murata, “Petri nets: Properties, analysis and applications,” Proceedings tina,” in Proceedings of the 3rd International Conference on the of the IEEE, vol. 77, no. 4, pp. 541–580, Apr 1989. Quantitative Evaluation of Systems, ser. QEST ’06. Washington, DC, [2] E. Bousse, J. Corley, B. Combemale, J. Gray, and B. Baudry, “Supporting USA: IEEE Computer Society, 2006, pp. 123–124. [Online]. Available: efficient and advanced omniscient debugging for xdsmls,” in Proceedings http://dx.doi.org/10.1109/QEST.2006.56 of the 2015 ACM SIGPLAN International Conference on Software Lan- [6] Y. Van Tendeloo, “Foundations of a multi-paradigm modelling tool,” in guage Engineering, ser. SLE 2015. New York, NY, USA: ACM, 2015, MoDELS ACM Student Research Competition, 2015, pp. 52–57. pp. 137–148. [7] J. Corley, B. P. Eddy, E. Syriani, and J. Gray, “Efficient and scalable om- [3] A. Chiş, M. Denker, T. Gı̂rba, and O. Nierstrasz, “Practical domain- niscient debugging for model transformations,” Software Quality Journal, specific debuggers using the moldable debugger framework,” Comput. pp. 1–42, 2016. Lang. Syst. Struct., vol. 44, no. PA, pp. 89–113, Dec. 2015. [4] S. Van Mierlo, Y. Van Tendeloo, and H. Vangheluwe, “Debugging Fig. 2. The visual modelling and debugging interface.