HW6 - Snakes and Ladders
Your task is to create a PRISM DTMC model of the Snakes and Ladders game
with the following board and an n-sided dice, where n is a PRISM constant, e.g.
const int n = 6, and the model is working correctly for all values n ∈ {1, 2, . . . , 8}.
http://bentobits.com/wp/wp-content/uploads/2012/03/SnakeLaddersA4.jpg
Let us simplify the rules as follows:
• There is only one player that starts at position "1" and aims to reach the
position "100".
• In each turn, he rolls the n-sided dice and moves forward the obtained
number of positions, following the numbers on the board.
• When he lands in the bottom of a ladder, he immediately moves to the
top of the ladder, i.e. the turn landing on "20" ends on "70".
• When the player lands on the head of a snake, he immediately moves back
to the snake’s tail, i.e. the turn landing on "99" ends on "69".
• To finish the game, the player has to land exactly on the last square "100".
If he rolls too high, he bounces off the last square and moves back, i.e.
rolling a five on "98" bounces back to "97", rolling a six on "97" bounces
back to "97", and rolling a five on "96" bounces back to "99" that (due to
the previous item) ends on "69".
Express formulas which you use to compute:
• Probability of finishing the game without landing on a snake’s head.
• Probability of finishing the game in at most 100 turns.
• Expected number of tosses to finish the game (see "Reachability reward"
properties).