使用Spec Explorer对象模型：基础篇

Article
12/27/2009

一些使用者希望能够自己处理Spec Explorer产生的探索结果，而不是其自带的功能。Spec Explorer的对象模型可以用于此类处理，本篇博客将对这种用法进行一个基础介绍。

当Spec Explorer对状态空间进行探索或者生成测试代码时，探索结果将被存在一个扩展名为seexpl的文件中，这个文件实际上是一些表示探索结果的xml文件的zip包。seexpl文件的内容在Visual Studio里面会显示为状态图，以SMB2 sample（安装Spec Explorer以后sample也随之安装）为例，TestSuite这个machine的探索结果如下图所示：

除了使用Visual Studio打开seexpl文件外，用户可以用自己的程序来打开。这里需要用到Microsoft.SpecExplorer.ObjectModel这个assembly。

让我们来实现一个输出探索结果统计信息（比如覆盖的需求，action的序列等等）的小程序。首先，创建一个console应用程序并把ObjectModel加到引用中。

对象模型就包含在Microsoft.SpecExplorer.ObjectModel这个命名空间中。

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

using Microsoft.SpecExplorer.ObjectModel;

namespace TransitionSystemDemo
{
    class Program
    {
      ...

最上层表示探索结果的对象被称为transition system，这个名字来源于探索被表示为一组状态以及所有状态之间的迁移（其标签即为action）。transition system这一对象可以被一个叫做TransitionSystemLoader的类加载，代码示例如下：

 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);
    }
}

Process这个方法将稍后定义。我们首先看看怎么通过一个方法调用输出transition system的统计信息。在这里我们用到LINQ来方便的计算所有被覆盖或者假定被覆盖的需求列表。

 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);
}

transition system有三个基本的属性，可用于遍历：

States：transition system中所有状态的数组。数组中的每一个元素是一个表示状态的对象，含有诸如状态类型，状态标签等信息。
InitialStates：transition system中所有初始状态的数组。如果该transition system表示的是一组测试，则每一个测试用例都会有一个初始状态。
Transitions：transition system中所有状态迁移的数组。数组中的每一个元素是一个表示状态前一的对象，含有诸如源状态，目标状态，需求覆盖等信息。

对SMB2 sample的TestSuite探索结果运行上述程序，结果如下：

计算需求非常的容易，现在让我们来计算action的序列，这一部分会稍微复杂一些：

我们的程序需要处理任意的transition system，则可能会遇到有环的情况。我们将通过一旦发现环就立刻停止遍历来实现。
transition system是可能包含分支（同一源状态存在多个状态迁移）的，即便是已经分拆成测试用例的transition system。我们将以一种类似cord语法的形式生成序列，比方说action A到达某个状态，而该状态之后B和C都被允许，则我们生成A;(B|C)的形式。

代码如下：

 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);
}

需要说明的是：

每一个状态都有一个RepresentativeState的属性。这个属性和symbolic transition system有关，symbolic的相关内容超出了本篇博客的范畴，我们将在之后的文章中进行解释。只需要记住，当我们访问一个含有RepresentativeState的状态时，我们跳过该状态，并从RepresentativeState继续遍历。
我们记录已经访问过的状态，所以可以方便的发现环。
我们使用tr.Action.Text来输出action，这个信息和我们在Visual Studio里面显示的action标签是一样的。但是我们必须明白，一个action对象不仅仅是标签那么简单，它含有更多的信息，只是我们这里不会用到。
计算状态和状态迁移时，我们搜索了transition system多次，这种方法很低效。实际的程序中，用户可能更愿意缓存这些信息。

对SMB2 Sample的TestSuite运行上述程序，则输出如下：

在transition system中，还有好多可利用的东西我们没有在这里展示。最酷的或许就是所有有关action和action参数的信息都可以直接被转变为反射信息和LINQ表达式，这样一个用户就可以写出基于transition system的测试执行器。我们会在以后的博客中继续介绍。

本篇博客的整个示例代码如下：

 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);
        }

    }
}

使用Spec Explorer对象模型：基础篇

Additional resources