MC.cfg

CONSTANTS
    BAD_NODES <- Bad_nodes
    GOOD_NODES <- Good_nodes
    MAX <- Max
    MIN <- Min
    MIN_PEERS <- Min_peers

SPECIFICATION
    Spec

INVARIANTS
    TypeOK
    NoSelfInteractions
    GoodNodesOnlyConnectWithPeers
    GoodNodesDoNotExceedMaxConnections
    GoodNodesOnlyExchangeMessagesWithPeers
    GoodNodesNeverHaveMessagesFromBlacklistedPeers
    GoodNodesHaveExlcusiveInProgressAndConnections
    GoodNodesOnlyConnectToNodesWithWhomTheyHaveExchangedAllMessages
    GoodNodesOnlyExchangeMetaMessagesAfterSendingAndReceivingConnectionMessages
    GoodNodesOnlyExchangeAckMessagesAfterSendingAndReceivingConnectionAndMetaMessages

PROPERTIES
    OnceConnectedAlwaysConnected
    OnceBlacklistedAlwaysBlacklisted
    PeerSaturationIsMonotonicIncreasing
    GoodNodesEventuallyExceedMinConnections
    GoodNodesAlwaysRespondToAckMessagesOrBlacklist
    GoodNodesAlwaysRespondToMetaMessagesOrBlacklist
    GoodNodesAlwaysRespondToConnectionMessagesOrBlacklist
    ConnectionsBetweenGoodNodesAreEventuallyBidirectionalOrClosed