SpireSafe.cfg

SPECIFICATION
    (*****************************************************************************)
    (* Various specification 'flavours' that may be used for bounded model       *)
    (* checking.                                                                 *)
    (*****************************************************************************)

    (*****************************************************************************)
    (* Regular specification for model checking.                                 *)
    (*****************************************************************************)
    Spec

    (*****************************************************************************)
    (* Starts in any state permitted by the inductive invariant `Inv'.           *)
    (* This is a traditional inductive specification that works for tiny         *)
    (* models, but scales poorly as the model size increases. Consider           *)
    (* using `RSpec' for larger models.                                          *)
    (*****************************************************************************)
    \* ISpec

    (*****************************************************************************)
    (* Uses random sampling to generate inductive initial states, being a subset *)
    (* of all possible initial states otherwise permitted by `Inv'. Each run     *)
    (* results in a different set of initial states.                             *)
    (* Sample sizes are configured by setting `Carg' and `Parg' in the module    *)
    (* definition.                                                               *)
    (*****************************************************************************)
    \* RSpec

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
    Inv
    SingularPrimedPerRound
    ChosenRequiresEarlierUnprimedOffers
    Consistency

SYMMETRY Symmetry