enduser/Discrete-Event-Controller-Synthesis.md

@@ -75,21 +75,23 @@ The states that the controller is expected to never block the plant from having
 
 ```
 Example = A1,
-A1 = (u12 -> A2 |
-u14 ->A4),
-A2 = (u21 -> A1),
-A4 = (c45 ->A5),
-A5 = (u55 -> A5).
+A1 = (u1 -> A2 | u3 ->A4),
+A2 = (u2 -> A1),
+A4 = (c ->A5),
+A5 = (u4 -> A5 | c -> A6),
+A6 = (u2 -> A6).
 
 ||Plant = Example.
 
 controllerSpec Goal = {
-    controllable = {c45}
-    marking = {c45, u55}
+    controllable = {c}
+    marking = {u4}
     nonblocking
 }
 
 heuristic ||DirectedController = Plant~{Goal}.
+
+||ControlledPlant = (DirectedController || Plant).
 ```
 
 * Keyword `liveness` followed by a set of assertions can be used to define marked states. Although the syntax is as in GR(1), the interpretation differs. Instead of requiring that every infinite trace of the composite plant, sees the liveness goals infinitely often, it requires that every finite trace can be extended (not necessarily controllably) in the controlled plant to see the liveness goals infinitely often.