Commit 466c5e75 authored by Markus Klinik's avatar Markus Klinik
Browse files

figure: plan and relaxation

parent d8156d37
......@@ -48,7 +48,10 @@
\renewcommand{\IEEEproofindentspace}{0pt}
\usepackage{tikz}
\usetikzlibrary{arrows.meta}
\usetikzlibrary{arrows}
\usetikzlibrary{positioning}
\usetikzlibrary{matrix}
\usetikzlibrary{shapes}
\usepackage{listings}
\input{languages.tex}
......@@ -146,6 +149,7 @@
\tikzset{skyline/.style={very thick}}
\tikzset{axis/.style={->}}
\tikzset{endInterval/.style={Bracket[]-Bracket[]}}
\tikzstyle{task}=[draw, minimum width=2em, minimum height=1.4em, text centered, inner sep=0.3em ]
% https://tex.stackexchange.com/questions/49888/tikzpicture-alignment-and-centering
\tikzset
......
......@@ -199,3 +199,38 @@ This counterexample is a valid plan.
\subsection{Plan Relaxation Using Dependence Analysis}
Given a valid plan from the synthesizer, the \emph{relaxer} identifies those actions of the plan that must be executed in the given order, and removes constraints from all others.
The relaxer uses dependence analysis, a common technique in the field of compiler construction to identify instructions that can be reordered or parallelized.
\begin{example}
(Making coffee, continued)
\Cref{fig:makingCoffee:relaxation} shows two plans for making coffee, one as it could be output by the plan synthesizer, and one after relaxation.
The relaxer sees that \name{AddWater} and \name{AddBeans} are independent of each other, but that \name{MakeCoffee} depends on both.
The reason for this is that \name{AddWater} and \name{AddBeans} act on different regions of the state.
\qed
\begin{figure}
\begin{tikzpicture}[->,>=stealth']
\matrix[column sep=1cm]
{
\node[task] (A) {AddWater}; & \node[task] (B) {AddBeans}; & \node[task] (C) {MakeCoffee}; \\
};
\path (A) edge (B);
\path (B) edge (C);
\end{tikzpicture}
\begin{tikzpicture}[->,>=stealth']
\matrix[column sep=1cm]
{
\node[task] (A) {AddWater}; \\
& \node[task] (C) {MakeCoffee}; \\
\node[task] (B) {AddBeans}; \\
};
\path (A) edge (C);
\path (B) edge (C);
\end{tikzpicture}
\caption{The plan for making coffee, before and after relaxation. Arrows indicate dependencies.}
\label{fig:makingCoffee:relaxation}
\end{figure}
\end{example}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment