IMITATOR: Experiments Data for ‘Tuning Trains Speed in Railway Scheduling’

Case Studies Related to Tuning Trains Speed in Railway Scheduling

This page is dedicated to the case studies related to the manuscript Tuning Trains Speed in Railway Scheduling by Étienne André.

IMITATOR

The version of IMITATOR used to run the experiments is "IMITATOR 3.4-alpha "Cheese Durian" (build feat/forall_actions/788f551"). The standalone binary for Linux (compiled on Linux Mint 64 bits) can be downloaded here.

Running case study

We describe the first case study, i.e., the running example from the paper.

Model files and results

All models can be found here.

All expected results can be found here.

We give the command for each setting to reproduce the experiments.

No parameter

> ./imitator networkKR23-noparam.imi networkKR23-synth.imiprop

1 parameter

> ./imitator networkKR23-1param.imi networkKR23-synth.imiprop

2 parameters

> ./imitator networkKR23-2param.imi networkKR23-synth.imiprop

3 parameters

> ./imitator networkKR23-3param.imi networkKR23-synth.imiprop

Scalability test

We describe the second case study, i.e., the scalability test aiming at exhibiting the limits of our approach when the possibilities of scheduling grow exponentially.

Model files and results

All models can be found here.

All expected results can be found here.

Reproducing all results

We provide a simple bash script to reproduce all results at once:

> bash runXP.sh

References

[Andre21]: Étienne André. IMITATOR 3: Synthesis of timing parameters beyond decidability. In Rustan Leino and Alexandra Silva (eds.), CAV’21, Springer LNCS 12759, pages 1-14, July 2021. DOI: 10.1007/978-3-030-81685-8_26 (English) [data | Slides]🌐

Contact

Étienne André