Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

enduser/Discrete-Event-Controller-Synthesis.md

@@ -61,6 +61,29 @@ This keyword may be useful for debugging a non-realizable specification (i.e., o
 plant ||Plant = (System)~{Spec}.
 ```
 
+## `permissive` keyword
+By default GR1 synthesis commits to a single strategy, keeping only the controllable
+moves that make progress towards the goal. Adding `permissive` to the `controllerSpec`
+instead produces the *maximally permissive* controller: it keeps **every** controllable
+move that still guarantees the goal, not just the progress-making ones. The result is
+the largest sub-behaviour of the plant that satisfies the specification — useful when
+you want to preserve all valid behaviours for later refinement or analysis — at the
+cost of a larger, non-deterministic controller.
+
+```
+controllerSpec Spec = {
+	safety = {NoB}
+	assumption = {G}
+	liveness = {E, D}
+	controllable = {a, c, e}
+	permissive
+}
+
+controller ||C = (System)~{Spec}.
+```
+
+(This feature is lightly maintained.)
+
 
 # Non-Blocking 
 
@@ -135,7 +158,6 @@ experimental and may not be fully functional.
 
 ## To be checked
 
-* `permissive` — permissive controller mode
 * `controlled_det` — controlled determinism
 * `lazyness` — controller laziness parameter
 * `non_transient` — non-transient constraint