component LayoutManager is {
      state {
         ports      : \set String;
         warehouses : \set String;
         vehicles   : \set String;
         buttons    : \set String;
         diff       : Integer;

         /* 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 {
         (#ports \eqgreater 0) \and (#warehouses \eqgreater 0) \and 
         (#vehicles \eqgreater 0) \and 
         (x \eqgreater 0) \and (y \eqgreater 0) \and 
         (width \eqgreater 0) \and (height \eqgreater 0) \and 
         (diff \eqgreater 0); 
      }
      interface {
         req ir1: DisplayVport();
         req ir2: DisplayEntity();
         req ir3: DisplayContents();
         req ir4: SelectItem(entity : String; item : Integer); 
         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: AcceptSelectEvent(list : String; parent_id : String;
                                     select_index : Integer);
         prov ip4: AcceptDeselectEvent(list : String; parent_id : String;
                                       deselect_index : Integer);
         prov ip5: AcceptButtonEvent(button : String; parent_id : 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) \and (label \not_in buttons);
            post (~vport_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
                 (label \in ~buttons);
         }
         prov op3: {
            let  lid : String;
                 pid : String;
                 itm : Integer;
            pre  ((lid \in ports) \or  
                  (lid \in warehouses) \or 
                  (lid \in vehicles)) \and
                 pid = id;
         }
         prov op5: {
            let  b : String;
                 pid : String;
            pre  (b \in buttons) \and (pid = id);
         }
         req or1: {
            let  vport_name : STATE_VARIABLE;
                 height : STATE_VARIABLE;
                 width : STATE_VARIABLE;
                 vport_fg : STATE_VARIABLE;
                 vport_bg : STATE_VARIABLE; 
            post (~vport_name = vport_name) \and 
                 (~height = height) \and (~width = width) \and 
                 (~vport_fg = vport_fg) \and (~vport_bg = vport_bg);
         } 
         req or2: {
            let  vport_name : STATE_VARIABLE;
                 entity_name : STATE_VARIABLE;
            post (~vport_name = vport_name) \and (~entity_name = entity_name);
         }
         req or3: {
            let  vport_name : STATE_VARIABLE;
                 cargo : STATE_VARIABLE;
            post (~vport_name = vport_name) \and
                 (~cargo = cargo); // cargo will be displayed as a set of strings
         }
         req or4: {
            let  entity_name : String;
                 item_loc : Integer;
                 vport_name : STATE_VARIABLE;
                 cargo_size : STATE_VARIABLE;
                 selected : STATE_VARIABLE;
            pre  (item_loc \eqless cargo_size) \and (entity_name = vport_name);
            post (~selected = item_loc) \and (~vport_name = vport_name);
         }
      }
      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 (list -> lid, parent_id -> pid, select_index -> itm);
         ip4 -> op3 (list -> lid, parent_id -> pid, deselect_index -> itm);
         ip5 -> op5 (button -> b, parent_id -> pid);
         ir1 -> or1 ();
         ir2 -> or2 ();
         ir3 -> or3 ();
         ir4 -> or4 (entity -> entity_name, item -> item_loc);
      }
   }