Using the exploration result object model: Basics - Spec Explorer Team Blog - Site Home

Several advanced users have expressed interest to process the test suite generated by Spec Explorer in a different way from the built-in test code generation. The Spec Explorer object model allows to do that. This article provides an introduction to its basic usage.

Whenever Spec Explorer performs an exploration – including a machine which generates test cases – the result is stored in a file ending in ‘.seexpl’. This file is in fact a zipped archive of several XML files representing the result of exploration. The content of this file is displayed under Visual Studio in the well-known graphical form, as shown below – from the far -- for the TestSuite machine of the SMB2 project which comes as a sample with Spec Explorer:

In addition to displaying this file in Visual Studio, it can be also processed with a user program – which we are going to demonstrate in this article.

To this end, the assembly Microsoft.SpecExplorer.ObjectModel contains all you need. Let’s use this to develop a little program which prints some statistics about exploration, the captured requirements, and the action sequences. To replay what we do, create a console application under Visual Studio and add the reference to the above assembly:

The object model is contained in the namespace Microsoft.SpecExplorer.ObjectModel:

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using Microsoft.SpecExplorer.ObjectModel;

namespace TransitionSystemDemo
{
    class Program
    {
      ...

The top-level object representing an exploration result is called a transition system. This stems from the fact that it actually represents the exploration as a set of states, and transitions between those states labeled with actions. The transition system is loaded by a class called TransitionSystemLoader. Our main method can therefore look as below:

static void Main(string[] args)
{
    if (args.Length != 1)
    {
        Console.WriteLine("usage: transitionsystemdemo <pathtoseexpl>");
        Environment.Exit(1);
    }
    try
    {
        var loader = new ExplorationResultLoader(args[0]);
        TransitionSystem tsys = loader.LoadTransitionSystem();
        Process(tsys);
    }
    catch (Exception e)
    {
        Console.WriteLine("failed: " + e.Message);
        Environment.Exit(2);
    }
}

The method Process will be defined later. Let us first examine how to print statistics about the transition system, a method which is called from within Process. We use a bit of LINQish magic to compute the ordered list of all requirements captured or assumed to be captured by the transition system:

static void PrintStatistics(TransitionSystem tsys)
{
    Console.WriteLine("{0} states ({1} initial), {2} steps",
        tsys.States.Length, tsys.InitialStates.Length, tsys.Transitions.Length);
    var captured =
        tsys.Transitions.Aggregate(
                new string[0] as IEnumerable<string>,
                (cs, tr) => cs.Concat(tr.CapturedRequirements).Concat(tr.AssumeCapturedRequirements))
                .Distinct()
                .OrderBy(x => x);
    Console.WriteLine("captured: ");
    foreach (var req in captured)
        Console.WriteLine("  " + req);
}

The transition system contains three central properties which build the hooks for traversing it:

The property tsys.States (of type State[]) is the array of all states in the transition system. Every entry in this array is an object containing information such as the state label, state kind, etc.
The property tsys.InitialStates (of type string[]) contains the array of state labels constituting the initial states of the transition system. If the transition system represents a test suite, these are typically the start states of each test case.
The property tsys.Transitions (of type Transition[]) is the array of all transitions. Every entry in this array is an object containing information such as the source and target state labels, the captured requirements, and the requirements which are assumed to be captured by the adapter

Running this part of the program on the exploration result file of the TestSuite machine in the SMB2 project results in output as below:

This part was easy. The more tricky part is to compute sequences (which would correspond to test cases) from the transition system. The challenges are:

We want to be able to run our program on arbitrary transition systems, and those may contain cycles. We will deal with this by just stopping once we have walked through a cycle.
The transition system – even in the case of a test suite – may contain branches (more than one outgoing transition from a given state). We will deal with this by actually generating our sequences similar to patterns in a Cord machine. So if we have an action A which leads to a state where both B and C are possible, we will generate A;(B|C).

The code resulting from this design is below:

static void PrintPatterns(TransitionSystem tsys)
{
    foreach (var stateLabel in tsys.InitialStates)
    {
        Console.WriteLine("Starting in state {0}:", stateLabel);
        Console.WriteLine(ToPattern(tsys, new HashSet<State>(), GetState(tsys, stateLabel)));
    }
}

static string ToPattern(TransitionSystem tsys, HashSet<State> visiting, State state)
{
    if (state.RepresentativeState != null)
        // skip intermediate state
      return ToPattern(tsys, visiting, GetState(tsys, state.RepresentativeState));
    if (visiting.Contains(state))
        // Stop at cycle
        return "";
    visiting.Add(state);
    // compute successor
    var successors = GetSuccessors(tsys, state).Select(tr => ToPattern(tsys, visiting, tr)).ToArray();
    visiting.Remove(state);
    if (successors.Length == 0)
        // end state
        return "";
    else if (successors.Length == 1)
        return successors[0];
    else
        return "(" + string.Join("|\r\n", successors) + ")";
}

static string ToPattern(TransitionSystem tsys, HashSet<State> visiting, Transition tr)
{
    var continuation = ToPattern(tsys, visiting, GetState(tsys, tr.Target));
    if (continuation != "")
        return tr.Action.Text + ";\r\n" + continuation;
    else
        return tr.Action.Text;
}

static State GetState(TransitionSystem tsys, string stateLabel)
{
    return tsys.States.First(state => state.Label == stateLabel);
}

static IEnumerable<Transition> GetSuccessors(TransitionSystem tsys, State state)
{
    return tsys.Transitions.Where(tr => tr.Source == state.Label);
}

Notes on this code:

Every state has a property RepresentativeState. The reason for that is related to the representation of symbolic transition systems, which goes beyond the scope of this article. In this context, whenever we visit a state which has a representative, we should just skip this state and continue with the representative instead.
We pass a set of the states which we are currently visiting through the algorithm. This allows us to detect cycles.
In order to print the action, we use tr.Action.Text. This is the same as shown in the labels of the graphical representation in Visual Studio. However, we should note that the action object has much more detailed information than just the action label text, which we don’t use here.
In order to compute the State object associated with a state label, and the successor transitions of a state, we search the arrays in the transition system again and again. This is indeed way too inefficient, and in a real application, we would like to cache this information.

We will illustrate the result again using the example of the TestSuite exploration result from the SMB2 project. The result for one of the proper sequence cases looks as below:

This concludes this little demo. There are a number of features of the transition system which you can exploit which we haven’t shown. Among the coolest is probably is that all information about actions and action parameters can be converted on-the-fly into reflection information and LINQ expressions, allowing one to write a test executor directly based on the transition system. I may come back with an example for this in a later post.

You can find the full text of the demo program in the window below:

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using Microsoft.SpecExplorer.ObjectModel;

namespace TransitionSystemDemo
{
    class Program
    {
        static void Main(string[] args)
        {
            if (args.Length != 1)
            {
                Console.WriteLine("usage: transitionsystemdemo <pathtoseexpl>");
                Environment.Exit(1);
            }
            try
            {
                var loader = new ExplorationResultLoader(args[0]);
                TransitionSystem tsys = loader.LoadTransitionSystem();
                Process(tsys);
            }
            catch (Exception e)
            {
                Console.WriteLine("failed: " + e.Message);
                Environment.Exit(2);
            }
        }

