Exploring a Machine

Exploring a machine constructs a state graph for it. Exploration of a given machine is requested by highlighting the machine in the list of machines in the Exploration Manager, and then clicking the Explore button in the top toolbar of the Exploration Manager. Only machines flagged ForExploration in their Cord configurations can be explored. The following image shows the exploration of the SlicedAccumulatorModelProgram machine.

Spec Explorer has explored the state space starting from the initial state S0, with the accumulator initialized to 0 (zero). The tool has determined that adding values to the accumulator leads to new states, where the accumulator has a new value. Calling ReadAndReset delivers the current counter value and then sets the accumulator back to 0. Given the constraints in the Cord configuration file for this machine, and the fact that only transitions between states are shown, the exploration performs two Add actions (from each state, the allowable Add values that increase the accumulator have values of 1 or 2) and then performs a ReadAndReset action. In the current view, states with the same accumulator value are merged; thus state S10 (with accumulator value 3) can be reached by two paths in the exploration, and ReadAndReset leads back to state S0, where the accumulator value is 0. The Cord configuration file for this machine is described in Defining a Machine. A deeper explanation of exploration can be found in section Using Spec Explorer

See Also

Concepts

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