Automatic synthesis of supervisory control systems