RequirementCoverageConstruct
This construct reduces a finite exploration result to the sub-graph necessary to cover a set of requirements. This construct is used to produce a graph that covers all reachable requirements in a model, as declared both in Requirement.Capture and in Requirement.AssumeCaptured statements (see details on these methods in the Requirement class).
Syntax Definition
RequirementCoverageConstruct ::= construct requirement coverage
[where [Strategy=Full | Selective ]
[**,RequirementsToCover=RequirementList ]
[,MinimumRequirementCount=**Number ]
[for Behavior ] ] .
Remarks
For Strategy, the following requirement strategies are supported. Both trim the exploration of the specified behavior and produce a new one:
If Strategy is set to Full, all requirement-covering transitions are retained. This is the default.
If Strategy is set to Selective, the requirement coverage from the original exploration is maintained. This potentially removes duplicated coverage.
If RequirementsToCover is specified, the RequirementList is a string containing a list of comma-separated requirement IDs. If it is not specified, all requirements in the behavior are covered.
If an integer is set for the Number value of MinimumRequirementCount, Spec Explorer checks that the count of distinct requirements in the original graph (after filtering it through the requirements-to-cover set, if applicable) is at least that number. Otherwise, exploration is aborted. The purpose of this switch is to prevent cases in which a certain number of requirements are thought to be covered, but they have been previously filtered out in an inner machine, for example, by a bound.
Exploration results of the input behavior must be finite; that is, exploration must end without hitting a bound for this construct to be useful. Otherwise, no systematic coverage of requirements can be achieved.
Example
The following Cord code shows the use of the RequirementCoverageConstruct. This code is extracted from the stand-alone Chat sample (see Finding the Code Samples).
machine ReqCoverage() : Actions where ForExploration = true
{
construct requirement coverage
where Strategy = "Selective"
for CombinedSlices
}