Juvix preamble

module node_architecture.engines.template_dynamics;

import Stdlib.Data.String open;
import prelude open;
import node_architecture.types.basics open;
import node_architecture.engines.template_overview open;
import node_architecture.engines.template_environment open;
import node_architecture.types.engine_dynamics open;

Template Dynamics

Overview

This engine does things in the ways described on this page.

Action labels

Auxiliary Juvix code

type SomeActionLabel := DoThis String;

type AnotherActionLabel := DoThat String;

type TemplateActionLabel :=
  | TemplateDoAlternative (Either SomeActionLabel AnotherActionLabel)
  | TemplateDoBoth (Pair SomeActionLabel AnotherActionLabel)
  | TemplateDoAnotherAction String;

TemplateDoAlternative

TemplateDoAlternative (Either SomeActionLabel AnotherActionLabel)

This action label corresponds to performing the doAlternative action and is relevant for guard X and Y.

example : TemplateActionLabel := TemplateDoAlternative (left (DoThis "do it!"));

TemplateDoAlternative action effect

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.

TemplateDoBoth

TemplateDoBoth (Pair SomeActionLabel AnotherActionLabel)

This action label corresponds to performing both the doAlternative and the doAnotherAction action.

TemplateDoBoth action effect

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.

TemplateDoAnotherAction

TemplateDoAnotherAction String

This action label corresponds to performing the doAnotherAction action.

TemplateDoAnotherAction action effect

This action 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.

Matchable arguments

Auxiliary Juvix code

syntax alias Val := Nat;

type TemplateMatchableArgument :=
  | TemplateMessageOne Val
  | TemplateSomeThingFromAMailbox String;

TemplateMessageOne

TemplateMessageOne Val

Lorem ipsum dolor sit amet, consectetur adipiscing elit.

TemplateMessageOne example

one : TemplateMatchableArgument := TemplateMessageOne 1;

TemplateMessageOne matchable argument

This matchable argument corresponds to the first message in the list of all messages.

Value1

Lorem ipsum dolor sit amet, consectetur adipiscing elit.

TemplateSomeThingFromAMailbox

TemplateSomeThingFromAMailbox String

Lorem ipsum dolor sit amet, consectetur adipiscing elit.

TemplateSomeThingFromAMailbox example

someThingFromAMailboxExample : TemplateMatchableArgument :=
  TemplateSomeThingFromAMailbox "Hello World!";

TemplateSomeThingFromAMailbox matchable argument

String

Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Precomputation results

Auxiliary Juvix code

syntax alias SomeMessageType := Nat;

type TemplatePrecomputationEntry :=
  | TemplateDeleteThisMessageFromMailbox SomeMessageType Nat
  | TemplateCloseMailbox Nat;

TemplatePrecomputation : Type := List TemplatePrecomputationEntry;

Often, the guard detects that we can close a mailbox and that we have to add a message to a mailbox. Note that we have a list of TemplatePrecomputationEntry-terms as precomputation result and that we describe the latter in more detail.

TemplateDeleteThisMessageFromMailbox

templateDeleteThisMessageFromMailboxExample : TemplatePrecomputationEntry :=
  TemplateDeleteThisMessageFromMailbox undef 1;

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

templateDeleteThisMessageFromMailboxExample : TemplatePrecomputationEntry :=
  TemplateDeleteThisMessageFromMailbox undef 1;

Guards

Auxiliary Juvix code

Type alias for the guard.

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

TemplateMessageOneGuard

flowchart TD
    C{TemplateMessageOne<br>received?}
    C -->|Yes| D[...]
    C -->|No| E[not enabled]
    D --> F([doAnotherAction n m])

TemplateMessageOneGuard flowchart

For TemplateMessageOne-messages, we do the other action, passing the String representation of the second and third argument.

messageOneGuard : TemplateGuard
  | _ _ :=
    some
      mkGuardOutput@{
        args := [TemplateSomeThingFromAMailbox "Hello World!"];
        label := TemplateDoAlternative (left (DoThis "paramneter 2"));
        other :=
          [TemplateCloseMailbox 1; TemplateDeleteThisMessageFromMailbox 1337 0]
      };

Action function

The action function amounts to one single case statement.

Auxiliary Juvix code

Type alias for the action function.

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

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

Conflict solver

Lorem ipsum dolor sit amet, consectetur adipiscing elit.

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

Template Engine Summary

TemplateEngineFamily
  : Anoma.EngineFamily
    TemplateLocalState
    TemplateMailboxState
    TemplateTimerHandle
    TemplateMatchableArgument
    TemplateActionLabel
    TemplatePrecomputation :=
  Anoma.mkEngineFamily@{
    guards := [messageOneGuard];
    action := templateAction;
    conflictSolver := templateConflictSolver
  };