module tutorial.engines.template_minimum_environment;

import tutorial.engines.template_minimum_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;

Template Minimum Environment¶

Overview¶

The Engine environment of the engine.

Mailbox state¶

TemplateMinimumMailboxState¶

TemplateMinimumMailboxState : Type := Unit;

Local state¶

TemplateMinimumLocalState¶

type TemplateMinimumLocalState := mkTemplateMinimumLocalState;

Timer handles¶

TemplateMinimumTimerHandle¶

TemplateMinimumTimerHandle : Type := Unit;

TemplateMinimumTimestampedTrigger¶

TemplateMinimumTimestampedTrigger : Type :=
  TimestampedTrigger TemplateMinimumTimerHandle Anoma.Msg;

Engine Environment¶

TemplateMinimumEnv¶

TemplateMinimumEnv : Type :=
  EngineEnv
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    Anoma.Msg;

Instantiation¶

exTemplateMinimumEnv : TemplateMinimumEnv :=
  mkEngineEnv@{
    localState := mkTemplateMinimumLocalState;
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };