regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:f2e0d031a395
+:4fcd802eba59
 preced ("prec") and
 cpreced ("cprec") and
 dependents ("dependants") and
 cp ("cprec") and
 holdents ("resources") and
+original_priority ("priority") and
 DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 (*>*)
 section {* Introduction *}
 @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\
 \end{tabular}}
 \end{isabelle}
 \noindent
+In this definition @{term "DUMMY # DUMMY"} stands for list-cons.
 Another function calculates the priority for a thread @{text "th"}, which is
 defined as
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{lcl}
 Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a
 state @{text s}. It is defined as
 \begin{isabelle}\ \ \ \ \ %%%
-@{thm cpreced_def2}\numbered{permprops}
+@{thm cpreced_def2}\hfill\numbered{cpreced}
 \end{isabelle}
 \noindent
 While the precedence @{term prec} of a thread is determined by the programmer
 (for example when the thread is
 \begin{isabelle}\ \ \ \ \ %%%
 @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
 \end{isabelle}
 \noindent
-The first function is a waiting queue function (that is takes a @{text "cs"} and returns the
+The first function is a waiting queue function (that is it takes a resource @{text "cs"} and returns the
 corresponding list of threads that wait for it), the second is a function that takes
-a thread and returns its current precedence (see ???). We assume the usual getter and
+a thread and returns its current precedence (see \eqref{cpreced}). We assume the usual getter and
 setter methods for such records.
 In the initial state, the scheduler starts with all resources unlocked and the
 current precedence of every thread is initialised with @{term "Prc 0 0"}; that means
-@{abbrev initial_cprec}. Therefore
+\mbox{@{abbrev initial_cprec}}. Therefore
 we have
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\
 \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}
 \end{tabular}
 \end{isabelle}
 Having the scheduler function @{term schs} at our disposal, we can ``lift'' the notions
-@{term waiting}, @{term holding} @{term depend} and @{term cp} such that they only depend
+@{term waiting}, @{term holding}, @{term depend} and @{term cp} such that they only depend
 on states.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}rcl}
 @{thm (lhs) s_holding_abv} & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv}\\
 @{thm (lhs) cp_def}        & @{text "\<equiv>"} & @{thm (rhs) cp_def}
 \end{tabular}
 \end{isabelle}
 \noindent
-With them we can introduce the notion of threads being @{term readys} (i.e.~threads
+With these abbreviations we can introduce for states
+the notion of threads being @{term readys} (i.e.~threads
 that do not wait for any resource) and the running thread.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm readys_def}\\
 @{thm runing_def}\\
 \end{tabular}
 \end{isabelle}
 \noindent
+In this definition @{term "f ` S"} stands for the set @{text S} under the image of the
+function @{text f}.
 Note that in the initial case, that is where the list of events is empty, the set
 @{term threads} is empty and therefore there is no thread ready nor a running.
 If there is one or more threads ready, then there can only be \emph{one} thread
 running, namely the one whose current precedence is equal to the maximum of all ready
-threads. We can also define the set of resources that are locked by a thread in a
+threads. We can also define the set of resources that are locked by a thread in any
 given state.
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm holdents_def}
 \end{isabelle}
 \noindent
 These resources are given by the holding edges in the RAG.
-Finally we can define what a \emph{valid state} is. For example we cannot exptect to
+Finally we can define what a \emph{valid state} is in our PIP. For example we cannot exptect to
 be able to exit a thread, if it was not created yet. These validity constraints
-are characterised by the inductive predicate @{term "step"} by the following five
+are characterised by the inductive predicate @{term "step"}. We give five
 inference rules relating a state and an event that can happen next.
 \begin{center}
 \begin{tabular}{c}
 @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}

changeset 299	4fcd802eba59
parent 298	f2e0d031a395
child 300	8524f94d251b