EWD687a_anim.cfg

CONSTANTS
    L = L
    P1 = P1
    P2 = P2
    P3 = P3
    P4 = P4
    P5 = P5

CONSTANT
    Procs <- NodesOfNetwork

CONSTANT
    Edges <- Network

CONSTANT
    Leader <- L

SPECIFICATION
    Spec

INVARIANT
    TypeOK
    DT1Inv
    InterestingBehavior

PROPERTY
    DT2
    \* CountersConsistent
    \* TreeWithRoot
    \* StableUpEdge

ALIAS
    Alias

CHECK_DEADLOCK
    FALSE

ACTION_CONSTRAINT
    NoSuperfluousIdleSteps