Abstract. The present article is an essay in research reproducibility after thirty years. We retrospectively consider a challenging problem proposed in 1994 by Ulrich Herzog and Vassilis Merksiotakis. This problem was about a multiprocessor computer, the Erlangen mainframe, that processes jobs of different priorities and is subject to hardware failures. Using the stochastic process algebra TIPP, a formal model of this mainframe was specified, which makes intensive use of parallel composition, multiway synchronisation between two or more concurrent processes, and compound transitions combining synchronised actions with rates of Continuous-Time Markov Chains. From this formal model, probabilistic results about availability, performability, and proper dimensioning of the mainframe were obtained using the TIPP software tools, which are no longer maintained. We investigate whether the same experiments can be reproduced today using state-of-the-art model checkers such as CADP, PRISM, and Storm.