/tla-examples

TLA+ example models

Primary LanguageTLAMIT LicenseMIT

TLA examples for the conference session Debugging Designs—Beyond the Rubber Duck held at Vincit Non-conference 2022

Copyright 2022 Erkki Seppälä erkki.seppala@vincit.fi and Jarno Malmari jarno.malmari@vincit.fi

License

This repository is licensed under the MIT license.

Examples

The DieHard example is copied from https://github.com/tlaplus/Examples/ and is licensed under the MIT license.

A simple example of a scenario involving a ball, a table, and a couch.

Demonstrates how to construct a set of two words using just three words!

An example about concurrent processes with PlusCal, with a bug when accessing the same variable from multiple threads without locking.

Aka "Enterprise directory downloader". An example where a client mirrors the contents of one directory on a remote server. Client and server and user interface exchange messages via a Channel, while the top-level Main module binds all the modules together.

To generate state diagram with tlsd:

tlc Main.tla -config tlsd.cfg | python3 -m tlsd