1. A method for operating a computer system comprising: receiving in the system a description of a finite state machine including a temporal logic condition; and generating code for emulating the described finite state machine.