Juvix preamble

module node_architecture.engines.template_behaviour;

import node_architecture.engines.template_messages open;
import node_architecture.engines.template_environment open;
import Stdlib.Data.String open;
import prelude open;
import node_architecture.types.basics open;
import node_architecture.types.engine open;

Template Behaviour¶

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)
  | _ := [];

Engine behaviour¶