Constructing the Test Cases

In Spec Explorer, testing of the system under test (SUT) is performed in one of three modes: Test code generation (TCG) testing, dynamic traversal (DT) testing, or on-the-fly (OTF) testing. The mode is chosen and controlled with Spec Explorer switches. The three modes differ in the way the model is evaluated and the way tests are carried out. This page discusses only the use of TCG, which is the default testing mode. For more information about TCG, DT, and OTF testing, see Testing.

The graph for machine SlicedAccumulatorModelProgram contains cycles (series of transitions that lead back to the original state) and various decision points (states with more than one outgoing edge). Constructing test cases from such a graph reduces cycles and decision points. AccumulatorTestSuite contains the Cord configuration necessary to construct TCG test cases for SlicedAccumulatorModelProgram. Following is the Cord code for this machine.

/// Builds a machine resulting from a link coverage traversal
/// of the sliced model program. It can be explored or saved as a
/// C# test suite that can be run in a VSTS unit test project
/// (by pushing the Generate Test Code button in the Exploration 
/// Manager toolbar). Most tests should fail, since the sample
/// implementation is empty.
machine AccumulatorTestSuite() : Main where ForExploration = true, TestEnabled = true
{
    construct test cases where strategy = "ShortTests" for SlicedAccumulatorModelProgram()
}

Note that, in addition to the ForExploration flag, the TestEnable flag must be set to true for the generation of test cases. The following is the result of exploring this machine.

Note

Exploring a test case machine uses actions from the model program, not the implementation. This is different from running generated test case code, which uses actions from the implementation program. Generating test cases from this machine still results in the exploration result of an abstract machine from which actual test code can be generated, in turn. For more details on the actual generating and running of the test code, see Generating and Running Test Cases.

See Also

Concepts

Using Spec Explorer for the First Time
Generating and Running Test Cases
Testing