component RouterArtist is {
      state {
         button : String;
         text_fields : \set String;
         text_field_vals : \set String;
         shipment : Shipment;

         /* C2 graphics binding specific variables;
            should be constant across all artists */
         title      : String;
         id         : String;
         x          : Integer;
         y          : Integer;
         foreground : String;
         background : String;
         width      : Integer;
         height     : Integer;
      }
      invariant {
         (x \eqgreater 0) \and (y \eqgreater 0) \and 
         (width \eqgreater 0) \and (height \eqgreater 0) \and
         (#text_fields = #text_field_vals); 
      }
      interface {
         req ir1: AddShipment(name : String; shp : Shipment);
         prov ip1: CreateViewport(title : String; id : String;
                                  x : Integer; y : Integer;
                                  width : Integer; height : Integer; 
                                  foreground : String; background : String);
         prov ip2: AddButton(x : Integer; y : Integer; width : Integer;
                             height : Integer; foreground : String;
                             background : String; label : String;
                             parent_id : String);
         prov ip3: AddTextField(x : Integer; y : Integer; width : Integer;
                                height : Integer; foreground : String;
                                background : String; label : String;
                                parent_id : String);
         prov ip4: AcceptButtonEvent(button : String; parent_id : String);
         prov ip5: AcceptTextFieldEvent(text_field : String; 
                                        parent_id : String; value : String);
      }
      operations {
         prov op1: {
            let  vport_title : String;
                 vport_id    : String;
                 vport_x     : Integer;
                 vport_y     : Integer;
                 vport_fg    : String;
                 vport_bg    : String;
                 vport_w     : Integer;
                 vport_h     : Integer;
            post (~title = vport_title) \and (~id = vport_id) \and
                 (~x = vport_x) \and (~y = vport_y) \and
                 (~foreground = vport_fg) \and (~background = vport_bg) \and
                 (~width = vport_w) \and (~height = vport_h);
         }
         prov op2: {
            let  vport_title : String;
                 label       : String;
                 button_x    : Integer;
                 button_y    : Integer;
                 button_fg   : String;
                 button_bg   : String;
                 button_w    : Integer;
                 button_h    : Integer;
            pre  (title = vport_title);
            post (~title = title) \and (~label = label) \and
                 (~button_x = button_x) \and (~button_y = button_y) \and
                 (~button_fg = button_fg) \and (~button_bg = button_bg) \and
                 (~button_w = button_w) \and (~button_h = button_h) \and
                 (~button = label);
         }
         prov op3: {
            let  vport_title : String;
                 label       : String;
                 tfield_x    : Integer;
                 tfield_y    : Integer;
                 tfield_fg   : String;
                 tfield_bg   : String;
                 tfield_w    : Integer;
                 tfield_h    : Integer;
            pre  (title = vport_title) \and (label \not_in text_fields);
            post (~title = title) \and (~label = label) \and
                 (~tfield_x = tfield_x) \and (~tfield_y = tfield_y) \and
                 (~tfield_fg = tfield_fg) \and (~tfield_bg = tfield_bg) \and
                 (~tfield_w = tfield_w) \and (~tfield_h = tfield_h) \and
                 (label \in ~text_fields);
         } 
         prov op4: {
            let  b : String;
                 parent : String;
            pre  (b = button) \and (parent = id);
            post (~shipment <> shipment); // place text_field_vals into it 
         }
         prov op5: {
            let  tf : String;
                 parent : String;
                 val : String;
            pre  (tf \in text_fields) \and (parent = id);
            post (val \in ~text_field_vals);
         }
         req or1: {
            let  n : String;
                 shp : Shipment;
            // invokes the appropriate InPort's PlaceShipment
         } 
      }
      map {
         ip1 -> op1 (title -> vport_title, id -> vport_id, x -> vport_x,
                     y -> vport_y, width -> vport_w, height -> vport_h,
                     foreground -> vport_fg, background -> vport_bg);
         ip2 -> op2 (x -> button_x, y -> button_y, width -> button_w,
                     height -> button_h, foreground -> button_fg,
                     background -> button_bg, label -> label, 
                     parent_id -> vport_title);
         ip3 -> op3 (x -> tfield_x, y -> tfield_y, width -> tfield_w,
                     height -> tfield_h, foreground -> tfield_fg,
                     background -> tfield_bg, label -> label, 
                     parent_id -> vport_title);
         ip4 -> op4 (button -> b, parent_id -> parent);
         ip5 -> op5 (text_field -> tf, parent_id -> parent, value -> val);
         ir1 -> or1 (name -> n, shp -> shp);
      }
   }