Skip to content
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 by exampleReplyGuard.
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];
};

Transport Action Flowchart

exampleReply Flowchart

flowchart TD
  subgraph C[Conditions]
    CMsg>TransportMsgExampleRequest<br/>from local engine]
    CEnv[(exampleValue < 10)]
  end

  G(exampleReplyGuard)
  A(exampleReplyAction)

  C --> G -- *exampleReplyActionLabel* --> A --> E

  subgraph E[Effects]
    EEnv[(exampleValue := exampleValue + 1)]
    EMsg>TransportMsgExampleResponse<br/>argOne]
  end
exampleReply flowchart