--- a/prio/Paper/Paper.thy Sat Feb 11 12:29:52 2012 +0000
+++ b/prio/Paper/Paper.thy Sat Feb 11 19:39:50 2012 +0000
@@ -185,7 +185,7 @@
a thread obtains a new priority given by the programmer or
user (for example via the {\tt nice} utility under UNIX). As in Paulson's work, we
need to define functions that allow one to make some observations
- about states. One, called @{term threads}, calculates, given a state @{text s}, the set of
+ about states. One, called @{term threads}, calculates the set of
``live'' threads that we have seen so far:
\begin{isabelle}\ \ \ \ \ %%%
@@ -305,14 +305,22 @@
An instance of a RAG is as follows:
\begin{center}
+ \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
\begin{tikzpicture}[scale=1]
- \draw[step=2mm] (0,0) grid (3,2);
+ %%\draw[step=2mm] (-3,2) grid (1,-1);
- \draw[rounded corners=1mm, very thick] (0,0) rectangle (0.6,0.6);
- \draw[rounded corners=1mm, very thick] (3,0) rectangle (3.6,0.6);
+ \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
+ \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
+ \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
+ \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
+ \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
+ \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
- \draw (0.3,0.3) node {\small$th_0$};
- \draw (3.3,0.3) node {\small$th_1$};
+ \draw [->,line width=0.6mm] (A) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding} (B);
+ \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B);
+ \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B);
+ \draw [->,line width=0.6mm] (D) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding} (E);
+ \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}waiting} (E);
\end{tikzpicture}
\end{center}