Add Apalache wrappers and configurations for example specifications#209
Draft
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. Resolve the launcher
per-platform and route batch files 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>
Translate`CHECK_DEADLOCK FALSE` into Apalache's `--no-deadlock` CLI flag. Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
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
1 participant
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.
For each spec where it was feasible, add:
AP.tla -- a non-invasive wrapper module that INSTANCEs the untyped original specification with typed CONSTANTS and VARIABLES, so that
apalache-mc typecheckaccepts the spec without modifying the source. A few wrappers also shadow polymorphic helpers (Sum,Range, ToSet, ...) with monomorphic versions, or defineVal` operators used by the .cfg below to fill in uninterpreted-type constants.AP.cfg -- a TLC-style model configuration adapted for Apalache. Each .cfg drives
apalache-mc checkfor the spec's safety properties (TLCPROPERTIESare intentionally dropped). Constants are either inlined (Int/Bool/Str) or substituted viaConst <- ConstValto attach the right uninterpreted type.