#The timer leaves state START non-deterministically.  This constraint 
#prevents it from staying in START forever, without leaving.
!(timer.state=START);

#The timer leaves state SHORT non-deterministically.  This constraint 
#prevents it from staying in SHORT forever, without leaving.
!(timer.state=SHORT);