Juvix imports

module arch.node.engines.template_behaviour;

import prelude open;
import arch.node.engines.template_messages open;
import arch.node.engines.template_environment open;
import arch.node.types.engine_behaviour 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 labels¶

Auxiliary Juvix code

type SomeActionLabel := DoThis String;

type AnotherActionLabel := DoThat String;

`TemplateActionLabelDoOneThing`¶

Lorem ipsum dolor sit amet, consectetur adipiscing elit.

`TemplateActionLabelDoAlternative DoAlternative`¶

DoAlternative : Type := Either SomeActionLabel AnotherActionLabel;

This action label corresponds to performing the doAlternative action.

Either.left

This alternative does the following.

Aspect	Description
State update	The state is unchanged as the timer will have all information necessary.
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

Either.right

This alternative does the following.

Aspect	Description
State update	The state is unchanged as the timer will have all information necessary.
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.
Spawned engines	No engines are spawned by this action.

`TemplateActionLabelDoBoth DoBoth`¶

DoBoth : Type := Pair SomeActionLabel AnotherActionLabel;

This action label corresponds to performing both the SomeActionLabel and the AnotherActionLabel.

Pair.fst

This alternative does the following.

Aspect	Description
State update	The state is unchanged as the timer will have all information necessary.
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.

Pair.snd

This alternative does the following.

Aspect	Description
State update	The state is unchanged as the timer will have all information necessary.
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.

`TemplateActionLabel`¶

type TemplateActionLabel :=
  | TemplateActionLabelDoOneThing
  | TemplateActionLabelDoAlternative DoAlternative
  | TemplateActionLabelDoBoth DoBoth;

Matchable arguments¶

The matchable arguments correspond to the arguments that can be matched on in guards. The data matched on is passed to the action function.

Auxiliary Juvix code

syntax alias Val := Nat;

`TemplateMatchableArgumentFirstOption FirstOptionMatchableArgument`¶

type FirstOptionMatchableArgument := mkFirstOptionMatchableArgument@{data : Val};

Arguments

data:: is the value of the matchable argument.

`TemplateMatchableArgumentSecondOption SecondOptionMatchableArgument`¶

type SecondOptionMatchableArgument :=
  mkSecondOptionMatchableArgument@{data : String};

Arguments

data:: is the value of the matchable argument.

`TemplateMatchableArgument`¶

type TemplateMatchableArgument :=
  | TemplateMatchableArgumentFirstOption FirstOptionMatchableArgument
  | TemplateMatchableArgumentSecondOption SecondOptionMatchableArgument;

Precomputation tasks results¶

Auxiliary Juvix code

syntax alias SomeMessageType := Nat;

Precomputation tasks results are the outcomes generated during the precomputation phase. These results are used to optimize and prepare the engine's state and environment before the main computation begins (by actions). The results of these tasks are then utilised by the engine to ensure efficient and accurate execution of its functions.

`TemplatePrecomputationEntryDeleteMessage DeleteMessage`¶

type DeleteMessage :=
  mkDeleteMessage@{
    messageType : SomeMessageType;
    messageId : Nat;
  };

We delete the given message from the mailbox with the mailbox ID.

Arguments

messageType:: is the type of the message to delete.
messageId:: is the ID of the message to delete.

`TemplatePrecomputationEntryCloseMailbox CloseMailbox`¶

type CloseMailbox := mkCloseMailbox@{mailboxId : Nat};

We close the mailbox with the given mailbox ID.

Arguments

mailboxId:: is the ID of the mailbox to close.

`TemplatePrecomputationEntry`¶

type TemplatePrecomputationEntry :=
  | TemplatePrecomputationEntryDeleteMessage DeleteMessage
  | TemplatePrecomputationEntryCloseMailbox CloseMailbox;

`TemplatePrecomputationList`¶

TemplatePrecomputationList : Type := List TemplatePrecomputationEntry;

The precomputation results consist of a list of TemplatePrecomputation terms. Each entry can be either:

A DeleteMessage entry indicating a message should be deleted from a mailbox
A CloseMailbox entry indicating a mailbox should be closed

These entries are used by guards to specify mailbox operations that need to be performed as part of processing a message.

Guards¶

Auxiliary Juvix code

`TemplateGuard`¶

TemplateGuard : Type :=
  Guard
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateMatchableArgument
    TemplateActionLabel
    TemplatePrecomputationList;

`TemplateGuardOutput`¶

TemplateGuardOutput : Type :=
  GuardOutput
    TemplateMatchableArgument
    TemplateActionLabel
    TemplatePrecomputationList;

`messageOneGuard`¶

messageOneGuard : TemplateGuard
  | _ _ :=
    some
      mkGuardOutput@{
        matchedArgs :=
          [
            TemplateMatchableArgumentSecondOption
              mkSecondOptionMatchableArgument@{
                data := "Hello World!";
              };
          ];
        actionLabel :=
          TemplateActionLabelDoAlternative (left (DoThis "parameter 2"));
        precomputationTasks :=
          [
            TemplatePrecomputationEntryCloseMailbox
              mkCloseMailbox@{
                mailboxId := 1;
              };
            TemplatePrecomputationEntryDeleteMessage
              mkDeleteMessage@{
                messageType := 1337;
                messageId := 0;
              };
          ];
      };

Action function¶

The action function amounts to one single case statement.

Auxiliary Juvix code

`TemplateActionInput`¶

TemplateActionInput : Type :=
  ActionInput
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateMatchableArgument
    TemplateActionLabel
    TemplatePrecomputationList;

`TemplateActionEffect`¶

TemplateActionEffect : Type :=
  ActionEffect
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateMatchableArgument
    TemplateActionLabel
    TemplatePrecomputationList;

`TemplateActionFunction`¶

TemplateActionFunction : Type :=
  ActionFunction
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateMatchableArgument
    TemplateActionLabel
    TemplatePrecomputationList;

`templateAction`¶

Give a short description of the action function. The following action called templateAction does nothing. It preserves the environment, produces no messages, sets no timers, spawns no engines.

templateAction : TemplateActionFunction
  | mkActionInput@{guardOutput := out; env := env} :=
    case GuardOutput.actionLabel out of
      | TemplateActionLabelDoAlternative (left _) :=
        mkActionEffect@{
          newEnv := env;
          producedMessages := [];
          timers := [];
          spawnedEngines := [];
        }
      | _ := undef;

Conflict solver¶

The conflict solver is responsible for resolving conflicts between multiple guards that match simultaneously. When multiple guards match the same input, the conflict solver determines which combinations of guards can execute together.

In this template example, the conflict solver is very simple. It always returns an empty list, meaning no guards can execute simultaneously. This effectively serializes guard execution, allowing only one guard to execute at a time.

`templateConflictSolver`¶

templateConflictSolver
  : Set TemplateMatchableArgument -> List (Set TemplateMatchableArgument)
  | _ := [];

The Template behaviour¶