This repository is part of Runtime Verification of Hard Realtime Systems with Copilot: A Tutorial, at Formal Methods 2024, September 9 2024. It contains a set of exercises that is used during the session, together with a Dockerfile for quickly getting a working Copilot installation.

This repository contains a number of files and directories:

. ├── Dockerfile ├── INSTALL.md ├── Makefile ├── README.md ├── answers ├── bin │   └── rundocker └── exercises    ├── ...    └── test    ├── Main.hs    └── run.sh 

The interesting files are:

• Dockerfile: defines the Docker image that we will be using.
• Makefile: helps us build the Docker image.
• answers/: The answers to the exercises.
• bin/rundocker: A wrapper script for running things inside Docker.
• exercises/: Directory containing exercises. Each exercise has its own subdirectory and a run.sh script for running it. test is not an exercise, but just a simple way to test your installation.

Please see INSTALL.md for installation.

Each exercise comes with its own file. There are two ways to run them, either by passing bin/rundocker runhaskell followed by the file to run:

$ bin/rundocker runhaskell exercises/Ex??-??.hs

Or, passing no arguments to open up a terminal inside the container in which we can call runhaskell:

$ bin/rundocker # cd /exercises/ # runhaskell Ex??-??.hs