Model Evaluation and Exploration Switches
Model evaluation and exploration (E&E) switches are used to control the way that Spec Explorer evaluates and explores machines.
Switches
Some E&E switches are available only for the Exploration Viewer. Others have different or no effects on model evaluation during testing. The following table details all the E&E switches. The TCG column indicates whether the switch applies to test code generation (TCG). The OTF column indicates whether the switch applies to on-the-fly (OTF) testing.
| Switch | Possible Values (Default Value Bold) | Description | TCG | OTF |
|---|---|---|---|---|
ConstraintSolverTimeout |
30000, number |
Timeout (in milliseconds) controlling how long the underlying constraint solver will try to satisfy a set of constraints before producing an error state. Consider increasing this value if an exploration result has error states with the following description: "Constraint solver exceeded configured timeout …". |
X |
X |
DefaultParameterExpansion |
Coverage, None, Product, Pairwise |
Specifies the default way to combine values when expanding action parameter domains. Coverage computes the set of parameters required to cover model code and to meet interaction goals. None (which must be specified as a keyword) keeps parameters symbolic. Product computes the Cartesian product of all parameters, and generates one step per possible combination of values from all parameter domains. Specifying Pairwise creates fewer steps by guaranteeing only each pair of values (for two parameters) to appear at least once. |
X |
X |
DefaultParameterExpansionLimit |
10240, number |
Specifies the default parameter expansion limit value. It indicates the maximal solution set that will be generated. |
X |
X |
DepthFirst |
true, false |
Specifies whether exploration is depth-first. If this value is set to false, it is breadth-first. |
X |
|
Description |
"", string |
Specifies the description that Exploration Manager displays for the machine. |
X |
X |
EnableExplorationCleanup |
true, false |
Specifies whether Spec Explorer will conduct exploration cleanup after the exploration procedure. true to perform exploration cleanup as part of exploration; otherwise, false. |
X |
X |
ExplorationTimeout |
none, number |
Specifies the timeout period (in milliseconds) after which Spec Explorer will terminate the exploration procedure. If the user clicks Stop or the combined exploration and cleanup procedures exceed the timeout period, then Spec Explorer displays an intermediate graph. The value none (which must be specified as a keyword) specifies that Spec Explorer should not use a timeout period. |
X |
X |
ForExploration |
true, false |
Determines whether the machine can be directly explored. Only machines with this switch set to true can be explored from Exploration Manager or SpecExplorer.exe. |
X |
|
Group |
"", string |
Specifies the group associated with a machine. Has no effect when exploration is done with SpecExplorer.exe. Affects only the Exploration Viewer. |
||
KeepOutputParametersUnexpanded |
true, false |
Specifies whether all values in event/return/out parameters should be kept symbolic. |
X |
X |
OnTheFlyRandomAccept |
50, number |
Specifies the percent probability that OTF testing will stop an experiment when a non-terminal accepting state is reached. Value must be between 0 and 100. |
X |
|
RandomSeed |
0, -1, non-negative number |
Defines a random seed for parameter generation. -1 indicates that a time-based random seed will be used. |
X |
X |
RecommendedViews |
"", string |
A comma-separated list of view identifiers to represent recommended views of machines based on this configuration. The first recommended view is used as a default. Affects only the Exploration Viewer. |
||
StackDepth |
512, number |
Depth of the exploration call stack. If the number of pending nested calls is greater than this number, exploration will stop. Consider adjusting the stack depth for recursive models. |
X |
X |
StopAtError |
true, false |
Specifies whether exploration should stop at the first error encountered. |
X |