Re:TLA+
by flazzarino on Monday March 08, 2021 @02:31PM
(#26390387)
You 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.
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.