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];
};