Feature: reintroduce Apalache functionalities
danwt opened this issue · 1 comments
Feature
Wrap Apalache with raw and pure functionalities (as is done for TLC in a269ae9)
Summary
c2a3f87 snapshots the codebase in a state that implemented wrappers for the Apalache model checker v0.17.0.
Apalache is now at version 0.19.x and has undergone changes in
- The way it writes to the filesystem (the output paths/directories are different)
- The structure of the traces it provides (now gives Informal Trace Format)
- Possibly some changes in the cli
We should update to keep up with these changes.
Steps
- 1. Checkout the snapshot and try to use it with Apalache 0.17.0 to see the goal.
- 2. Compare with the way the TLC wrapper is implemented
- 3. Mirror the current TLC wrapper, but for Apalache
An example of 'trickiness'
In Apalache 0.17.0 it was necessary to parse stdout to read the name of the directory that Apalache wrote it's output to. This lead to a solution here. This is an example of something that I'm sure has changed. Therefore this parsing may no longer be necessary.
There might be a few small tricks/non-obvious things going on here. Please ask me for help if you need it.
Resources
The branch
https://github.com/informalsystems/mbt-python/tree/danwt/apalache-0.17.0-checkpoint
checkpoints the functionality when it was implemented for Apalache 0.17.0.