enduser/Discrete-Event-Controller-Synthesis.md

@@ -61,6 +61,7 @@ This keyword may be useful for debugging a non-realizable specification (i.e., o
 plant ||Plant = (System)~{Spec}.
 ```
 
+
 ## `permissive` keyword
 
 This feature has known bugs. Do not use for now.
@@ -85,6 +86,31 @@ controllerSpec Spec = {
 controller ||C = (System)~{Spec}.
 ```
 
+# Reachability
+The `reachability` keyword is used within `controllerSpec`.
+When used instead of a GR(1) control problem a reachability one is solved. In other words, the liveness goal must be reached only once. 
+
+
+```
+set ContAlphabet = {c1, c2, c3}
+
+System = (c1 -> System | c2 -> u1 -> AUX | c3 -> u2 -> System), 
+AUX = (c2 -> AUX).
+
+fluent Fu1 = <u1, c1>
+assert Au1 = Fu1
+
+controllerSpec Spec = {
+	liveness = {Au1}
+	controllable = ContAlphabet
+	reachability
+
+}
+
+controller ||C = (System)~{Spec}.
+minimal ||ControlledSystem = (System || C).
+checkCompatibility ||Compatible =  (System)~{Spec}.
+```
 
 
 # Non-Blocking