enduser/Discrete-Event-Controller-Synthesis.md

@@ -53,7 +53,7 @@ For GR1 specifications, to check if the assumptions are compatible (i.e., the en
 checkCompatibility ||Compatible = (Plant)~{Spec}.
 ```
 
-# Non Blocking 
+# Non-Blocking 
 
 MTSA supports synthesis of controllers that achieve non-blocking control for safety properties. See Daniel Ciolek, Matias Duran, Florencia Zanollo, Nicolas Pazos, Julián Braier, Victor Braberman, Nicolas D'Ippolito, Sebastian Uchitel,
 On-the-fly informed search of non-blocking directed controllers, Automatica,
@@ -61,13 +61,7 @@ Volume 147, 2023, 110731, ISSN 0005-1098. [pdf](https://doi.org/10.1016/j.automa
 
 To do non-blocking synthesis the controller specification must include the keyword `nonblocking`.
 
-```
-controllerSpec ANonBlockingSpecification = {
-    controllable = {c45}
-    marking = {c45, u55}
-    nonblocking
-}
-```
+In addition, MTSA only supports non-blocking directors (i.e., non maximal) built using directed controller synthesis (DCS) which means that the keyword `heuristic` must be used. 
 
 The states that the controller is expected to never block the plant from having the possibility of reaching can be marked in two ways:
 
@@ -98,13 +92,14 @@ heuristic ||DirectedController = Plant~{Goal}.
 
 ```
 Example = A0,
-A0 = (a -> A1),
-A1 = (c_1 -> Up | u_1 -> Down),
-Up = (u_2 -> Up),
-Down = (u_3 -> Down).
+A0 = (u1 -> A1),
+A1 = (c1 -> Up | c2 -> Down | c3-> Up2),
+Up = (up -> Up),
+Down = (down -> Down), 
+Up2 = (down->up-> Up2).
 
-fluent GoingUp = <u_2, a>
-fluent GoingDown = <u_3, a>
+fluent GoingUp = <up, u1>
+fluent GoingDown = <down, u1>
 
 assert NeverGonnaGiveYouUp = (!GoingUp && GoingDown)
 
@@ -112,10 +107,11 @@ assert NeverGonnaGiveYouUp = (!GoingUp && GoingDown)
 
 controllerSpec Goal = {
     liveness = {NeverGonnaGiveYouUp}
-    controllable = {c_1}
+    controllable = {c1, c2, c3}
 }
 
 heuristic ||DirectedController = Plant~{Goal}.
+||ControlledPlant = (DirectedController || Plant).
 ```
 
 # Unsupported