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

Prerequisite The conda package manager for python Setup Navigate to ./Platoon 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. rendermode can be set to None, Minimal, Console, Viewer or Console_Viewer. The weigths of the agent get saved in ./Platoon/weigths and checkpoints can be found in ./Platoon/weigths/checkpoints. The checkpoints can be disabled by not using a callback 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 load_weigths 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 numcars, mindist, maxdist, accsteps the agent has been trained on startspeed, startdis can be changed, but might create situations where the agent has no way of preventing a crash rendermode can be set to None, Minimal, Console, Viewer or Console_Viewer 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 ./Platoon/weigths Environment the environment can be found in ./Platoon/custom_gym/envs/custom_env_dir and consists of platooning_env.py and car.py Safestragey Creating a Safe Strategy open UPPAAL and load the ./safe_stragety/cruise.xml file edit it however you want, use these two commands in the Verifier in order to save the strategy strategy safe = control: A[] distance > 5 saveStrategy("filename.txt", safe) Parser Usage In safe_strategy/ 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 shield to True shield_file should be the path to the previously created safestrategy