Changes between Version 14 and Version 15 of ContractReduction

Timestamp:

07/21/14 15:14:50 (12 years ago)

Author:

siegel

Comment:

--

ContractReduction

@@ -46 +46 @@
 * if the body of the function is present, the statements comprising the body may be analyzed to further restrict the reduction.
 
+== Ample set and the exact interpretation of $depends ==
+
+Fix a state s, a process q, and a statement S.
+
+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.
+
+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.
+
+Then define AMPLE as follows:
+{{{
+Function AMPLE(s:State, p:proc) : set of proc is
+  let AmpleProcs = {p};
+  let WorkSet = {p};
+  // invariant: WorkSet is a subset of AmpleProcs
+  while (WorkSet not empty) {
+    choose q in WorkSet;
+    WorkSet := WorkSet - {q};
+    forall statements S emanating from current 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;
+  }
+  return AmpleProcs;
+end Function AMPLE
+}}}
+
+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.
+
+Proof:  Let AMPLE=AMPLE(s,p).
+Let
+
+  (E)  t_1, t_2, ..., t_n, t
+
+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.
+
+Say t is dependent on transition t0, and that t0 has statement S0 in process q0, and q0 is 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.
+
+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.
+
+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.
+
+
 == Function specifiers ==