SpireLive.cfg

SPECIFICATION
    FairSpec

CONSTANTS
    None = "none"
    Rounds <- FiniteRounds
    Values = {x, y}
    MaxRound = 3

    (*****************************************************************************)
    (* Varying combinations of consenters and quorums. Uncomment to size the     *)
    (* model accordingly.                                                        *)
    (*****************************************************************************)

    \* Consenters = {a, b, c, d, e}
    \* Quorums = {{a, b, c}, {a, b, d}, {a, b, e}, {a, c, d}, {a, c, e}, {a, d, e}, {b, c, d}, {b, c, e}, {b, d, e}, {c, d, e}}

    \* Consenters = {a, b, c, d}
    \* Quorums = {{a, b, c}, {a, b, d}, {a, c, d}, {b, c, d}}

    Consenters = {a, b, c}
    Quorums = {{a, b}, {b, c}, {a, c}}

    \* Consenters = {a, b}
    \* Quorums = {{a, b}}

    \* Consenters = {a}
    \* Quorums = {{a}}

INVARIANTS
    TypeOK
    Consistency

PROPERTIES 
    TemporalProperties