intsoft/tlaplus：提供TLC模型检查器，用于系统行为、并发协议与状态性质的形式化验证。

Reject models that define more than 32768 model values.

ModelValue#write serializes a model value’s index as a short. When a state is read back from the disk-backed state queue, an index of 32768 to 65535 raises an ArrayIndexOutOfBoundsException, while an index of 65536 or more silently aliases another model value. Such aliasing can disable an action and thereby mask a reachable invariant violation.

32768 model values are more than enough for any model that TLC can realistically check. Rejecting larger models when constants are processed keeps the serialized format unchanged and turns the unsound result into an error.

Fixes Github issue #1500 https://github.com/tlaplus/tlaplus/issues/1500

[Bug][Tests][TLC]

Co-authored-by: Claude Opus 5.5 noreply@anthropic.com Signed-off-by: Markus Alexander Kuppe github.com@lemmster.de

Overview

This repository hosts the core TLA⁺ command line interface (CLI) Tools and the Toolbox integrated development environment (IDE). Its development is managed by the TLA⁺ Foundation. See http://tlapl.us for more information about TLA⁺ itself. For the TLA⁺ proof manager, see http://proofs.tlapl.us.

Versioned releases can be found on the Releases page. Currently, every commit to the master branch is built & uploaded to the 1.8.0 Clarke pre-release. If you want the latest fixes & features you can use that pre-release. If you want to consume the TLA⁺ tools as a Java dependency in your software project, Maven packages are periodically published to central.sonatype.org.

Use

The TLA⁺ tools require Java 11+ to run.

To use TLA⁺ from a graphical interface, see the TLA⁺ VS Code extension. The Eclipse-based TLA⁺ Toolbox GUI is also available from this repository, but it is currently unmaintained.

Get tla2tools.jar from the releases to use the tools from the command line. The tla2tools.jar file contains multiple TLA⁺ tools; after adding tla2tools.jar to your CLASSPATH, the tools can be used as follows:

EXPORT CLASSPATH=tla2tools.jar
java tla2sany.SANY -help  # The TLA⁺ parser
java tlc2.TLC -help       # The TLA⁺ model checker
java tlc2.REPL            # Enter the TLA⁺ REPL
java pcal.trans -help     # The PlusCal-to-TLA⁺ translator
java tla2tex.TLA -help    # The TLA⁺-to-LaTeX translator
java tla2sany.xml.XMLExporter -help # Export TLA⁺ parse tree as XML

Running java -jar tla2tools.jar is aliased to run tlc2.TLC.

For more information on using & consuming the TLA⁺ tools, see USE.md.

Developing & Contributing

The TLA⁺ Tools and Toolbox IDE are both written in Java. The TLA⁺ Tools source code is in tlatools/org.lamport.tlatools. The Toolbox IDE is based on Eclipse Platform and is in the toolbox directory. For instructions on building & testing these as well as setting up a development environment, see DEVELOPING.md.

We welcome your contributions to this open source project! TLA⁺ is used in safety-critical systems, so we have a contribution process in place to ensure quality is maintained; read CONTRIBUTING.md before beginning work.

License & Copyright

Licensed under the MIT License.