Share via


This construct transforms a behavior as follows:

  • In the resulting behavior, there is no state with more than one outgoing controlled step.

  • Every link (or step) in the original behavior is also contained in the resulting behavior, and potentially more than once.

Syntax Definition

TestCasesConstruct ::= construct test cases
whereStrategy="ShortTests" | "LongTests"
[,AllowUndeterminedCoverage= true | false ]
[,StopAtAccepting= true | false ]
[,MinimumPathLength= Number ]
for Behavior .


For test Strategy, the "ShortTests" and "LongTests" strategies are supported. Both strategies ensure that each step is covered at least once in at least one test case in the test suite. This amounts to full path coverage in the test suite. Here are more details on these test strategies.

  • The "ShortTests" strategy generates a complete test case as soon as it finds an accepting state with a path that includes at least one transition step that has not already been tested. To do this, it performs a depth-first search of the exploration graph, starting from an initial state, adding edges in the path to the current sub-graph (called a "test case"). When an accepting end state (an accepting state with no outgoing uncovered edges) is reached, the current test case is cut and added to the output, and a new test case starts from an initial state. Observable choice nodes cause the algorithm to explore all outgoing paths in parallel until they are all cut. Each (controllable) loop is expanded to a single iteration. This strategy tends to generate more but shorter test cases.

  • The "LongTests" strategy is based on a general tour of the exploration graphs in which it tries to find the most complete (that is, longest) path from an initial state that covers as many transition steps as possible before ending with an accepting state that is as deep as possible. This strategy tends to generate fewer but longer test cases.

The "ShortTests" strategy supports two switches that offer more control over the length and number of the resulting test cases:

  • StopAtAccepting. This Boolean specifies whether to cut a test case each time an accepting state is found, not only at accepting end states.

  • MinimumPathLength. This integer specifies that the test case is cut either at an accepting end state or at an accepting state at least this distance from the initial state, whichever comes first. This means that the algorithm behaves as if StopAtAccepting were set to false until it reaches the minimum path length. Then it acts as if StopAtAccepting were set to true. Setting this switch to zero is equivalent to setting StopAtAccepting to true.

The input behavior to this construct must have a finite number of states. In case of observation choices in the behavior, the transformation does not guarantee that every link is actually reachable for each possible choice.

By default, Spec Explorer checks at exploration time that the resulting suite does not rely on undetermined coverage. That is, there should be no requirement (or step, in case the model does not contain requirements) that can only be covered in paths that rely on implementation choices. If such a case is found, exploration is aborted, and an error message is shown, listing the requirements that might not be effectively covered (or the choice points preventing effective step coverage). Setting AllowUndeterminedCoverage to true enables overriding this default behavior by enabling the exploration of nonexhaustive test suites.

The offered signature of this construct is that of its enclosed behavior.


The following Cord code shows the use of the TestCasesConstruct. This code is extracted from the static model solution generated by the Model Wizard. For the complete Cord script, see Defining a Machine.

machine AccumulatorTestSuite() : Main where ForExploration = true, TestEnabled = true
    construct test cases 
        where Strategy = "ShortTests",
              StopAtAccepting = true,
              AllowUndeterminedCoverage = true
        for SlicedAccumulatorModelProgram

Machine TestSuite is based on configuration Main and uses the TestCasesConstruct to construct machine behavior using the "ShortTests" strategy.

See Also




Cord Syntax Definition
Defining a Machine