Illustration
abstract
  1. Actor computation
  • A collection of nodes represents actors. In other words: nodes : List Actor.
  • Each actor has an id. In other words, there is a function id : Actor → Id.
  • Each actor has an index in the list of actors. In other words, there is a function index : Actor → Index.
  • We say that two actors are equal in the list if they have the same ids, i.e., id(a1) = id(a2).
  • Actors may be repeated in the list, i.e., it might be the case that id(a1) = id(a2) ∧ index(a1) ≠ index(a2).
  • An edge x —[t:AType]→ y means that the node y has received the message t, which is a data structure of type AType. In other words: edge(x y t) : Edge and edges : List Edge.
  • We consider that two edges are equal if they start and end on the same nodes and transport the same message. In other words, given e1 ≡ edge(start1 end1 t1) and e2 ≡ edge(start2 end2 t2), we say that e1 = e2 iff start1 = start2 ∧ end1 = end2 ∧ t1 = t2.
  • The list of edges has no repetition.
  • Given a1,a2 two actors of nodes, we say that a < b iff there is an edge e ≡ edge(a b t) for some t.
  • < : Node Node → Prop forms a strict partial order on the nodes.
  • Given nodes and edges, (nodes,edges) : ActorComp is an actor computation.

If :

  • client represents some client, for instance your web browser;
  • Hello represents a HTTP request, for instance a POST request with data set to a JSON like {"type": "hello"}
  • World and Error are also HTTP requests;
  • server represents some web server.

Then : we may represent the discussion between the client and the server by an actor computation graph as follows:

First example
First example

Translated into English, a possible associated dialogue may be:

  1. The server received an instance of a Hello message from the client.
  2. The client received an instance of one of these two message types from the server: World or Error.