component DeliveryPort is subtype TimedCargoRouteEntity (int \and beh) {
      state {
         cargo          : \set Shipment;
         cargo_val      : \set String;
         name           : String;
         max_capacity   : Integer;
         capacity       : Integer; 
         internal_clock : Integer;
         selected       : Integer;
      }
      invariant {
         (capacity \eqgreater 0) \and (capacity \eqless max_capacity)
         \and (internal_clock \eqgreater 0);
      }
      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_setmax: SetMaxCapacity(c : Integer);
         prov ip_getmax: GetMaxCapacity() : Integer;
         prov ip_timinc: TimeIncrement(); 
         prov ip_getcrg: GetContentInfo() : \set String; 
         prov ip_selshp: Select(sel : Integer);
         prov ip_dslshp: Deselect(sel : Integer);
         req  ir_clktck: clockTick(); 
      }
      operations {
         prov op_dslshp: {
            let  num : Integer;
            pre  num = selected;
            post ~selected = -1; 
         }
         prov op_selshp: {
            let  num : Integer;
            pre  num \less #cargo;
            post ~selected = num;
         }
         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_setmax: {
            let  num : Integer;
            post ~max_capacity = num;
         }
         prov op_getmax: {
            post \result = max_capacity;
         }
         prov op_timinc: {
            post ~internal_clock = internal_clock + 1; 
         }
         prov op_getcrg: {
            post \result = cargo_val;
         }
         req or_clktck: {
            let  time : STATE_VARIABLE;
            post ~time = time + 1;
         }
      }
      map {
         ip_dslshp -> op_dslshp (sel -> num);
         ip_selshp -> op_selshp (sel -> num);
         ip_setcap -> op_setcap (c -> num);
         ip_getcap -> op_getcap ();
         ip_plcshp -> op_plcshp (shp -> shp, name -> n);
         ip_getshp -> op_getshp (loc -> shp_loc, name -> n);
         ip_remshp -> op_remshp (loc -> shp_loc, name -> n);
         ip_setnam -> op_setnam (new_name -> n);
         ip_getnam -> op_getnam ();
         ip_setmax -> op_setmax (c -> num);
         ip_getmax -> op_getmax ();
         ip_timinc -> op_timinc ();
         ip_getcrg -> op_getcrg ();
         ir_clktck -> or_clktck (); 
      }
   }