dtmc

formula isOnSlippery = !isOnGoal & !isOnLava & !isOnLeftCliff & !isOnRightCliff;
formula isOnRightCliff = position=7;
formula isOnLeftCliff = position=1 | position=2;
formula isOnLava = position=0;
formula isOnGoal = position=10;

label "goal" = isOnGoal;
label "lava" = isOnLava;
label "cliff" = isOnRightCliff | isOnLeftCliff;

// labels?
const double slipToRight = 0.5;

init
true
endinit

module robot_1D
 position : [0..10];

// commands?
[] isOnSlippery -> slipToRight: (position'=position+1) + 1-slipToRight: (position'=position-1);
[] isOnRightCliff -> (position'=position+1);
[] isOnLeftCliff -> (position'=position-1);
[] isOnGoal | isOnLava -> true;

endmodule