dtmc

module printer

	// local state, 1 - idle, 2 - printing, 3 - error, 4 - repair, 5 -done
	s : [1..5] init 1;

   [start] s=1 ->  (s'=2);
        [] s=2 -> 0.7 : (s'=5) + 0.25 : (s'=1) + 0.05 : (s'=3);
        [] s=3 -> 0.2 : (s'=3) + 0.7 : (s'=4) + 0.1 : (s'=2);
        [] s=4 -> 0.99 : (s'=2) + 0.001 : (s'=3)  + 0.009 : (s'=4);
    [done] s=5 -> (s'=1);

endmodule

module writer

       // 1 - sleeping, 2 - writting, 3 - print request, 4 - printing, 5 - reading
       w : [1..5] init 1;

        [] w=1 -> 0.8 : (w'=1) + 0.2 : (w'=2);
        [] w=2 -> 0.2 : (w'=1) + 0.65 : (w'=2) + 0.15 : (w'=3);
   [start] w=3 -> (w'=4);
    [done] w=4 -> (w'=5);
        [] w=5 -> 0.09 : (w'=1) + 0.01 : (w'=2)  + 0.9 : (w'=5);

endmodule