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

\* SPECIFICATION definition @modelBehaviorSpec:0
spec_157543425399217000 ==
Spec
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_157543425399318000 ==
IsSpread
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_157543425399319000 ==
Termination
----
=============================================================================
\* Modification History
\* Created Wed Dec 04 12:37:33 CST 2019 by oskarth
