Today is about my favorite probability puzzle – The Monty Hall problem. If you haven’t heard of it before you are in for a treat. The problem stated goes as follows (from Wikipedia):

*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 [but the door is not opened], 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?*

**Vos Savant's response was that the contestant should always switch to the other door.**[…]*Many readers refused to believe that switching is beneficial. After the Monty Hall problem appeared in Parade, approximately 10,000 readers, including nearly 1,000 with PhDs, wrote to the magazine claiming that vos Savant was wrong. (*

*Tierney 1991*

*) Even when given explanations, simulations, and formal mathematical proofs, many people still do not accept that switching is the best strategy.*

*The probability of the car being behind any door is uniformly 1/3

**The door that is opened has to have a goat behind it, and it cannot be the one you picked initially, in case the host has multiple choices it is assumed that s/he chooses uniformly at random

The problem is brilliant in its simplicity and the correct answer feels extremely counter-intuitive at first. The natural tendency is to think that it makes no difference whether you switch or not – but the truth is that you

*should*switch! And hopefully once you are done reading this article you will be convinced why.For an in-depth explanation (although a little too narrative in my opinion) watch this YouTube video – and if you think the answer is obvious, just scan the comments on the video to convince yourself that people have a

*hard*time understanding this answer!

**Solving the problem through modeling**

Let’s take a look at how we can tackle this problem in the world of Model-Based Testing [1]. This article is special in that

**I’m not going to have a system under test**– there is nothing to test here! Instead, what I’ll be doing is constructing a model that will be useful for simulating the flow of the Monty Hall problem.The model state machine consists of the following variables:

const int NumberOfDoors = 3;

const int DoorWithPrize = 0;

static int first_choice = -1;

static int revealed_door = -1;

static int final_choice = -1;

First, one thing I’d like to make clear is that I’m simplifying the problem by

*fixing*the door that contains the prize to be the first door – this does not make any difference, because the problem statement is equivalent no matter which door the prize is behind (likewise you could fix the initial choice and have the location of the prize be random). If you don’t believe this, then feel free to enumerate both policies for all three prize locations.To break the model down, the game show contains three stages, they are:

1) Pick your initial choice of door

2) Game host reveals a goat behind another door

3) You either switch or stick with your door

We will be modeling these stages as rules, and then define a slicing scenario that dictates the two choices of policies we have (switch/stick with choice).

The rules of the model become:

// Chooses a first choice door between 0 and 2

[Rule(Action = "PickDoor()/result")]

static int PickDoorRule()

{

first_choice = Choice.Some<int>(i => i >= 0 && i < NumberOfDoors);

return first_choice;

}

// Chooses a door to reveal between 0 and 2 that:

// * Is not our first choice

// * Is not the door with the prize (door: 0)

[Rule(Action = "RevealDoor()/result")]

static int RevealDoorRule()

{

revealed_door = Choice.Some<int>(i => i >= 0 && i < NumberOfDoors && i != first_choice && i != DoorWithPrize);

return revealed_door;

}

// Switches our choice of door and saves the value in final_choice, by picking a door between 0 and 2 that:

// * Is not our first choice

// * Is not the revealed door

[Rule(Action = "SwitchDoor()/result")]

static int SwitchDoorRule()

{

final_choice = Choice.Some<int>(i => i >= 0 && i < NumberOfDoors && i != first_choice && i != revealed_door);

return final_choice;

}

// Simply sticks with our first choice by setting final choice = first choice

[Rule(Action = "StickWithDoor()/result")]

static int StickWithDoorRule()

{

final_choice = first_choice;

return final_choice;

}

Notice that we leverage Spec Explorers ability to handle stochastic choices! The model does not know up-front which door the contestant will start out picking, and neither does it know which door the game host will reveal.

So, we could simply explore the model composing these rules, but that model would be nonsensical because it violates the rule of the game show – e.g. it would allow the game host to reveal two doors, etc. Therefore, we need to constrain the model into a meaningful slice. We have two policies so we need two slices; the first slice is for ‘sticking with your initial choice’:

/// The scenario is equivalent to sticking with your choice in the 'Let's make a deal' game show

machine DontSwitchScenario() : Main where ForExploration = true

{

(PickDoor; RevealDoor; StickWithDoor)

}

machine MontyHallDontSwitchModel() : Main where ForExploration = true

{

DontSwitchScenario || MontyHallRules

}

Let’s explore this model and have a look at the results:

The state bubbles show the currently selected door, and at the end it includes the outcome – whether we found a Ferrari or a goat behind our final choice door.

