SPECIFICATION Spec
CONSTANTS
    MaxTime = 5
    Timeout = 2
INVARIANTS
    TypeOK
    NoBlankWhilePrinting
PROPERTY
    NoBlindPrint
CHECK_DEADLOCK FALSE