module arch.node.types.engine;

import prelude open;
import arch.node.types.identities open;
import arch.node.types.engine_config open public;
import arch.node.types.engine_environment open public;
import arch.node.types.engine_behaviour open public;

The type for engines¶

An engine is a computational unit with a specific name and behaviour, plus an initial environment, which comprises the specific state, the mailbox cluster, the acquaintances, and the timers.

We refer to the type of engines as Engine, instantiated with the following type parameters:

• A: the type for the action arguments,
• C: the type for the read-only engine configuration,
• S: the type for the local engine-specific state,
• B: the type for the mailbox state,
• H: the type for the timer handles,
• AM: the type for all engine messages (Msg),
• AC: the type for all engine configurations (Cfg), and
• AE: the type for all engine environments (Env).

Each engine, not its type, is associated with:

• a specific [Engine Configuration|configuration], which contains the engine name (unique across the system), node ID, and engine-specific configuration,
• a declaration of its own execution context, that is, the engine-specific local state, the mailbox cluster, the acquaintances, and the timers,
• as well as a specific behaviour.

type Engine (C S B H A AM AC AE : Type) :=
  mkEngine@{
    cfg : EngineCfg C;
    env : EngineEnv S B H AM;
    behaviour : EngineBehaviour C S B H A AM AC AE;
  };