# README

This artifact is for MARS submission for paper __Safe and Near-Optimal Gate Control: A Case Study from the Danish West Coast__

- MARS_artifact
--- configs/
--- csvReaderLib/
--- WaterData/
--- WindData/
--- baseline_controller_eval_queries.q
--- BaselineController.xml
--- learned_controller_eval.q
--- learning_query.q
--- LearningController_eval.xml
--- LearningController.xml
--- README.md
--- run_high.sh
--- run_low.sh
--- run_normal.sh


The xml-files are the Uppaal models used. The q-files are the queries used in learning and evaluation. The folder csvReaderLib is the external C-library used to read the configuration files and the water level and wind speed data. The historical data is placed in WaterData and WindData. The folder configs contains the configuration files for the three sea level scenarios. The shell script are for learning strategies and evaluate both the learned controller and the baseline.


## Setting up Uppaal Stratego.
First, set up from https://uppaal.org/downloads/. Remember to apply for a license.

In the Uppaal folder, there a folder named bin with the file `verifyta`. We need the absolute path to this file for running the experiments.

## Build external library
cd csvReaderLib
mkdir build
cd build
cmake ..
make
cp libcsvReaderLib.so ../../libcsvReaderLib.so
cd ../..


## Run an experiment
./run_<normal,low,high>.sh <path-to-verifyta>

Thus, we first learn the strategy for either the normal, low, or high scenario.

Then the learned controller is evaluated.
To pass the results of the learned controller:

 - Formula 1: loads the strategy
 - Formula 2: Expected change of gate configuration.
 - Formula 3: Expected time of no migration. Take 1-<value> to match this result with the paper.
 - Formula 4: Expected max boat wait time.
 - Formula 5: Expected time out of safe range.
 - Formula 6: The expected maximum fjord level.
 - Formula 7: The expected minimum fjord level.


Then the baseline controller is evaluated.
To pass the results of the learned controller:

 - Formula 1: Expected change of gate configuration.
 - Formula 2: Expected time of no migration. Take 1-<value> to match this result with the paper.
 - Formula 3: Expected max boat wait time.
 - Formula 4: Expected time out of safe range.
 - Formula 5: The expected maximum fjord level.
 - Formula 6: The expected minimum fjord level.