Commit 69b5f1fc authored by Colin Eles's avatar Colin Eles
Browse files

latest version 

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@5825 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 40eabec8

GUI.m

+4 −1
Original line number Diff line number Diff line
@@ -196,7 +196,7 @@ classdef GUI < handle 
                set(obj.function_inputs_control,'String',obj.function_inputs_text);

            end



            obj.PVS = PVS_checker(obj);

            

            

            obj.set_command_pos;

            obj.reset_wh();
@@ -210,8 +210,11 @@ classdef GUI < handle 
                obj.settings.setvalues(obj.Data.settings);

            else

                obj.settings.init();

                

            end

            

            obj.PVS = PVS_checker(obj,obj.settings);

            

            obj.initialized = 1;

            obj.Data.open = 1;

            obj.Data.fig = obj.fig;

PVS_checker.m

+15 −3
Original line number Diff line number Diff line
@@ -8,13 +8,15 @@ classdef PVS_checker < handle 
        counter_size = 100;

        default_type = 'real';

        pvs_version = 4.2;

        settings

    end

    

    methods

        

        %% constructor

        function obj = PVS_checker(gui_new)

        function obj = PVS_checker(gui_new,settings)

            obj.gui = gui_new;

            obj.settings = settings;

        end

        

        %% pvs_ext_call
@@ -26,6 +28,7 @@ classdef PVS_checker < handle 
             

            code = [code obj.pvs_check_for_imports];

            

            code = [code obj.user_imports];

            % declare variables for each input

            

            %inputs = get(obj.gui.function_inputs_control,'String');
@@ -88,6 +91,15 @@ classdef PVS_checker < handle 
            end

        end

        

        function [string] = user_imports(obj)

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

            string = [];

            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

        

        %% parse_pvs_result

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

            found = regexp(result,'\w+(?=[\.]{4,})|(?<=[\.]{4,})\w+','match')
@@ -315,9 +327,9 @@ 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.counter_examples) ' :size ' sprintf('%d',obj.counter_size) '))"  )' 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)

            fprintf(fileid,code);

            fclose(fileid);

        end