ReferenceNetsReachabilityGraph

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 arrows 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 persons 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 arrow inscription.

Introducing an unbounded place

For every distinct state of the root net there is a state in the reachability graph. While common algorithms that create reachability graphs terminate in this case, the ReferenceNetsReachabilityGraph Plugin does not contain a comparison of markings yet. Consequently, if any net contains an unbounded place, an infinite amount of nodes are created in the reachability graph. 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 visualise a portion of it by setting a depth limit for exploration. However, a better approach to visualise 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.

Any node represents the root net instance with a certain marking. They can be expanded, which will open a copy of the root net instance in this particular state. This net instance behaves like a simulation step which can be fully inspected, meaning that all nets that this net has a reference of can be explored with their current marking, including, again, nets referenced in this net.

For any firing that happens within a subnet, the arrow is labeled with the identifier of the subnet proceeding the transition identifier, whereas transitions in the root net are only labeled with their 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 state changes of the producer/consumer have the net instance id as prefix.

The arrow 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.

A More Complex Example

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 states of the clock lead to an significantly increasing amount of distinct markings. This is even with the limitation of only a single clock instance at a time and the consumer not storing the clocks. Still, the reachability graph becomes extremely harder to read for the human eye, even with proper formatting of the graph.

However, the complexity of the actual system that is being modelled 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 states. 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 place. It is important to remain the flexibility to flag only certain subnets, since in many cases, some subnets should appear fully in the reachability graph, while some should not.