Example of refinement in TLA+ This example contains an abstract model of signal exchange according to the rendezvous model mentioned in my PhD theses theory.