ReferenceNetsReachabilityGraph

The Graph Creation Dialogue

Several options can be selected in the GUI. The "Skip Action Execution" checkbox will skip all bindings where a transition labeled with an action inscription would be fired. This prevents the firing of transitions that have side effects.

The "Skip Net Instance Creation" checkbox prevents the firing of transitions which would create net instances.

In the drop down menu "Node Inscriptions" the labels for the nodes in the reachability graph can be selected. For larger net systems it is recommended to choose "nothing" to remain some amount of clarity.

Additionally, a depth limit for the search can be set. This is further described in the section Depth limited search

"Start" initiates the creation process. The root net is the currently selected net in Renew.

With the "Cancel"-button, the process can be terminated prematurely.

Examples for the Reference Net Reachability Graph Plugin

Nets without subnets

The following example shows a simple reference net without any subnets. The reachability graph is generated as expected, with the red node representing the initial marking and any other node representing a reachable marking of the net. The edges are labeled with the respective transition that fired. The inscription can be extended to show the full binding of the firing.

Example

A reference net modeling the reader writer problem with two people and the generated reachability graph. Black tokens are noted as [] .

Depth limited search

If desired, the Reference Net Reachability Graph Plugin can generate the reachability graph only up to a specified depth. The following example shows the same net of the prior example, generated with a depth limit of 1. Here, all markings that can be reached by firing one transition are fully explored. All further bindings that the simulation finds are listed, but not explored. These special unexplored markings are represented by a triangular node. Note that it is possible that an unexplored marking could be identical to one of the already explored markings in the graph. As the markings are not explored however, they are not summarized to one marking.

Example

The same net as before, this time with a depth limit. Possible, but not explored bindings are represented with a triangular node. Bindings of unexecuted bindings are still listed, as can be seen on the lower left edge inscription.

Introducing an unbounded place

For every distinct state of the root net there is a node in the reachability graph. Consequently, if any net contains an unbounded place, the reachability graph is infinitely large. While common algorithms that create reachability graphs terminate in this case, a greater-equals relation for markings is not yet implemented in the ReferenceNetsReachabilityGraph Plugin. To illustrate, the previous example has been modified to include a place, which counts how many times the resource in the reader/writer problem has been accessed.

Example

As a result of the newly introduced place, a chain of nodes emerge in the reachability graph, wherein each cycle in the root net results in an additional token in the reachability graph. So although only one place in the net accumulates tokens and the possible transition sequences are irrelevant to the number of tokens in that place, the resulting reachability graph gets infinitely more nodes. It is still possible to visualize a portion of it by setting a depth limit for exploration. However, a better approach to visualize these kinds of state spaces would be the coverability graph, which may come in a later update.

Nets with subnets

The previous example displayed the reachability graph only for a single net without reference to other nets. For the inspection of more complicated and nested nets, we turn off the node inscriptions of the reachability graph and instead explore it interactively.

A graph node represents the root net instance in a certain marking. It can be double-clicked, which will open a copy of the root net instance in this particular marking. This root net instance may itself contain other net instances as tokens (each in a particular marking). In fact, the (marked) net instances in a single graph node can freely contain each other as long as they are reachable from the root net instance. They can be interactively explored in the UI starting from the root net instance by double-clicking net instance tokens.

For any firing that happens within a net instance other than the root net instance, the edge is labeled with the identifier of the net instance proceeding the transition identifier.

The Producer Consumer Problem

The first example is the classic producer consumer problem (with a storage capacity), where producer and consumer are distributed into an own net each. Their net instances are created in the system net, which also holds the storage place for the producer and consumer. The synchronisation happens via synchronous channels.

The ReferenceNetsReachabilityGraph Plugin is started with the system net as the root net. As the synchronous calls are initiated from the system net, they are listed without a prefix. The internal marking changes of the producer/consumer have the net instance ID as prefix.

The edge inscription with the yellow background has been extended to display the complete binding. The transition is a firing of the root net transition "consume", which is a synchronous channel. Therefore, also the corresponding transition in the consumer net instance is listed.

As mentioned before, node inscriptions would be more confusing than helpful. The plugin intends the interactive inspection of the graph. The following images show the inspection of the bottom right marking. The producer is back in his idle state whereas the the consumer is still in his waiting state and the storage is filled.

Note: The IDs of the net instances in the inspection differ from the IDs in the reachability graph, because they were inspected in a later simulation. Within a single execution of the plugin the IDs do not differ.

More Nested Examples

The Net System

The Reachability Graph

Exploration Of A Node In The Reachability Graph

Nested Example 2

The following example extends the producer consumer problem by an actual product subnet. Instead of black tokens, the producer creates a clock net instance. This (simple) clock has four internal states. The transitions can fire concurrently to any other transition that is not in this net instance. The model is further simplified by assuming that the consumer instantly destroys the clock and therefore never has a persistent reference on it.

The net System

The Reachability Graph

As expected, the internal state of the clock leads to a significantly increased amount of distinct markings. This is even the case with only a single clock instance at a time that is not stored by the consumer. Still, the reachability graph becomes extremely hard to read for the human eye, even with proper formatting of the graph.

However, the complexity of the actual system that is being modeled did not really increase and is, in fact, still easy to describe in words. A proposed solution to this discrepancy is the feature to abstract certain nets or parts of their markings. The result is a folded reachability graph, where nodes that only differ in a marking of places that are flagged as "ignore" are folded into a single node. It is important to maintain the flexibility to flag only certain subnets, since in many cases, some subnets' behavior should be fully represented in the reachability graph, while others' should not.