Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • T08-changes
  • fix-apt-get
  • emily
  • 2019Final
  • 2018Final
  • 2017Final
7 results
Blame Permalink
Code owners
Assign users and groups as approvers for specific file changes. Learn more.
MazeTracingRobot.tex 20.87 KiB 
%\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}{18 Maze Tracing Robot Example}

\input{../titlepage}

\begin{document}

\input{../footline}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Maze Tracing Robot Example}

\begin{itemize}
\item Administrative details
\item Index set example
\item Solar water heating tank example
\item Modules with external interaction
\item Dr.\ v.\ Mohrenschildt's maze tracing robot (see GitLab)
\item MIS for maze\_storage
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Administrative Details}

\begin{itemize}

\item Assignment 2
\begin{itemize}
\item {Files due by 11:59 pm Feb 19}
\item {File automatically sent to partners on Feb 20}
\item Lab report due by 11:59 pm Feb 27
\item {When returning an object, you can either create a new object or
    return a reference}
\item {\texttt{totalArea} is just the sum of the area of all circles,
    do not worry about overlap}
\item {Removed POS exception from syntax}
\item {Implementation does NOT have to look like the
    spec}
\end{itemize}

\item Midterm exam
\begin{itemize}
\item March 1, 7:00 pm, TSH/120
\item 90 minute duration
\item Multiple choice - 30--40 questions?
\item Open book (any paper)
\end{itemize}

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Index Set}

Write a function \texttt{indexSet(x, B)} that takes a value \texttt{x} and a
list of values \texttt{B} and returns a list of indices where \texttt{B[i] =
  x}.\\
~\newline
As a first step, how would you say this mathematically?

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Index Set}

Write a function \texttt{indexSet(x, B)} that takes a value \texttt{x} and a
list of values \texttt{B} and returns a list of indices where \texttt{B[i] =
  x}.\\

$$\mbox{indexSet}(x, B) \equiv \{i : \mathbb{N} | i \in [0 .. |B|-1] \wedge B_i =
x : i\}$$

How could you use \texttt{indexSet} to calculate \texttt{rank(x, A)}?

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Anticipated Changes}

\bi
\item The specific hardware on which the software is to run
\item The format of the initial input data
\item The format of the input parameters
\item The constraints on the input parameters
\item The format of the output data
\item The constraints on the output results
\item How the governing ODEs are defined using the input parameters
\item How the energy equations are defined using the input parameters
\item How the overall control of the calculations is orchestrated
\item The implementation of the sequence data structure
\item The algorithm used for the ODE solver
\item The implementation of plotting data
\ei

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Module Hierarchy by Secrets}
\begin{table}[h!]
\centering
\begin{tabular}{p{0.3\textwidth} p{0.6\textwidth}}
\toprule
\textbf{Level 1} & \textbf{Level 2}\\
\midrule

{Hardware-Hiding Module} & ~ \\
\midrule

\multirow{6}{0.3\textwidth}{Behaviour-Hiding Module} & Input Format Module\\
& Input Parameters Module\\
& Output Format Module\\
& Temperature ODEs Module\\
& Energy Equations Module\\ 
& Control Module\\
\midrule

\multirow{3}{0.3\textwidth}{Software Decision Module} & {Sequence Data Structure Module}\\
& ODE Solver Module\\
& Plotting Module\\
\bottomrule

\end{tabular}
\caption{Module Hierarchy}
\label{TblMH}
\end{table}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Example Modules from SWHS}

\textbf{Hardware Hiding Modules}

\begin{description}
\item[Secrets:]The data structure and algorithm used to implement the virtual
  hardware.
\item[Services:]Serves as a virtual hardware used by the rest of the
  system. This module provides the interface between the hardware and the
  software. So, the system can use it to display outputs or to accept inputs.
\item[Implemented By:] OS
\end{description}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Example Modules from SWHS}

\textbf{Input Verification Module}

\begin{description}
\item[Secrets:] The rules for the physical and software constraints.
\item[Services:] Verifies that the input parameters comply with physical and
  software constraints. Throws an error if a parameter violates a physical
  constraint. Throws a warning if a parameter violates a software constraint.
