Commit 3bd4c75d authored by Colin Eles's avatar Colin Eles
Browse files

Updated data that is stored in the block, removed unneccessary gui components from this 

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@5802 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent d70b012e

GUI.m

+41 −3
Original line number Diff line number Diff line
@@ -29,7 +29,7 @@ classdef GUI < handle 
        % height of header where buttons and text is

        header_height = 100;

        % window size

        fig_height = 500;

        fig_height = 600;

        fig_width = 800;

        % space inbetween buttons in header

        pb_offset = 5;
@@ -41,7 +41,7 @@ classdef GUI < handle 
        text_width = 250;

        name_label = [];

        input_label = [];

        

        Data = [];

        PVS = [];

        

    end
@@ -57,6 +57,15 @@ classdef GUI < handle 
            obj.block_handle = h;

        end

        

        function [] = setData(obj,Data)

            obj.Data = Data;

            obj.Grid0 = Data.Grid0;

            obj.Grid1 = Data.Grid1;

            obj.Grid2 = Data.Grid2;

            obj.function_name_text = Data.function_name;

            obj.function_inputs_text = Data.function_inputs;

        end

        

        %% init

        %   initialize the gui

        % inputs:
@@ -173,7 +182,14 @@ classdef GUI < handle 
            obj.set_command_pos;

            obj.reset_wh();

            obj.draw_allgrids(1);

            

            obj.setPBenable;

            

            obj.initialized = 1;

            obj.Data.open = 1;

            obj.Data.fig = obj.fig;

            

            

        end

        

        %% set_command_pos
@@ -1112,9 +1128,14 @@ classdef GUI < handle 
            save_conditions(object,object.Grid2);

            save_conditions(object,object.Grid1);

            save_results(object,object.Grid0);

            % depricated

            object.function_name_text = get(object.function_name_control,'String')

            object.function_inputs_text = get(object.function_inputs_control,'String')

            

            % new storage

            object.Data.function_name = get(object.function_name_control,'String')

            object.Data.function_inputs = get(object.function_inputs_control,'String')

            object.Data.open = 0;

            object.Data.fig = [];

            % delete the figure, closing the window.

            delete(object.fig);

            % remove reference to the old figure.
@@ -1650,6 +1671,23 @@ classdef GUI < handle 
                end  

            end

        end

        

        function [] = setPBenable(obj)

           if size(obj.Grid1.cells,2) > 1

                set(obj.Grid1.delete_cell_pb,'Enable','on');

           else

                set(obj.Grid1.delete_cell_pb,'Enable','off');

           end

           

           if size(obj.Grid2.cells,2) > 1

                set(obj.Grid2.delete_cell_pb,'Enable','on');

           else

                set(obj.Grid2.delete_cell_pb,'Enable','off');

           end

            

            %set(obj.Grid2.delete_cell_pb,'Enable','off');

            %set(obj.Grid1.delete_cell_pb,'Enable','off');

        end

    end

end

PVS_checker.m

+17 −4
Original line number Diff line number Diff line
@@ -7,6 +7,7 @@ classdef PVS_checker < handle 
        counter_examples = 10000;

        counter_size = 100;

        default_type = 'real';

        pvs_version = 4.2;

    end

    

    methods
@@ -61,6 +62,13 @@ classdef PVS_checker < handle 
            % generate the proof script

            obj.generate_pvs_script(get(obj.gui.function_name_control,'String'))

            

            

            % THIS SECTION NEEDS SOME WORK

            %-------------

            % delete the existing proof

            

            delete([get(obj.gui.function_name_control,'String') '.prf'])

            %---------

            % call pvs in batch mode with script

            % ADD check that pvs actually exists in system

            [status, result] = system(['pvs -batch -v 3 -l ' get(obj.gui.function_name_control,'String') '.el'])
@@ -90,12 +98,17 @@ classdef PVS_checker < handle 
                seqs = [];

                for i = 1:2:size(found,2)-1

                    if(~strcmp(char(found(i+1)),'proved'))

                        found2 = [];

                        found3 = [];

                        

                        found4 = [];

                        % These parsing depend on the version of PVS used,

                        % which may be a bad idea, although pvs is not

                        

                        if obj.pvs_version == 4.0

                        % find the TCC that was unprovable

                            search_str = sprintf('(?<=Proving formula %s[\\n]*)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)),char(found(i)));

                        elseif obj.pvs_version == 4.2

                            search_str =  sprintf('(?<=Installing rewrite rule singleton_rew\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)))

                        end

                        found2 = regexp(result,char(search_str),'match','once');

TTdiag.m

+75 −43
Original line number Diff line number Diff line
@@ -31,77 +31,109 @@ end 
end



function LocalCopyBlockFcn(blockHandleTTTopMask)

    gui = get(blockHandleTTTopMask,'UserData')

    if(~isempty(gui))

        gui_new = gui.clone(blockHandleTTTopMask);  

    data = get(blockHandleTTTopMask,'UserData')

    if(~isempty(data))

        data_new = data.clone(blockHandleTTTopMask);  

    %    gui_new = copy(gui,blockHandleTTTopMask)

    %    gui_new.function_name_text = get_param(blockHandleTTTopMask,'Name');

    %    gui_new.fig = [];

    %    gui_new.block_handle = blockHandleTTTopMask;

    % TEMPORARY SOLUTION

    set_param(blockHandleTTTopMask,'UserData',gui_new)

    set_param(blockHandleTTTopMask,'UserData',data_new)

    end

end



function LocalOpenBlockFcn(blockHandleTTTopMask)



        modelHandle = bdroot(blockHandleTTTopMask);





    gui = get_param(blockHandleTTTopMask,'UserData');

    % check if the user is trying to open the block from the library

    if strcmp(get_param(modelHandle,'Lock'), 'on') || ...

     strcmp(get_param(blockHandleTTTopMask,'LinkStatus'),'implicit')



    if ~isempty(gui)

        gui.block_handle = blockHandleTTTopMask;

        if ishghandle(gui.fig)

            set(gui.fig,'Visible','on')

            figure(gui.fig)

           %gui.init(); 

%           gui.reset_wh();

%            gui.draw_allgrids();

        else

            gui.init();

      errordlg(...

          DAStudio.message('can not open Model Locked, Add to new model to use'),...

          'Error', 'modal')

    return

        end



     



    data = get_param(blockHandleTTTopMask,'UserData');

    

    if isempty(data)

        data = Data();

        data.init();

        

%         gui.block_handle = blockHandleTTTopMask;

%         if ishghandle(gui.fig)

%             set(gui.fig,'Visible','on')

%             figure(gui.fig)

%            %gui.init(); 

% %           gui.reset_wh();

% %            gui.draw_allgrids();

%         else

%             gui.init();

%         end

       % set_param(gui.fig,'Visible','on')

    else

        if strcmp(get_param(modelHandle,'Lock'), 'on') || ...

     strcmp(get_param(blockHandleTTTopMask,'LinkStatus'),'implicit')



        if ~data.valid

             errordlg(...

          DAStudio.message('can not open Model Locked'),...

          DAStudio.message('Block Data has been corputed'),...

          'Error', 'modal')

            return

        end

        if data.open

            if ishghandle(data.fig)

             figure(data.fig)



            end

            return

        end

        

        Grid2 = Grid(2,[]);

        Grid1 = Grid(1,[]);

        rGrid = RGrid(Grid1,Grid2);

        Grid1.set_rGrid(rGrid);

        Grid2.set_rGrid(rGrid);

        Grid2.new_Cell;

        Grid1.new_Cell;

    end

    

    gui = GUI(blockHandleTTTopMask);   

        %gui.init();

        gui.set_grid(Grid2,Grid1,rGrid);

        gui.init();

        %gui.reset_wh();

        %gui.draw_allgrids();

                        set(Grid2.delete_cell_pb,'Enable','off');

                        set(Grid1.delete_cell_pb,'Enable','off');

    

        set_param(blockHandleTTTopMask,'UserData',gui); 

    gui.setData(data)

    gui.init();

%         

%         Grid2 = Grid(2,[]);

%         Grid1 = Grid(1,[]);

%         rGrid = RGrid(Grid1,Grid2);

%         Grid1.set_rGrid(rGrid);

%         Grid2.set_rGrid(rGrid);

%         Grid2.new_Cell;

%         Grid1.new_Cell;

%         

%         gui = GUI(blockHandleTTTopMask);

%         %gui.init();

%         gui.set_grid(Grid2,Grid1,rGrid);

%         gui.init();

%         %gui.reset_wh();

%         %gui.draw_allgrids();

%                         set(Grid2.delete_cell_pb,'Enable','off');

%                         set(Grid1.delete_cell_pb,'Enable','off');

%         

        set_param(blockHandleTTTopMask,'UserData',data); 

        set_param(blockHandleTTTopMask, 'UserDataPersistent', 'on');



    end

    

end



function LocalCloseRequestBlockFcn(blockHandleTTTopMask)

modelHandle = bdroot(blockHandleTTTopMask);





gui = get_param(blockHandleTTTopMask,'UserData')

data = get_param(blockHandleTTTopMask,'UserData')



set_param(gui.fig,'Visible','off')

if ~isempty(data)

    if data.open

        delete(data.fig)

    end

end

        %set_param(gui.fig,'Visible','off')

end



% Make a copy of a handle object.