In our paper “
Probabilistic modelling and verification using RoboChart and PRISM”, a statement “NFM-1 is needed due to the fact that DTMCs and MDPs are stochastic. Any state in a PRISM model has to have at least one outgoing transition.” is not fully explained. I am going to explain here.