Probabilistic Modeling with PRISM

9 weeks ago by mpm

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

march 2018 by mpm

I assembled all of the available ‘industrial’ examples I knew about. They’re all beginner to moderate in complexity.

tla+
march 2018 by mpm

TLA+ in Practice and Theory

july 2017 by mpm

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

tla+
july 2017 by mpm

TLA+ Course Lecture: Introduction to TLA+

march 2017 by mpm

Introduction to TLA+ (Lamport video)

tla+
march 2017 by mpm

Learn TLA+

february 2017 by mpm

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!

tla+
february 2017 by mpm

Metadata: Modeling a Replicated Storage System in TLA+

january 2017 by mpm

I assigned the students to model Voldemort with client-side routing as their first project.

tla+
january 2017 by mpm