module tutorial.engines.template_behaviour;

import tutorial.engines.template_messages open;
import tutorial.engines.template_config open;
import tutorial.engines.template_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 Behaviour¶

Overview¶

A template 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.

syntax alias Val := Nat;

One FirstArgument¶

type FirstArgument :=
  mk@{
    data : Val;
  };

Two SecondArgument¶

type SecondArgument :=
  mk@{
    data : String;
  };

TemplateActionArgument¶

type TemplateActionArgument :=
  | One FirstArgument
  | Two SecondArgument;

TemplateActionArguments¶

TemplateActionArguments : Type := List TemplateActionArgument;

Actions¶

TemplateAction : Type :=
  Action
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

TemplateActionInput : Type :=
  ActionInput
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg;

TemplateActionEffect : Type :=
  ActionEffect
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

TemplateActionExec : Type :=
  ActionExec
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

justHiAction¶

Action description.

State update

Update state with the data set by justHiGuard.

Messages to be sent

No messages are added to the send queue.

Engines to be spawned

No engine is created by this action.

Timer updates

No timers are set or cancelled.

Acquaintance updates

None.

justHiAction (input : TemplateActionInput) : Option TemplateActionEffect :=
  let
    env := ActionInput.env input;
    args := ActionInput.args input;
  in case args of
       | TemplateActionArgument.Two SecondArgument.mk@{data := data} :: _ :=
         some
           ActionEffect.mk@{
             env :=
               env@EngineEnv{localState := TemplateLocalState.mk@{
                                             taskQueue :=
                                               CustomData.mkCustomData@{
                                                 word := data;
                                               };
                                           }};
             msgs := [];
             timers := [];
             engines := [];
           }
       | _ := none;

exampleReplyAction¶

Respond with a TemplateMsgExampleReply.

State update

The state remains unchanged.

Messages to be sent

A TemplateMsgExampleReply 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 : TemplateActionInput) : Option TemplateActionEffect :=
  let
    cfg := ActionInput.cfg input;
    env := ActionInput.env input;
    trigger := ActionInput.trigger input;
    args := ActionInput.args input;
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some EngineMsg.mk@{
                msg := Anoma.Msg.Template (TemplateMsg.ExampleRequest req);
                sender := sender;
                target := target;
                mailbox := mailbox;
              } :=
         some
           ActionEffect.mk@{
             env := env;
             msgs :=
               [
                 EngineMsg.mk@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := sender;
                   mailbox := some 0;
                   msg :=
                     Anoma.Msg.Template
                       (TemplateMsg.ExampleReply
                         (ok
                           ExampleReplyOk.mkExampleReplyOk@{
                             argOne := ExampleRequest.argOne req;
                           }));
                 };
               ];
             timers := [];
             engines := [];
           }
       | _ := none;

Action Labels¶

justHiActionLabel¶

justHiActionLabel : TemplateActionExec := ActionExec.Seq [justHiAction];

exampleReplyActionLabel¶

exampleReplyActionLabel : TemplateActionExec :=
  ActionExec.Seq [exampleReplyAction];

doBothActionLabel¶

doBothActionLabel : TemplateActionExec :=
  ActionExec.Seq [justHiAction; exampleReplyAction];

Guards¶

TemplateGuard : Type :=
  Guard
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

TemplateGuardOutput : Type :=
  GuardOutput
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

TemplateGuardEval : Type :=
  GuardEval
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

justHiGuard¶

Guard description (optional).

Condition

Message type is TemplateMsgJustHi.

justHiGuard
  (trigger : TemplateTimestampedTrigger)
  (cfg : TemplateCfg)
  (env : TemplateEnv)
  : Option TemplateGuardOutput :=
  let
    emsg := getEngineMsgFromTimestampedTrigger trigger;
  in case emsg of
       | some EngineMsg.mk@{msg := Anoma.Msg.Template TemplateMsg.JustHi} :=
         some
           GuardOutput.mk@{
             action := justHiActionLabel;
             args :=
               [
                 TemplateActionArgument.Two
                   SecondArgument.mk@{
                     data := "Hello World!";
                   };
               ];
           }
       | _ := none;

exampleReplyGuard¶

Guard description (optional).

Condition

Message type is TemplateMsgExampleRequest.

exampleReplyGuard
  (trigger : TemplateTimestampedTrigger)
  (cfg : TemplateCfg)
  (env : TemplateEnv)
  : Option TemplateGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some EngineMsg.mk@{
             msg := Anoma.Msg.Template (TemplateMsg.ExampleRequest req);
             sender := mkPair none _;
           } :=
      some
        GuardOutput.mk@{
          action := exampleReplyActionLabel;
          args := [];
        }
    | _ := none;

Engine behaviour¶

TemplateBehaviour¶

TemplateBehaviour : Type :=
  EngineBehaviour
    TemplateLocalCfg
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

Instantiation¶

module template_behaviour_example;
  exTemplateBehaviour : TemplateBehaviour :=
    EngineBehaviour.mk@{
      guards := GuardEval.First [justHiGuard; exampleReplyGuard];
    };
end;

Template Action Flowchart¶

justHi Flowchart¶

flowchart TD
  subgraph C[Conditions]
    CMsg>TemplateMsgJustHi]
  end

  G(justHiGuard)
  A(justHiAction)

  C --> G -- *justHiActionLabel* --> A --> E

  subgraph E[Effects]
    EEnv[(Env update)]
  end

exampleReply Flowchart¶

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