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 TransportProtocolMsgExampleReplymessage 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 : 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]
  endexampleReply flowchart