// constant used for time bounded until and for specifying a subset of initial states
const int k;
// a stable state is reached with probability 1
P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=1) ]
// minimum probability a stable state is reached within k steps
Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=1){"init"}{min} ]
// maximum expected time to reach a stable state
Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=1) {"init"}{max} ]
// maximum expected time to reach a stable state for a subset of initial states
Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=k}{max} ]
// minimum expected time to reach a stable state for a subset of initial states
Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=k}{min} ]