dtmc

module printer

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

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

endmodule