document.m

CheckMate is a MATLAB-based tool for modeling, simulating and investigating properties of hybrid dyn

function document(var)

% 
% Syntax:
%     "document(variable)"
%  
% 
% Description:
% Documents a Checkmate specific global variable.  The function outputs the entire contents
% of the Checkmate structure to the screen and creates a .txt document with the same 
% information.  The text file is automatically opened in a new Matlab editor window.
% Global variables that can be displayed are the following:
% 
% 
%     -GLOBAL_PIHA: This is a structure that acts as a repository for all of the model information
%                   given by the user (from the Simulink model and the user-defined m-files).
%                   
%                   
%     -GLOBAL_AUTOMATON:  This is the finite state automaton that is created from the reachability analysis
%                         that Checkmate performs on the system (using the information contained in GLOBAL_PIHA).  
%                         Information about the regions of the concrete system that each state represents if
%                         given as well as information about the connectivity between regions.
%                         
%                         
%     -GLOBAL_TRANSISITON:  This is the raw transition system that Checkmate creates from the GLOBAL_AUTOMATON.
%                           This is the structure that model checking is performed on in order to verify the
%                           property specified by the user.
% 
% Syntax:
%   "display(variable)"
%
% Description:
%   "display(variable)" is used to display and archive the information contained within the Checkmate specific global
%   variables GLOBAL_PIHA, GLOBAL_AUTOMATON, or GLOBAL_TRANSITION.
%
% See Also:
%   piha

if ~iscell(var)
    if isfield(var,'Locations')
        %Input varialbe is a PIHA.
        warning off
        delete Piha_Data.txt
        warning on
        
        diary('Piha_Data.txt')
        %File introduction
        fprintf(1,'\n\nThis file logs all of the information contained in the Checkmate variable GLOBAL_PIHA\n');
        fprintf(1,'The GLOBAL_PIHA variable is a repository for all of the information contained in the \n');
        fprintf(1,'Simulink model and the user-defined m-file.  Creation of the GLOBAL_PIHA structure is the\n');
        fprintf(1,'is the first step in Checkmate''s verification procedure.\n\n');
        fprintf(1,['\nThis file was written on ' date '\n']);
        fprintf(1,'*****************************************************************************************\n\n');
       
        %Hyperplane List
        fprintf(1,'\n*****************************************************************************************\n');
        fprintf(1,'Hyperplane list:  This section lists all of the hyperplanes used to create the GLOBAL_PIHA\n');
        fprintf(1,'structure (i.e. hyperplanes from the guard regions, the analysis region, and the initial\n');
        fprintf(1,'continuous region).\n');
        fprintf(1,'*****************************************************************************************\n\n');
        for i=1:length(var.Hyperplanes)
            fprintf(1,'\nHyperplane %d\n',i);
            disp(var.Hyperplanes{i})
        end
        
        %NAR
        fprintf(1,'\n*****************************************************************************************\n');
        fprintf(1,'Number of Hyperplanes in the Analysis Region:  %d  \n',var.NAR);
        fprintf(1,'This is the total number of Hyperplanes that make up the Analysis Region.  The first %d\n',var.NAR);
        fprintf(1,'Hyperplanes listed above make up the Analysis Region.\n');
        fprintf(1,'*****************************************************************************************\n\n');
        
        
       
        
        %Initial sets
        fprintf(1,'\n*****************************************************************************************\n');
        fprintf(1,'Initial Sets:  This section lists the linearcons that make up the initial continuous\n');
        fprintf(1,'sets (ICS) and their corresponding discrete state.  This list describes all possible\n');
        fprintf(1,'initial conditions for the systems.\n');
        fprintf(1,'*****************************************************************************************\n\n');
        
        fprintf(1,'Initial Discrete State ');
        for j=1:length(var.InitialDiscreteSet{1})
            fprintf(1,'%d ',var.InitialDiscreteSet{1});
        end
        fprintf(1,'\n');
        for i=1:length(var.InitialContinuousSet)
            fprintf(1,'\nICS Element %d\n',i);
            var.InitialContinuousSet{i}
        end
        
        %Cells
        fprintf(1,'\n*****************************************************************************************\n');
        fprintf(1,'Cells:  This section lists all of the cell regions used in the analysis.  The "boundary"\n');
        fprintf(1,'field is a list of pointers to Hyperplanes in the Hyperplane list (above) that make up the region.\n');
        fprintf(1,'Each Hyperplane pointer has an associated flag that tells which side of the Hyerplane the region is on.\n');
        fprintf(1,'The "pthflags" field indicates which PTHB''s are true/false for each cell.\n');
        fprintf(1,'The initial cell(s) (i.e. the cell(s) where the inital continuous sets lie) are');
        for j=1:length(var.InitialCells)
            fprintf(1,' %d',var.InitialCells(j));
        end
        fprintf(1,'\n');
        fprintf(1,'*****************************************************************************************\n\n');
      
        for i=1:length(var.Cells)
            fprintf(1,'\nCell %d\n',i);
            disp(var.Cells{i})
        end
        
        %Locations
        fprintf(1,'*****************************************************************************************\n');
        fprintf(1,'Locations:  This section lists all of the PIHA Locations.  Locations correspond to discrete states\n');
        fprintf(1,'in the original system.  If more that one Stateflow block is present in the original system,\n');
        fprintf(1,'the locations listed here will be the cross product of the states in each machine.\n');
        fprintf(1,'All information about each location is listed here (invariants, transitions, etc.)\n');
        fprintf(1,'*****************************************************************************************\n');
      
        for i=1:length(var.Locations)
            fprintf(1,'\nLocations %d\n',i);
            disp(var.Locations{i})
            for j=1:length(var.Locations{i}.transitions)
                fprintf(1,'\nOutgoing transitions %d for location %d\n',j,i);
                    disp(var.Locations{i}.transitions{j})
                                
            end
        end
        
        %Clocks
        fprintf(1,'\n*****************************************************************************************\n');
        fprintf(1,'Clocks:  This section lists all of the clocks used for sampled data verification.\n');
        fprintf(1,'*****************************************************************************************\n\n');
      
        fprintf(1,'\n');
        disp(var.CLOCKBlocks)
           
        %SCSB's
        fprintf(1,'\n*****************************************************************************************\n');
        fprintf(1,'Switched Continuous System Blocks:  This section lists all of information about the SCSB''s from \n');
        fprintf(1,'the original system.\n');
        fprintf(1,'*****************************************************************************************\n\n');
      
        
        for j=1:length(var.SCSBlocks)
            fprintf(1,'SCSB %d\n',j);
            disp(var.SCSBlocks{j})
        end
        
        %PTHB's
        fprintf(1,'\n*****************************************************************************************\n');
        fprintf(1,'Polyhedral Threshold Blocks:  This section lists all of information about the PTHB''s from \n');
        fprintf(1,'the original system.\n');
        fprintf(1,'*****************************************************************************************\n\n');
      
        
        for j=1:length(var.PTHBlocks)
            fprintf(1,'PTHB %d\n',j);
            disp(var.PTHBlocks{j})
        end
        
        %FSMB's
        fprintf(1,'\n*****************************************************************************************\n');
        fprintf(1,'Finite State Machine Blocks:  This section lists all of FSMB''s and their associated states.\n');
        fprintf(1,'*****************************************************************************************\n\n');
      
        
        for j=1:length(var.FSMBlocks)
            fprintf(1,'FSM %d\n',j);
            disp(var.FSMBlocks{j})
        end
        
   
        diary off
    end
