Commit e9c65373 authored by Colin Eles's avatar Colin Eles
Browse files

created folder for OPG work and sample model of a NOP trip 

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

GUI.m

+27 −8
Original line number Diff line number Diff line
@@ -248,8 +248,10 @@ classdef GUI < handle 
        

        %% pvs_ext_call

        function [] = pvs_ext_call(object,src,event)

            error = object.check_call;

            if (~error)

                object.PVS.pvs_check;

            

            end



        end
@@ -524,14 +526,16 @@ classdef GUI < handle 
        %   event:eventdata - event that triggered the callback

        % outputs;

        %   none

        function [] = check_call(object,src,event)

            

        function error = check_call(object,src,event)

            error = 0;

            msg = object.check_grid_condition(object.Grid2);

            msg = [msg object.check_grid_condition(object.Grid1)];

            msg = [msg object.check_grid_result(object.Grid0)];

            if ~isempty(msg)

                msgbox(msg);

                error = 1;

            end

            

        end

        

        %% check_grid
@@ -548,14 +552,23 @@ classdef GUI < handle 
            msg = [];

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

                

                

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

                 error = ''

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

                

                if ( strcmp(string,'') || isempty(string)) && i == 1 && isempty(grid.parent_grid) && size(grid.cells,2) == 1

                    break

                end

                

                % if the string is empty indicating that the table is 1

                % dimensional or the string is "otherwise" skip the syntax

                % checking.

                if(~isempty(string) && ~strcmp(string,'otherwise'))

                    error = object.check_matlab_syntax_condition(char(string),0);

                end

                 if isempty(error)

                    if (strcmp(string,'') || isempty(string))

                    error = 'Cell is empty'

                    end

                end

                if ~isempty(error)

                    % generate the message string
@@ -599,10 +612,16 @@ classdef GUI < handle 
        function msg = check_grid_result(object,grid)

            msg = [];

            for i = 1:size(grid.Cells,2)

                string = get(grid.Cells(i).result,'String');

                error = ''

                error = object.check_matlab_syntax_condition(char(string),1);

                string = get(grid.Cells(i).result,'String');

                



                error = object.check_matlab_syntax_condition(char(string),1);

                if isempty(error)

                    if (strcmp(string,'') || isempty(string))

                    error = 'Cell is empty'

                    end

                end

                if ~isempty(error)

                     msg = [msg sprintf('\n')];

PVS_checker.m

+5 −4
Original line number Diff line number Diff line
@@ -74,14 +74,15 @@ 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)))

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

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

                    

                    

                    % find the counter examples

                    search_str = sprintf('(?<=%s.*?substitutions:).*?(?=This will undo the proof to: \\n%s)',char(found(i)),char(found(i)))

                    search_str = sprintf('(?<=%s.*?substitutions:).*?(?=This will undo the proof to: \\n%s)|(?<=%s.*?)No counter-examples(?=.*?%s)',char(found(i)),char(found(i)),char(found(i)),char(found(i)))

                    found3 = regexp(result,char(search_str),'match','once')

                    

                    if (~strcmp(found3,'No counter-examples'))

                        found4 = regexp(found3,'[^\n]*(?===>)|(?<===>)[^\n]*','match')

                    end

                    seqs = [seqs struct('id', '1234a', 'TCC', found(i), 'seq', found2, 'ce', {found4})]

                end