Architecture 2

​ The operational architecture specification concerns the state evolution of Anoma instances, broken into smaller steps: which messages are exchanged, how computation is performed on the level of function calls, and which intermediate states are reachable. The specification is organized into the following sections:

• Hardware Abstraction Machine

• Control Machine

• Identity Machine

• Networking Machine

• Ordering Machine

Engine models

All engines communicate via message passing, following the paradigm of message passing concurrency. Thus, the only direct state manipulations that engine instances can perform are local state changes. All instances of a specific kind of engine share their behavior, which is defined as a function that

• takes a message and the current local state of an engine instance as input and

• computes the set of new messages (to be sent to other engine instances as reaction to the received message) and, optionally, a state update.

By default, the local state of an engine instance is a (subset of) all messages that are sent and received.

On Engine Models

Engines communicate via message passing. Each message consists of a header and a body. The header gives information about the sender and the intended destination, e.g., in the form of ɪᴅs or addresses. The type of the body almost always depends on the specific type of message. For each engine, we provide the following.

• A list of type names. Each type name is a string that specifies the type of message bodies that the engine has to be able to process (with the additional context that the header provides). Optionally, each type name in this list is mapped to a set of protocols to which it belongs.

• A list of pairs of type names and engines for message reactions. Each type name has a “static” approximation of all message reactions that a received message might trigger. Typically, there is no need to add identities or addresses of engine instance here.

• A type for each type name. The type of the message body is called message type as short hand for message body type. The message type does not need to re-iterate information of the message header. It is allowed that several type names refer to the message type.

• The types and behavior for each message body type. Using links to GitHub, Message types should be specified as SML types/datatypes (eventually matching the restrictions of colorsets of CPN Tools, i.e., only datatypes without proper recursion / induction). The behavior also has to give some information about headers, and define the behavior, using SML functions. This amounts to one function ReactionTypeName_\(p_{i,j,1}\) as below.

Todo

Even when the following renders, it is not really clear what the structure of the description is.