Juvix imports

module arch.node.engines.local_time_series_storage_behaviour;

import arch.node.engines.local_time_series_storage_messages open;
import arch.node.engines.local_time_series_storage_config open;
import arch.node.engines.local_time_series_storage_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;

Local Time Series Storage Behaviour¶

Overview¶

A time series storage engine acts as a database that can store, retrieve, and delete time series data.

Action arguments¶

`LocalTSStorageActionArgument`¶

type LocalTSStorageActionArgument := Unit;

`LocalTSStorageActionArguments`¶

LocalTSStorageActionArguments : Type := List LocalTSStorageActionArgument;

Actions¶

Auxiliary Juvix code

`LocalTSStorageAction`¶

LocalTSStorageAction : Type :=
  Action
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

`LocalTSStorageActionInput`¶

LocalTSStorageActionInput : Type :=
  ActionInput
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg;

`LocalTSStorageActionEffect`¶

LocalTSStorageActionEffect : Type :=
  ActionEffect
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

`LocalTSStorageActionExec`¶

LocalTSStorageActionExec : Type :=
  ActionExec
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

`getDataAction`¶

Get data from the time series database.

State update: The state remains unchanged.
Messages to be sent: A GetDataTSStorageDBResponse message with the requested data.
Engines to be spawned: No engine is created by this action.
Timer updates: No timers are set or cancelled.

getDataAction
  (input : LocalTSStorageActionInput) : Option LocalTSStorageActionEffect :=
  let
    env := ActionInput.env input;
    trigger := ActionInput.trigger input;
    cfg := ActionInput.cfg input;
    local := EngineEnv.localState env;
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some mkEngineMsg@{
                msg := Anoma.MsgLocalTSStorage (LocalTSStorageMsgGetRequest request);
                sender := sender;
              } :=
         let
           result :=
             queryDB
               (LocalTSStorageLocalState.db local)
               (GetDataTSStorageDBRequest.query request);
         in case result of {
              | some data :=
                some
                  mkActionEffect@{
                    env := env;
                    msgs :=
                      [
                        mkEngineMsg@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := sender;
                          mailbox := some 0;
                          msg :=
                            Anoma.MsgLocalTSStorage
                              (LocalTSStorageMsgGetResponse
                                mkGetDataTSStorageDBResponse@{
                                  query :=
                                    GetDataTSStorageDBRequest.query request;
                                  data := data;
                                });
                        };
                      ];
                    timers := [];
                    engines := [];
                  }
              | none := none
            }
       | _ := none;

`recordDataAction`¶

Record new data in the time series database.

State update: Updates the database with new time series data, if successful.
Messages to be sent: A RecordDataTSStorageDBResponse message indicating success/failure.; Several DataChangedTSStorageDB messages to those interested engines, if successful.
Engines to be spawned: No engine is created by this action.
Timer updates: No timers are set or cancelled.

recordDataAction
  (input : LocalTSStorageActionInput) : Option LocalTSStorageActionEffect :=
  let
    env := ActionInput.env input;
    trigger := ActionInput.trigger input;
    cfg := ActionInput.cfg input;
    local := EngineEnv.localState env;
    newTime := advanceTime (LocalTSStorageLocalState.localClock local);
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some mkEngineMsg@{
                msg := Anoma.MsgLocalTSStorage (LocalTSStorageMsgRecordRequest request);
                sender := sender;
              } :=
         let
           query := RecordDataTSStorageDBRequest.query request;
           db := LocalTSStorageLocalState.db local;
           data := queryDB db query;
         in case data of {
              | some value :=
                let
                  newDb := updateDB db query value;
                  newEnv :=
                    env@EngineEnv{localState := mkLocalTSStorageLocalState@{
                                                  db := newDb;
                                                  localClock := newTime;
                                                }};
                  responseMsg :=
                    mkEngineMsg@{
                      sender := getEngineIDFromEngineCfg cfg;
                      target := sender;
                      mailbox := some 0;
                      msg :=
                        Anoma.MsgLocalTSStorage
                          (LocalTSStorageMsgDeleteResponse
                            mkDeleteDataTSStorageDBResponse@{
                              query := query;
                              success := true;
                            });
                    };
                  notificationMsg :=
                    \{target :=
                      mkEngineMsg@{
                        sender := getEngineIDFromEngineCfg cfg;
                        target := target;
                        mailbox := some 0;
                        msg :=
                          Anoma.MsgLocalTSStorage
                            (LocalTSStorageMsgDataChanged
                              mkDataChangedTSStorageDB@{
                                query := query;
                                data := value;
                                timestamp := newTime;
                              });
                      }};
                  notificationMsgs :=
                    map notificationMsg (getNotificationTargets query);
                in some
                  mkActionEffect@{
                    env := newEnv;
                    msgs := responseMsg :: notificationMsgs;
                    timers := [];
                    engines := [];
                  }
              | none :=
                some
                  mkActionEffect@{
                    env := env;
                    msgs :=
                      [
                        mkEngineMsg@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := sender;
                          mailbox := some 0;
                          msg :=
                            Anoma.MsgLocalTSStorage
                              (LocalTSStorageMsgRecordResponse
                                mkRecordDataTSStorageDBResponse@{
                                  query := query;
                                  success := false;
                                });
                        };
                      ];
                    timers := [];
                    engines := [];
                  }
            }
       | _ := none;

