What’s New

2023-08-02

Added topics Handling Unbound Models and Optimizing Model Checking.

2023-01-13

Added the Modelling Message Queues topic.

2022-11-11

Fixed various issues raised in Github, added a new operator example.

2022-07-25

Added an exercise directive, so I can start adding exercises to the core.

2022-07-08

Added the Standard Modules reference.

2022-06-30

Released beta!

Roadmap

• Core:

  • Exercises

  • Fixing whatever people find hard to understand

  • Some more diagrams

• Topics:

  • Refinement

  • Modeling ADTs

  • Community modules

  • Modeling legacy systems

  • Machine-world differences

  • Keeping a spec and a codebase in sync

  • Hyperproperties

  • :: syntax

• Examples:

  • Many

• Reference:

  • A troubleshooting page

  • LaTeX to ASCII chart

  • TLA+ and PlusCal Cheatsheets

• Misc:

  • PDF output for offline use

  • Panels for C-syntax pluscal

  • Popup footnotes