From ae3c731aba1ce1c6be6ae0fd687d85283307aba4 Mon Sep 17 00:00:00 2001 From: Colin Eles Date: Mon, 7 Mar 2011 21:54:24 +0000 Subject: [PATCH] found bug in parsing pvs result, updated proof script git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@7019 57e6efec-57d4-0310-aeb1-a6c144bb1a8b --- @CVC_checker/cvc_check.m | 6 +++--- @PVS_checker/generate_pvs_file.m | 18 +----------------- @PVS_checker/generate_pvs_script.m | 9 ++++++--- @PVS_checker/parse_pvs_result.m | 4 ++-- @PVS_checker/pvs_check.m | 6 ++++-- @PVS_checker/pvs_check_for_imports.m | 3 ++- 6 files changed, 18 insertions(+), 28 deletions(-) diff --git a/@CVC_checker/cvc_check.m b/@CVC_checker/cvc_check.m index 8dc62b8..55472cc 100644 --- a/@CVC_checker/cvc_check.m +++ b/@CVC_checker/cvc_check.m @@ -19,10 +19,10 @@ function [ check, seqs ] = cvc_check( object ) [filename, queries] = object.generate_file; waitbar(.10,box,'Running Proof'); - +tic % run the cvc command -[status, result] = system(['cvc3 ' filename ' +model']) - +[status, result] = system(['cvc3 ' filename ' +model']); +toc % check return status for errors if (status ~= 0) diff --git a/@PVS_checker/generate_pvs_file.m b/@PVS_checker/generate_pvs_file.m index 4434e4b..ddfbba5 100644 --- a/@PVS_checker/generate_pvs_file.m +++ b/@PVS_checker/generate_pvs_file.m @@ -130,23 +130,7 @@ end end code = [code sprintf('%s(%s):%s = \n',function_name,inputs_new,function_name_type)]; -%else - %inputs_new = []; - %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,1))) - % inputs_new = [inputs_new ',']; - % end - %end - %code = [code sprintf('%s(%s):%s = \n',function_name,inputs_new,function_name_type)]; - - %code = [code sprintf('%s(%s):real = \n',object.data.function_name,inputs_new)]; - - -%end + code = [code object.generate_pvs(object.data.Grid1,object.data.Grid2,0)]; code = [code sprintf('\nEND %s',function_name)]; fprintf(fileid,code); diff --git a/@PVS_checker/generate_pvs_script.m b/@PVS_checker/generate_pvs_script.m index 83d277a..589689d 100644 --- a/@PVS_checker/generate_pvs_script.m +++ b/@PVS_checker/generate_pvs_script.m @@ -9,10 +9,13 @@ % none % Author: Colin Eles elesc@mcmaster.ca % Organization: McMaster Centre for Software Certification -function [] = generate_pvs_script(object,filename) +function [] = generate_pvs_script(object,filename,sim_types) 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',object.data.settings.count) ' :size ' sprintf('%d',object.data.settings.range) '))" )' sprintf('\n')]; - +%if sim_types == 0 +code = ['(prove-tccs-pvs-file "' filename '" "(try (try (subtype-tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',object.data.settings.count) ' :size ' sprintf('%d',object.data.settings.range) '))" )' sprintf('\n')]; +%else +% code = ['(prove-tccs-pvs-file "' filename '" "(try (try (subtype-tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',object.data.settings.count) ' :size ' sprintf('%d',object.data.settings.range) '))" )' sprintf('\n')]; +%end fprintf(fileid,code); fclose(fileid); end diff --git a/@PVS_checker/parse_pvs_result.m b/@PVS_checker/parse_pvs_result.m index 2ef3994..c851be1 100644 --- a/@PVS_checker/parse_pvs_result.m +++ b/@PVS_checker/parse_pvs_result.m @@ -28,10 +28,10 @@ else % find the TCC that was unprovable search_str = sprintf('(?<=Proving formula %s[\\n]*)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)),char(found(i))); elseif strncmp(object.pvs_version,'PVS Version 4.2',15) - search_str = sprintf('(?<=Installing rewrite rule singleton_rew\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i))); + search_str = sprintf('(?<=Installing rewrite rule \\w+\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i))); end 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))); diff --git a/@PVS_checker/pvs_check.m b/@PVS_checker/pvs_check.m index f0aff8a..7852872 100644 --- a/@PVS_checker/pvs_check.m +++ b/@PVS_checker/pvs_check.m @@ -52,12 +52,14 @@ elseif (exists == 0 || strcmp(button,'Attempt to prove')) % generate the proof script - object.generate_pvs_script(function_name); + object.generate_pvs_script(function_name,1); waitbar(.10,box,'Running Proof'); %--------- % call pvs in batch mode with script % ADD check that pvs actually exists in system + tic [status, result] = system(['pvs -batch -v 3 -l ' function_name '.el']) + toc %objectect.msgbox_scroll(result); waitbar(.70,box,'Parsing Results'); [parsed error] = object.parse_pvs_result(result); @@ -76,7 +78,7 @@ elseif (exists == 0 || strcmp(button,'Attempt to prove')) end waitbar(.100,box,'Deleting Proof Script'); - delete([function_name '.el']); + %delete([function_name '.el']); delete(box); end diff --git a/@PVS_checker/pvs_check_for_imports.m b/@PVS_checker/pvs_check_for_imports.m index e5e2c3a..6e9e5c5 100644 --- a/@PVS_checker/pvs_check_for_imports.m +++ b/@PVS_checker/pvs_check_for_imports.m @@ -22,7 +22,8 @@ function string = pvs_check_for_imports(object) hashtable = {{'sqrt', 'reals@sqrt'} {'sin', 'trig@trig_basic'} {'cos', 'trig@trig_basic'} {'tan', 'trig@trig_basic'}}; for k=1:size(hashtable,2) - functions = regexp(object.data.function_inputs,hashtable{k}(1),'once') + + functions = regexp(char(object.data.function_inputs),hashtable{k}(1),'once') if ~isempty(functions{1}) if (~any(ismember(found,hashtable{k}(1)))) string = [string 'IMPORTING ' char(hashtable{k}(2)) sprintf('\n')]; -- GitLab