% ------------------------------------------------------------------ %
%                                                                    %
% Datei: dateien2.tex                                                %
% Autor: Oliver Nietsch                                              %
%                                                                    %
% Universitaet Hamburg                                               %
% Fachbereich Informatik                                             %
% Arbeitsbereich DBIS                                                %
%                                                                    %
% Thema: Diplomarbeit: Die Modellierung und Validierung dynamischen  %
%                      Systemverhaltens am Beispiel von StP/OMT      %
%                      und Tycoon                                    %
%                                                                    %
% Inhalt: LaTeX-Dokument: Diplomarbeit,                              %
%                         Anhang B: Anwendungsbeispiel Television    %
%                                                                    %
% Version vom 16. 4.1997                                             %
% ------------------------------------------------------------------ %

\chapter{Anwendungsbeispiel Television}
\label{Ann:TV}

\section{Statecharts}
\label{Ann:TVstatecharts}

\subsection{Zustand Television}
\label{Ann:TVChart1}

\begin{figure}[hbt]
  \begin{center}
    \ 
    \epsfig{figure=chart1.eps,width=15cm}
  \end{center}
\end{figure}

\newpage

\subsection{Verfeinerung Zustand Image}
\label{Ann:TVChart2}

\begin{figure}[hbt]
  \begin{center}
    \ 
    \epsfig{figure=chart2.eps,width=9cm,angle=90}
  \end{center}
\end{figure}

\newpage

