MCLola

MCLola is an EDSL written in Haskell that provides:

• A language, called MCLola, to write high level specifications based on Lola [1].
• A mechanism to compile MCLola specifications to C99 files that implement a monitor for the specification.

This project was developed within a research internship at IMDEA Institute, Madrid, Spain.
Student: Aldana Ramirez
Adviser: Cesar Sanchez
Collaborators: Martin Ceresa and Felipe Gorostiaga

Installation

To use MCLola, you need to install required software as specified below. Alternatively, a Dockerfile is provided to simplify the installation process.

Requirements

1. Install GHC.

2. Install the following Haskell libraries:

   • language-c99
   • language-c99-simple
   • pretty
   • compdata
   • base
   • mtl
   • containers

Dockerfile

1. Download this repo.

   git clone https://github.com/imdea-software/McLola.git

2. Build the Docker image for the project.

   cd McLola/
   docker build -t mclola .

3. Run a container using the image built above.

   docker run -it -v "$(pwd)":/MCLola --rm mclola bash

   This command also mounts the MCLola directory and opens an interactive shell. The -rm option erases the container when its execution finishes.

Usage

1. Write the MCLola specification.
   Create a new file that defines an element spec :: Specification and modify file src/Compile.hs:

   • Import the new file.
   • Define importedSpec as spec.

2. Generate C99 files for the monitor.
   Move to the MCLola/src directory and open GHCi:

   ghci

   Load the Compile.hs file and evaluate:

   • codegen to generate C99 files to implement the monitor for the specification.
   • analyse to generate a txt file with temporal information from the specification.

   All generated files are stored in the src/monitor directory.

   :l Compile.hs
   
   codegen
   analyse

3. Complete the monitor implementation.
   Write a monitor.c file that defines a main function that implements the monitor. To that end, use the initialise, step and finish functions generated by MCLola.
   

4. Compile C99 files and execute the monitor with a given input.

   make && ./monitor < input.csv > output.txt

Examples

The src/Example directory includes several examples. For each example, four files are provided:

• A .hs file with the MCLola specification.
• A monitor.c file with the monitor implementation, which uses the files generated by the tool.
• An input.csv file with an example instance for input values.
• An output.txt file with the output generated by the monitor for the instance given by input.csv.

References

[1] B. D'Angelo, S. Sankaranarayanan, C. Sanchez, W. Robinson, B. Finkbeiner, H. B. Sipma, S. Mehrotra, Z. Manna (2005). LOLA: runtime monitoring of synchronous systems. 12th International Symposium on Temporal Representation and Reasoning (TIME'05), pages 166-174.