elseif isfield(var{1},'initstate')
    %Input is a GLOBAL_AUTOMATON    
    warning off
    delete GA_Data.txt
    warning on
    
    diary('GA_Data.txt')
    %File introduction
    fprintf(1,'\n\nThis file logs all of the information contained in the Checkmate variable GLOBAL_AUTOMATON\n');
    fprintf(1,'The GLOBAL_AUTOMATON variable is a structure that represents the automaton created from the \n');
    fprintf(1,'information contained in the GLOBAL_PIHA structure.  Essentially, regions of the state space in the\n');
    fprintf(1,'original system correspond to states in the GLOBAL_AUTOMATON.  The GLOBAL_AUTOMATA contains information about\n');
    fprintf(1,'guards, interior regions, and reachability mappings from one region to another.\n\n');
    fprintf(1,['\nThis file was written on ' date '\n']);
    fprintf(1,'*****************************************************************************************\n\n');
    
    for i=1:length(var)
        
        %Locations
        if isfield(var{i},'initstate')
            for j=1:length(var{i}.initstate)
                fprintf(1,'Initial state %d\n',j);
                disp(var{i}.initstate{j})
                fprintf(1,'Polytope corresponding to initial state %d for location %\n',j,i);
                var{i}.initstate{j}.polytope
                fprintf(1,'\n');
                for k=1:length(var{i}.initstate{j}.mapping)
                    fprintf(1,'Mapping %d corresponding to initial state %d for location %\n',k,j,i);
                    var{i}.initstate{j}.mapping{k}
                    fprintf(1,'\n');
                end
            end
        end
        for j=1:length(var{i}.interior_region)
            fprintf(1,'Interior region %d in location %d\n\n',j,i);
            for k=1:length(var{i}.interior_region{j}.state)
                fprintf(1,'State %d for interior region %d in location %d\n\n',k,j,i);
                disp(var{i}.interior_region{j}.state{k})
                fprintf(1,'Polytope representing state %d\n',k);
                var{i}.interior_region{j}.state{k}.polytope
                for m=1:length(var{i}.interior_region{j}.state{k}.mapping)
                    fprintf(1,'Polytope %d representing the mapping for state %d \n',m,k);
                    var{i}.interior_region{j}.state{k}.mapping{m}
                end
            end
        end
        
    end
    diary off
    
elseif ~isstr(var{1})&isreal(var{1})
    %Input is a GLOBAL_TRANSITION
    warning off
    delete GT_Data.txt
    warning on
    
    diary('GT_Data.txt')
    %File introduction
    fprintf(1,'\n\nThis file logs all of the information contained in the Checkmate variable GLOBAL_TRANSITION.\n');
    fprintf(1,'The GLOBAL_TRANSITION variable describes the transition system that Checkmate creates from the\n');
    fprintf(1,'information conatined in GLOBAL_AUTOMATON.  Each state in GLOBAL_AUTOMATON corresponds to a state\n');
    fprintf(1,'in GLOBAL_TRANSITION.  The mappings and children information contained in GLOBAL_AUTOMATON are used\n');
    fprintf(1,'to construct the connectivity for the transition system.\n');
    fprintf(1,'Model checking is ultimately performed on the transition system described in GLOBAL_TRANSITION.\n\n');
    fprintf(1,'Note:  The structures GLOBAL_XSYS2AUTO_MAP and GLOBAL_AUTO2XSYS_MAP are needed in order to understand\n'); 
    fprintf(1,'which sates in GLOBAL_TRANSITION correspond to which states in GLOBAL_AUTOMATON.\n');
    fprintf(1,['\nThis file was written on ' date '\n']);
    fprintf(1,'*****************************************************************************************\n\n');
    
    fprintf(1,'List of states: \n');
    for i=1:length(var)
        fprintf(1,'%d \n',i);
    end
    fprintf(1,'\n\nList of transitions:\n');
    for i=1:length(var)
        for j=length(var{i})
            fprintf(1,'{%d,%d}\n',i,var{i}(j));
        end
    end
    
    
    diary off
    
    
end