Taken from QVBS (January 2026).
The given benchmark (including parameter instantiation and property) has been considered in QComp 2019 and QComp 2020.
Original Prism model and property files have been adapted for compatibility and simplicity:
- Constants: All open constants are now explicitly set within model.prism (no need to set them via command line)
- Properties: The properties only refer to labels and rewards as defined in the model.prism file. No variables or constants are used in the property.
- Formulas: some PRISM formula declarations have been renamed so that their identify does not crash with a label.