component CargoRouteEntityArtist is {
      state {
         entity_name : String;
         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 ip_initvp: InitVport(n : String;
                             x : Integer; y : Integer;
                             h : Integer; w : Integer;
                             fg : String; bg : String);
         prov ip_dispvp: DisplayVport();
         prov ip_dispent: DisplayEntity();
         prov ip_dispcont: DisplayContents();
         prov ip_setnam: SetName(name : String);
         prov ip_selitm: SelectItem(entity : String; item : Integer);
         req ir_continfo: GetContentInfo() : \set String;
         req ir_getnam: GetName() : String;
         req ir_sel: Select(sel : Integer);
         req ir_desel: Deselect(sel : Integer);
         req ir_getcap : GetCapacity() : Integer;
         req ir_setact : SetActive(name : String; act : Boolean);
      }
      operations {
         prov op_initvp: {
            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 op_dispvp: {
            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 op_dispent: {
            post (~vport_name = vport_name) \and (~entity_name = entity_name); 
         }
         prov op_dispcont: {
            post (~vport_name = vport_name) \and 
                 (~contents = contents); 
         }
         prov op_setnam: {
            let  n : String;
            post ~entity_name = n;
         }
         prov op_selitm: {
            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 or_continfo: {
            let  content : STATE_VARIABLE;
            post \result = content;
         }
         req or_getcap: {
            let  capacity : STATE_VARIABLE;
            post \result = capacity;
         }
         req or_getnam: {
            let  name : STATE_VARIABLE;
            post \result = name;
         }
         req or_sel: {
            let  num : Integer;
                 selected : STATE_VARIABLE;
                 cargo_size : STATE_VARIABLE;
            pre  num \eqless cargo_size;
            post ~selected = num;
         }
         req or_desel: {
            let  num : Integer;
                 sel : STATE_VARIABLE;
            pre  num = sel;
            post ~sel = -1;
         }
         req or_setact: {
            let  b : Boolean;
                 n : String;
                 veh_name : STATE_VARIABLE;
                 veh_act : STATE_VARIABLE;
            pre  n = veh_name;
            post (~veh_act = b) \and (~veh_name = veh_name);
         }
      }
      map {
         ip_initvp -> op_initvp (n -> n, x -> x, y -> y, h -> h,
                                 w -> w, fg -> fg, bg -> bg);
         ip_dispvp -> op_dispvp ();
         ip_dispent -> op_dispent ();
         ip_dispcont -> op_dispcont ();
         ip_setnam -> op_setnam (name -> n);
         ip_selitm -> op_selitm (entity -> name, item -> item_loc);
         ir_continfo -> or_continfo ();
         ir_getnam -> or_getnam ();
         ir_getcap -> or_getcap ();
         ir_sel -> or_sel (sel -> num);
         ir_desel -> or_desel (sel -> num);
         ir_setact -> or_setact (name -> n, act -> b);
      }
   }