Solving ‘The Monty Hall Problem’ using Models

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.

Modeling Multi-Threaded Applications

So last time we looked a bit at stochastic modeling and I introduced the concept in Spec Explorer for modeling random actions/decisions. The example we looked at was a stochastic counter – which is just a tiny bit contrived. Actually, I can’t think of anywhere I would like to use a stochastic counter. Thus, I want to spent some time modeling a real stochastic example in this post.

A very common use of stochasticity is multi-threading/parallel processing. In a parallel system more than one thread can work on solving a problem at the same time (often running on multiple CPUs at the same time). So why does this have to lead to stochastic systems? – you may ask. The fundamental answer to this question is timing. In a parallel environment, to make full use of system resources, you poll a pool of threads for the next available worker thread. Whichever thread is available is determined by “chance”, because it is impacted by the speed of the executing CPUs, latency of external dependencies (RAM, BUS, network, disk, etc.) which we (usually) cannot control.

Consider a fictitious parallel environment with 3 worker threads:

This component is used by assigning the Job Scheduler a Job to be processed, then the scheduler will hold this job in its internal queue and await a worker thread to be available, once a thread is available it will take the incoming Job and start processing it in its own execution context (i.e. CPU, RAM, etc.). After successfully processing the Job the worker thread stores the result in an aggregated result list (which has to be thread-safe).

A very common sunshine scenario to test would be to give the Job Scheduler a single Job and check that a worker thread starts working on it and finally check the result from the aggregated result list.

Modeling Stochastic Systems in Spec Explorer

One of the more advanced – and powerful – features of Spec Explorer is its ability to handle stochastic SUTs. Stochasticity is common in systems with external dependencies, this could for example be the file system, network interface or external devices. Common for all these dependencies is that they sometimes fail for various reasons. You cannot predict when this will happen, and for the most part in Software testing we strive to avoid these spurious behaviors at all cost.

Another source of stochasticity is the use of random in the SUT (which I will explore a bit more in this post) or stochastic behavior due to race-conditions in multi-threaded applications (which I will investigate further in a later post).

First of all, what does a stochastic model look like? Take a look here:

This picture represents a model of a stochastic accumulator. It shows a slice where the accumulator is increased twice then reset. Each addition is stochastic in that it can add either 1 or 2 to the counter.

When working with stochastic models, in addition to the normal “round” states, Spec Explorer introduces diamond-shaped decision states. Each diamond represents a choice in the model where the SUT can behave in one of many ways. In the case of the stochastic accumulator we can see that the value of the accumulator can go from the initial value of 0 to either 1 or 2 in the first addition step.

Re-Modeling the Traveling Salesman – Part II

Last time we had a look at a very crude model for growing graphs for the Travelling Salesman Problem (TSP). I neglected to actually visualize what the solutions looked like, so here is a rendering of a couple:

Not very complex indeed... So what seems to be the problem here? Well, the model itself is very exhaustive, so it will generate any conceivable graph on the input domain. The single model rule is generic on the full input domain:

config Grid20x20: Main

{

    action abstract static void TravelingSalesman.InsertVertex(int x, int y)

        where x in {0..19}, y in {0..19};

}

This means that for each state Spec Explorer will try X * Y rules, so for larger input domains like 20x20, it takes forever to explore a state fully. What we are interested in with the TSP is not to construct a plethora of simple graphs, but to generate high complexity graphs (because they are much harder to solve). So what we need is a depth-first search (DFS), luckily Spec Explorer allows us to do just that using a config switch:

config Main

{

    ...

    switch DepthFirst = true;

    ...

}

Unfortunately it turns out that the DFS exploration uses an “optimized” version of DFS, causing it to always fully explore each state it visits, instead of immediately exploring from newly discovered states. Not that it’s going to show the extra states that got explored, they are simply hidden away until they get fully explored much later in the process (sorry, guys but that’s just silly). Anyway, that is exactly what we wanted to avoid, because even when using DFS exploration on a 10x10 grid it will take hours to generate graphs with 10 vertices.

Modeling the Traveling Salesman

I’m going to attack a well-known problem from the 1800 century in this post: Traveling Salesman Problem (TSP).

The objective in the traveling salesman problem is to find the shortest path through a network graph visiting every node/vertex exactly once and returning to the origin, such a path is called a tour of the graph (or a Hamiltonian cycle if you are into computer science). The problem is NP-hard to solve, meaning it is likely that no feasible exact solution exists for large graphs. There exist a lot of variant on the traveling salesman problem. I will consider the form of the problem in which the graph lies in a plane, also known as the Euclidian TSP. This puts constraints on the distances between nodes and is a symmetric formulation of the problem. But still, this is an NP-hard problem.

To put things into perspective, the number of distinct Hamiltonian cycles through a graph is:

