classdef ValidationReport < handle
%UNTITLED Summary of this class goes here
% Detailed explanation goes here
properties
fig = [];
PVS_results = [];
fig_height = 400;
fig_width = 800;
edit_tcc = [];
edit_seq = [];
edit_ce = [];
pb_next = [];
pb_prev = [];
label_tcc = [];
label_seq = [];
label_ce = [];
label_page = [];
label_title = [];
label_height = 15;
TCC_width = 200;
TCC_height = 200;
seq_width = 300;
seq_height = 200;
ce_width = 200;
ce_height = 200;
header_height = 60;
gui = [];
pb_nav_width = 60;
pb_nav_height = 20;
offset = 10;
page = 1;
keyword = '1234a';
end
methods
function obj = ValidationReport(guinew)
obj.gui = guinew;
end
function [] = set_results(obj,res)
obj.PVS_results = res;
end
function [] = init(obj)
if size(obj.PVS_results,2) == 0
msgbox('table is proper')
else
obj.fig_width = obj.offset + obj.TCC_width + obj.offset + obj.seq_width + obj.offset + obj.ce_width + obj.offset
obj.fig_height = obj.offset + obj.header_height + obj.offset + obj.seq_height + obj.offset
obj.fig = figure('units','pixels',...
'position',[0, 0, obj.fig_width, obj.fig_height ],...
'menubar','none',...
'name','PVS Report',...
'numbertitle','off',...
'resize','off',...
'CloseRequestFcn',@(src,event)close_req_call(obj,src,event));
stop = 0
i = 1;
count = 0;
%first i will be '1234a'
obj.edit_tcc = uicontrol('style','edit',...
'Parent',obj.fig,...
'units','pix',...
'min',0,'max',1,... % This is the key to multiline edits.
'Max',2.0,...
'Clipping','on',...
'fontweight','bold',...
'BackgroundColor',[1 1 1],...
'horizontalalign','center',...
'fontsize',11);
obj.edit_seq = uicontrol('style','edit',...
'Parent',obj.fig,...
'units','pix',...
'min',0,'max',1,... % This is the key to multiline edits.
'Max',2.0,...
'Clipping','on',...
'fontweight','bold',...
'BackgroundColor',[1 1 1],...
'horizontalalign','left',...
'fontsize',11);
obj.edit_ce = uicontrol('style','edit',...
'Parent',obj.fig,...
'units','pix',...
'min',0,'max',1,... % This is the key to multiline edits.
'Max',2.0,...
'Clipping','on',...
'fontweight','bold',...
'BackgroundColor',[1 1 1],...
'horizontalalign','left',...
'fontsize',11);
obj.pb_next = uicontrol('style','push',...
'units','pix',...
'string','Next',...
'HorizontalAlign','left',...
'Parent',obj.fig,...
'callback',@(src,event)pb_next_call(obj,src,event));
if(size(obj.PVS_results,2)<=1)
set(obj.pb_next,'enable','off');
end
obj.pb_prev = uicontrol('style','push',...
'units','pix',...
'string','Prev',...
'HorizontalAlign','left',...
'Parent',obj.fig,...
'enable','off',...
'callback',@(src,event)pb_prev_call(obj,src,event));
obj.label_tcc = uicontrol('style','text',...
'string','TCC Name',...
'HorizontalAlign','left',...
'BackgroundColor',get(obj.fig,'Color'));
obj.label_seq = uicontrol('style','text',...
'string','Sequent',...
'HorizontalAlign','left',...
'BackgroundColor',get(obj.fig,'Color'));
obj.label_ce = uicontrol('style','text',...
'string','Counter Example',...
'HorizontalAlign','left',...
'BackgroundColor',get(obj.fig,'Color'));
obj.label_page = uicontrol('style','text',...
'string','',...
'HorizontalAlign','center',...
'BackgroundColor',get(obj.fig,'Color'));
obj.label_title = uicontrol('style','text',...
'string','Typecheck Summary',...
'HorizontalAlign','left',...
'FontWeight','bold',...
'FontSize',15,...
'BackgroundColor',get(obj.fig,'Color'));
obj.position;
obj.populate;
end
end
function [] = position(obj)
set(obj.edit_tcc,'position',[obj.offset, (obj.fig_height - obj.offset - obj.header_height - obj.offset - obj.seq_height) ,obj.TCC_width,obj.TCC_height])
set(obj.edit_seq,'position',[obj.offset + obj.TCC_width + obj.offset, (obj.fig_height - obj.offset - obj.header_height - obj.offset - obj.seq_height),obj.seq_width,obj.seq_height])
set(obj.edit_ce, 'position',[obj.offset + obj.TCC_width + obj.offset + obj.seq_width + obj.offset, (obj.fig_height - obj.offset - obj.header_height - obj.offset - obj.seq_height) ,obj.ce_width,obj.ce_height])
set(obj.label_tcc,'position',[obj.offset, (obj.fig_height - obj.offset - obj.header_height) ,obj.TCC_width,obj.label_height])
set(obj.label_seq,'position',[obj.offset + obj.TCC_width + obj.offset, (obj.fig_height - obj.offset - obj.header_height) ,obj.TCC_width,obj.label_height])
set(obj.label_ce,'position',[obj.offset + obj.TCC_width + obj.offset + obj.seq_width + obj.offset, (obj.fig_height - obj.offset - obj.header_height) ,obj.TCC_width,obj.label_height])
set(obj.label_title,'position',[obj.offset, (obj.fig_height - obj.offset - obj.label_height*2) ,obj.TCC_width,obj.label_height*2])
set(obj.label_page,'position',[obj.fig_width-obj.pb_nav_width*2-obj.offset*2, obj.fig_height-obj.offset-obj.header_height+obj.label_height+obj.pb_nav_height+obj.offset/2,obj.pb_nav_width*2+obj.offset,obj.pb_nav_height]);
set(obj.pb_next,'position',[obj.fig_width - obj.pb_nav_width - obj.offset, obj.fig_height - obj.offset - obj.header_height + obj.label_height + obj.offset/2, obj.pb_nav_width, obj.pb_nav_height]);
set(obj.pb_prev,'position',[obj.fig_width - obj.pb_nav_width - obj.offset - obj.offset - obj.pb_nav_width, obj.fig_height - obj.offset - obj.header_height + obj.label_height+obj.offset/2, obj.pb_nav_width, obj.pb_nav_height]);
end
function [] = pb_prev_call(obj,src,event)
obj.page = obj.page - 1;
obj.populate
if(obj.page == 1)
set(src,'enable','off');
end
set(obj.pb_next,'enable','on');
end
function [] = pb_next_call(obj,src,event)
obj.page = obj.page + 1;
obj.populate;
if (obj.page == size(obj.PVS_results,2))
set(src,'enable','off');
end
set(obj.pb_prev,'enable','on');
end
function [] = close_req_call(obj,src,event)
obj.gui.check_call([],[]);
delete(obj.fig);
end
function [] = populate(obj)
% temporarily used to reset colours
obj.gui.check_call([],[]);
set(obj.edit_tcc,'string',char(obj.PVS_results(obj.page).TCC));
set(obj.edit_seq,'string',char(obj.PVS_results(obj.page).seq));
set(obj.label_page,'string',[num2str(obj.page) ' of ' num2str(size(obj.PVS_results,2))]);
counter = []
if size(obj.PVS_results(obj.page).ce,2) == 0
counter = ['no counter example generated']
else
for i = 1:2:size(obj.PVS_results(obj.page).ce,2)
% need to do some translation back to matlab syntax
new_value = regexprep(char(obj.PVS_results(obj.page).ce(i+1)),'FALSE',' 0 ')
new_value = regexprep(new_value,'TRUE',' 1 ')
eval(['value = ' char(new_value)])
counter = [counter char(obj.PVS_results(obj.page).ce(i)) ' = ' num2str(value) ';' sprintf('\n')]
end
obj.gui.evaluate_counter(counter);
end
set(obj.edit_ce,'string',counter);
end
end
end