Commit 0f08de8b authored by Colin Eles's avatar Colin Eles
Browse files

latest update 

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

GUI.m

+38 −7
Original line number Diff line number Diff line
@@ -301,7 +301,16 @@ classdef GUI < handle 
            for i= 1:size(parsed_input,2)

                input = [input char(parsed_input{i}(1)) ',']

            end

            code = sprintf('function output = %s(%s)\noutput=0;\n',get(object.function_name_control,'String'),input)

            code = sprintf('function output = %s(%s)\n',get(object.function_name_control,'String'),input)

            % simulink forces you to have an output for all execution paths

            % since it can't compute completness and disjointness we need

            % to have a default value, if the user builds the table

            % properly the default value will never be used. since

            % different types might have a different default value, the

            % temporary solution is just to use one of the outputs from our

            % table, we will use the first cell because it is guaranteed to

            % be filled in, regardless of the dimensionality of the table.

            code = [code sprintf('output=%s;\n',get(object.Grid0.Cells(1).result,'String'))]

            code = [code object.generate_code(object.Grid1,object.Grid2,0)];

            fprintf('%s',code);
@@ -1595,16 +1604,38 @@ classdef GUI < handle 
            input_string2 = reshape(input_string',1,size(input_string,1)*size(input_string,2))

           inputs = regexprep(input_string2,'\s','')

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

           inputs = regexp(inputs,':','split')

           

           % need to be careful here because pvs dependant types can have

           % :'s in them

           

           % find the first :, any thing before this is considered the

           % variable any thing following is considered the type

           c_locations = regexp(inputs,':','start')

           for i= 1:size(inputs,2)

                valid = regexp(inputs{i}(1),'[a-zA-Z][_a-zA-Z0-9]*','match')

                if ~strcmp(inputs{i}(1),valid{1})

                    inputs{i}(2) = {'error'}

                if size(c_locations{i},2) == 0

                    sub_input{1} = inputs{i}

                    new_inputs{i} = sub_input

                else

                    sub_input{1} = inputs{i}(1:c_locations{i}(1)-1)

                    sub_input{2} = inputs{i}(c_locations{i}(1)+1:end)

                    new_inputs{i} = sub_input

                    %new_inputs{i}(1) = inputs{i}(1:c_locations{i}(1))

                    %new_inputs{i}(2) = inputs{i}(c_locations{i}(1):end)

                end

                    

           end

           

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

           

           for i=1:size(new_inputs,2)

                valid = regexp(new_inputs{i}(1),'[a-zA-Z][_a-zA-Z0-9]*','match')

                if ~strcmp(new_inputs{i}(1),valid{1})

                    new_inputs{i}(2) = {'error'}

                    %revised_input = cat(2,revised_input,[char(inputs{i}(1)); 'error'])

                end

           end 

           if isempty(revised_input)

               revised_input = inputs

               revised_input = new_inputs

           end

        end

PVS_checker.m

+44 −31
Original line number Diff line number Diff line
@@ -6,6 +6,7 @@ classdef PVS_checker < handle 
        gui = [];

        counter_examples = 10000;

        counter_size = 100;

        default_type = 'real';

    end

    

    methods
@@ -37,12 +38,14 @@ classdef PVS_checker < handle 
           for i=1:size(parsed_inputs,2)

                % set to zero

                if(size(parsed_inputs{i},2) == 2)

                    code = [code sprintf('%s:VAR %s\n',char(parsed_inputs{i}(1)), char(parsed_inputs{i}(2)))];

                    %code = [code sprintf('%s:VAR %s\n',char(parsed_inputs{i}(1)), char(parsed_inputs{i}(2)))];

                    inputs_new = [inputs_new char(parsed_inputs{i}(1)) ':' char(parsed_inputs{i}(2))];

                else

                    code = [code sprintf('%s:VAR real\n',char(parsed_inputs{i}(1)))];

                    %code = [code sprintf('%s:VAR real\n',char(parsed_inputs{i}(1)))];

                    inputs_new = [inputs_new char(parsed_inputs{i}(1)) ':' obj.default_type];

                end

                

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

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

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

                    inputs_new = [inputs_new ',']

                end
@@ -62,7 +65,11 @@ classdef PVS_checker < handle 
            % ADD check that pvs actually exists in system

            [status, result] = system(['pvs -batch -v 3 -l ' get(obj.gui.function_name_control,'String') '.el'])

            %object.msgbox_scroll(result);

            parsed = obj.parse_pvs_result(result);

            [parsed error] = obj.parse_pvs_result(result);

            if (error == 1)

                msgbox(result);

            else

                

                if (isempty(parsed))

                    msgbox('table is valid')

                else
@@ -71,34 +78,40 @@ classdef PVS_checker < handle 
                    Valid_Report.init();

                end

            end

        end

        

        %% parse_pvs_result

        function output = parse_pvs_result(obj,result)

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

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

            char(found)

            if (isempty(found))

                error = 1

                output = []

            else

                seqs = [];

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

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

                    found2 = []

                    found3 = []

                    found4 = []

                        found2 = [];

                        found3 = [];

                        found4 = [];



                        % 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','once')

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

                        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)|(?<=%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')

                        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')

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

                        end

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

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

                    end



                end

                output = seqs;

                error = 0;

            end

        end

        

              %% matlab_to_pvs_syntax_translation