Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add some Apalache models #108

Open
ahelwer opened this issue Jan 18, 2024 · 5 comments
Open

Add some Apalache models #108

ahelwer opened this issue Jan 18, 2024 · 5 comments

Comments

@ahelwer
Copy link
Collaborator

ahelwer commented Jan 18, 2024

Currently no specs included in the repository have an Apalache model. It would be nice to have some examples of this. The Einstein's Riddle spec would be an ideal first candidate, as TLC has a tough time with it. Apalache could then be added to the CI checks.

@nano-o
Copy link
Contributor

nano-o commented Jan 21, 2024

Here's a first one: #112

@nano-o
Copy link
Contributor

nano-o commented Jan 22, 2024

Also this one: #113

@ahelwer
Copy link
Collaborator Author

ahelwer commented Feb 6, 2024

Saving this here for future addition to CI download script:

# Get Apalache
wget -qN https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz -P /tmp
tar -xzf /tmp/apalache.tgz --directory "$DEPS_DIR"
mv "$DEPS_DIR/apalache-*" "$DEPS_DIR/apalache"

@lemmy
Copy link
Member

lemmy commented Feb 6, 2024

## Install Apalache
wget -qN https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz -P /tmp
mkdir -p tools/
tar -xvfz /tmp/apalache.tgz --directory tools/
echo 'export PATH=$PATH:/workspace/Examples/tools/apalache/bin:/workspaces/Examples/tools/apalache/bin' >> $HOME/.bashrc
tools/apalache/bin/apalache-mc config --enable-stats=true

@ahelwer
Copy link
Collaborator Author

ahelwer commented Feb 6, 2024

I did base it on that! Currently this is the only thing holding back adding apalache to the CI, because I want to import Apalache.tla from the Einstein Riddle spec for some fun additional type annotations: apalache-mc/apalache#2824

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Development

No branches or pull requests

3 participants