[tlaplus] How do we use the transaction api in spec？

[保建国 <inevity@xxxxxxxxx>]

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?

 

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/cc943fe1-e1fc-42c9-b65e-57eae30579f8n%40googlegroups.com.