SwitchClause
Switches offer a generic way to configure various aspects of tool operation. There are predefined switches in three categories: exploration, testing, and bound switches. Switches can be additionally configured with a facility that allows substitution of the values of Spec Explorer's built-in variables as well as system environment variables.
Switch settings are part of a Cord configuration. When a configuration is based on another configuration, the switch settings are inherited by the child configuration, but can be overridden by explicitly specifying the desired settings in the child configuration.
Syntax Definition
SwitchClause ::= switch Switch .
Switch ::= Ident = ( Literal | Ident | none ) .
Remarks
The generic syntax allows using an identifier on the right-hand side of the switch, which is treated as a string literal with the identifier name as its value.
Switches omitted from a configuration inherit the value defined in a parent configuration. If there is no ancestor configuration defining a value, the Spec Explorer default value is used. Switch values can be explicitly overridden at any level and carried down accordingly.
If a switch's value is a string literal, the value of that literal is case-insensitive.
Example 1: Variable Substitution
The following is an example of a Cord switch with an embedded environment variable for substitution. This example also shows the use of the escape sequence to insert double quote characters as part of the switch value.
switch TestMethodAttribute = "Owner(\"%username%\")"
Spec Explorer also keeps local "execution" variables that can be used for substitution. The following example shows such variables.
config Main
{
action abstract static void Adapter.OpenBrowser();
action abstract static void Adapter.Visit(string url);
action abstract static void Adapter.CloseBrowser();
switch StepBound = 128;
switch PathDepthBound = 128;
switch TestClassBase = "vs";
switch TestCaseName = "Browser$MachineName$";
switch TestMethodAttribute = "TestMethod, Priority($EndStateProbe(TestPriority)$), TestProperty(\"id\", \"$TestCaseHashCode$\")";
}
machine ModelProgram() : Main where TestEnabled = false
{
construct model program
}
machine TestSuite() : Main
{
construct test cases where strategy = "ShortTests" for ModelProgram()
}
Here, the indicated variables are substituted during test code generation, leading to the following when test code is generated from the TestSuite machine:
#region Test Starting in S0
[TestMethod, Priority(1), TestProperty("id", "0x01c80c2a162890be53bf5de7e873511161")]
public virtual void BrowserTestSuite() {
this.Manager.BeginTest("BrowserTestSuite");
this.Manager.Comment("reaching state \'S0\'");
this.Manager.Comment("executing step \'call OpenBrowser()\'");
Adapter.OpenBrowser();
this.Manager.Comment("reaching state \'S1\'");
this.Manager.Comment("checking step \'return OpenBrowser\'");
this.Manager.Comment("reaching state \'S10\'");
this.Manager.Comment("executing step \'call Visit(\"msdn.com\")\'");
Adapter.Visit("msdn.com");
this.Manager.Comment("reaching state \'S15\'");
this.Manager.Comment("checking step \'return Visit\'");
this.Manager.Comment("reaching state \'S20\'");
this.Manager.Comment("executing step \'call Visit(\"msdn.com\")\'");
Adapter.Visit("msdn.com");
this.Manager.Comment("reaching state \'S25\'");
this.Manager.Comment("checking step \'return Visit\'");
this.Manager.Comment("reaching state \'S28\'");
this.Manager.EndTest();
}
#endregion
Example 2: Switch Inheritance
The following example shows inheritance of switch values (coded in Spec Explorer's Cord modeling language).
config Base
{
// Other configuration clauses
switch StateBound=50;
}
config Child : Base
{
// Other configuration clauses
switch StopAtError=true;
}
In this example, configuration Base has the actual switch values StateBound=50, as stated explicitly, and StopAtError=false, implicitly set by system default. Configuration Child has StateBound=50 implicitly inherited from its parent configuration and StopAtError=true explicitly specified.
Complete Switch List
The following tables cover all available switches. Each set of switches is preceded by a link to the page defining the switches.
Model Evaluation and Exploration Switches
ConstraintSolverTimeout |
DefaultParameterExpansion |
DefaultParameterExpansionLimit |
DepthFirst |
Description |
EnableExplorationCleanup |
ExplorationTimeout |
ForExploration |
Group |
KeepOutputParametersUnexpanded |
OnTheFlyRandomAccept |
RandomSeed |
RecommendedViews |
StackDepth |
StopAtError |
Model Evaluation and Exploration Bounds Switches
ExplorationErrorBound |
PathDepthBound |
StateBound |
StepBound |
StepsPerStateBound |
ClassCleanupAttribute |
ClassInitializeAttribute |
LogProbes |
OnTheFlyAllowEndingAtEventState |
OnTheFlyExperimentInconclusiveException |
OnTheFlyMinimumPathDepth |
OnTheFlyMinimumRequirementCount |
OnTheFlyReplayStrategy |
OnTheFlySaveExperimentTrace |
OnTheFlySaveState |
OnTheFlyTestRunPath |
ProceedControlTimeout |
QuiescenceTimeout |
ReRuns |
SuppressGeneratedTestLogging |
TestAssemblyAttribute |
TestClassAttribute |
TestClassBase |
TestCleanupAttribute |
TestInitializeAttribute |
TestMethodAttribute |
DynamicTestStrategy |
GenerateDynamicTest |
GenerateEventHandlers |
GenerateStaticTestMethods |
GeneratedTestClass |
GeneratedTestFile |
GeneratedTestNamespace |
GeneratedTestPath |
TestCaseName |
TestEnabled |
TestFailedExceptionType |
TestFailedReturnValue |
TestMethodReturnType |
TestPassedReturnValue |
OnTheFlyGracePeriod |
OnTheFlyMaximumExperimentCount |
OnTheFlyTimeOut |
Variable Substitution
Switches can be additionally configured using substitution of variable values from Spec Explorer’s built-in variables and from system environment variables. These variable substitutions are specified by bracketing the variable name with $ or % symbols. The $ bracketing is used for value substitution of Spec Explorer built-in variables; the % bracketing is used for value substitution of system environment variables. These variable substitutions cannot be nested. Multiple variable substitutions can be specified, but only for Test switches. Substitution in a switch is no guarantee that the resulting value is valid in the domain where the substitution is ultimately applied.
Using Built-in Variables
Built-in variable names must be bracketed by $ characters. For example: $MachineName$. All built-in variables are treated as type string and their substitution can only be used in Test switches. If there is no built-in variable by the specified name then the substitution value will be an empty string. The following built-in variables are recognized.
| Variable Name | Description |
|---|---|
$MachineName$ |
The machine name from which the test is generated. |
$TestCoveredRequirementSet$ |
Requirement set covered by the test case. |
$TestCoveredRequirementSequence$ |
Requirement sequence covered by the test case. |
$TestCaseHashCode$ |
The hash code of the test case. |
$EndStateProbe(<probename>)$ |
Where <probename> stands for the name of a probe. The probe value substituted is from the end state of a test case. If there is no end state (that is, in the case of an end loop) an arbitrary state of the end loop will be used. |
Using Environment Variables
System environment variable names must be bracketed by % characters. For example: %username%. Environment variable substitution can be used in all Spec Explorer switches. If there is no system environment variable by the specified name then SE will report an error.
See Also
Reference
Concepts
Cord Syntax Definition
Model Evaluation and Exploration Switches
Test Execution Switches
Test Code Generation Switches
Model Evaluation and Exploration Bounds Switches
Test Run Bounds