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 |