Commit 5c825cb1 authored by Colin Eles's avatar Colin Eles
Browse files

added functionality for parsing .prf files 

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

EMLGenerator.m

+1 −1
Original line number Diff line number Diff line
@@ -72,7 +72,7 @@ classdef EMLGenerator < handle 
                        input = [input ',']

                    end

                end

                code = sprintf('function output = %s(%s)\n',obj.data.function_name,input);

                code = sprintf('function output = %s(%s)\n%s\n',obj.data.function_name,input,'%%#eml');

                % 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

GUI.m

+10 −6
Original line number Diff line number Diff line
@@ -345,11 +345,13 @@ classdef GUI < handle 
        % outputs;

        %   none

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

            object.save_data;

            % file name will be expression_name.m

            fileid = fopen([get(object.function_name_control,'String') '.m'],'w');

            code = [];

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

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

            %code = [];

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

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

            code = object.EMLGen.generate_eml_code;

            

            fprintf(fileid,code);

            % save an extra file called expression_name.data which
@@ -434,6 +436,8 @@ classdef GUI < handle 
                    myState = S.find('-isa','Stateflow.EMChart', '-and', 'Path', code_block); % find which one we want to edit

                    if strncmp(myState.Outputs.DataType,'Inherit',7);

                        type = ''

                    elseif strncmp(myState.Outputs.DataType,'boolean',7);

                        type = 'logical'

                    else

                        type = myState.Outputs.DataType;

                    end
@@ -651,9 +655,7 @@ classdef GUI < handle 
        function error = check_matlab_syntax_condition(obj,string,result)

           % split the list of inputs to get inputs seperatly

           

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

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

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

           parsed_input = EMLGenerator.parse_inputs(get(obj.function_inputs_control,'string'));

           check_string = [];

           

           % initialize inputs to zero
@@ -750,6 +752,7 @@ classdef GUI < handle 
            object.fig = [];

        end

        

        %%

        function [] = save_data(object)

            save_conditions(object,object.Grid2);

            save_conditions(object,object.Grid1);
@@ -771,6 +774,7 @@ classdef GUI < handle 
            object.Data.settings = set;

        end

        

        %%

        function [] = save_settings(object)

            set.set = 1;

            set.inputs = object.settings.pvs_includes;

PVS_checker.m

