dtmc

const double deliverySuccess = 0.9;

label "delivered" = s=3;

module msg_delivery
 s : [0..3] init 0;

 [] s=0 -> (s'=1);
 [] s=1 -> deliverySuccess : (s'=3) + 1-deliverySuccess: (s'=2);
 [] s=2 -> (s'=1);
 [] s=3 -> (s'=0);
endmodule