Installing Command-Line Tools

Many of the tools can be run from the command line. This page describes how to run various tools on a local machine.

Installing Dependencies

The ABS compiler is contained in a single file called absfrontend.jar.

Running the ABS compiler requires Java (version 21 or greater) and Erlang (version 26 or greater) installed. Java can be downloaded, e.g., from https://adoptopenjdk.net. Erlang is available at https://www.erlang.org/downloads (but also check below for platform-specific instructions).

Installing dependencies on MacOS

On MacOS, the homebrew package manager can be used to install the dependencies. After installing homebrew, run the following commands in a terminal:

brew install erlang git openjdk
export PATH="/opt/homebrew/opt/openjdk/bin:$PATH"

Installing dependencies on Windows

On windows, the chocolatey package manager can be used to install the dependencies. First install chocolatey following the instructions at https://chocolatey.org/install, then run the following command in a terminal with Administrator rights:

choco install openjdk21 git erlang visualstudio2019buildtools

To compile the ABS toolchain, make sure to run the command ./gradlew build from a developer shell (Start -> Visual Studio 2019 -> Developer PowerShell for VS 2019).

Installing dependencies on Linux

On Linux, check if your distribution offers the necessary programs pre-packaged in the version needed (JDK21, Erlang >= 26, a C compiler); otherwise download from the distribution pages linked above.

Using a pre-built ABS compiler

A pre-built absfrontend.jar of the current release of ABS is always linked from https://github.com/abstools/abstools/releases/latest. It can be invoked with java -jar absfrontend.jar --help. (Java and Erlang still need to be installed to run ABS, as above.)

To compile an ABS model model.abs, invoke the compiler with java -jar absfrontend.jar --erlang model.abs, then run the model with ./gen/erl/run.

Using Docker to run the ABS compiler

The latest released ABS compiler is always published as a docker image called abslang/absc:latest. To use this image, first install the docker tool from https://www.docker.com/products/docker-desktop or via your operating system’s package manager.

To install or update the docker image of the ABS compiler, run docker pull abslang/absc:latest. Then, run docker run --rm abslang/absc:latest --help – you should see the help output of the ABS compiler.

To compile an ABS model model.abs in the current directory, invoke the compiler with the following command:

docker run --rm -v "$PWD":/usr/src -w /usr/src abslang/absc:latest --erlang model.abs

To run the model after compiling, either run ./gen/erl/run (if the host machine has erlang installed), or run the model inside docker with the following command:

docker run --rm -v "$PWD":/usr/src -w /usr/src --entrypoint /usr/src/gen/erl/run abslang/absc

Note that using the Model API of a model running inside a docker container requires additional parameters to make the listening port visible on the host system. To run the Model API on port 8080, use the following command:

docker run --rm -v "$PWD":/usr/src -p 8080:8080 -w /usr/src --entrypoint /usr/src/gen/erl/run abslang/absc -p 8080

Compiling the ABS compiler from source

To compile the ABS compiler from source, clone the git repository and run gradle (after installing the necessary dependencies):

# on Linux, macOS
git clone https://github.com/abstools/abstools.git
cd abstools
./gradlew assemble
frontend/bin/absc --help

# on Windows
git clone "https://github.com/abstools/abstools.git"
cd abstools
.\gradlew assemble
frontend\bin\absc.bat --help

At the end of these commands, you should see the help output of the ABS compiler.

The directory abstools/frontend/bin contains convenience scripts absc (for Linux, macOS, other Unix systems) and absc.bat (for Windows) that invoke the ABS compiler. This directory can be added to the PATH environment variable if desired.

To compile an ABS model model.abs, invoke the compiler with absc --erlang model.abs, then run the model with ./gen/erl/run.

Installing Crowbar

For a local installation of the Crowbar verification systems, either download a prepackaged jar file, or compile the code locally. Crowbar requires Java >= 1.8 and an SMT-Solver to run. On an Ubuntu machine, run the following to install Crowbar and run it on an example file:

sudo apt-get install z3
mkdir crowbar
cd crowbar
git clone https://github.com/Edkamb/crowbar-tool.git .
./gradlew assemble
java -jar build/libs/crowbar.jar --full examples/account.abs

The expected output should end in the lines

...
Crowbar  : Final verification result: true
Crowbar  : Verification time: ...
Crowbar  : Total number of branches: 6

Installing KeY-ABS

For a local installation of the KeY-ABS theorem prover, install Java 8. Then, download KeY-ABS from http://i12www.ira.uka.de/key/key-abs/key-abs.zip. Unzipping that downloaded file and double-clicking on the key.jar file should start KeY-ABS. To start from the command line, use:

java -jar key.jar