Probe Attribute
When applied to a method or property in a model program, the ProbeAttribute attribute creates a probe, which is state information that can be accessed when examining exploration results for the model. The name of the probe is set to the name of the member to which the Probe attribute is applied. The Probe attribute can be applied to static, parameterless methods and to static, parameterless properties that contain a get method.
The state browser in the Exploration Graph Viewer displays probes in a separate category, and you can create a view definition that uses a defined probe to change the displayed label of each state, or to hide or group states. For more information about using probes to modify the representation of an exploration graph, see View Definitions.
Probe values can be inserted into logging statements during test generation time. For more details, see Test Execution Switches.
Rules with the Probe attribute generate a Probe object in the transition system. These are available for post-processing as well.
Example
The following example shows a probe from the Sailboat code sample.
static int x, y;
/// <summary>
/// State description, which could be represented as a probe value.
/// </summary>
[Probe]
public static string Position()
{
return string.Format("{0},{1}", x, y);
}
Remarks
Do not use action-related constraints, such as a method of the Condition class, in a member marked with a Probe attribute. Spec Explorer may not return a value for such a member, and some states in the graph might contain an invalid probe value. Similarly, if the probe member can return null or throw an exception, some states might contain an invalid probe value.
If a Probe attribute is applied to a member that has parameters, Spec Explorer generates an error when a machine based on the model program is explored.
If a Probe attribute is applied to a member in a class that does not contain any rules, Spec Explorer does not generate the associated probe.