module arch.node.engines.wall_clock_environment;

import prelude open;
import arch.node.engines.wall_clock_messages 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;

syntax alias WallClockMailboxState := Unit;

type WallClockLocalState :=
  mkWallClockLocalState@{
    currentTime : EpochTimestamp;
  };

syntax alias WallClockTimerHandle := Unit;

axiom advanceTime : EpochTimestamp -> EpochTimestamp;

WallClockEnv : Type :=
  EngineEnv
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    Anoma.Msg;

module wall_clock_environment_example;
  
  wallClockEnv : WallClockEnv :=
    mkEngineEnv@{
      localState :=
        mkWallClockLocalState@{
          currentTime := 0;
        };
      mailboxCluster := Map.empty;
      acquaintances := Set.empty;
      timers := [];
    };
end;