Conversation
There was a problem hiding this comment.
Pull request overview
This PR adjusts the Variants standard module so that its default (TLC/TLAPS-visible) definitions no longer trigger TLC edge-case bugs, and adds TLC-based integration tests to guard against regressions when using Apalache modules with TLC.
Changes:
- Reworked the untyped implementations of
Variant,VariantFilter,VariantTag,VariantGetOrElse, andVariantGetUnsafeinVariants.tlato use a function-based encoding that TLC handles correctly. - Documented and exercised TLC-compatible behavior of Apalache operators (notably
MkSeq,FunAsSeq,Guess, and fold operators) via newTestApalache.tlaandTestVariants.tlamodels, driven by a shared TLC config. - Added an mdx-based TLC integration test driver (
tlc-integration-tests.md) and corresponding changelog entry to systematically run TLC against the Apalache/Variants modules.
Reviewed changes
Copilot reviewed 7 out of 7 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
src/tla/Variants.tla |
Switches variant representation to single-key functions and updates helper operators so TLC’s semantics align better with Apalache’s intended typed view. |
src/tla/Apalache.tla |
Clarifies the TLC-facing implementation of MkSeq and how it interacts with FunAsSeq, explaining why TLC may fail when __F is partial while Apalache still works symbolically. |
test/tla/TestVariants.tla |
Adapts the existing variant tests to the new encoding and adds a tiny state machine so the variant tests can be checked as TLC invariants. |
test/tla/TestApalache.tla |
Introduces a dedicated TLC model that validates key Apalache operators (MkSeq, FunAsSeq, Guess, ApaFoldSet, ApaFoldSeqLeft) behave as expected under TLC, with failing edge cases kept out of AllTests. |
test/tla/test.cfg |
Defines a simple TLC configuration (Init, Next, INVARIANT AllTests) reusable across the new TLC test specifications. |
test/tla/tlc-integration-tests.md |
Adds an mdx test harness that downloads tla2tools.jar and runs TLC against TestVariants.tla and TestApalache.tla; minor doc nits noted (unbalanced parenthesis in the Semantic Versioning link and an example referencing a non-existent section name in this file). |
.unreleased/bug-fixes/tlc3255.md |
Records the bug fix “Make Variants compatible with TLC” for release notes. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
|
|
||
| Since `tla2tools.jar` has been changing under the same version number for over | ||
| four years, we download it every time. This goes against [Semantic | ||
| Versioning](https://semver.org/)), but we cannot enforce good practices at |
There was a problem hiding this comment.
There appears to be an extra closing parenthesis in this sentence after the Semantic Versioning URL (https://semver.org/))); consider dropping one ) so the markdown renders cleanly and the punctuation is balanced.
| Versioning](https://semver.org/)), but we cannot enforce good practices at | |
| Versioning](https://semver.org/), but we cannot enforce good practices at |
| E.g., to run just the test for the `version` command, run | ||
|
|
||
| <!-- $MDX skip --> | ||
| ```sh | ||
| test/mdx-test.py "executable prints version" | ||
| ``` |
There was a problem hiding this comment.
The example here refers to running the test section named "executable prints version", but this file does not define such a section (that heading exists in cli-integration-tests.md). To avoid confusion, it would be better to either reference a heading actually defined in this file (e.g., "TLC prints help") or clarify that this is a generic example taken from the other integration-test file.
|
@copilot open a new pull request to apply changes based on the comments in this thread |
Co-authored-by: konnov <436810+konnov@users.noreply.github.com>
Fix documentation errors in tlc-integration-tests.md
thpani
left a comment
There was a problem hiding this comment.
I don't understand the documented use of mdx-test.py. Maybe I'm missing something
Otherwise, LGTM
| The code blocks in this file use [mdx](https://github.com/realworldocaml/mdx) to | ||
| run integration tests of the Apalache CLI interface. | ||
|
|
||
| To run these tests, execute the [../mdx-test.py](../mdx-test.py) script with no |
There was a problem hiding this comment.
I don't understand.
Don't you have to pass the .md file to the script?
There was a problem hiding this comment.
You are right! Fixed the tests (since they were skipped). Also, included tlc-integration-tests.md in the integration target in Makefile. It thought mdx-test.py was going over all md-files, but it defaults to cli-integration-tests.md.
|
|
||
| <!-- $MDX skip --> | ||
| ```sh | ||
| test/mdx-test.py |
There was a problem hiding this comment.
... and here and the code snippets below?
Closes #3248. As discussed in tlaplus/tlaplus#1284, TLC does not play well with the current implementation of
Variants.tla. This PR fixes the issue by defining variants as functions of singleton domains, so they become more TLC compatible. In addition, we add integration testsTestApalache.tlaandTestVariants.tlaintlc-integration-tests.md, so we would be able to quickly find regressions.make fmt-fix(or had formatting run automatically on all files edited)./unreleased/for any new functionality