diff --git a/@CVC_checker/cvc_check.m b/@CVC_checker/cvc_check.m index c13462e2c10bda072ff290a7fd6723960b49eb9d..8dc62b8b46d5d770b6b51522dbe2912f04eee48f 100644 --- a/@CVC_checker/cvc_check.m +++ b/@CVC_checker/cvc_check.m @@ -21,7 +21,7 @@ function [ check, seqs ] = cvc_check( object ) waitbar(.10,box,'Running Proof'); % run the cvc command -[status, result] = system(['cvc3 ' filename ' +model']); +[status, result] = system(['cvc3 ' filename ' +model']) % check return status for errors if (status ~= 0) diff --git a/@PVS_checker/pvs_check.m b/@PVS_checker/pvs_check.m index 13db80a4a35919af0da182dc2af290eff5f0e21a..f0aff8a3c1487dfb51cd51025edcc5e61c4b8708 100644 --- a/@PVS_checker/pvs_check.m +++ b/@PVS_checker/pvs_check.m @@ -42,7 +42,7 @@ if (exists == 1 && (isempty(button) || strcmp(button,'Cancel'))) output = 'canceled'; return; elseif (exists == 1 && (strcmp(button,'Open PVS'))); - [status, result] = system(['pvs ' 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'); diff --git a/@PVS_checker/pvs_check_for_imports.m b/@PVS_checker/pvs_check_for_imports.m index 7db9fa7a6b99b0bfe987238e7aaafafbfcc633cf..e5e2c3a468ee9d8e1dd871c1afac6ac157a35a9d 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) - if ~isempty(regexp(object.data.function_inputs,hashtable{k}(1),'once')) + functions = regexp(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')]; found = [found hashtable{k}(1)]; diff --git a/@Settings/init.m b/@Settings/init.m index c2333b017f6c2281727f88a523763ccf4a23eaea..867e03af2eca132821e23ebd29413f760a593c07 100644 --- a/@Settings/init.m +++ b/@Settings/init.m @@ -11,6 +11,6 @@ function [] = init(object) object.pvs_includes = []; object.counter_trials = 1000; object.counter_range = 100; -object.exception = 0; +object.except = 0; end diff --git a/@Settings/setvalues.m b/@Settings/setvalues.m index 6072fb43bd68fa4e061c93bd4877d3fd16a52b54..7e5a7550cd8b8089c4e44bc0b22efa77ac5be67d 100644 --- a/@Settings/setvalues.m +++ b/@Settings/setvalues.m @@ -15,7 +15,6 @@ object.counter_range = settings.range; if ~isfield(settings,'except') settings.except = 0; end -%object.except = settings.except; -object.except = 1; +object.except = settings.except; end