Repetability for "Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction"

The repeatability package is only available on Linux. It has been tested on Fedora 32. Contents <em>binaries</em> contains the symrob, rttar and imitator binaries needed,<em>robustness</em> contains all the models for the robustness experiments,<em>parametric</em> contains all the models for the parametric experiments,<em>results</em> contains a pre-computed set of results that will be overwritten when re-running the experiments, and<em>the root</em> contains run_*.sh<em> </em>files for running the appropriate experiments and extract_*.sh files for extracting the result-tables in latex form from the raw output of the binaries. The pre-populated results were computed on AMD EPYC 7551 processors. Running experiments To run a test-set, execute ./run_X.sh binaries/Y where X is replaced by either <em>parametric</em> or <em>robust</em> and Y is a valid binary from the binary folder. E.g. to run the parametric test-series using rttar, execute the following: ./run_parametric.sh ./binaries/rttar_parametric If a slurm-enabled compute-cluster is available a concurrent execution can be conducted by first executing the following export: export EXECUTOR=sbatch After a successful execution, results can be extracted by calling ./extract_parametric.sh which outputs an entire latex document to standard out.