diff --git a/GUI.m b/GUI.m index 07f4b6277d94dc1611a922913f607cf8097f8613..565266943fd79740b3d0a0fed67f45ad2099f56f 100644 --- a/GUI.m +++ b/GUI.m @@ -242,7 +242,7 @@ classdef GUI < handle obj.update_Statusbar; - obj.PVS = PVS_checker(obj,obj.settings); + obj.PVS = PVS_checker(obj.Data); obj.initialized = 1; obj.Data.open = 1; @@ -253,6 +253,7 @@ classdef GUI < handle function [] = set_block_display(object) + if (object.mode == 1) %if object.pvs_checked == 1 mask_string = []; code_block = sprintf('%s/code',getfullname(object.block_handle)); @@ -268,7 +269,7 @@ classdef GUI < handle end set_param(getfullname(object.block_handle),'MaskDisplay',mask_string); - %end + end end @@ -396,11 +397,17 @@ classdef GUI < handle end %% pvs_ext_call function [] = pvs_ext_call(object,src,event) + object.save_data; error = object.check_call; + if (~error) - check = object.PVS.pvs_check; + [check,result] = object.PVS.pvs_check; if (check == 1) msgbox('table is valid') + else + Valid_Report = ValidationReport(object); + Valid_Report.set_results(result); + Valid_Report.init(); end object.pvs_checked = check; object.update_Statusbar; @@ -1818,8 +1825,12 @@ classdef GUI < handle %% function [] = textbox_callback(object,src,event) + if object.pvs_checked == 1 object.pvs_checked = 0; object.update_Statusbar + object.set_block_display; + end + end %% clone diff --git a/PVS_checker.m b/PVS_checker.m index 82170409a0fa13baa45b39bb884e03dc39608ae4..a9aa41bd55c4cb993126322b9203712990bdae24 100644 --- a/PVS_checker.m +++ b/PVS_checker.m @@ -3,29 +3,30 @@ classdef PVS_checker < handle % prover properties - gui = []; counter_examples = 10000; counter_size = 100; default_type = 'real'; pvs_version = 4.2; - settings + + data = []; + mode = []; % 0 - graphical, 1 - command end methods %% constructor - function obj = PVS_checker(gui_new,settings) - obj.gui = gui_new; - obj.settings = settings; + function obj = PVS_checker(data) + obj.data = data; end %% pvs_ext_call - function check = pvs_check(obj) + function [check,output] = pvs_check(obj) check = 0; + output = []; % file name will be expression_name.m - fileid = fopen([get(obj.gui.function_name_control,'String') '.pvs'],'w'); + fileid = fopen([obj.data.function_name '.pvs'],'w'); code = []; - code = sprintf('%s:THEORY\nBEGIN\n',get(obj.gui.function_name_control,'String')); + code = sprintf('%s:THEORY\nBEGIN\n',obj.data.function_name); code = [code obj.pvs_check_for_imports]; @@ -34,7 +35,7 @@ classdef PVS_checker < handle %inputs = get(obj.gui.function_inputs_control,'String'); %inputs = regexp(inputs,',','split'); - parsed_inputs = obj.gui.parse_inputs(get(obj.gui.function_inputs_control,'string')); + parsed_inputs = obj.parse_inputs(obj.data.function_inputs); % initialize inputs to zero % functions are assumed to be total, so 0 is just for @@ -56,26 +57,26 @@ classdef PVS_checker < handle end end - code = [code sprintf('%s(%s):real = \n',get(obj.gui.function_name_control,'String'),inputs_new)]; - code = [code obj.generate_pvs(obj.gui.Grid1,obj.gui.Grid2,0)]; - code = [code sprintf('\nEND %s',get(obj.gui.function_name_control,'String'))]; + code = [code sprintf('%s(%s):real = \n',obj.data.function_name,inputs_new)]; + code = [code obj.generate_pvs(obj.data.Grid1,obj.data.Grid2,0)]; + code = [code sprintf('\nEND %s',obj.data.function_name)]; fprintf(fileid,code); fclose(fileid); % generate the proof script - obj.generate_pvs_script(get(obj.gui.function_name_control,'String')) + obj.generate_pvs_script(obj.data.function_name) % THIS SECTION NEEDS SOME WORK %------------- % delete the existing proof - delete([get(obj.gui.function_name_control,'String') '.prf']) + delete([obj.data.function_name '.prf']) %--------- % call pvs in batch mode with script % ADD check that pvs actually exists in system - [status, result] = system(['pvs -batch -v 3 -l ' get(obj.gui.function_name_control,'String') '.el']) + [status, result] = system(['pvs -batch -v 3 -l ' obj.data.function_name '.el']) %object.msgbox_scroll(result); [parsed error] = obj.parse_pvs_result(result); if (error == 1) @@ -84,18 +85,60 @@ classdef PVS_checker < handle if (isempty(parsed)) check = 1; + output = []; else - Valid_Report = ValidationReport(obj.gui); - Valid_Report.set_results(parsed); - Valid_Report.init(); + output = parsed; + %Valid_Report = ValidationReport(obj.gui); + %Valid_Report.set_results(parsed); + %Valid_Report.init(); end end end + function revised_input = parse_inputs(obj,input_string) + revised_input = []; + input_string2 = reshape(input_string',1,size(input_string,1)*size(input_string,2)); + inputs = regexprep(input_string2,'\s',''); + 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) + 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 = new_inputs; + end + end + function [string] = user_imports(obj) string = []; - if ~isempty(obj.settings.pvs_includes) - files = regexp(obj.settings.pvs_includes,',','split'); + if ~isempty(obj.data.settings.inputs) + files = regexp(obj.data.settings.inputs,',','split'); for i=1:size(files,2) file_no_ext = regexp(files{i},'\w*(?=\.\w*)','match'); @@ -176,7 +219,7 @@ classdef PVS_checker < handle continue end code = [code sprintf('%s->',obj.matlab_to_pvs_syntax_translation(strtrim(char(get(g1.cells(i).cond,'String')))))]; - resultcell = obj.gui.Grid0.search_return(g1.cells(i),g2_cell); + resultcell = obj.data.Grid0.search_return(g1.cells(i),g2_cell); if(~isempty(resultcell)) code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String'))))]; @@ -193,7 +236,7 @@ classdef PVS_checker < handle end end if(~isempty(elsecell)) - resultcell = obj.gui.Grid0.search_return(elsecell,g2_cell); + resultcell = obj.data.Grid0.search_return(elsecell,g2_cell); code = [code sprintf('ELSE->%s\n',obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String')))))]; end @@ -237,7 +280,7 @@ classdef PVS_checker < handle code = [code obj.generate_pvs_horizontal(g1,g2.cells(i),depth)]; else - resultcell = obj.gui.Grid0.search_return(g1.cells(1),g2.cells(i)); + resultcell = obj.data.Grid0.search_return(g1.cells(1),g2.cells(i)); if(~isempty(resultcell)) code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String'))))]; @@ -270,7 +313,7 @@ classdef PVS_checker < handle code = [code obj.generate_pvs_horizontal(g1,elsecell,depth) sprintf('\n')]; else - resultcell = obj.gui.Grid0.search_return(g1.cells(1),elsecell); + resultcell = obj.data.Grid0.search_return(g1.cells(1),elsecell); if(~isempty(resultcell)) code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String')))) sprintf('\n')]; @@ -293,8 +336,8 @@ classdef PVS_checker < handle %% pvs_check_for_imports function string = pvs_check_for_imports(obj) - [string,found] = obj.pvs_check_for_imports_g(obj.gui.Grid2,{}); - [string2,found2] = obj.pvs_check_for_imports_g(obj.gui.Grid1,found); + [string,found] = obj.pvs_check_for_imports_g(obj.data.Grid2,{}); + [string2,found2] = obj.pvs_check_for_imports_g(obj.data.Grid1,found); string = [string string2]; end @@ -330,7 +373,7 @@ 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.settings.counter_trials) ' :size ' sprintf('%d',obj.settings.counter_range) '))" )' sprintf('\n')]; + code = ['(prove-tccs-pvs-file "' filename '" "(try (try (tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',obj.data.settings.count) ' :size ' sprintf('%d',obj.data.settings.range) '))" )' sprintf('\n')]; fprintf(fileid,code); fclose(fileid); diff --git a/ValidationReport.m b/ValidationReport.m index 7727fa79cbf426bcf8450670a6bf66cc3af09a98..24385b530267865f34cd5f70eb69bcd7c83de5fd 100644 --- a/ValidationReport.m +++ b/ValidationReport.m @@ -48,7 +48,6 @@ classdef ValidationReport < handle function [] = init(obj) if size(obj.PVS_results,2) == 0 - msgbox('table is proper') else