Juvix imports

module arch.node.engines.template_behaviour;

import arch.node.engines.template_messages open;
import arch.node.engines.template_environment open;
import Stdlib.Data.String open;
import prelude open;
import arch.node.types.basics 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;

TemplateActionLabel constructors¶

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.

This action consists of two components.

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;

TemplateMatchableArgument constructors¶

TemplateMatchableArgumentFirstOption FirstOptionMatchableArgument

type FirstOptionMatchableArgument := mkFirstOptionMatchableArgument {data : Val};

TemplateMatchableArgumentSecondOption SecondOptionMatchableArgument

type SecondOptionMatchableArgument :=
  mkSecondOptionMatchableArgument {data : String};

TemplateMatchableArgument¶

type TemplateMatchableArgument :=
  | TemplateMatchableArgumentFirstOption FirstOptionMatchableArgument
  | TemplateMatchableArgumentSecondOption SecondOptionMatchableArgument;

Examples of using TemplateMatchableArgument

Lorem ipsum dolor sit amet, consectetur adipiscing elit.

one : TemplateMatchableArgument :=
  TemplateMatchableArgumentFirstOption
    mkFirstOptionMatchableArgument@{
      data := 1
    };

someThingFromAMailboxExample : TemplateMatchableArgument :=
  TemplateMatchableArgumentSecondOption
    mkSecondOptionMatchableArgument@{
      data := "Hello World!"
    };

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 utilized by the engine to ensure efficient and accurate execution of its functions.

TemplatePrecomputation constructors¶

TemplatePrecomputationEntryDeleteMessage DeleteMessage

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

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

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.

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. 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¶

TemplateBehaviour¶

TemplateBehaviour : Type :=
  EngineBehaviour
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateMatchableArgument
    TemplateActionLabel
    TemplatePrecomputationList;

Instantiation¶

templateBehaviour : TemplateBehaviour :=
  mkEngineBehaviour@{
    guards := [messageOneGuard];
    action := templateAction;
    conflictSolver := templateConflictSolver
  };