Announcing PlusPy: Python interpreter for TLA+ specifications

[Robbert Van Renesse]

While Cornell was closed down for a few weeks, I wrote a "TLA+ executor" in Python.  It handles a similar subset of specifications that are handled by the TLC model checker.  However, instead of exploring the entire state space, PlusPy just tries to find one behavior consistent with the specification.  If high performance is not a requirement, then, rather than having to manually implement a TLA+ specification, you may be able to run it directly using PlusPy.  PlusPy supports multi-threading so you may be able to run concurrent TLA+ or PlusCal algorithms with PlusPy.  You can, for example, run the Peterson algorithm with actual threads.  PlusPy also has support for distribution and messaging so you may be able to run a consensus algorithm using PlusPy.  PlusPy comes with examples of each.  Using PlusPy TLA+ modules can invoke Python code and vice versa.

If you're interested, try it out.  Clone it from https://github.com/tlaplus/PlusPy.  All you need is Python3 to run it.  Just know that it is brand-new software and likely to have lots of issues, but I would much appreciate your questions and comments.

As a small preview, here's the output of running the HourClock spec from Leslie's book:

$ ./pluspy -c10 HourClock

Initial context: [ hr |-> 6 ]

Next state: 0 [ hr |-> 7 ]

Next state: 1 [ hr |-> 8 ]

Next state: 2 [ hr |-> 9 ]

Next state: 3 [ hr |-> 10 ]

Next state: 4 [ hr |-> 11 ]

Next state: 5 [ hr |-> 12 ]

Next state: 6 [ hr |-> 1 ]

Next state: 7 [ hr |-> 2 ]

Next state: 8 [ hr |-> 3 ]

Next state: 9 [ hr |-> 4 ]

$