Completing to Accepting States

There is a simple way to take the model from any state to an accepting state. It would suffice to sail a long distance, more than 1000 miles, in any direction. The model would then generate a RunAground event, after which the Rescue action could be used to get to an accepting state. This could be done, for example, in a Cord scenario such as Sail, as shown in the following code example. Try a parameter combination for Sail, and then sail 2000 miles north and allow any three atomic actions.

Sail(Heading.N, 2000, 1); _; _; _

However, this is not the most useful for more complex systems. The steps needed to complete each path could be different and very hard to manually discover and describe with a pattern. Suppose, for example, that each leg sailed by the sailboat were limited to a certain length, or that the speed or direction in which the sailboat can sail were determined by another model variable, such as the wind.

If after the first leg the sailboat sails for at most 30 hours in a leg, at no more than 20 knots and only northeast, the scenario becomes more complicated.

However, a BoundedShoot machine can be defined to rely on Spec Explorer to find the best way to complete bounded paths. This is shown in the following code example (from file Config.cord).

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

machine BoundedShoot() : MovementActions
{
    construct accept completion
    where
        Completer = "ShootCompleter"
    for
        construct bounded exploration
        where
            PathDepth = 2
        for
            Shoot
}

This uses the AcceptCompletionConstruct. The BoundedShoot machine does not stop after two steps, because the accept completion construct extends each bounded path until it reaches an accepting state, if possible. The value of the Completer switch in the accept completion construct must be a string representing a machine name.

These two constructs are used so often together that Spec Explorer provides a shorter way to apply them both, using a Completer switch in the BoundedExplorationConstruct. This alternative way to define the BoundedShoot machine is shown in the following code example (from file Config.cord).

machine BoundedShoot2() : MovementActions
{
   construct bounded exploration
   where 
      PathDepth = 2, Completer = "ShootCompleter"
   for
      Shoot
}

The following illustration shows an excerpt of the exploration graph for this machine.

In this exploration, all paths end in an accepting state. However, the diamonds in the first row indicate that the sailboat is running aground immediately, because the test is shooting from the initial state when the sailboat is very close to the shore.

The sailboat should first sail away from the shore, and only then should parameter combinations be tested.

See Also

Reference

AcceptCompletionConstruct
BoundedExplorationConstruct

Concepts

Point and Shoot
Pointing Before Shooting