Exploration

Exploration is an operation by which Spec Explorer systematically discovers all possible states defined by a model, and the steps to transition from one state to another. The unit of exploration in Spec Explorer is a machine. Machines are defined in Cord scripts and each machine is based on one or more configurations. Configurations declare the set of actions that can be used to label steps, together with switches that control the exploration process. The result of an exploration is a transition system, which can be displayed in the Exploration Graph Viewer as an exploration graph.

States and steps in an exploration graph can contain symbolic values. For more information, see Symbolic Exploration.

To explore one or more machines, select the machines in Exploration Manager, and then click Explore on the Exploration Manager toolbar. Alternately, right-click the selected machines and click Explore.

If only one machine is selected, Spec Explorer explores the machine and displays the exploration graph. If multiple machines are selected, Spec Explorer explores the selected machines and displays a summary of the exploration operation. You can open individual exploration graphs from the summary or by opening the associated file from within Visual Studio.

Spec Explorer saves the transition system for machines that have been explored. If the model has not changed, Spec Explorer uses the saved transition system; otherwise, it explores the new or updated model and generates a new transition system. To force Spec Explorer to re-explore one or more machines, select the machines and click Re-explore.

Only machines that are exploration-enabled can be explored. To enable a machine for exploration, set the ForExploration switch to true in the configuration on which the machine is based. (true is the default value for this switch.) Alternatively, add where ForExploration = true after the name of the last configuration in the machine declaration.

The following Cord script defines a machine that is exploration and test-enabled.

machine TestSuite() : Main where ForExploration = true, TestEnabled = true
{
   construct  test cases for SlicedModelProgram()
}

By default, machine exploration does not include the exploration cleanup process. To enable exploration cleanup for a machine, set the EnableExplorationCleanup switch to true in the machine header or in a configuration for the machine. For more information, see Exploration Cleanup.

See Also

Concepts

Exploration Manager
Exploration Graph Viewer
Symbolic Exploration
Exploration Cleanup
Configurations
Machines
Model Evaluation and Exploration Switches