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.

Model Slicing with Spec Explorer

It’s been some time since I had the chance to blog on MBT. January 2^nd 2012 my second son was born, and I’ve been on three weeks of paternity leave. Since then I’ve been too busy at work to squeeze in time to play with MBT, but now I’ve finally managed.

Today I want to talk about model slicing which is one of the more advanced features of Spec Explorer. Slicing is extremely powerful, because it allows you to build your models very generically, and then create many slices of that model with differing purposes.

I’m going to show some very simple examples on how slicing works, and then I will dig up the Binary Search Tree model to illustrate how this would work in practice.

Slicing

For my example on slicing I’m going to construct a very simple model. The state is one integer variable, and I have two rules defined the following way:

        [Rule(Action = "A()")]

        static void A()

        {

            value *= -1;

        }

        [Rule(Action = "B()")]

        static void B()

        {

            value++;

        }

Rule “A” flips the sign of the value and “B” increases it by one. The state space of this model is infinite. If you explore it you get something like: