Changes between Version 15 and Version 16 of ContractReduction

Timestamp:

07/21/14 15:55:41 (12 years ago)

Author:

siegel

Comment:

--

ContractReduction

@@ -48 +48 @@
 == Ample set and the exact interpretation of $depends ==
 
-Fix a state s, a process q, and a statement S.
+Fix a statement S and a process q.
 
-Let T(s,S,q) denote the set of transitions specified by having q execute S from s.  We say this is a set because some statements S are nondeterministic, meaning they can generate multiple transitions. Note that T(s,S,q) includes all transitions specified by S, even those that are not enabled.
+Let T(S,q) denote the set of transitions specified by having q execute S.  We say this is a set because some statements S are nondeterministic, meaning they can generate multiple transitions.  Note that T(S,q) is independent of the state.  In particular, it must include all possible transitions that could be generated by S, even if not all of them are enabled in every state.
+
+Now fix a state s and assume that the origin of S is the location of q in s.
 
 Suppose A(s,S,q) is a set of procs which satisfies the following:
 
-In any execution departing from s, no transition dependent on a transition in T(s,S,q) can occur without a transition from a proc in A(s,S,q) occurring first.
+In any execution departing from s, no transition dependent on a transition in T(S,q) can occur without a transition from a proc in A(s,S,q) occurring first.
 
 Then define AMPLE as follows:
@@ -65 +67 @@
     choose q in WorkSet;
     WorkSet := WorkSet - {q};
-    forall statements S emanating from current location of q in s:
+    forall statements S with origin the location of q in s:
       foreach r in A(s,S,q): if r is not in AmpleProcs, add r to AmpleProcs and to WorkSet
     end forall;
@@ -73 +75 @@
 }}}
 
-Claim: for any process p, if AMPLE(s,p) contains a process with at least one enabled transition in s, then it defines an ample set, i.e., from any execution departing from s, no transition dependent
+Claim: for any process p, if AMPLE(s,p) contains a process with at least one enabled transition in s,
+then it defines an ample set, i.e., from any execution departing from s, no transition dependent
 on a transition from a proc in AMPLE(s,p) can occur without a transition from a proc in AMPLE(s,p) occurring first.
 
@@ -83 +86 @@
 be any execution prefix starting from s for which t is dependent on a transition from a proc in AMPLE.
 
-ASSUME that none of the t_i are from procs in AMPLE.
+ASSUME that none of the t_i are from procs in AMPLE.  We aim to get a contradiction.
 
-Say t is dependent on transition t0, and that t0 has statement S0 in process q0, and q0 is in AMPLE.
+Say t is dependent on transition t0 in T(S0,q0), for some statement S0 and process q0 in AMPLE.
 
-Throughout the entire execution prefix (E), q0 remains at the location it had in state s.  In particular, S0 emanates 
-from the current location of q0 in s.
+By assumption, throughout the entire execution prefix (E), q0 remains at the location it had in state s.
+In particular, the origin of S0 is the location of q0 in s.
 
-Since q0 is in AMPLE, that means from the algorithm that defines AMPLE that we must
-have A(s,S0,q0) is a subset of AMPLE.
+Since q0 is in AMPLE, it follows from the algorithm that defines AMPLE that A(s,S0,q0) is a subset of AMPLE.
 
-From the contract defining A, we know that no transition dependent on a transition in T(s,S0,q0) can occur without a transition
-from a proc in A(s,S0,q0) occurring first.  Hence for some i, t_i is from a proc in A(s,S0,q0), and therefore t_i is in AMPLE.
-
-We conclude that no transition dependent on a transition from a proc in AMPLE can occur without a transition from a proc
-in AMPLE occurring first.  QED.
+From the contract defining A, we know that no transition dependent on a transition in T(S0,q0) can occur without a transition
+from a proc in A(s,S0,q0) occurring first.  Hence for some i, t_i is from a proc in A(s,S0,q0), and therefore t_i is in AMPLE,
+contradicting the ASSUMPTION.  QED.