-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 setvaetne sfporactehies esaxmpleoreindptuotsc)h.eTcok wanhaeltyhseer tahnesuenwsyasntetmeds,sttahtee (ffuolrl 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 intera 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 rbeeacahuetdom(batriecaakllpyoipnatiunsge)d. Tathitsheshmouolmdelnetada tsotaetaerloiefrindteetreecsttioins 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. INTRODUCTION using a breakpoint), after which they are free to step through the rest of the reachability analysis by hand. While our tool is built for the Petrinets formalism, the techniques are general and can be applied to other non-deterministic formalisms.
Non-deterministic formalisms, such as Petrinets [
Recently, multiple works have introduced debugging
operations for a number of modelling formalisms [
Debugging operations for non-deterministic formalisms have not been thoroughly researched. This paper presents a prototype debugging tool for Petrinets, which is a basic, but representative example of a non-deterministic formalism. Usually, to analyse a Petrinets model, its reachability graph is constructed and subsequently queried: if an undesirable state can be reached (for example, a deadlock state), the user needs
This section describes the Petrinets debugger. We first look
at its architecture, which is based on the Modelverse [
Our architecture is based on the Modelverse, our modelling
framework and repository [
The semantics of the language is defined in the Modelverse in the form of an action language model (an analyser). The analyser produces a reachability graph, which consists of a set of reachable markings. A marking contains a number of tokens for each place. These markings are connected: a link denotes that the destination marking can be reached from the source marking when a transition is triggered. A transition can be triggered when all of its input places contain at least one token; it then subtracts one token from all its input places and adds a token in all its output places (resulting in a new reachable marking).
Figure 1 visualises the architecture of our solution: the Modelverse provides all modelling operations and allows to define an analyser in action code. It is deployed on a server which provides an API that is called using XMLHTTP requests. For visualization purposes, we implement a Python Tkinter application which allows to visually model Petrinets in one window and analyse/debug them, showing the reachability graph in a separate frame and allowing the user to interact with it. The following subsection explains which debugging operations we added to the reachability graph construction algorithm. Details on the visual modelling and debugging interface are provided in the last subsection.
Continuous Operation executes the reachability graph construction algorithm until the full reachability graph has been generated (this is equivalent to running the analyser without debugging support).
Step executes one analysis “step”: it generates one additional reachable node in the reachability graph. Manual allows the user to fully control the analyser through the visual interface. The debuggable analyser will expose these phases in the algorithm and allow the user to control them: 1) The analyser communicates all markings that are “unexplored”. An unexplored marking has at least one enabled, non-explored transition. Unexplored markings are highlighted in the interface, and the user can choose on of them.
Modelverse
Python 2) When the user has chosen one of the unexplored markings, the marking is loaded into the Petrinet model and the analyser communicates which transitions are enabled (and unexplored) in that particular marking. These transitions are highlighted in green and the user can choose one of them by clicking on it. 3) The analyser executes the transition and updates the reachability graph.
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.
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 producer-consumer system (1). A toolbar allows to edit the model (2). Below, the (partial) reachability graph is shown (3). A toolbar allows the user to control the analysis using the operations defined in the previous subsection (4). In the screenshot, the user is manually controlling the analysis algorithm and has selected the bottom-most marking (highlighted in yellow). In the Petrinets model, the marking is loaded in the places, and the enabled transitions are highlighted in green. By clicking one of them, a new (unexplored) marking will be added to the reachability graph.
This paper presents a prototype visual modelling, analysis
and debugging interface for Petrinets, chosen as a
representative non-deterministic formalism. The interface allows to
model Petrinets and analyse them, visualising its reachability
graph as it is constructed. Additional control is given to
the user in the form of debugging operations: the user can
step through the reachability graph construction and manually
control which marking is generated next. This allows users to
interactively explore the reachability graph. In future work,
these techniques can be used to build debuggers for more
advanced non-deterministic formalisms (such as model
transformations [
This work was funded by Flanders Make vzw, the strategic research centre for the manufacturing industry, and with a PhD fellowship from the Agency for Innovation by Science and Technology in Flanders (IWT). We thank Yentl Van Tendeloo for his support of and with the Modelverse.