Using the exploration result object model: Basics
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);
}
}
}
Comments
Anonymous
November 25, 2009
It is awesome!Anonymous
December 01, 2009
This example is very helpful, thanks for posting it. I know that the example is not intended to cover everything, but was wondering if you can provide some insight on how the current state of the system can be inspected as we walk through an Exploration recursively. For example, after each transition, I want to print (a) the requirements covered by that transition and (b) the current state of the system after the transition. (a) is very straightforward, but I'm not sure on how to accomplish (b).Anonymous
December 08, 2009
Regards Anne's question: the model state is not directly exposed. This is by design. We believe the state of the model is an "implementation" detail of the model, and what matters, are the transitions, which are based on the vocabulary defined in the configuration. One can use different model states to define the same transition system. Having said so, you can access the state in some ways. The best one is to define a [Probe] in your model. This is a property which extracts something from your state. The evaluation result of all probes is available for each state in the transition system. There are also means to access the state as it is displayed in the state browser, but this is mainly for state visualization purposes, and there is no strong contract on that representation.Anonymous
December 29, 2009
Regarding using [Probe] in the model, Spec Explorer only seems to support static probe methods - this is not intuitive for instance-based models (though one could keep a static set of all instances of the class as a workaround). Regarding accessing the state as it is displayed in the state browser - from using the State Browser for state visualization, I can see there is not a strong contract here. But wondering if you can you provide sample code for accessing this information?Anonymous
March 26, 2015
Anne, is right the probe works only for static models (states)... Like the requirement coverage option also only works on static models.... I think the whole architecture of spec explorer needs to be revised.