Our goal is to evaluate how the applicability of our translation in practical cases is influenced by the lack of support for some of the DSL constructs and the constraints added to ensure that our mission specification is within the PRISM specification language.

Dataset

We considered the benchmark of 20 mission requirements from RQ1 that were expressible in our DSL. This dataset contains 14 patterns out of the 22 mission specification patterns of our catalog.

rq1-coverage.csv: “Year”, “Link”, “Conference”, “Title”, “Mission”, “Patterns”.

Methodology

We considered each of the 20 mission requirements of our dataset. We applied our translation by running the automated support provided by QUARTET. We recorded whether the translation was applicable or not. When the translation was applicable, we stored the mission specification generated by QUARTET.