Addition of A3 Part 1 Solution, Specification for Part 2.

Assignments/A3/A3Soln/Assig3Part1Solution_Specification.tex

+\documentclass[12pt]{article}
+
+\usepackage{graphicx}
+\usepackage{paralist}
+\usepackage{amsfonts}
+
+\oddsidemargin 0mm
+\evensidemargin 0mm
+\textwidth 160mm
+\textheight 200mm
+\renewcommand\baselinestretch{1.0}
+
+\pagestyle {plain}
+\pagenumbering{arabic}
+
+\newcounter{stepnum}
+
+\title{Assignment 3, Part 1, Specification}
+\author{SFWR ENG 2AA4}
+
+\begin {document}
+
+\maketitle
+
+The purpose of this software design exercise is to design and implement a
+portion of the specification for an autonomous rescue robot.  This document
+shows the complete specification, which will be the basis for your
+implementation and testing.
+
+\newpage
+
+\section* {Constants Module}
+
+\subsection*{Module}
+
+Constants
+
+\subsection* {Uses}
+
+N/A
+
+\subsection* {Syntax}
+
+\subsubsection* {Exported Constants}
+
+MAX\_X = 180 {\it //dimension in the x-direction of the problem area}\\
+MAX\_Y = 160 {\it //dimension in the y-direction of the problem area}\\ 
+TOLERANCE = 5 {\it //space allowance around obstacles}\\
+VELOCITY\_LINEAR = 15 {\it //speed of the robot when driving straight}\\
+VELOCITY\_ANGULAR = 30 {\it //speed of the robot when turing}
+
+\subsubsection* {Exported Access Programs}
+
+none
+
+\subsection* {Semantics}
+
+\subsubsection* {State Variables}
+
+none
+
+\subsubsection* {State Invariant}
+
+none
+
+\newpage
+
+\section* {Point ADT Module}
+
+\subsection*{Template Module}
+
+PointT
+
+\subsection* {Uses}
+
+Constants
+
+\subsection* {Syntax}
+
+\subsubsection* {Exported Types}
+
+PointT = ?
+
+\subsubsection* {Exported Access Programs}
+
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+PointT & real, real & PointT & InvalidPointException\\
+\hline
+xcrd & ~ & real & ~\\
+\hline
+ycrd & ~ & real & ~\\
+\hline
+dist & PointT & real & ~\\
+\hline
+\end{tabular}
+
+\subsection* {Semantics}
+
+\subsubsection* {State Variables}
+
+$xc$: real\\
+$yc$: real
+
+\subsubsection* {State Invariant}
+
+none
+
+\subsubsection* {Assumptions}
+The constructor PointT is called for each abstract object before any other
+access routine is called for that object.  The constructor cannot be called on
+an existing object.
+
+\subsubsection* {Access Routine Semantics}
+
+PointT($x, y$):
+\begin{itemize}
+\item transition: $xc, yc := x, y$
+\item output: $out := \mathit{self}$
+\item exception
+ $exc := ((\neg(0 \leq x \leq \mbox{Contants.MAX\_X}) \vee \neg(0 \leq y \leq \mbox{Constants.MAX\_Y})) \Rightarrow
+\mbox{InvalidPointException})$
+\end{itemize}
+
+\noindent xcrd():
+\begin{itemize}
+\item output: $out := xc$
+\item exception: none
+\end{itemize}
+
+\noindent ycrd():
+\begin{itemize}
+\item output: $out := yc$
+\item exception: none
+\end{itemize}
+
+\noindent dist($p$):
+\begin{itemize}
+\item output: $out := \sqrt{(\mathit{self}.xc - p.xc)^2 + (\mathit{self}.yc - p.yc)^2}$
+\item exception: none
+\end{itemize}
+
+\newpage
+
+\section* {Region Module}
+
+\subsection* {Template Module}
+
+RegionT
+
+\subsection* {Uses}
+
+PointT
+
+\subsection* {Syntax}
+
+\subsubsection* {Exported Types}
+
+RegionT = ?
+
+\subsubsection* {Exported Access Programs}
+
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+RegionT & PointT, real, real & RegionT & InvalidRegionException\\
+\hline
+pointInRegion & PointT & boolean & ~\\
+\hline 
+\end{tabular}
+
+\subsection* {Semantics}
+
+\subsubsection* {State Variables}
+
+$\mathit{lower\_left}$: PointT {\it //coordinates of the lower left corner of the region}\\
+$\mathit{width}$: real {\it //width of the rectangular region}\\
+$\mathit{height}$: real {\it //height of the rectangular region}
+
+\subsubsection* {State Invariant}
+None
+
+\subsubsection* {Assumptions}
+The RegionT constructor is called for each abstract object before any other
+access routine is called for that object.  The constructor can only be called
+once.
+
+\subsubsection* {Access Routine Semantics}
+
+\noindent RegionT($p, w, h$):
+\begin{itemize}
+\item transition: $\mathit{lower\_left}, \mathit{width}, \mathit{height} := p, w, h$
+\item output: $out := \mathit{self}$
+\item exception: 
+\begin{eqnarray*}
+\lefteqn{exc := \neg ( w > 0 \wedge}\\
+& &  h > 0 \wedge\\
+& &  (p.\mbox{xcrd}() + w) < \mbox{Constants.MAX\_X} \wedge\\
+& &  (p.\mbox{ycrd}() + h) < \mbox{Constants.MAX\_Y})  \Rightarrow \mbox{InvalidRegionException}
+\end{eqnarray*}
+\end{itemize}
+
+\noindent pointInRegion($p$):
+\begin{itemize}
+\item output: $\mathit{out} := \exists ( q: \mbox{PointT} | q \in \mbox{Region} : p.\mbox{dist}(q) \leq \mbox{Constants.TOLERANCE})$
+\item exception: none
+\end{itemize}
+
+\subsubsection* {Local Functions}
+
+Region: set of PointT\\
+\begin{eqnarray*}
+\lefteqn{\mbox{Region} \equiv \cup (q: \mbox{PointT} |}\\
+& & \mathit{lower\_left}.\mbox{xcrd} \leq q.\mbox{xcrd} \leq (\mathit{lower\_left}.\mbox{xcrd} + \mathit{width})
+\wedge\\
+& & \mathit{lower\_left}.\mbox{ycrd} \leq q.\mbox{ycrd} \leq (\mathit{lower\_left}.\mbox{ycrd} + \mathit{height}):
+\{ q \} )
+\end{eqnarray*}
+
+\newpage
+
+\section* {Generic List Module}
+
+\subsection* {Generic Template Module}
+
+GenericList(T)
+
+\subsection* {Uses}
+
+N/A
+
+\subsection* {Syntax}
+
+\subsubsection* {Exported Types}
+GenericList(T) = ?
+
+\subsubsection* {Exported Constants}
+
+MAX\_SIZE = 100
+
+\subsubsection* {Exported Access Programs}
+
+\begin{tabular}{| l | l | l | p{5cm} |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+GenericList & ~ & GenericList & ~\\
+\hline
+add & integer, T & ~ & FullSequenceException,\newline InvalidPositionException\\
+\hline
+del & integer & ~ & InvalidPositionException\\
+\hline
+setval & integer, T & ~ & InvalidPositionException\\
+\hline
+getval & integer & T & InvalidPositionException\\
+\hline
+size & ~ & integer & ~\\
+\hline
+
+\end{tabular}
+
+\subsection* {Semantics}
+
+\subsubsection* {State Variables}
+
+$s$: sequence of T
+
+\subsubsection* {State Invariant}
+
+$| s | \leq \mathrm{MAX\_SIZE}$
+
+\subsubsection* {Assumptions}
+
+The GenericList() constructor is called for each abstract object before any
+other access routine is called for that object.  The constructor can only be
+called once.
+
+\subsubsection* {Access Routine Semantics}
+
+GenericList():
+\begin{itemize}
+\item transition: $\mathit{self}.s := < >$
+\item output: $\mathit{out} := \mathit{self}$
+\item exception: none
+\end{itemize}
+
+\noindent add($i, p$):
+\begin{itemize}
+\item transition: $s := s[0..i-1] || <p> || s[i..|s|-1]$
+\item exception: $exc := (|s| = \mathrm{MAX\_SIZE} \Rightarrow  \mathrm{FullSequenceException} ~ | ~ i \notin [0..|s|] \Rightarrow
+\mathrm{InvalidPositionException})$
+\end{itemize}
+
+\noindent del($i$):
+\begin{itemize}
+\item transition: $s := s[0..i-1] || s[i+1..|s|-1]$
+\item exception:  $exc := (i \notin [0..|s|-1] \Rightarrow \mathrm{InvalidPositionException})$
+\end{itemize}
+
+\noindent setval($i, p$):
+\begin{itemize}
+\item transition: $s[i] := p$
+\item exception: $exc := (i \notin [0..|s|-1] \Rightarrow \mathrm{InvalidPositionException})$
+\end{itemize}
+
+\noindent getval($i$):
+\begin{itemize}
+\item output: $out := s[i]$
+\item exception: $exc := (i \notin [0..|s|-1] \Rightarrow \mathrm{InvalidPositionException})$
+\end{itemize}
+
+\noindent size():
+\begin{itemize}
+\item output: $out := | s |$
+\item exception: none
+\end{itemize}
+
+\newpage
+
+\section* {Path Module}
+
+\subsection* {Template Module}
+
+PathT is GenericList(PointT)
+
+\section* {Obstacles Module}
+
+\subsection* {Template Module}
+
+Obstacles is GenericList(RegionT)
+
+\section* {Destinations Module}
+
+\subsection* {Template Module}
+
+Destinations is GenericList(RegionT)
+
+\section* {SafeZone Module}
+
+\subsection* {Template Module}
+
+SafeZone extends GenericList(RegionT)
+
+\subsection*{Exported Constants}
+MAX\_SIZE = 1
+
+%\section* {Path List Module}
+
+%\subsection* {Template Module}
+
+%PathListT is GenericList(PathT)
+
+\newpage
+
+\section* {Map Module}
+
+\subsection* {Module}
+
+Map
+
+\subsection* {Uses}
+
+Obstacles, Destinations, SafeZone
+
+\subsection* {Syntax}
+
+\subsubsection* {Exported Access Programs}
+
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+init & Obstacles, Destinations, SafeZone & ~ & ~\\
+\hline
+get\_obstacles & ~ & Obstacles & ~\\
+\hline
+get\_destinations & ~ & Destinations & ~\\
+\hline
+get\_safeZone & ~ & SafeZone & ~\\
+\hline
+
+\end{tabular}
+
+\subsection* {Semantics}
+
+\subsubsection*{State Variables}
+$\mathit{obstacles}:$ Obstacles\\
+$\mathit{destinations}:$ Destinations\\
+$\mathit{safeZone}:$ SafeZone
+
+\subsubsection* {State Invariant}
+none
+
+\subsubsection* {Assumptions}
+The access routine init() is called for the abstract object before any other access routine is called.  If the map is
+changed, init() can be called again to change the map.
+
+\subsubsection* {Access Routine Semantics}
+
+\noindent init($o, d, \mathit{sz}$):
+\begin{itemize}
+\item transition: $\mathit{obstacles}, \mathit{destinations}, \mathit{safeZone}  := o, d, \mathit{sz}$
+\item exception: none
+\end{itemize}
+
+\noindent get\_obstacles():
+\begin{itemize}
+\item output: $\mathit{out} := \mathit{obstacles}$
+\item exception: none
+\end{itemize}
+
+\noindent get\_destinations():
+\begin{itemize}
+\item output: $\mathit{out} := \mathit{destinations}$
+\item exception: none
+\end{itemize}
+
+\noindent get\_safeZone():
+\begin{itemize}
+\item output: $\mathit{out} := \mathit{safeZone}$
+\item exception: none
+\end{itemize}
+
+\newpage
+
+\section* {Path Calculation Module}
+
+\subsection* {Module}
+
+PathCalculation
+
+\subsection* {Uses}
+
+Constants, PointT, RegionT, PathT, Obstacles, Destinations, SafeZone, Map
+
+\subsection* {Syntax}
+
+\subsubsection* {Exported Access Programs}
+
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+is\_validSegment & PointT, PointT & boolean & ~\\
+\hline
+is\_validPath & PathT & boolean & ~\\
+\hline
+is\_shortestPath & PathT & boolean & ~\\
+\hline
+totalDistance & PathT & real & ~\\
+\hline
+totalTurns & PathT & integer & ~\\
+\hline
+estimatedTime & PathT & real & ~\\
+\hline
+%sortPathList & PathListT & PathListT & ~\\
+%\hline
+
+\end{tabular}
+
+\subsection* {Semantics}
+
+\noindent is\_validSegment($p_1, p_2$):
+\begin{itemize}
+\item output: $\mathit{out} := \forall (i: \mathbb{N}| 0 \leq i < \mbox{Map.get\_obstacles.size()} :
+\mbox{is\_valid\_segment\_for\_region}(p_1, p_2, i))$
+\item exception: none
+\end{itemize}
+
+\noindent is\_validPath($p$):
+\begin{itemize}
+\item output: 
+\begin{eqnarray*}
+\lefteqn{\mathit{out} := }\\
+& & \mbox{Map.get\_safeZone.getval}(0).\mbox{pointInRegion}(p.\mbox{getval}(0)) \wedge\\
+& & \mbox{Map.get\_safeZone.getval}(0).\mbox{pointInRegion}(p.\mbox{getval}(p.\mbox{size()} -1)) \wedge\\
+& & \forall (i: \mathbb{N} | 0 \leq i < \mbox{Map.get\_destinations.size()} :
+\mbox{pathPassesThroughDestination}(p, i)) \wedge\\
+& & \forall (i: \mathbb{N} | 0 \leq i < p.\mbox{size()}-1 :
+\mbox{is\_validSegment}(p.\mbox{getval}(i), p.\mbox{getval}(i+1)))\\
+\end{eqnarray*}
+\item exception: none
+\end{itemize}
+
+\noindent is\_shortestPath($p$):
+\begin{itemize}
+\item output: 
+$$\mathit{out} := \forall (q: \mbox{PathT}| \mbox{is\_validPath}(q) : \mbox{is\_validPath}(p) \wedge
+\mbox{totalDistance}(p) \leq \mbox{totalDistance}(q))$$
+\item exception: none
+\end{itemize}
+
+\noindent totalDistance($p$):
+\begin{itemize}
+\item output: 
+$$\mathit{out} := + (i: \mathbb{N}| 0 \leq i < (p.\mbox{size}()-1) :
+p.\mbox{getval}(i).\mbox{dist}(p.\mbox{getval}(i+1)))$$
+\item exception: none
+\end{itemize}
+
+\noindent totalTurns($p$):
+\begin{itemize}
+\item output: 
+$$\mathit{out} := + (i: \mathbb{N}| 0 \leq i < (p.\mbox{size}()-2) :
+\mbox{angle}(p.\mbox{getval}(i), p.\mbox{getval}(i+1), p.\mbox{getval}(i+2)) \neq 0 : 1)$$
+\item exception: none
+\end{itemize}
+
+\noindent estimatedTime($p$):
+\begin{itemize}
+\item output: 
+$\mathit{out} := \mbox{linear\_time}(p) + \mbox{angular\_time}(p)$
+\item exception: none
+\end{itemize}
+
+\subsubsection* {Local Functions}
+\noindent \textbf{is\_valid\_segment\_for\_region}: PointT $\times$ PointT $\times$ integer $\rightarrow$ boolean\\
+$\mbox{is\_valid\_segment\_for\_region}(p_1, p_2, i) \equiv$
+$$\forall (t: \mathbb{R} | 0 \leq t \leq 1 : \neg
+\mbox{Map.get\_obstacles.getval}(i).\mbox{pointInRegion}(t p_1 + (1 - t) p_2 ))$$
+
+\noindent \textbf{pathPassesThroughDestination}: PathT $\times$ integer $\rightarrow$ boolean\\
+$\mbox{pathPassesThroughDestination}(p, i) \equiv$
+$$\exists(q: \mbox{PointT} | q \in \mbox{Path} : \mbox{Map.get\_destinations.getval}(i).\mbox{pointInRegion}(q))$$
+\noindent where Path $\equiv p$.  This solution assumes that the sequence of points in the path include points within the
+destination regions.  This assumption is fine, but if one decided not to make this assumption, then the definition of Path is a
+little more involved, as follows:
+$$Path \equiv \cup ( i: \mathbb{N} | 0 \leq i < (p.\mbox{size}() - 1) :\mbox{LineSeg}(p.\mbox{getval}(i),
+p.\mbox{getval}(i + 1)))$$
+
+\noindent where LinSeg: set of PointT, $\mbox{LinSeg}(p_1, p_2) \equiv \cup (t :\mathbb{R} | 0 \leq t \leq 1 : \{ t p_1 +
+(1 - t) p_2
+\} )$.
+~\newline
+
+\noindent \textbf{angle}: PointT $\times$ PointT $\times$ PointT $\rightarrow$ real\\
+$\mbox{angle}(p_1, p_2, p_3) \equiv \cos^{-1} \left ( \frac {\mathbf{u} \cdot \mathbf{v}}{|| \mathbf{u} || ||
+\mathbf{v} ||} \right )$
+\noindent where $\mathbf{u} = \mathbf{p_2} - \mathbf{p_1}$, $\mathbf{v} = \mathbf{p_3} - \mathbf{p_2}$, $||
+\mathbf{u} || = p_1.\mbox{dist}(p_2)$ and $||\mathbf{v} || = p_2.\mbox{dist}(p_3)$, with $\mathbf{p_i}$ being the
+vector from the origin to the point $p_i$ for $i \in [1..3]$.
+
+~\newline
+
+\noindent \textbf{linear\_time}: PathT $\rightarrow$ real\\
+$$\mbox{linear\_time}(p) \equiv + \left ( i : \mathbb{N} | 0 \leq i < p.\mbox{size}() - 1 :
+\frac{p.\mbox{getval}(i).\mbox{dist}(p.\mbox{getval}(i+1))}{\mbox{Constants.VELOCITY\_LINEAR}} \right )$$
+
+~\newline
+
+\noindent \textbf{angular\_time}: PathT $\rightarrow$ real\\
+$$\mbox{angular\_time}(p) \equiv + \left ( i : \mathbb{N} | 0 \leq i < p.\mbox{size}() - 2 :
+\frac{\mbox{angle}(p.\mbox{getval}(i), p.\mbox{getval}(i+1), p.\mbox{getval}(i+2))}{\mbox{Constants.VELOCITY\_ANGULAR}}
+\right )$$
+\end {document}
\ No newline at end of file