Add Apalache wrappers and configurations for example specifications#209
Open
Add Apalache wrappers and configurations for example specifications#209
Conversation
For each spec where it was feasible, add:
* AP<Spec>.tla -- a non-invasive wrapper module that INSTANCEs the
untyped original specification with typed CONSTANTS and VARIABLES,
so that `apalache-mc typecheck` accepts the spec without modifying
the source. A few wrappers also shadow polymorphic helpers (`Sum`,
`Range`, ToSet`, ...) with monomorphic versions, or define
`<Const>Val` operators used by the .cfg below to fill in
uninterpreted-type constants.
* AP<Spec>.cfg -- a TLC-style model configuration adapted for
Apalache. Each .cfg drives `apalache-mc check` for the spec's
safety properties (TLC `PROPERTIES` are intentionally dropped).
Constants are either inlined (Int/Bool/Str) or substituted via
`Const <- ConstVal` to attach the right uninterpreted type.
Co-authored-by: Claude Code 4.7 <claude@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
…s for Apalache Temporarily disable various checks in the CI workflow related to Unicode and manifest validation, as Apalache cannot model-check Unicode-translated specifications. Adjust the model checks to focus solely on Apalache-compatible configurations, specifically restricting checks to AP*.cfg files. This change is part of ongoing efforts to integrate Apalache into the CI process. Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
`tla_utils.check_model` hard-coded `bin/apalache-mc`, but on Windows
the launcher is `bin/apalache-mc.bat` and `subprocess.run` cannot
spawn `.bat` files via CreateProcess directly. Pick the launcher per
platform and route the Windows batch file through `cmd.exe /c`.
This was latent because the only symbolic-mode model in CI
(EinsteinRiddle) was always being skipped: `[ ${{ matrix.unicode }} ]`
in CI.yml is truthy for both "true" and "false", so the SKIP entry
was added unconditionally rather than only on the Unicode variant.
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Collaborator
|
Good idea! |
Translate`CHECK_DEADLOCK FALSE` into Apalache's `--no-deadlock` CLI flag. Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Always pass `--length=5` to `apalache-mc check` from the CI driver, instead of opting individual model .cfg files in via a per-model marker comment. Apalache's own default of 10 is just as arbitrary; 5 keeps the suite within CI timeouts while still exercising each spec. Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
konnov
reviewed
Apr 23, 2026
Collaborator
konnov
left a comment
konnov
left a comment
There was a problem hiding this comment.
This looks nice! I really like the trick with introducing an additional instance to deal with type annotations. I noticed a few temporary fixes in the yml files. You probably want to fix those first
Comment on lines
+152
to
+153
| line. Used to translate the directive to Apalache's `--no-deadlock` CLI | ||
| flag, since Apalache silently ignores it in the config file. |
Collaborator
There was a problem hiding this comment.
It's worth opening an issue in Apalache on that
Member
Author
There was a problem hiding this comment.
Is it feasible for this PR to wait on this feature to appear in Apalache?
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
AI has made substantial progress over the past few years, and that progress is starting to have very practical implications for tooling like Apalache.
Around 2–3 years ago, I experimented with using AI to synthesize Apalache-style type annotations. At the time, even frontier models struggled to consistently produce syntactically correct annotations, which made the approach impractical.
Revisiting this recently with Claude Opus 4.7 shows a clear shift. When provided with the type annotation guide from the Apalache repository and given CLI access to Apalache (no Skills, MCPs, ...), the model was able to synthesize type annotations for a large portion of the existing TLA+ examples. The total wall-clock time for this process was on the order of a few hours.
That said, a meaningful portion of the remaining specs will require deeper changes. A key challenge is that Apalache's type system distinguishes between sequences, records, and functions, whereas in TLA+ these are all represented uniformly as functions. Bridging that conceptual gap will require structural refactoring rather than straightforward annotation, and Apalache's Variant type will likely be relevant.