search

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities
Other
1.29k stars 200 forks source link

Refinement mapping for AsyncTerminationDetection => SyncTerminationDetection #36

Closed lemmy closed 3 years ago

lemmy commented 3 years ago

@muenchnerkindl TLC "agrees" with this refinement mapping for N = 3 and N = 5. Do you too? I stopped at the third level of a refinement proof.

muenchnerkindl commented 3 years ago

@lemmy Yes, that's nice! I'll try to write a formal proof.