\item[Implemented By:] SWHS
\end{description}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Example Modules from SWHS}

\textbf{ODE Solver Module}

\begin{description}
\item[Secrets:] The algorithm to solve a system of first order ODEs.
\item[Services:] Provides solvers that take the governing equation, initial
  conditions, and numerical parameters, and solve them.
\item[Implemented By:] Matlab
\end{description}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[plain, fragile]

\frametitle{SWHS Uses Hierarchy}

\begin{center}
\includegraphics[scale=0.55]{UsesHierarchy.pdf}
\end{center}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Modules with External Interaction}

\begin{itemize}
\item In general, some modules may interact with the environment or other modules
%\item The Display Point Masses Applet module does this
\item Environment might include the keyboard, the screen, the file system, motors, sensors, etc.
\item Sometimes the interaction is informally specified using prose (natural language)
\item Can introduce an environment variable
\begin{itemize}
\item Name, type
\item Interpretation
\end{itemize}
\item Environment variables include the screen, the state of a motor (on, direction of rotation, power level, etc.),
the position of a robot

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{External Interaction Continued}

\begin{itemize}
\item Some external interactions are hidden
\begin{itemize}
\item Present in the implementation, but not in the MIS
\item An example might be OS memory allocation calls
\end{itemize}
\item External interaction described in the MIS
\begin{itemize}
\item Naming access programs of the other modules
\item Specifying how the other module's state variables are changed
\item The MIS should identify what external modules are used
\end{itemize}
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{MIS for GUI Modules}

\begin{itemize}
\item Could introduce an environment variable
\item window: sequence [RES\_H][RES\_V] of pixelT
\begin{itemize}
\item Where window[r][c] is the pixel located at row r and column c, with numbering zero-relative and beginning at the
upper left corner
\item Would still need to define pixelT
\end{itemize}
\item Could formally specify the environment variable transitions
\item More often it is reasonable to specify the transition in prose
\item In some cases the proposed GUI might be shown by rough sketches
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Display Point Masses Module Syntax}

\textbf{Exported Access Programs}\\
~\newline
\begin{tabular}{| l | l | l | l |}
\hline
\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exc.}\\
\hline
DisplayPointMassesApplet & ~ & DisplayPointMassesApplet & ~\\
\hline
paint & ~ & ~ & ~\\
\hline
\end{tabular}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Display Point Masses Module Semantics}

\textbf{Environment Variables}\\
$\mathit{win}:$ 2D sequence of pixels displayed within a web-browser \\

\noindent DisplayPointMassesApplet():
\begin{itemize}
\item transition: The state of the abstract object ListPointMasses is modified as follows:\\
ListPointMasses.init()\\
ListPointMasses.add(0, PointMassT(20, 20, 10)\\
ListPointMasses.add(1, PointMassT(120, 200, 20)\\
...
\end{itemize}

\noindent paint():
\begin{itemize}
\item transition $win := $ Modify window so that the point masses in ListPointMasses 
are plotted as circles.  The centre of each circles should be the corresponding x and y coordinates and the radius should
be the mass of the point mass.
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Assignment 3 Vector Module}

\textbf {Exported Access Programs}\\
~\newline
\begin{tabular}{| l | l | l | p{0.75in} |}
\hline
\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
\hline
new vectorT & real $\rightarrow$ real & vectorT & ~\\
\hline
getf & ~ & real $\rightarrow$ real & ~\\
\hline
eval & real, real, integer & sequence of real & deltaNeg, nstepsNeg\\
\hline
evalPrint & real, real, integer & ~ & deltaNeg, nstepsNeg\\
\hline
\end{tabular}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Vector Module Semantics}

