Commit 942eb7be authored by Colin Eles's avatar Colin Eles
Browse files

minor adjustments to prevent output from being displayed 

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

GUI.m

+83 −83

File changed.

Preview size limit exceeded, changes collapsed.

Grid.m

+6 −6
Original line number Diff line number Diff line
@@ -66,9 +66,9 @@ classdef Grid < handle 
           last_cell = obj.num_cells;

           obj.rGrid.delete_g2s(obj.cells(end));

           delete(obj.cells(end).cond)

           obj.cells(end).cond = []

           obj.cells(end).cond = [];

           delete(obj.cells(end).grid_pb);

           obj.cells(end).grid_pb = []

           obj.cells(end).grid_pb = [];

           delete(obj.cells(end))

           obj.cells(end) = [];

           if(~isempty(obj.rGrid))
@@ -87,7 +87,7 @@ classdef Grid < handle 
        %   m:integer - value representing the maximum width from the

        %   current grid.

        function m = max_width(obj,width)

            temp = []

            temp = [];

            for i=1:size(obj.cells,2)

                if (~isempty(obj.cells(i).subgrid))

                    temp = [temp obj.cells(i).subgrid.max_width(width+1)];
@@ -214,7 +214,7 @@ classdef Grid < handle 
         function [] = pb_delete_call(obj,src,event)

           gui = get(src,'userdata');

        

           deleted_cell = obj.cells(end)

           deleted_cell = obj.cells(end);

            % button could be pressed in the left or top grid so we need to

            % try to remove the result cell associated with either case.

            obj.rGrid.delete_g2s(deleted_cell);
@@ -267,9 +267,9 @@ classdef Grid < handle 
         function [] = clone(obj,dest_grid,index,p_cell)

            for i=1:size(obj.cells,2)

                dest_grid.new_Cell();

                dest_grid.cells(i).cond_text = obj.cells(i).cond_text

                dest_grid.cells(i).cond_text = obj.cells(i).cond_text;

                if (~isempty(obj.cells(i).subgrid))

                    dest_grid.cells(i).subgrid = Grid(dest_grid.cells(i).cell_index,dest_grid.cells(i))

                    dest_grid.cells(i).subgrid = Grid(dest_grid.cells(i).cell_index,dest_grid.cells(i));

                    dest_grid.cells(i).subgrid.set_rGrid(dest_grid.cells(i).parent_grid.rGrid);

                   obj.cells(i).subgrid.clone(dest_grid.cells(i).subgrid,obj.cells(i).subgrid.grid_index,dest_grid.cells(i))

                else

PVS_checker.m

+26 −24
Original line number Diff line number Diff line
@@ -33,7 +33,7 @@ classdef PVS_checker < handle 
            

            %inputs = get(obj.gui.function_inputs_control,'String');

           %inputs = regexp(inputs,',','split');

                       parsed_inputs = obj.gui.parse_inputs(get(obj.gui.function_inputs_control,'string'))

                       parsed_inputs = obj.gui.parse_inputs(get(obj.gui.function_inputs_control,'string'));

                       

           % initialize inputs to zero

           % functions are assumed to be total, so 0 is just for
@@ -51,7 +51,7 @@ classdef PVS_checker < handle 
                

                %inputs_new = [inputs_new char(parsed_inputs{i}(1))];

                if(i~=(size(parsed_inputs,2)))

                    inputs_new = [inputs_new ',']

                    inputs_new = [inputs_new ','];

                end

           end
@@ -92,20 +92,23 @@ classdef PVS_checker < handle 
        end

        

        function [string] = user_imports(obj)

            files = regexp(obj.settings.pvs_includes,',','split')

            string = [];

            if ~isempty(obj.settings.pvs_includes)

                files = regexp(obj.settings.pvs_includes,',','split');

                

                for i=1:size(files,2)

                   file_no_ext = regexp(files{i},'\w*(?=\.\w*)','match');

                   string = [string sprintf('IMPORTING %s\n', char(file_no_ext)) ];

                end

            end

        end

        

        %% parse_pvs_result

        function [output error] = parse_pvs_result(obj,result)

            found = regexp(result,'\w+(?=[\.]{4,})|(?<=[\.]{4,})\w+','match')

            found = regexp(result,'\w+(?=[\.]{4,})|(?<=[\.]{4,})\w+','match');

            if (isempty(found))

                error = 1

                output = []

                error = 1;

                output = [];

            else

                seqs = [];

                for i = 1:2:size(found,2)-1
