TLC does explicit state enumeration. The tool is described in Yuan Yu, Panagiotis Manolios, Leslie Lamport: Model Checking TLA+ Specifications. 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 1999). Bad Herrenalb, Germany. Springer LNCS 1703, pp. 54-66. Regards, Stephan
|