enduser/fltl.md

+# Fluents and LTL properties
+
+With the `fluent` keyword we can define a set of transitions that if taken will make the fluent be `True` (if the transition was in the left set) or `False` (for transitions in the second set) as shown below.
+
+`assert` can be conjunction and disjunction of `fluents` with the `&&` and `||` operators respectively.
+
+`ltl_property` can have temporal operators as well, `[]` indicates that the following must always hold, and `<>` eventually. 
+
+The `liveness` keyword in controllerSpec takes `one` assertion `L` and will make it so the built controller ensures `[]<>L`. 
+The `assumption` keyword can be used in the same way as `liveness`, and the controller will guarantee that `[]<>A -> []<>L`
+
+Example of a controllable case, using [DCS](https://bitbucket.org/lnahabedian/mtsa/wiki/enduser/DCS) as algorithm:
+```
+Example = A0,
+A0 = (a -> A1),
+A1 = (c_1 -> Up | u_1 -> Down),
+Up = (u_2 -> Up),
+Down = (u_3 -> Down).
+
+fluent UpF = <u_2, {a, u_3}>
+fluent DownF = <u_3, {a, u_2}>
+
+assert idealDirection = DownF
+
+||Plant = Example.
+
+controllerSpec Goal = {
+liveness = {idealDirection}
+controllable = {c_1}
+}
+
+heuristic ||DirectedController = Plant~{Goal}.
+```