enduser/Discrete-Event-Controller-Synthesis.md

@@ -62,6 +62,9 @@ plant ||Plant = (System)~{Spec}.
 ```
 
 ## `permissive` keyword
+
+This feature has known bugs. Do not use for now.
+
 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
@@ -82,7 +85,6 @@ controllerSpec Spec = {
 controller ||C = (System)~{Spec}.
 ```
 
-(This feature is lightly maintained.)
 
 
 # Non-Blocking