Skip to content
Juvix imports

module arch.node.net.transport_protocol_behaviour;

import arch.node.net.transport_protocol_messages open;
import arch.node.net.transport_protocol_config open;
import arch.node.net.transport_protocol_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 Protocol Behaviour

Overview

A node proxy 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.

TransportProtocolActionArguments

TransportProtocolActionArguments : Type := Unit;

Actions

Auxiliary Juvix code

TransportProtocolAction

TransportProtocolAction : Type :=
Action
TransportProtocolLocalCfg
TransportProtocolLocalState
TransportProtocolMailboxState
TransportProtocolTimerHandle
TransportProtocolActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;

TransportProtocolActionInput

TransportProtocolActionInput : Type :=
ActionInput
TransportProtocolLocalCfg
TransportProtocolLocalState
TransportProtocolMailboxState
TransportProtocolTimerHandle
TransportProtocolActionArguments
Anoma.Msg;

TransportProtocolActionEffect

TransportProtocolActionEffect : Type :=
ActionEffect
TransportProtocolLocalState
TransportProtocolMailboxState
TransportProtocolTimerHandle
Anoma.Msg
Anoma.Cfg
Anoma.Env;

TransportProtocolActionExec

TransportProtocolActionExec : Type :=
ActionExec
TransportProtocolLocalCfg
TransportProtocolLocalState
TransportProtocolMailboxState
TransportProtocolTimerHandle
TransportProtocolActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;

exampleReplyAction

Respond with a TransportProtocolMsgExampleResponse.

State update
The state remains unchanged.
Messages to be sent
A TransportProtocolMsgExampleReply 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 : TransportProtocolActionInput)
: Option TransportProtocolActionEffect := TODO;

Action Labels

exampleReplyActionLabel

exampleReplyActionLabel : TransportProtocolActionExec :=
Seq [exampleReplyAction];

Guards

Auxiliary Juvix code

TransportProtocolGuard

TransportProtocolGuard : Type :=
Guard
TransportProtocolLocalCfg
TransportProtocolLocalState
TransportProtocolMailboxState
TransportProtocolTimerHandle
TransportProtocolActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;

TransportProtocolGuardOutput

TransportProtocolGuardOutput : Type :=
GuardOutput
TransportProtocolLocalCfg
TransportProtocolLocalState
TransportProtocolMailboxState
TransportProtocolTimerHandle
TransportProtocolActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;

TransportProtocolGuardEval

TransportProtocolGuardEval : Type :=
GuardEval
TransportProtocolLocalCfg
TransportProtocolLocalState
TransportProtocolMailboxState
TransportProtocolTimerHandle
TransportProtocolActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;

exampleReplyGuard

Guard description (optional).

Condition
Message type is TransportProtocolMsgExampleRequest.
exampleReplyGuard
(trigger : TransportProtocolTimestampedTrigger)
(cfg : TransportProtocolCfg)
(env : TransportProtocolEnv)
: Option TransportProtocolGuardOutput := TODO;

The Transport Protocol behaviour

TransportProtocolBehaviour

TransportProtocolBehaviour : Type :=
EngineBehaviour
TransportProtocolLocalCfg
TransportProtocolLocalState
TransportProtocolMailboxState
TransportProtocolTimerHandle
TransportProtocolActionArguments
Anoma.Msg
Anoma.Cfg
Anoma.Env;

Instantiation

module transport_protocol_behaviour_example;
exTransportProtocolBehaviour : TransportProtocolBehaviour :=
mkEngineBehaviour@{
guards := First [exampleReplyGuard];
};
end;

Transport Protocol Action Flowchart

exampleReply Flowchart

flowchart TD
  subgraph C[Conditions]
    CMsg>TransportProtocolMsgExampleRequest<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>TransportProtocolMsgExampleResponse<br/>argOne]
  end
exampleReply flowchart