3 ms·
TLC is the model checker that operates on TLA+ specs. TLAPS is a proof system. So, TLA+ has both.
by duality 7y ago
TLC is the model checker that operates on TLA+ specs. TLAPS is a proof system. So, TLA+ has both.
- strangecasts 7y agoYep :) Hence "most" - you can write deductive proofs with TLAPS, but most of the documentation and the community is devoted to model-checking.