\section{TL Repr"asentation}
\label{Ann:TVschnitt}

% \begin{scriptsize}
\begin{xple}
\k{module} statechartTelevision
(*
   System: statechartDemo
   File: statechartTelevision.tm
   Author: Oliver Nietsch
   Date: 07-OCT-1996
   Purpose: Creation of Television Statechart Elements
*)
\k{import}

  list set statechart

\k{export}

  \k{let} television = statechart.newChart()

  \k{Let} Event = television.Event
  \k{Let} Events = list.T(Event)
  \k{Let} Action = television.Action

  (* Auxiliary Functions *)
  \k{let} emptySet(A $<:$\k{Ok}) :set.T(A) = set.new(:A fun(element1, element2 :A) :Bool
    element1 == element2)

  (* Triggers *)
  \k{let} triggerPower = television.createPrimitiveEvent("{}power"{})
  \k{let} triggerProgrButton = television.createPrimitiveEvent("{}progr\_button"{})
  \k{let} triggerStandby = television.createPrimitiveEvent("{}standby"{})
  \k{let} triggerVtxt = television.createPrimitiveEvent("{}vtxt"{})
  \k{let} triggerSoundOff = television.createPrimitiveEvent("{}sound\_off"{})
  \k{let} triggerSoundOn = television.createPrimitiveEvent("{}sound\_on"{})
  \k{let} triggerDisplayProgr = television.createPrimitiveEvent("{}display\_progr"{})
  \k{let} triggerHidePicture = television.createPrimitiveEvent("{}hide\_picture"{})
  \k{let} triggerHideProgrNr = television.createPrimitiveEvent("{}hide\_progrNr"{})
  \k{let} triggerShowPage = television.createPrimitiveEvent("{}show\_page"{})

  (* Actions *)
  \k{let} actionSoundOff = television.createAction("{}sound\_off"{} triggerSoundOff \k{fun}() :\k{Ok} ok)
  \k{let} actionDisplayProgr = television.createAction("{}display\_progr"{}
    triggerDisplayProgr \k{fun}() :\k{Ok} ok)
  \k{let} actionSoundOn = television.createAction("{}sound\_on"{} triggerSoundOn \k{fun}() :\k{Ok} ok)
  \k{let} actionShowPage = television.createAction("{}show\_page"{}
    triggerShowPage \k{fun}() :\k{Ok} ok)

  (* States *)
  (* --- Videotxt substate --- *)
  \k{let} displayPage = television.createBasicState("{}Display\_Page"{}
    emptySet(:television.Action) emptySet(:television.Action)
    emptySet(:television.Activity))
  \k{let} getHundred = television.createBasicState("{}Get\_Hundred"{}
    emptySet(:television.Action) emptySet(:television.Action)
    emptySet(:television.Activity))
  \k{let} getTen = television.createBasicState("{}Get\_Ten"{} emptySet(:television.Action)
    emptySet(:television.Action) emptySet(:television.Activity))
  \k{let} actionSet = emptySet(:television.Action)
  set.insert(actionSet actionShowPage)
  \k{let} getOne = television.createBasicState("{}Get\_One"{} actionSet
    emptySet(:television.Action) emptySet(:television.Activity))  
  \k{let} stateSet = emptySet(:television.State)
  set.insert(stateSet displayPage)
  set.insert(stateSet getHundred)
  set.insert(stateSet getTen)
  set.insert(stateSet getOne)
  \k{let} actionSet = emptySet(:television.Action)
  set.insert(actionSet actionSoundOn)
  \k{let} videotxt = television.createCompositeOrState("{}Videotxt"{}
    emptySet(:television.Action) actionSet
    emptySet(:television.Activity) stateSet displayPage)

  (* --- Show\_ProgrNr substate --- *)
  \k{let} displayProgrNr = television.createBasicState("{}Display\_ProgrNr"{}
    emptySet(:television.Action) emptySet(:television.Action)
    emptySet(:television.Activity))
  \k{let} hideProgrNr = television.createBasicState("{}Hide\_ProgrNr"{}
    emptySet(:television.Action) emptySet(:television.Action)
    emptySet(:television.Activity))
  \k{let} stateSet = emptySet(:television.State)
  set.insert(stateSet displayProgrNr)
  set.insert(stateSet hideProgrNr)
  \k{let} showProgrNr = television.createCompositeOrState("{}Show\_ProgrNr"{}
    emptySet(:television.Action) emptySet(:television.Action)
    emptySet(:television.Activity) stateSet displayProgrNr)
  (* --- Show\_Picture substate --- *)
  \k{let} displayPicture = television.createBasicState("{}Display\_Picture"{}
    emptySet(:television.Action) emptySet(:television.Action)
    emptySet(:television.Activity))
  \k{let} hidePicture = television.createBasicState("{}Hide\_Picture"{} emptySet(:television.Action)
    emptySet(:television.Action) emptySet(:television.Activity))
  \k{let} stateSet = emptySet(:television.State)
  set.insert(stateSet displayPicture)
  set.insert(stateSet hidePicture)
  \k{let} showPicture = television.createCompositeOrState("{}Show\_Picture"{}
    emptySet(:television.Action) emptySet(:television.Action)
    emptySet(:television.Activity) stateSet displayPicture)

  (* --- Display substate --- *)
  \k{let} stateSet = emptySet(:television.State)
  set.insert(stateSet showPicture)
  set.insert(stateSet showProgrNr)
  \k{let} display = television.createCompositeAndState("{}Display"{} emptySet(:television.Action)
    emptySet(:television.Action) emptySet(:television.Activity) stateSet)

  (* --- Normal substate --- *)
  \k{let} actionSet = emptySet(:television.Action)
  set.insert(actionSet actionDisplayProgr)
  \k{let} setProgr = television.createBasicState("{}Set\_Progr"{} actionSet
    emptySet(:television.Action) emptySet(:television.Activity))
  \k{let} stateSet = emptySet(:television.State)
  set.insert(stateSet display)
  set.insert(stateSet setProgr)
  \k{let} normal = television.createCompositeOrState("{}Normal"{} emptySet(:television.Action)
    emptySet(:television.Action) emptySet(:television.Activity) stateSet setProgr)

  (* --- Image substate --- *)
  \k{let} stateSet = emptySet(:television.State)
  set.insert(stateSet normal)
  set.insert(stateSet videotxt)
  \k{let} image = television.createCompositeOrState("{}Image"{} emptySet(:television.Action)
    emptySet(:television.Action) emptySet(:television.Activity) stateSet normal)

  (* --- Sound substate --- *)
  \k{let} soundOn = television.createBasicState("{}Sound\_On"{} emptySet(:television.Action)
    emptySet(:television.Action) emptySet(:television.Activity))

  \k{let} mute = television.createBasicState("{}Mute"{} emptySet(:television.Action)
    emptySet(:television.Action) emptySet(:television.Activity))
  \k{let} stateSet = emptySet(:television.State)
  set.insert(stateSet soundOn)
  set.insert(stateSet mute)
  \k{let} sound = television.createCompositeOrState("{}Sound"{} emptySet(:television.Action)
    emptySet(:television.Action) emptySet(:television.Activity) stateSet soundOn)

  (* --- On substate --- *)
  \k{let} stateSet = emptySet(:television.State)
  set.insert(stateSet image)
  set.insert(stateSet sound)
  \k{let} on = television.createCompositeAndState("{}On"{} emptySet(:television.Action)
    emptySet(:television.Action) emptySet(:television.Activity) stateSet)

  (* --- Power\_On substate --- *)
  \k{let} standby = television.createBasicState("{}Standby"{} emptySet(:television.Action)
    emptySet(:television.Action) emptySet(:television.Activity))
  \k{let} stateSet = emptySet(:television.State)
  set.insert(stateSet standby)
  set.insert(stateSet on)
  \k{let} powerOn = television.createCompositeOrState("{}Power\_On"{}
    emptySet(:television.Action) emptySet(:television.Action)
    emptySet(:television.Activity) stateSet standby)

  (* --- Television superstate --- *)
  \k{let} powerOff = television.createBasicState("{}Power\_Off"{} emptySet(:television.Action)
    emptySet(:television.Action) emptySet(:television.Activity))
  \k{let} stateSet = emptySet(:television.State)
  set.insert(stateSet powerOff)
  set.insert(stateSet powerOn)
  \k{let} tv = television.createRootState("{}Television"{} emptySet(:television.Action)
    emptySet(:television.Action) emptySet(:television.Activity) stateSet powerOff)

  (* Transitions *)
  \k{let} trigger1 = list.cons(triggerPower list.new(:television.Event))
  \k{let} t1 = television.createNormalTransition(powerOff powerOn trigger1)
  \k{let} t2 = television.createNormalTransition(powerOn powerOff trigger1)
  \k{let} trigger2 = list.cons(triggerProgrButton list.new(:television.Event))
  \k{let} t3 = television.createNormalTransition(standby on trigger2)
  \k{let} t10 = television.createNormalTransition(display setProgr trigger2)
  \k{let} t15 = television.createNormalTransition(displayPage getHundred trigger2)
  \k{let} t16 = television.createNormalTransition(getHundred getTen trigger2)
  \k{let} t17 = television.createNormalTransition(getTen getOne trigger2)
  \k{let} trigger3 = list.cons(triggerStandby list.new(:television.Event))
  \k{let} t4 = television.createNormalTransition(on standby trigger3)
  \k{let} trigger4 = list.cons(triggerVtxt list.new(:television.Event))
  \k{let} action1 = emptySet(:television.Action)
  set.insert(:television.Action action1 actionSoundOff)
  \k{let} t5 = television.createTransitionWithActions(normal videotxt trigger4 action1)
  \k{let} t6 = television.createNormalTransition(videotxt display trigger4)
  \k{let} trigger5 = list.cons(triggerSoundOff list.new(:television.Event))
  \k{let} t7 = television.createNormalTransition(soundOn mute trigger5)
  \k{let} trigger6 = list.cons(triggerSoundOn list.new(:television.Event))
  \k{let} t8 = television.createNormalTransition(mute soundOn trigger6)
  \k{let} trigger7 = list.cons(triggerDisplayProgr list.new(:television.Event))
  \k{let} t9 = television.createNormalTransition(setProgr display trigger7)
  \k{let} trigger8 = list.cons(triggerHidePicture list.new(:television.Event))
  \k{let} t11 = television.createTransitionWithActions(displayPicture
    hidePicture trigger8 action1)
  \k{let} action2 = emptySet(:television.Action)
  set.insert(:television.Action action2 actionSoundOn)
  \k{let} t12 = television.createTransitionWithActions(hidePicture
    displayPicture trigger8 action2)
  \k{let} trigger9 = list.cons(triggerHideProgrNr list.new(:television.Event))
  \k{let} t13 = television.createNormalTransition(displayProgrNr hideProgrNr trigger9)
  \k{let} t14 = television.createNormalTransition(hideProgrNr displayProgrNr trigger9)
  \k{let} trigger10 = list.cons(triggerShowPage list.new(:television.Event))
  \k{let} t18 = television.createNormalTransition(getOne displayPage trigger10)


\k{end}; (* statechartTelevision *)
\end{xple}
% \end{scriptsize}

\newpage

\section{Szenariobasierter Validierungslauf}
\label{Ann:SzenVal}

\begin{table}[hbt]
\begin{center}
\begin{tabular}{|l|l|l|}
\hline
{\bf Konfiguration} & {\bf Ereignis} & {\bf Folgekonfiguration}\\
\hline\hline
{\sl Television}, {\sl Power\_On}, {\sl Standby} & {\sl progr\_button} & {\sl Television}, {\sl Power\_On}, {\sl On},\\
                                                 &                     & {\sl Image}, {\sl Normal}, {\sl Display},\\
                                                 &                     & {\sl Show\_Picture}, {\sl Display\_Picture},\\
                                                 &                     & {\sl Show\_ProgrNr}, {\sl Display\_ProgrNr},\\
                                                 &                     & {\sl Sound}, {\sl Sound\_On}\\
\hline
$\vdots$                           & $\vdots$            & $\vdots$\\
\hline
{\sl Television}, {\sl Power\_On}, {\sl On}, & {\sl vtxt} & {\sl Television}, {\sl Power\_On}, {\sl On},\\
{\sl Image}, {\sl Normal}, {\sl Display},    &            & {\sl Image}, {\sl Videotxt}, {\sl Display\_Page},\\
{\sl Show\_Picture}, {\sl Display\_Picture}, &            & {\sl Sound}, {\sl Sound\_Off}\\
{\sl Show\_ProgrNr}, {\sl Display\_ProgrNr}, &            & \\
{\sl Sound}, {\sl Sound\_On}                 &            & \\
\hline
$\vdots$                           & $\vdots$            & $\vdots$\\
\hline
{\sl Television}, {\sl Power\_On}, {\sl On},      & {\sl vtxt} & {\sl Television}, {\sl Power\_On}, {\sl On},\\
{\sl Image}, {\sl Videotxt}, {\sl Display\_Page}, &            & {\sl Image}, {\sl Normal}, {\sl Display},\\
{\sl Sound}, {\sl Sound\_Off}                     &            & {\sl Show\_Picture}, {\sl Display\_Picture},\\
                                                  &            & {\sl Show\_ProgrNr}, {\sl Display\_ProgrNr},\\
                                                  &            & {\sl Sound}, {\sl Sound\_Off}\\
\hline
{\sl Television}, {\sl Power\_On}, {\sl On}, & {\sl sound\_off} & {\sl Television}, {\sl Power\_On}, {\sl On},\\
{\sl Image}, {\sl Normal}, {\sl Display},    &                  & {\sl Image}, {\sl Normal}, {\sl Display},\\
{\sl Show\_Picture}, {\sl Display\_Picture}, &                  & {\sl Show\_Picture}, {\sl Display\_Picture},\\
{\sl Show\_ProgrNr}, {\sl Display\_ProgrNr}, &                  & {\sl Show\_ProgrNr}, {\sl Display\_ProgrNr},\\
{\sl Sound}, {\sl Sound\_Off}                &                  & {\sl Sound}, {\sl Sound\_Off}\\
\hline
{\sl Television}, {\sl Power\_On}, {\sl On}, & {\sl standby} & {\sl Television}, {\sl Power\_On}, {\sl Standby}\\
{\sl Image}, {\sl Normal}, {\sl Display},    &               & \\
{\sl Show\_Picture}, {\sl Display\_Picture}, &               & \\
{\sl Show\_ProgrNr}, {\sl Display\_ProgrNr}, &               & \\
{\sl Sound}, {\sl Sound\_Off}                &               & \\
\hline
\end{tabular}
\end{center}
\label{Tab:DynVal2}
\end{table}

\clearemptydoublepage
