//-----------------------------------------------------------------------
// <copyright file="BoundedAsync.cs" company="Microsoft">
//      Copyright (c) Microsoft Corporation. All rights reserved.
// 
//      THIS CODE AND INFORMATION ARE PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, 
//      EITHER EXPRESSED OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE IMPLIED WARRANTIES 
//      OF MERCHANTABILITY AND/OR FITNESS FOR A PARTICULAR PURPOSE.
// ----------------------------------------------------------------------------------
//      The example companies, organizations, products, domain names,
//      e-mail addresses, logos, people, places, and events depicted
//      herein are fictitious.  No association with any real company,
//      organization, product, domain name, email address, logo, person,
//      places, or events is intended or should be inferred.
// </copyright>
//-----------------------------------------------------------------------

using System;
using System.Collections.Generic;
using Microsoft.PSharp;

namespace BoundedAsync
{
    #region Events

    internal class eUnit : Event { }
    internal class eReq : Event { }
    internal class eResp : Event { }
    internal class eDone : Event { }

    internal class eInit : Event
    {
        public eInit(Object payload)
            : base(payload)
        { }
    }

    internal class eMyCount : Event
    {
        public eMyCount(Object payload)
            : base(payload)
        { }
    }

    #endregion

    #region C# Classes and Structs

    internal struct CountMessage
    {
        public int Count;

        public CountMessage(int count)
        {
            this.Count = count;
        }
    }

    #endregion

    #region Machines

    [Main]
    [Ghost]
    internal class Scheduler : Machine
    {
        private Machine Process1;
        private Machine Process2;
        private Machine Process3;
        private int Count;
        private int DoneCounter;

        [Initial]
        private class Init : State
        {
            protected override void OnEntry()
            {
                Console.WriteLine("Initializing Scheduler");

                (this.Machine as Scheduler).Process1 =
                    Machine.Factory.CreateMachine<Process>(this.Machine);
                (this.Machine as Scheduler).Process2 =
                    Machine.Factory.CreateMachine<Process>(this.Machine);
                (this.Machine as Scheduler).Process3 =
                    Machine.Factory.CreateMachine<Process>(this.Machine);

                Console.WriteLine("{0} sending event {1} to {2}",
                    this.Machine, typeof(eInit), (this.Machine as Scheduler).Process1);
                this.Send((this.Machine as Scheduler).Process1,
                    new eInit(new Tuple<Machine, Machine>(
                        (this.Machine as Scheduler).Process2,
                        (this.Machine as Scheduler).Process3)
                        ));

                Console.WriteLine("{0} sending event {1} to {2}",
                    this.Machine, typeof(eInit), (this.Machine as Scheduler).Process1);
                this.Send((this.Machine as Scheduler).Process2,
                    new eInit(new Tuple<Machine, Machine>(
                        (this.Machine as Scheduler).Process1,
                        (this.Machine as Scheduler).Process3)
                        ));

                Console.WriteLine("{0} sending event {1} to {2}",
                    this.Machine, typeof(eInit), (this.Machine as Scheduler).Process1);
                this.Send((this.Machine as Scheduler).Process3,
                    new eInit(new Tuple<Machine, Machine>(
                        (this.Machine as Scheduler).Process1,
                        (this.Machine as Scheduler).Process2)
                        ));

                (this.Machine as Scheduler).Count = 0;
                Console.WriteLine("Scheduler: Count: {0}", (this.Machine as Scheduler).Count);

                (this.Machine as Scheduler).DoneCounter = 3;

                Console.WriteLine("{0} raising event {1}", this.Machine, typeof(eResp));
                this.Raise(new eUnit());
            }

            protected override HashSet<Type> DefineDeferredEvents()
            {
                return new HashSet<Type>
                {
                    typeof(eReq)
                };
            }
        }

        private class Sync : State
        {
            protected override void OnExit()
            {
                Console.WriteLine("{0} sending event {1} to {2}",
                    this.Machine, typeof(eResp), (this.Machine as Scheduler).Process1);
                this.Send((this.Machine as Scheduler).Process1, new eResp());

                Console.WriteLine("{0} sending event {1} to {2}",
                    this.Machine, typeof(eResp), (this.Machine as Scheduler).Process1);
                this.Send((this.Machine as Scheduler).Process2, new eResp());

                Console.WriteLine("{0} sending event {1} to {2}",
                    this.Machine, typeof(eResp), (this.Machine as Scheduler).Process1);
                this.Send((this.Machine as Scheduler).Process3, new eResp());
            }
        }

        private class Done : State
        {
            protected override void OnEntry()
            {
                this.Delete();
            }
        }

        private void CountReq()
        {
            this.Count++;
            Console.WriteLine("Scheduler: Count: {0}", this.Count);

            if (this.Count == 3)
            {
                this.Count = 0;
                Console.WriteLine("Scheduler: Count: {0}", this.Count);

                Console.WriteLine("{0} raising event {1}", this, typeof(eResp));
                this.Raise(new eResp());
            }
        }

        private void CheckIfDone()
        {
            this.DoneCounter--;

            if (this.DoneCounter == 0)
            {
                Console.WriteLine("Scheduler: Done");
                this.Delete();
            }
        }

