module arch.node.net.router_environment;

import arch.node.net.router_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;

Router Environment¶

Overview¶

The Engine environment of the engine.

Mailbox state¶

RouterMailboxState : Type := Unit;

Local state¶

type RouterLocalState := mkRouterLocalState;

Timer handles¶

RouterTimerHandle : Type := Unit;

Timestamped Trigger¶

RouterTimestampedTrigger : Type :=
  TimestampedTrigger RouterTimerHandle Anoma.Msg;

The Router Environment¶

RouterEnv¶

RouterEnv : Type :=
  EngineEnv RouterLocalState RouterMailboxState RouterTimerHandle Anoma.Msg;

Instantiation¶

exRouterEnv : RouterEnv :=
  mkEngineEnv@{
    localState := mkRouterLocalState;
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };