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

<strong>Prerequisite</strong> The <em>conda</em> package manager for python <strong>Setup</strong> Navigate to <em>./Platoon</em> and execute following commands <pre><code class="language-bash">conda env create -n your_env_name -f conda_env.yml conda activate your_env_name pip install -r pip_req.txt</code></pre> <strong>Usage</strong>:<br> <strong>Creating an Agent (platoon.py)</strong><br> First you need to create an environment <pre><code class="language-java">gym.make(ENV_NAME, rendermode, numcars, startdist, startspeed, mindist, maxdist, accsteps, rendermode, seed, shield, shield_file)</code></pre> All of these key word arguments already have default values and can be changed if needed.<br> <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> <br> and checkpoints can be found in <em>./Platoon/weigths/checkpoints</em><em>.</em><br> The checkpoints can be disabled by not using a <em>callback</em> for the dqnAgent.<br> <br> All the agents have been trained by taking some amount of steps, saving the weights, reloading the weights and then start the training again. <br> The first training session should be between 60.000 and 80.000 steps. (here the <em>load_weigths</em> is not needed)<br> After that the session can be a larger amount of steps but should not be unreasonably large (80.000 - 200.000). <br> Larger amount of cars need more training sessions in order to achieve a good performance. <strong>Using an Agent (test_agent.py)</strong><br> 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 <br> <em>startspeed</em>, <em>startdis</em> can be changed, but might create situations where the agent has no way of preventing a crash<br> <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 <br> now the weigths of the agent can be loaded <pre><code class="language-java">dqn.load_weights('weights/agent_name')</code></pre> Pre-trained agents from 2 - 10 cars can be found in <em>./Platoon/weigths</em> <strong>Environment</strong><br> 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> <strong>Safestragey</strong> <strong>Creating a Safe Strategy</strong> 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 <pre><code>strategy safe = control: A[] distance &gt; 5 saveStrategy("filename.txt", safe)</code></pre> <strong>Parser Usage</strong> In <em>safe_strategy/</em> <pre><code class="language-bash">python parser.py -create in_file_name out_file_name python parser.py -test file_name</code></pre> <strong>Using the safestrategy</strong> <pre><code class="language-java">gym.make(ENV_NAME, rendermode, numcars, startdist, startspeed, mindist, maxdist, accsteps, rendermode, seed, shield, shield_file)</code></pre> Enable the shield by setting <em>shield</em> to <em>True</em><br> <em>shield_file</em> should be the path to the previously created safestrategy