How to initialize the initial state from an external source

We received several emails to ask how to initialize the initial state from an external source recently, this post introduces a good pattern to do it.

We can implement our own data loader to load data from external source, and use this loader to initialize the state. Note that since data loading method might involve native invocation, we’d better set our loader to native (more details can be found at https://msdn.microsoft.com/en-us/library/ee620483.aspx).

Here is an example:

Model.cs

using System;
using System.Collections.Generic;
using System.Text;
using System.Linq;
using Microsoft.Modeling;
using Microsoft.Xrt.Runtime;
using System.IO;

[assembly: NativeType(typeof(Sample.MyLoader))]
namespace Sample
{
    static class MyLoader
    {
        internal static Sequence<UserData> Load()
        {
            int i;
            UserData data;
            Sequence<UserData> dataSequence = new Sequence<UserData>();
            string[] contents = File.ReadAllLines("c:\\temp\\data.txt");
            for (i = 0; i < contents.Length; i=i+2)
            {
                data.Name = contents[i];
                data.Address = contents[i + 1];
                dataSequence = dataSequence.Add(data);
            }
            return dataSequence;
        }
    }

    public struct UserData
    {
        public string Name;
        public string Address;
    }

    static class ModelProgram
    {
        static Sequence<UserData> Data = MyLoader.Load();

        [Rule]
        static Sequence<UserData> ShowData()
        {
            return Data;
        }

        [Rule]
        static void Clear()
        {
            Data = new Sequence<UserData>();
        }
    }
}

Config.cord

using Sample;
using Microsoft.Modeling;

config Main
{
    action abstract static Sequence<UserData> Adapter.ShowData();
    action abstract static void Adapter.Clear();

    switch StepBound = 128;
    switch PathDepthBound = 128;
}

machine ModelProgram() : Main
{
    construct model program from Main
}

And the data under c:\temp

Lisa
#5, Danling Street
Bob
Queen Square

Then we explore the ModelProgram machine, and get the exploration graph like:

Of course the data source is not limited to text files, you can design your own loader to make your model more powerful.

Please feel free to share your thoughts or other good approaches to initialize initial state.

Comments

• Anonymous
  February 15, 2012
  Hi to all I am trying to explore spec explorer Extension Feature in visual studio 2010.i have a basic doubt that how to automatically generate cord file code and model program code..If any one knows the answer please do reply to me either to my mail "ashokkumar1531@gmail.com" or else u can reply to this post..

• Anonymous
  November 19, 2012
  Will Spec Explorer be available soon for VS2012?