// mdp model of robot moving through terrain that is divided up into a 3×2 grid dtmc module M s : [0..5] init 0; [] s=0 -> 0.2 : (s'=0) + 0.35 : (s'=1) + 0.4 : (s'=3) + 0.05 : (s'=4); [] s=1 -> 0.75 : (s'=2) + 0.25 : (s'=4); [] s=2 -> 1 : (s'=2); [] s=3 -> 1 : (s'=3); [] s=4 -> 0.3 : (s'=3) + 0.2 : (s'=4) + 0.5 : (s'=5); [] s=5 -> 0.45 : (s'=2) + 0.5 : (s'=4) + 0.05 : (s'=5); endmodule // atomic propositions labelling states label "hazard" = s=1; label "goal1" = s=5; label "goal2" = s=2|s=3; // reward structures rewards "r1" s=1 : 1; endrewards rewards "r2" [] true : 1; endrewards