Skip to content
...@@ -16,6 +16,14 @@ for i = 1:size(grid.cells,2) ...@@ -16,6 +16,14 @@ for i = 1:size(grid.cells,2)
error = ''; error = '';
string = get(grid.cells(i).cond,'String'); string = get(grid.cells(i).cond,'String');
if size(string) > 0
s = [string(1,:)];
for j = 2:size(string,1)
s = [s ' ' string(j,:)];
end
string = s;
end
if ( strcmp(string,'') || isempty(string)) && i == 1 && isempty(grid.parent_grid) && size(grid.cells,2) == 1 if ( strcmp(string,'') || isempty(string)) && i == 1 && isempty(grid.parent_grid) && size(grid.cells,2) == 1
break; break;
...@@ -40,7 +48,7 @@ for i = 1:size(grid.cells,2) ...@@ -40,7 +48,7 @@ for i = 1:size(grid.cells,2)
msg = [msg error sprintf('\n')]; msg = [msg error sprintf('\n')];
% set tooltip string of cell to error msg % set tooltip string of cell to error msg
set(grid.cells(i).cond,'TooltipString',error) set(grid.cells(i).cond,'TooltipString',error);
% change background colour % change background colour
grid.cells(i).flag_cell(1); grid.cells(i).flag_cell(1);
else else
......
...@@ -28,6 +28,7 @@ for i=1:size(parsed_input,2) ...@@ -28,6 +28,7 @@ for i=1:size(parsed_input,2)
end end
if ~result if ~result
% the string is a condition we need to evaulate it as it % the string is a condition we need to evaulate it as it
% will be used in the code, as in order for an if statement % will be used in the code, as in order for an if statement
......
...@@ -11,7 +11,8 @@ ...@@ -11,7 +11,8 @@
% Organization: McMaster Centre for Software Certification % Organization: McMaster Centre for Software Certification
function [] = close_fig(object,src,event) function [] = close_fig(object,src,event)
if (object.validation_report_handle ~= 0) if (object.validation_report_handle ~= 0)
delete(object.validation_report_handle) delete(object.validation_report_handle);
object.validation_report_handle = 0;
end end
object.save_data; object.save_data;
object.Data.open = 0; object.Data.open = 0;
...@@ -19,6 +20,8 @@ object.Data.fig = []; ...@@ -19,6 +20,8 @@ object.Data.fig = [];
delete(object.fig); delete(object.fig);
% remove reference to the old figure. % remove reference to the old figure.
object.fig = []; object.fig = [];
% Purge unnecessary information from Data
object.Data.purge;
% in simulink mode % in simulink mode
if(object.mode == 1) if(object.mode == 1)
parent = get_param(object.block_handle,'Parent'); parent = get_param(object.block_handle,'Parent');
......
...@@ -19,7 +19,6 @@ control = uicontrol('style','edit',... ...@@ -19,7 +19,6 @@ control = uicontrol('style','edit',...
'min',0,'max',1,... % This is the key to multiline edits. 'min',0,'max',1,... % This is the key to multiline edits.
'string',{''},... 'string',{''},...
'Max',2.0,... 'Max',2.0,...
'Clipping','on',...
'fontweight','bold',... 'fontweight','bold',...
'BackgroundColor',[1 1 1],... 'BackgroundColor',[1 1 1],...
'horizontalalign','center',... 'horizontalalign','center',...
......
...@@ -7,6 +7,7 @@ object.save_call([],[]); ...@@ -7,6 +7,7 @@ object.save_call([],[]);
object.save_data; object.save_data;
if (object.validation_report_handle ~= 0) if (object.validation_report_handle ~= 0)
delete(object.validation_report_handle); delete(object.validation_report_handle);
object.validation_report_handle = 0;
end end
error = object.check_call([],2); error = object.check_call([],2);
...@@ -22,6 +23,7 @@ if (~error) ...@@ -22,6 +23,7 @@ if (~error)
else else
Valid_Report = ValidationReport(object); Valid_Report = ValidationReport(object);
Valid_Report.set_results(result); Valid_Report.set_results(result);
Valid_Report.set_mode(1);
Valid_Report.init(); Valid_Report.init();
end end
object.pvs_checked = check; object.pvs_checked = check;
......
...@@ -2,8 +2,8 @@ ...@@ -2,8 +2,8 @@
% function will call the draw methods for each of the 3 grids. % function will call the draw methods for each of the 3 grids.
% inputs: % inputs:
% obj:GUI - current GUI object % obj:GUI - current GUI object
% load:boolean - 0 if grid is being refreshed, 1 if grid is being % load:tristate - 0 if grid is being refreshed, 1 if grid should reload
% loaded for the firs time. % data, 2 if the grid is being initialized.
% outputs: % outputs:
% none % none
% Author: Colin Eles elesc@mcmaster.ca % Author: Colin Eles elesc@mcmaster.ca
......
...@@ -3,13 +3,13 @@ ...@@ -3,13 +3,13 @@
% inputs: % inputs:
% obj:GUI - current GUI object % obj:GUI - current GUI object
% grid:Grid - grid to be drawn, should be grid on left. % grid:Grid - grid to be drawn, should be grid on left.
% load:boolean - 0 if grid is being refreshed, 1 if grid is being % load:tristate - 0 if grid is being refreshed, 1 if grid should reload
% loaded for the firs time. % data, 2 if the grid is being initialized.
% outputs: % outputs:
% none % none
% Author: Colin Eles elesc@mcmaster.ca % Author: Colin Eles elesc@mcmaster.ca
% Organization: McMaster Centre for Software Certification % Organization: McMaster Centre for Software Certification
function [] = draw_grid0(object,grid,load) function [] = draw_grid0(object,grid,load, init)
% ensure that the results grid is up to date. % ensure that the results grid is up to date.
grid.refresh(); grid.refresh();
for i=1:size(grid.Cells,2) for i=1:size(grid.Cells,2)
...@@ -22,12 +22,12 @@ for i=1:size(grid.Cells,2) ...@@ -22,12 +22,12 @@ for i=1:size(grid.Cells,2)
pos(2) = pos2(2); pos(2) = pos2(2);
pos(3) = pos1(3); pos(3) = pos1(3);
pos(4) = pos2(4); pos(4) = pos2(4);
if isempty(grid.Cells(i).result) || ~ishandle(grid.Cells(i).result)%load == 1 if load == 2 || isempty(grid.Cells(i).result) || ~ishandle(grid.Cells(i).result)
grid.Cells(i).result = object.create_std_text(object.fig,pos); grid.Cells(i).result = object.create_std_text(object.fig,pos);
% if we are loading the cell, try to restore the text % if we are loading the cell, try to restore the text
% that was saved using save_results. % that was saved using save_results.
if load == 1 if load ~= 0
set(grid.Cells(i).result,'String',grid.Cells(i).result_text); set(grid.Cells(i).result,'String',grid.Cells(i).result_text);
end end
else else
......
...@@ -4,8 +4,8 @@ ...@@ -4,8 +4,8 @@
% inputs: % inputs:
% obj:GUI - current GUI object % obj:GUI - current GUI object
% grid:Grid - grid to be drawn, should be grid on top. % grid:Grid - grid to be drawn, should be grid on top.
% load:boolean - 0 if grid is being refreshed, 1 if grid is being % load:tristate - 0 if grid is being refreshed, 1 if grid should reload
% loaded for the firs time. % data, 2 if the grid is being initialized.
% outputs: % outputs:
% none % none
% Author: Colin Eles elesc@mcmaster.ca % Author: Colin Eles elesc@mcmaster.ca
...@@ -34,9 +34,9 @@ for i=1:size(grid.cells,2) ...@@ -34,9 +34,9 @@ for i=1:size(grid.cells,2)
pos(1) = pos(1) + (i-1)*grid.cells(i).condition_text_width + grid.cells(i).condition_text_offset + pb_space; pos(1) = pos(1) + (i-1)*grid.cells(i).condition_text_width + grid.cells(i).condition_text_offset + pb_space;
% if the edit box does not exist create it, if it does % if the edit box does not exist create it, if it does
% adjust it's position. % adjust it's position.
if (isempty(grid.cells(i).cond) || ~ishandle(grid.cells(i).cond))%load == 1) if (load == 2 || isempty(grid.cells(i).cond) || ~ishandle(grid.cells(i).cond))
grid.cells(i).cond = object.create_std_text(object.fig,pos); grid.cells(i).cond = object.create_std_text(object.fig,pos);
if (load == 1) if (load ~= 0)
set(grid.cells(i).cond,'String',grid.cells(i).cond_text); set(grid.cells(i).cond,'String',grid.cells(i).cond_text);
end end
else else
...@@ -66,12 +66,12 @@ if( object.edit == 1) ...@@ -66,12 +66,12 @@ if( object.edit == 1)
set(grid.delete_cell_pb,'userdata',object); set(grid.delete_cell_pb,'userdata',object);
set(grid.new_cell_pb,'userdata',object); set(grid.new_cell_pb,'userdata',object);
else else
delete(grid.new_cell_pb) delete(grid.new_cell_pb);
grid.new_cell_pb = []; grid.new_cell_pb = [];
delete(grid.delete_cell_pb) delete(grid.delete_cell_pb)
grid.delete_cell_pb = []; grid.delete_cell_pb = [];
end end
if object.edit ==1 || load == 1 if object.edit ==1 || load ~= 0
fig_pos = get(object.fig,'position'); fig_pos = get(object.fig,'position');
if(pos(1)+pos(3)>fig_pos(3)) if(pos(1)+pos(3)>fig_pos(3))
fig_pos(3) = pos(1)+pos(3); fig_pos(3) = pos(1)+pos(3);
......
...@@ -3,8 +3,8 @@ ...@@ -3,8 +3,8 @@
% inputs: % inputs:
% obj:GUI - current GUI object % obj:GUI - current GUI object
% grid:Grid - grid to be drawn, should be grid on left. % grid:Grid - grid to be drawn, should be grid on left.
% load:boolean - 0 if grid is being refreshed, 1 if grid is being % load:tristate - 0 if grid is being refreshed, 1 if grid should reload
% loaded for the firs time. % data, 2 if the grid is being initialized.
% outputs: % outputs:
% none % none
% Author: Colin Eles elesc@mcmaster.ca % Author: Colin Eles elesc@mcmaster.ca
...@@ -67,7 +67,7 @@ if (~isempty(grid)) ...@@ -67,7 +67,7 @@ if (~isempty(grid))
% if the edit box does not exist, ie. it is just being % if the edit box does not exist, ie. it is just being
% created or we are loading the figure % created or we are loading the figure
if (isempty(grid.cells(i).cond) || ~ishandle(grid.cells(i).cond))%load == 1) if (load == 2 || isempty(grid.cells(i).cond) || ~ishandle(grid.cells(i).cond))
% create the new edit box % create the new edit box
grid.cells(i).cond = object.create_std_text(object.fig,pos); grid.cells(i).cond = object.create_std_text(object.fig,pos);
% if cell is the first in the grid use the new % if cell is the first in the grid use the new
...@@ -82,7 +82,7 @@ if (~isempty(grid)) ...@@ -82,7 +82,7 @@ if (~isempty(grid))
% if we are loading the cell set the string of the % if we are loading the cell set the string of the
% edit box to be the value that we saved as a % edit box to be the value that we saved as a
% result of calling save_conditions % result of calling save_conditions
if (load == 1) if (load ~= 0)
set(grid.cells(i).cond,'String',grid.cells(i).cond_text); set(grid.cells(i).cond,'String',grid.cells(i).cond_text);
end end
else else
...@@ -100,11 +100,11 @@ if (~isempty(grid)) ...@@ -100,11 +100,11 @@ if (~isempty(grid))
if (ishghandle(grid.cells(i).grid_pb)) if (ishghandle(grid.cells(i).grid_pb))
set(grid.cells(i).grid_pb,'Visible','on'); set(grid.cells(i).grid_pb,'Visible','on');
end end
grid.cells(i).set_pb(object.fig,pb_pos) grid.cells(i).set_pb(object.fig,pb_pos);
set(grid.cells(i).grid_pb,'UserData',object); set(grid.cells(i).grid_pb,'UserData',object);
elseif(grid.cells(i).pb_flag == 1 && object.edit ~= 1) elseif(grid.cells(i).pb_flag == 1 && object.edit ~= 1)
if (ishghandle(grid.cells(i).grid_pb)) if (ishghandle(grid.cells(i).grid_pb))
set(grid.cells(i).grid_pb,'Visible','off') set(grid.cells(i).grid_pb,'Visible','off');
end end
end end
......
...@@ -40,6 +40,15 @@ end ...@@ -40,6 +40,15 @@ end
check_string = [check_string counter sprintf('\n')]; check_string = [check_string counter sprintf('\n')];
for i=1:size(grid.cells,2) for i=1:size(grid.cells,2)
condition_string = get(grid.cells(i).cond,'string'); condition_string = get(grid.cells(i).cond,'string');
if size(condition_string,1) > 0
s = [condition_string(1,:)];
for j = 2:size(condition_string,1)
s = [s ' ' condition_string(j,:)];
end
condition_string = s;
end
if(~isempty(condition_string)) if(~isempty(condition_string))
eval([check_string 'result =(' char(condition_string) ');']) eval([check_string 'result =(' char(condition_string) ');'])
......
...@@ -174,18 +174,18 @@ uimenu(checkmenu,'Label','PVS Generate file','Callback',@(src,event)pvs_file_cal ...@@ -174,18 +174,18 @@ uimenu(checkmenu,'Label','PVS Generate file','Callback',@(src,event)pvs_file_cal
uimenu(checkmenu,'Label','PVS Typecheck SimTypes','Callback',@(src,event)pvs_ext_call_sim(object,src,event)); uimenu(checkmenu,'Label','PVS Typecheck SimTypes','Callback',@(src,event)pvs_ext_call_sim(object,src,event));
uimenu(helpmenu,'Label','Product Help','Callback',@(src,event)help_call(object,src,event)); uimenu(helpmenu,'Label','Product Help','Callback',@(src,event)help_call(object,src,event));
uimenu(helpmenu,'Label','About Table Tool','Callback',@(src,event)about_call(object,src,event)); uimenu(helpmenu,'Label','About Tabular Expression Toolbox','Callback',@(src,event)about_call(object,src,event));
object.set_command_pos; object.set_command_pos;
object.reset_wh(); object.reset_wh();
object.draw_allgrids(1); object.draw_allgrids(2);
object.saved = 1; object.saved = 1;
object.setPBenable; object.setPBenable;
object.default_prover = object.CVC_const; object.default_prover = object.CVC_const;
object.settings = Settings(); object.settings = TTSettings();
if isfield(object.Data.settings,'set') if isfield(object.Data.settings,'set')
object.settings.setvalues(object.Data.settings); object.settings.setvalues(object.Data.settings);
else else
......
...@@ -13,6 +13,7 @@ object.save_call([],[]); ...@@ -13,6 +13,7 @@ object.save_call([],[]);
object.save_data; object.save_data;
if (object.validation_report_handle ~= 0) if (object.validation_report_handle ~= 0)
delete(object.validation_report_handle); delete(object.validation_report_handle);
object.validation_report_handle = 0;
end end
error = object.check_call([],2); error = object.check_call([],2);
...@@ -35,6 +36,7 @@ if (~error) ...@@ -35,6 +36,7 @@ if (~error)
else else
Valid_Report = ValidationReport(object); Valid_Report = ValidationReport(object);
Valid_Report.set_results(result); Valid_Report.set_results(result);
Valid_Report.set_mode(0);
Valid_Report.init(); Valid_Report.init();
end end
object.pvs_checked = check; object.pvs_checked = check;
......
...@@ -41,6 +41,7 @@ if (~error) ...@@ -41,6 +41,7 @@ if (~error)
else else
Valid_Report = ValidationReport(object); Valid_Report = ValidationReport(object);
Valid_Report.set_results(result); Valid_Report.set_results(result);
Valid_Report.set_mode(0);
Valid_Report.init(); Valid_Report.init();
end end
object.pvs_checked = check; object.pvs_checked = check;
......
...@@ -10,7 +10,7 @@ ...@@ -10,7 +10,7 @@
% Author: Colin Eles elesc@mcmaster.ca % Author: Colin Eles elesc@mcmaster.ca
% Organization: McMaster Centre for Software Certification % Organization: McMaster Centre for Software Certification
function [] = pvs_file_call(object,src,event) function [] = pvs_file_call(object,src,event)
object.save_data object.save_data;
object.PVS.generate_pvs_file(object.Data.function_name); object.PVS.generate_pvs_file(object.Data.function_name);
......
...@@ -35,7 +35,7 @@ if object.mode == 0 ...@@ -35,7 +35,7 @@ if object.mode == 0
open_system(model); open_system(model);
load_system('TableLibrary'); load_system('TableLibrary');
new_block = add_block('TableLibrary/Tabular Expression',[model '/' function_name]); new_block = add_block('TableLibrary/Tabular Expression',[model '/' function_name]);
set_param(new_block,'UserData',object.Data) set_param(new_block,'UserData',object.Data);
set_param(new_block, 'UserDataPersistent', 'on'); set_param(new_block, 'UserDataPersistent', 'on');
object.mode = 1; object.mode = 1;
object.block_handle = new_block; object.block_handle = new_block;
......
...@@ -24,6 +24,7 @@ set.set = 1; ...@@ -24,6 +24,7 @@ set.set = 1;
set.inputs = object.settings.pvs_includes; set.inputs = object.settings.pvs_includes;
set.count = object.settings.counter_trials; set.count = object.settings.counter_trials;
set.range = object.settings.counter_range; set.range = object.settings.counter_range;
set.except = object.settings.except;
object.Data.settings = set; object.Data.settings = set;
end end
...@@ -29,7 +29,7 @@ if(~isempty(unicode2native(event.Character))) ...@@ -29,7 +29,7 @@ if(~isempty(unicode2native(event.Character)))
if event.Character > 33 || event.Character == 8 if event.Character > 33 || event.Character == 8
if object.pvs_checked == 1 if object.pvs_checked == 1
object.pvs_checked = 0; object.pvs_checked = 0;
object.update_Statusbar object.update_Statusbar;
if (object.mode == 1) if (object.mode == 1)
TableBlock.set_block_display(object.block_handle,object.pvs_checked); TableBlock.set_block_display(object.block_handle,object.pvs_checked);
end end
......
...@@ -66,6 +66,6 @@ else ...@@ -66,6 +66,6 @@ else
end end
object.update_undoredo object.update_undoredo;
end end
...@@ -31,7 +31,7 @@ if isempty(event) || event ~= 1 ...@@ -31,7 +31,7 @@ if isempty(event) || event ~= 1
gui.undo_man.new_state(undo_data); gui.undo_man.new_state(undo_data);
end end
gui.update_undoredo gui.update_undoredo;
end end
......
%% purge
% Removes useless data from the block on saving, avoiding unnecessary
% changes and data storage.
% inputs:
% object - Grid object
% outputs:
% none
% Author: Matthew Dawson <matthew@mjdsystems.ca>
% Organization: McMaster Centre for Software Certification
function purge( object )
% delete(object.new_cell_pb)
% delete(object.delete_cell_pb)
object.new_cell_pb = [];
object.delete_cell_pb = [];
for i=1:size(object.cells, 2)
object.cells(i).purge
end
end