component Warehouse is subtype CargoRouteEntity (int \and beh) {
      state {
         cargo          : \set Shipment;
         cargo_val      : \set String;
         name           : String;
         max_capacity   : Integer;
         capacity       : Integer; 
         internal_clock : Integer;
      }
      invariant {
         (capacity \eqgreater 0) \and (capacity \eqless max_capacity); 
      }
      interface {
         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_getcrg: GetContentInfo() : \set String; 
      }
      operations {
         prov op_setcap: {
            let  num : Integer;
            post ~capacity = num;
         }
         prov op_getcap: {
            post \result = capacity;
         }
         prov op_plcshp: {
            let  shp : Shipment;
                 n : String;
                 shp_size : Integer; // a function placeholder
            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;
                 n : String;
                 shp_by_loc : Shipment; // a function placeholder
                 shp_size : Integer; // 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_setmaxcap: {
            let  num : Integer;
            post ~max_capacity = num;
         }
         prov op_getmaxcap: {
            post \result = max_capacity;
         }
         prov op_getcrg: {
            post \result = cargo_val;
         }
      }
      map {
         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_setmaxcap -> op_setmaxcap (c -> num);
         ip_getmaxcap -> op_getmaxcap ();
         ip_getcrg -> op_getcrg ();
      }
   }