NativeType Attribute

In general, Spec Explorer cannot explore unmanaged code. Unmanaged code is any code that runs outside the common language runtime. COM components, ActiveX components, and Win32 API functions are examples of unmanaged code.

However, Spec Explorer can evaluate all types defined in the System.Runtime.InteropServices and Microsoft.Win32 namespaces, as well as any type declared in a subnamespace of the Microsoft.Win32 or System.Runtime.InteropServices namespace.

In addition, Spec Explorer can explore other unmanaged types if the types are declared in a Microsoft.Xrt.Runtime.NativeTypeAttribute attribute in a modeling assembly.

Example 1

The following machine uses the native AddDays method of the System.DateTime type to add a specific number of days to a given date.

The C# model program looks like this:

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


using Microsoft.Modeling;

[assembly: Microsoft.Xrt.Runtime.NativeType("System.DateTime")]
namespace Date
{
    /// <summary>
    /// An example model program.
    /// </summary>
    static class ModelProgram
    {
        static DateTime dateTime = DateTime.Now;

        
        [Rule]
        static void AddDays(int days)
        {
            dateTime = dateTime.AddDays(days);
        }

    }
}

And the corresponding Cord configuration file looks like this:

config Main 
{
    action abstract static void DateAdapter.AddDays(int days) where days in {0..2};

    switch StepBound = 128;
    switch PathDepthBound = 128;
}

machine ModelProgram() : Main
{
    construct model program
    where scope = "Date.ModelProgram"
}

While DateTime is a managed type, some of the methods are implemented using unmanaged code. Thus the NativeType attribute is required for exploration. Exploring this machine shows that the model works correctly, adding zero, one, or two days for each step.

Example 2

The following machine models an incrementer and decrementer.

The C# model program looks like this:

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

using Microsoft.Modeling;

// [assembly: Microsoft.Xrt.Runtime.NativeType("nativeTest.Model.ReferenceType")]
namespace nativeTest.Model
{
    /// <summary>
    /// An example model program.
    /// </summary>
    static class ModelProgram
    {
        static ReferenceType reference = new ReferenceType();

        [Rule]
        static void Add()
        {
            reference.x++;
        }

        [Rule]
        static void Sub()
        {
            reference.x--;
        }

    }

    class ReferenceType
    {
        public int x;
    }
}

The corresponding Cord configuration file looks like this:

config Main 
{
    action abstract static void Adapter.Add();
    action abstract static void Adapter.Sub();

    switch StepBound = 128;
    switch PathDepthBound = 128;
}

/// Constructs a machine from the model program. 
/// Since the model is not finite, this machine explodes
/// and exploration is stopped by a bound.
machine ModelProgram() : Main
{
    construct model program
    where scope = "nativeTest.Model"
}

The exploration graph for the above machine shows many states since ReferenceType is a managed method. If the comment marks are removed from model program statement, making the assemblyAttribute active, the exploration graph shows only one step, as Spec Explorer can explore only the reference to the object.

// [assembly: Microsoft.Xrt.Runtime.NativeType("nativeTest.Model.ReferenceType")]

See Also

Reference

NativeTypeAttribute

Concepts

Model Programs

Other Resources

Model Program Attributes