@@ -119,7 +122,7 @@ classdef PVS_checker < handle 
                        % 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)))

                            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');
@@ -144,12 +147,12 @@ classdef PVS_checker < handle 
              % will be added to in the future

              % will only work for functions in the prelude

        function pvs_string = matlab_to_pvs_syntax_translation(obj,matlab_string)

            pvs_string = regexprep(matlab_string,'&&',' AND ')

            pvs_string = regexprep(pvs_string,'~(?!=)',' NOT ')

            pvs_string = regexprep(pvs_string,'~=',' /= ')

            pvs_string = regexprep(pvs_string,'==',' = ')

            pvs_string = regexprep(pvs_string,'\|\|',' OR ')

            pvs_string = regexprep(pvs_string,'ceil','ceiling')

            pvs_string = regexprep(matlab_string,'&&',' AND ');

            pvs_string = regexprep(pvs_string,'~(?!=)',' NOT ');

            pvs_string = regexprep(pvs_string,'~=',' /= ');

            pvs_string = regexprep(pvs_string,'==',' = ');

            pvs_string = regexprep(pvs_string,'\|\|',' OR ');

            pvs_string = regexprep(pvs_string,'ceil','ceiling');

        end
@@ -174,7 +177,7 @@ classdef PVS_checker < handle 
                code = [code sprintf('%s->',obj.matlab_to_pvs_syntax_translation(strtrim(char(get(g1.cells(i).cond,'String')))))];

                resultcell = obj.gui.Grid0.search_return(g1.cells(i),g2_cell);

                if(~isempty(resultcell))

                    code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String'))))]

                    code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String'))))];

                    

                    if(isempty(elsecell))

                        if(i~= size(g1.cells,2))
@@ -235,7 +238,7 @@ classdef PVS_checker < handle 
                

                        resultcell = obj.gui.Grid0.search_return(g1.cells(1),g2.cells(i));

                        if(~isempty(resultcell))

                            code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String'))))]

                            code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String'))))];



                            

                        else
@@ -268,7 +271,7 @@ classdef PVS_checker < handle 
                

                        resultcell = obj.gui.Grid0.search_return(g1.cells(1),elsecell);

                        if(~isempty(resultcell))

                            code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String')))) sprintf('\n')]

                            code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String')))) sprintf('\n')];
@@ -285,13 +288,12 @@ classdef PVS_checker < handle 
            

            

          end

          code

        end

        

        %% pvs_check_for_imports

        function string = pvs_check_for_imports(obj)

            [string,found] = obj.pvs_check_for_imports_g(obj.gui.Grid2,{});

            [string2,found2] = obj.pvs_check_for_imports_g(obj.gui.Grid1,found)

            [string2,found2] = obj.pvs_check_for_imports_g(obj.gui.Grid1,found);

            string = [string string2];

        end
@@ -305,14 +307,14 @@ classdef PVS_checker < handle 
                end

                text = char(get(grid.cells(i).cond,'String'));

                

                vars = regexp(text,'([a-zA-Z][a-zA-Z0-9_]*)','match')

                vars = regexp(text,'([a-zA-Z][a-zA-Z0-9_]*)','match');

                

                for j=1:size(vars,2)

                   if(exist(vars{j},'file')==2 && ~strcmp(vars{j},'otherwise'))

                       %check if already imported file

                       if (~any(ismember(found,vars{j})))

                            string = [string 'IMPORTING ' vars{j} sprintf('\n')];

                            found = [found vars{j}]

                            found = [found vars{j}];

                       end

                   end

                end
@@ -327,7 +329,7 @@ classdef PVS_checker < handle 
        %% generate_pvs_script

        function [] = generate_pvs_script(obj,filename)

            fileid = fopen([filename '.el'],'w');

            code = ['(prove-tccs-pvs-file "' filename '" "(try (try (tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',obj.settings.counter_trials) ' :size ' sprintf('%d',obj.settings.counter_range) '))"  )' sprintf('\n')]

            code = ['(prove-tccs-pvs-file "' filename '" "(try (try (tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',obj.settings.counter_trials) ' :size ' sprintf('%d',obj.settings.counter_range) '))"  )' sprintf('\n')];



            fprintf(fileid,code);

            fclose(fileid);

Settings.m

