Changes between Version 18 and Version 19 of ContractReduction


Ignore:
Timestamp:
07/21/14 18:39:11 (12 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • ContractReduction

    v18 v19  
    7979}}}
    8080
     81Note: AMPLE(s,p) is the smallest set containing and p and satisfying:
     82
     83if q is in AMPLE(s,p) then for all statements S with origin the location of q in s, A(s,S,q) is a subset of AMPLE(s,p).
     84
    8185Claim: for any process p, if AMPLE(s,p) contains a process with at least one enabled transition in s,
    8286then it defines an ample set, i.e., from any execution departing from s, no transition dependent