module arch.node.engines.logging_behaviour;

import arch.node.engines.logging_messages open;
import arch.node.engines.logging_config open;
import arch.node.engines.logging_environment open;
import prelude 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;

Logging Behaviour¶

Overview¶

A logging engine maintains a logbook of entries and provides the capability to append new entries.

Action arguments¶

LoggingActionArgument¶

type LoggingActionArgument := Unit;

LoggingActionArguments¶

LoggingActionArguments : Type := List LoggingActionArgument;

Actions¶

LoggingAction : Type :=
  Action
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LoggingActionInput : Type :=
  ActionInput
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg;

LoggingActionEffect : Type :=
  ActionEffect
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LoggingActionExec : Type :=
  ActionExec
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

appendLogAction¶

Append new log entry to the logbook.

State update

Add the new log entry to the logbook.

Messages to be sent

No messages are sent by this action.

Engines to be spawned

No engine is created by this action.

Timer updates

No timers are set or cancelled.

appendLogAction (input : LoggingActionInput) : Option LoggingActionEffect :=
  let
    env := ActionInput.env input;
    trigger := ActionInput.trigger input;
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some mkEngineMsg@{
                msg := Anoma.MsgLogging (LoggingMsgAppend mkAppendValue@{
                                                            value := value;
                                                          });
              } :=
         let
           currentLogbook :=
             LoggingLocalState.logbook (EngineEnv.localState env);
           newLogbook := value :: currentLogbook;
         in some
           mkActionEffect@{
             env :=
               env@EngineEnv{localState := mkLoggingLocalState@{
                                             logbook := newLogbook;
                                           }};
             msgs := [];
             timers := [];
             engines := [];
           }
       | _ := none;

Action Labels¶

appendLogActionLabel¶

appendLogActionLabel : LoggingActionExec := Seq [appendLogAction];

Guards¶

LoggingGuard : Type :=
  Guard
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LoggingGuardOutput : Type :=
  GuardOutput
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LoggingGuardEval : Type :=
  GuardEval
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

appendLogGuard¶

Guard for append log action.

Condition

Message type is LoggingMsgAppend.

appendLogGuard
  (trigger : LoggingTimestampedTrigger)
  (cfg : EngineCfg LoggingCfg)
  (env : LoggingEnv)
  : Option LoggingGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{msg := Anoma.MsgLogging (LoggingMsgAppend _)} :=
      some
        mkGuardOutput@{
          action := appendLogActionLabel;
          args := [];
        }
    | _ := none;

The Logging behaviour¶

LoggingBehaviour¶

LoggingBehaviour : Type :=
  EngineBehaviour
    LoggingCfg
    LoggingLocalState
    LoggingMailboxState
    LoggingTimerHandle
    LoggingActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

Instantiation¶

loggingBehaviour : LoggingBehaviour :=
  mkEngineBehaviour@{
    guards := First [appendLogGuard];
  };

Logging Action Flowchart¶

appendLog Flowchart¶

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

  G(appendLogGuard)
  A(appendLogAction)

  C --> G -- *appendLogActionLabel* --> A --> E

  subgraph E[Effects]
    EEnv[(Update logbook)]
  end