Test Generation
Spec Explorer supports three modes of testing: test code generation (TCG), dynamic traversal (DT), and on-the-fly (OTF) testing. This topic covers TCG and DT testing. The differences between the three modes are discussed in detail in the Testing topic. For more information about OTF testing, see On-The-Fly Testing.
Note that dynamic traversal is a special case of TCG, and thus all the details below apply to both testing modes. DT also enables users to provide their own custom traversal strategy. For more information about using DT and creating your own traversal strategy, see the Using Dynamic Traversal section.
Test Code Generation
Automatic test generation from a model is an important feature of Spec Explorer. Its goal is to create one or more test suites that comprehensively cover the model. When run against an implementation, these test suites can provide adequate confidence of its conformance with the behavior predicted by the model.
To generate tests for one or more machines in a project, select the machines in Exploration Manager, and then click Generate Test on the Exploration Manager toolbar. TCG and DT testing is available only for machines that are test-enabled by setting the TestEnabled switch to true (which is the default) in the configuration on which the machine is based, or by adding TestEnabled = true in the switch clause of the machine declaration. Following is an example machine declaration in Cord.
machine TestSuite() : Main where TestEnabled = true
{
construct test cases for SlicedModeProgram
}
The result of TCG is one or more C# files. If one machine is selected for TCG, after generating the tests, Spec Explorer displays the filename and location of these files on the Exploration Manager information bar. If multiple machines are selected, after test generation, Spec Explorer displays a summary of the operation.
Tests are generated in a format that can be consumed by a test framework, such as Visual Studio Test Tools (VSTT). Before running a test, add the test to a test project. Several properties of the generated code can be defined using testing switches in a Cord configuration. Generated tests do not require the model to run; they contain all necessary information to provide inputs and to evaluate the outputs of an implementation. Spec Explorer uses the model for a machine to generate a transition system for the machine, and then uses the transition system to generate the tests. However, the model is not available to the test framework, and the transition system is available only to the test framework for dynamic traversal.
Note
If the underlying model or scenario changes, regenerate the tests and update the associated test projects before running test cases.
Unit Test Formats
Spec Explorer can generate test code customized for different test frameworks. To specify the test framework to use for a machine, add the TestClassBase switch to the machine or to the configuration for the machine.
To use the VSTT unit test format, set the value of the switch to vs.
To use a different unit test format, set the value of the switch to the name of the test base-class, and add test code generation switches as necessary.
For more information about the TestClassBase switch, see Test Execution Switches. For more information about other switches that affect TCG, see Test Code Generation Switches.
Using Dynamic Traversal
TCG defines a fixed set of test strategies; DT allows for the use of custom test strategies.
To enable a machine for DT, set the GenerateDynamicTest switch to true for the machine. When DT is enabled, Spec Explorer creates dynamic tests for the machine, rather than the static tests for default TCG. Dynamic tests can also be generated using the command-line tool SpecExplorer.exe for any machine that is enabled for DT.
Spec Explorer provides a default test strategy for DT. To use a different test strategy, set the value of the DynamicTestStrategy switch to the fully qualified name of a class implementing the IDynamicTraversal interface.
For more information about dynamic traversal, see the IDynamicTraversal interface and the Microsoft.SpecExplorer.DynamicTraversal namespace.
See Also
Reference
SwitchClause
TestCasesConstruct