Enumerating all possibilities becomes infeasible for even small graphs. For n = 21 the number of solutions is 1,216,451,004,088,320,000. For the case of n = 101 the number of solutions is approximately 9e+157 which exceeds the approximated number of atoms in the known universe. Of course, I’m not claiming to solve this problem – actually I’m not trying to solve it at all. Many better people have tried that before me. I’ll however focus on testing a TSP solver. It may be exceptionally difficult to solve the problem, but it is possible to construct graphs for which the solution is known (and non-trivial) without too much effort. A model for that could look like:

I plan on doing a series of posts on this problem. In this first post I will define the problem and the method in which I’m constructing a graph for the TSP. In the following posts I will investigate different models for growing TSP graphs, and look into how they perform.

Multi-Threaded Modeling – Barrier Synchronization

Okay, all my previous posts have been based on static system models, where rules and actions are static functions in classes. A lot can be accomplished with this, and it is also possible to wrap instance based applications inside static functions. However, Spec Explorer allows us to work with actual instance based models.

So what does this mean for us? Well, it means we are allowed to instantiate any number of objects of some type and Spec Explorer can reference each of these objects individually. For example, you could write a class that represents a complex number, and have Spec Explorer create two instances of this object and then add them together. This would be a basic example, but instead let’s jump to something more tricky – multi-threading!

You can imagine that instance based modeling and multi-threading are closely related. But there are some key issues one must understand first. Instance based modeling is not multi-threaded, it is exactly as sequential as any static model. Spec Explorer will not create a new thread for you when you instantiate an object. Any interaction by Spec Explorer will be from the “main”-thread, you have to handle communication with your threads.

Barrier synchronization

The example I have picked for this post is a barrier synchronization implementation. Barrier synchronization is a pattern for worker threads in multi-threaded application. With barrier synchronization each thread must wait for its co-workers to complete their cycle of work before the next cycle starts. Denoting the number of cycles completed by thread i as c_i, this can be stated by the following invariant:

          

Essentially each thread reaches a “barrier” upon completion of its work. This “barrier” is only lowered once all threads have reached it. Upon release of the “barrier” the worker threads continues their work.

Model-Based Testing in Agile Development Cycles – Part II

Last post I left you hanging after a model had emerged from our initial acceptance requirements. The model we generated looked like:

Today’s post is about what you can use this model for in agile development, and what kind of test cases it produces.

Design discussions

As I already pointed out in the previous post, models are great in discussions. Often when you explain the model to the product owner he/she will start noticing quirks. For the example model we developed, one such quirk is that the system is not allowed to reverse a payment if said payment has been involved in a financial application. Although it is a requirement in the system, it was not mentioned in the acceptance criteria because it is not a sun-shine scenario. Design discussions based on models will help you uncover these implicit requirements.

Model-Based Testing in Agile Development Cycles – Part I

Today I’m strafing away from Model-Based Integration testing as I’d like to ramble a bit about using Model-Based Testing in an Agile development cycle. For those few of you who haven’t heard about Agile, here’s my crude and narrow look at it.

Agile development

Agile development is often referred to as Scrum, however Scrum is just one Agile methodology, many more exists. In Agile development work is broken up into short sprints of roughly two weeks duration. At the beginning of a sprint you sit down with your team (size 4-7 roughly) and plan what you believe you can achieve during the next two weeks. The main idea is that when you complete a sprint you are done. In contrast, way too often in waterfall you hear the developer/tester saying I’m done (or “almost done”) and what they mean is that the code is done, but they need to run tests, validate performance, security, stress, etc. That does not fly in Agile, done means done, your code is ready for production. The idea of course, is that you do not have to go back and revisit your work at a later point in time – it is Agile because you do not drag a huge backlog of items you need to do when you enter the next sprint.

Okay, enough about Agile – there are lots of other (and better) sources out there online [1] and in books [2].

Model-Based Testing and Agile

Recently I’ve gained some experience applying Model-Based Testing in an Agile development cycle. It’s tricky business and you have to balance your time carefully. There are definitely some pros of applying Model-Based Testing in Agile, but one has to be very careful not to focus too much on modeling through the sprint - instead I suggest taking the time early on in the sprint to formalize a model, which servers as a good aid in discussions as well as a great reference tool later on.

Applying Model-Based Testing for Fault-Injection in cloud services – Part II

Okay, so I have to admit I’m mixing things up a bit here. This week I wanted to go to a 2-service model, but I realized that would be jumping ahead of things. Instead I want to take the next steps in actually implementing the shopping cart service and the model interface to this service, as this has some interesting challenges.

First the service…

Shopping cart service

