diff --git a/manifest.json b/manifest.json index d5528b4b..8bb3a6fe 100644 --- a/manifest.json +++ b/manifest.json @@ -453,7 +453,8 @@ "description": "A simple KVS implementing snapshot isolation", "source": "", "authors": [ - "Andrew Helwer" + "Andrew Helwer", + "Murat Demirbas" ], "tags": [], "modules": [ @@ -502,7 +503,50 @@ "result": "success" } ] - } + }, + { + "path": "specifications/KeyValueStore/KVsnap.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": ["pluscal"], + "models": [] + }, + { + "path": "specifications/KeyValueStore/MCKVsnap.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/KeyValueStore/MCKVsnap.cfg", + "runtime": "00:00:50", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness", + "symmetry" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/KeyValueStore/Util.tla", + "communityDependencies": [ + "Functions" + ], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/KeyValueStore/ClientCentric.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } ] }, { diff --git a/specifications/KeyValueStore/ClientCentric.tla b/specifications/KeyValueStore/ClientCentric.tla new file mode 100644 index 00000000..3cf66553 --- /dev/null +++ b/specifications/KeyValueStore/ClientCentric.tla @@ -0,0 +1,185 @@ +--------------------------- MODULE ClientCentric --------------------------- +EXTENDS Naturals, TLC, Sequences, FiniteSets, Util +VARIABLES Keys, Values +\* TODO InitValue could be bottom (_|_) + +\* TLA+ specifications of Client Centric Isolation Specification by Crooks et al: https://dl.acm.org/doi/10.1145/3087801.3087802 +\* TLA+ specifications by Tim Soethout (tim.soethout@ing.com) + +\* A database `State` is represented by keys with corresponding values +State == [Keys -> Values] + +\* An `Operation` is a read or write of a key and value +Operation == [op: {"read", "write"}, key: Keys, value: Values] + +\* Helpers representing Reads and Writes +r(k,v) == [op |-> "read", key |-> k, value |-> v] +w(k,v) == [op |-> "write", key |-> k, value |-> v] + +\* A `Transaction` is a total order of `Operation`s +\* Transaction == [ops: Seq(Operation), start: TimeStamp, commit: TimeStamp] +Transaction == Seq(Operation) +\* For simplicity we store start and commit in a lookup function +TimeStamp == Nat +TransactionTimes == [t \in Transaction |-> [start: TimeStamp, commit: TimeStamp]] + +\* "An execution e for a set of transactions +\* T is a totally ordered set defined by the pair (Se,−−t \in T−→), +\* where Se is the set of states generated by applying, +\* starting from the system’s initial state, a permutation of all the transactions in T ." +ExecutionElem == [parentState: State, transaction: Transaction] +\* resultState is the parentState of the next transaction, but not used in the isolation definitions. +\* ExecutionElem == [parentState: State, transaction: Transaction, resultState: State] +\* We represent an `Execution` as a sequence of `Transaction`s with their corresponding parent state. +\* Note: This execution does therefor not contain the "final state" of the execution, since it is not a parent state of a transaction. +Execution == Seq(ExecutionElem) + +\* Seq +executionStates(execution) == [ i \in 1..Len(execution) |-> execution[i].parentState ] +\* Set +executionTransactions(execution) == { ep.transaction : ep \in SeqToSet(execution) } + +\* "The parent state is the last state in the execution +\* Definition 1: s -T-> s' ≡ [(k,v) ∈ s ∧ (k,v) \notin s'] => k ∈ W_T /\ w(k,v) ∈ Σ_T => (k,v) ∈ s. +\* We refer to s as the parent state of T (denoted as sp,T ); to the +\* transaction that generated s as Ts ; and to the set of keys in which +\* s and s′ differ as ∆(s,s′)" +parentState(execution, transaction) == + LET ind == CHOOSE i \in 1..Len(execution): execution[i].transaction = transaction + IN execution[ind].parentState + +\* w(k,v) -to-> r(k,v) +\* check reads and writes, implicit because of "write" check in ReadStates +earlierInTransaction(transaction, op1, op2) == Index(transaction, op1) < Index(transaction, op2) + +\* state1 -*-> state2 +beforeOrEqualInExecution(execution, state1, state2) == + LET states == executionStates(execution) + IN Index(states, state1) <= Index(states, state2) + +\* Read states: from which states can the operation read it's value +ReadStates(execution, operation, transaction) == + LET Se == SeqToSet(executionStates(execution)) + sp == parentState(execution, transaction) + IN { s \in Se: + /\ beforeOrEqualInExecution(execution, s, sp) \* s -*-> s_p: restrict the valid read states for the operations in T to be no later than sp + /\ \/ s[operation.key] = operation.value \* (k,v) \in s + \/ \E write \in SeqToSet(transaction): + /\ write.op = "write" /\ write.key = operation.key /\ write.value = operation.value + /\ earlierInTransaction(transaction, write, operation) \* w(k,v)-to->r(k,v) +\* "By convention, write operations have read states too: for a write operation in T , they include all states in Se up to and including T ’s parent state." + \/ operation.op = "write" + } + +Preread(execution, transaction) == + \A operation \in SeqToSet(transaction): ReadStates(execution, operation, transaction) /= {} + +PrereadAll(execution, transactions) == + \A transaction \in transactions: Preread(execution, transaction) + +\* A state `s` is complete for `T` in `e` if every operation in `T` can read from `s` +Complete(execution, transaction, state) == + LET setOfAllReadStatesOfOperation(transactionOperations) == + { ReadStates(execution, operation, transaction) : operation \in SeqToSet(transactionOperations) } + \* readStatesForEmptyTransaction contains all previous states, to ensure that empty txns do not incorrectly invalidate the checked isolation level + readStatesForEmptyTransaction == { s \in SeqToSet(executionStates(execution)) : beforeOrEqualInExecution(execution, s, parentState(execution, transaction)) } + IN state \in INTERSECTION(setOfAllReadStatesOfOperation(transaction) \union { readStatesForEmptyTransaction } ) + +\* "the write set of T comprises the keys that T updates: WT = {k|w(k, v) ∈ ΣT }. +\* For simplicity of exposition, we assume that a transaction only writes a key once." +WriteSet(transaction) == + LET writes == { operation \in SeqToSet(transaction) : operation.op = "write" } + IN { operation.key : operation \in writes } +\* "Denoting the set of keys in which s and s′ differ as ∆(s, s′), we express this as NO-CONF_T (s) ≡ ∆(s, sp) ∩ WT = ∅" +NoConf(execution, transaction, state) == + LET Sp == parentState(execution, transaction) + delta == { key \in DOMAIN Sp : Sp[key] /= state[key] } + IN delta \intersect WriteSet(transaction) = {} + +\* `t1` comes before `t2` in wall clock/oracle time +ComesStrictBefore(t1, t2, timestamps) == timestamps[t1].commit < timestamps[t2].start + +\* Given system state and single transaction (seq of operations), determines new state +effects(state, transaction) == + ReduceSeq(LAMBDA o, newState: IF o.op = "write" THEN [newState EXCEPT ![o.key] = o.value] ELSE newState, transaction, state) + +\* Lists all possible permutations of executions given set of transactions +executions(initialState, transactions) == + \* All possible permutations + LET orderings == PermSeqs(transactions) +\* initialState == [k \in Keys |-> InitValue] \* makes it level-1 therefor pass it in + accummulator == [ execution |-> <<>>, nextState |-> initialState ] + IN { LET executionAcc == ReduceSeq( + \* store ExecutionElem in accumulator + LAMBDA t, acc: [ execution |-> Append(acc.execution, [parentState |-> acc.nextState, transaction |-> t]) + \* calcultate next state + , nextState |-> effects(acc.nextState,t) + ], + ordering, accummulator) +\* recover ExecutionElems + IN executionAcc.execution + : ordering \in orderings } + +\* Helper: checks if specific execution satisfies given commit test +executionSatisfiesCT(execution, commitTest(_,_)) == + LET transactions == executionTransactions(execution) + IN \A transaction \in transactions: commitTest(transaction, execution) + +\* tests there exists an execution for `transactions`, that satisfies the isolation level given by `commitTest` +\* "Definition 5 Given a set of transactions T and their read states, +\* a storagesystem satisfies an isolation level I iff ∃e:∀t ∈ T :CTI(t,e)." +satisfyIsolationLevel(initialState, transactions, commitTest(_,_)) == + \E execution \in executions(initialState, transactions): \A transaction \in transactions: + \* PrintT(<<"try execution:",execution>>) => + commitTest(transaction, execution) + +\* Serializability commit test +CT_SER(transaction, execution) == + Complete(execution, transaction, parentState(execution, transaction)) +Serializability(initialState, transactions) == satisfyIsolationLevel(initialState, transactions, CT_SER) + +\*SerializabilityDebug(initialState, transactions) == +\* \* if no executions satify commit test, print all executions +\* \/ (~\E execution \in executions(initialState, transactions): \A transaction \in transactions: +\* CT_SER(transaction, execution)) => \A execution \in executions(initialState, transactions): PrintT(<<"Execution not Serializable:",execution>>) +\* \* fall back to normal check +\* \/ \E execution \in executions(initialState, transactions): \A transaction \in transactions: CT_SER(transaction, execution) + +SerializabilityDebug(initialState, transactions) == + ~ Serializability(initialState, transactions) => Print(<<"Executions not Serializable:", executions(initialState, transactions)>>, FALSE) + +\* Snapshot Isolation +CT_SI(transaction, execution) == \E state \in SeqToSet(executionStates(execution)): + Complete(execution, transaction, state) /\ NoConf(execution, transaction, state) +SnapshotIsolation(initialState, transactions) == satisfyIsolationLevel(initialState, transactions, CT_SI) + +\* Strict Serializability: ∀T ∈T:T s_T′ -*-> s_T. +CT_SSER(timestamps, transaction, execution) == + LET Sp == parentState(execution, transaction) + IN /\ Complete(execution, transaction, Sp) + /\ \A otherTransaction \in executionTransactions(execution): + ComesStrictBefore(otherTransaction, transaction, timestamps) => + beforeOrEqualInExecution(execution, parentState(execution, otherTransaction), Sp) +\* For now inline `satisfyIsolationLevel` instead of `satisfyIsolationLevel(transactions, CT_SSER(timestamps)) because partial functions are not supported/hard` +StrictSerializability(initialState, transactions, timestamps) == + \E execution \in executions(initialState, transactions): \A transaction \in transactions: CT_SSER(timestamps, transaction, execution) + +\* Read Committed +CT_RC(transaction, execution) == Preread(execution, transaction) +ReadCommitted(initialState, transactions) == satisfyIsolationLevel(initialState, transactions, CT_RC) + +\* Read Uncommitted +CT_RU(transaction, execution) == TRUE +ReadUncommitted(initialState, transactions) == satisfyIsolationLevel(initialState, transactions, CT_RU) + +\* Check types in derived specification +TypeOKT(transactions) == +\* /\ InitValue \in Values + /\ transactions \subseteq Transaction + +TypeOK(transactions, execution) == + /\ TypeOKT(transactions) +\* /\ PrintT(State) + /\ execution \in Execution + +============================================================================= diff --git a/specifications/KeyValueStore/KVsnap.tla b/specifications/KeyValueStore/KVsnap.tla new file mode 100644 index 00000000..a2dbe08a --- /dev/null +++ b/specifications/KeyValueStore/KVsnap.tla @@ -0,0 +1,184 @@ +--------------------------- MODULE KVsnap --------------------------------- +(**************************************************************************) +(* Pluscal algoritm for a simple key-value store with snapshot isolation *) +(* This version has atomic updates of store and missed sets of txns *) +(**************************************************************************) +EXTENDS Integers, Sequences, FiniteSets, TLC, Util + +CONSTANTS Key, \* The set of all keys. + TxId, \* The set of all transaction IDs. + NoVal \* NoVal, which all keys are initialized with. + +\* Instantiating ClientCentric enables us to check transaction isolation guarantees this model satisfies +\* https://muratbuffalo.blogspot.com/2022/07/automated-validation-of-state-based.html +CC == INSTANCE ClientCentric WITH Keys <- Key, Values <- TxId \union {NoVal} + +wOp(k,v) == CC!w(k,v) +rOp(k,v) == CC!r(k,v) + +(* --algorithm KVsnap { + +variables + \* A data store mapping keys to values + store = [k \in Key |-> NoVal], + + \* The set of open snapshot transactions + tx = {}, + + \* The set of writes invisible to each transaction + missed = [t \in TxId |-> {}], + + \* reads/writes per txn_id, used for interfacing to CC + ops = [ tId \in TxId |-> <<>> ]; + +define { + \* for instantiating the ClientCentric module + InitialState == [k \in Key |-> NoVal] + SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f) + + \* snapshot isolation invariant + SnapshotIsolation == CC!SnapshotIsolation(InitialState, Range(ops)) + +\* Serialization == CC!Serializability(InitialState, Range(ops)) + + TypeOK == \* type invariant + /\ store \in [Key -> TxId \union {NoVal}] + /\ tx \subseteq TxId + /\ missed \in [TxId -> SUBSET Key] +} + + +\* Transaction processing +fair process (t \in TxId) +variables + snapshotStore = [k \in Key |-> NoVal], \* local snapshot of the store + read_keys={}, \* read keys for the transaction + write_keys={}; \* write keys for the transaction +{ +START: \* Start the transaction + tx := tx \union {self}; + snapshotStore := store; \* take my snapshot of store + + with (rk \in SUBSET Key; wk \in SUBSET Key \ {}) { + read_keys := rk; \* select a random read-key-set from possible read-keys + write_keys := wk; \* select a random write-key-set from possible write-keys + }; + + +READ: \* Process reads on my snapshot + \* log reads for CC isolation check + ops[self] := ops[self] \o SetToSeq({rOp(k, snapshotStore[k]): k \in read_keys}); + +UPDATE: \* Process writes on my snapshot, write 'self' as value + snapshotStore := [k \in Key |-> IF k \in write_keys THEN self ELSE snapshotStore[k] ]; + +COMMIT: \* Commit the transaction to the database if there is no conflict + if (missed[self] \intersect write_keys = {}) { + \* take self off of active txn set + tx := tx \ {self}; + + \* Update the missed writes for other open transactions (nonlocal update!) + missed := [o \in TxId |-> IF o \in tx THEN missed[o] \union write_keys ELSE missed[o]]; + + \* update store + store := [k \in Key |-> IF k \in write_keys THEN snapshotStore[k] ELSE store[k] ]; + + \* log reads for CC isolation check + ops[self] := ops[self] \o SetToSeq({wOp(k, self): k \in write_keys}); + } +} + + +} +*) + +\* BEGIN TRANSLATION (chksum(pcal) = "5ef5c453" /\ chksum(tla) = "f592c6a0") +VARIABLES store, tx, missed, ops, pc + +(* define statement *) +InitialState == [k \in Key |-> NoVal] +SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f) + + +SnapshotIsolation == CC!SnapshotIsolation(InitialState, Range(ops)) + + + +TypeOK == + /\ store \in [Key -> TxId \union {NoVal}] + /\ tx \subseteq TxId + /\ missed \in [TxId -> SUBSET Key] + +VARIABLES snapshotStore, read_keys, write_keys + +vars == << store, tx, missed, ops, pc, snapshotStore, read_keys, write_keys + >> + +ProcSet == (TxId) + +Init == (* Global variables *) + /\ store = [k \in Key |-> NoVal] + /\ tx = {} + /\ missed = [t \in TxId |-> {}] + /\ ops = [ tId \in TxId |-> <<>> ] + (* Process t *) + /\ snapshotStore = [self \in TxId |-> [k \in Key |-> NoVal]] + /\ read_keys = [self \in TxId |-> {}] + /\ write_keys = [self \in TxId |-> {}] + /\ pc = [self \in ProcSet |-> "START"] + +START(self) == /\ pc[self] = "START" + /\ tx' = (tx \union {self}) + /\ snapshotStore' = [snapshotStore EXCEPT ![self] = store] + /\ \E rk \in SUBSET Key: + \E wk \in SUBSET Key \ {}: + /\ read_keys' = [read_keys EXCEPT ![self] = rk] + /\ write_keys' = [write_keys EXCEPT ![self] = wk] + /\ pc' = [pc EXCEPT ![self] = "READ"] + /\ UNCHANGED << store, missed, ops >> + +READ(self) == /\ pc[self] = "READ" + /\ ops' = [ops EXCEPT ![self] = ops[self] \o SetToSeq({rOp(k, snapshotStore[self][k]): k \in read_keys[self]})] + /\ pc' = [pc EXCEPT ![self] = "UPDATE"] + /\ UNCHANGED << store, tx, missed, snapshotStore, read_keys, + write_keys >> + +UPDATE(self) == /\ pc[self] = "UPDATE" + /\ snapshotStore' = [snapshotStore EXCEPT ![self] = [k \in Key |-> IF k \in write_keys[self] THEN self ELSE snapshotStore[self][k] ]] + /\ pc' = [pc EXCEPT ![self] = "COMMIT"] + /\ UNCHANGED << store, tx, missed, ops, read_keys, write_keys >> + +COMMIT(self) == /\ pc[self] = "COMMIT" + /\ IF missed[self] \intersect write_keys[self] = {} + THEN /\ tx' = tx \ {self} + /\ missed' = [o \in TxId |-> IF o \in tx' THEN missed[o] \union write_keys[self] ELSE missed[o]] + /\ store' = [k \in Key |-> IF k \in write_keys[self] THEN snapshotStore[self][k] ELSE store[k] ] + /\ ops' = [ops EXCEPT ![self] = ops[self] \o SetToSeq({wOp(k, self): k \in write_keys[self]})] + ELSE /\ TRUE + /\ UNCHANGED << store, tx, missed, ops >> + /\ pc' = [pc EXCEPT ![self] = "Done"] + /\ UNCHANGED << snapshotStore, read_keys, write_keys >> + +t(self) == START(self) \/ READ(self) \/ UPDATE(self) \/ COMMIT(self) + +(* Allow infinite stuttering to prevent deadlock on termination. *) +Terminating == /\ \A self \in ProcSet: pc[self] = "Done" + /\ UNCHANGED vars + +Next == (\E self \in TxId: t(self)) + \/ Terminating + +Spec == /\ Init /\ [][Next]_vars + /\ \A self \in TxId : WF_vars(t(self)) + +Termination == <>(\A self \in ProcSet: pc[self] = "Done") + +\* END TRANSLATION + + +=========================================================================== +As an exercise try to add more yield points, make the actions smaller. +Especially see if you can pull out something from the atomic "COMMIT" label to earlier, and see what breaks. + + + diff --git a/specifications/KeyValueStore/LICENSE b/specifications/KeyValueStore/LICENSE new file mode 100644 index 00000000..87a9458a --- /dev/null +++ b/specifications/KeyValueStore/LICENSE @@ -0,0 +1,25 @@ +BSD 2-Clause License for ClientCentric.tla + +Copyright (c) 2020, ING Bank / CWI +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this + list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. \ No newline at end of file diff --git a/specifications/KeyValueStore/MCKVsnap.cfg b/specifications/KeyValueStore/MCKVsnap.cfg new file mode 100644 index 00000000..c37043fb --- /dev/null +++ b/specifications/KeyValueStore/MCKVsnap.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Key = {k1, k2} + TxId = {t1, t2, t3} + NoVal = NoVal + +SYMMETRY + TxIdSymmetric + +SPECIFICATION + Spec + +INVARIANTS + TypeOK + SnapshotIsolation +\* Serialization + +PROPERTIES + Termination \ No newline at end of file diff --git a/specifications/KeyValueStore/MCKVsnap.tla b/specifications/KeyValueStore/MCKVsnap.tla new file mode 100644 index 00000000..4f672b21 --- /dev/null +++ b/specifications/KeyValueStore/MCKVsnap.tla @@ -0,0 +1,5 @@ +---- MODULE MCKVsnap ---- +EXTENDS KVsnap, TLC +TxIdSymmetric == Permutations(TxId) +==== + diff --git a/specifications/KeyValueStore/README.md b/specifications/KeyValueStore/README.md new file mode 100644 index 00000000..f7e03efa --- /dev/null +++ b/specifications/KeyValueStore/README.md @@ -0,0 +1,21 @@ +This repo contains TLA+ specifications of simple key-value store exhibiting snapshot algorithm. + +## TLA+ model +Andrew Helwer contributed the following: ++ `KeyValueStore.tla` has the TLA+ specs for the key-value store with snapshot isolation ++ `MCKS.tla` is the file to use for TLC model checking ++ `MCKVS*.cfg` are alternative config files to use for TLC checking + + +## PlusCal model +Murat Demirbas wrote a PlusCal version of the key-value store with snapshot isolation. He also instantiated the `ClientCentric.tla` (from Tim Soethout's work) to be able to properly check the key-value store for snapshot isolation semantics. ++ `KVsnap.tla` is the Pluscal model for the key-value store ++ `MCKVsnap.tla` is the file to use for TLC model checking ++ `MCKVsnap.cfg` is the corresponding config file for model checking (with this config, model checking completes under a minute; it is possible to add another key and model check) + +If you uncomment the Serialization invariant in `KVsnap.tla`, and `MCKVsnap.cfg`, you can see a counterexample of how this snapshot-isolation key-value store violates serializability. + +## Model checking with VSCode TLA+ plugin ++ Make sure TLA+ plugin is installed in VSCode ++ Open the .cfg file you are interested in checking in VSCode ++ Get the VSCode panel (Option+X on Mac), and choose "TLA+: Check Model with TLC") \ No newline at end of file diff --git a/specifications/KeyValueStore/Util.tla b/specifications/KeyValueStore/Util.tla new file mode 100644 index 00000000..b4012922 --- /dev/null +++ b/specifications/KeyValueStore/Util.tla @@ -0,0 +1,45 @@ +-------------------------------- MODULE Util -------------------------------- +EXTENDS Sequences, Functions, Naturals, TLC +\* Simple utility functions +intersects(a, b) == a \cap b # {} +max(s) == CHOOSE i \in s : (~\E j \in s : j > i) +min(s) == CHOOSE i \in s : (~\E j \in s : j < i) + +ReduceSet(op(_, _), set, base) == + LET iter[s \in SUBSET set] == + IF s = {} THEN base + ELSE LET x == CHOOSE x \in s: TRUE + IN op(x, iter[s \ {x}]) + IN iter[set] + +ReduceSeq(op(_, _), seq, acc) == FoldFunction(op, acc, seq) + +Index(seq, e) == CHOOSE i \in 1..Len(seq): seq[i] = e + +SeqToSet(s) == {s[i] : i \in DOMAIN s} +Last(seq) == seq[Len(seq)] +IsEmpty(seq) == Len(seq) = 0 +\* Remove all occurences of `elem` from `seq` +Remove(seq, elem) == SelectSeq(seq, LAMBDA e: e /= elem) + +\* Dual to UNION on intersect +INTERSECTION(setOfSets) == ReduceSet(\intersect, setOfSets, UNION setOfSets) + +\* Borrowed from Stephan Merz. TLA+ Case Study: A Resource Allocator. [Intern report] A04-R-101 || merz04a, 2004, 20 p. ffinria-00107809f +(* The set of permutations of a finite set, represented as sequences. *) +PermSeqs(S) == + LET perms[ss \in SUBSET S] == + IF ss = {} THEN { << >> } + ELSE LET ps == [ x \in ss |-> + { Append(sq,x) : sq \in perms[ss \ {x}] } ] + IN UNION { ps[x] : x \in ss } + IN perms[S] + +\* Helper to write "unit test" ASSUMES which print when false +test(lhs, rhs) == lhs /= rhs => Print(<>, FALSE) + + +============================================================================= +\* Modification History +\* Last modified Sun Aug 05 16:44:44 ET 2023 by murat +\* Created Tue Apr 28 16:43:24 CEST 2020 by tim