Chai is a Python RPC client to interact with the Server for Human-Apalache Interaction (or Shai). It enables transparent interactions with the Apalache model checker via python function calls.
Chai is developed by the Apalache team at Informal Systems.
You can install the apalache-chai library from this git repo with:
pip install git+https://github.com/informalsystems/apalache-chai.gitIf you are using poetry to manage your project,
you can add a dependency on apalache-chai with:
poetry add git+https://github.com/informalsystems/apalache-chai.gitgit clone --recurse-submodules [email protected]:informalsystems/apalache-chai.gitThe --recurse-submodules flag is needed because we use a git submodule to
bring in the .proto files from Apalache.
poetry shellTo update he proto files, first update to the desired commit of the apalache
submodule, then regenerate the gRPC code, e.g.,
pushd apalache && git pull && popod
make update-grpcWe use pdoc for generating our API docs.
You can run the doc server on the code base with
poetry run pdoc ./chaiUnit tests are defined in ./tests.
Run the unit tests (this also runs static analysis via pyright):
make test- Ensure required version of Apalache is built by running
make apalache. - Source the .envrc (automatic if you use
direnv). - The nix package manager with flakes enabled
The reason for depending on nix for our integration test is as follows: To run
the integration tests, we need the version of Apalache included as a git
submodule. We ensure the version is kept in sync by building the Apalache
executable from the exact same git submodule used to obtain the proto files.
Since we are building Apalache, we need to ensure that we have all build
dependencies. We therefore reuse Apalache's flake.nix, which is already
maintained and ensures pre-requisties are supplied.
make integration