GUI.m

                            % down by one cell
                            prev_pos = grid.cells(i-1).get_pos;
                            pos(3) = grid.cells(i).width * grid.cells(i).condition_text_width;
                            pos(4) = grid.cells(i).height * grid.cells(i).condition_text_height;
                            pos(1) = parent_pos(1) + parent_pos(3);
                            pos(2) = prev_pos(2) - pos(4);
                            grid_color = grid.cells(i-1).color;
                            
                        end
                    else
                        % grid is the root grid.
                        % position of the first cell is based on
                        % condition_text_x, and condition_text_y, as well
                        % as the height of the figure and header.
                        figpos = get(object.fig,'position');
                        pos = [grid.cells(i).condition_text_x figpos(4)-object.header_height-grid.cells(i).condition_text_y grid.cells(i).condition_text_width grid.cells(i).condition_text_height];
                        if i == 1
                            pos(1) = pos(1);
                            pos(4) = grid.cells(i).height * grid.cells(i).condition_text_height;

                            pos(2) = pos(2)-pos(4)-grid.cells(i).condition_text_height-grid.cells(i).condition_text_offset;
                            pos(3) = grid.cells(i).width * grid.cells(i).condition_text_width;
                            pos(4) = grid.cells(i).height * grid.cells(i).condition_text_height;
                        else
                            prev_pos = grid.cells(i-1).get_pos;
                            pos(3) = grid.cells(i).width * grid.cells(i).condition_text_width;
                            pos(4) = grid.cells(i).height * grid.cells(i).condition_text_height;
                            pos(1) = pos(1);
                            pos(2) = prev_pos(2) - pos(4);
                            grid_color = grid.cells(i-1).color;
                        end
                    end
                    
                    
                    % if the edit box does not exist, ie. it is just being
                    % created or we are loading the figure
                    if (isempty(grid.cells(i).cond) || load == 1)
                        % create the new edit box
                        grid.cells(i).cond = object.create_std_text(object.fig,pos);
                        % if cell is the first in the grid use the new
                        % colour, else take the colour of the previous cell
                        % in the grid.
                        if(i==1)
                        set(grid.cells(i).cond,'BackgroundColor',grid_color);
                        else
                            set(grid.cells(i).cond,'BackgroundColor',get(grid.cells(i-1).cond,'BackgroundColor'))
                        end
                        grid.cells(i).color = grid_color;
                        % if we are loading the cell set the string of the
                        % edit box to be the value that we saved as a
                        % result of calling save_conditions
                        if (load == 1)
                            set(grid.cells(i).cond,'String',grid.cells(i).cond_text);
                        end
                    else
                        % if the edit box is already created change is
                        % position to newly determined position.
                        grid.cells(i).set_pos(pos);
                    end
                    % determine if we want to draw the new subgrid buttons,
                    % which is located to the right of each of the leaf
                    % cells.
                    if(grid.cells(i).pb_flag == 1 && object.edit == 1)
                        pb_pos = pos;
                        pb_pos(1) = pos(1)+pos(3);
                        pb_pos(3) = grid.cells(i).grid_push_width;
                        if (ishghandle(grid.cells(i).grid_pb))
                            set(grid.cells(i).grid_pb,'Visible','on');
                        end
                        grid.cells(i).set_pb(object.fig,pb_pos)
                        set(grid.cells(i).grid_pb,'UserData',object);
                    elseif(grid.cells(i).pb_flag == 1 && object.edit ~= 1)
                        if (ishghandle(grid.cells(i).grid_pb))
                        set(grid.cells(i).grid_pb,'Visible','off')
                        end
                    end
                    
                    delete_pb_pos = [];
                   
                    
                    % detemine if we want to draw the new cell buttons,
                    % which are located at the botton of the set of cells.
                    if (i == size(grid.cells,2) && object.edit == 1)
                        new_pb_pos = pos;
                        new_pb_pos(4) = grid.cells(i).condition_text_height/2;
                        new_pb_pos(3) = pos(3)/2;
                        new_pb_pos(2) = pos(2) - new_pb_pos(4);
                        if (ishghandle(grid.new_cell_pb))
                            set(grid.new_cell_pb,'Visible','on');
                        end
                        grid.set_pb(object.fig,new_pb_pos);
                        set(grid.new_cell_pb,'userdata',object);
                        
                        
                        delete_pb_pos = new_pb_pos;
                        delete_pb_pos(1) = new_pb_pos(1) + new_pb_pos(3);
                        if (ishghandle(grid.delete_cell_pb))
                            set(grid.delete_cell_pb,'Visible','on');
                        end
                        grid.set_delete_pb(object.fig,delete_pb_pos);
                        set(grid.delete_cell_pb,'userdata',object);
                    elseif (i == size(grid.cells,2) && object.edit ~= 1)

                        if (ishghandle(grid.new_cell_pb))
                            set(grid.new_cell_pb,'Visible','off');
                        end

                        if (ishghandle(grid.delete_cell_pb))
                            set(grid.delete_cell_pb,'Visible','off');
                        end
                    end
                    
                    
                    
                    % recursively draw the subgrid of the cell if it
                    % exists.
                    object.draw_grid2(grid.cells(i).subgrid,load);
                end
                
       
            end
        end
        
        %% reset_wh
        %    function will call the set_widths and set_heights methods on
        %    the left grid in the table. The height and width values are
        %    used to draw the grid.
        % inputs:
        %   obj:GUI - current GUI object
        % outputs:
        %   none
        function [] = reset_wh(object)
            width = object.Grid2.max_width(1);
            object.Grid2.set_widths(width);
            object.Grid2.set_heights(object.edit);
        end
        
        %% draw_grid1
        %     Draws the grid on the top onto the figure. the current
        %     assumption is that the top grid does not have any subgrids, 
        % inputs:
        %   obj:GUI - current GUI object
        %   grid:Grid - grid to be drawn, should be grid on top.
        %   load:boolean - 0 if grid is being refreshed, 1 if grid is being
        %       loaded for the firs time.
        % outputs:
        %   none
        function [] = draw_grid1(object,grid,load)
            % assumption grid 1 has no subgrids
            pos = [];
            for i=1:size(grid.cells,2)
                % if we are in edit mode we need to shift over the cells to
                % accomidate for the new grid buttons in the left grid.
                if(object.edit == 1)
                    pb_space = grid.cells(i).grid_push_width;
                else
                    pb_space = 0;
                end
                figpos = get(object.fig,'position');

                % check if grid2 is empty, currently grid 2 will never be
                % empty, may change in future though.
                if (isempty(object.Grid2))      
                    pos = [grid.cells(i).condition_text_x grid.cells(i).condition_text_y grid.cells(i).condition_text_width grid.cells(i).condition_text_height];
                else
                    pos = [grid.cells(i).condition_text_x+grid.cells(i).condition_text_width*object.Grid2.max_width(1) figpos(4)-object.header_height-grid.cells(i).condition_text_y-grid.cells(i).condition_text_height grid.cells(i).condition_text_width grid.cells(i).condition_text_height];
                end
                % set the x coordinate of the cell
                pos(1) = pos(1) + (i-1)*grid.cells(i).condition_text_width + grid.cells(i).condition_text_offset + pb_space;
                % if the edit box does not exist create it, if it does
                % adjust it's position.
                if (isempty(grid.cells(i).cond) || load == 1)
                    grid.cells(i).cond = object.create_std_text(object.fig,pos);
                    if (load == 1)
                        set(grid.cells(i).cond,'String',grid.cells(i).cond_text); 
                    end
                else
                    grid.cells(i).set_pos(pos);
                end
            end
            % if we are in edit mode, draw the new and delete buttons at
            % the right of the last cell
            if( object.edit == 1)
                pos(1) = pos(1) + pos(3);
                pos(2) = pos(2) + 20;
                pos(4) = 20;
                pos(3) = 60;
                grid.set_pb(object.fig,pos);
                pos(2) = pos(2) - 20;
                
                grid.set_delete_pb(object.fig,pos);
                set(grid.delete_cell_pb,'userdata',object);
                set(grid.new_cell_pb,'userdata',object);
            else
                delete(grid.new_cell_pb)
                grid.new_cell_pb = [];
                delete(grid.delete_cell_pb)
                grid.delete_cell_pb = [];
            end
            if object.edit ==1 || load == 1
                fig_pos = get(object.fig,'position');
                if(pos(1)+pos(3)>fig_pos(3))
                    fig_pos(3) = pos(1)+pos(3);
                    set(object.fig,'position',fig_pos);
                elseif (pos(1) + pos(3)<object.fig_width)
                    fig_pos(3) = object.fig_width;
                    set(object.fig,'position',fig_pos);
                elseif (pos(1) + pos(3)<fig_pos(3) && pos(1) +pos(3) >object.fig_width)
                    fig_pos(3) = pos(1)+pos(3);
                    set(object.fig,'position',fig_pos);
                end
            end
        end
        
        %% draw_grid0
        %   function will draw the output grid onto the figure  
        % inputs:
        %   obj:GUI - current GUI object
        %   grid:Grid - grid to be drawn, should be grid on left.
        %   load:boolean - 0 if grid is being refreshed, 1 if grid is being
        %       loaded for the firs time.
        % outputs:
        %   none
        function [] = draw_grid0(object,grid,load)
            % ensure that the results grid is up to date.
            grid.refresh();
            for i=1:size(grid.Cells,2)
                % get the x coordinate from the associated top grid cell,
                % get the y coordinate from the associated right grid cell.
                pos1 = grid.Cells(i).Cell1.get_pos;
                pos2 = grid.Cells(i).Cell2.get_pos;
                pos = [0 0 0 0];
                pos(1) = pos1(1);
                pos(2) = pos2(2);
                pos(3) = pos1(3);
                pos(4) = pos2(4);
                if isempty(grid.Cells(i).result) || load == 1
                    
                    grid.Cells(i).result = object.create_std_text(object.fig,pos);
                    % if we are loading the cell, try to restore the text
                    % that was saved using save_results.
                    if load == 1
                        set(grid.Cells(i).result,'String',grid.Cells(i).result_text);
                    end
                else
                    set(grid.Cells(i).result,'position',pos);
                end
            end
        end
        
        %% draw_allgrids
        %    function will call the draw methods for each of the 3 grids.
        % inputs:
        %   obj:GUI - current GUI object
        %   load:boolean - 0 if grid is being refreshed, 1 if grid is being
        %       loaded for the firs time.
        % outputs:
        %   none
        function [] = draw_allgrids(object,load)
            object.draw_grid2(object.Grid2,load);
            object.draw_grid1(object.Grid1,load);
            
            object.draw_grid0(object.Grid0,load);
        end
        
        %% evaluate_counter
        %    function will call the evaluation function for a given counter
        %    example.
        % inputs:
        %   object:GUI - current GUI object
        %   counter:string - string representing the counter example, ie. 
        %       'x = 3\ny = 5'
        % outputs:
        %   none
        function [] = evaluate_counter(object,counter)
            
            problem = object.evaluate_counter_grid(object.Grid2, counter);
            if(~problem)
                object.evaluate_counter_grid(object.Grid1, counter)
            end
        end
        
        %% evaluate_counter_grid
        %    function will evaluate a counter example for a given grid.
        % inputs:
        %   object:GUI - current GUI object
        %   grid:Grid - the grid to evaluate
        %   counter:string - string representing the counter example, ie. 
        %       'x = 3\ny = 5'
        % outputs:
        %   problem:boolean - 1 if grid has overlapping or underspecified
        %       cells, 0 if not.
        function problem = evaluate_counter_grid(object,grid,counter)
        % split the list of inputs to get inputs seperatly
           inputs = get(object.function_inputs_control,'String');
           inputs = regexp(inputs,',','split');
           check_string = [];
           
           % keep track of the number of condtitions that evaulate to true
           true_conds = 0;
           sub_problem = 0;
           problem = 0;
           empty_cell = 0;
           % initialize inputs to zero
           % functions are assumed to be total, so 0 is just for 
           % convienence
           for i=1:size(inputs,2)
                % set to zero
                
                %need to parse the types out of the inputs
                inputi = regexp(char(inputs(i)),'\w*','match','once');
                check_string = [check_string sprintf('%s=0;\n',char(inputi))];
           end
           
           check_string = [check_string counter sprintf('\n')];
           for i=1:size(grid.cells,2)
                condition_string = get(grid.cells(i).cond,'string');
                if(~isempty(condition_string))
                   
                    eval([check_string  'result =(' char(condition_string) ');'])
                    if(result == 0)
                        grid.cells(i).flag_cell(1);
                    else
                        true_conds = true_conds + 1;
                        
                        grid.cells(i).flag_cell(2);
                    end
                else
                    empty_cell = 1;
                end
           end
           
           if (true_conds == 1)
               for i=1:size(grid.cells,2)
                    condition_string = get(grid.cells(i).cond,'string');
                    if(~isempty(condition_string))

                        eval([check_string  'result =(' char(condition_string) ');'])
                        if(result == 0)
                            grid.cells(i).flag_cell(1);
                        else

                            if (~isempty(grid.cells(i).subgrid))
                                sub_problem = object.evaluate_counter_grid(grid.cells(i).subgrid,counter);
                            end
                            grid.cells(i).flag_cell(2);
                        end
                    else
                        empty_cell = 1;
                    end
               end
           end
           
           
           if (true_conds ~= 1 || sub_problem == 1)
               problem = 1;
           end
           
           if (empty_cell)
               problem = 0;
           end
           
        end
       
        
        %% create_std_text
        %   function will create an edit text box used for conditons and
        %   results. we want these to be consistent so its easier for it to
        %   be in one function.
        % inputs:
        %   obj:GUI - current GUI object
        %   Parent:double - handle to parent figure
        %   position:[double double double double] - position to place edit
        %       box in.
        % outputs:
        %   control:double - handle pointing to newly created uicontrol
        function control = create_std_text(object, Parent, position)
            control = uicontrol('style','edit',...
                'Parent',Parent,...
                'units','pix',...
                'position',position,...
                'min',0,'max',1,...  % This is the key to multiline edits.
                'string',{''},...
                'Max',2.0,...
                'Clipping','on',...
                'fontweight','bold',...
                'BackgroundColor',[1 1 1],...
                'horizontalalign','center',...
                'KeyPressFcn',@(src,event)textbox_callback(object,src,event),...
                'fontsize',11);
        end
       
        %% textbox_callback
        %    callback for when the text of a callback is changed.
        % inputs:
        %   object - current GUI object
        %   src - source of the callback calling
        %   event - event that triggered the callback
        % outputs:
        %   none   
        function [] = textbox_callback(object,src,event)
            % make sure the character pressed isn't empty
            if(~isempty(unicode2native(event.Character)))
                % make sure the character is a printable character
                if event.Character > 33 || event.Character == 8
                    if object.pvs_checked == 1
                    object.pvs_checked = 0;
                    object.update_Statusbar
                        if (object.mode == 1)
                            TableBlock.set_block_display(object.block_handle,object.pvs_checked);
                        end
                    end
                end
            end
            
        end
        
      
        %% check_inputs
        %    ensure that the inputs are proper variable names, and that the
        %    input string parses properly
        % inputs:
        %   object:GUI - current GUI object
        % outputs:
        %   error:string - error string if variable is not inputed properly
        function error = check_inputs(object)
            parsed_input = EMLGenerator.parse_inputs(get(object.function_inputs_control,'string'));
            error = [];
            for i=1:size(parsed_input,2)
                if(size(parsed_input{i},2) == 2)
                    if (strcmp(parsed_input{i}(2),'error'))
                        error = [error sprintf('%s is not a valid variable name\n',char(parsed_input{i}(1))) ];
                    end
                end  
            end
        end
        
        %% setBPenable
        %    enable or diable the delete cell buttons based on the size of
        %    a grid, so that you can't delete below one cell.
        % inputs:
        %   object:GUI - current GUI object
        % outputs:
        %   none
        function [] = setPBenable(object)
           if size(object.Grid1.cells,2) > 1
                set(object.Grid1.delete_cell_pb,'Enable','on');
           else
                set(object.Grid1.delete_cell_pb,'Enable','off');
           end
           
           if size(object.Grid2.cells,2) > 1
                set(object.Grid2.delete_cell_pb,'Enable','on');
           else
                set(object.Grid2.delete_cell_pb,'Enable','off');
           end
            
        end
    end
    
    methods(Static)
        %% msgbox_scroll
        %    create a message box with a scrollable text area
        % inputs:
        %   msg:string - string to put into the message box
        % outputs:
        %   none
        function [] = msgbox_scroll(msg)
            fig = figure('units','pixels',...
                'position',[0 0 700 500],...
                'menubar','none',...
                'name','PVS Report',...       
                'numbertitle','off');
            
        uicontrol('style','edit',...
                'units','pix',...
                'Parent',fig,...
                'HorizontalAlign','center',...
                'FontWeight','bold',...
                'FontSize',12,...
                'Max',2.0,...
                'HorizontalAlign','left',...
                'String',msg,...
                'Position',[1 1 698 498],...
                'BackgroundColor',[1 1 1]);
            
        end
    end
end