Ticker Environment

Juvix preamble

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;

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 : Type := 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.

The Ticker Environment

TickerEnvironment

TickerEnvironment : Type :=
  EngineEnvironment TickerLocalState TickerMailboxState TickerTimerHandle;

Instantiation

zeroTickerEnvironment : TickerEnvironment :=
  mkEngineEnvironment@{
    name := "ticker";
    localState :=
      mkTickerLocalState@{
        counter := 0
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := []
  };