Complex systems, such as business processes, software systems, or protocols are often modeled by means of Petri nets [Aa13,Aa98,De01,De98,Pe81,Wo13]. Petri nets have a formal semantics and an intuitive graphical representation. However, constructing a Petri net model from a real world process is a costly and error-prone task [Aa13,Aa98,Ma07]. To support the modeling process, there is a big variety of different academic, as well as commercial tools to support the construction of valid process models. Most tools in that context feature some sort of synthesis or mining algorithm to automatically generate a process model from a behavioral specification. The most prominent tools in the area of synthesis are GENET [Ca09], Petrify [Co97], VipTool [Be08], and APT [Be15]. ProM [Aa09] is the most prominent framework in the area of process mining and supports a wide variety of process discovery techniques. The three most prominent commercial process mining tools are Celonis3, Minit4, and Disco [WGR12]. These tools have in common that they leave the relation between the resulting model and its underlying specification (e.g. an event log or a transition system) implicit, i.e. they only show the result of a synthesis procedure or a mining algorithm. In the present paper, we introduce a new split-screen module of travis to make the relation of two models explicit (e.g. a synthesized Petri net and its underlying behavioral specification or a Petri net and its calculated reachability graph), by also showing the relation between the input and the output by means of regions.
The focus of travis [Me17] is, on the one hand, to support the synthesis of systems with final states and, on the other hand, to introduce an easy to access online synthesis tool for the purpose of teaching theory related to modern synthesis techniques. Therefore, travis can synthesize a Petri net from a reachability graph and construct a reachability graph of a Petri net by an unfolding procedure. In all of its algorithms travis is able to handle and respect final states. travis was originally introduced in [Me17]. The goal of the new split-screen module is to apply travis in a teaching scenario where a split-screen view supports a learner during the modeling process by visualizing underlying concepts and intermediate results of the executed algorithms.
travis is developed in Java, using the Google Web Toolkit (GWT). GWT is an open source development kit for browser-based applications. The GWT compiler can generate HTML, CSS and JavaScript from Java code. Thus, travis is pure HTML, CSS and JavaScript. The travis homepage5 provides a short introduction and the example files used in this paper.
In the current version, travis offers two different kinds of editors: a transition system editor including an event log loader, and a Petri net editor. A model browser of travis enables the user to switch between multiple models or to delete models. Figure 1 shows an overview of the main features of travis where each editor is depicted by a framed box. The transition system editor of travis allows to load, create, and edit transition systems with or without final states. Within the editor, the user can toggle any set of states to be final. Of course, travis supports all standard editing features for states, labels, and transitions, and includes graph drawing algorithms like a simple spring layout and a tree layout. travis has a simple interface to import files. The event log loader of travis loads log-files in the standard XES file format [Ve11]. The user can drag-and-drop a stored file into the event log loader. To handle transition systems with final states, travis adapts the file format of the APT framework [Be15].
The Petri net editor of travis allows to load, create, edit, and simulate Petri nets with or without final markings. Again, travis supports all standard editing features and includes graph drawing algorithms. travis provides an options window where final markings can be created, edited, deleted, and highlighted in the Petri net at hand. travis uses the PNML file format [Ki06] to handle Petri nets and their sets of final markings. Using this format, travis is able to share Petri net files with analysis tools like VipTool, Charlie [He15] and WoPeD [Ec08].
In addition to the two main editors, Figure 1 depicts the core features and algorithms implemented in travis as bold arcs: (A) transformation of an event log into a transition system with final states, (B) synthesis of a k-bounded Petri net (see [Ca10]) extended by final states (see [Me16]) from a transition system with final states, (C) construction of the reachability graph -in terms of a transition system -with final states of a k-bounded Petri net with final states, and (D) adding a neat place (see [Me16]) to a k-bounded Petri net.
In the current version of travis, execution of either the synthesis (B) or the unfolding procedure (C) forces travis to switch to the editor related to the produced result i.e. either the transition system editor or the Petri net editor. Thus, the user loses information about the related construction process. For example, during the execution of the synthesis method, travis constructs the set of so-called minimal regions. This set characterizes the exact relation between the input (i.e. a transition system) and the calculated Petri net. Until now, travis was not able to visualize this set of regions although this is most valuable when trying to understand or analyze the processed synthesis procedure. Such a visualization is even more important when applying travis in a teaching scenario. The same holds for the unfolding procedure. Although, during the calculation of the reachability graph the set of all reachable states is computed, this information is lost when closing the Petri net editor and switching to the transition system editor.
In this paper, we present an obvious but elegant solution to the problem at hand. The actual version of travis features a new split-screen module which stores the set of minimal regions, as well as the set of reachable markings during the synthesis and unfolding procedures. travis is now able to visualize these sets using the new split-screen module by projecting regions to places of the Petri net and projecting markings to states of the transition system respectively the reachability graph.
Visualizing Regions with a new Split-Screen View for the Online Tool travis 189 14 Benjamin Meis, Robin Bergenthum
In the next section we will recapitulate the concept of regions, transition systems, and reachability graphs, before we introduce the new split-screen module in section three.
In this chapter, we will briefly recall the concepts of k-bounded Petri nets, their reachability graphs in terms of transition systems, and region-based synthesis. We refer the reader to [Ba15] for a detailed introduction. A transition t ∈ T is enabled at a marking m : P → N, if for all p ∈ P: m(p) ≥ W(p, t) holds. If t is enabled at m, t can fire. Firing t transforms m to a marking m . For every p ∈ P, m is defined by the equation m (p) = m(p) + W(t, p) − W(p, t). We write
A reachability graph is a transition system representing the behavior of a k-bounded place/transition net.
A transition system is a tuple T S = (S, T, Θ, s 0 ), where S is a finite set of states, T is a finite set of events, Θ ⊆ (S × T × S) is the set of labeled state transitions, and s 0 ∈ S is the initial state of T S. Let N = (P, T, W, m 0 ) be a marked place/transition net. The reachability graph of N is the transition system
Assuming a transition system modeling the behavior of a system, the synthesis problem aims at generating a Petri net so that its reachability graph is isomorphic to the specified transition system, i.e. both graphs with labeled arcs are identical up to the names of states.
Let T S be a transition system. The synthesis problem is to construct a k-bounded Petri net N such that its reachability graph is isomorphic to T S.
The synthesis problem is tackled using the theory of regions. We briefly recapitulate the theory of regions for the synthesis of k-bounded nets, but refer the reader to [Co98,Ca08b,Ca08a,Ca10] for a more detailed introduction.
Visualizing Regions with a new Split-Screen View for the Online Tool travis 15 Definition 2.4 (Region) Let T S = (S, T, Θ, s 0 ) be a transition system and r be a multiset of S. The gradient of a transition (s, t, s ) ∈ Θ is defined as ∆ r (s, t, s ) = r(s ) − r(s). An event t has a constant gradient in r if ∀(s, t, s ), (s , t, s ) ∈ Θ : r(s ) − r(s) = r(s ) − r(s ) holds. r is a region of T S if all events t ∈ T have a constant gradient in r.
We synthesize k-bounded place/transition nets. Thus, we only consider k-bounded regions.
The power of a multiset r is defined by r = max s ∈S r(s). A region is k-bounded if the power of the related multiset is less or equal to k. Every minimal k-bounded region of a transition system defines a place in the resulting Petri net solving the synthesis problem.
Like already stated in the introduction, travis has two built-in editors: a Petri net editor and a transition system editor. travis can synthesize a Petri net from a transition system (see (B) of Figure 1) and travis can calculate the reachability graph of a Petri net (see (C) of Figure 1) to kind of translate the reachability graph to a Petri net and vice versa. Until now, the user had access to only one of these editors at a time, i.e. travis either shows a single transition system or a single Petri net. Thus, it is not possible to see or visualize the direct relation between both models. In this chapter, we present a new split-screen module to show the Petri net and the related transition system.
During the synthesis of a Petri net, travis calculates the set of regions of the transition system at hand. This set is the link between the behavioral model, i.e. the transition system, and the Petri net model. Every region is a multiset of states with constant gradients for equally labeled transitions. A region and the gradients directly define a visible one-place Petri net, which is a possible and valid sub-net of a solution of the synthesis problem. More precisely, if we merge the set of sub-nets related to the set of minimal regions, we get the final result of the synthesis procedure for a k-bounded net. Looking at this from the other direction, for every place of the synthesized Petri net there is exactly one minimal region responsible for the existence of this place. Thus, really understanding the set of minimal regions of a transition system helps to understand and grasp the synthesis result.
When calculating the reachability graph of a k-bounded Petri net, travis performs a breadthfirst search on the set of consecutive enabled transitions of the Petri net and keeps track of the produced markings. Of course, every state of the reachability graph directly relates to a marking of the Petri net. But again, if we fix a place of the Petri net and project all calculated markings of all states to this place, we get a region of the reachability graph. So again, understanding this set of regions, as well as the set of produced markings of the reachability graph helps to clearly grasp the relation between the Petri net and its reachability graph.
Altogether, the set of regions and the set of reachable markings are two faces of the same coin. This set clearly pinpoints the relation between the transition system and the Petri net. We can calculate the set of regions by either performing the synthesis algorithm or
Visualizing Regions with a new Split-Screen View for the Online Tool travis 191
16 Benjamin Meis, Robin Bergenthum performing the unfolding algorithm of travis. We are able to visualize the set of regions by selecting one place and depicting the related region in the transition system and we are able to visualize the set of reachable markings by selecting a state and depicting the related marking in the Petri net.
To select places and states to visualize markings and regions, the new version of travis provides a split-screen module. The user simply clicks on the related button on the main toolbar of one of the editors to open this view. In this view, as depicted in Figure 2a and 2b, the Petri net editor is at the top and the transition system editor is at the bottom of the screen. At the upper left corner of each browser window, we see a small toolbar where the user can exit the split-screen view, can activate the default cursor to select and move elements, or can activate the token game mode to fire transitions of the Petri net. As an example, we synthesize a 3-bounded Petri net from a transition system. Figure 2a shows both models. The transition system consists of 17 states and includes five different events, a, b, c, d, and e. When the user clicks on place p 2 of the synthesized Petri net, the 192 Benjamin Meis, Robin Bergenthum
Visualizing Regions with a new Split-Screen View for the Online Tool travis 17 transition system editor shows the directly related multiset. The depicted multiset is a region, because all events have a constant gradient: the transition labeled by a has a gradient of +3, the transition labeled by b has a gradient of +2, transitions labeled by c have a gradient of −1, transitions labeled by d have a gradient of −1, and the transition labeled by e has a gradient of 0. The arc-weights of p 2 directly relate to the gradient of each event.
Whenever the user clicks on a place in the Petri net, the related minimal region of this place is depicted in the transition system. A region is a multiset of states of the transition system. Every state, which multiplicity is greater than zero is surrounded by a number of gray circles whereby the number of circles is equal to the multiplicity. For example, in Figure 2a, the state s 7 in the region related to place p 2 has three gray circles, i.e. in state s 7 , there are three tokens on place p 2 . The other way around, whenever the user clicks on a state of the transition system, travis shows the marking related to this state in the Petri net. Regarding regions, when a state of the transition system is selected, markings of the places in the Petri net are shown, whose regions have a multiplicity greater than zero in the selected state. For example, in Figure 2b, state s 7 is selected and only the regions of places p 2 and p 3 include state s 7 with a multiplicity greater than zero. Thus, there are tokens on places p 2 and p 3 .
The actual version of travis supports a state-based synthesis, calculating regions of a transition system. Thus, the split-screen module is limited to the visualization of regions in transition systems. Of course, it is possible to transfer the concept of the split-screen module to other notions of regions and synthesis algorithms provided that such an algorithm produces intermediate results -like state-based regions -which can be depicted within the model editor.
As one possible use case, we used travis with its split-screen view at our chair. We conducted a seminar on the topic Modeling Languages in Software Engineering with 13 of our students where one of the students talks was about Petri net synthesis. After his talk, we attached a short practical phase where all students had the chance to use travis and the split-screen view. With travis they modeled an exemplary transition system and synthesized a Petri net model.
To gain more insight into the synthesis algorithm presented by the student and to better understand the relations between places and regions, the students used the split-screen view of travis, where they could click on a place to display the related region in the transition system. We got the feedback, that the split-screen view is quite intuitive to use and that the visualization of both models at the same time helps to analyze the relation between the input and the output model, especially because when switching the focus between the two models, there is no visual interruption, like there would be when only one editor could be shown at a time.
The new split-screen module of travis is suitable for many use cases. As mentioned in the introduction, travis is an online tool which is executed in the browser and there is no need for any installation. Therefore, students and teachers within a learning environment have easy access to travis as a tool to support teaching scenarios, concerning the modeling of systems, especially with Petri nets.
This paper presents the new split-screen module for the online tool travis. travis can be executed simply in a browser and is free from any registration. Within travis, one can synthesize a Petri net from a transition system or unfold a Petri net by calculating its reachability graph. In an educational context, the new split-screen module of travis can further support teaching scenarios by visualizing the relations between Petri nets and transition systems and reachability graphs respectively in terms of regions. For future work, we will extend the split-screen module such that the user gains more detailed insights into the synthesis and unfolding procedures and gets more information about intermediate results.