enduser/Discrete-Event-Controller-Synthesis.md

@@ -24,8 +24,8 @@ controllerSpec NAME = {
 A concrete example:
 
 ```
-Plant = (a -> b -> d -> Plant | c -> d -> Plant | e -> AUX), 
-AUX = (f -> AUX | g -> Plant).
+System = (a -> b -> d -> System | c -> d -> System | e -> AUX), 
+AUX = (f -> AUX | g -> System).
 
 ltl_property NoB = []!b
 fluent FE = <e, {a, b, c, d, f, g}>
@@ -42,7 +42,8 @@ controllerSpec Spec = {
 	controllable = {a, c, e}
 }
 
-controller ||C = (Plant)~{Spec}.
+controller ||C = (System)~{Spec}.
+||ControlledSystem = (System || C).
 ```
 
 
@@ -53,6 +54,14 @@ For GR1 specifications, to check if the assumptions are compatible (i.e., the en
 checkCompatibility ||Compatible = (Plant)~{Spec}.
 ```
 
+## `plant` keyword
+This keyword may be useful for debugging a non-realizable specification (i.e., one that does not have a controller). It returns an LTS that is the composition of the system to be controlled with the safety properties that must be guaranteed. Following example above:
+
+```
+plant ||Plant = (System)~{Spec}.
+```
+
+
 # Non-Blocking 
 
 MTSA supports synthesis of controllers that achieve non-blocking control for safety properties. See Daniel Ciolek, Matias Duran, Florencia Zanollo, Nicolas Pazos, Julián Braier, Victor Braberman, Nicolas D'Ippolito, Sebastian Uchitel,
@@ -124,21 +133,10 @@ 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