module arch.node.engines.local_key_value_storage_behaviour;

import arch.node.engines.local_key_value_storage_messages open;
import arch.node.engines.local_key_value_storage_config open;
import arch.node.engines.local_key_value_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 Key-Value Storage Behaviour¶

Overview¶

The Local Key-Value Storage engine processes get, set, and delete operations on key-value pairs.

Action arguments¶

LocalKVStorageActionArgument¶

type LocalKVStorageActionArgument := LocalKVStorageReplyTo EngineID;

LocalKVStorageActionArguments¶

LocalKVStorageActionArguments : Type := List LocalKVStorageActionArgument;

Actions¶

LocalKVStorageAction : Type :=
  Action
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LocalKVStorageActionInput : Type :=
  ActionInput
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg;

LocalKVStorageActionEffect : Type :=
  ActionEffect
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LocalKVStorageActionExec : Type :=
  ActionExec
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

getValueAction¶

Retrieve a value from storage by key.

State update

The state remains unchanged.

Messages to be sent

A GetValueKVStoreResponse message with the requested value.

Engines to be spawned

No engines are created by this action.

Timer updates

No timers are set or cancelled.

getValueAction
  (input : LocalKVStorageActionInput) : Option LocalKVStorageActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    local := EngineEnv.localState env;
    storage := LocalKVStorageLocalState.storage local;
    trigger := ActionInput.trigger input;
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some emsg :=
         case emsg of {
           | mkEngineMsg@{
               msg := Anoma.MsgLocalKVStorage (LocalKVStorageMsgGetValueRequest req);
             } :=
             some
               mkActionEffect@{
                 env := env;
                 msgs :=
                   [
                     mkEngineMsg@{
                       sender := getEngineIDFromEngineCfg cfg;
                       target := EngineMsg.sender emsg;
                       mailbox := some 0;
                       msg :=
                         Anoma.MsgLocalKVStorage
                           (LocalKVStorageMsgGetValueResponse
                             mkGetValueKVStoreResponse@{
                               key := GetValueKVStoreRequest.key req;
                               value :=
                                 fromOption
                                   (Map.lookup
                                     (GetValueKVStoreRequest.key req)
                                     storage)
                                   "";
                             });
                     };
                   ];
                 timers := [];
                 engines := [];
               }
           | _ := none
         }
       | _ := none;

setValueAction¶

Store a value in storage with given key.

State update

The storage map is updated with new key-value pair.

Messages to be sent

A SetValueKVStoreResponse message indicating success/failure.

Several LocalKVStorageMsgValueChanged messages to those interested engines.

Engines to be spawned

No engines are created by this action.

Timer updates

No timers are set or cancelled.

setValueAction
  (input : LocalKVStorageActionInput) : Option LocalKVStorageActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    local := EngineEnv.localState env;
    storage := LocalKVStorageLocalState.storage local;
    trigger := ActionInput.trigger input;
    newTime := advanceTime (LocalKVStorageLocalState.localClock local);
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some emsg :=
         case emsg of {
           | mkEngineMsg@{
               msg := Anoma.MsgLocalKVStorage (LocalKVStorageMsgSetValueRequest req);
             } :=
             let
               key := SetValueKVStoreRequest.key req;
               value := SetValueKVStoreRequest.value req;
               newStorage := Map.insert key value storage;
               newLocal :=
                 local@LocalKVStorageLocalState{
                   storage := newStorage;
                   localClock := newTime;
                 };
               newEnv := env@EngineEnv{localState := newLocal};
               responseMsg :=
                 mkEngineMsg@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := EngineMsg.sender emsg;
                   mailbox := some 0;
                   msg :=
                     Anoma.MsgLocalKVStorage
                       (LocalKVStorageMsgSetValueResponse
                         mkSetValueKVStoreResponse@{
                           key := key;
                           success := true;
                         });
                 };
               notificationMsg :=
                 \{target :=
                   mkEngineMsg@{
                     sender := getEngineIDFromEngineCfg cfg;
                     target := target;
                     mailbox := some 0;
                     msg :=
                       Anoma.MsgLocalKVStorage
                         (LocalKVStorageMsgValueChanged
                           mkValueChangedKVStore@{
                             key := key;
                             value := value;
                             timestamp := newTime;
                           });
                   }};
               notificationMsgs :=
                 map notificationMsg (getNotificationTargets key);
             in some
               mkActionEffect@{
                 env := newEnv;
                 msgs := responseMsg :: notificationMsgs;
                 timers := [];
                 engines := [];
               }
           | _ := none
         }
       | _ := none;

deleteValueAction¶

Remove a value from storage by key.

State update

The storage map is updated to remove the key-value pair.

Messages to be sent

A DeleteValueKVStoreResponse message indicating success/failure.

Several LocalKVStorageMsgValueChanged messages to those interested engines.

Engines to be spawned

No engines are created by this action.

Timer updates

No timers are set or cancelled.

deleteValueAction
  (input : LocalKVStorageActionInput) : Option LocalKVStorageActionEffect :=
  let
    env := ActionInput.env input;
    cfg := ActionInput.cfg input;
    local := EngineEnv.localState env;
    storage := LocalKVStorageLocalState.storage local;
    trigger := ActionInput.trigger input;
    newTime := advanceTime (LocalKVStorageLocalState.localClock local);
  in case getEngineMsgFromTimestampedTrigger trigger of
       | some emsg :=
         case emsg of {
           | mkEngineMsg@{
               msg := Anoma.MsgLocalKVStorage (LocalKVStorageMsgDeleteValueRequest req);
             } :=
             let
               key := DeleteValueKVStoreRequest.key req;
               newStorage := Map.delete key storage;
               newLocal :=
                 local@LocalKVStorageLocalState{
                   storage := newStorage;
                   localClock := newTime;
                 };
               newEnv := env@EngineEnv{localState := newLocal};
               responseMsg :=
                 mkEngineMsg@{
                   sender := getEngineIDFromEngineCfg cfg;
                   target := EngineMsg.sender emsg;
                   mailbox := some 0;
                   msg :=
                     Anoma.MsgLocalKVStorage
                       (LocalKVStorageMsgDeleteValueResponse
                         mkDeleteValueKVStoreResponse@{
                           key := key;
                           success := true;
                         });
                 };
               notificationMsg :=
                 \{target :=
                   mkEngineMsg@{
                     sender := getEngineIDFromEngineCfg cfg;
                     target := target;
                     mailbox := some 0;
                     msg :=
                       Anoma.MsgLocalKVStorage
                         (LocalKVStorageMsgValueChanged
                           mkValueChangedKVStore@{
                             key := key;
                             value := "";
                             timestamp := newTime;
                           });
                   }};
               notificationMsgs :=
                 map notificationMsg (getNotificationTargets key);
             in some
               mkActionEffect@{
                 env := newEnv;
                 msgs := responseMsg :: notificationMsgs;
                 timers := [];
                 engines := [];
               }
           | _ := none
         }
       | _ := none;

Action Labels¶

getValueActionLabel¶

getValueActionLabel : LocalKVStorageActionExec := Seq [getValueAction];

setValueActionLabel¶

setValueActionLabel : LocalKVStorageActionExec := Seq [setValueAction];

deleteValueActionLabel¶

deleteValueActionLabel : LocalKVStorageActionExec := Seq [deleteValueAction];

Guards¶

LocalKVStorageGuard : Type :=
  Guard
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LocalKVStorageGuardOutput : Type :=
  GuardOutput
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

LocalKVStorageGuardEval : Type :=
  GuardEval
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

getValueGuard¶

Condition

Message type is LocalKVStorageMsgGetValueRequest.

getValueGuard
  (trigger : LocalKVStorageTimestampedTrigger)
  (cfg : EngineCfg LocalKVStorageCfg)
  (env : LocalKVStorageEnv)
  : Option LocalKVStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgLocalKVStorage (LocalKVStorageMsgGetValueRequest _);
           } :=
      some
        mkGuardOutput@{
          action := getValueActionLabel;
          args := [];
        }
    | _ := none;

setValueGuard¶

Condition

Message type is LocalKVStorageMsgSetValueRequest.

setValueGuard
  (trigger : LocalKVStorageTimestampedTrigger)
  (cfg : EngineCfg LocalKVStorageCfg)
  (env : LocalKVStorageEnv)
  : Option LocalKVStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgLocalKVStorage (LocalKVStorageMsgSetValueRequest _);
           } :=
      some
        mkGuardOutput@{
          action := setValueActionLabel;
          args := [];
        }
    | _ := none;

deleteValueGuard¶

Condition

Message type is LocalKVStorageMsgDeleteValueRequest.

deleteValueGuard
  (trigger : LocalKVStorageTimestampedTrigger)
  (cfg : EngineCfg LocalKVStorageCfg)
  (env : LocalKVStorageEnv)
  : Option LocalKVStorageGuardOutput :=
  case getEngineMsgFromTimestampedTrigger trigger of
    | some mkEngineMsg@{
             msg := Anoma.MsgLocalKVStorage (LocalKVStorageMsgDeleteValueRequest _);
           } :=
      some
        mkGuardOutput@{
          action := deleteValueActionLabel;
          args := [];
        }
    | _ := none;

The Local Key-Value Storage behaviour¶

LocalKVStorageBehaviour¶

LocalKVStorageBehaviour : Type :=
  EngineBehaviour
    LocalKVStorageCfg
    LocalKVStorageLocalState
    LocalKVStorageMailboxState
    LocalKVStorageTimerHandle
    LocalKVStorageActionArguments
    Anoma.Msg
    Anoma.Cfg
    Anoma.Env;

Instantiation¶

localKVStorageBehaviour : LocalKVStorageBehaviour :=
  mkEngineBehaviour@{
    guards := First [getValueGuard; setValueGuard; deleteValueGuard];
  };

Local Key-Value Storage Action Flowcharts¶

getValue Flowchart¶

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

  G(getValueGuard)
  A(getValueAction)

  C --> G -- *getValueActionLabel* --> A --> E

  subgraph E[Effects]
    EMsg>LocalKVStorageMsgGetValueResponse<br/>key, value]
  end

setValue Flowchart¶

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

  G(setValueGuard)
  A(setValueAction)

  C --> G -- *setValueActionLabel* --> A --> E

  subgraph E[Effects]
    EEnv[(storage := Map.insert key value storage)]
    EMsg>LocalKVStorageMsgSetValueResponse<br/>success]
  end

deleteValue Flowchart¶

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

  G(deleteValueGuard)
  A(deleteValueAction)

  C --> G -- *deleteValueActionLabel* --> A --> E

  subgraph E[Effects]
    EEnv[(storage := Map.delete key storage)]
    EMsg>LocalKVStorageMsgDeleteValueResponse<br/>success]
  end