Following is an example for synthesis of reach-avoid controller for a unicycle in a 2D state space. For details of the model and the problem, please see the paper[1].
[1] SCOTS: A Tool for the Synthesis of Symbolic Controllers