Skip to content
Snippets Groups Projects
Commit 52a6ea1d authored by W. Spencer Smith's avatar W. Spencer Smith
Browse files

Revisions to L23. just started version of L24.

parent d87390c7
No related branches found
No related tags found
No related merge requests found
No preview for this file type
......@@ -400,6 +400,26 @@ $\mathbf{c}$ & - & - & - & $q_0$\\
\begin{frame}
\frametitle{When to use FSMs for Specification?}
\bi
\item \structure{When is an FSM a good choice for specification?}
\item \structure{What are some examples of things we would specify using an FSM?}
\ei
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{When to Potentially use FSMs}
\bi
\item Describing control flow
\item Clear finite set of states (or modes)
\item Specify acceptable strings for a parser
\item Specifying hardware design
\item For synchronous models (at any time a global state must be defined and a
single transition must occur)
\ei
\end{frame}
......@@ -481,7 +501,7 @@ to be $k_1 + k_2 + ... + k_n$)
\begin{itemize}
\item Events can be viewed as ``pulses'' in time - they do not last (retain their values)
\item Conditions may retain their values idefinitely
\item Conditions may retain their values indefinitely
\end{itemize}
\end{frame}
......
%\documentclass[t,12pt,numbers,fleqn,handout]{beamer}
\documentclass[t,12pt,numbers,fleqn]{beamer}
\usepackage{pgfpages}
\usepackage{hyperref}
\hypersetup{colorlinks=true,
linkcolor=blue,
citecolor=blue,
filecolor=blue,
urlcolor=blue,
unicode=false}
\urlstyle{same}
\usepackage{booktabs}
\usepackage{multirow}
\useoutertheme{split} %so the footline can be seen, without needing pgfpages
% \pgfpagesuselayout{resize to}[letterpaper,border
% shrink=5mm,landscape] %if this is uncommented, the hyperref links do not work
\mode<presentation>{}
\input{../def-beamer}
\newcommand{\topic}{24 Generics and Interfaces in Java}
\input{../titlepage}
\begin{document}
\input{../footline}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Finite State Machines}
\begin{itemize}
\item Administrative details
\item Classification of specification styles
\item Continuation on specification qualities
\item Homework exercise
\item How to verify a specification
\item Finite state machines
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Administrative Details}
\begin{itemize}
\item Some of today's slides adapted from Dr.\ Wassyng's slides (and Ghezzi et al)
\item A3 deadlines
\begin{itemize}
\item Part 1 - Specification: due 11:59 pm Mar 8
\item Part 2 - Code: due 11:59 pm Mar 20
\end{itemize}
\item A4
\bi
\item Your own design and specification
\item Due April 3 at 11:59 pm
\ei
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Same Symbol/Term Different Meaning}
\begin{itemize}
\item \structure{Can you think of some symbols/terms that have different
meanings depending on the context?}
\item \href{http://writingexplained.org/homonyms-and-homophones}{Homonyms}
\bi
\item Homograph - same spelling different meaning, maybe different pronunciation
(ex.\ bank, bow, biweekly, ...)
\item Homophone - same pronunciation, but different meaning, origin or spelling
(ex.\ new/knew, to/too/two, ...)
\ei
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Consistent}
\begin{itemize}
\item Language and terminology must be consistent within the specification
\item Potential problem with homonyms, for instance consider the symbol $\sigma$
\begin{itemize}
\item Represents standard deviation
\item Represents stress
\item Represents the Stefan-Boltzmann constant (for radiative heat transfer)
\end{itemize}
\item Changing the symbol may be necessary for consistency, but it could adversely effect understandability
\item Potential problem with \href{https://en.wikipedia.org/wiki/Synonym}{synonyms}
\begin{itemize}
\item Externally funded graduate students, versus eligible graduate students, versus non-VISA students
%ask who would think about graduate school?
%\item Material behaviour model versus constitutive equation
\item Enter key versus Return key
\item \structure{Other examples?}
\end{itemize}
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Complete}
\begin{itemize}
\item Internal completeness
\begin{itemize}
\item The specification must define any new concept or terminology that it uses
\begin{itemize}
\item A glossary is helpful for this purpose
\end{itemize}
\end{itemize}
\item External completeness
\begin{itemize}
\item The specification must document all the needed requirements
\begin{itemize}
\item Difficulty: when should one stop?
\end{itemize}
\end{itemize}
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Incremental}
\begin{itemize}
\item Referring to the specification process
\begin{itemize}
\item Start from a sketchy document and progressively add details
\item A document template can help with this
\end{itemize}
\item Referring to the specification document
\begin{itemize}
\item Document is structured and can be understood in increments
\item Again a document template can help with this
\end{itemize}
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Another Example}
\begin{itemize}
\item Operational specification
\begin{itemize}
\item ``Let $a$ be an array of $n$ elements. The result of its sorting is an array $b$ of $n$ elements such that the
first element of $b$ is the minimum of $a$ (if several elements of a have the same value, any one of them is acceptable);
the second element of $b$ is the minimum of the array of $n-1$ elements obtained from $a$ by removing its minimum
element; and so on until all $n$ elements of $a$ have been removed.''
\end{itemize}
\item Descriptive specification
\begin{itemize}
\item ``The result of sorting array $a$ is an array $b$ which is a permutation of $a$ and is sorted.''
\item \structure<1>{How can we further specify (formalize) the notion of sorted?}
\item <2-> \structure<2>{$\mbox{sorted}(A) \equiv \forall ( i : \mathbb{N} | 0 \leq i \leq (|A| - 2) : A[i] \leq
A[i+1])$}
\end{itemize}
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Classification of Specification Styles}
\begin{itemize}
\item Informal, semi-formal, formal
\item Operational
\begin{itemize}
\item Behaviour specification in terms of some abstract machine
\end{itemize}
\item Descriptive
\begin{itemize}
\item Behaviour described in terms of properties
\end{itemize}
\item The module state machine specification that we use is a mix of operational
and descriptive specification - \structure{Why?}
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Example Operational Specification}
\begin{itemize}
\item Specification of a geometric figure $E$
\item $E$ can be drawn as follows
\begin{enumerate}
\item Select two points $P_1$ and $P_2$ on a plane
\item Get a string of a certain length and fix its ends to $P_1$ and $P_2$
\item Position a pencil as shown in the next figure
\item Move the pen clockwise, keeping the string tightly stretched, until you reach the point where you started
drawing
\end{enumerate}
\end{itemize}
\begin{figure}
\includegraphics[scale=0.35]{../Figures/DrawingACircle.png}
\end{figure}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Example Descriptive Specification}
Geometric figure $E$ is described by the following equation
$$ a x^2 + b y^2 + c = 0 $$
where $a$, $b$ and $c$ are suitable constants
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Homework Exercise}
\begin{itemize}
\item Consider the \textbf{line formatter} specification and
\be
\item How well does the specification do with respect to the following
qualities: abstract, correct, unambiguous, complete, consistent and verifiable?
\item For a requirement specification like that given, what are the advantages
and disadvantages of maintaining both a formal specification and a natural
language specification?
\ee
\item Even spending 5 minutes thinking about will help when we discuss next week
\item In repo
\bi
\item The
\href{https://gitlab.cas.mcmaster.ca/smiths/se2aa4_cs2me3/tree/master/Lectures/LineFormatter}{line
formatter specification}
\item
\href{https://gitlab.cas.mcmaster.ca/smiths/se2aa4_cs2me3/blob/master/ReferenceMaterial/Meyer1985.pdf}{Meyer
(1985)} ``On Formalism in Specification''
\ei
\item Will discuss next day
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{How to Verify a Specification}
\begin{itemize}
\item \structure{Observe} dynamic behaviour of the specified system
\begin{itemize}
\item Simulation
\item Prototyping
\item ``testing'' the specification
\end{itemize}
\item Analyze properties of the specified system
\item Analogy with traditional engineering
\begin{itemize}
\item Physical model of a bridge (prototype)
\item Mathematical model of a bridge
\end{itemize}
\item We will return to this topic when we cover verification (Chapter 6)
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Finite State Machines (FSMs)}
\begin{itemize}
\item Can specify control flow aspects
\item Defined as
\begin{itemize}
\item A finite set of states $Q$
\item A finite set of inputs $I$
\item A transition function $\delta: Q \times I \rightarrow Q$ ($\delta$ can be a partial function)
\end{itemize}
\end{itemize}
\begin{figure}
\includegraphics[scale=0.25]{../Figures/StateTransitionDiagram.png}
\end{figure}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{FSMs Continued}
~\newline
\begin{tabular}{| c | c | c| c| c|}
\hline
~ & $\mathbf{q_0}$ & $\mathbf{q_1}$ & $\mathbf{q_2}$ & $\mathbf{q_3}$\\
\hline
$\mathbf{a}$ & $q_1$ & $q_2$ & - & -\\
\hline
$\mathbf{b}$ & - & $q_3$ & $q_3$ & - \\
\hline
$\mathbf{c}$ & - & - & - & $q_0$\\
\hline
\end{tabular}
\begin{figure}
\includegraphics[scale=0.25]{../Figures/StateTransitionDiagram.png}
\end{figure}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Example: A Lamp}
\bi
\item \structure{What are the states $Q$ for a typical lamp?}
\item \structure{What are the set of inputs $I$}
\item \structure{What is the transition function $\delta$?}
\ei
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Example: A Lamp}
\begin{figure}
\includegraphics[scale=0.45]{../Figures/ExampleLamp.png}
\end{figure}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Example: A Plant Control System}
\begin{figure}
\includegraphics[scale=0.45]{../Figures/PlantControlSystem.png}
\end{figure}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{A Refinement}
\begin{figure}
\includegraphics[scale=0.45]{../Figures/ARefinement.png}
\end{figure}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{When to use FSMs for Specification?}
\bi
\item \structure{When is an FSM a good choice for specification?}
\item \structure{What are some examples of things we would specify using an FSM?}
\ei
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{When to Potentially use FSMs}
\bi
\item Describing control flow
\item Clear finite set of states (or modes)
\item Specify acceptable strings for a parser
\item Specifying hardware design
\item For synchronous models (at any time a global state must be defined and a
single transition must occur)
\ei
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Classes of FSMs}
\begin{itemize}
\item Deterministic/nondeterministic
\item FSMs as recognizers - introduce final states
\item FSMs as transducers - introduce set of output
\item ...
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{FSMs as Recognizers}
\begin{figure}
\includegraphics[scale=0.5]{../Figures/FSM_as_Recognizers.png}
\end{figure}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{FSMs as Recognizers Continued}
\begin{figure}
\includegraphics[scale=0.5]{../Figures/FSM_as_Recognizers2.png}
\end{figure}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Limitations}
\begin{itemize}
\item Finite memory
\item State explosion - Given a number of FSMs with $k_1, k_2, ... k_m$ states, their composition is an FSM with $k1
\times k_2 \times ... \times k_n$. This growth is exponential with the number of FSMs, not linear (we would like it
to be $k_1 + k_2 + ... + k_n$)
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{State Explosion: An Example}
\begin{figure}
\includegraphics[scale=0.5]{../Figures/StateExplosionExample.png}
\end{figure}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{The Resulting FSM}
\begin{figure}
\includegraphics[scale=0.5]{../Figures/StateExplosionResult.png}
\end{figure}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Events Versus Conditions}
\begin{itemize}
\item Events can be viewed as ``pulses'' in time - they do not last (retain their values)
\item Conditions may retain their values idefinitely
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{FSM Example: Security Alarm}
\begin{figure}
\includegraphics[scale=0.45]{../Figures/Security.pdf}
\end{figure}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Security Alarm Example Continued}
\begin{figure}
\includegraphics[scale=0.6]{../Figures/States_ass4.pdf}
\end{figure}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment