# Tutorial on writing a simple "Hello, world!" P# program

We provide a small tutorial on how to create a simple "Hello, world!" P# program. We also provide the source code
for this "Hello, world!" program. The source code is fully documented to help you further understand how to
develop a simple P# program.

## Contents

* hello-world
  This dir contains the source code for the "Hello, world!" P# program.

## Build instructions: "Hello, world!" P# program

1. cd to the directory "hello-world"
2. Open the "HelloWorld.sln" solution in Visual Studio 2015 Preview.
3. Switch to "Release" in the configuration manager.
4. Select "Build Solution" to build the P# libraries.
5. The binaries are placed in "\pldi15_artifact\2-psharp-example\hello-world\Binaries\Release"

## Running the "Hello, world!" P# program

1. cd to the directory "\pldi15_artifact\2-psharp-example\hello-world\Binaries\Release"
2. Run the command:

```
.\HelloWorld.exe
```

You should see "Hello, World!" printed in the terminal.

## Tutorial

Note: This tutorial assumes basic knowledge of using Visual Studio.

1. Create a new Visual Studio 2015 Preview solution.
2. Create a new "Console Application" project.
3. Create a new "HelloWorld.cs" file.

The "HelloWorld.cs" file initially contains only the main method:

```
public class HelloWorld
{
  static void Main(string[] args)
  {

  }
}
```

4. Add the Microsoft.PSharp.dll reference to your project. The dll is available in the
  "\pldi15_artifact\2-psharp-example\hello-world" directory.

