SPECIFICATION Spec
CONSTANT defaultInitValue = defaultInitValue
\* Add statements after this line.
CONSTANTS
Timers = {"timer1", "timer2"}
DeltaRange = 10
Subscribers = {"subscriber1", "subscriber2"}
Servers = {"server1", "server2"}
Clients = {"client1", "client2"}
PROPERTIES
starvation_free
INVARIANTS
running_xor_waiting
running_then_not_delta_list
type_check