3 ms·
> How valuable is TLA+ for non-concurrent applications? My understanding is that TLA+ is for concurrent applications, but with a broad definition of "concurren
by Taikonerd 6y ago
> How valuable is TLA+ for non-concurrent applications?
My understanding is that TLA+ is for concurrent applications, but with a broad definition of "concurrent." For example, it could be...
* multiple hosts messaging each other
* multiple threads in one process sharing a data structure
* multiple API calls that all use the same Postgres DB
In other words, any sort of system where different actors can step on each others' toes.
- Jtsummers 6y agoThat's definitely the main use. But TLA+ can also be applied to single threaded specifications by encoding various invariants (pre/post conditions on entry and exit, loop invariants).
- flazzarino 6y agoYou define variables and code that changes the variables over time. TLA+ lets you observe variable states and assert constraints. The amount of concurrency is up to you, it works fine with a single process. Non-determinism might be a better thing to anchor the value to. For example in a deterministic "normal" programming environment, an if/then/else statement will execute only one out of two possible code paths. You have to run the code with a complementary condition to observe the other code path. In a non-deterministic environment like TLA+ both possible code paths are executed. You can observe state transitions in both possibilities. In a deterministic context the combinatorics of code paths can get out of hand quickly. Non-deterministically you have one set of assertions for all code paths, or patterns of paths.