enduser/reactiveSynthesis.md

+# under construction
+
+MTSA implements discrete event controller synthesis for GR1 formulae. 
+
+To use this functionality first declare a controller goal using 
+
+controllerSpec NAME = {
+       safety = { COMMA SEPARATED PROCESS NAMES (WITH ERROR STATES) }
+       assumption = { COMMA SEPARATED ASSERTION NAMES} 
+       liveness = { COMMA SEPARATED ASSERTION NAMES}  
+       controllable = { NAME OF SET OF LABELS}
+}
+
+Then build the controller from a plant
+
+controller ||CONTROLLERNAME = (PLANTNAME)~{CONTROLLERSPECNAME}.
+
+To check if the assumptions are compatible use 
+
+check compatibility ||CONTROLLERNAME = (PLANTNAME)~{CONTROLLERSPECNAME}.
\ No newline at end of file