component Vehicle is subtype TimedCargoRouteEntity (int \and beh) {
      state {
         cargo          : \set Shipment;
         cargo_val      : \set String;
         name           : String;
         max_capacity   : Integer;
         capacity       : Integer; 
         internal_clock : Integer;
         max_speed      : Integer;
         speed          : Integer;
         active         : Boolean;
         distance       : Integer;
      }
      invariant {
         (capacity \eqgreater 0) \and (capacity \eqless max_capacity) \and
         (speed \eqgreater 0) \and (speed \eqless max_speed) \and
         (distance \eqgreater 0);
      }
      interface {
         prov ip_setspd: SetSpeed(s : Integer);
         prov ip_getspd: GetSpeed() : Integer;
         prov ip_setmaxspd: SetMaxSpeed(s : Integer);
         prov ip_getmaxspd: GetMaxSpeed() : Integer;
         prov ip_setcap: SetCapacity(c : Integer);
         prov ip_getcap: GetCapacity() : Integer;
         prov ip_plcshp: PlaceShipment(name : String; shp : Shipment);
         prov ip_getshp: GetShipment(name : String; loc : Integer) : Shipment;
         prov ip_remshp: RemoveShipment(name : String; loc : Integer);
         prov ip_setnam: SetName(new_name : String);
         prov ip_getnam: GetName() : String;
         prov ip_setmaxcap: SetMaxCapacity(c : Integer);
         prov ip_getmaxcap: GetMaxCapacity() : Integer;
         prov ip_timinc: TimeIncrement(); 
         prov ip_getcrg: GetContentInfo() : \set String; 
         prov ip_setact: Activate(name : String; start : String;
                                  end : String);
         prov ip_deact: Deactivate(name : String);
         prov ip_getact: IsActive(name : String) : Boolean;
         req  ir_clktck: clockTick(); 
         req  ir_calcdist: CalcDistance(start : String; end : String) : Integer;

      }
      operations {
         prov op_setact: {
            let  n : String;
                 start : String;
                 end : String;
            pre  n = name;
            post (~active <> active);
         }
         prov op_deact: {
            let  n : String;
            pre  n = name;
            post (~name = name) \and (~active <> active);
         }
         prov op_getact: {
            let  n : String;
            pre  n = name;
            post (\result = active) \and (~name = name) \and 
                 (~distance = distance);
         }
         prov op_setspd: {
            let  num : Integer;
            post ~speed = num;
         }
         prov op_getspd: {
            post \result = speed;
         }
         prov op_setcap: {
            let  num : Integer;
            post ~capacity = num;
         }
         prov op_getcap: {
            post \result = capacity;
         }
         prov op_plcshp: {
            let  shp : Shipment;
                 shp_size : Integer;
                 n : String;
            pre  name = n;
            post (shp \in ~cargo) \and
                 (~capacity = capacity + shp_size) \and
                 (~name = name);
         }
         prov op_getshp: {
            let  shp_loc : Integer;
                 n : String;
                 shp_by_loc : Shipment; // a function placeholder
            pre  name = n;
            post (\result = shp_by_loc) \and (~name = name);
         }
         prov op_remshp: {
            let  shp_loc : Integer;
                 shp_size : Integer;
                 n : String;
                 shp_by_loc : Shipment; // a function placeholder
            pre  (name = n) \and (shp_by_loc \in cargo);
            post (shp_by_loc \not_in ~cargo) \and
                 (~capacity = capacity - shp_size) \and
                 (~name = name);
         }
         prov op_setnam: {
            let  n : String;
            post ~name = n;
         }
         prov op_getnam: {
            post \result = name;
         }
         prov op_setmaxspd: {
            let  num : Integer;
            post ~max_speed = num;
         }
         prov op_getmaxspd: {
            post \result = max_speed;
         }
         prov op_setmaxcap: {
            let  num : Integer;
            post ~max_capacity = num;
         }
         prov op_getmaxcap: {
            post \result = max_capacity;
         }
         prov op_timinc: {
            post (~internal_clock = internal_clock + 1) \and
                 (~distance = distance - speed); // for 1 second 
         }
         prov op_getcrg: {
            post \result = cargo_val;
         }
         req or_calcdist: {
            let  start : String;
                 end : String;
                 vertices : STATE_VARIABLE;
                 vert_dist : Integer;
            pre  (start \in vertices) \and (end \in vertices);
            post (\result = vert_dist) \and
                 (~start \in vertices) \and
                 (~end \in vertices);
         }
         req or_clktck: {
            let  time : STATE_VARIABLE;
            post ~time = time + 1;
         }
      }
      map {
         ip_setact -> op_setact (name -> n, start -> start, end -> end);
         ip_deact -> op_deact (name -> n);
         ip_getact -> op_getact (name -> n);
         ip_setspd -> op_setspd (s -> num);
         ip_getspd -> op_getspd ();
         ip_setcap -> op_setcap (c -> num);
         ip_getcap -> op_getcap ();
         ip_plcshp -> op_plcshp (name -> n, shp -> shp);
         ip_getshp -> op_getshp (name -> n, loc -> shp_loc);
         ip_remshp -> op_remshp (name -> n, loc -> shp_loc);
         ip_setnam -> op_setnam (new_name -> n);
         ip_getnam -> op_getnam ();
         ip_setmaxspd -> op_setmaxspd (s -> num);
         ip_getmaxspd -> op_getmaxspd ();
         ip_setmaxcap -> op_setmaxcap (c -> num);
         ip_getmaxcap -> op_getmaxcap ();
         ip_timinc -> op_timinc ();
         ip_getcrg -> op_getcrg ();
         ir_clktck -> or_clktck (); 
         ir_calcdist -> or_calcdist (start -> start, end -> end);
      }
   }