(***************************************************************************) (* This is a TLC configuration file for testing that TypeInvariant is *) (* an invariant of the specification TC *) (***************************************************************************) SPECIFICATION TE \* This statement tells TLC that TE is the specification that it \* should check. PROPERTY TE INVARIANT TypeInvariant \* This statement tells TLC to check that formula TypeInvariant is an \* invariant of the specification--in other words, that the \* specification implies []TypeInvariant. CONSTANT ThreadsPossibleStates = {unstarted, started, waiting, running, finished} unstarted = unstarted started = started waiting = waiting running = running finished = finished verifying = verifying