Composition of keywords
I want to be able to do minimal controller
minimal controller ||C = (Plant)~{G}.
instead of:
Plant = (a -> b -> 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}> assert E = FE assert D = FD
controllerSpec G = { safety = {NoB} assumption = {E, D} liveness = {E, D} controllable = {a, c, e} }
controller ||C = (Plant)~{G}. minimal ||MC = C.