enduser/Discrete-Event-Controller-Synthesis.md

@@ -25,29 +25,35 @@ A concrete example
 
 
 ```
-Plant = (a -> b -> Plant | c -> d -> Plant | e -> AUX), 
+Plant = (a -> b -> d -> 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}>
+fluent FG = <g, {a, b, c, d, e, f}>
 assert E = FE
 assert D = FD
+assert G = FG
 
-controllerSpec G = {
+controllerSpec Spec = {
 	safety = {NoB}
-	assumption = {E, D}
+	assumption = {G}
 	liveness = {E, D}
 	controllable = {a, c, e}
 }
 
-controller ||C = (Plant)~{G}.
+controller ||C = (Plant)~{Spec}.
 ```
 
-To check if the assumptions are compatible use:
+
+# Compatibility
+To check if the assumptions in a controller specification are compatible (i.e., the environment can achieve the assumptions for any controller), which is diserable (see Nicolás Roque D'Ippolito, Victor Braberman, Nir Piterman, and Sebastián Uchitel. 2010. Synthesis of live behaviour models. In Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering (FSE '10). Association for Computing Machinery, New York, NY, USA, 77–86. [pdf](https://doi.org/10.1145/1882291.1882305)
 
 ```
-check compatibility ||CONTROLLERNAME = (PLANTNAME)~{CONTROLLERSPECNAME}.
+checkCompatibility ||Compatible = (Plant)~{Spec}.
 ```