From a quick glance of this model it looks like we are in pretty good shape – we see two goats versus two Ferraris. But we need to read the picture correctly, actually we don’t decide which door is revealed, it is stochastically decided, meaning there is a 50/50 chance that either door 1 or door 2 is revealed – however, the final outcome is the same – we win no matter which door the host reveals under this policy (which is expected because our choice is unaffected by the host’s choice when we stick with the initial choice).

To compute the expected outcome for this model observe that we pick the initial door randomly with 1/3 probability, then in two out of three options the game host can only reveal one door (with probability 1), and in the final option the game host picks one of the remaining doors with probability 0.5. Getting the Ferrari has utility 1 and the goat has 0. The expected outcome is then:

E[MontyHall|Stick with choice] = 1/3 * 0 + 1/3 * 0 + 1/3 * (1/2 * 1 + 1/2 * 1) = 1/3

The fact that there are two ways of winning when we have picked door zero initially should not count double. What matters is that given our

*initial*three options, which*paths*will give what outcome? In our case the two left-most paths will result in ‘winning’ a goat, where the right-most choice (under our policy) will win us a Ferrari! Our chance of winning the Ferrari is thus 1/3.Next, let’s look at the switching policy:

/// The scenario is equivalent to switching your choice in the 'Let's make a deal' game show

machine SwitchScenario() : Main where ForExploration = true

{

(PickDoor; RevealDoor; SwitchDoor)

}

machine MontyHallSwitchModel() : Main where ForExploration = true

{

SwitchScenario || MontyHallRules

}

It is clear that the only difference is in the third stage of the model, where we now switch our choice instead of sticking with it. The model looks slightly different:

Notice now that the mechanics of the game have switched! Under the policy where we switch, two of our initial branches will lead to winning the Ferrari! Only one branch will lead us down the path where we ‘win’ a goat – again it does not matter whether the game host reveals door one or two, once we are down the path of picking door zero initially we are guaranteed to lose the game. The expected outcome is:

E[MontyHall|Switch] = 1/3 * 1 + 1/3 * 1 + 1/3 * (1/2 * 0 + 1/2 * 0) = 2/3

The key to understanding this problem (in my opinion) lies with understanding what happens when the host reveals a door under the switching policy. Notice that under this policy the game host only has one option in two out of three cases – incidentally, in these two cases, when he reveals the door with the goat behind it he is consequently also revealing which door the Ferrari is behind!

**Conclusion**

We saw in this article how models can be useful for simulating problems without actually acting against a system under test. Modeling is a great technique for visualizing simulation results and through Spec Explorers powerful stochastic modeling feature you can simulate decision-trees for random processes, like the Monty Hall problem.

**References**

[1] Monty Hall Model

Thank you, Simon, for this interesting article. I really liked your conclusion, that models are also useful besides testing.

ReplyDeleteI was a bit confused when you talked about "Spec Explorer's powerful stochastic modelling feature": Does Spec Explorer really cover probabilities (i.e. quantitative choices)? What you are using is rather non-determinism (i.e. qualitative choices), isn't it? If Spec Explorer were aware of probabilities, you wouldn't have to compute the expected values by hand, for instance. If you are interested, have a look at http://www.prismmodelchecker.org, a really suitable tool for probabilistic modelling, such as your zonk problem.

Using slicing to fix the rules of the zonk game was really concise. Do you know whether that is best practice (at Microsoft)? I would have thought you should use slicing only for .... wait for it ..... slicing the exploration, and not to determine the semantics of your system (under test). But I admit that using e.g. a GameStateEnum consisting of FirstPick, Reveal, SecondPick, and incorporating it into the rules would be far less concise.

Cheers & plz keep on posting!

David

Thanks for your comment David.

ReplyDeleteYou are of course correct on the point that Spec Explorer only models qualitative choices! In fact I believe I already touched a bit on this lack in the conclusion in a previous article:

Modeling Multi-Threaded Applications

It kind of feels like the feature is half-done, I would really like to be able to assign probabilities to my choices, and have Spec Explorer validate that my system under test is actually performing within a desired stochastic profile. One example of this use would be to assert that a load balancing application in fact balances the load uniformly among the worker processes, and that it is not biased.

Incidentally, when implementing the parallel job scheduler in the above mentioned article, I accidentally defined the C# Random class as a local variable, which meant that it would repeatedly be constructed. As the initial seed for the random generator is time dependent, it means the sequence is not random very random if you create thousands of instances within the same second. I ended up with a solution that strongly favored one outcome over another, which would have resulted in a skewed probability distribution.

Regarding slicing, I'm not actually aware of the best practice on this area. I tend to think about modeling as broad as possible, and then reduce my model through slicing. This makes it easier to go and explore additional scenarios, because I don't need to change my state machine.