module arch.node.net.transport_environment;

import arch.node.net.transport_messages open;
import arch.node.types.basics open;
import arch.node.types.engine open;
import arch.node.types.messages open;
import arch.node.types.identities open;
import arch.node.types.anoma_message as Anoma open;

Transport Environment¶

Overview¶

The Engine environment of the engine.

Mailbox state¶

TransportMailboxState¶

TransportMailboxState : Type := Unit;

Local state¶

TransportLocalState¶

type TransportLocalState := mkTransportLocalState;

Timer handles¶

TransportTimerHandle¶

TransportTimerHandle : Type := Unit;

TransportTimestampedTrigger¶

TransportTimestampedTrigger : Type :=
  TimestampedTrigger TransportTimerHandle Anoma.Msg;

The Transport Environment¶

TransportEnv¶

TransportEnv : Type :=
  EngineEnv
    TransportLocalState
    TransportMailboxState
    TransportTimerHandle
    Anoma.Msg;

Instantiation¶

transportEnv : TransportEnv :=
  mkEngineEnv@{
    localState := mkTransportLocalState;
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };