# Artefact for "Optimal spare management via statistical model checking: A case study in research reactors" This artefact contains the Uppaal model, analysis queries and results for the paper: *"Optimal spare management via statistical model checking: A case study in research reactors"* by Reza Soltani, Matthias Volk, Leonardo Diamonte, Milan Lopuhaä-Zwakenberg, and Mariëlle Stoelinga ## Prerequisites - [Download Uppaal](https://uppaal.org/downloads/): We use *Uppaal 5 rc-3 (pre-release)* in our evaluation. *Uppaal Stratego 4.1.20* can also be used, but takes significantly more computation time (days instead of minutes). ## Model Open the provided model file in Uppaal via `File -> Open System` and load the file `Spare_ver4.2.xml`. The tab `Editor` shows the automata for the individual components (BE, spare, warehouse, etc.) as described in Sect. 5. ## Results By selecting the tab `Verifier`, the synthesis and analysis queries from Table 3 (in Sect. 6.2) can be seen. The results from previous runs of these queries are shown and correspond to the results from Table 3. ### Reproduce results The queries can be rerun by selecting them in order and clicking the button `Check` for each of them. The first learning query `MinCost` can take several minutes, the other ones finish in seconds. We also provide queries for spare configurations from 1 to 10 spares. These queries were used to generate the plots in Figures 9 and 10. ### Configuration The configuration has already been adapted according to Table 2 and can be seen by clicking the preferences (gear symbol). The most relevants are the `learning parameters` and `statistical parameters`.