Changes between Version 23 and Version 24 of ReferenceNetsReachabilityGraph

Timestamp:

Jun 3, 2019, 3:45:07 PM (6 years ago)

Author:

9simon

Comment:

state -> marking where appropriate

ReferenceNetsReachabilityGraph

@@ -38 +38 @@
 == Introducing an unbounded place
 
-For every distinct state of the root net there is a state in the reachability graph. 
+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.
@@ -59 +59 @@
 
 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.
+They can be expanded, which will open a copy of the root net instance in this particular marking.
 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.
 
@@ -74 +74 @@
 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 internal marking changes of the producer/consumer have the net instance ID as prefix.
 
 [[Image(prod-cons-rg-2.png, 95%)]]
@@ -111 +111 @@
 
 However, the complexity of the actual system that is being modeled 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.
+A proposed solution to this discrepancy is the feature to abstract certain nets or parts of their markings.
 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.