module arch.node.engines.ticker_behaviour;

import arch.node.engines.ticker_messages open;
import arch.node.engines.ticker_config open;
import arch.node.engines.ticker_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;

Ticker Behaviour¶

Overview¶

The Ticker engine maintains a counter as local state and allows two actions: incrementing the counter and sending the current counter value.

Action arguments¶

TickerActionArgumentReplyTo ReplyTo¶

type ReplyTo :=
  mkReplyTo@{
    whoAsked : Option EngineID;
    mailbox : Option MailboxID;
  };

This action argument contains the address and mailbox ID of where the response message should be sent.

whoAsked:

is the address of the engine that sent the message.

mailbox:

is the mailbox ID where the response message should be sent.

TickerActionArgument¶

type TickerActionArgument := | TickerActionArgumentReplyTo ReplyTo;

TickerActionArguments¶

TickerActionArguments : Type := List TickerActionArgument;

Actions¶

TickerAction : Type :=
  Action
    TickerLocalCfg
    TickerLocalState
    TickerMailboxState
    TickerTimerHandle
    TickerActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

TickerActionInput : Type :=
  ActionInput
    TickerLocalCfg
    TickerLocalState
    TickerMailboxState
    TickerTimerHandle
    TickerActionArguments
    Anoma.Msg;

TickerActionEffect : Type :=
  ActionEffect
    TickerLocalState
    TickerMailboxState
    TickerTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

TickerActionExec : Type :=
  ActionExec
    TickerLocalCfg
    TickerLocalState
    TickerMailboxState
    TickerTimerHandle
    TickerActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

incrementAction¶

Increment the counter.

State update

The counter value is increased by one.

Messages to be sent

No messages are added to the send queue.

Engines to be spawned

No engine is created by this action.

Timer updates

No timers are set or cancelled.

incrementAction (input : TickerActionInput) : Option TickerActionEffect :=
  let
    env := ActionInput.env input;
    counterValue := TickerLocalState.counter (EngineEnv.localState env);
  in some
    mkActionEffect@{
      env :=
        env@EngineEnv{localState := mkTickerLocalState@{
                                      counter := counterValue + 1;
                                    }};
      msgs := [];
      timers := [];
      engines := [];
    };

countReplyAction¶

Respond with the counter value.

State update

The state remains unchanged.

Messages to be sent

A message with the current counter value is sent to the requester.

Engines to be spawned

No engine is created by this action.

Timer updates

No timers are set or cancelled.

countReplyAction (input : TickerActionInput) : Option TickerActionEffect :=
  let
    cfg := ActionInput.cfg input;
    env := ActionInput.env input;
    trigger := ActionInput.trigger input;
    counterValue := TickerLocalState.counter (EngineEnv.localState env);
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some emsg :=
         some
           mkActionEffect@{
             env := env;
             msgs :=
               [
                 mkEngineMsg@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := EngineMsg.sender emsg;
                   mailbox := some 0;
                   msg :=
                     Anoma.MsgTicker
                       (TickerMsgCountReply
                         mkCountReply@{
                           counter := counterValue;
                         });
                 };
               ];
             timers := [];
             engines := [];
           }
       | _ := none;

Action Labels¶

incrementActionLabel¶

incrementActionLabel : TickerActionExec := Seq [incrementAction];

countReplyActionLabel¶

countReplyActionLabel : TickerActionExec := Seq [countReplyAction];

Guards¶

TickerGuard : Type :=
  Guard
    TickerLocalCfg
    TickerLocalState
    TickerMailboxState
    TickerTimerHandle
    TickerActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

TickerGuardOutput : Type :=
  GuardOutput
    TickerLocalCfg
    TickerLocalState
    TickerMailboxState
    TickerTimerHandle
    TickerActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

TickerGuardEval : Type :=
  GuardEval
    TickerLocalCfg
    TickerLocalState
    TickerMailboxState
    TickerTimerHandle
    TickerActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

incrementGuard¶

Condition

Message type is TickerMsgIncrement.

incrementGuard
  (trigger : TimestampedTrigger TickerTimerHandle Anoma.Msg)
  (cfg : TickerCfg)
  (env : TickerEnv)
  : Option TickerGuardOutput :=
  let
    emsg := getEngineMsgFromTimestampedTrigger trigger;
  in case emsg of
       | some mkEngineMsg@{msg := Anoma.MsgTicker TickerMsgIncrement} :=
         some
           mkGuardOutput@{
             action := incrementActionLabel;
             args := [];
           }
       | _ := none;

countReplyGuard¶

Condition

Message type is TickerMsgCountRequest.

countReplyGuard
  (trigger : TimestampedTrigger TickerTimerHandle Anoma.Msg)
  (cfg : TickerCfg)
  (env : TickerEnv)
  : Option TickerGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{msg := Anoma.MsgTicker TickerMsgCountRequest} :=
      some
        mkGuardOutput@{
          action := countReplyActionLabel;
          args := [];
        }
    | _ := none;

The Ticker behaviour¶

TickerBehaviour¶

TickerBehaviour : Type :=
  EngineBehaviour
    TickerLocalCfg
    TickerLocalState
    TickerMailboxState
    TickerTimerHandle
    TickerActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

Instantiation¶

tickerBehaviour : TickerBehaviour :=
  mkEngineBehaviour@{
    guards := First [incrementGuard; countReplyGuard];
  };

Ticker Action Flowchart¶

incrementAction flowchart¶

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

  G(incrementGuard)
  A(incrementAction)

  C --> G -- *incrementActionLabel* --> A --> E

  subgraph E[Effects]
    EEnv[(counter := counter + 1)]
  end

countReplyAction flowchart¶

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

  G(countReplyGuard)
  A(countReplyAction)

  C --> G -- *countReplyActionLabel* --> A --> E

  subgraph E[Effects]
    EMsg>TickerMsgCountReply<br/>counter]
  end