--- a/doc-src/TutorialI/CTL/document/Base.tex Tue Oct 03 01:15:11 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex Tue Oct 03 11:26:54 2000 +0200
@@ -18,33 +18,66 @@
very efficient one. The main proof obligation is to show that the semantics
and the model checker agree.
-Our models are transition systems.
+\underscoreon
-START with simple example: mutex or something.
+Our models are \emph{transition systems}, i.e.\ sets of \emph{states} with
+transitions between them, as shown in this simple example:
+\begin{center}
+\unitlength.5mm
+\thicklines
+\begin{picture}(100,60)
+\put(50,50){\circle{20}}
+\put(50,50){\makebox(0,0){$p,q$}}
+\put(61,55){\makebox(0,0)[l]{$s_0$}}
+\put(44,42){\vector(-1,-1){26}}
+\put(16,18){\vector(1,1){26}}
+\put(57,43){\vector(1,-1){26}}
+\put(10,10){\circle{20}}
+\put(10,10){\makebox(0,0){$q,r$}}
+\put(-1,15){\makebox(0,0)[r]{$s_1$}}
+\put(20,10){\vector(1,0){60}}
+\put(90,10){\circle{20}}
+\put(90,10){\makebox(0,0){$r$}}
+\put(98, 5){\line(1,0){10}}
+\put(108, 5){\line(0,1){10}}
+\put(108,15){\vector(-1,0){10}}
+\put(91,21){\makebox(0,0)[bl]{$s_2$}}
+\end{picture}
+\end{center}
+Each state has a unique name or number ($s_0,s_1,s_2$), and in each
+state certain \emph{atomic propositions} ($p,q,r$) are true.
+The aim of temporal logic is to formalize statements such as ``there is no
+transition sequence starting from $s_2$ leading to a state where $p$ or $q$
+are true''.
Abstracting from this concrete example, we assume there is some type of
-atomic propositions%
+states%
+\end{isamarkuptext}%
+\isacommand{typedecl}\ state%
+\begin{isamarkuptext}%
+\noindent
+which we merely declare rather than define because it is an implicit
+parameter of our model. Of course it would have been more generic to make
+\isa{state} a type parameter of everything but fixing \isa{state} as above
+reduces clutter.
+Similarly we declare an arbitrary but fixed transition system, i.e.\
+relation between states:%
+\end{isamarkuptext}%
+\isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+Again, we could have made \isa{M} a parameter of everything.
+Finally we introduce a type of atomic propositions%
\end{isamarkuptext}%
\isacommand{typedecl}\ atom%
\begin{isamarkuptext}%
\noindent
-which we merely declare rather than define because it is an implicit parameter of our model.
-Of course it would have been more generic to make \isa{atom} a type parameter of everything
-but fixing \isa{atom} as above reduces clutter.
-
-Instead of introducing both a separate type of states and a function
-telling us which atoms are true in each state we simply identify each
-state with that set of atoms:%
+and a \emph{labelling function}%
\end{isamarkuptext}%
-\isacommand{types}\ state\ {\isacharequal}\ {\isachardoublequote}atom\ set{\isachardoublequote}%
+\isacommand{consts}\ L\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ atom\ set{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-Finally we declare an arbitrary but fixed transition system, i.e.\ relation between states:%
-\end{isamarkuptext}%
-\isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}%
-\begin{isamarkuptext}%
-\noindent
-Again, we could have made \isa{M} a parameter of everything.%
+telling us which atomic propositions are true in each state.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables: