enduser/Discrete-Event-Controller-Synthesis.md

@@ -8,7 +8,7 @@ controller ||CONTROLLER = (PLANT)~{SPECIFICATIONS}.
 The specification includes various items, some are optional:
 
 * Safety properties. These are process names that describe bad behaviour with error states. They may have been constructed using the property or ltl_property keyword)
-* Assumptions. These are names of assertions that must be boolean formulae (i.e., no temporal operators). An assertion A is interpreted by the synthesis procedure as []<>A.
+* Assumptions. These are names of assertions that must be boolean formulae (i.e., no temporal operators) expressed in terms of fluents. An assertion A is interpreted by the synthesis procedure as []<>A.
 * Liveness. As with assumptions, they are boolean formulae and are interpreted as being g preceded by []<>.
 * Controllable alphabet. This is the set of events that are controllable by the controller to be synthesised.  
 
@@ -21,8 +21,29 @@ controllerSpec NAME = {
 }
 ```
 
+A concrete example 
 
 
+```
+Plant = (a -> b -> Plant | c -> d -> Plant | e -> AUX), 
+AUX = (f -> AUX | g -> Plant).
+
+ltl_property NoB = []!b
+fluent FE = <e, {a, b, c, d, f, g}>
+fluent FD = <d, {a, b, c, e, f, g}>
+assert E = FE
+assert D = FD
+
+controllerSpec G = {
+	safety = {NoB}
+	assumption = {E, D}
+	liveness = {E, D}
+	controllable = {a, c, e}
+}
+
+controller ||C = (Plant)~{G}.
+```
+
 To check if the assumptions are compatible use:
 
 ```