MC_liveness.cfg

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

SPECIFICATION
    Spec

PROPERTIES
    OnceBlacklistedAlwaysBlacklisted
    PeerSaturationIsMonotonicIncreasing
    GoodNodesEventuallyExceedMinConnections
    GoodNodesAlwaysRespondToAckMessagesOrBlacklist
    GoodNodesAlwaysRespondToMetaMessagesOrBlacklist
    GoodNodesAlwaysRespondToConnectionMessagesOrBlacklist
    ConnectionsBetweenGoodNodesAreEventuallyBidirectionalOrClosed