Examples Add some Apalache models

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.

Jan 18 '24 14:01 ahelwer

Here's a first one: https://github.com/tlaplus/Examples/pull/112

Jan 21 '24 16:01 nano-o

Also this one: https://github.com/tlaplus/Examples/pull/113

Jan 22 '24 18:01 nano-o

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"

Feb 06 '24 17:02 ahelwer

https://github.com/tlaplus/Examples/blob/789a653495f2e41d449d28e3935b15ab4b21e147/.devcontainer/install.sh#L40-L45

Feb 06 '24 17:02 lemmy

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: https://github.com/informalsystems/apalache/discussions/2824

Feb 06 '24 17:02 ahelwer