# Experimental Evaluation This folder contains the results of the evaluation of both `Bosy` (using its QBF encoding and RAReQS as the underlying solver) and our prototypical solver on several arbiter benchmarks, as described in the accompanying paper. More precisely, this folder contains three files: - `ltl-synth.csv` - `pltl-search.csv` - `pltl-points.csv` # `ltl-synth.csv` This file contains the results of calling `Bosy` on the specifications of arbiters for up to ten resources. The timeout was set to 60,000 seconds, i.e., 100 minutes. - `r`: The number of resources the arbiter can manage - `realizable`: 'True', if the specification could be realized, empty if it could not, i.e., `Bosy` encountered a time out - `time`: The time in seconds until `Bosy` terminated. Empty, if `Bosy` encountered a time out # `pltl-search.csv` This file contains the results of letting our implementation search for a strategy that implements an arbiter with `r` resources, `r_p` of which are prioritized. The timeout was set to 60,000 seconds, i.e., 100 minutes. - `r`: The number of resources the arbiter can manage - `r_p`: The number of resources the arbiter prioritizes - `realizable`: 'True', if the specification could be realized, empty if it could not, i.e., our tool encountered a time out - `time`: The time in seconds until our tool terminated. Empty, if it encountered a time out # `pltl-points.csv` This file contains the results of letting our implementation search for a strategy with `n` states that implements an arbiter with `r` resources, `r_p` of which are prioritized, with respect to the time bound at most `2k`. The timeout was set to 12,000 seconds, i.e., 20 minutes. - `r`: The number of resources the arbiter can manage - `r_p`: The number of resources the arbiter prioritizes - `n`: The size of the strategy to be synthesized - `k`: The bound on the alternating color technique - `realizable`: 'True', if the specification could be realized, empty if it could not, i.e., our tool encountered a time out - `time`: The time in seconds until our tool terminated. Empty, if it encountered a time out