Skip to content
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 TemplateMinimumMsgExampleReply 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 : 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]
  end
exampleReply flowchart