#define OFF (-1)
#define TOVAL (0)

/*discrete time macros*/

/* timer data type */
typedef timer 
{
short val=OFF;
}

/* basic timing statements */

#define set(tmr,value) tmr.val=value   
#define expire(tmr) (tmr.val==TOVAL) /*timeout*/
#define reset(tmr) tmr.val=OFF
/* derived timing statements */

#define delay(tmr,value) set(tmr,value); expire(tmr)   /* delay of val ticks */
#define udelay(tmr) do :: delay(tmr,1); ::break; od /* unbounded delay */

/* nondeterministic bounded delay */
#define bdelay(tmr,val,auxtmr) \
           set(tmr,val);\
           do \
           :: expire(tmr) -> break \
           :: else -> if :: break; :: delay(auxtmr,1); fi\
           od
	   
active proctype __Timers()
{
 end__Timers:    do :: timeout od;
}