=Paper=
{{Paper
|id=Vol-2424/paper12
|storemode=property
|title=A First Prototype for the Visualization of the Reachability Graph of Reference Nets
|pdfUrl=https://ceur-ws.org/Vol-2424/paper12.pdf
|volume=Vol-2424
|authors=Michael Simon,Daniel Moldt,Henri Engelhardt,Sven Willrodt
|dblpUrl=https://dblp.org/rec/conf/apn/SimonMEW19
}}
==A First Prototype for the Visualization of the Reachability Graph of Reference Nets==
https://ceur-ws.org/Vol-2424/paper12.pdf
A First Prototype for the Visualization of the
Reachability Graph of Reference Nets
Michael Simon, Daniel Moldt, Henri Engelhardt, Sven Willrodt
University of Hamburg, Faculty of Mathematics, Informatics and Natural Sciences,
Department of Informatics, http://www.informatik.uni-hamburg.de/TGI/
Abstract Up to now, there was no reachability graph generation and
visualization for Reference nets. This contribution presents an executable
prototype. A major challenge is to cope with the dynamic net structure
of the Reference net formalism. Our presented solution uses the internal
functionality of Renew to visualize a marking in the reachability graph
as the graphical representation of the root net marking.
Keywords: High-level Petri Nets, Coloured Petri Nets, Reference Nets,
Tools, Renew, Reachability Graph
Introduction
The Reference Net Reachability Graph Plugin (Rnrgp) is a novel tool for the
analysis of the Reference net formalism in the Renew simulator1 .
Reference Nets Reference nets are a high-level Petri net formalism based on
the modeling approach of nets-within-nets. They allow the use of net instance
tokens, which are comparable to objects in object-oriented programming and
recognize Java expressions as inscriptions. Synchronous channels are used to
synchronize and communicate with net instance tokens. Due to these concepts,
normal reachability graph generation does not work for Reference nets.
Challenges for Reachability Graph Generation of Reference Nets The
main challenges for a reachability graph generation tool are the definitions of
a marking / state of the whole simulation and of the equality notion of these
markings. Net instances can dynamically create new net instances and all in-
stances can freely reference each other. The marking of the whole simulation is
thus a set of marked nets with arbitrary reference connections between them.
In the Reference net formalism, two net instance tokens are only equal if they
point to the exact same net instance. This equality definition is problematic
for the reachability graph generation: two successive executions of the same
transition binding creating a net instance token would lead to two different
markings. Instead, a comparison of the markings of the individual net instances
is desirable.
1
Renew: The Reference Net Workshop, http://www.Renew.de
Kummer, O.: Referenznetze. Logos Verlag, Berlin (2002)
166 PNSE’19 – Petri Nets and Software Engineering
The Reference Net Reachability Graph Plugin
The Reference Net Reachability Graph Plugin (Rnrgp) allows the generation of
a new kind of reachability graph for Reference nets and its visualization.
Visualization and Usability The reachability graph generation starts with
the initial marking of a root Reference net. Each node in the graph is a mark-
ing of this net, from which all of the net instance tokens are accessible. Any
possible transition binding execution, including from within net instance tokens,
will result in an outgoing edge. Edges are inscribed with the name of the fired
transition but a detailed description of the binding can also be accessed.
Specific bindings can be excluded from the exploration, e.g. to avoid the exe-
cution of transitions with action inscriptions that generally have side effects. Ad-
ditionally, a depth limit can be set. It defines a maximum distance from the initial
marking for the exploration. Overall, all markings can be investigated as visual
representations of the net instances and as a compressed text notation. This visu-
alization highly simplifies the comprehension of complex systems, since markings
are represented directly in the context of the modeled nets. Some examples of
different kinds of visualizations can be found at https://paose.informatik.
uni-hamburg.de/paose/wiki/ReferenceNetsReachabilityGraph.
Technical Details The implementation is isolated in a single Renew plugin
and the preexisting simulation core was not changed. Thus, its optimization
for the normal simulation remains untouched. However, this approach necessi-
tates workaround functionality. Net instance markings have to be copied and
reset often and central simulation algorithms to minimize the number of binding
searches cannot be used because they would require further adaptation.
Like the Reference net simulation, the graph generation starts with a single
root net instance. Two root net instance markings are equal, iff there exists a
bijective mapping between all net instances reachable from the root net instances
and the marking of each net instance in the mapping is equal to the marking of
the mapped instance after replacing each net instance token by the corresponding
mapped instance. The root net instances are mapped to each other and the
mapping of the other instances is sought by a depth-first search.
The reachability graph is generated by a breadth-first search. A marking is
explored by searching for the bindings of all transitions in all net instances. Each
found binding becomes an edge in the graph. All bindings that do not violate
the criteria given by the user are executed to find the target marking.
Conclusion and Outlook
While the efficiency of the Rnrgp is bad compared to normal Petri net tools, it
is the first tool that allows the generation of a reachability graph for Reference
nets. To solve the problem of the dynamic net structures a special visualization
has been chosen in the form of net instances. Based on the results reached so far,
the Rnrgp opens opportunities for formal analysis of Reference nets. Efficiency
will be possible by adapting the so far untouched Renew simulation core.