Gossip Protocol: Alloy spec

gossip_protocol.als

some sig Version {}

some sig ID {}

some sig Server {
    id: one ID,
    version: one Version,
    var cache: set ID -> Version
}

fact init {
    // Initialize the cache with the its own server id/version
    all s: Server |  s.cache = (s.id -> s.version)

    // Cache cardinality should be equal to the servers
    all s: Server | #s.cache < #Server

    // Ensure the cache has only don't has duplicated keys
    all s: Server| one ~(s.cache).(s.id)

    // Garantee the uniqueness of Server ids
    all disj x, y : Server | no (x.id & y.id)

    // Ensure the cardinality of ids to be equal to servers
    #Server.id = #Server

    // No dangling version
    all v: Version | one version.v

    all i: ID | one id.i
}

fact server_has_own_cache {
    all s: Server | (s.id -> s.version) in s.cache
}

fact transitions {
    always (
        (some disj x, y: Server | gossip[x, y]) or
        stutter
    )
}

fact consistency {
    eventually (
        let final_cache = ~id.version | all s: Server | final_cache = s.cache
    )
}

pred gossip[from, to: Server] {
    some from.cache
    to.cache' = to.cache + from.cache
    from.cache' = from.cache
}

pred stutter {
  cache' = cache
}

run example {}