Login | Register
My pages Projects Community openCollabNet

How to use backtracking

Backtracking is mbt's way of handling decision making in a model. It gives the user the possibility of 'regretting' a chosen path in a model, and backtrack to a given vertex, and try again.

For example, the vertex 'A' has two possible out edges, representing the same action, but leading to two different vertices 'B' and 'C', depending on some known (or unknown) factor. 


Fig. 1 The graph is not a complete model.

If we would generate a static test sequence, we would probably in some point in time, end up in the wrong state according to the generated test sequence. So, the static approach  would not work for us in this case.

The keyword BACKTRACK

The solution for this case is to introduce the possibility of 'regretting', or backtrack your own foot steps and try again. This is done by adding the keyword BACKTRACK to the edges.


Fig. 2 The graph is not a complete model.

Let's do a dry-run:

  1. We are currently in state 'A'
  2. We ask the mbt for an edge taking us to the next state.
  3. mbt gives us the edge 'd', which will take us to vertex 'B'.
  4. As next step, mbt gives us the vertex 'B''.
  5. When our test tool tries to verify vertex 'B' it will fail, because the system under test has taken us to state 'C', which is not the state the edge delivered to us by mbt in 3. took us.
  6. So now what? We will ask mbt to backtrack, and try again.
  7. mbt now gives us the vertex 'C', and this time our test tool will succeed with the verification of that vertex. 

Example of the above run:

Line 1: $ java -jar mbt.jar dynamic -o -g foo.graphml
Line 2: A
Line 3: 0
Line 4: d BACKTRACK
Line 5: 0
Line 6: B BACKTRACK
Line 7: 1
Line 8: C BACKTRACK

Let me break down the above run. In red color, we see the input from the user during the execution (standard input):

    1. At this line, we start the execution.
    2. Here we get a vertex to verify. (Please note, that in a real execution, the first line is always an edge)
    3. We send back the integer 0, which orders mbt to give us the next edge or vertex.
    4. mbt gives us the output: 'd BACKTRACK'. This means, that backtrack is now enabled.
    5. We send back the integer 0, continue as normal.
    6. mbt gives us the output: 'B BACKTRACK'. But when our test tool tries to verify state 'B', it will fail, probably because we may very well be in state 'C', so we ask of mbt to backtrack by sending the integer 1 to mbt.
    7. Now, mbt gives us the output: 'C BACKTRACK'.

Rules concerning BACKTRACK

When to backtrack

Backtracking is only permitted where the graph says so, by using the keyword BACKTRACK.

If we try to backtrack by sending the integer 1 to mbt, and backtrack is not currently enabled, mbt will stop the execution.

Backtracking is enabled only if the keyword BACKTRACK is added to the vertex or edge.

Look at step 1 in the example above. The key word 'BACKTRACK' is not added to the vertex 'A', and thus backtracking is not enabled. If we tried to send 1, instead of 0 at line 3, the test would stop.

What mbt sends back

Backtracking from a vertex

If we backtrack from a vertex, the next line delivered to us from mbt would be a vertex (not an edge).

It can only be a vertex, that has an incoming edge, with the same label as the edge going to the vertex we're backtracking from.

Mind you, since random rules, the delivered vertex could be the same one we're backtracking from.


Fig. 3 The graph is not a complete model.

In the model above, let's say that we currently are at vertex 'B', and we want to backtrack. What happens here? What possible vertices would mbt send us back? Let's go through the options:

  • When we backtrack from 'B', mbt goes back to vertex 'A'.
  • Since we did a backtrack from a vertex 'B', the action done by the edge 'd', is irreversible, so we have to go to a state, pointed to by a vertex with the same label.
  • There are 2 edges with the same label 'd' coming from vertex 'A', and so the edge 'e' is ruled out. The 2 edges has the vertices 'B' and 'C' as destinations.
  • Random decides which of the 2 vertices are chosen.

Backtracking from an edge

If we would backtrack from an edge (see line 5, in the example above), mbt would would send us any edge coming from the source vertex of the backtracking edge.

In the model above, if our current location in the graph would be the edge 'd' (the one that goes the 'B'), and we choose to do a backtrack from here, this is what happens:

  • mbt goes back to vertex 'A'.
  • Since we did a backtrack from an edge, any out-edge coming from the 'A', is a valid choice.
  • Random will decide which of the out-edges coming from 'A' is to be chosen.