module arch.node.engines.local_time_series_storage_environment;

import prelude open;
import arch.node.engines.local_time_series_storage_messages open;
import arch.node.types.engine open;
import arch.node.types.messages open;
import arch.node.types.identities open;
import arch.node.types.anoma_message as Anoma open;

Local Time Series Storage Environment¶

Overview¶

The Local Time Series Storage Engine maintains a database of time series data with query and update capabilities.

Mailbox state¶

syntax alias LocalTSStorageMailboxState := Unit;

Local state¶

syntax alias Database := String;

axiom updateDB : Database -> TSStorageDBQuery -> TSStorageDBData -> Database;

axiom queryDB : Database -> TSStorageDBQuery -> Option TSStorageDBData;

axiom getNotificationTargets : TSStorageDBQuery -> List EngineID;

axiom advanceTime : EpochTimestamp -> EpochTimestamp;

LocalTSStorageLocalState¶

type LocalTSStorageLocalState :=
  mkLocalTSStorageLocalState@{
    db : Database;
    localClock : EpochTimestamp;
  };

Timer Handle¶

syntax alias LocalTSStorageTimerHandle := Unit;

LocalTSStorageTimestampedTrigger¶

LocalTSStorageTimestampedTrigger : Type :=
  TimestampedTrigger LocalTSStorageTimerHandle Anoma.Msg;

The Local Time Series Storage Environment¶

LocalTSStorageEnv¶

LocalTSStorageEnv : Type :=
  EngineEnv
    LocalTSStorageLocalState
    LocalTSStorageMailboxState
    LocalTSStorageTimerHandle
    Anoma.Msg;

Instantiation¶

localTSStorageEnv : LocalTSStorageEnv :=
  mkEngineEnv@{
    localState :=
      mkLocalTSStorageLocalState@{
        db := "";
        localClock := 0;
      };
    mailboxCluster := Map.empty;
    acquaintances := Set.empty;
    timers := [];
  };