autoCode4
Synthesizing embedded control software from formal specifications
...Such feature is mandated in developing safety-critical systems and are considered essential for specification validation or integrating manual implementation such as legacy code.
The LTL specification captures the desired behavior of a controller where the environment takes the first move (i.e., sense/input then react/output), so the synthesized controller can be viewed as a Mealy machine.
A step-by-step tutorial is available within the software package.