module General =

process shift_event =
   ( ? event t;
       event Tick;
     ! event shifted_t;
   )
   (| t_instant := t default not Tick
    | zt_instant := t_instant $ init false
    | shifted_t := when zt_instant
    |)
   where
     boolean t_instant, zt_instant;
   end;


process topmod =
   { integer m; }
   ( ? event start;
     ! integer v;
       event reset;
   )
   (| v := (0 when start) default (0 when reset) default (zv + 1)
    | reset := when (zv >= (m - 1))
    | zv := v $ init m
    |)
   where
     integer zv;
   end;

end;