\textbf{Environment Variables}\\
$\mathit{screen}$ : two dimensional sequence of positions on the screen, which each position holding a character\\
~\newline
\textbf{State Variables}\\
$f$: real $\rightarrow$ real\\
~\newline
\textbf{Access Routine Semantics}\\
\noindent eval ($\mathit{startx}, \mathit{deltax}, \mathit{nsteps}$):
\begin{itemize}
\item output: $out := < f(\mathit{startx}), f(\mathit{startx} + \mathit{deltax}), f(\mathit{startx} + 2 \cdot \mathit{deltax}), ...
, f(\mathit{startx} + \mathit{nsteps} \cdot \mathit{deltax})>$
\item exception: $exc := ((\mathit{deltax} < 0) \Rightarrow  \mbox{deltaNeg} | (\mathit{nsteps} < 0) \Rightarrow
\mbox{nstepsNeg})$
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Vector Module Semantics Continued}

\noindent evalPrint ($\mathit{startx}, \mathit{deltax}, \mathit{nsteps}$):
\begin{itemize}
\item transition: The state of $\mathit{screen}$ is modified so that the sequence returned by eval ($\mathit{startx}$,
$\mathit{deltax}$, $\mathit{nsteps}$) is displayed.
\item exception: $exc := ((\mathit{deltax} < 0) \Rightarrow  \mbox{deltaNeg} | (\mathit{nsteps} < 0) \Rightarrow
\mbox{nstepsNeg})$
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Dr.\ v.\ Mohrenschildt's Maze Tracing Robot Example}

\begin{figure}
\includegraphics[scale=0.42]{ExampleMaze.pdf}
\end{figure}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Maze Tracing Robot Expected Changes}

\begin{itemize}
\item Changes to the geometry of the robot such that the mapping from a position to the robot inputs is different
\item Changes to the interface to the robot
\item Changes to the format of the maze
\item Changes to any constant values
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Maze Tracing Robot Uses Hierarchy}

\begin{figure}[H]
\includegraphics[scale=0.42]{UsesHierarchyBetter.pdf}
\end{figure}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Maze Tracing Robot MG}
\begin{itemize}
\item \structure<1>{Module name:} maze\_storage
\begin{itemize}
\item \structure<1>{Secret:} how the maze is stored
\item \structure<1>{Service:} stores the maze
\item \structure<1>{Module prefix:} ms\_
\end{itemize}
\item \structure<1>{Module name:} load\_maze
\begin{itemize}
\item \structure<1>{Secret:} where and how the maze file is read in
\item \structure<1>{Service:} loads the maze
\item \structure<1>{Module prefix:} lm\_
\end{itemize}
\item \structure<1>{Module name:} find\_path
\begin{itemize}
\item \structure<1>{Secret:} the algorithm for finding the shortest path
\item \structure<1>{Service:} finds the shortest path through the maze
\item \structure<1>{Module prefix:} fp\_
\end{itemize}
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Maze Tracing Robot MG Continued}
\begin{itemize}
\item \structure<1>{Module name:} control
\begin{itemize}
\item \structure<1>{Secret:} how the arm moves from position to position and how the buttons are checked
\item \structure<1>{Service:} controls the movement of the arm
\item \structure<1>{Module prefix:} cn\_
\end{itemize}
\item \structure<1>{Module name:} geometry
\begin{itemize}
\item \structure<1>{Secret:} how the calculations from cell coords to robot coords are performed
\item \structure<1>{Service:} handles geometric positioning of the arm
\item \structure<1>{Module prefix:} gm\_
\end{itemize}
\item \structure<1>{Module name:} hardware
\begin{itemize}
\item \structure<1>{Secret:} how it interfaces with the robot
\item \structure<1>{Service:} handles hardware aspects of arm (movement and button checking)
\item \structure<1>{Module prefix:} hw\_
\end{itemize}
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Maze Tracing Robot MG Continued}
\begin{itemize}
\item \structure<1>{Module name:} types\_constants
\begin{itemize}
\item \structure<1>{Secret:} how the data structures are defined and constants defined
\item \structure<1>{Service:} provides standard variable types and constants to modules
\end{itemize}
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{maze\_storage MIS}

\textbf{Module}\\
~\newline
maze\_storage\\
~\newline

\textbf{Uses}\\
~\newline
types\_constants\\
~\newline

\textbf{Exported Access Programs}\\
~\newline
\begin{tabular}{| l | l | l | l |}
\hline
\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
\hline
... & ... & ... & ...\\
\hline
%any thoughts from the class on the design of the interface?
\end{tabular}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{maze\_storage Exported Access Programs}

