﻿using Microsoft.PSharp;
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

namespace RaceTest
{
    /// <summary>
    /// A simple client server program with a race.
    /// Our detector should correctly flag it, as well as
    /// report line numbers for the conflicting accesses 
    /// when the /trace-readwrite switch is passed to it
    /// </summary>
    class Program
    {
        static void Main(string[] args)
        {
            var runtime = PSharpRuntime.Create();
            Program.Execute(runtime);
            Console.ReadLine();
        }

        [Microsoft.PSharp.Test]
        public static void Execute(PSharpRuntime runtime)
        {
            runtime.CreateMachine(typeof(Server));
        }
    }
}