5. Import the following 3 namespaces (the last one is the P# runtime namespace):

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

6. Create a new "Hello" class which inherits from the abstract class "Machine" (this class is provided
  by the P# runtime).

```
internal class Hello : Machine
{

}
```

7. Because this is the main machine in the program (i.e. the first machine to be invoked by the P# runtime),
you have to add the attribute "Main":

```
[Main]
internal class Hello : Machine
{

}
```

8. Next, create a nested class in the Hello machine, called "Init", which inherits from the abstract
  class "State" (again provided by the P# runtime). As this is the initial state that the machine
  begins in, it must have the attribute "Initial":

```
[Main]
internal class Hello : Machine
{
  [Initial]
  private class Init : State
  {

  }
}
```

9. The next step is to create the OnEntry() method of the "Init" state, which is the method that is executed
  when the machine transitions to this state (in our case the very first method to be executed when the Machine
  is constructed). Thus, you can think of the OnEntry() method of the Initial state of a machine, as the
  constructor of the machine. OnEntry() overrides the virtual method provided by the abstract State class.

[Main]
internal class Hello : Machine
{
  [Initial]
  private class Init : State
  {
    protected override void OnEntry()
    {

    }
  }
}

10. In our example, the above OnEntry() will create a "World" machine, send the new machine an event containing the
  "Hello," string, and then terminate the Hello machine. To do this, add the following 3 lines of code to the OnEntry()

```
(this.Machine as Hello).World = Machine.Factory.CreateMachine<World>();
```

The above is the constructor for a new machine. The "this.Machine" is a handler that points to the machine class that
contains the state. It is a useful handler when you are coding inside a State class.

```
this.Send((this.Machine as Hello).World, new TextEvent("Hello,"));
```

The "Send" method is used for asynchronously sending a new event to a target machine. In our case we create a new
event TextEvent, which takes as an argument a string.

```
this.Delete();
```

The "Delete" method terminates the called machine and releases any resources.

Also declare a new field in the "Hello" machine:

```
private World World;
```

And delcare the event in the namespace scope. An event is a simple class that either contains no data (and thus
no constructor, only the default), or contains an object that must be cast to the correct type, when the event is
received.

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

Your code so far should look like:

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

namespace HelloWorld
{
  internal class TextEvent : Event
  {
    public TextEvent(Object payload)
    : base(payload)
    { }
  }

  [Main]
  internal class Hello : Machine
  {
    private World World;

    [Initial]
    private class Init : State
    {
      protected override void OnEntry()
      {
        (this.Machine as Hello).World = Machine.Factory.CreateMachine<World>();
        this.Send((this.Machine as Hello).World, new TextEvent("Hello,"));
        this.Delete();
      }
    }
  }

  public class HelloWorld
  {
    static void Main(string[] args)
    {

    }
  }
}
```

11. Next, you have to create the "World" machine. Similarly to "Hello", write the following code:

```
internal class World : Machine
{
  [Initial]
  private class Init : State
  {
    protected override void OnEntry()
    {

    }
  }
}
```

12. This time add a new empty state called "Waiting":

```
private class Waiting : State
{

}
```

To transition to this new state, add the following code to the OnEntry() of the Init state:

```
this.Raise(new NextEvent());
```

This raises a new event locally. Also add the following event to the namespace:

```
internal class NextEvent : Event { }
```

This is a simple event that contains no data.

To define the state transition, you have to override the method "DefineStepStateTransitions",
as follows:

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

  var initDict = new StepStateTransitions();
  initDict.Add(typeof(NextEvent), typeof(Waiting));

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

  return dict;
}
```

In the above code you create a new dictionary from "Type" to "StepStateTransitions", then you create a
new "StepStateTransitions" collection, you add a state transition (from the type of the received event,
to the type of the state to transition to). Finally, you add the "StepStateTransitions" collection to
the dictionary, which is returned to the P# Runtime.

13. Next, crete a new method called "Receive", this represents an action of the "World" machine.

```
private void Receive()
{
  string message = (string)this.Payload;

  message += " World!";

  Console.WriteLine(message);

  this.Delete();
}
```

In this action, you have access to "this.Payload", which is a handler to the implicitly received data
from the event that triggered to this action. Because the "TextEvent" event contained a string, the
Payload is casted as a string. Then the action add the string " World!" to the received string, and
prints the string. Finally, the action calls "Delete" to terminate the "World" machine.

14. Next, add an action binding for triggering the above "Receive" action. This is similar to how you
  can define a state transition:

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

  var waitingDict = new ActionBindings();
  waitingDict.Add(typeof(TextEvent), new Action(Receive));

  dict.Add(typeof(Waiting), waitingDict);

  return dict;
}
```

The "World" machine should now look like:

```
internal class World : Machine
{
  [Initial]
  private class Init : State
  {
    protected override void OnEntry()
    {
      this.Raise(new NextEvent());
    }
  }

  private class Waiting : State
  {

  }

  private void Receive()
  {
    string message = (string)this.Payload;

    message += " World!";

    Console.WriteLine(message);

    this.Delete();
  }

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

    var initDict = new StepStateTransitions();
    initDict.Add(typeof(NextEvent), typeof(Waiting));

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

    return dict;
  }

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

    var waitingDict = new ActionBindings();
    waitingDict.Add(typeof(TextEvent), new Action(Receive));

    dict.Add(typeof(Waiting), waitingDict);

    return dict;
  }
}
```

15. Finally, you must register the events and machines to the P# Runtime in the Main method, to
  "close" the environment. No machine or event type is allowed to be declared after the P#
  Runtime after the runtime starts. To do this use the following code:

```
Runtime.RegisterNewEvent(typeof(TextEvent));
Runtime.RegisterNewEvent(typeof(NextEvent));

Runtime.RegisterNewMachine(typeof(Hello));
Runtime.RegisterNewMachine(typeof(World));
```

16. Everything is ready now for the P# Runtime to start. To do this, call the following method
  in the Main method:

```
Runtime.Start();
```

To wait for the runtime to finish call:

```
Runtime.Wait();
```

Finally, call the following to dispose all the resources after the runtime terminates:

```
Runtime.Dispose();
```

This concludes the tutorial. Please also see the "Hello, World!" example source code for further help.
