Exploration Graph Viewer

  • Article

When you explore a single action machine from Exploration Manager, Spec Explorer opens the exploration result in a Visual Studio document window and displays an exploration graph that represents the associated transition system. When you explore one or more machines, Spec Explorer saves each exploration result in an .seexpl file. When an .seexpl file is opened on a computer on which Spec Explorer is installed, the file opens in the graph viewer.

Exploration Graph Viewer provides a number of options for displaying and interacting with an exploration graph.

The Exploration Graph

The exploration graph is a directed graph whose nodes correspond to internal states of an action machine and whose edges correspond to steps between these states. Each step is labeled with the action invocation that produces the transition.

The graph viewer contains additional information about each state. The following table describes how each type of state is represented in the graph.

Representation

State

Description

Gray fill

Initial state

A starting state of the transition system.

Orange fill

Unexplored state

A state for which Spec Explorer did not complete exploration. This could be due to state-specific information (steps per state or path bounds) or global information (total-step bounds or total-state bounds). Exploration does not have any further knowledge of the state's outgoing steps.

Red fill

Error state

A state for which Spec Explorer could not complete exploration. This could be due to an unhandled exception thrown from a rule or from a rule executing a Microsoft.Modeling.Condition.Fail statement.

Green border

Accepting state

A state that represents a legal termination point of an action machine.

Red border

Problem state

Either an error state, as described previously, or a nonaccepting end state.

Black border with white fill

Normal state

A fully explored state that is not an initial or end state.

Diamond

Non-deterministic state

A state from which the system under test can have more than one legitimate response.

Using Graph Viewer

The graph viewer's current view is determined by the selected view definition that is in effect. This selection is made on the right side of the toolbar in the Selected View drop-down list. For more details on the definitions of these selections, see View Definitions. Within the graph viewer, clicking a step reveals its content in a Step Browser window, and clicking a state selects it and reveals its content in a State Browser window. A selected state can be compared with another state by right-clicking the second state and choosing Compare with selected state on the pop-up menu. The comparison details are shown in a State Comparison window.

The Graph Viewer toolbar has the following buttons to control the view in various ways. Moving the mouse pointer over a button reveals its tooltip.

  • Zoom In
    Use this to reveal more detail by focusing on a portion of the graph centered in the current view.
  • Zoom Out
    Use this to hide detail while revealing more of the total graph.

  • Mode
    Use this drop-down menu to select one of the following modes that apply when using the mouse to interactively change the view.

    • Magnify
      Performs the Zoom In operation on the selected portion of the graph. The selection is done by using the mouse to click and stretch a selection box around a portion of the graph. Magnify is the default mode.
    • Move
      This mode allows you to click and drag items in the graph while retaining their graphical connections.
    • Pan
      This mode allows you to click and drag the content of the view window, effectively scrolling the graph shown within the window.

  • Save Graph Image
    Use this pop-up menu to save the current graph image in one of the following formats:

    • Save graph
      Saves the graph image in the .MSAGL file format.
    • Save in bitmap format
      Saves the graph image in the .JPG file format.
    • Save in vector format
      Saves the graph image in the .EMF file format.
  • Full Screen
    Maximizes the Exploration Graph Viewer window to fill most of the computer screen. Alternate clicks of this button restore the window to its original size within Visual Studio.
  • Fit to Screen
    Adjusts the presentation so that the entire exploration graph is shown within the view window.
  • Manage Views
    Displays the Spec Explorer View Definitions dialog box, for creating or modifying exploration views. For more information, see View Definitions.
  • Find States
    Shows or hides a state search pane, for locating particular states or types of states in large exploration graphs. For more information, see Searching for States.
  • Selected View
    Displays the name of the current exploration view. If you have defined custom views for this project, the Selected View drop-down list contains the names of these views. Default views for the machine being explored appear above a dashed line in the drop-down list. To mark a view as a default view, use the RecommendedViews switch in the associated Cord configuration or machine definition block. For more information about the RecommendedViews switch, see Model Evaluation and Exploration Switches.

Graph Viewer Example

The following illustration shows a simple state graph, along with the related status bar from the graph viewer.

SE_ExplorationGraphViewer1 SE_ExplorationStatusBar

Spec Explorer starts at state zero (S0) and explores until it reaches the specified bound for the configuration. In the illustration, the bound was reached at S19 and S20.

Reaching a state bound indicates that the machine is not yet ready for testing.

The graph viewer status bar, shown above for this graph, shows details of the graph view.

States n/m: Number of visible states in the current view / total number of states in the exploration.

Steps n/m: Number of visible steps (actions) in the current view / total number of steps in the exploration.

Requirements n/m: Number of requirements visible / total number of requirements in the exploration.

Bound n/m [Path Depth]: Number of bound states in the current view / total number of bound states in the exploration (maximum depth reached in the exploration).

Errors n/m: Number of visible error states in the current view / total number of errors in the exploration.

See Also

Concepts

Operating Spec Explorer
View Definitions
Browsing Steps and States
Searching for States