---- MODULE MC ----
EXTENDS gossip, TLC

\* SPECIFICATION definition @modelBehaviorSpec:0
spec_15753830630934000 ==
Spec
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_15753830630935000 ==
NoOverdrafts
----
=============================================================================
\* Modification History
\* Created Tue Dec 03 22:24:23 CST 2019 by oskarth
