Juvix imports
module tutorial.engines.template_minimum_behaviour;
import tutorial.engines.template_minimum_messages open;
import tutorial.engines.template_minimum_config open;
import tutorial.engines.template_minimum_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;
Template Minimum Behaviour¶
Overview¶
A Template Minimum 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.
TemplateMinimumActionArguments¶
TemplateMinimumActionArguments : Type := Unit;
Actions¶
Auxiliary Juvix code
TemplateMinimumAction¶
TemplateMinimumAction : Type :=
  Action
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;
TemplateMinimumActionInput¶
TemplateMinimumActionInput : Type :=
  ActionInput
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg;
TemplateMinimumActionEffect¶
TemplateMinimumActionEffect : Type :=
  ActionEffect
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;
TemplateMinimumActionExec¶
TemplateMinimumActionExec : Type :=
  ActionExec
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;
exampleReplyAction¶
Respond with a TemplateMinimumMsgExampleResponse.
- State update
- The state remains unchanged.
- Messages to be sent
- A TemplateMinimumMsgExampleReplymessage 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 : TemplateMinimumActionInput) : Option TemplateMinimumActionEffect :=
  TODO;
Action Labels¶
exampleReplyActionLabel¶
exampleReplyActionLabel : TemplateMinimumActionExec := Seq [exampleReplyAction];
Guards¶
Auxiliary Juvix code
TemplateMinimumGuard¶
TemplateMinimumGuard : Type :=
  Guard
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;
TemplateMinimumGuardOutput¶
TemplateMinimumGuardOutput : Type :=
  GuardOutput
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;
TemplateMinimumGuardEval¶
TemplateMinimumGuardEval : Type :=
  GuardEval
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;
exampleReplyGuard¶
Guard description (optional).
- Condition
- Message type is TemplateMinimumMsgExampleRequest.
exampleReplyGuard
  (trigger : TemplateMinimumTimestampedTrigger)
  (cfg : TemplateMinimumCfg)
  (env : TemplateMinimumEnv)
  : Option TemplateMinimumGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgTemplateMinimum (TemplateMinimumMsgExampleRequest req);
             sender := mkPair none _;
           } :=
      some
        mkGuardOutput@{
          action := exampleReplyActionLabel;
          args := unit;
        }
    | _ := none;
Engine behaviour¶
TemplateMinimumBehaviour¶
TemplateMinimumBehaviour : Type :=
  EngineBehaviour
    TemplateMinimumLocalCfg
    TemplateMinimumLocalState
    TemplateMinimumMailboxState
    TemplateMinimumTimerHandle
    TemplateMinimumActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;
Instantiation¶
module template_minimum_behaviour_example;
  exTemplateMinimumBehaviour : TemplateMinimumBehaviour :=
    mkEngineBehaviour@{
      guards := First [exampleReplyGuard];
    };
end;
Action Flowchart¶
exampleReply Flowchart¶
flowchart TD
  subgraph C[Conditions]
    CMsg>TemplateMinimumMsgExampleRequest<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>TemplateMinimumMsgExampleResponse<br/>argOne]
  endexampleReply flowchart