| Display the liveness checking startup banner only once. |
|
More...
|
4 months ago
|
| Checking liveness properties in simulation mode creates a scalability bottleneck due to unnecessary sharing of ILiveCheck instances. |
|
More...
|
4 months ago
|
| SANY: Only add variant once to commandVariants. |
|
More...
|
4 months ago
|
| SANY: remove unused 'stats' feature. |
|
More...
|
4 months ago
|
| Continue job even if publishing to OSS Sonatype fails. |
|
More...
|
4 months ago
|
| Evaluate the ALIAS expression on counterexamples generated by liveness checking while running in simulation mode. |
|
More...
|
4 months ago
|
| Support running the TLA+ debugger with multiple workers. |
|
More...
|
4 months ago
|
| Support running the TLA+ debugger with multiple workers. |
|
More...
|
4 months ago
|
| Cancel PR CI workflow runs when newer changes are pushed |
|
More...
|
4 months ago
|
| Cannot debug TLC VIEW with TLA+ Debugger. |
|
More...
|
4 months ago
|
| ClassCastException when evaluating TLCGet("spec") with coverage enabled. |
|
More...
|
4 months ago
|
| SANY XML: added CLI help text |
|
More...
|
4 months ago
|
| SANY XML: add pretty-print CLI option |
|
More...
|
4 months ago
|
| SANY XML exporter: use local schema file |
|
More...
|
4 months ago
|
| Added syntax tests for tuples |
|
More...
|
4 months ago
|
| Annotate the GraphNode if it fulfills the promises. |
|
More...
|
4 months ago
|
| Add link to asynchronous version of Conway's Game of Life |
|
More...
|
4 months ago
|
| Syntax tests: added additional failing cases |
|
More...
|
4 months ago
|
| Syntax tests: fixed number set definition translation |
|
More...
|
4 months ago
|
| Syntax tests: fixed proof step translation |
|
More...
|
4 months ago
|
| Syntax tests: resolve node kinds to human-readable strings |
|
More...
|
4 months ago
|
| Syntax tests: added ability to skip or expect failures |
|
More...
|
4 months ago
|
| Added syntax tests from TLAPM work |
|
More...
|
4 months ago
|
| Leave note about related conf talk https://www.youtube.com/watch?v=cYenTPD7740 |
|
More...
|
4 months ago
|
| POSTCONDITION is evaluated twice with different values for TLCExt!Counterexample when TLC detects a liveness violation. |
|
More...
|
4 months ago
|
| Rename confusing variable name in AddTwo.tla (#152) |
|
More...
|
4 months ago
|
| Generate HTML railroad diagram from TLA+ JavaCC grammar |
|
More...
|
4 months ago
|
| Broke tla2sany unit tests into submodules Also restricted visibility of tla2sany.semantic.Context.Pair |
|
More...
|
4 months ago
|
| Convert TLC.traceNum to a non-static class variable |
|
More...
|
5 months ago
|
| Add small improvements to the Disruptor spec. (#151) |
|
More...
|
5 months ago
|
