Changes between Version 17 and Version 18 of ContractReduction

Timestamp:

07/21/14 16:22:13 (12 years ago)

Author:

siegel

Comment:

--

ContractReduction

@@ -32 +32 @@
 }}}
 where `e` is an expression of boolean type.   For each process `p`, the `e` can be evaluated in the context of `p`.   If `e` evaluates to `true`, then `p` must be included in an ample set containing a call to this function. 
+
+The expression `e` hence defines a predicate d(s,p), where s ranges over states, and p over procs.   The requirement is the following:
+
+Let s be any state and p a proc such that a function call for this function is enabled in p.  Then in any execution departing from s, no transition dependent on the execution of this function call can occur without a transition from p or a proc q satisfying d(s,q) occurring first.
 
 The following built-in functions may be used as constituents in the boolean expression `e`: