enduser/Discrete-Event-Controller-Synthesis.md

@@ -92,7 +92,7 @@ controllerSpec Goal = {
 heuristic ||DirectedController = Plant~{Goal}.
 ```
 
-* Keyword `liveness` followed by a set of assertions can be used to define marked states. Although the syntax is as in GR(1), the interpretation differs. Each liveness goal does not need to occur infinitely often; it must be possible to occur infinitely often instead.
+* Keyword `liveness` followed by a set of assertions can be used to define marked states. Although the syntax is as in GR(1), the interpretation differs. Instead of requiring that every infinite trace of the composite plant, sees the liveness goals infinitely often, it requires that every finite trace can be extended (not necessarily controllably) in the controlled plant to see the liveness goals infinitely often.
 
 ```
 Example = A0,