Limiting Exploration
The goal in this example is to test a single call to Sail with different parameters, rather than to test a sequence of these calls, let alone many different sequences in which parameters vary in each step in all possible combinations. As we saw earlier in this walkthrough, exploring the unconstrained Shoot machine leads to a potentially infinite exploration result that causes the exploration to hit state or step bounds. So, the Shoot machine can be limited to only a single step. This step is actually two steps because each stimulus action stands for two atomic actions: a call and a return.
One way to achieve this limiting would be by adding a bound to a configuration. So far, the AllDirections configuration has been used only for the Shoot machine, making it the best candidate for carrying a BoundClause as shown in the following code example.
bound pathdepth = 2;
However, there is no guarantee that this configuration will be used only in this machine. Restricting all machines based on this configuration to only two steps is likely to be too constrained. Alternatively, a third configuration could be derived from this one and the bound added to it.
The Point and Shoot capability of Spec Explorer provides a way to do this more locally, by bounding any behavior through the use of a BoundedExplorationConstruct, as shown in the following code example (from file Config.cord).
machine BoundedShoot1() : MovementActions
{
construct bounded exploration where PathDepth = 2 for Shoot
}
With this, the machine would generate 16 different parameter combinations for the Sail action. However, this machine is still not suitable for testing because all paths end in a non-accepting state. A non-accepting state is a state where a test cannot successfully end to leave the system in a stable state. All 16 tests generated from the machine would fail because all tests assume that the sailboat starts at the origin. They have no way to confirm or deny this, because no observation actions are provided by the System Under Test.
Moreover, these test cases would not test anything. The only response defined by the system is the RunAground event. The purpose of the model is thus mainly to predict at which point in the execution this event should be raised, besides checking that the methods implementing Sail and Rescue can indeed be called in the corresponding states without raising an exception. This is another reason only states after a rescue are the ones considered accepting, in addition to the initial one, which does not affect testing, because the empty test is never generated.
The conclusion is that these test cases would fail, but also that they would not test anything.
See Also
Reference
ConstructBehavior
BoundedExplorationConstruct