component CargoRouter is {
      state {
         distances         : \set MapInfo;
         dist_start        : String; // function placeholder
         dist_end_by_start : String; // function placeholder
         dist_start_to_end : Integer; // function placeholder
         current_trips     : \set TripInfo;
         veh_in_transit    : \set String;
      }
      invariant {
         #veh_in_transit = #current_trips;
      }
      interface {
         prov ip_setdist: SetDistance(origin : String; 
                                      destination : String; 
                                      distance : Integer); 
         prov ip_addshp: AddShipment(name : String; shp : Shipment);
         prov ip_bgntrp: BeginTrip(veh_name : String; destination : String);
         prov ip_endtrp: EndTrip(veh_name : String);
         req  ir_plcshp: PlaceShipment(name : String; shp : Shipment);
         req  ir_getshp: GetShipment(name : String; loc : Integer) : Shipment;
         req  ir_remshp: RemoveShipment(name : String; loc : Integer);
         req  ir_setact: Activate(name : String; start : String; 
                                  end : String);
         req  ir_deact: Deactivate(name : String);

      }
      operations {
         prov op_setdist: {
            let  start : String; 
                 end : String; 
                 dist : Integer;
            pre (start = dist_start) \and (end = dist_end_by_start);
            post (~dist_start_to_end = dist) \and 
                 ((#~distances = #distances) \or (#~distances = #distances + 1));
         }
         prov op_bgntrp: {
            let  name : String; 
                 dest : String;
            pre  name \not_in veh_in_transit;
            post (name \in ~veh_in_transit) \and 
                 (#current_trips = #current_trips + 1);
         }
         prov op_endtrp: {
            let  name : String;
            pre  name \in veh_in_transit;
            post (name \not_in ~veh_in_transit) \and 
                 (#current_trips = #current_trips - 1);
         }
         prov op_addshp: {
            let  name : String;
                 s : Shipment;
            // invoke PlaceShipment
         }
         req or_plcshp: {
            let  shp : Shipment; 
                 n : String; 
                 shp_size : Integer;
                 cargo : STATE_VARIABLE;
                 capacity : STATE_VARIABLE;
                 name : STATE_VARIABLE;
            pre  (n = name);
            post (shp \in ~cargo) \and 
                 (~capacity = capacity + shp_size) \and
                 (~name = name);
         }
         req or_getshp: {
            let  shp_loc : Integer;
                 n : String;
                 name : STATE_VARIABLE;
                 shipment_by_location : Shipment; 
            pre  (name = n);
            post (\result = shipment_by_location) \and
                 (~name = name);
         }
         req or_remshp: {
            let  shp_loc : Integer;
                 n : String;
                 shipment_by_location : Shipment; 
                 shipment_size : Integer; 
                 cargo : STATE_VARIABLE; 
                 name : STATE_VARIABLE; 
                 capacity : STATE_VARIABLE; 
            pre  (name = n) \and (shipment_by_location \in cargo);
            post (shipment_by_location \not_in ~cargo) \and
                 (~capacity = capacity - shipment_size) \and
                 (~name = name);
         }
         req or_setact: {
            let  n : String;
                 start : String;
                 end : String;
                 name : STATE_VARIABLE;
                 active : STATE_VARIABLE;
            pre  n = name;
            post ~active <> active;
         }
         req or_deact: {
            let  n : String;
                 name : STATE_VARIABLE;
                 active : STATE_VARIABLE;
            pre  n = name;
            post (~name = name) \and (~active <> active);
         }
      }
      map {
         ip_setdist -> op_setdist (origin -> start, destination -> end,
                                   distance -> dist);
         ip_bgntrp -> op_bgntrp (veh_name -> name, destination -> dest); 
         ip_endtrp -> op_endtrp (veh_name -> name);
         ip_addshp -> op_addshp (name -> name, shp -> s);
         ir_plcshp -> or_plcshp (shp -> shp, name -> n);
         ir_getshp -> or_getshp (loc -> shp_loc, name -> n);
         ir_remshp -> or_remshp (loc -> shp_loc, name -> n);
         ir_setact -> or_setact (name -> n, start -> start, end -> end);
         ir_deact -> or_deact (name -> n);
      }
   }