Newer
Older
pos(1) = parent_pos(1) + parent_pos(3);
pos(2) = prev_pos(2) - pos(4);
grid_color = grid.cells(i-1).color;
end
else
% grid is the root grid.
% position of the first cell is based on
% condition_text_x, and condition_text_y, as well
% as the height of the figure and header.
figpos = get(object.fig,'position');
pos = [grid.cells(i).condition_text_x figpos(4)-object.header_height-grid.cells(i).condition_text_y grid.cells(i).condition_text_width grid.cells(i).condition_text_height];
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
if i == 1
pos(1) = pos(1);
pos(4) = grid.cells(i).height * grid.cells(i).condition_text_height;
pos(2) = pos(2)-pos(4)-grid.cells(i).condition_text_height-grid.cells(i).condition_text_offset;
pos(3) = grid.cells(i).width * grid.cells(i).condition_text_width;
pos(4) = grid.cells(i).height * grid.cells(i).condition_text_height;
else
prev_pos = grid.cells(i-1).get_pos;
pos(3) = grid.cells(i).width * grid.cells(i).condition_text_width;
pos(4) = grid.cells(i).height * grid.cells(i).condition_text_height;
pos(1) = pos(1);
pos(2) = prev_pos(2) - pos(4);
grid_color = grid.cells(i-1).color;
end
end
% if the edit box does not exist, ie. it is just being
% created or we are loading the figure
if (isempty(grid.cells(i).cond) || load == 1)
% create the new edit box
grid.cells(i).cond = object.create_std_text(object.fig,pos);
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
% if cell is the first in the grid use the new
% colour, else take the colour of the previous cell
% in the grid.
if(i==1)
set(grid.cells(i).cond,'BackgroundColor',grid_color);
else
set(grid.cells(i).cond,'BackgroundColor',get(grid.cells(i-1).cond,'BackgroundColor'))
end
grid.cells(i).color = grid_color;
% if we are loading the cell set the string of the
% edit box to be the value that we saved as a
% result of calling save_conditions
if (load == 1)
set(grid.cells(i).cond,'String',grid.cells(i).cond_text);
end
else
% if the edit box is already created change is
% position to newly determined position.
grid.cells(i).set_pos(pos);
end
% determine if we want to draw the new subgrid buttons,
% which is located to the right of each of the leaf
% cells.
if(grid.cells(i).pb_flag == 1 && object.edit == 1)
pb_pos = pos;
pb_pos(1) = pos(1)+pos(3);
pb_pos(3) = grid.cells(i).grid_push_width;
if (ishghandle(grid.cells(i).grid_pb))
set(grid.cells(i).grid_pb,'Visible','on');
end
grid.cells(i).set_pb(object.fig,pb_pos)
set(grid.cells(i).grid_pb,'UserData',object);
elseif(grid.cells(i).pb_flag == 1 && object.edit ~= 1)
if (ishghandle(grid.cells(i).grid_pb))
set(grid.cells(i).grid_pb,'Visible','off')
end
end
delete_pb_pos = [];
% detemine if we want to draw the new cell buttons,
% which are located at the botton of the set of cells.
if (i == size(grid.cells,2) && object.edit == 1)
new_pb_pos = pos;
new_pb_pos(4) = grid.cells(i).condition_text_height/2;
new_pb_pos(3) = pos(3)/2;
new_pb_pos(2) = pos(2) - new_pb_pos(4);
if (ishghandle(grid.new_cell_pb))
set(grid.new_cell_pb,'Visible','on');
end
grid.set_pb(object.fig,new_pb_pos);
set(grid.new_cell_pb,'userdata',object);
delete_pb_pos = new_pb_pos;
delete_pb_pos(1) = new_pb_pos(1) + new_pb_pos(3);
if (ishghandle(grid.delete_cell_pb))
set(grid.delete_cell_pb,'Visible','on');
end
grid.set_delete_pb(object.fig,delete_pb_pos);
set(grid.delete_cell_pb,'userdata',object);
elseif (i == size(grid.cells,2) && object.edit ~= 1)
if (ishghandle(grid.new_cell_pb))
set(grid.new_cell_pb,'Visible','off');
end
if (ishghandle(grid.delete_cell_pb))
set(grid.delete_cell_pb,'Visible','off');
end
end
% recursively draw the subgrid of the cell if it
% exists.
object.draw_grid2(grid.cells(i).subgrid,load);
end
end
end
%% reset_wh
% function will call the set_widths and set_heights methods on
% the left grid in the table. The height and width values are
% used to draw the grid.
% inputs:
% obj:GUI - current GUI object
function [] = reset_wh(object)
width = object.Grid2.max_width(1);
object.Grid2.set_widths(width);
object.Grid2.set_heights(object.edit);
end
%% draw_grid1
% Draws the grid on the top onto the figure. the current
% assumption is that the top grid does not have any subgrids,
% inputs:
% obj:GUI - current GUI object
% grid:Grid - grid to be drawn, should be grid on top.
% load:boolean - 0 if grid is being refreshed, 1 if grid is being
% loaded for the firs time.
function [] = draw_grid1(object,grid,load)
% assumption grid 1 has no subgrids
pos = [];
for i=1:size(grid.cells,2)
% if we are in edit mode we need to shift over the cells to
% accomidate for the new grid buttons in the left grid.
pb_space = grid.cells(i).grid_push_width;
else
pb_space = 0;
end
figpos = get(object.fig,'position');
% check if grid2 is empty, currently grid 2 will never be
% empty, may change in future though.
pos = [grid.cells(i).condition_text_x grid.cells(i).condition_text_y grid.cells(i).condition_text_width grid.cells(i).condition_text_height];
else
pos = [grid.cells(i).condition_text_x+grid.cells(i).condition_text_width*object.Grid2.max_width(1) figpos(4)-object.header_height-grid.cells(i).condition_text_y-grid.cells(i).condition_text_height grid.cells(i).condition_text_width grid.cells(i).condition_text_height];
end
% set the x coordinate of the cell
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
% adjust it's position.
if (isempty(grid.cells(i).cond) || load == 1)
grid.cells(i).cond = object.create_std_text(object.fig,pos);
if (load == 1)
set(grid.cells(i).cond,'String',grid.cells(i).cond_text);
end
else
grid.cells(i).set_pos(pos);
end
end
% if we are in edit mode, draw the new and delete buttons at
% the right of the last cell
pos(1) = pos(1) + pos(3);
pos(2) = pos(2) + 20;
pos(4) = 20;
pos(3) = 60;
grid.set_delete_pb(object.fig,pos);
set(grid.delete_cell_pb,'userdata',object);
set(grid.new_cell_pb,'userdata',object);
else
delete(grid.new_cell_pb)
grid.new_cell_pb = [];
delete(grid.delete_cell_pb)
grid.delete_cell_pb = [];
end
if object.edit ==1 || load == 1
fig_pos = get(object.fig,'position');
fig_pos(3) = pos(1)+pos(3);
set(object.fig,'position',fig_pos);
elseif (pos(1) + pos(3)<object.fig_width)
fig_pos(3) = object.fig_width;
set(object.fig,'position',fig_pos);
elseif (pos(1) + pos(3)<fig_pos(3) && pos(1) +pos(3) >object.fig_width)
fig_pos(3) = pos(1)+pos(3);
set(object.fig,'position',fig_pos);
end
end
end
%% draw_grid0
% function will draw the output grid onto the figure
% inputs:
% obj:GUI - current GUI object
% grid:Grid - grid to be drawn, should be grid on left.
% load:boolean - 0 if grid is being refreshed, 1 if grid is being
% loaded for the firs time.
function [] = draw_grid0(object,grid,load)
% ensure that the results grid is up to date.
grid.refresh();
for i=1:size(grid.Cells,2)
% get the x coordinate from the associated top grid cell,
% get the y coordinate from the associated right grid cell.
pos1 = grid.Cells(i).Cell1.get_pos;
pos2 = grid.Cells(i).Cell2.get_pos;
pos = [0 0 0 0];
pos(1) = pos1(1);
pos(2) = pos2(2);
pos(3) = pos1(3);
pos(4) = pos2(4);
if isempty(grid.Cells(i).result) || load == 1
grid.Cells(i).result = object.create_std_text(object.fig,pos);
% if we are loading the cell, try to restore the text
% that was saved using save_results.
if load == 1
set(grid.Cells(i).result,'String',grid.Cells(i).result_text);
end
else
set(grid.Cells(i).result,'position',pos);
end
end
end
%% draw_allgrids
% function will call the draw methods for each of the 3 grids.
% inputs:
% obj:GUI - current GUI object
% load:boolean - 0 if grid is being refreshed, 1 if grid is being
% loaded for the firs time.
function [] = draw_allgrids(object,load)
object.draw_grid2(object.Grid2,load);
object.draw_grid1(object.Grid1,load);
object.draw_grid0(object.Grid0,load);
% 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'
function [] = evaluate_counter(object,counter)
problem = object.evaluate_counter_grid(object.Grid2, counter);
object.evaluate_counter_grid(object.Grid1, counter)
% 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'
% problem:boolean - 1 if grid has overlapping or underspecified
% cells, 0 if not.
function problem = evaluate_counter_grid(object,grid,counter)
inputs = get(object.function_inputs_control,'String');
inputs = regexp(inputs,',','split');
check_string = [];
% keep track of the number of condtitions that evaulate to true
true_conds = 0;
sub_problem = 0;
problem = 0;
empty_cell = 0;
% initialize inputs to zero
% functions are assumed to be total, so 0 is just for
% convienence
for i=1:size(inputs,2)
% set to zero
%need to parse the types out of the inputs
inputi = regexp(char(inputs(i)),'\w*','match','once');
check_string = [check_string sprintf('%s=0;\n',char(inputi))];
end
check_string = [check_string counter sprintf('\n')];
for i=1:size(grid.cells,2)
condition_string = get(grid.cells(i).cond,'string');
if(~isempty(condition_string))
eval([check_string 'result =(' char(condition_string) ');'])
if(result == 0)
grid.cells(i).flag_cell(1);
else
true_conds = true_conds + 1;
grid.cells(i).flag_cell(2);
end
else
empty_cell = 1;
end
end
if (true_conds == 1)
for i=1:size(grid.cells,2)
condition_string = get(grid.cells(i).cond,'string');
if(~isempty(condition_string))
eval([check_string 'result =(' char(condition_string) ');'])
if(result == 0)
grid.cells(i).flag_cell(1);
else
if (~isempty(grid.cells(i).subgrid))
sub_problem = object.evaluate_counter_grid(grid.cells(i).subgrid,counter);
end
grid.cells(i).flag_cell(2);
end
else
empty_cell = 1;
end
end
end
if (true_conds ~= 1 || sub_problem == 1)
end
end
%% create_std_text
% function will create an edit text box used for conditons and
% results. we want these to be consistent so its easier for it to
% be in one function.
% inputs:
% obj:GUI - current GUI object
% Parent:double - handle to parent figure
% position:[double double double double] - position to place edit
% box in.
% control:double - handle pointing to newly created uicontrol
function control = create_std_text(object, Parent, position)
control = uicontrol('style','edit',...
'Parent',Parent,...
'units','pix',...
'position',position,...
'min',0,'max',1,... % This is the key to multiline edits.
'string',{''},...
'Max',2.0,...
'Clipping','on',...
'fontweight','bold',...
'BackgroundColor',[1 1 1],...
'horizontalalign','center',...
'KeyPressFcn',@(src,event)textbox_callback(object,src,event),...
%% 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
function [] = textbox_callback(object,src,event)
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
Colin Eles
committed
end
Colin Eles
committed
%% check_inputs
% ensure that the inputs are proper variable names, and that the
% input string parses properly
% inputs:
% object:GUI - current GUI object
% 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 = [];
for i=1:size(parsed_input,2)
if(size(parsed_input{i},2) == 2)
if (strcmp(parsed_input{i}(2),'error'))
error = [error sprintf('%s is not a valid variable name\n',char(parsed_input{i}(1))) ];
end
end
end
end
Colin Eles
committed
%% 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
function [] = setPBenable(object)
if size(object.Grid1.cells,2) > 1
set(object.Grid1.delete_cell_pb,'Enable','on');
Colin Eles
committed
else
set(object.Grid1.delete_cell_pb,'Enable','off');
Colin Eles
committed
end
if size(object.Grid2.cells,2) > 1
set(object.Grid2.delete_cell_pb,'Enable','on');
Colin Eles
committed
else
set(object.Grid2.delete_cell_pb,'Enable','off');
Colin Eles
committed
end
end
end
methods(Static)
%% msgbox_scroll
% create a message box with a scrollable text area
% inputs:
% msg:string - string to put into the message box
function [] = msgbox_scroll(msg)
fig = figure('units','pixels',...
'position',[0 0 700 500],...
'menubar','none',...
'name','PVS Report',...
'numbertitle','off');
uicontrol('style','edit',...
'units','pix',...
'Parent',fig,...
'HorizontalAlign','center',...
'FontWeight','bold',...
'FontSize',12,...
'Max',2.0,...
'HorizontalAlign','left',...
'String',msg,...
'Position',[1 1 698 498],...
'BackgroundColor',[1 1 1]);
Colin Eles
committed
end