3 ms·
There are excellent probabilistic extensions to temporal logic out there that are very useful to uncover subtle performance bugs in protocol specifications, see
by nextos 10mo ago
There are excellent probabilistic extensions to temporal logic out there that are very useful to uncover subtle performance bugs in protocol specifications, see e.g. what PRISM [1] and Storm [2] implement. That is not within the scope of TLA+.
Formal methods are really broad, ranging from lightweight type systems to theorem proving. Some techniques are fantastic for one type of problem but fail at others. This is quite natural, the same thing happens with different programming paradigms.
For example, what is adequate for a hard real-time system (timed automata) is useless for a typical CRUD application.
[1] https://www.prismmodelchecker.org https://www.prismmodelchecker.org
[2] https://www.stormchecker.org https://www.stormchecker.org
- hwayne 10mo agoI really do wish that PRISM can one day add some quality of life features like "strings" and "functions" (Then again, AIUI it's basically a thin wrapper over stochastic matrices, so maybe that's asking too much...)