Finite response checker should support state invariants.
State invariants should be taken into account when determining whether a controllable loop exists.
For the following specification it should be concluded that there is finite response.
plant A:
controllable c;
input int[0..10] I;
location p:
initial;
edge c when I = 3;
end
plant A.I != 3;