Juvix preamble

module node_architecture.engines.ticker_behaviour;

import node_architecture.engines.ticker_messages open;
import node_architecture.engines.ticker_environment open;
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 open;
import node_architecture.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¶

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) :=
  \ {_ := []};

Engine behaviour¶