Bisimia is a browser-based local-first environment to write and model-check TLA+ specs.
I started working on this in January wanting to have a better environment to write TLA+ specs and model check them. I started out with running TLC via CheerpJ https://cheerpj.com/ (which I later on found out to be the approach taken by https://learning.tlapl.us/), however after many days and nights I've abandoned this for a few reasons, the most prominent of which is performance. Now we use GraalVM https://www.graalvm.org/ and some magic around it to achieve a median improvement of 22×, with speedups reaching nearly 70× compared to CheerpJ.
The goal here was to run the real TLC (and be bug-for-bug compatible) and not re-implement things (which is the approach taken for example by https://will62794.github.io/spectacle/).
Comments URL: https://news.ycombinator.com/item?id=50385004
Points: 2
# Comments: 0
