component Clock is {
      state {
         time : Integer; 
         speed : Integer; 
      }
      invariant {
         speed \eqgreater 0;
      }
      interface {
         prov ip1: Tick();
         prov ip2: setClockSpeed(rate : Integer);
      }
      operations {
         prov op1: {
            post ~time = time + 1;
         }
         prov op2: {
            let  r : Integer;
            post ~speed = r;
         }
      }
      map {
         ip1 -> op1 ();
         ip2 -> op2 (rate -> r);
      }
   }