Defining a Machine

The Cord configuration file specifies how to turn the model program discussed earlier into a Cord machine, which makes it available for exploration.

Note that the model program has an effectively infinite state space, as it is always possible to add some number to the current accumulator variable to create a value we have not seen before. Limiting this state space to make exploration tractable and meaningful is an important part of Spec Explorer.

The machines that are defined for the model are contained in file Config.cord as follows.

// This is a Spec Explorer coordination script (Cord version 1.0).
// Here is where you define configurations and machines describing the
// exploration to be performed.

using SpecExplorer1.Sample; 

/// Contains actions of the model, bounds, and switches.
config Main 
{
    /// The two implementation actions that will be modeled and tested
    action abstract static void Accumulator.Add(int x);
    action abstract static int Accumulator.ReadAndReset();

    switch StepBound = 128;
    switch PathDepthBound = 128;
    switch TestClassBase = "vs";
    switch GeneratedTestPath = "..\\SpecExplorer1.TestSuite";
    switch GeneratedTestNamespace = "SpecExplorer1.TestSuite";
    switch TestEnabled = false;
    switch ForExploration = false;
}

/// This configuration provides a domain for 
/// parameter in the previous one. 
config ParameterCombination: Main 
{
    action abstract static void Accumulator.Add(int x)
        where x in {0..2};    
}

/// Constructs a machine from the model program. 
/// Since the model is not finite, this machine explodes
/// and exploration is stopped by a bound.
/// Switch ForExploration makes the machine appear in Exploration Manager.
machine AccumulatorModelProgram() : Main where ForExploration = true
{
    construct model program from ParameterCombination 
    where scope = "SpecExplorer1.AccumulatorModelProgram"
    //The value of the scope switch can be a .Net namespace or a fully-qualified class name.
}

/// Defines a scenario for slicing.
/// When explored on its own, this machine
/// leaves all its parameters unexpanded.
machine DoubleAddScenario() : Main where ForExploration = true
{
    //Omitting the parenthesis for an action invocation 
    //is equivalent to setting all its parameters to _ (unknown).
    (Add(_); Add; ReadAndReset)*
}

/// Selects the slice of the model program
/// that matches the scenario. The model program
/// supplies all parameter and state data omitted from the scenario.
machine SlicedAccumulatorModelProgram() : Main where ForExploration = true
{
    DoubleAddScenario || AccumulatorModelProgram //(synchronized) parallel composition
}

/// Builds a machine resulting from a link coverage traversal
/// of the sliced model program. It can be explored or saved as a
/// C# test suite that can be run in a VSTS unit test project
/// (by pushing the Generate Test Code button in the Exploration 
/// Manager toolbar). Most tests should fail, since the sample
/// implementation is empty.
machine AccumulatorTestSuite() : Main where ForExploration = true, TestEnabled = true
{
    construct test cases where strategy = "ShortTests" for SlicedAccumulatorModelProgram()
}

The first configuration (config Main) has several functions:

1. Define Actions: Each action declaration refers to a .NET method or event in the implementation contained in Accumulator.cs. Declaring actions as abstract allows the use of actions that do not correspond to actual implementation methods or event. Thus abstract actions allow modeling before the implementation is started, and can later be bound to an implementation when it does exist. See Actions for more details on actions.

2. Set Switches: Switches control exploration and testing. See SwitchClause for more details on switches.

The second configuration (config ParameterCombination) binds all occurrences of the Accumulator.Add action to the range (0 .. 2).

The machine definition (machine AccumulatorModelProgram) collects all Rule methods in the SpecExplorer1.Model.AccumulatorModelProgram namespace. The machine inherits the switch settings, action declarations, and parameter restrictions from ParameterCombination. Note also that the ForExploration flag has been set to true, which allows the machine to be explored.

See Also

Reference

SwitchClause

Concepts

Using Spec Explorer for the First Time
Actions