enduser/Discrete-Event-Controller-Synthesis.md

-MTSA supports synthesising behaviour models that control a given plant to satisfy a given property. The plant is defined using an FSP composite process, which may be explicitly marked with the `plant` keyword (e.g. `plant ||NAME = (...).`) to designate it as the uncontrolled environment for synthesis. The property is defined using the `controllerSpec` keyword.
+MTSA supports synthesising behaviour models that control a given plant to satisfy a given property. The plant is defined using an FSP composite process, The property is defined using the `controllerSpec` keyword.
 
 
 # GR1
@@ -117,7 +117,7 @@ heuristic ||DirectedController = Plant~{Goal}.
 ```
 
 # Unsupported
-
+The following are unsupported or not yet documented properly
 ## 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
@@ -126,5 +126,72 @@ 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.
 
+## Controller Synthesis (GR1)
+
+* `controller` (alias: `gr`) — GR1 controller synthesis
+* `controllerSpec` — declares a controller goal specification
+* `safety` — safety processes within a `controllerSpec`
+* `assumption` — liveness assumptions within a `controllerSpec`
+* `liveness` — liveness guarantees within a `controllerSpec`
+* `controllable` — set of controllable actions
+* `checkCompatibility` — checks whether GR1 assumptions are compatible
+
+## To be checked
+
+* `permissive` — permissive controller mode
+* `controlled_det` — controlled determinism
+* `nonblocking` — non-blocking requirement
+* `lazyness` — controller laziness parameter
+* `non_transient` — non-transient constraint
+* `reachability` — reachability analysis
+
+## DCS / Non-blocking
+
+* `heuristic` — triggers Directed Controller Synthesis
+* `marking` — marks states for non-blocking synthesis
+* `disturbances` — disturbance specification
+* `partialOrderReduction` — enables partial order reduction
+* `compositional` — compositional synthesis approach
+* `monolithicDirector` — monolithic director synthesis
+
+## RTC Controllers
+
+* `rtc` — Reactive Test Case controller
+* `rtcAnalysis` — RTC analysis controller
+* `failure` — fault/failure specification
+* `test_latency` — test latency specification
+* `exceptionHandling` — exception handling
+
+
+## Updating Controller
+
+* `updatingController` — updating controller problem
+* `oldController` — reference to the old controller
+* `oldGoal` — old goal specification
+* `newGoal` — new goal specification
+* `mapping` — state mapping
+* `transition` — transition specification
+* `graphUpdate` — graph update specification
+* `initialState` — initial state in the update graph
+* `transitions` — transitions in the update graph
+
+
+
+## Control Stack
+
+* `controlstack` — control stack specification
+* `tier` — control tier definition
+
+
+
+## Exploration
+
+* `exploration` — exploration specification
+* `environment` — exploration environment
+* `model` — exploration model
+* `goal` — exploration goal
+* `environment_actions` — environment action set
+
+
 ---
 [← End User](End-User)
\ No newline at end of file