diff --git a/@EMLGenerator/EMLGenerator.m b/@EMLGenerator/EMLGenerator.m index c76e5c0fe2a349eb0d9406c4731d8ecf877fd839..40ec03ecb6ac7b931eb3605ec02cddce13ecbd1c 100644 --- a/@EMLGenerator/EMLGenerator.m +++ b/@EMLGenerator/EMLGenerator.m @@ -5,7 +5,7 @@ classdef EMLGenerator < handle properties data = []; datatype = []; - multi_output = 1; + multi_output = 0; end methods(Static) diff --git a/@EMLGenerator/parse_inputs.m b/@EMLGenerator/parse_inputs.m index c91e5649e7797b844d665840a070e25354907dd7..da89204d669583db519bea9a2eb55026afa86498 100644 --- a/@EMLGenerator/parse_inputs.m +++ b/@EMLGenerator/parse_inputs.m @@ -11,7 +11,7 @@ function revised_input = parse_inputs(input_string) revised_input = []; input_string2 = reshape(input_string',1,size(input_string,1)*size(input_string,2)); - inputs = regexprep(input_string2,'\s',''); + inputs = regexprep(input_string2,'\n',''); inputs = regexp(inputs,',','split'); % need to be careful here because pvs dependant types can have @@ -21,6 +21,7 @@ % variable any thing following is considered the type c_locations = regexp(inputs,':','start'); for i= 1:size(inputs,2) + sub_input = []; if size(c_locations{i},2) == 0 sub_input{1} = inputs{i}; new_inputs{i} = sub_input; @@ -36,6 +37,8 @@ %inputs = regexp(inputs,':','split') for i=1:size(new_inputs,2) + new_inputs{i}(1) = regexprep(new_inputs{i}(1),'\s',''); + valid = regexp(new_inputs{i}(1),'[a-zA-Z][_a-zA-Z0-9]*','match'); if isempty(char(new_inputs{i}(1))) || ~strcmp(new_inputs{i}(1),valid{1}) new_inputs{i}(2) = {'error'}; diff --git a/@GUI/GUI.m b/@GUI/GUI.m index b3cd76bffb3ae41ff456fc8251dc05b210944fe4..62b16f43fe2ca155d496d213f432bfd9ac891285 100644 --- a/@GUI/GUI.m +++ b/@GUI/GUI.m @@ -53,6 +53,7 @@ classdef GUI < handle EMLGen = []; TableBlk = []; saved = []; + validation_report_handle = []; end methods diff --git a/@GUI/close_fig.m b/@GUI/close_fig.m index 0372a78e4ca201c785614a128acb18aa9108f7cd..1f86ab92e15070371faf95bdb6adb9edfe3b48a6 100644 --- a/@GUI/close_fig.m +++ b/@GUI/close_fig.m @@ -8,12 +8,19 @@ % outputs: % none function [] = close_fig(object,src,event) - + if (object.validation_report_handle ~= 0) + delete(object.validation_report_handle) + end object.save_data; object.Data.open = 0; object.Data.fig = []; delete(object.fig); % remove reference to the old figure. object.fig = []; + % in simulink mode + if(object.mode == 1) + parent = get_param(object.block_handle,'Parent'); + open_system(parent); + end end diff --git a/@GUI/evaluate_counter_grid.m b/@GUI/evaluate_counter_grid.m index 7455817016cd60697f07db96fb5d5adccdef1f76..19cb3edf4f15db9ad3e66374f2e6e1e9ff339925 100644 --- a/@GUI/evaluate_counter_grid.m +++ b/@GUI/evaluate_counter_grid.m @@ -11,7 +11,12 @@ function problem = evaluate_counter_grid(object,grid,counter) % split the list of inputs to get inputs seperatly inputs = get(object.function_inputs_control,'String'); - inputs = regexp(inputs,',','split'); + inputs2 = []; + for i=1:size(inputs,1) + inputs2 = [inputs2 inputs(i,:)] + end + inputs2 = regexprep(inputs2,'\s',''); + inputs = regexp(inputs2,',','split'); check_string = []; % keep track of the number of condtitions that evaulate to true diff --git a/@GUI/pvs_ext_call.m b/@GUI/pvs_ext_call.m index e6d36cf03dcf5ab3ce2c848621260403935e10b1..3e9dca9a08248273450dbffff77ac5f60866b7f4 100644 --- a/@GUI/pvs_ext_call.m +++ b/@GUI/pvs_ext_call.m @@ -7,7 +7,11 @@ % outputs: % none function [] = pvs_ext_call(object,src,event) + object.save_call([],[]); object.save_data; + if (object.validation_report_handle ~= 0) + delete(object.validation_report_handle) + end error = object.check_call; object.PVS.output_type = object.output_data_type; object.PVS.input_type = object.input_data_type; diff --git a/@GUI/save_call.m b/@GUI/save_call.m index 5da402394e23a71af1745e416ba5c77658a09963..4b499dc1755922a4b43a77630fbacc9884c181aa 100644 --- a/@GUI/save_call.m +++ b/@GUI/save_call.m @@ -11,7 +11,7 @@ % outputs: % none function eml_handle = save_call(object,src,event) - multi_type = 1; + multi_type = 0; if(object.check_call([],[]) == 1) return; end diff --git a/@PVS_checker/generate_pvs_file.m b/@PVS_checker/generate_pvs_file.m index c39624b91f91c6d25416d55071b8dc81cc3fd310..830628c12e9189e21568888faf0729991483c8d7 100644 --- a/@PVS_checker/generate_pvs_file.m +++ b/@PVS_checker/generate_pvs_file.m @@ -15,12 +15,15 @@ function_names = EMLGenerator.parse_inputs(object.data.function_name); function_name = char(function_names{1}(1)); + if (size(function_names{1},2) == 2) function_name_type = char(function_names{1}(2)); - + else + function_name_type = 'real'; + end fileid = fopen([filename '.pvs'],'w'); code = []; code = sprintf('%s:THEORY\nBEGIN\n',function_name); - code = [code sprintf('IMPORTING Funcs\n')]; + %code = [code sprintf('IMPORTING Funcs\n')]; code = [code object.pvs_check_for_imports]; code = [code object.user_imports]; @@ -59,7 +62,9 @@ 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)]; + + %code = [code sprintf('%s(%s):real = \n',object.data.function_name,inputs_new)]; end diff --git a/@ValidationReport/close_req_call.m b/@ValidationReport/close_req_call.m index 91d38591570a50bd0f57c7ffbf091d5950567aef..e01089d8d0335d9f74c21f784f455e6374fa16bd 100644 --- a/@ValidationReport/close_req_call.m +++ b/@ValidationReport/close_req_call.m @@ -9,7 +9,10 @@ % outputs: % none function [] = close_req_call(object,src,event) - object.gui.check_call([],[]); + if (object.gui.Data.open) + object.gui.check_call([],[]); + end + object.gui.validation_report_handle = 0; delete(object.fig); end diff --git a/@ValidationReport/init.m b/@ValidationReport/init.m index 5633ef4ad830b5566bfc955d9bf5667d888a675f..b4c16cc8782c2e85235e798ae813f3a38d7fa294 100644 --- a/@ValidationReport/init.m +++ b/@ValidationReport/init.m @@ -114,6 +114,7 @@ object.position; object.populate; + object.gui.validation_report_handle = object.fig; end end