| Added Eclipse project setting file enforcing UTF-8 |
|
More...
|
5 months ago
|
| Convert MODEL_PART_OF_JAR static variable to class variable |
|
More...
|
5 months ago
|
| A race can occur in `TLCExt!TLCGetAndSet` if `key \in DOMAIN TLCGet("all")` evaluates to true because the key has already been `TLCSet` in the thread-local storage of worker A, but the thread-local storage of the worker (thread), evaluating `TLCGet(key)`, has not (yet) been set. |
|
More...
|
5 months ago
|
| `TLCExt!TLCEvalDefinition(name)` equals the value of the definition (reachable from the root module) with that name. |
|
More...
|
5 months ago
|
| TLC throws an EvalException when reconstructing a counterexample if the next-state relation involves `TLC!RandomElement`. |
|
More...
|
5 months ago
|
| Evaluate `_PERIODIC` in simulation mode. |
|
More...
|
5 months ago
|
| Include CONSTRAINT and ACTION_CONSTRAINT in TLCGet("spec"). |
|
More...
|
5 months ago
|
| Updated copyright info in README and LICENSE |
|
More...
|
5 months ago
|
| `TLCExt!TLCEvalDefinition(name)` equals the value of the definition (reachable from the root module) with that name. |
|
More...
|
5 months ago
|
| Added note about sonatype maven packages to top-level README Also added badge |
|
More...
|
5 months ago
|
| Add documentation for `constrained` sub-command that causes TLC to include states in the dot file that are excluded from the model via a state or action constraint. |
|
More...
|
5 months ago
|
| Upload tla2tools.jar maven packages to OSS Sonatype (see ossrh.xml.README) instead of authentication-only Github maven packages. |
|
More...
|
5 months ago
|
| Removed parser support for set-except syntax |
|
More...
|
5 months ago
|
| Removed dead code from JavaCC-generated parser |
|
More...
|
5 months ago
|
| Add syntax tests to improve parser code coverage |
|
More...
|
5 months ago
|
| Bump tla2tools.jar maven version to 1.8.0 |
|
More...
|
5 months ago
|
| Print a log message whenever simulator has finished to compute initial state |
|
More...
|
5 months ago
|
| Added some basic tests for the level checker |
|
More...
|
5 months ago
|
| Simplified & documented JList parsing code |
|
More...
|
5 months ago
|
| Add spec of the Disruptor concurrency library. (#150) |
|
More...
|
5 months ago
|
| Allow CommunityModules to trigger a build by sending a repository_dispatch |
|
More...
|
5 months ago
|
| Better parameterized instantiation support in behavior spec. |
|
More...
|
5 months ago
|
| Refinement checking for INSTANCEs with arguments. |
|
More...
|
5 months ago
|
| Don't enforce LF line endings on JavaCC-generated code This interferes with how git line endings work on Windows |
|
More...
|
6 months ago
|
| Moved canonical op defs out of ConfigConstants.java |
|
More...
|
6 months ago
|
| Statically initialize built-in op levels |
|
More...
|
6 months ago
|
| Removed config.jj parser |
|
More...
|
6 months ago
|
| Load built-in ops statically |
|
More...
|
6 months ago
|
| Added unit test for built-in op init |
|
More...
|
6 months ago
|
| Added simple syntax error test |
|
More...
|
6 months ago
|