\begin{tabular}{| l | l | l | p{3.5cm} |}
\hline
\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
\hline
ms\_init & ~ & ~ & ~\\
\hline
ms\_set\_maze\_start & cell & ~ & ms\_not\_initialized, ms\_cell\_out\_of\_range\\
\hline
ms\_set\_maze\_end & cell & ~ & ms\_not\_initialized, ms\_cell\_out\_of\_range\\
\hline
ms\_get\_maze\_start & ~ & cell & ms\_not\_initialized\\
\hline
ms\_get\_maze\_end & ~ & cell & ms\_not\_initialized\\
\hline
ms\_set\_wall & cell, cell & ~ & ms\_not\_initialized, ms\_not\_valid\_wall\\
\hline
ms\_is\_connected & cell, cell & boolean & ms\_not\_initialized, ms\_cell\_out\_of\_range\\
\hline
\end{tabular}\\
~\newline
cell = tuple of (x: integer, y: integer)
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{maze\_storage Semantics}

\textbf{State Variables}\\
~\newline
\uncover<2->{\structure<2>{$\mathit{maze}$: set of tuple of ( cell, cell )}}\\
\uncover<2->{\structure<2>{$\mathit{start}: \mbox{cell} $}}\\
\uncover<2->{\structure<2>{$\mathit{end}: \mbox{cell} $}}\\
\uncover<2->{\structure<2>{$\mathit{is\_init}: \mbox{boolean} := \mathit{false}$}}\\

~\newline
\textbf{State Invariant:} none\\
% there could be one related to maximum size of the map
~\newline
\textbf{Assumptions}\\
~\newline
ms\_get\_maze\_start and ms\_get\_maze\_end are not called until after the corresponding set routines have been called.

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Access Routine Semantics}

\noindent ms\_init():
\begin{itemize}
\item transition: \uncover<2->{\structure<2>{$\mathit{maze}, \mathit{is\_init} := \{ \}, \mathit{true}$}}
\item exception: \uncover<2->{\structure<2>{none}}
\end{itemize}

\noindent ms\_set\_maze\_start(c):
\begin{itemize}
\item transition: \uncover<3->{\structure<3>{$start := c$}}
\item exception: \uncover<4->{\structure<4>{$exc := (\neg \mathit{is\_init} \Rightarrow \mbox{ms\_not\_initialized } |
\mbox{ } \neg \mbox{cell\_in\_range}(c) \Rightarrow \mbox{ms\_cell\_out\_of\_range})$}}
\end{itemize}

\noindent ms\_set\_maze\_end(c):
\begin{itemize}
\item transition: \uncover<3->{\structure<3>{$end := c$}}
\item exception: \uncover<4->{\structure<4>{$exc := (\neg \mathit{is\_init} \Rightarrow \mbox{ms\_not\_initialized } |
\mbox{ } \neg \mbox{cell\_in\_range}(c) \Rightarrow \mbox{ms\_cell\_out\_of\_range})$}}
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Access Routine Semantics Continued}

\noindent ms\_get\_maze\_start():
\begin{itemize}
\item output: \uncover<2->{\structure<2>{$\mathit{out} := \mathit{start}$}}
\item exception: \uncover<3->{\structure<3>{$exc := (\neg \mathit{is\_init} \Rightarrow \mbox{ms\_not\_initialized})$}}
\end{itemize}

\noindent ms\_get\_maze\_end():
\begin{itemize}
\item output: \uncover<2->{\structure<2>{$\mathit{out} := \mathit{end}$}}
\item exception: \uncover<3->{\structure<3>{$exc := (\neg \mathit{is\_init} \Rightarrow \mbox{ms\_not\_initialized})$}}
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Access Routine Semantics Continued}

