# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1499088564 -3600
# Node ID 5d4c398c81873332f1c9b299ececd6d71ed9bb7f
# Parent  1e7d55d8b3da6e4a7d4beb3443933d062bcdb93a
updated

diff -r 1e7d55d8b3da -r 5d4c398c8187 Journal/Paper.thy
--- a/Journal/Paper.thy	Mon Jul 03 13:31:20 2017 +0100
+++ b/Journal/Paper.thy	Mon Jul 03 14:29:24 2017 +0100
@@ -1829,10 +1829,11 @@
   depends on the precedenes of all threads in its subtree---a ``global'' transitive notion,
   which is indeed heavy weight (see the equation for @{text cprec} shown in \eqref{overloaded}).
   We can however improve upon this. For this recall the notion
-  of @{term children} of @{text th} (defined in \eqref{children})
+  of @{term children} of a thread @{text th} (defined in \eqref{children})
   where a child is a thread that is only one ``hop'' away from the thread
   @{text th} in the @{term TDG} (and waiting for @{text th} to release
-  a resource). With this we can prove the following lemma.
+  a resource). Using children, we can prove the following lemma for calculating
+  @{text cprec}.
 
 
   \begin{lemma}\label{childrenlem}
@@ -1847,7 +1848,8 @@
   computed locally by considering only the static precedence of @{text th}
   and 
   the current precedences of the children of @{text th}. In
-  effect, it only needs to be recomputed for @{text th} when one of
+  effect, it only needs to be recomputed for @{text th} when its static
+  precedence is re-set or when one of
   its children changes its current precedence.  This is much more efficient 
   because when the  @{text cprec}-value is not changed for a child, 
   the recursion does not need to decend into the corresponding subtree.
@@ -1869,15 +1871,15 @@
 
 text {*
   \noindent
-  \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s'} and 
-  the next state @{term "s \<equiv> Create th prio#s'"} are both valid (meaning the event
-  is allowed to occur). In this situation we can show that
+  \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s} and 
+  the next state @{term "e#s"}, where \mbox{@{term "e = Create th prio"}}, are both valid (meaning the event
+  is allowed to occur in @{text s}). In this situation we can show that
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  HERE ?? %@ {thm eq_dep},\\
-  @{thm valid_trace_create.eq_cp_th}, and\\
-  @{thm[mode=IfThen] valid_trace_create.eq_cp}
+  @{thm (concl) valid_trace_create.RAG_es},\\
+  @{thm (concl) valid_trace_create.eq_cp_th}, and\\
+  @{text "If"} @{thm (prem 2) valid_trace_create.eq_cp} @{text "then"} @{thm (concl) valid_trace_create.eq_cp}
   \end{tabular}
   \end{isabelle}
 
diff -r 1e7d55d8b3da -r 5d4c398c8187 journal.pdf
Binary file journal.pdf has changed