SPECIFICATION Spec
CONSTANTS
    Users = {u1, u2}
    Creator = u1
    NumScripts = 2
    MaxVersion = 2
    NULL = NULL
CONSTRAINT StateConstraint
INVARIANTS
    TypeOK
    ForkAcyclic
    InstalledImpliesPublished
    RunningImpliesInstalled
    ScanRefsPublishedVersion
    ForkParentCreated
CHECK_DEADLOCK FALSE