Slicing with Scenarios

Spec Explorer provides scenario-based slicing to select a finite slice of the full model program behavior. A scenario limits the potential control flow of the state graph of a model, while preserving the test oracle and other semantic constraints from the model program. When the slicing scenario is combined with the model program the resulting graph will be a finite subset of the model program’s full, potentially infinite behavior. For more details on scenario slicing see Scenarios and Slicing.

In the previous topic Exploring a Machine, we explored a scenario rather than the full model program behavior. Note that if we had explored the full model program behavior, we would have hit exploration bounds (defined in the Cord configuration config Main) that would have constrained the exploration, as the full model program behavior is effectively infinite.

Exploring the DoubleAddScenario by itself yields the following exploration graph.

The scenario says to perform the Add action twice, and then the ReadAndReset action. Note that the scenario uses placeholders instead of concrete parameters; it also omits the result of the call to ReadAndReset. (The two forms of Add used here, Add(_) and Add, are equivalent. These parameters can also be fixed, if desired.

The following machine configuration gives us the exploration graph described in the Exploring a Machine topic.

/// Defines a scenario for slicing.
/// When explored on its own, this machine
/// leaves all its parameters unexpanded.
machine DoubleAddScenario() : Main where ForExploration = true
{
    //Omitting the parenthesis for an action invocation 
    //is equivalent to setting all its parameters to _ (unknown).
    (Add(_); Add; ReadAndReset)*
}

When a scenario such as DoubleAddScenario is combined with another behavior using the parallel composition operator ||, the resulting behavior contains only those steps that match against both behaviors. Following is an example of this in Cord.

/// Selects the slice of the model program
/// that matches the scenario. The model program
/// supplies all parameter and state data omitted from the scenario.
machine SlicedAccumulatorModelProgram() : Main where ForExploration = true
{
    DoubleAddScenario || AccumulatorModelProgram // (synchronized) parallel composition
}

See Also

Concepts

Using Spec Explorer for the First Time
Defining a Machine
Exploring a Machine