This SDF model illustrates the use of numerical synthesis for fast prototyping. In this model, we hope to create an FSMActor as a
controller that can, based on the requirement of clients, grant the resource. However, it is forbidden that the controller grants
two clients simultaneously. The overall requirement can be concretized by the following specification. Also, whether Client1 wants
the resource is based on comparing values produced from two sensors.
ALWAYS (X+Y>3 -> NEXT (grant1))
ALWAYS (X^2+Y^2<4 -> NEXT (grant2))
ALWAYS (!(grant1 && grant2))
INPUT req1, req2
OUTPUT grant1, grant2
In this example, when we take X+Y>3 and X^2+Y^2<4 as two independent boolean input variables req1 and req2, we are unable to find a
controller, as it is possible to have (req1, req2) = (true, true).
However, we can check the invalidty of this counter strategy using JBernstein (http://www6.in.tum.de/~chengch/efsmt/jbernstein.html)
\forall x, y \in [0, 4]: !(X+Y>3 && X^2+Y^2<4), which is equivalent to
\forall x, y \in [0, 4]: X+Y>3 -> X^2+Y^2>=4, a format that can be checked by JBernstein
JBernstein returns true.
Therefore, this counter strategy is impossible to be realized. We can add the following to the specification, based on the proporgated
result from the theory: "ASSUME (ALWAYS !(req1 && req2))". When we rerun the synthesis engine, we can have a controller.