Loading GUI.m +177 −60 Original line number Diff line number Diff line Loading @@ -58,13 +58,21 @@ classdef GUI < handle % constructor % inputs: % h:double - handle to Tabular block in model % mode:boolean - the mode of the gui, 1 for simuink, 0 for matlab % outputs; % obj:GUI - object that is created % object:GUI - object that is created function object = GUI(h,mode) object.block_handle = h; object.mode = mode; end %% setData % set the gui data object based on inputed data structure % inputs: % obj:GUI - GUI object % Data:Data - Data object % outputs; % object:GUI - object that is created function [] = setData(object,Data) object.Data = Data; object.Grid0 = Data.Grid0; Loading Loading @@ -285,12 +293,28 @@ classdef GUI < handle end end %% %% new_call % callback for new button % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = new_call(object,src,event) TableToolMatlab end %% pvs_file_call % callback for the generate pvs file button, generates a pvs file % for the table, does not attempt to prove, overwrites. % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = pvs_file_call(object,src,event) object.save_data object.PVS.generate_pvs_file(object.Data.function_name); Loading @@ -298,7 +322,17 @@ classdef GUI < handle end %% %% prf_file_call % callback for the check status menu option, this function will % check the current status of the table, if the table has been % proven it will alert the user and update the status, if it has % not been proven it will alert the user. % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = prf_file_call(object,src,event) object.save_data; % check if a pvs file exists Loading Loading @@ -334,8 +368,6 @@ classdef GUI < handle delete([temp_pvs '.pvs']); status = object.PVS.check_status; if (status ~= object.pvs_checked) Loading @@ -352,19 +384,18 @@ classdef GUI < handle else msgbox('Table has not been proven'); end % [FileName, PathName, FilterIndex] = uigetfile('*.prf','Select prf file'); % if ~isempty(FileName) % data = textread([PathName FileName], '%s', 'whitespace', '', 'bufsize', 268435456); % %data_one = regexprep(data,'\n',''); % string = data{1}; % [theory_name, decls] = PVS_checker.parse_prf_file(string); % % % % end end %% %% open_call % callback for the open option, will show a file picker and % attempt to load the file into a new window. % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = open_call(object,src,event) [FileName, PathName, FilterIndex] = uigetfile('*.table','Select pvs files'); if ~isempty(FileName) Loading Loading @@ -450,8 +481,18 @@ classdef GUI < handle fclose(fileid); end %% %% input_call % function will open up the ports and data management window if % in simulink mode. % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = input_call(object,src,event) % make sure in simulink mode. if object.mode == 1 eml_handle = object.save_call([],[]); currentDir = pwd; cd([matlabroot filesep 'toolbox' filesep 'stateflow' filesep 'stateflow' filesep 'private']); Loading @@ -459,13 +500,29 @@ classdef GUI < handle cd(currentDir); fHandle('edit_data_ports', sf('get', get_param(char(eml_handle),'UserData'), '.chart')) end end %% %% input_call % open up the settings window % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = settings_call(object,src,event) object.settings.show; end %% pvs_ext_call % function will initiate the typechecking procedure for the table % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = pvs_ext_call(object,src,event) object.save_data; error = object.check_call; Loading @@ -489,9 +546,16 @@ classdef GUI < handle end %% output_data_type % this function will determine what the desired output type of % the function is, based on what the user has selected using the % ports and datamanagement window. if the user has selected an % unconvertable type, (inheret, fixed pt. etc.) it will return % the empty string % inputs: % object:GUI - GUI objecto % outputs; % type:string - string representation of the output type. function type = output_data_type(object) if (object.mode == 1) S = sfroot; Loading Loading @@ -815,12 +879,20 @@ classdef GUI < handle function [] = close_fig(object,src,event) object.save_data; object.Data.open = 0; object.Data.fig = []; delete(object.fig); % remove reference to the old figure. object.fig = []; end %% %% save_data % save the current state of the table to the data object so that % it can be saved either in a block or in a binary file % inputs: % object:GUI - current GUI object % outputs; % none function [] = save_data(object) save_conditions(object,object.Grid2); save_conditions(object,object.Grid1); Loading @@ -832,8 +904,8 @@ classdef GUI < handle object.Data.function_name = get(object.function_name_control,'String'); object.Data.function_inputs = get(object.function_inputs_control,'String'); object.Data.checked = object.pvs_checked; object.Data.open = 0; object.Data.fig = []; %object.Data.open = 0; %object.Data.fig = []; set.set = 1; set.inputs = object.settings.pvs_includes; Loading @@ -842,7 +914,12 @@ classdef GUI < handle object.Data.settings = set; end %% %% save_settings % save just the settings to the data object % inputs: % object:GUI - current GUI object % outputs; % none function [] = save_settings(object) set.set = 1; set.inputs = object.settings.pvs_includes; Loading Loading @@ -1187,6 +1264,14 @@ classdef GUI < handle end %% evaluate_counter % function will call the evaluation function for a given counter % example. % inputs: % object:GUI - current GUI object % counter:string - string representing the counter example, ie. % 'x = 3\ny = 5' % outputs; % none function [] = evaluate_counter(object,counter) problem = object.evaluate_counter_grid(object.Grid2, counter); Loading @@ -1196,7 +1281,15 @@ classdef GUI < handle end %% evaluate_counter_grid % counter has form 'x=0\ny=2' % function will evaluate a counter example for a given grid. % inputs: % object:GUI - current GUI object % grid:Grid - the grid to evaluate % counter:string - string representing the counter example, ie. % 'x = 3\ny = 5' % outputs; % problem:boolean - 1 if grid has overlapping or underspecified % cells, 0 if not. function problem = evaluate_counter_grid(object,grid,counter) % split the list of inputs to get inputs seperatly inputs = get(object.function_inputs_control,'String'); Loading Loading @@ -1296,16 +1389,24 @@ classdef GUI < handle 'KeyPressFcn',@(src,event)textbox_callback(object,src,event),... 'fontsize',11); end %% %% textbox_callback % callback for when the text of a callback is changed. % inputs: % object - current GUI object % src - source of the callback calling % event - event that triggered the callback % outputs; % none function [] = textbox_callback(object,src,event) % make sure the character pressed isn't empty if(~isempty(unicode2native(event.Character))) % make sure the character is a printable character if event.Character > 33 || event.Character == 8 if object.pvs_checked == 1 object.pvs_checked = 0; object.update_Statusbar if (object.mode == 1) TableBlock.set_block_display(object.block_handle,object.pvs_checked); end end Loading @@ -1315,9 +1416,13 @@ classdef GUI < handle end %% check_inputs % ensure that the inputs are proper variable names, and that the % input string parses properly % inputs: % object:GUI - current GUI object % outputs; % error:string - error string if variable is not inputed properly function error = check_inputs(object) parsed_input = EMLGenerator.parse_inputs(get(object.function_inputs_control,'string')); error = []; Loading @@ -1330,6 +1435,13 @@ classdef GUI < handle end end %% setBPenable % enable or diable the delete cell buttons based on the size of % a grid, so that you can't delete below one cell. % inputs: % object:GUI - current GUI object % outputs; % none function [] = setPBenable(object) if size(object.Grid1.cells,2) > 1 set(object.Grid1.delete_cell_pb,'Enable','on'); Loading @@ -1348,6 +1460,11 @@ classdef GUI < handle methods(Static) %% msgbox_scroll % create a message box with a scrollable text area % inputs: % msg:string - string to put into the message box % outputs; % none function [] = msgbox_scroll(msg) fig = figure('units','pixels',... 'position',[0 0 700 500],... Loading PVS_checker.m +2 −1 Original line number Diff line number Diff line Loading @@ -395,7 +395,8 @@ classdef PVS_checker < handle [parsed error] = object.parse_pvs_result(result); if (error == 1) msgbox(result); err_str = ['There was an error proving tabular expression ' sprintf('\n\n') 'Error string below:' sprintf('\n\n') result]; GUI.msgbox_scroll(err_str); else if (isempty(parsed)) Loading Loading
GUI.m +177 −60 Original line number Diff line number Diff line Loading @@ -58,13 +58,21 @@ classdef GUI < handle % constructor % inputs: % h:double - handle to Tabular block in model % mode:boolean - the mode of the gui, 1 for simuink, 0 for matlab % outputs; % obj:GUI - object that is created % object:GUI - object that is created function object = GUI(h,mode) object.block_handle = h; object.mode = mode; end %% setData % set the gui data object based on inputed data structure % inputs: % obj:GUI - GUI object % Data:Data - Data object % outputs; % object:GUI - object that is created function [] = setData(object,Data) object.Data = Data; object.Grid0 = Data.Grid0; Loading Loading @@ -285,12 +293,28 @@ classdef GUI < handle end end %% %% new_call % callback for new button % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = new_call(object,src,event) TableToolMatlab end %% pvs_file_call % callback for the generate pvs file button, generates a pvs file % for the table, does not attempt to prove, overwrites. % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = pvs_file_call(object,src,event) object.save_data object.PVS.generate_pvs_file(object.Data.function_name); Loading @@ -298,7 +322,17 @@ classdef GUI < handle end %% %% prf_file_call % callback for the check status menu option, this function will % check the current status of the table, if the table has been % proven it will alert the user and update the status, if it has % not been proven it will alert the user. % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = prf_file_call(object,src,event) object.save_data; % check if a pvs file exists Loading Loading @@ -334,8 +368,6 @@ classdef GUI < handle delete([temp_pvs '.pvs']); status = object.PVS.check_status; if (status ~= object.pvs_checked) Loading @@ -352,19 +384,18 @@ classdef GUI < handle else msgbox('Table has not been proven'); end % [FileName, PathName, FilterIndex] = uigetfile('*.prf','Select prf file'); % if ~isempty(FileName) % data = textread([PathName FileName], '%s', 'whitespace', '', 'bufsize', 268435456); % %data_one = regexprep(data,'\n',''); % string = data{1}; % [theory_name, decls] = PVS_checker.parse_prf_file(string); % % % % end end %% %% open_call % callback for the open option, will show a file picker and % attempt to load the file into a new window. % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = open_call(object,src,event) [FileName, PathName, FilterIndex] = uigetfile('*.table','Select pvs files'); if ~isempty(FileName) Loading Loading @@ -450,8 +481,18 @@ classdef GUI < handle fclose(fileid); end %% %% input_call % function will open up the ports and data management window if % in simulink mode. % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = input_call(object,src,event) % make sure in simulink mode. if object.mode == 1 eml_handle = object.save_call([],[]); currentDir = pwd; cd([matlabroot filesep 'toolbox' filesep 'stateflow' filesep 'stateflow' filesep 'private']); Loading @@ -459,13 +500,29 @@ classdef GUI < handle cd(currentDir); fHandle('edit_data_ports', sf('get', get_param(char(eml_handle),'UserData'), '.chart')) end end %% %% input_call % open up the settings window % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = settings_call(object,src,event) object.settings.show; end %% pvs_ext_call % function will initiate the typechecking procedure for the table % inputs: % obj:GUI - GUI objecto % src:double - source of the callback calling % event:eventdata - event that triggered the callback % outputs; % none function [] = pvs_ext_call(object,src,event) object.save_data; error = object.check_call; Loading @@ -489,9 +546,16 @@ classdef GUI < handle end %% output_data_type % this function will determine what the desired output type of % the function is, based on what the user has selected using the % ports and datamanagement window. if the user has selected an % unconvertable type, (inheret, fixed pt. etc.) it will return % the empty string % inputs: % object:GUI - GUI objecto % outputs; % type:string - string representation of the output type. function type = output_data_type(object) if (object.mode == 1) S = sfroot; Loading Loading @@ -815,12 +879,20 @@ classdef GUI < handle function [] = close_fig(object,src,event) object.save_data; object.Data.open = 0; object.Data.fig = []; delete(object.fig); % remove reference to the old figure. object.fig = []; end %% %% save_data % save the current state of the table to the data object so that % it can be saved either in a block or in a binary file % inputs: % object:GUI - current GUI object % outputs; % none function [] = save_data(object) save_conditions(object,object.Grid2); save_conditions(object,object.Grid1); Loading @@ -832,8 +904,8 @@ classdef GUI < handle object.Data.function_name = get(object.function_name_control,'String'); object.Data.function_inputs = get(object.function_inputs_control,'String'); object.Data.checked = object.pvs_checked; object.Data.open = 0; object.Data.fig = []; %object.Data.open = 0; %object.Data.fig = []; set.set = 1; set.inputs = object.settings.pvs_includes; Loading @@ -842,7 +914,12 @@ classdef GUI < handle object.Data.settings = set; end %% %% save_settings % save just the settings to the data object % inputs: % object:GUI - current GUI object % outputs; % none function [] = save_settings(object) set.set = 1; set.inputs = object.settings.pvs_includes; Loading Loading @@ -1187,6 +1264,14 @@ classdef GUI < handle end %% evaluate_counter % function will call the evaluation function for a given counter % example. % inputs: % object:GUI - current GUI object % counter:string - string representing the counter example, ie. % 'x = 3\ny = 5' % outputs; % none function [] = evaluate_counter(object,counter) problem = object.evaluate_counter_grid(object.Grid2, counter); Loading @@ -1196,7 +1281,15 @@ classdef GUI < handle end %% evaluate_counter_grid % counter has form 'x=0\ny=2' % function will evaluate a counter example for a given grid. % inputs: % object:GUI - current GUI object % grid:Grid - the grid to evaluate % counter:string - string representing the counter example, ie. % 'x = 3\ny = 5' % outputs; % problem:boolean - 1 if grid has overlapping or underspecified % cells, 0 if not. function problem = evaluate_counter_grid(object,grid,counter) % split the list of inputs to get inputs seperatly inputs = get(object.function_inputs_control,'String'); Loading Loading @@ -1296,16 +1389,24 @@ classdef GUI < handle 'KeyPressFcn',@(src,event)textbox_callback(object,src,event),... 'fontsize',11); end %% %% textbox_callback % callback for when the text of a callback is changed. % inputs: % object - current GUI object % src - source of the callback calling % event - event that triggered the callback % outputs; % none function [] = textbox_callback(object,src,event) % make sure the character pressed isn't empty if(~isempty(unicode2native(event.Character))) % make sure the character is a printable character if event.Character > 33 || event.Character == 8 if object.pvs_checked == 1 object.pvs_checked = 0; object.update_Statusbar if (object.mode == 1) TableBlock.set_block_display(object.block_handle,object.pvs_checked); end end Loading @@ -1315,9 +1416,13 @@ classdef GUI < handle end %% check_inputs % ensure that the inputs are proper variable names, and that the % input string parses properly % inputs: % object:GUI - current GUI object % outputs; % error:string - error string if variable is not inputed properly function error = check_inputs(object) parsed_input = EMLGenerator.parse_inputs(get(object.function_inputs_control,'string')); error = []; Loading @@ -1330,6 +1435,13 @@ classdef GUI < handle end end %% setBPenable % enable or diable the delete cell buttons based on the size of % a grid, so that you can't delete below one cell. % inputs: % object:GUI - current GUI object % outputs; % none function [] = setPBenable(object) if size(object.Grid1.cells,2) > 1 set(object.Grid1.delete_cell_pb,'Enable','on'); Loading @@ -1348,6 +1460,11 @@ classdef GUI < handle methods(Static) %% msgbox_scroll % create a message box with a scrollable text area % inputs: % msg:string - string to put into the message box % outputs; % none function [] = msgbox_scroll(msg) fig = figure('units','pixels',... 'position',[0 0 700 500],... Loading
PVS_checker.m +2 −1 Original line number Diff line number Diff line Loading @@ -395,7 +395,8 @@ classdef PVS_checker < handle [parsed error] = object.parse_pvs_result(result); if (error == 1) msgbox(result); err_str = ['There was an error proving tabular expression ' sprintf('\n\n') 'Error string below:' sprintf('\n\n') result]; GUI.msgbox_scroll(err_str); else if (isempty(parsed)) Loading