Automatic Synthesis of Controllers from Formal Specification