GLOBAL VARIABLES

CheckMate uses many global variables to track progress and data throughout the verification process.  Below is an explanation of the purpose and structure of each variable.
 

Variable Name
Description
Structure
GLOBAL_ITERATION
Stores the number of iterations in the verification process.  At any point in the process, GLOBAL_ITERATION contains the number of the last completed iteration. double array
GLOBAL_SYSTEM
Contains the name of the Simulink model representing the threshold event driven hybrid system (TEDHS). character array (string)
GLOBAL_APARAM Contains the name of a Matlab function file which returns a structure of approximation parameters as a function of the composite discrete state. character array (string)

function should return a structure with the following fields:
 .dir_tol tolerance for patch "single-sided-ness"
 .var_tol tolerance for patch vector field variation relative to the vector field variation on the parent invariant face.
 .size_tol tolerance for patch size
 .W (diagonal) weighting matrix
 .T time step for flow pipe computation
 .max_time time limit (sec) for mapping computation
 .eq_tol equilibrium termination tolerance for mapping computation

GLOBAL_SPEC
Contains the ACTL specification to be verified character array (string)
GLOBAL_PROGRESS
Contains the current verification step structure array

with field:
 .step current step of process

GLOBAL_PIHA
Polyhedral Invariant Hybrid Automata (PIHA) model converted from Simulink system specified in GLOBAL_SYSTEM structure array

with fields:
 .Hyperplanes List of threshold hyperplanes in the C/E system
 .NAR Number of hyperplanes on analysis boundary
 .InitialContinuousSet Set of initial continuous states
 .InitialDiscreteSet Set of initial discrete states
 .Cells List of cells in the continuous state space 
partition
 .InitialCells List of cells which overlaps with the initial continuous set
 .Locations List of hybrid automaton locations
 .InitialLocations Indices to initial locations
 .SCSBlocks List of switch continuous system blocks in the C/E system
 .PTHBlocks List of polyhedral threshold blocks in the C/E system
  .FSMBlocks List of finite state machine blocks in the C/E system

 GLOBAL_AUTOMATON Contains the current approximating automaton cell array

Each cell is a structure with the fields:
 .initstate discretization of initial continuous set for each location
 .face{i}.state discretization of ith invariant face for each location

Each state has the following components:
 .polytope Continuous set for this state.
 .mapping Continuous mapping computed from polytope.
 .children Destination states.
 .null_event There exists trajectories that never trigger any further event from the polytope for this state.
 .time_limit Mapping computation terminated by time limit so the mapping may not contain all states in mapping set.
 .out_of_bound Part of the mapping computed goes out of analysis region.
 .indeterminate Cannot determine further evolution of the system from this state. Reasons maybe that polytope for this state contains singularities so that mapping cannot be computed. This flag must be set by the user. 
 .terminal If there exists a trajectory from the polytope for this state that causes the FSM to switch to a terminal FSM state q', i.e the FSM state for which there is no outgoing transition from any of the component states, then the cell array .terminal contains q', otherwise it is empty.

 GLOBAL_TRANSITION
Generic transition system representing "flattened out" GLOBAL_AUTOMATON cell array
 GLOBAL_REV_TRANSITION
Reverse transition system of GLOBAL_TRANSITION cell array
 GLOBAL_AUTO2XSYS_MAP
State map from GLOBAL_AUTOMATON to GLOBAL_TRANSITION structure array

with fields:
 .init_state_map{l}{s} Gives the index of the state in GLOBAL_TRANSITION corresponding to the initial state s in the location l in GLOBAL_AUTOMATON
 .init_state_range Gives the range of states in GLOBAL_TRANSITION that correspond to states in the initial state partition in GLOBAL_AUTOMATON
 .face_state_map{l}{f}{s} Gives the index of the state in GLOBAL_TRANSITION corresponding to state s on face f of invariant of location l in GLOBAL_AUTOMATON
 .face_state_range Gives the range of states in GLOBAL_TRANSITION that correspond to states in the face state partition in GLOBAL_AUTOMATON
 .ne_start Gives the starting index for "null_event" states in GLOBAL_TRANSITION 
 .tl_start Gives the starting index for "time limit" states in GLOBAL_TRANSITION
 .oob_start Gives the starting index for "out-of-bound" states in GLOBAL_TRANSITION
 .ind_start Gives the starting index for "indeterminate" states in GLOBAL_TRANSITION 

 GLOBAL_XSYS2AUTO_MAP
State map from GLOBAL_TRANSITION to GLOBAL_AUTOMATON cell array
 GLOBAL_SPEC_TREE
Parse tree for ACTL specification structure array

with fields:
.symbol Type name of terminal or variable symbols (string)
.production Name of production that is used to obtain the symbol's value (next field). Valid only for state formula symbols
.value Cell array of symbol nodes comprising the current symbol value

 GLOBAL_AP_BUILD_LIST
Atomic proposition build list cell array

each cell is a structure with fields:
.name The name of the atomic proposition. For a polyhedral threshold atomic proposition, this is the name of the corresponding PTHB. For a finite state machine atomic proposition, the name is <FSMB>_in_<state>.
.build_info Specifies the type of each atomic propositon. For a PTHAP, this is poly_ap. For an FSMAP, it is a cell array of the form {'fsmap' <FSMB> <state>}.

 GLOBAL_AP
Atomic propositions structure array

with fields:
.ap Contains the region object describing where the ap is true. There is one field for each ap in GLOBAL_SPEC.

 GLOBAL_TBR
Set of states in GLOBAL_TRANSITION that are "to-be-refined" region object
 GLOBAL_NEW_AUTOMATON
New approximating automaton obtained by refining GLOBAL_AUTOMATON cell array

Each cell is a structure with the fields:
 .initstate discretization of initial continuous set for each location
 .face{i}.state discretization of ith invariant face for each location

Each state has the following components:
 .polytope Continuous set for this state.
 .mapping Continuous mapping computed from polytope.
 .children Destination states.
 .null_event There exists trajectories that never trigger any further event from the polytope for this state.
 .time_limit Mapping computation terminated by time limit so the mapping may not contain all states in mapping set.
 .out_of_bound Part of the mapping computed goes out of analysis region.
 .indeterminate Cannot determine further evolution of the system from this state. Reasons maybe that polytope for this state contains singularities so that mapping cannot be computed. This flag must be set by the user. 
 .terminal If there exists a trajectory from the polytope for this state that causes the FSM to switch to a terminal FSM state q', i.e the FSM state for which there is no outgoing transition from any of the component states, then the cell array .terminal contains q', otherwise it is empty.

 GLOBAL_RAUTO_REMAP_LIST
List of refined states in GLOBAL_NEW_AUTOMATON for which the mapping needs to be computed cell array
 GLOBAL_RAUTO_FACE_MAP
State map from face states in GLOBAL_AUTOMATON to face states in GLOBAL_NEW_AUTOMATON cell array