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

namespace HelloWorld
{
    #region Events

    /// <summary>
    /// A simple event that does not contain any data.
    /// </summary>
    internal class NextEvent : Event { }

    /// <summary>
    /// An event that contains an object. It is up to
    /// the machines to know how to interprete this object.
    /// In our case the object is a string.
    /// </summary>
    internal class TextEvent : Event
    {
        public TextEvent(Object payload)
            : base(payload)
        { }
    }

    #endregion

    #region Machines

    /// <summary>
    /// This is the main machine in the P# program. It creates a "Hello,"
    /// string and sends it to the World machine. There can be only one
    /// main machine (declared with [Main] attribute).
    /// </summary>
    [Main]
    internal class Hello : Machine
    {
        /// <summary>
        /// Reference to the World machine. This is required to know
        /// to which machine to communicate.
        /// </summary>
        private World World;

        /// <summary>
        /// This is the initial state of the machine. There can only be one
        /// initial state per machine (declared with [Initial] attribute).
        /// </summary>
        [Initial]
        private class Init : State
        {
            /// <summary>
            /// The OnEntry() method is the first method that executes upon entering
            /// a new state.
            /// </summary>
            protected override void OnEntry()
            {
                // Creates a new World machine.
                (this.Machine as Hello).World = Machine.Factory.CreateMachine<World>();

                // Sends asynchronously a new text event to World machine.
                this.Send((this.Machine as Hello).World, new TextEvent("Hello,"));

                // Terminates the machine as no more work is required to be done.
                this.Delete();
            }
        }
    }

    /// <summary>
    /// The World machine.
    /// </summary>
    internal class World : Machine
    {
        [Initial]
        private class Init : State
        {
            protected override void OnEntry()
            {
                // This is a locally raised event that transitions the machine to
                // the Waiting state.
                this.Raise(new NextEvent());
            }
        }

        /// <summary>
        /// A new state that the machine transitions to, when it receives the
        /// event TextEvent.
        /// </summary>
        private class Waiting : State
        {
            // The state does not perform any OnEntry() functionality.
            // It just waits until it receives a message from the Hello
            // machine.
        }

        private void Receive()
        {
            // The payload is the data contained in the implicitly received event.
            // It has to be casted to the expected type.
            string message = (string)this.Payload;

            message += " World!";

            Console.WriteLine(message);

            // Terminates the machine as no more work is required to be done.
            this.Delete();
        }

        /// <summary>
        /// Overriden method where the user must define all possible state transitions.
        /// </summary>
        protected override Dictionary<Type, StepStateTransitions> DefineStepStateTransitions()
        {
            // Create a new dictionary from Type to StepStateTransitions
            var dict = new Dictionary<Type, StepStateTransitions>();

            // Create a new StepStateTransitions collection
            var initDict = new StepStateTransitions();

            // Add a state transition: from the type of the received event, to the type of
            // the State to transition to.
            initDict.Add(typeof(NextEvent), typeof(Waiting));

            // Add the StepStateTransitions collection to the dictionary
            dict.Add(typeof(Init), initDict);

            return dict;
        }

        /// <summary>
        /// Overriden method where the user must define all possible action bindings.
        /// </summary>
        protected override Dictionary<Type, ActionBindings> DefineActionBindings()
        {
            // Create a new dictionary from Type to ActionBindings
            var dict = new Dictionary<Type, ActionBindings>();

            // Create a new ActionBindings collection
            var waitingDict = new ActionBindings();

            // Add an action binding: from the type of the received event, to the type of
            // the action to perform.
            waitingDict.Add(typeof(TextEvent), new Action(Receive));

            // Add the ActionBindings collection to the dictionary
            dict.Add(typeof(Waiting), waitingDict);

            return dict;
        }
    }

    #endregion

    /// <summary>
    /// This is an example of using P#.
    /// </summary>
    public class HelloWorld
    {
        /// <summary>
        /// Entry point to the program, where the user must register all possible
        /// events and machines, before invoking the P# runtime. The registration
        /// happens to "close" the environment. No new machines daclarations are
        /// allowed after the P# runtime has started.
        /// </summary>
        static void Main(string[] args)
        {
            // Registers all events
            Runtime.RegisterNewEvent(typeof(TextEvent));
            Runtime.RegisterNewEvent(typeof(NextEvent));

            // Registers all machines
            Runtime.RegisterNewMachine(typeof(Hello));
            Runtime.RegisterNewMachine(typeof(World));

            // Starts the P# runtime.
            Runtime.Start();

            // Waits for the program to finish.
            Runtime.Wait();

            // Disposes any resources.
            Runtime.Dispose();
        }
    }
}
