An example showcasing almost all nifty features of Momba is centered around Racetrack. Originally, Racetrack has been a pen and paper game where a car has to be steered on a two-dimensional grid from a start position to a goal position. We developed a formal model of this game using Momba. This page documents how you may use this model for your own research. It also serves as a paradigmatic example how to leverage Python’s vast ecosystem for documentation and model exploration. This documentation has been generated using Sphinx with embedded Jupyter Notebook cells. Check out the Sphinx source of this page for further details.


The Racetrack model is not bundled with Momba but can easily be installed as follows:

pip install racetrack

The full source code of this package is available here.

The racetrack package also comes with an interactive game mode where you can steer the car through the track and thereby explore the behavior of the formal model.