diff --git a/@CVC_checker/generate_file.m b/@CVC_checker/generate_file.m index d05e555a22117f866f811aaf8699ddc1b86dee55..59e0edad57a28c50144f07b474bf4d9694663454 100644 --- a/@CVC_checker/generate_file.m +++ b/@CVC_checker/generate_file.m @@ -10,16 +10,25 @@ code = []; % output the input variables inputs = EMLGenerator.parse_inputs(object.data.function_inputs); for i = 1:size(inputs,2) - code = [code char(inputs{i}(1)) ':INT;' char(10)]; + code = [code char(inputs{i}(1)) ':REAL;' char(10)]; end % call the recursive function to generate the queries -%generate grid 1 -[new_code,queries] = CVC_checker.generate_cvc_grid(object.data.Grid2,0); +%generate grid 2 +if size(object.data.Grid2.cells,2) > 1 + [new_code,queries] = CVC_checker.generate_cvc_grid(object.data.Grid2,0); +end code = [code new_code]; +if size(object.data.Grid1.cells,2) > 1 + [new_code,new_queries] = CVC_checker.generate_cvc_grid(object.data.Grid1,size(queries,2)); + queries = [queries new_queries] + code = [code new_code]; + +end + % generate grid 2 diff --git a/@GUI/check_call.m b/@GUI/check_call.m index 08c4f0e78015da03d63f71bc4162bf84d089d757..8e2c2c151f43862fa8e64bad196314792c52e1c1 100644 --- a/@GUI/check_call.m +++ b/@GUI/check_call.m @@ -26,7 +26,10 @@ else end if ~isempty(msg) - msgbox(msg); + + if isempty(event) + msgbox(msg); + end error = 1; end diff --git a/@GUI/cvc_ext_call.m b/@GUI/cvc_ext_call.m new file mode 100644 index 0000000000000000000000000000000000000000..57b539d62ed917aba4bd81f477b60f9301eb1ea3 --- /dev/null +++ b/@GUI/cvc_ext_call.m @@ -0,0 +1,37 @@ +function [] = cvc_ext_call( object,src,event ) +%CVC_EXT_CALL Summary of this function goes here +% Detailed explanation goes here + + +object.save_call([],[]); +object.save_data; +if (object.validation_report_handle ~= 0) + delete(object.validation_report_handle); +end +error = object.check_call([],2); + + +if (~error) + + [check,result] = object.CVC.cvc_check; + + if (check == 1) + msgbox('table is valid'); + elseif (check == 0 && strcmp(result,'canceled')) + return; + else + Valid_Report = ValidationReport(object); + Valid_Report.set_results(result); + Valid_Report.init(); + end + object.pvs_checked = check; + object.update_Statusbar; + if (object.mode == 1) + + TableBlock.set_block_display(object.block_handle,object.pvs_checked); + end + +end +end + + diff --git a/@GUI/pvs_ext_call.m b/@GUI/pvs_ext_call.m index 5cb159429a2f705915332b21a2cb2b2fa70a3f67..b762b40e8afc50bbf464fa22ee34519926d51f97 100644 --- a/@GUI/pvs_ext_call.m +++ b/@GUI/pvs_ext_call.m @@ -14,7 +14,7 @@ object.save_data; if (object.validation_report_handle ~= 0) delete(object.validation_report_handle); end -error = object.check_call; +error = object.check_call([],2); if(object.multi_mode == 0) object.PVS.output_type = object.output_data_type; @@ -22,7 +22,6 @@ if(object.multi_mode == 0) object.PVS.input_type = object.input_data_type; - end object.PVS.type_mode = 0;