Exploration Manager

  • Article

Exploration Manager provides support for validating and exploring models, and performing tests. To display the Exploration Manager window, on the Spec Explorer menu, click Exploration Manager. By default, the window appears in the right pane in Visual Studio.

The Exploration Manager window contains a list of all machines defined in Cord scripts that are marked as exploration-enabled in the open solution. Machines are marked as exploration-enabled by setting the ForExploration switch to true in the configuration on which the machine is based, or by writing where ForExploration = true after the name of the last configuration in the machine declaration. The default value of the ForExploration switch is true. Most operations performed from the Exploration Manager affect the machines selected in this list. Double-click a machine entry, or right-click the entry and click Go To Machine Definition, to open the definition of the machine in a Cord script.

Exploration Manager Toolbar Controls

The following operations are available on the Exploration Manager toolbar.

  • Validation
    Validation checks for consistency all of the Cord scripts and the model code they reference. If needed, the model code is compiled before the check. Exploration, test generation, and on-the-fly (OTF) testing include validation. To validate your model without exploring a machine, click Validate script(s).

    For more information about validation, see Validation.

  • Exploration
    Explore expands the behavior of the selected machines. If only one machine is selected, Spec Explorer explores the machine and displays the transition system as an exploration graph. If multiple machines are selected, Spec Explorer explores the selected machines and displays a summary of the exploration operation. You can open an individual transition system from the summary or by opening the associated file from within Visual Studio. The configuration or configurations on which a machine is based define switches that can control how Spec Explorer performs exploration.

    Spec Explorer saves the transition system of each machine it has 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 a machine, select the machine and click Re-explore.

    For more information about exploration, see Exploration. For information about working with the exploration graph, see Exploration Graph Viewer.

  • On-The-Fly Testing
    Run On-The-Fly Test performs on-the-fly (OTF) tests (also called experiments) against one selected machine. Spec Explorer can run OTF tests on a machine that is not marked as test-enabled.

    For more information about OTF testing, see On-The-Fly Testing.

  • Test Generation
    Generate Test Code explores the selected machines and generates stand-alone test cases for each one. If only one machine is selected, Spec Explorer generates test code from the transition system of the machine. If multiple machines are selected, Spec Explorer generates test code for each machine selected, and displays a summary of the operation.

    Not every machine is suitable for test generation. Spec Explorer currently limits the generation of tests to machines that are in test normal form. The user can mark a machine as being suitable for test generation by setting the TestEnabled switch to true (which is the default) in the configuration on which the machine is based, or by writing where TestEnabled = true after the name of the last configuration in the machine declaration.

    If Spec Explorer has saved a transition system for a machine, and the model has not changed, then Spec Explorer uses the saved transition system when generating tests for that machine.

    For more information about test generation, see Test Generation.

  • Stop
    Stop stops the current activity, whether exploration (including exploration cleanup), execution of OTF tests, test generation, or post-processing.
  • Filtering
    To filter the machine list, select the column to which to apply the filter from the Filter Column drop-down list, and enter the filter text in the Filter Text text box. Spec Explorer restricts the machine list dynamically as you enter text. To clear the filter text and restore all machines to the list, click Clear Filter.
  • Refresh
    Refresh checks for changes to the configuration files and refreshes the machine list.

Post-Processing

When you add customized post-processing to Spec Explorer, Spec Explorer enables the post-processing option on the Perform User Task submenu on the context menu for the selected machines. For more information about customized post-processing, see Customized Post-Processing.

See Also

Reference

SwitchClause

Concepts

Operating Spec Explorer
Spec Explorer Overview
Configurations
Machines
Working with Machines
View Definitions