Juvix imports
module arch.node.net.transport_behaviour;
import arch.node.net.transport_messages open;
import arch.node.net.transport_config open;
import arch.node.net.transport_environment 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;
Transport Behaviour¶
Overview¶
A transport engine acts in the ways described on this page. The action labels correspond to the actions that can be performed by the engine. Using the action labels, we describe the effects of the actions.
Action arguments¶
The action arguments are set by a guard
and passed to the action function as part of the GuardOutput
.
TransportActionArguments
¶
TransportActionArguments : Type := Unit;
Actions¶
Auxiliary Juvix code
TransportAction
¶
TransportAction : Type :=
Action
TransportLocalCfg
TransportLocalState
TransportMailboxState
TransportTimerHandle
TransportActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;
TransportActionInput
¶
TransportActionInput : Type :=
ActionInput
TransportLocalCfg
TransportLocalState
TransportMailboxState
TransportTimerHandle
TransportActionArguments
Anoma.Msg;
TransportActionEffect
¶
TransportActionEffect : Type :=
ActionEffect
TransportLocalState
TransportMailboxState
TransportTimerHandle
Anoma.Msg
Anoma.Cfg
Anoma.Env;
TransportActionExec
¶
TransportActionExec : Type :=
ActionExec
TransportLocalCfg
TransportLocalState
TransportMailboxState
TransportTimerHandle
TransportActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;
exampleReplyAction
¶
Respond with a TransportMsgExampleResponse
.
- State update
- The state remains unchanged.
- Messages to be sent
- A
TransportMsgExampleReply
message with the data set byexampleReplyGuard
. - Engines to be spawned
- No engine is created by this action.
- Timer updates
- No timers are set or cancelled.
exampleReplyAction
(input : TransportActionInput) : Option TransportActionEffect := TODO;
Action Labels¶
exampleReplyActionLabel
¶
exampleReplyActionLabel : TransportActionExec := Seq [exampleReplyAction];
Guards¶
Auxiliary Juvix code
TransportGuard
¶
TransportGuard : Type :=
Guard
TransportLocalCfg
TransportLocalState
TransportMailboxState
TransportTimerHandle
TransportActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;
TransportGuardOutput
¶
TransportGuardOutput : Type :=
GuardOutput
TransportLocalCfg
TransportLocalState
TransportMailboxState
TransportTimerHandle
TransportActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;
TransportGuardEval
¶
TransportGuardEval : Type :=
GuardEval
TransportLocalCfg
TransportLocalState
TransportMailboxState
TransportTimerHandle
TransportActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;
exampleReplyGuard
¶
Guard description (optional).
- Condition
- Message type is
TransportMsgExampleRequest
.
exampleReplyGuard
(trigger : TransportTimestampedTrigger)
(cfg : TransportCfg)
(env : TransportEnv)
: Option TransportGuardOutput := TODO;
The Transport behaviour¶
TransportBehaviour
¶
TransportBehaviour : Type :=
EngineBehaviour
TransportLocalCfg
TransportLocalState
TransportMailboxState
TransportTimerHandle
TransportActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;
Instantiation¶
transportBehaviour : TransportBehaviour :=
mkEngineBehaviour@{
guards := First [exampleReplyGuard];
};