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.

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.

Example 1

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.

Example 2