\* TLC model-check config for GitOnObjectStore.
\* Run: tlc GitOnObjectStore.tla -config GitOnObjectStore.cfg
SPECIFICATION Spec
CONSTANTS
Pushers = {p1, p2, p3}
MaxManifests = 3
INVARIANT Safety
CONSTRAINT BoundedManifests
\* TLC model-check config for GitOnObjectStore.
\* Run: tlc GitOnObjectStore.tla -config GitOnObjectStore.cfg
SPECIFICATION Spec
CONSTANTS
Pushers = {p1, p2, p3}
MaxManifests = 3
INVARIANT Safety
CONSTRAINT BoundedManifests