/[dtapublic]/sf_code/esrgpcpj/hyreach/doc/hyreachm/s_glo0/s_glo0.tex
ViewVC logotype

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 26 - (show annotations) (download) (as text)
Sat Oct 8 06:57:57 2016 UTC (7 years, 4 months ago) by dashley
File MIME type: application/x-tex
File size: 3535 byte(s)
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.

dashley@gmail.com
ViewVC Help
Powered by ViewVC 1.1.25