--- a/PrioGDef.thy	Tue Oct 06 11:26:18 2015 +0800
+++ b/PrioGDef.thy	Tue Oct 06 13:08:00 2015 +0800
@@ -5,11 +5,13 @@
 (*>*)
 
 text {*
-  In this section, the formal model of Priority Inheritance is presented. 
+  In this section, the formal model of  Priority Inheritance Protocol (PIP) is presented. 
   The model is based on Paulson's inductive protocol verification method, where 
   the state of the system is modelled as a list of events happened so far with the latest 
   event put at the head. 
+*}
 
+text {*
   To define events, the identifiers of {\em threads},
   {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) 
   need to be represented. All three are represetned using standard 
@@ -22,7 +24,8 @@
 
 text {*
   \noindent
-  Every event in the system corresponds to a system call, the formats of which are
+  The abstraction of Priority Inheritance Protocol (PIP) is set at the system call level.
+  Every system call is represented as an event. The format of events is defined 
   defined as follows:
   *}
 
@@ -33,6 +36,14 @@
   V thread cs | -- {* Thread @{text "thread"}  releasing critical resource @{text "cs"}. *}
   Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *}
 
+
+text {* 
+  As mentioned earlier, in Paulson's inductive method, the states of system are represented as lists of events,
+  which is defined by the following type @{text "state"}:
+  *}
+type_synonym state = "event list"
+
+
 text {* 
 \noindent
   Resource Allocation Graph (RAG for short) is used extensively in our formal analysis. 
@@ -42,12 +53,6 @@
    Th "thread" | -- {* Node for thread. *}
    Cs "cs" -- {* Node for critical resource. *}
 
-text {* 
-  In Paulson's inductive method, the states of system are represented as lists of events,
-  which is defined by the following type @{text "state"}:
-  *}
-type_synonym state = "event list"
-
 text {*
   \noindent
   The following function
@@ -64,6 +69,7 @@
   "threads (Exit thread # s) = (threads s) - {thread}" | 
   -- {* Other kind of events does not affect the value of @{text "threads"}: *}
   "threads (e#s) = threads s" 
+
 text {* \noindent
   Functions such as @{text "threads"}, which extract information out of system states, are called
   {\em observing functions}. A series of observing functions will be defined in the sequel in order to 
@@ -88,7 +94,7 @@
 text {*
   \noindent
   In the following,
-  @{text "last_set th s"} is the time when thread @{text "th"} is created, 
+  @{text "last_set th s"} is the last time when the priority of thread @{text "th"} is set, 
   observed from state @{text "s"}.
   The time in the system is measured by the number of events happened so far since the very beginning.
 *}
@@ -104,8 +110,8 @@
 text {*
   \noindent 
   The {\em precedence} is a notion derived from {\em priority}, where the {\em precedence} of 
-  a thread is the combination of its {\em original priority} and {\em birth time}. The intention is
-  to discriminate threads with the same priority by giving threads whose priority
+  a thread is the combination of its {\em original priority} and {\em time} the priority is set. 
+  The intention is to discriminate threads with the same priority by giving threads whose priority
   is assigned earlier higher precedences, becasue such threads are more urgent to finish. 
   This explains the following definition:
   *}
@@ -115,7 +121,14 @@
 
 text {*
   \noindent
-  A number of important notions are defined here:
+  A number of important notions in PIP are represented as functions defined 
+  in terms of the waiting queues of the system, where the waiting queues 
+  , as a whole, is represented by the @{text "wq"} argument of every notion function.
+  The @{text "wq"} argument is itself a functions which 
+  maps every critical resource @{text "cs"} to the list of threads which are holding or waiting for it. 
+  The thread at the head of this list is designated as the thread which is current 
+  holding the resrouce, which is slightly different from tradition where
+  all threads in the waiting queue are considered as waiting for the resource.
   *}
 
 consts 
@@ -124,21 +137,15 @@
   RAG :: "'b \<Rightarrow> (node \<times> node) set"
   dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
 
-text {*
-  \noindent
-  In the definition of the following several functions, it is supposed that
-  the waiting queue of every critical resource is given by a waiting queue 
-  function @{text "wq"}, which servers as arguments of these functions.
-  *}
 defs (overloaded) 
   -- {* 
   \begin{minipage}{0.9\textwidth}
-  We define that the thread which is at the head of waiting queue of resource @{text "cs"}
-  is holding the resource. This definition is slightly different from tradition where
-  all threads in the waiting queue are considered as waiting for the resource.
-  This notion is reflected in the definition of @{text "holding wq th cs"} as follows:
+  This meaning of @{text "wq"} is reflected in the following definition of @{text "holding wq th cs"},
+  where @{text "holding wq th cs"} means thread @{text "th"} is holding the critical 
+  resource @{text "cs"}. This decision is based on @{text "wq"}.
   \end{minipage}
   *}
+
   cs_holding_def: 
   "holding wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"
   -- {* 
@@ -153,8 +160,8 @@
   "waiting wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
   -- {* 
   \begin{minipage}{0.9\textwidth}
-  @{text "RAG wq"} represents the Resource Allocation Graph of the system under the waiting 
-  queue function @{text "wq"}.
+  @{text "RAG wq"} generates RAG (a binary relations on @{text "node"})
+  out of waiting queues of the system (represented by the @{text "wq"} argument):
   \end{minipage}
   *}
   cs_RAG_def: 
@@ -163,12 +170,14 @@
   -- {* 
   \begin{minipage}{0.9\textwidth}
   The following @{text "dependants wq th"} represents the set of threads which are RAGing on
-  thread @{text "th"} in Resource Allocation Graph @{text "RAG wq"}:
+  thread @{text "th"} in Resource Allocation Graph @{text "RAG wq"}. 
+  Here, "RAGing" means waiting directly or indirectly on the critical resource. 
   \end{minipage}
   *}
   cs_dependants_def: 
   "dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"
 
+(* I stop here for the moment ccc *)
 
 text {*
   The data structure used by the operating system for scheduling is referred to as