Pointing Before Shooting

To point before shooting, the states that are suitable for shooting must be established. In the example, a state is suitable for shooting if it is away from the shore. This can be represented with a property in the model program, as shown in the following code example (from file Model.cs).

public static bool AwayFromTheShore
{
    get
    {
        return 350 < x && x < 650 && 350 < y && y < 650;
    }
}

Also, a machine must be defined that can potentially reach one or more shooting states. This is usually a general machine, such as the model program sliced with a broad scenario or by binding some parameters of its actions.

In this case, our pointing machine is similar to the ShootCompleter in the previous section, but its behavior allows two possible leg durations, as shown in the following code example.

machine Point() : MovementActions
{
   bind Sail(Heading.NE, {30, 15}, 10)
   in
      construct model program
      where scope = "Sailboat.Model"
}

The following graph shows the result of exploring this Point machine.

The following code example builds the PointAndShoot machine that solves the problem under discussion and exhibits the PointShootConstruct feature provided in Spec Explorer.

machine PointAndShoot() : MovementActions 
{
    construct point shoot where Shoot = "BoundedShoot" 
    with 
    (.
        Sailboat.Model.SailboatModel.AwayFromTheShore
    .)
    for 
        Point
}

The exploration graph for this PointAndShoot machine is complex but is considerably simpler than the Shoot machine first proposed in the walkthrough above.

Spec Explorer has syntax to merge several steps into one by providing switches for the point-and-shoot construct. The following machine is an equivalent way to define the PointAndShoot machine; this approach avoids constructing the BoundedShoot machine altogether.

machine PointAndShoot2() : MovementActions 
{
    construct point shoot
    where 
        PathDepth = 2, 
        Shoot = "Shoot", 
        Completer = "ShootCompleter" 
    with 
    (.
        Sailboat.Model.SailboatModel.AwayFromTheShore
    .)
    for 
        Point
}

From these machines, test cases can be generated that bring the sailboat to a position close to the center of the lake, try a parameter combination there, and then sail the boat to the northeast shore, from which it can be rescued for the next test.

The following machine uses the TestCasesConstruct to create such test cases.

machine TestSuite() : MovementActions where TestEnabled = true
{
    construct test cases 
    where Strategy="longtests" 
    for PointAndShoot
}

The following shows some of the results of exploring this TestSuite machine. These columns represent test cases.

See Also

Reference

PointShootConstruct
TestCasesConstruct

Concepts

Point and Shoot