1 | 1. E: TaggedEventStruct 2. tr: |E| List 3. Q: ||tr||Prop 4. i:||tr||. Dec(Q(i)) 5. i: ||tr|| 6. Q(i) 7. i:||tr||. Q(i) is-send(E)(tr[i]) 8. i,j:||tr||. Q(i) Q(j) tag(E)(tr[i]) = tag(E)(tr[j]) 9. i,j:||tr||. Q(i) ij C(Q)(j) 10. i,j:||tr||. (tr[i] =msg=(E) tr[j]) tag(E)(tr[i]) = tag(E)(tr[j]) 11. Causal(E)(tr) 12. No-dup-send(E)(tr) 13. tr = nil x:||tr||. Dec(C(Q)(x)) |
2 | 1. E: TaggedEventStruct 2. tr: |E| List 3. Q: ||tr||Prop 4. i:||tr||. Dec(Q(i)) 5. i: ||tr|| 6. Q(i) 7. i:||tr||. Q(i) is-send(E)(tr[i]) 8. i,j:||tr||. Q(i) Q(j) tag(E)(tr[i]) = tag(E)(tr[j]) 9. i,j:||tr||. Q(i) ij C(Q)(j) 10. i,j:||tr||. (tr[i] =msg=(E) tr[j]) tag(E)(tr[i]) = tag(E)(tr[j]) 11. Causal(E)(tr) 12. No-dup-send(E)(tr) 13. tr = nil i,j:||tr||. C(Q)(i) i < j C(Q)(j) |
3 | 1. E: TaggedEventStruct 2. tr: |E| List 3. Q: ||tr||Prop 4. i:||tr||. Dec(Q(i)) 5. i: ||tr|| 6. Q(i) 7. i:||tr||. Q(i) is-send(E)(tr[i]) 8. i,j:||tr||. Q(i) Q(j) tag(E)(tr[i]) = tag(E)(tr[j]) 9. i,j:||tr||. Q(i) ij C(Q)(j) 10. i,j:||tr||. (tr[i] =msg=(E) tr[j]) tag(E)(tr[i]) = tag(E)(tr[j]) 11. Causal(E)(tr) 12. No-dup-send(E)(tr) 13. tr = nil 14. L_1,L_2:|E| List. tr = (L_1 @ L_2) & (i:||tr||. C(Q)(i) ||L_1||i) L_1,L_2:Trace(E). tr = (L_1 @ L_2) & L_2 = nil |E| List & (xL_1.(yL_2.(x =msg=(E) y))) & (m:Label. (xL_2.tag(E)(x) = m)) |
About: