Changes between Version 11 and Version 12 of ReferenceNetsReachabilityGraph

Timestamp:

May 15, 2019, 5:47:51 PM (6 years ago)

Author:

5willrod

Comment:

--

ReferenceNetsReachabilityGraph

@@ -93 +93 @@
 ''Note: The ids of the net instances in the inspection differ from the ids in the reachability graph, because they were inspected in a later simulation.''
 ''Within a single execution of the plugin the ids do not differ.''
+
+== A More Complex Example
+
+The following example extends the producer consumer problem by an actual product subnet. 
+Instead of black tokens, the producer creates a clock net instance.
+This (simple) clock has four internal states.
+The transitions can fire concurrently to any other transition that is not in this net instance.
+The model is further simplified by assuming that the consumer instantly destroys the clock and therefore never has a persistent reference on it.
+
+=== The net System
+[[Image(prodconsclock-complete.pdf)]]
+
+=== The Reachability Graph
+As expected, the internal states of the clock lead to an significantly increasing amount of distinct markings.
+This is even with the limitation of only a single clock instance at a time and the consumer not storing the clocks.
+Still, the reachability graph becomes extremely harder to read for the human eye, even with proper formatting of the graph.
+
+However, the complexity of the actual system that is being modelled 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.
+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.
+
+
+[[Image(prodcons-clockRG.pdf)]]