\noindent ms\_set\_wall(c1, c2):
\begin{itemize}
\item transition: \uncover<2->{\structure<2>{$\mathit{maze} := \mathit{maze} \cup \{ < c1, c2 > \}$}}
\item exception: \uncover<3->{\structure<3>{$exc := (\neg \mathit{is\_init} \Rightarrow \mbox{ms\_not\_initialized } |
\mbox{ wall\_is\_point}(c1, c2) \vee \mbox{wall\_is\_diagonal}(c1, c2) \vee \mbox{wall\_is\_out\_of\_range}(c1, c2)
\Rightarrow \mbox{ms\_not\_valid\_wall})$}}
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Access Routine Semantics Continued}

\noindent ms\_is\_connected(c1, c2):
\begin{itemize}
\item output: \uncover<2->{\structure<2>{$out := < c1, c2 > \in \mathit{maze}$}}
\item exception: \uncover<3->{\structure<3>{$exc := (\neg \mathit{is\_init} \Rightarrow \mbox{ms\_not\_initialized } |
\mbox{ } \neg \mbox{cell\_in\_range}(c1) \Rightarrow \mbox{ms\_cell\_out\_of\_range } |
\mbox{ } \neg \mbox{cell\_in\_range}(c2) \Rightarrow \mbox{ms\_cell\_out\_of\_range} )$}}
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Local Functions}

\noindent cell\_in\_range : cell $\rightarrow$ boolean
\begin{itemize}
\item \uncover<2->{\structure<2>{cell\_in\_range (c) $\equiv (0 \leq c.x < \mbox{MAX\_NUM\_CELLS}) \wedge (0 \leq c.y <
\mbox{MAX\_NUM\_CELLS})$}}
\end{itemize}

\noindent wall\_is\_point: cell $\times$ cell $\rightarrow$ boolean
\begin{itemize}
\item \uncover<3->{\structure<3>{wall\_is\_point (c1, c2) $\equiv c1 = c2$}}
\end{itemize}

\noindent wall\_is\_diagonal: cell $\times$ cell $\rightarrow$ boolean
\begin{itemize}
\item \uncover<4->{\structure<4>{wall\_is\_diagonal (c1, c2) $\equiv \neg ( (c1.x = c2.x) \vee (c1.y = c2.y) )$}}
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Additional Specifications for Determining the Path}

pathT = sequence of cell\\
~\newline

\noindent validPath : pathT $\rightarrow$ boolean
\begin{itemize}
\item \uncover<2->{\structure<2>{validPath (p) $\equiv (p[0] = \mbox{ms\_get\_maze\_start}() 
\wedge p[|p| - 1] = \mbox{ms\_get\_maze\_end}()
\wedge \forall (i:\mathbb{N} | 0 \leq i \leq |p| - 2 : \mbox{ms\_is\_connected}(p[i], p[i+1]) )$}}
\end{itemize}
~\newline
\uncover<3->{\structure<3>{How would you specify the length of a wall?}}\\
\uncover<4->{\structure<4>{lengthWall: tuple of cell $\rightarrow$ integer}}\\
\uncover<4->{\structure<4>{$$\mbox{lengthWall}(<c1, c2>) \equiv (c1.x = c2.x \Rightarrow | c1.y - c2.y |$$}}
\uncover<4->{\structure<4>{$$ |  c1.y = c2.y \Rightarrow | c1.x - c2.x |)$$}}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Shortest Path}

How would you specify the length of a path?\\
\uncover<2->{\structure<2>{lengthPath: pathT $\rightarrow$ integer}}\\
\uncover<2->{\structure<2>{$$\mbox{lengthPath}(p) \equiv + (i: \mathbb{N} | 0 \leq i < (|p| -1 ) : \mbox{lengthWall}(<p_i, p_{i+1} >))+1$$}}
% the plus 1 is added because the length does not include the last point
\noindent How would you specify whether a path is the shortest path?\\
\uncover<3->{\structure<3>{isShortest: pathT $\rightarrow$ boolean}}\\
\uncover<3->{\structure<3>{$$\mbox{isShortest}(p) = \forall ( q : \mbox{pathT} $$}}
\uncover<3->{\structure<3>{$$|\mbox{validPath}(q) : \mbox{validPath}(p) \wedge \mbox{lengthPath}(p) \leq \mbox{lengthPath}(q))$$}}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\end{document}