module arch.node.engines.wall_clock_behaviour;

import arch.node.engines.wall_clock_messages open;
import arch.node.engines.wall_clock_config open;
import arch.node.engines.wall_clock_environment open;
import prelude open;
import arch.node.types.basics open;
import arch.node.types.identities open;
import arch.node.types.messages open;
import arch.node.types.engine open;
import arch.node.types.anoma as Anoma open;

Wall Clock Behaviour¶

Overview¶

The behavior of the Wall Clock Engine defines how it processes get time requests and produces time results using the current wall clock time.

Action arguments¶

WallClockActionArgumentFrom MessageFrom¶

type MessageFrom :=
  mkMessageFrom@{
    whoAsked : Option EngineID;
    mailbox : Option MailboxID;
  };

WallClockActionArgument¶

type WallClockActionArgument := WallClockActionArgumentFrom MessageFrom;

WallClockActionArguments¶

WallClockActionArguments : Type := List WallClockActionArgument;

Actions¶

WallClockAction : Type :=
  Action
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

WallClockActionInput : Type :=
  ActionInput
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg;

WallClockActionEffect : Type :=
  ActionEffect
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

WallClockActionExec : Type :=
  ActionExec
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

getTimeAction¶

Return the current wall clock time.

State update

Time will have advanced.

Messages to be sent

A WallClockGetTimeResult message with the current time.

Engines to be spawned

No engine is created by this action.

Timer updates

No timers are set or cancelled.

getTimeAction (input : WallClockActionInput) : Option WallClockActionEffect :=
  let
    cfg := ActionInput.cfg input;
    env := ActionInput.env input;
    trigger := ActionInput.trigger input;
    currentTime := WallClockLocalState.currentTime (EngineEnv.localState env);
    newTime := advanceTime currentTime;
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some emsg :=
         some
           mkActionEffect@{
             env :=
               env@EngineEnv{localState := mkWallClockLocalState@{
                                             currentTime := newTime;
                                           }};
             msgs :=
               [
                 mkEngineMsg@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := EngineMsg.sender emsg;
                   mailbox := some 0;
                   msg :=
                     Anoma.MsgWallClock
                       (WallClockGetTimeResult
                         mkTimeResult@{
                           epochTime := newTime;
                         });
                 };
               ];
             timers := [];
             engines := [];
           }
       | _ := none;

Action Labels¶

getTimeActionLabel¶

getTimeActionLabel : WallClockActionExec := Seq [getTimeAction];

Guards¶

WallClockGuard : Type :=
  Guard
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

WallClockGuardOutput : Type :=
  GuardOutput
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

WallClockGuardEval : Type :=
  GuardEval
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

getTimeGuard¶

Condition

Message type is WallClockGetTime.

getTimeGuard
  (trigger : TimestampedTrigger WallClockTimerHandle Anoma.Msg)
  (cfg : EngineCfg WallClockCfg)
  (env : WallClockEnv)
  : Option WallClockGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{msg := Anoma.MsgWallClock WallClockGetTime} :=
      some
        mkGuardOutput@{
          action := getTimeActionLabel;
          args := [];
        }
    | _ := none;

The Wall Clock behaviour¶

WallClockBehaviour¶

WallClockBehaviour : Type :=
  EngineBehaviour
    WallClockCfg
    WallClockLocalState
    WallClockMailboxState
    WallClockTimerHandle
    WallClockActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

Instantiation¶

wallClockBehaviour : WallClockBehaviour :=
  mkEngineBehaviour@{
    guards := First [getTimeGuard];
  };

Wall Clock Action Flowchart¶

getTime Flowchart¶

flowchart TD
  subgraph C[Conditions]
    CMsg>WallClockGetTime]
  end

  G(getTimeGuard)
  A(getTimeAction)

  C --> G -- *getTimeActionLabel* --> A --> E

  subgraph E[Effects]
    EEnv[(time := advanceTime time)]
    EMsg>WallClockGetTimeResult<br/>epochTime]
  end