(***************************************************************************) (* This is a TLC configuration file for testing that TE implies TE2. *) (***************************************************************************) SPECIFICATION TE \* This statement tells TLC that it is to take formula TC2 as \* the specification it is checking. PROPERTY TE \* This statement tells TLC to check that the specification \* implies the property TC2. (In TLA, a specification is \* also a property.) INVARIANT TypeInvariant INVARIANT NotEarlyOrLateAssertion CONSTANT ThreadsPossibleStates = {unstarted, started, waiting, running, finished} unstarted = unstarted started = started waiting = waiting running = running finished = finished verifying = verifying