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

<p><strong>Prerequisite</strong></p> <p>The <em>conda</em> package manager for python</p> <p><strong>Setup</strong></p> <p>Navigate to <em>./Platoon</em> and execute following commands</p> <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> <p><strong>Usage</strong>:<br> <strong>Creating an Agent (platoon.py)</strong><br> First you need to create an environment</p> <pre><code class="language-java">gym.make(ENV_NAME, rendermode, numcars, startdist, startspeed, mindist, maxdist, accsteps, rendermode, seed, shield, shield_file)</code></pre> <p>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></p> <p>The weigths of the agent get saved in <em>./Platoon/weigths</em>&nbsp;<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> &nbsp;<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. &nbsp;<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). &nbsp;<br> Larger amount of cars need more training sessions in order to achieve a good performance.</p> <p><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 &nbsp;<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></p> <p>the model, memory and policy need to be set according to the agent &nbsp;<br> now the weigths of the agent can be loaded</p> <pre><code class="language-java">dqn.load_weights('weights/agent_name')</code></pre> <p>Pre-trained agents from 2 - 10 cars can be found in <em>./Platoon/weigths</em></p> <p><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></p> <p><strong>Safestragey</strong></p> <p><strong>Creating a Safe Strategy</strong></p> <ol> <li>open UPPAAL and load the <em>./safe_stragety/cruise.xml</em> file &nbsp;</li> <li>edit it however you want,</li> <li>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> <p>&nbsp;</p> </li> </ol> <p><strong>Parser Usage</strong></p> <p>In <em>safe_strategy/</em></p> <pre><code class="language-bash">python parser.py -create in_file_name out_file_name python parser.py -test file_name</code></pre> <p>&nbsp;</p> <p><strong>Using the safestrategy</strong></p> <pre><code class="language-java">gym.make(ENV_NAME, rendermode, numcars, startdist, startspeed, mindist, maxdist, accsteps, rendermode, seed, shield, shield_file)</code></pre> <p>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</p>