# Experiments
This folder contains all information on the experiments run which are included in my Master's thesis.

### General remark
The verification results are stored in `*.jld` files, which can be opend using the julia package `JLD`:
```
> using JLD
> result = load("[filepath]")
```
It is worth to note, that `result["args"]` contains all parameters with which the tool was called.

## Adapative Cruise Control
The KeYmaera X model of the ACC case study can be found in `acc/keymaerax`.
The model's reimport was tested with version 4.9.9 of Keymaera X.

The training procedure of the neural networks is documented in the folder `acc/training` the `PPO_ACC-NETWORK` notebooks document the conversion from torch models to ONNX models. The other notebooks document the training of the various models.
The relevant OpenAI Gym environments can be found in `acc/training/acc.py`.

The logs of all verification runs (`*.out`) and the verification results (`*.jld`) can be found in the `acc/acc-*` folders).

All plots in the `acc` folder were generated by the `Analysis` notebook.

## Zeppelin
The KeYmaera X model of the Zeppelin case study can be found in `zeppelin/keymaerax`.
The final model corresponds to `zeppelin/keymaerax/model-exact.kyx`.
The model's reimport was tested with version 4.9.9 of Keymaera X.
While the import worked without problems, rerunning the proof tactics may sometimes fail (especially for the controller proofs).
In this case, the tactic can be executed by copying the tactic from the file into the tactic textarea of a fresh proof.

All training information can be found in `zeppelin/training`.
The OpenAI Gym is located in `zeppelin/training/zeppelin_gym/env3.py`.
The torch to ONNX transformation can be found in `Transform_Network`, the `Single-Obstacle-*` notebooks describe the training procedure (`Single-Obstacle-Avoidance-WindSystem-Small2.ipynb` is more relevant to the thesis).
The reward plot was generated using `Reward-Plot.ipynb`.  

The relevant verification results are in `zeppelin/zeppelin-small2-1400000`.
My thesis describes the result of the `approx1-precise` run.

All other plots were generated using the `zeppelin/Analysis` notebook.

## Tool builds
The logs for the tool builds are in `build.log`,`build2.log` and `build3.log`.