Changes between Version 2 and Version 3 of ReferenceNetsReachabilityGraph

Timestamp:

Apr 26, 2019, 7:17:32 PM (6 years ago)

Author:

5willrod

Comment:

--

ReferenceNetsReachabilityGraph

@@ -1 +1 @@
 **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. This can be further extended, so that any arrow instead is labeled with the full binding of the firing.
+
+=== Example
+
+[[Image(rw-net.pdf)]]
 [[Image(rw-rggraph.pdf)]]
+
+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
+
+[[Image(rw-net.pdf)]]
+[[Image(rw-rggraph-depthlimit.pdf)]]
+
+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 explored, 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
+
+=== Example 2
+