Looking at the Model Program

The Static Model that is generated by the wizard models a very simple accumulator. Values can be added to the accumulator, and the current accumulated value can be read out and reset.

Following is the C# code for the model program (from file AccumulatorModelProgram.cs):

using System;
using System.Collections.Generic;
using System.Text;
using System.Linq;

using Microsoft.Modeling;

namespace SpecExplorer1
{
    /// <summary>
    /// An example model program.
    /// </summary>
    static class AccumulatorModelProgram
    {
        static int accumulator;

        /// <summary>
        /// A rule that models the action of incrementing
        /// the accumulator by a number.
        /// </summary>
        /// <param name="x">The increment to be addded to the accumulator.</param>
        [Rule(Action = "Add(x)")]
        static void AddRule(int x)
        {
            Condition.IsTrue(x > 0);
            accumulator += x;
        }

        /// <summary>
        /// A rule that models the action of reading the 
        /// current value of the accumulator and then setting
        /// it back to zero.
        /// </summary>
        /// <returns>The value of the accumulator before being reset.</returns>
        [Rule(Action = "ReadAndReset()/result")]
        static int ReadAndResetRule()
        {
            Condition.IsTrue(accumulator > 0);
            int oldValue = accumulator;
            accumulator = 0;
            return oldValue;
        }
    }
}

Things to note about this program:

1. The state space of this model program consists of the variable accumulator. Clicking on any state in the Exploration Graph Viewer will show the State Browser pane, displaying the contents of the clicked state, with the accumulator set to the corresponding value.

2. Methods marked with the [Rule] attribute describe state transition rules. A state transition is enabled if all Condition statements are satisfied (that is, all required conditions are true). If a state transition is enabled in a given state, it will fire in that state, producing updates on the state variables resulting in a successor state.

3. In the [Rule] attribute, an Action label associates an action of the implementation under test with the transition rule. Variables used as arguments in the label must correspond to parameters in the transition rule method. The special name result can be used to refer to the return value of the method.

See Also

Concepts

Using Spec Explorer for the First Time