component DeliveryPortArtist is subtype CargoRouteEntityArtist(int \and beh) {
      state {
         entity_name : String; // InPort
         contents    : \set String;
         vport_name  : String;
         vport_xpos  : Integer;
         vport_ypos  : Integer;
         vport_fg    : String;
         vport_bg    : String;
         width       : Integer;
         height      : Integer;
         selection   : Integer;
      }
      invariant {
         (width \eqgreater 0) \and (height \eqgreater 0) \and 
         (vport_xpos \eqgreater 0) \and (vport_ypos \eqgreater 0); 
      }
      interface {
         prov ip1: InitVport(n : String;
                             x : Integer; y : Integer;
                             h : Integer; w : Integer;
                             fg : String; bg : String);
         prov ip2: DisplayVport();
         prov ip3: DisplayEntity();
         prov ip4: DisplayContents();
         prov ip5: SetName(name : String);
         prov ip6: SelectItem(entity : String; item : Integer);
         req ir1: GetCapacity() : Integer;
         req ir2: GetContentInfo() : \set String;
         req ir3: GetName() : String;
         req ir4: Select(sel : Integer);
         req ir5: Deselect(sel : Number);
      }
      operations {
         prov op1: {
            let  n : String;
                 x : Integer;
                 y : Integer;
                 h : Integer;
                 w : Integer;
                 fg : String;
                 bg : String;
            pre  (x \eqgreater 0) \and (y \eqgreater 0) \and
                 (h \eqgreater 0) \and (w \eqgreater 0);
            post (~vport_name = n) \and (~vport_xpos = x) \and
                 (~vport_ypos = y) \and (~height = h) \and
                 (~width = w) \and (~vport_fg = fg) \and (~vport_bg = bg);
         }
         prov op2: {
            post (~vport_name = vport_name) \and 
                 (~vport_xpos = vport_xpos) \and 
                 (~vport_ypos = vport_ypos) \and 
                 (~height = height) \and (~width = width) \and 
                 (~vport_fg = vport_fg) \and (~vport_bg = vport_bg);
         } 
         prov op3: {
            post (~vport_name = vport_name) \and (~entity_name = entity_name); 
         }
         prov op4: {
            post (~vport_name = vport_name) \and 
                 (~contents = contents); 
         }
         prov op5: {
            let  n : String;
            post ~entity_name = n;
         }
         prov op6: {
            let  name : String;
                 item_loc : Integer;
            pre  (item_loc \eqless #contents) \and (name = entity_name);
            post (~selection = item_loc) \and (~entity_name = entity_name);
         }
         req or1: {
            let  capacity : STATE_VARIABLE;
            post \result = capacity;
         }
         req or2: {
            let  cargo : STATE_VARIABLE;
            post \result = cargo;
         }
         req or3: {
            let  NAME : STATE_VARIABLE;
            post \result = NAME;
         }
         req or4: {
            let  num : Integer;
                 selection : STATE_VARIABLE;
                 cargo_size : STATE_VARIABLE;
            pre  num \eqless cargo_size;
            post ~selection = num;
         }
         req or5: {
            let  num : Number;
                 sel : STATE_VARIABLE;
            pre  num = sel;
            post ~sel = -1;
         }
      }
      map {
         ir1 -> or1 ();
         ir2 -> or2 ();
         ir3 -> or3 ();
         ir4 -> or4 (sel -> num);
         ir5 -> or5 (sel -> num);
         ip1 -> op1 (n -> n, x -> x, y -> y, h -> h,
                     w -> w, fg -> fg, bg -> bg);
         ip2 -> op2 ();
         ip3 -> op3 ();
         ip4 -> op4 ();
         ip5 -> op5 (name -> n);
         ip6 -> op6 (entity -> name, item -> item_loc);
      }
   }