SwitchClause

  • Article

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

Test Execution Switches

ClassCleanupAttribute

ClassInitializeAttribute

LogProbes

OnTheFlyAllowEndingAtEventState

OnTheFlyExperimentInconclusiveException

OnTheFlyMinimumPathDepth

OnTheFlyMinimumRequirementCount

OnTheFlyReplayStrategy

OnTheFlySaveExperimentTrace

OnTheFlySaveState

OnTheFlyTestRunPath

ProceedControlTimeout

QuiescenceTimeout

ReRuns

SuppressGeneratedTestLogging

TestAssemblyAttribute

TestClassAttribute

TestClassBase

TestCleanupAttribute

TestInitializeAttribute

TestMethodAttribute

Test Code Generation Switches

DynamicTestStrategy

GenerateDynamicTest

GenerateEventHandlers

GenerateStaticTestMethods

GeneratedTestClass

GeneratedTestFile

GeneratedTestNamespace

GeneratedTestPath

TestCaseName

TestEnabled

TestFailedExceptionType

TestFailedReturnValue

TestMethodReturnType

TestPassedReturnValue

Test Run Bounds

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

Configuration

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

Other Resources

Cord Scripting Language