        protected override Dictionary<Type, StepStateTransitions> DefineStepStateTransitions()
        {
            Dictionary<Type, StepStateTransitions> dict = new Dictionary<Type, StepStateTransitions>();

            StepStateTransitions initDict = new StepStateTransitions();
            initDict.Add(typeof(eUnit), typeof(Sync));

            StepStateTransitions syncDict = new StepStateTransitions();
            syncDict.Add(typeof(eResp), typeof(Sync));
            syncDict.Add(typeof(eUnit), typeof(Done));

            dict.Add(typeof(Init), initDict);
            dict.Add(typeof(Sync), syncDict);

            return dict;
        }

        protected override Dictionary<Type, ActionBindings> DefineActionBindings()
        {
            Dictionary<Type, ActionBindings> dict = new Dictionary<Type, ActionBindings>();

            ActionBindings syncDict = new ActionBindings();
            syncDict.Add(typeof(eReq), new Action(CountReq));
            syncDict.Add(typeof(eDone), new Action(CheckIfDone));

            dict.Add(typeof(Sync), syncDict);

            return dict;
        }
    }

    [Ghost]
    internal class Process : Machine
    {
        private Machine Scheduler;
        private Machine LeftProcess;
        private Machine RightProcess;

        private CountMessage CountMessage;

        [Initial]
        private class _Init : State
        {
            protected override void OnEntry()
            {
                var machine = this.Machine as Process;

                Console.WriteLine("Initializing Process");

                machine.Scheduler = (Machine)this.Payload;

                Console.WriteLine("{0} raising event {1}", this.Machine, typeof(eUnit));
                this.Raise(new eUnit());
            }

            protected override HashSet<Type> DefineDeferredEvents()
            {
                return new HashSet<Type>
                {
                    typeof(eInit)
                };
            }
        }

        private class Init : State
        {
            protected override void OnEntry()
            {
                var machine = this.Machine as Process;

                machine.CountMessage = new CountMessage(0);

                Console.WriteLine("Process: Count: {0}", machine.CountMessage.Count);
            }
        }

        private class SendCount : State
        {
            protected override void OnEntry()
            {
                var machine = this.Machine as Process;

                machine.CountMessage.Count = machine.CountMessage.Count + 1;
                Console.WriteLine("Process: Count: {0}", machine.CountMessage.Count);

                var msg1 = machine.CountMessage;
                var msg2 = new CountMessage(machine.CountMessage.Count);

                Console.WriteLine("{0} sending event {1} to {2}",
                    this.Machine, typeof(eMyCount), machine.LeftProcess);
                this.Send(machine.LeftProcess, new eMyCount(msg1));

                Console.WriteLine("{0} sending event {1} to {2}",
                    this.Machine, typeof(eMyCount), machine.RightProcess);
                this.Send(machine.RightProcess, new eMyCount(msg2));

                Console.WriteLine("{0} sending event {1} to {2}",
                    this.Machine, typeof(eReq), machine.Scheduler);
                this.Send(machine.Scheduler, new eReq());

                if (machine.CountMessage.Count > 10)
                {
                    this.Raise(new eUnit());
                }
            }
        }

        private class Done : State
        {
            protected override void OnEntry()
            {
                var machine = this.Machine as Process;

                Console.WriteLine("Process: Done");
                this.Send(machine.Scheduler, new eDone());
                this.Delete();
            }

            protected override HashSet<Type> DefineIgnoredEvents()
            {
                return new HashSet<Type>
                {
                    typeof(eResp),
                    typeof(eMyCount)
                };
            }
        }

        private void InitAction()
        {
            Console.WriteLine("Process: Performing InitAction");

            this.LeftProcess = ((Tuple<Machine, Machine>)this.Payload).Item1;
            this.RightProcess = ((Tuple<Machine, Machine>)this.Payload).Item2;

            Console.WriteLine("{0} sending event {1} to {2}",
                    this, typeof(eReq), this.Scheduler);
            this.Send(this.Scheduler, new eReq());
        }

        private void ConfirmThatInSync()
        {
            Console.WriteLine("Process: Performing ConfirmThatInSync");

            var countMsg = (CountMessage)this.Payload;

            Runtime.Assert((this.CountMessage.Count <= countMsg.Count) &&
                (this.CountMessage.Count >= (countMsg.Count - 1)));
        }

        protected override Dictionary<Type, StepStateTransitions> DefineStepStateTransitions()
        {
            Dictionary<Type, StepStateTransitions> dict = new Dictionary<Type, StepStateTransitions>();

            StepStateTransitions _initDict = new StepStateTransitions();
            _initDict.Add(typeof(eUnit), typeof(Init));

            StepStateTransitions initDict = new StepStateTransitions();
            initDict.Add(typeof(eMyCount), typeof(Init));
            initDict.Add(typeof(eResp), typeof(SendCount));

            StepStateTransitions sendCountDict = new StepStateTransitions();
            sendCountDict.Add(typeof(eUnit), typeof(Done));
            sendCountDict.Add(typeof(eResp), typeof(SendCount));

            dict.Add(typeof(_Init), _initDict);
            dict.Add(typeof(Init), initDict);
            dict.Add(typeof(SendCount), sendCountDict);

            return dict;
        }

        protected override Dictionary<Type, ActionBindings> DefineActionBindings()
        {
            Dictionary<Type, ActionBindings> dict = new Dictionary<Type, ActionBindings>();

            ActionBindings initDict = new ActionBindings();
            initDict.Add(typeof(eInit), new Action(InitAction));

            ActionBindings sendCountDict = new ActionBindings();
            sendCountDict.Add(typeof(eMyCount), new Action(ConfirmThatInSync));

            dict.Add(typeof(Init), initDict);
            dict.Add(typeof(SendCount), sendCountDict);

            return dict;
        }
    }

    #endregion
}
