User Guide to Model Checking for Industrial Programmers with TLA+github.com/gshanemiller 1 pointscrubs3 months ago1 commentSaveHideCopy link On HNComments−scrubsOP3moIf 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.
Comments
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 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.