+10 −10
Original line number Diff line number Diff line
@@ -96,8 +96,8 @@ classdef Settings < handle 
                'Position',[0, obj.fig_height-obj.text_offset-obj.title_height, obj.fig_width, obj.title_height],...

                'BackgroundColor',get(obj.fig,'Color'));

            

            panel_height = obj.text_offset*6+obj.label_height*3

            panel_width = obj.fig_width-obj.text_offset*2

            panel_height = obj.text_offset*6+obj.label_height*3;

            panel_width = obj.fig_width-obj.text_offset*2;

            panel = uipanel('Title','PVS',...

                'visible','on',...

                'units','pix',...
@@ -186,10 +186,10 @@ classdef Settings < handle 
            string = [];

            if iscell(files)

                for i = 1:size(files,2)

                    string = strcat(string,files(i))

                    string = strcat(string,files(i));

                    %string = [string, files(i)];

                    if i ~= size(files,2)

                        string = strcat(string,', ')

                        string = strcat(string,', ');

                        %string = [string, ',']

                    end

                end
@@ -201,22 +201,22 @@ classdef Settings < handle 
        end

        

        function err = save(obj)

            msg = []    

            msg = []    ;

            err = 0;

            if isempty(str2num(get(obj.count_text,'String')))

                msg = [msg get(obj.count_text,'String') ' is not a valid number']

                msg = [msg get(obj.count_text,'String') ' is not a valid number'];

                err = 1;

            else

                obj.counter_trials = str2num(get(obj.count_text,'String'))

                obj.counter_trials = str2num(get(obj.count_text,'String'));

            end

            

            if isempty(str2num(get(obj.range_text,'String')))

                msg = [msg sprintf('\n') get(obj.count_text,'String') ' is not a valid number']

                msg = [msg sprintf('\n') get(obj.count_text,'String') ' is not a valid number'];

                err = 1;

            else

                obj.counter_range = str2num(get(obj.range_text,'String'))

                obj.counter_range = str2num(get(obj.range_text,'String'));

            end

            obj.pvs_includes = get(obj.include_text,'String')

            obj.pvs_includes = get(obj.include_text,'String');

           

            if err

                msgbox(msg);

ValidationReport.m

+8 −8
Original line number Diff line number Diff line
@@ -50,8 +50,8 @@ classdef ValidationReport < handle 
            

            else

            

                obj.fig_width = obj.offset + obj.TCC_width + obj.offset + obj.seq_width + obj.offset + obj.ce_width + obj.offset

                obj.fig_height = obj.offset + obj.header_height + obj.offset + obj.seq_height + obj.offset

                obj.fig_width = obj.offset + obj.TCC_width + obj.offset + obj.seq_width + obj.offset + obj.ce_width + obj.offset;

                obj.fig_height = obj.offset + obj.header_height + obj.offset + obj.seq_height + obj.offset;

                obj.fig = figure('units','pixels',...

                    'position',[0, 0, obj.fig_width, obj.fig_height ],...

                    'menubar','none',...
@@ -60,7 +60,7 @@ classdef ValidationReport < handle 
                    'resize','off',...

                    'CloseRequestFcn',@(src,event)close_req_call(obj,src,event));



                stop = 0

                stop = 0;

                i = 1;

                count = 0;
@@ -199,20 +199,20 @@ classdef ValidationReport < handle 
            set(obj.edit_tcc,'string',char(obj.PVS_results(obj.page).TCC));

            set(obj.edit_seq,'string',char(obj.PVS_results(obj.page).seq));

            set(obj.label_page,'string',[num2str(obj.page) '  of  ' num2str(size(obj.PVS_results,2))]);

            counter = []

            counter = [];

            if size(obj.PVS_results(obj.page).ce,2) == 0

                counter = ['no counter example generated']

                counter = ['no counter example generated'];

           

            else

                for i = 1:2:size(obj.PVS_results(obj.page).ce,2)

                    

                    

                    % need to do some translation back to matlab syntax

                    new_value = regexprep(char(obj.PVS_results(obj.page).ce(i+1)),'FALSE',' 0 ')

                    new_value = regexprep(new_value,'TRUE',' 1 ')

                    new_value = regexprep(char(obj.PVS_results(obj.page).ce(i+1)),'FALSE',' 0 ');

                    new_value = regexprep(new_value,'TRUE',' 1 ');

                    eval(['value = ' char(new_value)])



                    counter = [counter char(obj.PVS_results(obj.page).ce(i)) ' = ' num2str(value) ';' sprintf('\n')]

                    counter = [counter char(obj.PVS_results(obj.page).ce(i)) ' = ' num2str(value) ';' sprintf('\n')];

                end