User Guide to Model Checking for Industrial Programmers with TLA+ (github.com) 1 points by scrubs 1mo ago ↗ HN
[–] scrubs 1mo ago ↗ If you interested in formal model checking using TLA+, this may of interest you. In this github repository https://github.com/gshanemiller/tla-examples find,- tla.pdf - numerous examplesThe PDF describes model checking in TLA working through minimal background (fairness, model state etc.), application in TLA, two non-trivial models, and two appendices with reference background on TLA, and its procedural cousin PlusCal.
1 comment
[ 2.6 ms ] story [ 11.0 ms ] thread- tla.pdf - numerous examples
The PDF describes model checking in TLA working through minimal background (fairness, model state etc.), application in TLA, two non-trivial models, and two appendices with reference background on TLA, and its procedural cousin PlusCal.