1 | 1. E: TaggedEventStruct 2. tr: |E| List 3. i,j,k:||tr||. i < j is-send(E)(tr[i]) is-send(E)(tr[j]) tag(E)(tr[i]) = tag(E)(tr[j]) tr[j] delivered at time k (k':||tr||. k' < k & tr[i] delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k])) 4. i: ||tr|| 5. j: ||tr|| 6. is-send(E)(tr[i]) 7. is-send(E)(tr[j]) 8. i < j & tr[j] somewhere delivered before tr[i] j < i & tr[i] somewhere delivered before tr[j] tag(E)(tr[i]) = tag(E)(tr[j]) |
2 | 1. E: TaggedEventStruct 2. tr: |E| List 3. i,j:||tr||. is-send(E)(tr[i]) & is-send(E)(tr[j]) & i < j & tr[j] somewhere delivered before tr[i] j < i & tr[i] somewhere delivered before tr[j] tag(E)(tr[i]) = tag(E)(tr[j]) 4. i: ||tr|| 5. j: ||tr|| 6. k: ||tr|| 7. i < j 8. is-send(E)(tr[i]) 9. is-send(E)(tr[j]) 10. tag(E)(tr[i]) = tag(E)(tr[j]) 11. tr[j] delivered at time k k':||tr||. k' < k & tr[i] delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k]) |
About: