# Contents of /sf_code/esrgpcpj/hyreach/doc/hyreachm/s_glo0/s_glo0.tex

Initial commit.

 1 %$Header: /cvsroot/esrg/sfesrg/esrgpcpj/hyreach/doc/hyreachm/s_glo0/s_glo0.tex,v 1.4 2002/01/29 17:04:00 dtashley Exp$ 2 % 3 \section{Glossary Of Terms} 4 \label{sglo0} 5 6 \begin{glossaryenum} 7 \item \textbf{CHM}\index{CHM} \\ 8 \emph{C}omposite \emph{h}ybrid \emph{m}achine. A timed automaton which is 9 created by \swname{} by combining the state-spaces of all EHMs supplied as 10 input using a well-defined mathematical operation. In general, each location 11 of a CHM corresponds to one location from each EHM. 12 \item \textbf{configuration}\index{configuration} \\ 13 See \emph{location}. 14 \item \textbf{EHM}\index{EHM} \\ 15 \emph{E}lementary \emph{h}ybrid \emph{m}achine. A timed automaton supplied 16 as input to \swname{}. 17 \item \textbf{location}\index{location} \\ 18 The discrete component of an EHM's state. The state of an EHM is divided into 19 two components: 20 \begin{itemize} 21 \item The discrete state, which is usually shown on a state transition diagram 22 as a circle or a rectangle. 23 \item The values of clocks which the EHM sets and tests. These values are 24 conceptually continuous, but for machine representation reasons are 25 confined to integers. 26 \end{itemize} 27 The \emph{location} is the disctete state only. 28 \item \textbf{on-the-fly}\index{on-the-fly} \\ 29 Creating (dynamically allocating) the locations of a CHM as needed during 30 verification, rather than in 31 advance. For analyzing reachability, creating locations of a CHM before verification 32 begins has performance disadvantages for three reasons: 33 \begin{itemize} 34 \item A large number of CHM locations may not be reachable, and so are not used 35 during the verification. Creating these locations is a wasted motion. 36 \item In the event that an illegal location is reachable, in most cases 37 creating all CHM locations 38 in advance will greatly slow down finding 39 that the illegal location is reachable. Because a model with illegal 40 states reachable usually requires correction, this will slow down the 41 development cycle in which \swname{} is being used. 42 \item For models with a very large state space, not all symbolic information for 43 all locations can be 44 kept in memory at one time (and it is not necessary to do so). For large 45 models, it is not 46 possible to create all locations in advance. 47 \end{itemize} 48 \end{glossaryenum} 49 50 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 51 \noindent\begin{figure}[!b] 52 \noindent\rule[-0.25in]{\textwidth}{1pt} 53 \begin{tiny} 54 \begin{verbatim} 55 $RCSfile: s_glo0.tex,v$ 56 $Source: /cvsroot/esrg/sfesrg/esrgpcpj/hyreach/doc/hyreachm/s_glo0/s_glo0.tex,v$ 57 $Revision: 1.4$ 58 $Author: dtashley$ 59 $Date: 2002/01/29 17:04:00$ 60 \end{verbatim} 61 \end{tiny} 62 \noindent\rule[0.25in]{\textwidth}{1pt} 63 \end{figure} 64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 65 %$Log: s_glo0.tex,v$ 66 %Revision 1.4 2002/01/29 17:04:00 dtashley 67 %Version control info added, and minor edits. 68 % 69 %Revision 1.3 2001/10/31 04:31:37 dtashley 70 %Nightly safety checkin. 71 % 72 %Revision 1.2 2001/10/01 06:08:09 dtashley 73 %Basic hacks in place for a workable document. 74 % 75 %Revision 1.1 2001/09/26 02:31:14 dtashley 76 %Initial checkin, and some edits of main TEX file. 77 % 78 %End of S_GLO0.TEX.