        static void Process(TransitionSystem tsys)
        {
            PrintStatistics(tsys);
            PrintPatterns(tsys);          
        }

        static void PrintStatistics(TransitionSystem tsys)
        {
            Console.WriteLine("{0} states ({1} initial), {2} steps",
                tsys.States.Length, tsys.InitialStates.Length, tsys.Transitions.Length);
            var captured =
                tsys.Transitions.Aggregate(
                        new string[0] as IEnumerable<string>,
                        (cs, tr) => cs.Concat(tr.CapturedRequirements).Concat(tr.AssumeCapturedRequirements))
                        .Distinct()
                        .OrderBy(x => x);
            Console.WriteLine("captured: ");
            foreach (var req in captured)
                Console.WriteLine("  " + req);
        }

        static void PrintPatterns(TransitionSystem tsys)
        {
            foreach (var stateLabel in tsys.InitialStates)
            {
                Console.WriteLine("Starting in state {0}:", stateLabel);
                Console.WriteLine(ToPattern(tsys, new HashSet<State>(), GetState(tsys, stateLabel)));
            }
        }

        static string ToPattern(TransitionSystem tsys, HashSet<State> visiting, State state)
        {
            if (state.RepresentativeState != null)
                // skip intermediate state
              return ToPattern(tsys, visiting, GetState(tsys, state.RepresentativeState));
            if (visiting.Contains(state))
                // Stop at cycle
                return "";
            visiting.Add(state);
            // compute successor
            var successors = GetSuccessors(tsys, state).Select(tr => ToPattern(tsys, visiting, tr)).ToArray();
            visiting.Remove(state);
            if (successors.Length == 0)
                // end state
                return "";
            else if (successors.Length == 1)
                return successors[0];
            else
                return "(" + string.Join("|\r\n", successors) + ")";
        }

        static string ToPattern(TransitionSystem tsys, HashSet<State> visiting, Transition tr)
        {
            var continuation = ToPattern(tsys, visiting, GetState(tsys, tr.Target));
            if (continuation != "")
                return tr.Action.Text + ";\r\n" + continuation;
            else
                return tr.Action.Text;
        }

        static State GetState(TransitionSystem tsys, string stateLabel)
        {
            return tsys.States.First(state => state.Label == stateLabel);
        }

        static IEnumerable<Transition> GetSuccessors(TransitionSystem tsys, State state)
        {
            return tsys.Transitions.Where(tr => tr.Source == state.Label);
        }

    }
}