Animation of a controller is broken
In the following example, if Control is built (i.e., “compose”) and an animation is started, the animation offers “a” and “b” when Control only offers “a”.
Instead, if System is built and the animation is started the animation behaves correctly, offering only “a”.
I’d say there is some problem with the status of compositeState when the controller is returned. Perhaps the composition is not built.
P = (a -> P1 | b -> P1),
P1 = (c -> P | d -> P).
||Env = (P).
assert Assumption = (a)
assert Guarantee = (d)
controllerSpec Goal = {
assumption = {Assumption}
liveness = {Guarantee}
controllable = {a, b}
}
controller ||Control = (Env)~{Goal}.
||System = (Control || Env).