option "dtmc"; int(0..6) result; property P_Correct1 = Pmax(<> (result == 1)); property P_Correct2 = Pmax(<> (result == 2)); property P_Correct3 = Pmax(<> (result == 3)); property P_Correct4 = Pmax(<> (result == 4)); property P_Correct5 = Pmax(<> (result == 5)); property P_Correct6 = Pmax(<> (result == 6)); property R_NumThrows = Xmin(S, result != 0); process ThreeDie(int offset) { palt { :0.5: palt { :0.5: ThreeDie(offset) :0.5: {= result = offset =}; Done() } :0.5: palt { :0.5: {= result = offset + 1 =}; Done() :0.5: {= result = offset + 2 =}; Done() } } } process Done() { tau; Done() } palt { :0.5: ThreeDie(1) :0.5: ThreeDie(4) }