The shopping cart service is a Windows Azure WCF Service Web Role project. It implements a very crude interface. You can add an item to the cart, reset it (empty it), retrieve the number of stored items and proceed to checkout (which includes emptying the cart). The interface is:

    public interface IShoppingCart

    {

        /// <summary>

        /// Empties the shopping cart

        /// </summary>

        [OperationContract]

        void Reset();

        /// <summary>

        /// Adds the item with given name to the shopping cart

        /// </summary>

        /// <param name="item">Name of item to add</param>

        [OperationContract]

        void AddItem(string item);

        /// <summary>

        /// Returns the number of items currently in the cart

        /// </summary>

        /// <returns>Number of items in cart</returns>

        [OperationContract]

        int GetCount();

        /// <summary>

        /// Continues to payment input, and empties the shopping cart

        /// </summary>

        /// <returns>False if no items are in the cart</returns>

        [OperationContract]

        bool ProceedToCheckout();

    }

The service can be started from within Visual Studio where you can debug it, or you can generate an Azure ASP.NET Web Role that consumes it.

Writing tests against a service is piece-of-cake. You simply add a service reference to the test project and create a static instance of the service client, which you can then call. The adapter layer of our model based tests will simply call the appropriate service method for each action, with the exception of the “KillService” and “RestoreService” rules that are special.

The implementation of a shopping cart service can be found in the appendix [1]. 

These actions are a bit more tricky to implement...

Application of Model Based Testing to a Binary Search Tree - Part II

Okay, today I want to wrap up on the model based testing of the binary search tree implementation I did last time. Remember how we uncovered a problem that the model did not cover all of the code? Drawing from our experience from the Application of Code Coverage to Model Based Testing post we understand that our model does not reflect closely the actual implementation, and we have a risk in terms of a test hole.

Understanding the problem

Before we jump in to adding additional tests, let’s try and understand what the problem really is. Remember I hinted that it has to do with our choice of container in the model. So let’s try to understand this some more by building some trees from the model:

Notice that even though these three trees are very different constructs, the internal set representation of the model reads (0, 1, 2) for all cases.

Application of Model Based Testing to a Binary Search Tree - Part I

I wanted to post some real modeling examples for a change, where I show how to use model based testing to explore test case combinatorics. The obvious choice is of course the more than sufficiently modeled calculator. So I decided not to choose a calculator, but something a bit different. I thought to myself, why not a simple Binary Search Tree? Hmm, but does it have any potential?

BSTs are really nice in that you can write invariants for them: 

For all nodes n in T: value(left(n)) < value(n) < value(right(n))

However, in a normal functional testing paradigm this is not entirely sufficient to validate the tree. The problem is that any given sub-tree of the BST will pass the integrity check – thus if I were to introduce a bug that removed the whole sub-tree when deleting a node from the tree, the resulting tree is still a valid BST but it’s not the expected! Normally we would need to check the node count and also that the expected values are to be found in the tree, however in a model based testing paradigm this is no longer required as we will see later on.

Finite vs. infinite state space

Okay, the first "real" post. So what is a finite state space model?
Any model that you can explore completely is by definition finite. That means you can try out every single combination in finite time (although in some cases this can be a very long time).

Opposite, an infinite model is one where the number of inputs grow infinite.

Theoretically we cannot have infinite models in a computer, because the state space will be determined by the variables in the model which all have finite ranges - but say you combine two 32bit integers, the state space explodes to 18446744073709551616 states - which is practically infinite.

In general model exploration is bound by number of states and steps, and as such we don't know if a model is infinite if it has more states than the state bound. A classic example of a (practically) infinite model would be a counter with internal state variable int x = 0, and the action Increment() { x++; }. This model will generate a state for every value x >= 0. Exploring the model gives the following result:

So basically what this means is that anytime you have numbers in your model that can take arbitraty values you have infinite state space. Bummer. Okay, but there are of course ways to work with this. Enter: Equivalence Class Partitioning - ECP is all about determining which values you consider to be different. A great example is the addition function of your calculator - say add(x,y), consider testing that: add(2,2) = 4 if this holds true, would you expect add(2,3) <> 5? Of course not, if addition works for 2 it should work for 3 as well. Thus we consider y > 0 equivalent. Likewise y < 0 should be equivalent and y = 0 is a boundary case. (really, for all practical purposes we would assume y completely equivalent).

We can apply ECP the same way to our model state variables. Instead of modeling the counter fully we could assume that x > 0 is equivalent, thus we adjust the model slightly to be Increment() { if(x < 1) x++; }. Notice that the increment action is valid from any state, but calling Increment with x = 1 does not change the internal state representation. The model is now limited to two states, x = 0 and x = 1. It is also finite under our equivalence assumption. Model exploration gives:

Closing exercise: Extend the counter model to support negative numbers using a Decrement() action and apply ECP to make the state space finite.

[1] Counter models