An approach to the automatic synthesis of controllers with mixed qualitative/quantitative specifications.