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 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}.