mpm + tla+   6

Probabilistic Modeling with PRISM
TLA and Alloy are good for absolutes. You can say “there exists an error in this design”. But you can’t express statistical properties, like “this should take an average of less than 10 minutes” or “it is more likely this recovers than crashes.” Nor can you assign weights to actions, like “this has an 80% chance of continuing and a 20% chance of failing.” For that, we need probabilistic modeling (PM). PRISM is one such modeling language, and comes with some really powerful tools to inspect probabilities. But there’s a fundamental tradeoff in modeling: the more powerful the checker, the less expressive the language. And to get such a powerful checker, PRISM has to make some serious expressivity tradeoffs.
tla+  modeling 
9 weeks ago by mpm
List of TLA+ Examples
I assembled all of the available ‘industrial’ examples I knew about. They’re all beginner to moderate in complexity.
march 2018 by mpm
TLA+ in Practice and Theory
This series is neither necessary nor sufficient for putting TLA+ to good use, but I think it is both necessary and sufficient for understanding it
july 2017 by mpm
TLA+ Course Lecture: Introduction to TLA+
Introduction to TLA+ (Lamport video)
march 2017 by mpm
Learn TLA+
This is intended to be a guide to TLA+, aimed at making it practical for day-to-day startup work. It assumes you have some experience with programming (otherwise this will be nonsensical) and familiarity with unit testing (otherwise that’s probably worth learning first). If you’ve got both of those, let’s learn some TLA!
february 2017 by mpm
Metadata: Modeling a Replicated Storage System in TLA+
I assigned the students to model Voldemort with client-side routing as their first project.
january 2017 by mpm

related tags

modeling  tla+ 

Copy this bookmark: