Commit 004091be authored by Colin Eles's avatar Colin Eles
Browse files

added typing to output for pvs purposes 

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

@EMLGenerator/generate_preamble.m

+2 −2
Original line number Diff line number Diff line
@@ -8,7 +8,7 @@ 
        %   code:string - string of eml code

        function code = generate_preamble(object)

                code = [];



                function_name = EMLGenerator.parse_inputs(object.data.function_name);

                %generate input list

                parsed_input = EMLGenerator.parse_inputs(object.data.function_inputs);

                input = [];
@@ -18,7 +18,7 @@ 
                        input = [input ',']

                    end

                end

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

                code = sprintf('function output = %s(%s)\n%s\n',char(function_name{1}(1)),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/save_call.m

+5 −2
Original line number Diff line number Diff line
@@ -14,6 +14,9 @@ 
             if(object.check_call([],[]) == 1)

                 return;

             end

             

             function_names = EMLGenerator.parse_inputs(get(object.function_name_control,'String'));

             function_name = char(function_names{1}(1));

            object.save_data;

            if object.mode == 0

                model = gcs;
@@ -31,7 +34,7 @@ 
                %end

                open_system(model);

                load_system('TableLibrary');

                new_block = add_block('TableLibrary/Tabular Expression',[model '/' get(object.function_name_control,'String')]);

                new_block = add_block('TableLibrary/Tabular Expression',[model '/' function_name]);

                set_param(new_block,'UserData',object.Data)

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

                object.mode = 1;
@@ -47,7 +50,7 @@ 
                %code = [code object.generate_code(object.Grid1,object.Grid2,0)];

                %fprintf('%s',code);



               eml_handle = TableBlock.set_code(object.block_handle,code,object.Data.function_name);

               eml_handle = TableBlock.set_code(object.block_handle,code,function_name);

@PVS_checker/generate_pvs_file.m

+14 −9
Original line number Diff line number Diff line
@@ -9,10 +9,17 @@ 
        % outputs;

        %   none

        function [] = generate_pvs_file(object,filename)

        type_mode = 1;

        % type_mode = 0 -> use pvs types

        % type_mode = 1 -> use simulink typing information

        type_mode = 0;

        

         function_names = EMLGenerator.parse_inputs(object.data.function_name);

         function_name = char(function_names{1}(1));

         function_name_type = char(function_names{1}(2));

        

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

            code = [];

            code = sprintf('%s:THEORY\nBEGIN\n',object.data.function_name);

            code = sprintf('%s:THEORY\nBEGIN\n',function_name);

            code = [code sprintf('IMPORTING Funcs\n')];

            code = [code object.pvs_check_for_imports];
@@ -25,9 +32,7 @@ 
           %inputs = regexp(inputs,',','split');

                       parsed_inputs = EMLGenerator.parse_inputs(object.data.function_inputs);

                       

           % initialize inputs to zero

           % functions are assumed to be total, so 0 is just for 

           % convienence

           % add inputs to list of inputs to function

           inputs_new = [];

           for i=1:size(parsed_inputs,2)

                % set to zero
@@ -41,16 +46,16 @@ 
                    inputs_new = [inputs_new ','];

                end

           end

              code = [code sprintf('%s(%s):real = \n',object.data.function_name,inputs_new)];

              code = [code sprintf('%s(%s):%s = \n',function_name,inputs_new,function_name_type)];



            else

                inputs_new = [];

           for i=1:size(object.input_type,2)

           for i=1:size(object.input_type,1)

               

        

                   inputs_new = [inputs_new char(object.input_type(i,1)) ':' PVS_checker.matlab_type_to_pvs_type(char(object.input_type(i,2)))];

                

                if(i~=(size(object.input_type,2)))

                if(i~=(size(object.input_type,1)))

                    inputs_new = [inputs_new ','];

                end

           end
@@ -59,7 +64,7 @@ 
                

            end

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

            code = [code sprintf('\nEND %s',object.data.function_name)];

            code = [code sprintf('\nEND %s',function_name)];

            fprintf(fileid,code);



            fclose(fileid);

@PVS_checker/matlab_type_to_pvs_type.m

+1 −1
Original line number Diff line number Diff line
@@ -12,7 +12,7 @@ function matlab_type = matlab_type_to_pvs_type( pvs_type ) 
    elseif (strncmp(pvs_type,'fixdt',5))

        params = regexp(pvs_type,'(?<=\().*(?=\))','match');

        split_params = regexp(params,',','split');

        matlab_type = sprintf('fp[%d,%d,%d]',eval(char(split_params{1}(2))),eval(char(split_params{1}(2)))-eval(char(split_params{1}(3)))-eval(char(split_params{1}(1))),eval(char(split_params{1}(1))));

        matlab_type = sprintf('fp2[%d,%d,%d]',eval(char(split_params{1}(2))),eval(char(split_params{1}(2)))-eval(char(split_params{1}(3)))-eval(char(split_params{1}(1))),eval(char(split_params{1}(1))));

    else

        matlab_type = 'error';

    end

@PVS_checker/pvs_check.m

+11 −8
Original line number Diff line number Diff line
@@ -11,7 +11,10 @@ 
            check = 0;

            output = [];

            % file name will be expression_name.m

            object.generate_pvs_file(object.data.function_name);

            

             function_names = EMLGenerator.parse_inputs(object.data.function_name);

             function_name = char(function_names{1}(1));

            object.generate_pvs_file(function_name);

            

            object.pvs_version = PVS_checker.get_pvs_version;
@@ -25,31 +28,31 @@ 
            

            exists = 0;

            button = '';

            if (exist([object.data.function_name '.prf'],'file'))

            if (exist([function_name '.prf'],'file'))

                exists = 1;

                button = questdlg(['A proof file already exists for function ' object.data.function_name sprintf('\n') ' What would you like to do' sprintf('\n') 'Note: Attempting to prove will delete existing prf file'],'prf exists','Attempt to prove','Open PVS','Cancel','Cancel') 

                button = questdlg(['A proof file already exists for function ' function_name sprintf('\n') ' What would you like to do' sprintf('\n') 'Note: Attempting to prove will delete existing prf file'],'prf exists','Attempt to prove','Open PVS','Cancel','Cancel') 

            end

            

            if (exists == 1 && (isempty(button) || strcmp(button,'Cancel')))

                output = 'canceled';

                return;

            elseif (exists == 1 && (strcmp(button,'Open PVS')));

                [status, result] = system(['pvs ' object.data.function_name '.pvs']);

                [status, result] = system(['pvs ' function_name '.pvs']);

                output = 'canceled';

            elseif (exists == 0 || strcmp(button,'Attempt to prove'))

                box = waitbar(0,'Generating Proof Script') 





                    delete([object.data.function_name '.prf'])

                    delete([function_name '.prf'])





                % generate the proof script

                object.generate_pvs_script(object.data.function_name)

                object.generate_pvs_script(function_name)

                waitbar(.10,box,'Running Proof') 

                %---------

                % call pvs in batch mode with script

                % ADD check that pvs actually exists in system

                [status, result] = system(['pvs -batch -v 3 -l ' object.data.function_name '.el'])

                [status, result] = system(['pvs -batch -v 3 -l ' function_name '.el'])

                %objectect.msgbox_scroll(result);

                waitbar(.70,box,'Parsing Results') 

                [parsed error] = object.parse_pvs_result(result);
@@ -68,7 +71,7 @@ 
                end

                waitbar(.100,box,'Deleting Proof Script') 



                delete([object.data.function_name '.el']);

                delete([function_name '.el']);

                

                delete(box);

            end