enduser/Discrete-Event-Controller-Synthesis.md

-MTSA supports a synthesising behaviour models that control a given plant to satisfy a given property. 
+MTSA supports a 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. 
+
+
+```
+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.
+* 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.  
+
+```
+controllerSpec NAME = {
+    safety = { COMMA SEPARATED PROCESS NAMES }
+    assumption = { COMMA SEPARATED ASSERTION NAMES }
+    liveness = { COMMA SEPARATED ASSERTION NAMES }
+    controllable = { NAME OF SET OF LABELS }
+}
+```
+
+
+
+To check if the assumptions are compatible use:
+
+```
+check compatibility ||CONTROLLERNAME = (PLANTNAME)~{CONTROLLERSPECNAME}.
+```
+
 
 * [Supervisory Control](enduser/supervisoryControl)
 * [Reactive Synthesis](enduser/reactiveSynthesis)