Ticker Environment¶

module arch.node.engines.ticker_environment;

import prelude open;
import arch.node.types.basics open;
import arch.node.engines.ticker_messages open;
import arch.node.types.engine_environment open;
import arch.node.types.messages open;
import arch.node.types.identities open;
import arch.node.types.anoma_message as Anoma open;

Overview¶

The sole data item of the ticker environment that deserves mention is the counter; we do not need timers, or mailbox state.

Mailbox states¶

syntax alias TickerMailboxState := Unit;

Local state¶

type TickerLocalState :=
  mkTickerLocalState@{
    counter : Nat;
  };

Timer Handle¶

syntax alias TickerTimerHandle := Unit;

The ticker does not require a timer handle type. Therefore, we define the timer handle type as Unit.

Timestamped Trigger¶

TickerTimestampedTrigger : Type :=
  TimestampedTrigger TickerTimerHandle Anoma.Msg;

The Ticker Environment¶

TickerEnv¶

TickerEnv : Type :=
  EngineEnv TickerLocalState TickerMailboxState TickerTimerHandle Anoma.Msg;

Instantiation¶

tickerEnv : TickerEnv :=
  mkEngineEnv@{
    localState :=
      mkTickerLocalState@{
        counter := 0;
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };