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


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

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

image_12[1]

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

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

image_2[1] 对象模型就包含在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探索结果运行上述程序,结果如下:

image_4[1] 计算需求非常的容易,现在让我们来计算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运行上述程序,则输出如下:
image_10[1] 在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);
}

}
}


Skip to main content