`deleteDataAction`¶

Delete data from the time series database.

State update: Updates the database by removing specified time series data, if successful.
Messages to be sent: A DeleteDataTSStorageDBResponse message indicating success/failure.; Several DataChangedTSStorageDB messages to those interested engines, if successful.
Engines to be spawned: No engine is created by this action.
Timer updates: No timers are set or cancelled.

deleteDataAction
  (input : LocalTSStorageActionInput) : Option LocalTSStorageActionEffect :=
  let
    env := ActionInput.env input;
    trigger := ActionInput.trigger input;
    cfg := ActionInput.cfg input;
    local := EngineEnv.localState env;
    newTime := advanceTime (LocalTSStorageLocalState.localClock local);
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some mkEngineMsg@{
                msg := Anoma.MsgLocalTSStorage (LocalTSStorageMsgDeleteRequest request);
                sender := sender;
              } :=
         let
           query := DeleteDataTSStorageDBRequest.query request;
           db := LocalTSStorageLocalState.db local;
           data := queryDB db query;
         in case data of {
              | some value :=
                let
                  newDb := updateDB db query "";
                  newEnv :=
                    env@EngineEnv{localState := mkLocalTSStorageLocalState@{
                                                  db := newDb;
                                                  localClock := newTime;
                                                }};
                  responseMsg :=
                    mkEngineMsg@{
                      sender := getEngineIDFromEngineCfg cfg;
                      target := sender;
                      mailbox := some 0;
                      msg :=
                        Anoma.MsgLocalTSStorage
                          (LocalTSStorageMsgDeleteResponse
                            mkDeleteDataTSStorageDBResponse@{
                              query := query;
                              success := true;
                            });
                    };
                  notificationMsg :=
                    \{target :=
                      mkEngineMsg@{
                        sender := getEngineIDFromEngineCfg cfg;
                        target := target;
                        mailbox := some 0;
                        msg :=
                          Anoma.MsgLocalTSStorage
                            (LocalTSStorageMsgDataChanged
                              mkDataChangedTSStorageDB@{
                                query := query;
                                data := value;
                                timestamp := newTime;
                              });
                      }};
                  notificationMsgs :=
                    map notificationMsg (getNotificationTargets query);
                in some
                  mkActionEffect@{
                    env := newEnv;
                    msgs := responseMsg :: notificationMsgs;
                    timers := [];
                    engines := [];
                  }
              | none :=
                some
                  mkActionEffect@{
                    env := env;
                    msgs :=
                      [
                        mkEngineMsg@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := sender;
                          mailbox := some 0;
                          msg :=
                            Anoma.MsgLocalTSStorage
                              (LocalTSStorageMsgDeleteResponse
                                mkDeleteDataTSStorageDBResponse@{
                                  query := query;
                                  success := false;
                                });
                        };
                      ];
                    timers := [];
                    engines := [];
                  }
            }
       | _ := none;

Action Labels¶

`getDataActionLabel`¶

getDataActionLabel : LocalTSStorageActionExec := Seq [getDataAction];

