libtlafmt 0.4.1

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/KeyValueStore.tla
---
----------------------------- MODULE KeyValueStore -----------------------------
(**************************************************************************)
(* A simple key-value store exhibiting snapshot isolation. If two         *)
(* concurrent transactions write to the same key, the one merging later   *)
(* will be rejected. If they write different keys both will succeed. For  *)
(* a more-detailed specification of snapshot isolation, look at the       *)
(* specifications/SnapshotIsolation specs in the tlaplus/examples repo.   *)
(**************************************************************************)

CONSTANTS Key,              \* The set of all keys.
    Val,                    \* The set of all values.
    TxId                    \* The set of all transaction IDs.
VARIABLES store,            \* A data store mapping keys to values.
    tx,                     \* The set of open snapshot transactions.
    snapshotStore,          \* Snapshots of the store for each transaction.
    written,                \* A log of writes performed within each transaction.
    missed                  \* The set of writes invisible to each transaction.
--------------------------------------------------------------------------------
NoVal == \* Choose something to represent the absence of a value.
    CHOOSE v: v \notin Val

Store == \* The set of all key-value stores.
    [Key -> Val \union {NoVal}]

Init == \* The initial predicate.
    /\ store = [k \in Key |-> NoVal]        \* All store values are initially NoVal.
    /\ tx = {}                              \* The set of open transactions is initially empty.
    /\ snapshotStore =                      \* All snapshotStore values are initially NoVal.
        [t \in TxId |-> [k \in Key |-> NoVal]]
    /\ written = [t \in TxId |-> {}]        \* All write logs are initially empty.
    /\ missed = [t \in TxId |-> {}]         \* All missed writes are initially empty.

TypeInvariant == \* The type invariant.
    /\ store \in Store
    /\ tx \subseteq TxId
    /\ snapshotStore \in [TxId -> Store]
    /\ written \in [TxId -> SUBSET Key]
    /\ missed \in [TxId -> SUBSET Key]

TxLifecycle ==
    /\ \A t \in tx: \* If store != snapshot & we haven't written it, we must have missed a write.
        \A k \in Key: (store[k] /= snapshotStore[t][k] /\ k \notin written[t]) => k \in missed[t]
    /\ \A t \in TxId \ tx: \* Checks transactions are cleaned up after disposal.
        /\ \A k \in Key: snapshotStore[t][k] = NoVal
        /\ written[t] = {}
        /\ missed[t] = {}

OpenTx(t) == \* Open a new transaction.
    /\ t \notin tx
    /\ tx' = tx \union {t}
    /\ snapshotStore' = [snapshotStore EXCEPT ![t] = store]
    /\ UNCHANGED << written, missed, store >>

Add(t, k, v) == \* Using transaction t, add value v to the store under key k.
    /\ t \in tx
    /\ snapshotStore[t][k] = NoVal
    /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v]
    /\ written' = [written EXCEPT ![t] = @ \union {k}]
    /\ UNCHANGED << tx, missed, store >>

Update(t, k, v) == \* Using transaction t, update the value associated with key k to v.
    /\ t \in tx
    /\ snapshotStore[t][k] \notin {NoVal, v}
    /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v]
    /\ written' = [written EXCEPT ![t] = @ \union {k}]
    /\ UNCHANGED << tx, missed, store >>

Remove(t, k) == \* Using transaction t, remove key k from the store.
    /\ t \in tx
    /\ snapshotStore[t][k] /= NoVal
    /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = NoVal]
    /\ written' = [written EXCEPT ![t] = @ \union {k}]
    /\ UNCHANGED << tx, missed, store >>

RollbackTx(t) == \* Close the transaction without merging writes into store.
    /\ t \in tx
    /\ tx' = tx \ {t}
    /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]]
    /\ written' = [written EXCEPT ![t] = {}]
    /\ missed' = [missed EXCEPT ![t] = {}]
    /\ UNCHANGED store

CloseTx(t) == \* Close transaction t, merging writes into store.
    /\ t \in tx
    /\ missed[t] \intersect written[t] = {} \* Detection of write-write conflicts.
    /\ store' =                             \* Merge snapshotStore writes into store.
        [k \in Key |-> IF k \in written[t] THEN snapshotStore[t][k] ELSE store[k]]
    /\ tx' = tx \ {t}
    /\ missed' = \* Update the missed writes for other open transactions.
        [otherTx \in TxId |-> IF otherTx \in tx' THEN missed[otherTx] \union written[t] ELSE {}]
    /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]]
    /\ written' = [written EXCEPT ![t] = {}]

Next == \* The next-state relation.
    \/ \E t \in TxId: OpenTx(t)
    \/ \E t \in tx: \E k \in Key: \E v \in Val: Add(t, k, v)
    \/ \E t \in tx: \E k \in Key: \E v \in Val: Update(t, k, v)
    \/ \E t \in tx: \E k \in Key: Remove(t, k)
    \/ \E t \in tx: RollbackTx(t)
    \/ \E t \in tx: CloseTx(t)

Spec == \* Initialize state with Init and transition with Next.
    Init /\ [][Next]_<< store, tx, snapshotStore, written, missed >>
--------------------------------------------------------------------------------
THEOREM Spec => [](TypeInvariant /\ TxLifecycle)
================================================================================