Monty Hall Example

Monty Hall Example

The Monty Hall problem is a probability puzzle based on the American television game show. A well-known statement of the problem was published in Marilyn vos Savant's "Ask Marilyn" column in Parade magazine in 1990:

Suppose you're on a game show, and you're given the choice of three doors: Behind one door is a car; behind the others, goats. You pick a door, say No. 1, and the host, who knows what's behind the doors, opens another door, say No. 3, which has a goat. He then says to you, "Do you want to pick door No. 2?" Is it to your advantage to switch your choice?

Following is the model:

enum{Door1, Door2, Door3};
var car = -1;
var guess = -1;
var goat = -1;
var final = false;
#define goal guess == car && final;

Here we first define 3 doors; and car, guess, goat, final are variables to record the positions of car or goats. Our goal now is finally the guest will get the car.

PlaceCar = []i:{Door1,Door2,Door3}@ placecar.i{car=i} -> Skip;
Guest = pcase {
                                        1: guest.Door1{guess=Door1} -> Skip
                                        1 : guest.Door2{guess=Door2} -> Skip
                                       1 : guest.Door3{guess=Door3} -> Skip
                                   };
Goat = []i:{Door1,Door2,Door3}@
                                                              ifb (i != car && i != guess) {
                                                                                                         hostopen.i{goat = i} -> Skip
                                                                                                       };
TakeOffer = []i:{Door1,Door2,Door3}@
                                                                       ifb (i != guess && i != goat) {
                                                                                                                     changeguess{guess = i; final = true} -> Stop
                                                                                                                       };
NotTakeOffer = keepguess{final = true} -> Stop;

The whole game is divided into several parts: firstly we should put the car behind a random door; and then the guest could have his own guess; then host will show the guest a goat; finally, the guest will decide if he will take the "switch" offer from the host.

According to if the guest will take the server, we have two systems as follows.

Sys_Take_Offer = PlaceCar; Guest; Goat; TakeOffer;
Sys_Not_Take_Offer = PlaceCar; Guest; Goat; NotTakeOffer;

Finally, we have the assertion to check the probability this guest could get the car:

#assert Sys_Take_Offer reaches goal with prob;
#assert Sys_Not_Take_Offer reaches goal with prob;