Juvix preamble

module node_architecture.engines.ticker_dynamics;

import prelude open;
import node_architecture.types.basics open;
import node_architecture.types.identities open;
import node_architecture.types.messages open;
import node_architecture.types.engine_environment open;
import node_architecture.types.engine_dynamics open;
import node_architecture.engines.ticker_overview open;
import node_architecture.engines.ticker_environment open;
import node_architecture.types.anoma_message open using {MsgTicker};

Ticker Dynamics

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

type TickerActionLabel :=
  | DoIncrement
  | DoRespond;

DoIncrement

DoIncrement

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

DoIncrement action effect

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.

DoRespond

DoRespond

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

DoRespond action effect

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.

Matchable arguments

type TickerMatchableArgument := ReplyTo (Option EngineID) (Option MailboxID);

ReplyTo

ReplyTo (Option EngineID) (Option MailboxID)

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

Precomputation results

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

syntax alias TickerPrecomputation := Unit;

Guards

Auxiliary Juvix code

Type alias for the guard.

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

TickerGuardOutput : Type :=
  GuardOutput TickerMatchableArgument TickerActionLabel TickerPrecomputation;

incrementGuard

flowchart TD
C{Increment<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@{
          args := [];
          label := DoIncrement;
          other := unit
        }
    | _ := 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@{
            args := [ReplyTo (some sender) none];
            label := DoRespond;
            other := unit
          };
      }
    | _ := none;

Action function

Auxiliary Juvix code

Type alias for the action function.

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

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

tickerAction (input : TickerActionInput) : TickerActionEffect :=
  let
    env := ActionInput.env input;
    out := ActionInput.guardOutput input;
  in case GuardOutput.label out of
       | DoIncrement :=
         let
           counterValue :=
             TickerLocalState.counter (EngineEnvironment.localState env);
         in mkActionEffect@{
           newEnv :=
             env@EngineEnvironment{localState := mkTickerLocalState@{
               counter := counterValue + 1
             }};
           producedMessages := [];
           timers := [];
           spawnedEngines := []
         }
       | DoRespond :=
         let
           counterValue :=
             TickerLocalState.counter (EngineEnvironment.localState env);
         in case GuardOutput.args out of
              | ReplyTo (some whoAsked) mailbox :: _ :=
                mkActionEffect@{
                  newEnv := env;
                  producedMessages :=
                    [ mkEngineMessage@{
                      sender := getSenderFromActionInput input;
                      target := whoAsked;
                      mailbox := some 0;
                      msg := MsgTicker Count
                    }
                    ];
                  timers := [];
                  spawnedEngines := []
                }
              | _ :=
                mkActionEffect@{
                  newEnv := env;
                  producedMessages := [];
                  timers := [];
                  spawnedEngines := []
                };

Conflict solver

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

Ticker Engine Family Summary

TickerEngineFamily
  : Anoma.EngineFamily
    TickerLocalState
    TickerMailboxState
    TickerTimerHandle
    TickerMatchableArgument
    TickerActionLabel
    TickerPrecomputation :=
  Anoma.mkEngineFamily@{
    guards := [incrementGuard; countGuard];
    action := tickerAction;
    conflictSolver := tickerConflictSolver
  };