A manager for TLA projects

  • By Adrien Champion, Keryan Didier, Steven de Oliveira, OCamlPro.

Matla is a manager for TLA+ projects written in Rust and pronounced like "matelas", which is French for "mattress". It is heavily inspired by cargo, the critically acclaimed Rust project manager.

This user manual assumes you are familiar with TLA+ and its associated verification engine TLC.

Matla is not a big project, it is inspired by cargo but nowhere near as complex or feature-packed. We develop matla with three things (a trifecta of sorts) in mind: safety (confidence in the code and thus the analysis), simplicity and ergonomics. This last aspect is not here for PR reasons: as heavy Rust users, we recognize how nice an experience it is to interact with a tool with readable, colored output, and where each interaction shows a great deal of care for user-friendliness.


There is a TLDR at the end of this file for crash course on using matla.


Matla is still very young. There are many issues to address; some of them have to do with quirks at TLC-level, others are just blind spots that we have not triggered yet in our use of matla. If you run into some of these problems, consider opening an issue to help us improve matla 😸

Main features currently implemented

Motivated in the next section and discussed in details in the rest of this document:

  • retrieve/handle/update the TLA+ toolbox tla2tool.jar behind the scenes;
  • convenient automatic project initialization;
  • deal with the files generated by TLC's analyses cleanly, in a gitignored target folder where all compilation/run artifacts live;
  • allow users to have a global configuration (specifying TLC arguments such as seed, difftrace, ...), (potentially/partially) overridden by the project configuration, (potentially/partially) overridden by command-line configuration (options);
  • handling integration tests in a directory that's distinct from the main source directory;
  • debug assertions, i.e. assertions checked in debug mode but compiled away in release mode (the mode is specified by users whenever they call matla, e.g. matla run --release);
  • modernized output with clearer error messages: very much WIP at the moment, most likely requires a collaboration with the TLC team;
  • pretty, readable counterexample traces.

Features we are considering implementing soon-ish

Very strong emphasis on soon-ish:

  • unit tests specified in TLA+ source files;
  • documentation tests specified in comments in the TLA+ source files;
  • documentation generation: the TLA+ toolbox can generate a very nice PDF of the sources using LaTeX, but on big projects the lack of hyperlinks, search bar, etc. can be quite frustrating. It is also not clear we can have documentation tests appear nicely in the documentation using TLA+ toolbox's documentation capabilities. Also, we are quite fond of markdown as a (code) documentation language given how simple and universal it has become (for better or worse);

Features we might consider at some point

  • notion of dependency (library), most likely building on git-based online services;
  • optional static type-checking: quite ambitious as it requires parsing, representing and manipulating (subsets of) the TLA+ language. Do not hold your breath.

TL;DR

  • install by retrieving the latest release or using cargo

    cargo install https://github.com/OCamlPro/matla#latest

  • setup, required unless you plan to run in portable mode (matla --portable .../matla -p ...)

    matla setup

  • initialize a project directory

    matla init

  • run top.tla/top.cfg

    matla run top

    or matla run if there is only one .tla/.cfg pair in the project directory

  • run tests (modules with .tla and .cfg files) in <proj_dir>/tests

    matla test

  • you will probably want to read about matla's user/project/cla configuration hierarchy