Comprehensive Testing
In this walkthrough, the goal is to test Sail in all directions and for a couple of variations of time and speed. Exhaustively testing all combinations of eight directions, two time durations, and two speeds would result in 32 combinations. Performing pairwise combinations of the parameters reduces the combinations by half.
One way to reduce the combinations is to extend an existing configuration by providing a parameter combination configuration for one or more actions, as shown in the following example code (from file Config.cord).
config AllDirections : MovementActions
{
action static void SailboatController.Sail(Heading heading, int hours, int knots)
where
{.
Condition.In<int>(hours, 5, 10);
Condition.In<int>(knots, 20, 30);
Combination.Pairwise(heading, hours, knots);
.};
}
There is no need to provide a domain for the parameter heading, because Spec Explorer provides a domain by default for data types such as enumerations. At this point, the model might be considered ready to be explored under these combinations. This step is called shooting, as if the test were shooting in every direction, trying to hit a bug. The machine that does the shooting can be defined as shown in the following example code (from file Config.cord).
machine Shoot() : MovementActions where ForExploration = false
{
construct model program from AllDirections
where scope = "Sailboat.Model"
}
The Shoot machine has a ForExploration = false clause because exploration of this machine would lead to a potentially infinite exploration result, and because the enabling of such exploration is not normally needed. You can temporarily set this to true and perform the exploration, to observe the high complexity of the exploration result and to see that the exploration reaches the bounds on the number of steps and states. Despite this complexity, the bounds on the maximum number of steps and states should be set fairly high so that the test does not run short in subsequent modifications of the model; in the following example code (from file Config.cord), they are set to 4000. In lieu of additional constraints introduced into the model, these constraints constitute a default set of step and state bounds for the model.
config MovementActions
{
// ...
switch StepBound = 4000;
switch StateBound = 4000;
// ...
}
As seen earlier, the AllDirections configuration inherits any switch defined in its base configuration (from MovementActions in this case). The Position method must be added to the SailboatModel class to return a string representation of the current sailboat location, as shown in the following example code (from file Model.cs).
[Probe]
public static string Position()
{
return string.Format("{0},{1}", x, y);
}
The method is marked with the [Probe] attribute to enable the later display of state properties in the Spec Explorer State Browser. If you set ForExploration to true, an exploration of the Shoot machine hits the bound of 4000 steps because states where exploration is stopped are non-accepting end states, which is a situation that would lead to false positives during testing. Although testing cannot continue at this point, the implementation has correctly followed the model so far.
What is needed is a way to further limit this potentially infinite exploration result.