This SDF model illustrates the use of 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. Also,we have a super-client (ImportantClient1) that needs to
be served quickly. Whenever a request is issued by client 1, the resource needs to
be granted either immediately or in the next cycle. The overall requirement can be
concretized by the following specification.
ALWAYS (req1 -> ( grant1 || NEXT grant1))
ALWAYS (req2 -> EVENTUALLY grant2)
ALWAYS (req3 -> EVENTUALLY grant3)
ALWAYS !(grant1 && grant2)
ALWAYS !(grant2 && grant3)
ALWAYS !(grant1 && grant3)
INPUT req1, req2, req3
OUTPUT grant1, grant2, grant3