
diff -r 95e7933968f8 -r a88af0e4731f PIPDefs.thy
--- a/PIPDefs.thy	Thu Jun 02 13:15:03 2016 +0100
+++ b/PIPDefs.thy	Tue Jun 07 13:51:39 2016 +0100
@@ -7,10 +7,10 @@
 chapter {* Definitions *}
 
 text {*
-  In this section, the formal model of  Priority Inheritance Protocol (PIP) 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. 
+  the state of the system is modelled as a list of events (trace) happened so far with the 
+  latest event put at the head. 
 *}
 
 text {*
@@ -32,11 +32,11 @@
   *}
 
 datatype event = 
-  Create thread priority | -- {* Thread @{text "thread"} is created with priority @{text "priority"}. *}
-  Exit thread | -- {* Thread @{text "thread"} finishing its execution. *}
-  P thread cs | -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *}
-  V thread cs | -- {* Thread @{text "thread"}  releasing critical resource @{text "cs"}. *}
-  Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *}
+  Create thread priority   -- {* Thread @{text "thread"} is created with priority @{text "priority"}. *}
+| Exit thread              -- {* Thread @{text "thread"} finishing its execution. *}
+| P thread cs              -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *}
+| V thread cs              -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *}
+| Set thread priority      -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *}
 
 fun actor  where
   "actor (Exit th) = th" |
@@ -45,6 +45,7 @@
   "actor (Set th pty) = th" |
   "actor (Create th prio) = th"
 
+-- {* The actions of a set of threads *}
 definition "actions_of ths s = filter (\<lambda> e. actor e \<in> ths) s"
 
 fun isCreate :: "event \<Rightarrow> bool" where
@@ -60,27 +61,23 @@
   "isV _ = False"
 
 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"}:
-  *}
+  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. 
-  The following type @{text "node"} is used to represent nodes in RAG.
-  *}
+  Resource Allocation Graphs (RAG for short) are used extensively in our formal analysis. 
+  The following type @{text "node"} is used to represent the two types of nodes in RAGs. *}
 datatype node = 
-   Th "thread" | -- {* Node for thread. *}
-   Cs "cs" -- {* Node for critical resource. *}
+  Th "thread" -- {* Node for a thread. *}
+| Cs "cs"     -- {* Node for a critical resource. *}
 
 text {*
-  \noindent
-  The following function
-  @{text "threads"} is used to calculate the set of live threads (@{text "threads s"})
-  in state @{text "s"}.
-  *}
+  The function @{text "threads"} is used to calculate the set of live threads (@{text "threads s"})
+  in state @{text "s"}. *}
+
 fun threads :: "state \<Rightarrow> thread set"
   where 
   -- {* At the start of the system, the set of threads is empty: *}
@@ -93,28 +90,28 @@
   "threads (e#s) = threads s" 
 
 text {* 
-  \noindent
-  The function @{text "threads"} defined above is one of 
-  the so called {\em observation function}s which forms 
-  the very basis of Paulson's inductive protocol verification method.
-  Each observation function {\em observes} one particular aspect (or attribute)
-  of the system. For example, the attribute observed by  @{text "threads s"}
-  is the set of threads living in state @{text "s"}. 
-  The protocol being modelled 
-  The decision made the protocol being modelled is based on the {\em observation}s
-  returned by {\em observation function}s. Since {\observation function}s forms 
-  the very basis on which Paulson's inductive method is based, there will be 
-  a lot of such observation functions introduced in the following. In fact, any function 
-  which takes event list as argument is a {\em observation function}.
-  *}
 
-text {* \noindent
-  Observation @{text "priority th s"} is
-  the {\em original priority} of thread @{text "th"} in state @{text "s"}. 
-  The {\em original priority} is the priority 
-  assigned to a thread when it is created or when it is reset by system call 
-  (represented by event @{text "Set thread priority"}).
-*}
+  \noindent The function @{text "threads"} defined above is one of the
+  so called {\em observation function}s which forms the very basis of
+  Paulson's inductive protocol verification method.  Each observation
+  function {\em observes} one particular aspect (or attribute) of the
+  system. For example, the attribute observed by @{text "threads s"}
+  is the set of threads living in state @{text "s"}.  The protocol
+  being modelled The decision made the protocol being modelled is
+  based on the {\em observation}s returned by {\em observation
+  function}s. Since {\observation function}s forms the very basis on
+  which Paulson's inductive method is based, there will be a lot of
+  such observation functions introduced in the following. In fact, any
+  function which takes event list as argument is a {\em observation
+  function}.  *}
+
+text {* 
+
+  \noindent Observation @{text "priority th s"} is the {\em original
+  priority} of thread @{text "th"} in state @{text "s"}.  The {\em
+  original priority} is the priority assigned to a thread when it is
+  created or when it is reset by system call (represented by event
+  @{text "Set thread priority"}).  *}
 
 fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
   where
@@ -127,11 +124,12 @@
   "priority thread (e#s) = priority thread s"
 
 text {*
-  \noindent
-  Observation @{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.
-*}
+
+  \noindent Observation @{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.  *}
+
 fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"
   where
   "last_set thread [] = 0" |
@@ -142,28 +140,31 @@
   "last_set thread (_#s) = last_set thread s"
 
 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 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:
-  *}
+
+  \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 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: *}
+
 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
   where "preced thread s \<equiv> Prc (priority thread s) (last_set thread s)"
 
 
 text {*
-  \noindent
-  A number of important notions in PIP are represented as the following 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.
-  *}
+
+  \noindent A number of important notions in PIP are represented as
+  the following 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 
@@ -173,8 +174,7 @@
   dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
 *)
 
-definition 
-  -- {* 
+-- {* 
   \begin{minipage}{0.9\textwidth}
   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
@@ -183,6 +183,7 @@
   \end{minipage}
   *}
 
+definition
   cs_holding_raw:   
   "holding_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"
 




