|
|
|---|
|
|
|
|---|
Transitions for timer expiration.
Here we define the system state transitions
caused by
Each validator starts a timer when it advances its round. At some point, the timer may expire. We do not model real time currently, but we model the fact that a timer may change state, from running to expired.