Changes between Version 29 and Version 30 of ReferenceNetsReachabilityGraph

Timestamp:

Jun 3, 2019, 5:35:38 PM (6 years ago)

Author:

5willrod

Comment:

--

ReferenceNetsReachabilityGraph

@@ -39 +39 @@
 
 For every distinct state of the root net there is a node 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.
+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.