research/tlaplus/gossip/gossip.toolbox/Model_1/MC.tla

15 lines
374 B
Plaintext

---- MODULE MC ----
EXTENDS gossip, TLC
\* SPECIFICATION definition @modelBehaviorSpec:0
spec_157543427551222000 ==
Spec
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_157543427551223000 ==
IsSpread
----
=============================================================================
\* Modification History
\* Created Wed Dec 04 12:37:55 CST 2019 by oskarth