Generating and Running Test Cases
This page discusses only the use of test code generation (TCG). For more information about testing modes in Spec Explorer, see Testing.
To generate test code for AccumulatorTestSuite, select the machine and click Generate Test Code on the Exploration Manager toolbar. Spec Explorer explores the machine and generates test code. Spec Explorer stores the test code to a configured file name and location.
The test code represents the same information as the graph, but in C#, where every test case is represented by an executable unit test. Spec Explorer supports both a unit test format and a customizable format. This can be controlled by the TestClassBase switch (defined in file Config.cord), which can have one of the following values:
vs: standard Visual Testing Tools unit test format.
MyClassName: User-defined name of test base class. By providing other switches for attributes identifying test class elements, you can target other test frameworks such as NUnit.
Once the tests have been generated, you can run the tests by selecting Test -> Run -> All Tests in Solution from the main Visual Studio menu. The screenshot below shows the status of the tool after executing the test suite with the shortTests flag set. Note that the implementation (contained in file implementation.cs) is not correct with respect to the model program because it has been hardwired for purposes of illustration to always return the value 4 regardless of input. Thus, three of the test cases fail. It is the implementation that is failing and not the model.
.gif "Test Case Run for the Static Model Solution")