Changes between Version 10 and Version 11 of ReferenceNetsReachabilityGraph

Timestamp:

May 15, 2019, 2:38:50 PM (6 years ago)

Author:

5willrod

Comment:

--

ReferenceNetsReachabilityGraph

@@ -34 +34 @@
 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
+
+[[Image(rw-counter-net.pdf)]]
+[[Image(rw-counter-rggraph.pdf)]]
+
+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