Experiments for "It's Time to Play Safe: Shield Synthesis for Timed Systems"

Prerequisite The <em>conda</em> package manager for python Setup Navigate to <em>./Platoon</em> and execute following commands conda env create -n your_env_name -f conda_env.yml conda activate your_env_name pip install -r pip_req.txt Usage: Creating an Agent (platoon.py) First you need to create an environment gym.make(ENV_NAME, rendermode, numcars, startdist, startspeed, mindist, maxdist, accsteps, rendermode, seed, shield, shield_file) All of these key word arguments already have default values and can be changed if needed. <em>rendermode</em> can be set to <em>None</em>, <em>Minimal</em>, <em>Console</em>, <em>Viewer</em> or <em>Console_Viewer</em><em>.</em> The weigths of the agent get saved in <em>./Platoon/weigths</em>  and checkpoints can be found in <em>./Platoon/weigths/checkpoints</em><em>.</em> The checkpoints can be disabled by not using a <em>callback</em> for the dqnAgent.   All the agents have been trained by taking some amount of steps, saving the weights, reloading the weights and then start the training again.   The first training session should be between 60.000 and 80.000 steps. (here the <em>load_weigths</em> is not needed) After that the session can be a larger amount of steps but should not be unreasonably large (80.000 - 200.000).   Larger amount of cars need more training sessions in order to achieve a good performance. Using an Agent (test_agent.py) the gym should be initialized with the values <em>numcars</em>, <em>mindist</em>, <em>maxdist</em>, <em>accsteps</em> the agent has been trained on   <em>startspeed</em>, <em>startdis</em> can be changed, but might create situations where the agent has no way of preventing a crash <em>rendermode</em> can be set to <em>None</em>, <em>Minimal</em>, <em>Console</em>, <em>Viewer</em> or <em>Console_Viewer</em> the model, memory and policy need to be set according to the agent   now the weigths of the agent can be loaded dqn.load_weights('weights/agent_name') Pre-trained agents from 2 - 10 cars can be found in <em>./Platoon/weigths</em> Environment the environment can be found in <em>./Platoon/custom_gym/envs/custom_env_dir</em> and consists of <em>platooning_env.py</em> and <em>car.py</em> Safestragey Creating a Safe Strategy open UPPAAL and load the <em>./safe_stragety/cruise.xml</em> file  edit it however you want,use these two commands in the Verifier in order to save the strategy strategy safe = control: A[] distance &gt; 5 saveStrategy("filename.txt", safe)   Parser Usage In <em>safe_strategy/</em> python parser.py -create in_file_name out_file_name python parser.py -test file_name   Using the safestrategy gym.make(ENV_NAME, rendermode, numcars, startdist, startspeed, mindist, maxdist, accsteps, rendermode, seed, shield, shield_file) Enable the shield by setting <em>shield</em> to <em>True</em> <em>shield_file</em> should be the path to the previously created safestrategy