module arch.node.types.engine_environment;

import arch.node.types.basics open public;
import arch.node.types.identities open;
import arch.node.types.messages open;

Engine environment¶

Engine environment type¶

The engine environment contains the following dynamic information for engine instances:

• Local state whose type is specific to the engine.
• Mailbox cluster, which is a map of mailbox IDs to mailboxes.
• A set of names of acquainted engine instances. It is implicit that the engine instance is acquainted with itself, so there is no need to include its own name.
• A list of timers that have been set.

This data is encapsulated within the EngineEnv type, which is parameterised by four types, which represent:

• S: the local state,
• B: the type of mailboxes' states,
• H: the type of handles for timers, and
• AM: the type of all engine messages (Msg).

These same letters will be used in the rest of the document to represent these types.

type EngineEnv (S B H AM : Type) :=
  mkEngineEnv@{
    localState : S;
    mailboxCluster : Map MailboxID (Mailbox B AM);
    acquaintances : Set EngineName;
    timers : List (Timer H);
  };