+240 −1
Original line number Diff line number Diff line
@@ -12,6 +12,242 @@ classdef PVS_checker < handle 
        mode = []; % 0 - graphical, 1 - command

    end

    

    

    methods(Static)

    

        function [theory_id, decls] = parse_prf_file()

                decls = [];    

                data = textread('Held_For.prf', '%s', 'whitespace', '', 'bufsize', 100000000);

                %data_one = regexprep(data,'\n','');

                string = data{1};

                if string(1) ~= '('

                   msgbox('error reading file')

                end

                i = 2;

                theory_id = [];

                % find theory name

                while (string(i) ~= ' ')

                    theory_id = [theory_id string(i)];

                    i = i + 1;

                end

                % addvance to next (

                while (string(i) ~= '(')

                    i = i+1;

                end

                

                while(string(i) ~= ')')

                    if (string(i) == '(')

                        pos = i;

                        [decl_id_temp, pos_temp] = PVS_checker.parse_decl_id(string,pos)

                        decls = [decls decl_id_temp];

                        i = pos_temp;

                    end

                    i = i + 1;

                end

           

                



        end



        function [decl_id,new_pos] = parse_decl_id(string,pos)

            i = pos + 1;

            decl_id.id = [];

            decl_id.default_proof_posn = [];

            decl_id.ids = [];

            

            while(string(i) ~= ' ')

               decl_id.id = [decl_id.id string(i)];

               i = i + 1;

            end

            

            while(string(i) == ' ' || string(i) == 10 || string(i) == 13)

                i = i + 1;

            end

            

            

            while(string(i) ~= ' ')

                decl_id.default_proof_posn = [decl_id.default_proof_posn string(i)];

                i = i + 1;

            end

            

            while(string(i) ~= '(')

                i = i + 1;

            end

            

            

            while(string(i) ~= ')')

                if (string(i) == '(')

                    pos = i;

                    [id_temp, pos_temp] = PVS_checker.parse_id(string,pos)

                    decl_id.ids = [decl_id.ids id_temp];

                    i = pos_temp

                end

                i = i + 1;

            end

            new_pos = i;

            



        end



        function [id,new_pos] = parse_id(string,pos)

            i = pos + 1;

            id.id = [];

            id.description = [];

            id.run_date = [];

            id.create_date = [];

            id.status = [];

            id.refers_to = [];

            id.real_time = [];

            id.run_time = [];

            id.interactive = [];

            id.decision_proc = [];

            

            

            while(string(i) ~= ' ')

               id.id = [id.id string(i)];

               i = i + 1;

            end

            

            i = i + 1;

            

            % find the description

            if (string(i) == '"')

                stop_char = '"';

            else

                stop_char = ' ';

            end

            

            while(string(i) ~= stop_char)

               id.description = [id.description string(i)];

               i = i + 1;

            end

            

            if (string(i) == '"')

                i = i + 1;

            end

            

            % get the create_date

            i = i + 1;

            

            while(string(i) ~= ' ')

               id.create_date = [id.create_date string(i)];

               i = i + 1;

            end

            

            % get the run date

            i = i + 1;

            

            while(string(i) ~= ' ')

               id.run_date = [id.run_date string(i)];

               i = i + 1;

            end

            

            while(string(i) ~= '(')

                i = i + 1;

            end

            

            [id.script, new_pos] = PVS_checker.parse_paren(string,i);

            

            i = new_pos + 1;

            while(string(i) == ' ' || string(i) == 10 || string(i) == 13)

                i = i + 1;

            end

            

            %get the status

            

            

            while(string(i) ~= ' ')

               id.status = [id.status string(i)];

               i = i + 1;

            end

            

            while(string(i) == ' ' || string(i) == 10 || string(i) == 13)

                i = i + 1;

            end

            

            % get the refers_to

            

            if (string(i) == '(')

                [id.refers_to, new_pos] = PVS_checker.parse_paren(string,i);

                i = new_pos + 1;

            else

                while(string(i) ~= ' ')

                    id.refers_to = [id.refers_to string(i)];

                    i = i + 1;

                end

            end

            

         

            

            % get the real_time

            

            while(string(i) == ' ' || string(i) == 10 || string(i) == 13)

                i = i + 1;

            end

            

            while(string(i) ~= ' ')

               id.real_time = [id.real_time string(i)];

               i = i + 1;

            end

            

            

            % get the run_time

             while(string(i) == ' ' || string(i) == 10 || string(i) == 13)

                i = i + 1;

            end

            

            while(string(i) ~= ' ' )

               id.run_time = [id.run_time string(i)];

               i = i + 1;

            end

            % get the interactive

            

             while(string(i) == ' ' || string(i) == 10 || string(i) == 13)

                i = i + 1;

            end

            

            while(string(i) ~= ' ')

               id.interactive = [id.interactive string(i)];

               i = i + 1;

            end

            

            % get the decision_proc

             while(string(i) == ' ' || string(i) == 10 || string(i) == 13)

                i = i + 1;

            end

            

            while(string(i) ~= ')')

               id.decision_proc = [id.decision_proc string(i)];

               i = i + 1;

            end

            new_pos = i;

            

        end

        

        % new_pos points to last )

        function [paren_string, new_pos] = parse_paren(string,pos)

            % pos points to opening (

            paren_string = string(pos);

            i = pos+1;

            

            while( string(i) ~= ')')

                if (string(i) == '(')

                    [paren_string_temp, new_pos] = PVS_checker.parse_paren(string,i);

                    paren_string = [paren_string paren_string_temp];

                    i = new_pos;

                else

                    paren_string = [paren_string string(i)];

                end

                i = i + 1;

            end

            paren_string = [paren_string string(i)];

            new_pos = i;

            

        end



    end

    

    

    methods

        

        %% constructor
@@ -327,6 +563,9 @@ classdef PVS_checker < handle 
            end

        end

        

        

        

        

        %% pvs_check_for_imports

        function [] = pvs_check_for_imports_rg(obj)