`recordDataActionLabel`¶

recordDataActionLabel : LocalTSStorageActionExec := Seq [recordDataAction];

`deleteDataActionLabel`¶

deleteDataActionLabel : LocalTSStorageActionExec := Seq [deleteDataAction];

Guards¶

Auxiliary Juvix code

`LocalTSStorageGuard`¶

LocalTSStorageGuard : Type :=
  Guard
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

`LocalTSStorageGuardOutput`¶

LocalTSStorageGuardOutput : Type :=
  GuardOutput
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

`LocalTSStorageGuardEval`¶

LocalTSStorageGuardEval : Type :=
  GuardEval
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

`getDataGuard`¶

Condition: Message type is LocalTSStorageMsgGetRequest.

getDataGuard
  (trigger : LocalTSStorageTimestampedTrigger)
  (cfg : EngineCfg LocalTSStorageCfg)
  (env : LocalTSStorageEnv)
  : Option LocalTSStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgLocalTSStorage (LocalTSStorageMsgGetRequest _);
           } :=
      some
        mkGuardOutput@{
          action := getDataActionLabel;
          args := [];
        }
    | _ := none;

`recordDataGuard`¶

Condition: Message type is LocalTSStorageMsgRecordRequest.

recordDataGuard
  (trigger : LocalTSStorageTimestampedTrigger)
  (cfg : EngineCfg LocalTSStorageCfg)
  (env : LocalTSStorageEnv)
  : Option LocalTSStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgLocalTSStorage (LocalTSStorageMsgRecordRequest _);
           } :=
      some
        mkGuardOutput@{
          action := recordDataActionLabel;
          args := [];
        }
    | _ := none;

`deleteDataGuard`¶

Condition: Message type is LocalTSStorageMsgDeleteRequest.

deleteDataGuard
  (trigger : LocalTSStorageTimestampedTrigger)
  (cfg : EngineCfg LocalTSStorageCfg)
  (env : LocalTSStorageEnv)
  : Option LocalTSStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgLocalTSStorage (LocalTSStorageMsgDeleteRequest _);
           } :=
      some
        mkGuardOutput@{
          action := deleteDataActionLabel;
          args := [];
        }
    | _ := none;

The Local Time Series Storage Behaviour¶

`LocalTSStorageBehaviour`¶

LocalTSStorageBehaviour : Type :=
  EngineBehaviour
    LocalTSStorageCfg
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    LocalTSStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

Instantiation¶

localTSStorageBehaviour : LocalTSStorageBehaviour :=
  mkEngineBehaviour@{
    guards := First [getDataGuard; recordDataGuard; deleteDataGuard];
  };

Local Time Series Storage Action Flowcharts¶

`getData` Flowchart¶

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

  G(getDataGuard)
  A(getDataAction)

  C --> G -- *getDataActionLabel* --> A --> E

  subgraph E[Effects]
    EMsg>LocalTSStorageMsgGetResponse]
  end

getData flowchart

`recordData` Flowchart¶

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

  G(recordDataGuard)
  A(recordDataAction)

  C --> G -- *recordDataActionLabel* --> A --> E

  subgraph E[Effects]
    EEnv[(DB update)]
    EMsg1>LocalTSStorageMsgRecordResponse]
    EMsg2>LocalTSStorageMsgDataChanged]
  end

recordData flowchart

`deleteData` Flowchart¶

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

  G(deleteDataGuard)
  A(deleteDataAction)

  C --> G -- *deleteDataActionLabel* --> A --> E

  subgraph E[Effects]
    EEnv[(DB update)]
    EMsg1>LocalTSStorageMsgDeleteResponse]
    EMsg2>LocalTSStorageMsgDataChanged]
  end

deleteData flowchart

Local Time Series Storage Behaviour¶

Overview¶

Action arguments¶

LocalTSStorageActionArgument¶

LocalTSStorageActionArguments¶

Actions¶

LocalTSStorageAction¶

LocalTSStorageActionInput¶

LocalTSStorageActionEffect¶

LocalTSStorageActionExec¶

getDataAction¶

recordDataAction¶

deleteDataAction¶

Action Labels¶

getDataActionLabel¶

recordDataActionLabel¶

deleteDataActionLabel¶