Add Apalache wrappers and configurations for example specifications#209
Open
Add Apalache wrappers and configurations for example specifications#209
Conversation
lemmy
force-pushed
the
mku-Apalache
branch
3 times, most recently
from
7919c07 to
22a2165
Compare
Collaborator
|
Good idea! |
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
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.
Requires Apalache 0.57 due to apalache-mc/apalache#3311
Co-authored-by: Claude Code 4.7 <claude@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Update CI workflow to disable Unicode checks and restrict model checks 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>
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>
Continues 4ed740d. Adds nine more non-invasive AP<Spec>.tla wrappers (plus matching .cfg files where apalache-mc check is feasible): * acp/APACP_SB.tla -- the seven uninterpreted "tag" constants (yes/no/undecided/commit/abort/waiting/notsent) are typed Str and substituted with concrete strings; participants use the uninterpreted PARTICIPANT type. Uses INIT/NEXT because the original Spec adds fairness; CHECK_DEADLOCK FALSE matches ACP_SB_TLC.cfg. * Disruptor/APRingBuffer.tla -- typecheck-only. RingBuffer is a helper module with no Next; the protocol invariants are exercised end-to-end via APDisruptor_SPMC / APDisruptor_MPMC. * SpecifyingSystems/HourClock/APHourClock2.tla -- the (hr % 12) + 1 reformulation of HourClock. * SpecifyingSystems/Composing/APHourClock.tla, SpecifyingSystems/Composing/APChannel.tla, SpecifyingSystems/FIFO/APChannel.tla, SpecifyingSystems/Liveness/APHourClock.tla -- wrap the duplicate HourClock.tla / Channel.tla files kept in each chapter directory of the Specifying Systems repository so that consumers in those chapters can EXTENDS HourClock / Channel from a sibling. * SpecifyingSystems/FIFO/APInnerFIFOInstanced.tla -- the hand-expanded variant of InnerFIFO that does not use INSTANCE (because old TLC versions did not support it). * SpecifyingSystems/FIFO/APMCInnerFIFO.tla -- TLC-style model wrapper around InnerFIFOInstanced that adds the bounded-queue constraint Len(q) <= qLen. manifest.json files for acp/, Disruptor/, and SpecifyingSystems/ are updated with the new wrappers; check_manifest_files.py and check_manifest_schema.py both pass. Co-authored-by: Claude Code 4.7 <claude@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Member
Author
|
The last commit introduces type annotations to a few additional steps. Claude Opus 4.7 claims that it cannot add type annotations to the remaining specifications without altering them. |
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 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.