1973 %@ { thm (concl) valid_trace_v_n.RAG_s}\\ |
1973 %@ { thm (concl) valid_trace_v_n.RAG_s}\\ |
1974 @{term "RAG (e#s) = RAG s - {(C cs,T th), (T th',C cs)} \<union> {(C cs, T th')}"} |
1974 @{term "RAG (e#s) = RAG s - {(C cs,T th), (T th',C cs)} \<union> {(C cs, T th')}"} |
1975 \end{isabelle} |
1975 \end{isabelle} |
1976 |
1976 |
1977 \noindent |
1977 \noindent |
1978 which shows how the @{text RAG} needs to be changed. The next lemma suggests |
1978 which shows how the @{text RAG} needs to be changed. The next lemmas suggest |
1979 how the current precedences need to be recalculated. For threads that are |
1979 how the current precedences need to be recalculated. For threads that are |
1980 not @{text "th"} and @{text "th'"} nothing needs to be changed, since we |
1980 not @{text "th"} and @{text "th'"} nothing needs to be changed, since we |
1981 can show |
1981 can show |
1982 |
1982 |
1983 \begin{isabelle}\ \ \ \ \ %%% |
1983 \begin{isabelle}\ \ \ \ \ %%% |
1984 @{text "If"} @{text "th'' \<noteq> th"} and |
1984 @{text "If"} @{text "th'' \<noteq> th"} and |
1985 @{text "th'' \<noteq> th'"} |
1985 @{text "th'' \<noteq> th'"} |
1986 @{thm (concl) valid_trace_v_n.cp_kept[where ?th1.0="th''"]} |
1986 @{thm (concl) valid_trace_v_n.cp_kept[where ?th1.0="th''"]} |
|
1987 \hfill\numbered{fone} |
1987 \end{isabelle} |
1988 \end{isabelle} |
1988 |
1989 |
1989 \noindent |
1990 \noindent |
1990 For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to |
1991 For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to |
1991 recalculate their current precedence since their children have changed. |
1992 recalculate their current precedence since their children have changed. |
1992 |
1993 However, neither @{text "th"} and @{text "th'"} is element of the |
1993 |
1994 respective children, which is shown by the following two facts: |
1994 \begin{isabelle}\ \ \ \ \ %%% |
1995 |
1995 @{thm (concl) valid_trace_v_n.t1}\\ |
1996 |
1996 @{thm (concl) valid_trace_v_n.t2} |
1997 \begin{isabelle}\ \ \ \ \ %%% |
1997 \end{isabelle} |
1998 \begin{tabular}{@ {}l} |
|
1999 @{term "th' \<notin> children (TDG (e#s)) th"}\\ |
|
2000 @{term "th \<notin> children (TDG (e#s)) th'"} |
|
2001 \end{tabular}\hfill{}\numbered{ftwo} |
|
2002 \end{isabelle} |
|
2003 |
|
2004 \noindent |
|
2005 This means the recalculation of the @{text cprec} of @{text "th"} and |
|
2006 @{text "th'"} can be done independently and also done locally by only |
|
2007 looking at the children: according to \eqref{fone} and \eqref{ftwo} |
|
2008 none of the @{text cprecs} of the children |
|
2009 changes, just the children-sets changes by a @{text V}-event. This |
|
2010 in turn means the recalculation of |
|
2011 @{text cprec} for @{text th} and @{text "th'"} terminates since |
|
2012 none of the @{text cprec} need the be recalculated. |
|
2013 |
1998 *} |
2014 *} |
1999 |
2015 |
2000 text {* |
2016 text {* |
2001 \noindent |
2017 \noindent |
2002 In the other case where there is no thread that takes over @{text cs}, |
2018 In the other case where there is no thread that takes over @{text cs}, |