Just another question:For multiply keys transaction access, we just wrapped it's ops as an action which is atomic or put in a label if using pluscal. In my humble knowledge, this way will impl multiply keys transaction atomic. But no any concurrency control, and no any concurrency the txns can use, so the performance will low. Am i right?For some spec which use the kv/db txn api, Why can we use this way to model the kv/db txn api?在2022年9月8日星期四 UTC+8 10:45:24<保建国> 写道：I think OpenTx(t),Add(t, k, v),Update(t, k, v),Remove(t, k),RollbackTx(t),CloseTx(t) in the example are the txn apis, In my spec i can instant the example spec and use those api.在2022年9月7日星期三 UTC+8 20:34:30<andrew...@xxxxxxxxx> 写道：If you want functionality like snapshot isolation for each transaction you'll need to write the logic in TLA+ yourself. There is an example of a key-value store with snapshot isolation on the wikipedia article: https://en.wikipedia.org/wiki/TLA%2B#ExamplesAndrewOn Tuesday, September 6, 2022 at 10:53:51 PM UTC-4 ine...@xxxxxxxxx wrote:Such as we write an distributed app spec which need access db.For multiply keys transaction access, we just wrapped it's ops as an action or put in a label if using pluscal. Is is enough ? In my humble knowledge, this way just enable single key linearizablity and transaction atomic. but no transaction isolation, am i right?Always we may need external consistency or strict Serializable , or serializable , even snapshot isolation level.So how do we use this api in an spec?I see too many spec impl transaction to verfiy the consistency or the atomic. But What is the transaction api it expose? such as beginop, keyops, commit/abort?