Juvix imports

module arch.node.engines.ticker_behaviour;

import arch.node.engines.ticker_messages 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_message open using {MsgTicker};

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 labels¶

TickerActionLabel constructors¶

TickerActionLabelDoIncrement

This action label corresponds to incrementing the counter and is relevant for the TickerMsgIncrement message.

This action does the following:

Aspect	Description
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.

TickerActionLabelDoRespond

This action label corresponds to responding with the current counter value and is relevant for the TickerMsgCount message.

This action does the following:

Aspect	Description
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.

TickerActionLabel¶

type TickerActionLabel :=
  | TickerActionLabelDoIncrement
  | TickerActionLabelDoRespond;

Matchable arguments¶

TickerMatchableArgument constructors¶

TickerMatchableArgumentReplyTo ReplyTo

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

This matchable 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.

TickerMatchableArgument¶

type TickerMatchableArgument := TickerMatchableArgumentReplyTo ReplyTo;

Precomputation tasks results¶

The Ticker engine does not require any non-trivial pre-computations.

TickerPrecomputationEntry¶

syntax alias TickerPrecomputationEntry := Unit;

TickerPrecomputation¶

TickerPrecomputationList : Type := List TickerPrecomputationEntry;

Guards¶

Auxiliary Juvix code

TickerGuard¶

TickerGuard : Type :=
  Guard
    TickerLocalState
    TickerTimerHandle
    TickerMailboxState
    TickerMatchableArgument
    TickerActionLabel
    TickerPrecomputationList;

TickerGuardOutput¶

TickerGuardOutput : Type :=
  GuardOutput TickerMatchableArgument TickerActionLabel TickerPrecomputationList;

incrementGuard¶

flowchart TD
C{TickerMsgIncrement<br>message<br>received?}
C -->|Yes| D[enabled]
C -->|No| E[not enabled]
D --> F([DoIncrement])

incrementGuard flowchart

incrementGuard
  (t : TimestampedTrigger TickerTimerHandle)
  (env : TickerEnvironment)
  : Option TickerGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgTicker Increment) :=
      some
        mkGuardOutput@{
          matchedArgs := [];
          actionLabel := TickerActionLabelDoIncrement;
          precomputationTasks := []
        }
    | _ := none;

countGuard¶

flowchart TD
C{Count<br>message<br>received?}
C -->|Yes| D[enabled]
C -->|No| E[not enabled]
D --> F([DoRespond])

countGuard flowchart

countGuard
  (t : TimestampedTrigger TickerTimerHandle)
  (env : TickerEnvironment)
  : Option TickerGuardOutput :=
  case getMessageFromTimestampedTrigger t of
    | some (MsgTicker Count) :=
      do {
        sender <- getSenderFromTimestampedTrigger t;
        pure
          mkGuardOutput@{
            matchedArgs :=
              [ TickerMatchableArgumentReplyTo
                mkReplyTo@{
                  whoAsked := some sender;
                  mailbox := none
                }
              ];
            actionLabel := TickerActionLabelDoRespond;
            precomputationTasks := []
          };
      }
    | _ := none;

Action function¶

Auxiliary Juvix code

TickerActionInput¶

TickerActionInput : Type :=
  ActionInput
    TickerLocalState
    TickerMailboxState
    TickerTimerHandle
    TickerMatchableArgument
    TickerActionLabel
    TickerPrecomputationList;

TickerActionEffect¶

TickerActionEffect : Type :=
  ActionEffect
    TickerLocalState
    TickerMailboxState
    TickerTimerHandle
    TickerMatchableArgument
    TickerActionLabel
    TickerPrecomputationList;

TickerActionFunction¶

TickerActionFunction : Type :=
  ActionFunction
    TickerLocalState
    TickerMailboxState
    TickerTimerHandle
    TickerMatchableArgument
    TickerActionLabel
    TickerPrecomputationList;

tickerAction¶

This action function does the following:

Increments the counter if the TickerMsgIncrement message is received, actioned by the TickerActionLabelDoIncrement label.`
Responds with the current counter value if the TickerMsgCount message is received, actioned by the TickerActionLabelDoRespond label.

tickerAction (input : TickerActionInput) : TickerActionEffect :=
  let
    env := ActionInput.env input;
    out := ActionInput.guardOutput input;
  in case GuardOutput.actionLabel out of
       | TickerActionLabelDoIncrement :=
         let
           counterValue :=
             TickerLocalState.counter (EngineEnvironment.localState env);
         in mkActionEffect@{
           newEnv :=
             env@EngineEnvironment{localState := mkTickerLocalState@{
               counter := counterValue + 1
             }};
           producedMessages := [];
           timers := [];
           spawnedEngines := []
         }
       | TickerActionLabelDoRespond :=
         let
           counterValue :=
             TickerLocalState.counter (EngineEnvironment.localState env);
         in case GuardOutput.matchedArgs out of
              | TickerMatchableArgumentReplyTo
                  mkReplyTo@{whoAsked := some whoAsked; mailbox := mailbox}
                :: _ :=
                mkActionEffect@{
                  newEnv := env;
                  producedMessages :=
                    [ mkEngineMessage@{
                      sender := getSenderFromActionInput input;
                      target := whoAsked;
                      mailbox := some 0;
                      msg := MsgTicker TickerMsgCount
                    }
                    ];
                  timers := [];
                  spawnedEngines := []
                }
              | _ :=
                mkActionEffect@{
                  newEnv := env;
                  producedMessages := [];
                  timers := [];
                  spawnedEngines := []
                };

Conflict solver¶

tickerConflictSolver¶

tickerConflictSolver
  : Set TickerMatchableArgument -> List (Set TickerMatchableArgument) :=
  \ {_ := []};

The Ticker behaviour¶

TickerBehaviour¶

TickerBehaviour : Type :=
  EngineBehaviour
    TickerLocalState
    TickerMailboxState
    TickerTimerHandle
    TickerMatchableArgument
    TickerActionLabel
    TickerPrecomputationList;

Instantiation¶

tickerBehaviour : TickerBehaviour :=
  mkEngineBehaviour@{
    guards := [incrementGuard; countGuard];
    action := tickerAction;
    conflictSolver := tickerConflictSolver
  };