Skip to content
Juvix imports

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

Auxiliary Juvix code

TickerAction

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

TickerActionInput

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

TickerActionEffect

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

TickerActionExec

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

Auxiliary Juvix code

TickerGuard

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

TickerGuardOutput

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

TickerGuardEval

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
incrementAction flowchart

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
countReplyAction flowchart