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

diff -r 5d4c398c8187 -r 5067a2ab5557 Journal/Paper.thy
--- a/Journal/Paper.thy	Mon Jul 03 14:29:24 2017 +0100
+++ b/Journal/Paper.thy	Mon Jul 03 15:29:29 2017 +0100
@@ -1872,8 +1872,8 @@
 text {*
   \noindent
   \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
+  the next state @{term "e#s"}, whereby \mbox{@{term "e \<equiv> Create th prio"}}, are both valid (meaning the event
+  @{text "Create"} is allowed to occur in @{text s}). In this situation we can show that
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -1892,13 +1892,13 @@
 
 text {*
   \noindent
-  \colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s'} and 
-  the next state @{term "s \<equiv> Exit th#s'"} are both valid. We can show that
+  \colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s} and 
+  the next state @{term "e#s"}, whereby this time  @{term "e \<equiv> Exit th"}, are both valid. We can show that
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  HERE %@ {thm valid_trace_create.eq_dep}, and\\
-  @{thm[mode=IfThen] valid_trace_create.eq_cp}
+  @{thm (concl) valid_trace_exit.RAG_es}, and\\
+  @{text "If"} @{thm (prem 2) valid_trace_exit.eq_cp} @{text "then"} @{thm (concl) valid_trace_exit.eq_cp}
   \end{tabular}
   \end{isabelle}
 
@@ -1912,22 +1912,23 @@
 
 text {*
   \noindent
-  \colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s'} and 
-  @{term "s \<equiv> Set th prio#s'"} are both valid. We can show that
+  \colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s} and 
+  @{term "e#s"} with @{term "e \<equiv> Set th prio"} are both valid. We can show that
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  %@ {thm[mode=IfThen] eq_dep}, and\\
-  %@ {thm[mode=IfThen] valid_trace_create.eq_cp_pre}
+  @{thm (concl) valid_trace_set.RAG_es}, and\\
+  @{text "If"} @{thm (prem 2) valid_trace_set.eq_cp} @{text "then"} @{thm (concl) valid_trace_set.eq_cp}
   \end{tabular}
   \end{isabelle}
 
-  \noindent
-  The first property is again telling us we do not need to change the @{text RAG}. 
-  The second shows that the @{term cp}-values of all threads other than @{text th} 
-  are unchanged. The reason is that @{text th} is running; therefore it is not in 
-  the @{term dependants} relation of any other thread. This in turn means that the 
-  change of its priority cannot affect other threads.
+  \noindent The first property is again telling us we do not need to
+  change the @{text RAG}.  The second shows that the @{term cp}-values
+  of all threads other than @{text th} are unchanged. The reason for
+  this is more subtle: Since @{text th} must be running, that is does
+  not wait for any resource to be released, it cannot be in any
+  subtree of any other thread. So all current precedences of other
+  threads are unchanged.
 
   %The second
   %however states that only threads that are \emph{not} dependants of @{text th} have their
@@ -1968,6 +1969,7 @@
 
 
   \begin{isabelle}\ \ \ \ \ %%%
+  @{thm (concl) valid_trace_v_n.RAG_s}\\
   %@ {thm RAG_s}
   \end{isabelle}
   
diff -r 5d4c398c8187 -r 5067a2ab5557 journal.pdf
Binary file journal.pdf has changed