InitialModeAttribute Class

Defines a set of mode tags that is assigned to the initial state of the model program.

Namespace: Microsoft.Modeling
Assembly: Microsoft.Xrt.Runtime (in Microsoft.Xrt.Runtime.dll)

Usage

'Usage

Syntax

'Declaration

[AttributeUsageAttribute(AttributeTargets.Class|AttributeTargets.Struct|AttributeTargets.Interface, AllowMultiple=true, Inherited=false)] 
public sealed class InitialModeAttribute : Attribute

Example

The following example shows a model program that makes use of various mode attributes to describe parts of the model behavior.

using Microsoft.Modeling;

namespace Modes
{
    [InitialMode("Unstarted")]
    [AcceptingMode("Finished")]
    [AcceptingMode("Unstarted")]
    [ErrorMode("StartError")]
    static class ModesModelProgram
    {
        static int jobCount = 0;

        [Probe]
        public static string CountProbe { get { return string.Format("Jobs: {0}", jobCount); } }

        [AcceptingStateCondition]
        static bool IsAccepting { get { return jobCount == 0; } }

        [Rule(Action = "Start(initialCount)", ModeTransition = "Unstarted->Running")]
        static void Start(int initialCount)
        {
            Condition.IsTrue(initialCount > 0);
            jobCount = initialCount;
        }

        [Rule(Action = "Start(initialCount)", ModeTransition = "Unstarted->StartError")]
        static void StartError(int initialCount)
        {
            Condition.IsFalse(initialCount > 0);
        }

        [Rule(Action = "DoNext", ModeTransition = "Running->Running")]
        static void DoNext()
        {
            Condition.IsTrue(jobCount > 0);
            jobCount--;
        }

        [Rule(Action = "Stop/result", ModeTransition = "Running->Finished")]
        static int Stop()
        {
            Condition.IsTrue(jobCount == 0);
            return jobCount;
        }

        [Rule(Action = "Stop/result", ModeTransition = "Running->JobError")]
        static int StopError()
        {
            Condition.IsFalse(jobCount == 0);
            return jobCount;
        }

        [Rule(ModeTransition = "Finished->Unstarted")]
        static void Reset()
        {
            jobCount = 0;
        }
    }
}

Remarks

During exploration, for each initial mode set that is defined, Spec Explorer creates a copy of the initial state and initializes the mode set of the initial state to the initial mode set. Spec Explorer marks each such state as an initial state of the transition system. For more information about using mode transitions, see Mode Sets.

Spec Explorer's validation process checks the value of the Mode property and generates a validation error if the value of the property is invalid. The compiler does not identify such errors.

For more information about using attributes, see Extending Metadata Using Attributes.

Inheritance Hierarchy

System.Object
   System.Attribute
    Microsoft.Modeling.InitialModeAttribute

Thread Safety

Any public static (Shared in Visual Basic) members of this type are thread safe. Any instance members are not guaranteed to be thread safe.

Platforms

Development Platforms

Microsoft Windows 7, Microsoft Windows Vista, Microsoft Windows XP SP2 or later, Microsoft Windows Server 2008, Microsoft Windows Server 2003

Change History

See Also

Reference

InitialModeAttribute Members
Microsoft.Modeling Namespace
AcceptingModeAttribute Class
ErrorModeAttribute Class
RuleAttribute.ModeTransition