Changeset 200 for docs/trunk/omega-test-slides/omega-test.tex

Legend:

Unmodified

Added

Removed

• docs/trunk/omega-test-slides/omega-test.tex

  r199	r200
  514	514	\[ a\beta \leq abx \leq b\alpha \]
  515	515
  516	We can eliminate $x$ ($a\beta \leq b\alpha$; termed $C_R,ドル the ``real'' shadow) but there may (削除) be solutions to that but not the original (削除ここまで).
  516	We can eliminate $x$ ($a\beta \leq b\alpha$; termed $C_R,ドル the ``real'' shadow) but there may (追記) then be solutions to that were not originally present (追記ここまで).
  517	517
  518	518	\begin{itemize}
  …	…
  678	678	\end{itemize}
  679	679	~\\
  680	\begin{tabular}{cccc}
  680
  681
  682	\begin{tabular}{ccc|c}
  681	683	$C_R = C_D$ & $\operatorname{hasIntSol}(C_R)$ & $\operatorname{hasIntSol}(C_D)$ & $\operatorname{hasIntSol}(C)$ \\
  682	684	\hline
  683	(削除) (削除ここまで)\\
  685	(追記) ~&~&~& (追記ここまで)\\
  684	686	%\tick & & & $ = \operatorname{hasIntSol}(C_R)$ \\
  685	687	\tick & \tick & & \tick \\
  686	688	\tick & \cross & & \cross \\
  687	\cross & \cross & & \cross \\
  688	\cross & \tick & \tick & \tick \\
  689	\\
  690	\hline
  691	\only<2->{\cross & \tick & \cross & Difficult! \\}
  689	\only<2->{\cross & \cross & & \cross \\}
  690	\only<3->{\cross & \tick & \tick & \tick \\}
  691	\only<4->{\cross & \tick & \cross & Difficult! \\}
  692	\only<-1>{~&~&~&\\}
  693	\only<-2>{~&~&~&\\}
  694	\only<-3>{~&~&~&\\}
  692	695	\end{tabular}
  693	696
  …	…
  702	705
  703	706	\begin{frame}[fragile]
  704	\frametitle{What do we know in the difficult case?}
  705	\begin{itemize}
  707	\frametitle{What Do We Know in the Difficult Case?}
  708	\begin{itemize}
  709	\item Recall: $hasIntSol(C_D) \implies b\alpha - a\beta > ab - a - b$
  706	710	\item $\lnot hasIntSol(C_D) \implies b\alpha - a\beta \leq ab - a - b$
  707	711	\item $hasIntSol(C_R) \implies a\beta \leq b\alpha$
  708	\item If there is a solution:
  709	\begin{itemize}
  710	\item $\exists x: a\beta \leq abx \leq b\alpha$
  711	\item $\therefore \exists x: a\beta \leq abx \leq ab - a - b + a\beta$
  712	\end{itemize}
  713	\end{itemize}
  714	\end{frame}
  715
  716	\begin{frame}[fragile]
  717	\frametitle{Narrowing it down}
  712	\end{itemize}
  713	\end{frame}
  714
  715	\begin{frame}[fragile]
  716	\frametitle{Narrowing It Down}
  718	717	\begin{center} \includegraphics[width=100mm]{Omega-Test-Number-Line-3.png} \end{center}
  719	718	\begin{itemize}
  …	…
  765	764
  766	765	\begin{frame}[fragile]
  767	\frametitle{Modulo (REM) -- (削除) constant d (削除ここまで)ivisor}
  766	\frametitle{Modulo (REM) -- (追記) Constant D (追記ここまで)ivisor}
  768	767	\begin{itemize}
  769	768	\item $x \operatorname{REM} y = x - \operatorname{sign}(x)|y| \lfloor \frac{|x|}{|y|} \rfloor$
  …	…
  796	795
  797	796	\begin{frame}[fragile]
  798	\frametitle{Modulo (REM) -- (削除) variable d (削除ここまで)ivisor}
  797	\frametitle{Modulo (REM) -- (追記) Variable D (追記ここまで)ivisor}
  799	798	\begin{itemize}
  800	799	\item Previous solution, $x \operatorname{REM} y = x + m|y|$ doesn't work when $m$ and $y$ are both unknown
  …	…
  810	809
  811	810	\begin{frame}[fragile]
  812	\frametitle{Modulo (REM) -- (削除) variable d (削除ここまで)ivisor}
  811	\frametitle{Modulo (REM) -- (追記) Variable D (追記ここまで)ivisor}
  813	812	\begin{itemize}
  814	813	\item Instead of $a \leq 0,ドル consider two cases (recall: $a$ is a multiple of $y$):
  …	…
  820	819	\end{itemize}
  821	820	\begin{lstlisting}
  822	[n]INT as:(削除) -- not valid occam (yet?) (削除ここまで)
  821	[n]INT as:(追記) (追記ここまで)
  823	822	PAR i = 0 FOR n
  824	823	as[(i + 1) REM n] := 42
  …	…
  873	872	\begin{itemize}
  874	873	\item For parallel replication (e.g. 0 FOR 10), we introduce a ghost variable $i'$: 0ドル \leq i < i' \leq 9$
  875	\item Effectively checking for any two arbitrary (non-equal) indices
  876	\item Must check both ways!
  877	\begin{itemize}
  878	\item \lstinline|a[i] := a[i+1]| is `safe' for $i = i' + 1,ドル but not $i + 1 = i'$
  879	\end{itemize}
  880	\end{itemize}
  874	\item Effectively checking for any two arbitrary (non-equal) indices:
  875	\end{itemize}
  876	\begin{lstlisting}
  877	PAR
  878	a[i] := a[i + 1]
  879	a[i'] := a[i' + 1]
  880	\end{lstlisting}
  881	\end{frame}
  882
  883	\begin{frame}[fragile]
  884	\frametitle{Replication}
  885	\begin{lstlisting}
  886	PAR
  887	a[i] := a[i + 1]
  888	a[i'] := a[i' + 1]
  889	\end{lstlisting}
  890	\begin{itemize}
  891	\item Recall: 0ドル \leq i < i' \leq 9$
  892	\item $i = i'$ \cross
  893	\item $i = i' + 1$ \cross
  894	\item $i + 1 = i'$ \tick
  895	\end{itemize}
  896
  881	897	\end{frame}
  882	898
  …	…
  1066	1082
  1067	1083	\begin{frame}[fragile]
  1068	\frametitle{Future (削除) work -- r (削除ここまで)eachability}
  1084	\frametitle{Future (追記) Work -- R (追記ここまで)eachability}
  1069	1085	%Reachability
  1070	1086	\begin{itemize}
  …	…
  1083	1099
  1084	1100	\begin{frame}[fragile]
  1085	\frametitle{Future (削除) work -- advanced r (削除ここまで)eachability}
  1101	\frametitle{Future (追記) Work -- Advanced R (追記ここまで)eachability}
  1086	1102	We could use conditions in \lstinline|IF| and \lstinline|WHILE| as constraints:
  1087	1103	\begin{lstlisting}
  …	…
  1097	1113
  1098	1114	\begin{frame}
  1099	\frametitle{Future (削除) work -- optimising out c (削除ここまで)hecks}
  1115	\frametitle{Future (追記) Work -- Optimising out C (追記ここまで)hecks}
  1100	1116	\begin{itemize}
  1101	1117	\item We could use the integer analysis to check if array indexes are always within bounds

Note: See TracChangeset for help on using the changeset viewer.