Share via


Point and Shoot

This section uses a running example to illustrate the basic concepts of the Spec Explorer's point-and-shoot feature.

The example models a sailboat in a square lake of 1000 by 1000 miles. It can sail in eight directions, at different speeds, and for different times. The boat starts in position (0, 0), the southwest corner of the lake. When it hits the lake shore, the boat raises the RunAground event and cannot sail anymore. The only way to keep using the boat is to rescue it with the Rescue action, which takes it back to position (0, 0). The only accepting state is the one in which the boat is docked at this position, because another test can start from there.

The goal in this example is to test all eight directions with several speeds and times, in pairwise combination. (For more information about pairwise combination, see Parameter Generation). Instead of doing such a test from the start position, the user wants to first take the sailboat to a position close to the center of the lake, away from the shores, and then test from there.

Although this example is rather abstract and does not represent a typical problem in model-based testing, it is very well suited to demonstrate the ideas behind the point-and-shoot exploration strategy. Clearly, the state space (1000 by 1000 positions) is large, and testing all desired parameter combinations after each step would quickly explode. The point-and-shoot strategy helps to master this kind of problem.

The walkthrough in this branch uses code extracted from the Sailboat stand-alone sample (see Finding the Code Samples). This walkthrough has enough code excerpts to make it self-contained for exposition purposes. See the Sailboat sample for the complete running code. You can also load that sample solution and follow the walkthrough within Spec Explorer.

In This Section

See Also

Reference

PointShootConstruct

Concepts

Parameter Generation
Finding the Code Samples

Other Resources

Modeling Toolbox