Tutorial: How to set up and use the Mule Docker image? 

In this tutorial we describe how to set up and execute the model checker Mule using Docker. The steps considered throughout the tutorial are:
1. Install Docker

Tutorials on how to install Docker on most operating systems are provided on its official website and will not be explicitly restated here. 

For your convenience a direct link to these tutorials for Windows, Linux and Mac OS X users are given below:
After installing Docker you should be able to run the following command from a regular terminal on Linux, respectively from a Docker terminal on Mac OS X and Windows:

docker --help

In the following the word terminal will refer to the regular terminal for Linux users, respectively the Docker terminal for Mac OS X and Windows users.

Click here to go back to the top of the page.

2. Download Mule Docker image

The Mule Docker image is made freely available online in the Docker Hub Registry. It can be downloaded using the following command in the terminal:

docker pull icerage/mule

where "icerage" is the username of Ovidiu Parvu and "mule" is the name of the Docker Hub repository.

Click here to go back to the top of the page.

3. Create and run Mule Docker container

To create and run a Docker container using the Docker image downloaded at the previous step execute the following command in the terminal:

docker run -ti icerage/mule

where the command line arguments "-ti" are used to ensure that commands can be executed in the Docker container using standard input; see the documentation of the Docker run command for more details.

After executing the immediately above command the last line in your terminal should look similar to:


This is an indication that the container was successfully created and commands can be executed inside it.

Click here to go back to the top of the page.

4. Run model checker Mule

To display the help page of Mule execute the following command in the terminal:

Mule --help

Click here to go back to the top of the page.

5. Case study: Acute inflammation of the gut and lung

We illustrate how to use Mule for the verification of a computational model based on the acute inflammation of the gut and lung case study.

5.1. Download model simulation traces

First of all an archive will be downloaded containing the model simulation traces previously generated for the acute inflammation of the gut and lung case study:

wget http://ovidiuparvu.com/data/software/mule/case_studies/acute_inflammation_of_gut_and_lung/acute_inflammation_of_gut_and_lung_mstml_dataset.zip

Remark: Alternatively it is possible to download the computational model and generate simulation traces on demand but this requires additionally installing the corresponding model simulator.

Next a folder is created in which the contents of the model simulation traces archive are extracted. The archive is then removed. This can be done by executing the following command in the terminal:

mkdir traces && unzip acute_inflammation_of_gut_and_lung_mstml_dataset.zip -d traces && rm acute_inflammation_of_gut_and_lung_mstml_dataset.zip

5.2. Download formal PBLMSTL specification
Afterwards the formal PBLMSTL specification is downloaded by executing the following command in the terminal:

wget http://ovidiuparvu.com/data/software/mule/case_studies/acute_inflammation_of_gut_and_lung/specification_pblmstl_acute_inflammation_of_gut_and_lung.in

5.3. Download multiscale architecture graph

The multiscale architecture graph is downloaded using the following command:

wget http://ovidiuparvu.com/data/software/mule/case_studies/acute_inflammation_of_gut_and_lung/multiscale_architecture_graph_acute_inflammation_of_gut_and_lung.xml

5.4. Execute model checker

Finally the model checker Mule can be executed considering the model simulation traces, the formal PBLMSTL specification and the multiscale architecture graph using a statistical model checking algorithm with the probabilities of type I and type II errors set to 5% using the following command:

Mule -v -q specification_pblmstl_acute_inflammation_of_gut_and_lung.in -t traces -a multiscale_architecture_graph_acute_inflammation_of_gut_and_lung.xml -m 1 -e 0 --type-I-error 0.05 --type-II-error 0.05

where the command line argument:
  • "-v" specifies that the model checker should be executed in "verbose" mode;
  • "-q" specifies the path to the logic queries or formal PBLMSTL specification;
  • "-t" specifies the path to the folder containing the model simulation traces;
  • "-a" specifies the path to the multiscale architecture graph;
  • "-m" specifies which model checking algorithm should be employed (e.g. 1 = frequentist statistical);
  • "-e" specifies the extra evaluation time i.e. if there are insufficient model simulation traces available how many minutes should Mule wait for new model simulation traces to be potentially provided;
  • "--type-I-error" specifies the probability of type I errors;
  • "--type-II-error" specifies the probability of type II errors.
Click here to go back to the top of the page.