The TLA+ models/specifications described here should not be confused with TLC models. A TLC model is a finite instance of a TLA+ model/specification used to model check it. For example, you might have TLC check a TLA+ model/specification of an N-process system with a TLC model in which N equals 3.