Using probabilities in the formal-methods-based development of safety-critical software has quickened interests in academia and industry. We address this area by our model-driven engineering method for reactive systems ...