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¶

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

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

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

LocalTSStorageActionExec : Type :=
  ActionExec
    LocalTSStorageLocalCfg
    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 GetDataTSStorageDBReply 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 EngineMsg.mk@{
                msg := Anoma.Msg.LocalTSStorage (LocalTSStorageMsg.GetRequest request);
                sender := sender;
              } :=
         let
           result :=
             queryDB
               (LocalTSStorageLocalState.db local)
               (GetDataTSStorageDBRequest.query request);
         in case result of {
              | some data :=
                some
                  ActionEffect.mk@{
                    env := env;
                    msgs :=
                      [
                        EngineMsg.mk@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := sender;
                          mailbox := some 0;
                          msg :=
                            Anoma.Msg.LocalTSStorage
                              (LocalTSStorageMsg.GetReply
                                GetDataTSStorageDBReply.mkGetDataTSStorageDBReply@{
                                  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 RecordDataTSStorageDBReply 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 EngineMsg.mk@{
                msg := Anoma.Msg.LocalTSStorage (LocalTSStorageMsg.RecordRequest 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 := LocalTSStorageLocalState.mk@{
                                                  db := newDb;
                                                  localClock := newTime;
                                                }};
                  responseMsg :=
                    EngineMsg.mk@{
                      sender := getEngineIDFromEngineCfg cfg;
                      target := sender;
                      mailbox := some 0;
                      msg :=
                        Anoma.Msg.LocalTSStorage
                          (LocalTSStorageMsg.DeleteReply
                            DeleteDataTSStorageDBReply.mkDeleteDataTSStorageDBReply@{
                              query := query;
                              success := true;
                            });
                    };
                  notificationMsg :=
                    \{target :=
                      EngineMsg.mk@{
                        sender := getEngineIDFromEngineCfg cfg;
                        target := target;
                        mailbox := some 0;
                        msg :=
                          Anoma.Msg.LocalTSStorage
                            (LocalTSStorageMsg.DataChanged
                              DataChangedTSStorageDB.mkDataChangedTSStorageDB@{
                                query := query;
                                data := value;
                                timestamp := newTime;
                              });
                      }};
                  notificationMsgs :=
                    map notificationMsg (getNotificationTargets query);
                in some
                  ActionEffect.mk@{
                    env := newEnv;
                    msgs := responseMsg :: notificationMsgs;
                    timers := [];
                    engines := [];
                  }
              | none :=
                some
                  ActionEffect.mk@{
                    env := env;
                    msgs :=
                      [
                        EngineMsg.mk@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := sender;
                          mailbox := some 0;
                          msg :=
                            Anoma.Msg.LocalTSStorage
                              (LocalTSStorageMsg.RecordReply
                                RecordDataTSStorageDBReply.mkRecordDataTSStorageDBReply@{
                                  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 DeleteDataTSStorageDBReply 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 EngineMsg.mk@{
                msg := Anoma.Msg.LocalTSStorage (LocalTSStorageMsg.DeleteRequest 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 := LocalTSStorageLocalState.mk@{
                                                  db := newDb;
                                                  localClock := newTime;
                                                }};
                  responseMsg :=
                    EngineMsg.mk@{
                      sender := getEngineIDFromEngineCfg cfg;
                      target := sender;
                      mailbox := some 0;
                      msg :=
                        Anoma.Msg.LocalTSStorage
                          (LocalTSStorageMsg.DeleteReply
                            DeleteDataTSStorageDBReply.mkDeleteDataTSStorageDBReply@{
                              query := query;
                              success := true;
                            });
                    };
                  notificationMsg :=
                    \{target :=
                      EngineMsg.mk@{
                        sender := getEngineIDFromEngineCfg cfg;
                        target := target;
                        mailbox := some 0;
                        msg :=
                          Anoma.Msg.LocalTSStorage
                            (LocalTSStorageMsg.DataChanged
                              DataChangedTSStorageDB.mkDataChangedTSStorageDB@{
                                query := query;
                                data := value;
                                timestamp := newTime;
                              });
                      }};
                  notificationMsgs :=
                    map notificationMsg (getNotificationTargets query);
                in some
                  ActionEffect.mk@{
                    env := newEnv;
                    msgs := responseMsg :: notificationMsgs;
                    timers := [];
                    engines := [];
                  }
              | none :=
                some
                  ActionEffect.mk@{
                    env := env;
                    msgs :=
                      [
                        EngineMsg.mk@{
                          sender := getEngineIDFromEngineCfg cfg;
                          target := sender;
                          mailbox := some 0;
                          msg :=
                            Anoma.Msg.LocalTSStorage
                              (LocalTSStorageMsg.DeleteReply
                                DeleteDataTSStorageDBReply.mkDeleteDataTSStorageDBReply@{
                                  query := query;
                                  success := false;
                                });
                        };
                      ];
                    timers := [];
                    engines := [];
                  }
            }
       | _ := none;

Action Labels¶

getDataActionLabel¶

getDataActionLabel : LocalTSStorageActionExec := ActionExec.Seq [getDataAction];

recordDataActionLabel¶

recordDataActionLabel : LocalTSStorageActionExec :=
  ActionExec.Seq [recordDataAction];

deleteDataActionLabel¶

deleteDataActionLabel : LocalTSStorageActionExec :=
  ActionExec.Seq [deleteDataAction];

Guards¶

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

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

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

getDataGuard¶

Condition

Message type is LocalTSStorageMsgGetRequest.

getDataGuard
  (trigger : LocalTSStorageTimestampedTrigger)
  (cfg : LocalTSStorageCfg)
  (env : LocalTSStorageEnv)
  : Option LocalTSStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some EngineMsg.mk@{
             msg := Anoma.Msg.LocalTSStorage (LocalTSStorageMsg.GetRequest _);
           } :=
      some
        GuardOutput.mk@{
          action := getDataActionLabel;
          args := [];
        }
    | _ := none;

recordDataGuard¶

Condition

Message type is LocalTSStorageMsgRecordRequest.

recordDataGuard
  (trigger : LocalTSStorageTimestampedTrigger)
  (cfg : LocalTSStorageCfg)
  (env : LocalTSStorageEnv)
  : Option LocalTSStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some EngineMsg.mk@{
             msg := Anoma.Msg.LocalTSStorage (LocalTSStorageMsg.RecordRequest _);
           } :=
      some
        GuardOutput.mk@{
          action := recordDataActionLabel;
          args := [];
        }
    | _ := none;

deleteDataGuard¶

Condition

Message type is LocalTSStorageMsgDeleteRequest.

deleteDataGuard
  (trigger : LocalTSStorageTimestampedTrigger)
  (cfg : LocalTSStorageCfg)
  (env : LocalTSStorageEnv)
  : Option LocalTSStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some EngineMsg.mk@{
             msg := Anoma.Msg.LocalTSStorage (LocalTSStorageMsg.DeleteRequest _);
           } :=
      some
        GuardOutput.mk@{
          action := deleteDataActionLabel;
          args := [];
        }
    | _ := none;

The Local Time Series Storage Behaviour¶

LocalTSStorageBehaviour¶

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

Instantiation¶

localTSStorageBehaviour : LocalTSStorageBehaviour :=
  EngineBehaviour.mk@{
    guards := GuardEval.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>LocalTSStorageMsgGetReply]
  end

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>LocalTSStorageMsgRecordReply]
    EMsg2>LocalTSStorageMsgDataChanged]
  end

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>LocalTSStorageMsgDeleteReply]
    EMsg2>LocalTSStorageMsgDataChanged]
  end