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

enduser/Discrete-Event-Controller-Synthesis.md

@@ -116,5 +116,15 @@ controllerSpec Goal = {
 heuristic ||DirectedController = Plant~{Goal}.
 ```
 
+# Unsupported
+
+## Fluent Activity / Concurrency
+These are soft-goal clauses used inside a `controllerSpec` / controller goal block,
+telling the heuristic controller synthesiser what to optimise. This functionality is
+experimental and may not be fully functional.
+
+* `concurrencyFluents={...}` — names fluents whose *simultaneous* truth the synthesiser tries to maximise; a non-empty set routes synthesis to a dedicated concurrency-control problem.
+* `activityFluents={...}` — names "activity" fluents the synthesiser tries to keep active; drives the "best controller" heuristic.
+
 ---
 [← End User](End-User)