5 ms·
TLA+ is originally mainly meant to check for concurrency bugs, so the possibility of parallel threads is kind of in its core DNA. The name "process" might also
by loup-vaillant 8y ago
TLA+ is originally mainly meant to check for concurrency bugs, so the possibility of parallel threads is kind of in its core DNA. The name "process" might also give a hint that parallel threads are indeed possible.
I don't know how, but I expect you can indeed model actual transactions.
- hwayne 8y agoDepends on what you mean by "actual transaction". Every TLA+ behavior is describable as a series of "next-states", where _usually_ (not always, but _usually_) one action is true. In which case you'd model the transaction by determining the changes that the overall transaction makes and then declaring them all as part of a single action.