Summary: We describe the results of analyzing the performance model of a finite-source retrial queueing system with the probabilistic model checker PRISM. The system has been previously investigated with the help of the performance modeling environment MOSEL; we are able to accurately reproduce the results reported in the literature. The present paper compares PRISM and MOSEL with respect to their modeling languages and ways of specifying performance queries.