| CI: filter on max proof time in manifests (#213) |
|
More...
|
about 1 month ago
|
| Add an hypothesis why CASE is rejected with TLC_LIVE_CANNOT_HANDLE_FORMULA. |
|
More...
|
about 1 month ago
|
| Skip Apalache-specific examples in parse-only CI steps. |
|
More...
|
about 1 month ago
|
| Allow RECURSIVE operators to define liveness properties. |
|
More...
|
about 1 month ago
|
| CI: record proof runtime (#206) |
|
More...
|
about 1 month ago
|
| Close missing BY clauses in TypeOK_Step network cases |
|
More...
|
about 1 month ago
|
| tcp: add TLAPS safety proof for RFC 9293 state machine |
|
More...
|
about 1 month ago
|
| Remove outdated Folds and Functions modules from FiniteMonotonic specifications. Update manifest.json to reflect these deletions. |
|
More...
|
about 1 month ago
|
| List the new `_proof.tla` files in per-spec manifest.json and README.md |
|
More...
|
about 1 month ago
|
| BlockingQueue: bump submodule to v39 |
|
More...
|
about 1 month ago
|
| Add TLAPS proof companions for example specifications |
|
More...
|
about 1 month ago
|
| Name unnamed ASSUMEs in three example specifications |
|
More...
|
about 1 month ago
|
| Allow INSTANCE with multiple substitutions in PlusCal `define` blocks. |
|
More...
|
about 1 month ago
|
| Fix overlay tree edge definition in comment of EWD687a.tla |
|
More...
|
about 2 months ago
|
| Stop periodically printing `_PrintCounts` for `_POSSIBLE` |
|
More...
|
about 2 months ago
|
| Skip Apalache when running tlaplus/examples specs in Unicode mode. |
|
More...
|
about 2 months ago
|
| Add TLCGet("revision").calver and use it to tag every master build with its CalVer string. |
|
More...
|
about 2 months ago
|
| ewd998: move RECURSIVE SimpleCycle from Utils.tla to EWD998_anim.tla |
|
More...
|
about 2 months ago
|
| CI: skip Apalache checks on Unicode specs |
|
More...
|
2 months ago
|
| CI: Default Apalache --length=5 for all examples |
|
More...
|
2 months ago
|
| CI: invoke Apalache via apalache-mc.bat (and cmd.exe) on Windows |
|
More...
|
2 months ago
|
| Fix variable name in markdown table check script. |
|
More...
|
2 months ago
|
| Add Apalache wrappers and configurations for example specifications |
|
More...
|
2 months ago
|
| CI: check proofs using find | jq | xargs bash pipeline (#205) |
|
More...
|
2 months ago
|
| Add support for asserting reachability of state- and action-level predicates. |
|
More...
|
3 months ago
|
| Allow multiple postconditions in .cfg files, matching the convention of INVARIANTS/PROPERTIES. |
|
More...
|
3 months ago
|
| Add string-keyed per-worker registers to TLCGet/TLCSet |
|
More...
|
3 months ago
|
| Shutdown executor after liveness trace reconstruction |
|
More...
|
3 months ago
|
| Skip JUnit report publishing for fork PRs where GITHUB_TOKEN is read-only. |
|
More...
|
3 months ago
|
| CI: Parse examples using find | xargs bash pipeline Remove dependency on Python script |
|
More...
|
3 months ago
|
