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

