| title Healthy Replication |
| |
| participant Client1 |
| participant Instance1 |
| participant Instance2 |
| participant Client2 |
| |
| state over Client1, Client2, Instance1, Instance2: W0 |
| state over Client1 : W0 -> W1 |
| Client1 -> +Instance1: Push W1 |
| Instance1 -> Client1: Ack W1 |
| state over Instance1 : W0 -> W1 |
| Instance1->-Instance2: Replicate W1 |
| state over Instance2, Client1, Instance1: W0 -> W1 |
| |
| state over Instance1 : Crash |
| |
| state over Client2 : W0 -> W2 |
| Client2 -> +Instance2: Push W2 |
| Instance2 -> Client2: Missing W1 |
| Client2 -> Instance2: Pull W1 |
| state over Client2 : W0 -> W1 -> W2 |
| Client2 -> Instance2: Push W2 |
| |
| state over Instance2 : W0 -> W1 -> W2 |
| |
| state over Instance1: Restart |
| |
| Instance2->Instance1: Replicate W2 |
| |
| state over Instance2, Client2, Instance1: W0 -> W1 -> W2 |
| |
| |
