CREDITS
- Leslie Lamport for his work on TLA+... and lots of other things.
- Jess Frazelle for containers on the deskop.
WHAT DOES THIS DO?
This is a container that runs the TLA+ Toolbox.
WHY?
- TLA+ Toolbox requires Java.
- Who wants to install Java?
- TLA+ is neat... you should keep reading!
- Impress your friends by running a GUI application in Docker.
WHAT IS TLA+?
"TLA+ is especially well suited for writing high-level specifications of concurrent and distributed systems." (source)
HOW DO I LEARN MORE?
Visit The TLA Home Page.
HOW TO RUN IT?
- Make sure you're on a system running X.
- Disable X access control (don't do this on a public-facing machine):
$ xhost + $ cdto a path where you want to write some .tla files.$ docker run -d -v /tmp/.X11-unix:/tmp/.X11-unix -v `pwd`:`pwd` -e DISPLAY=$DISPLAY hackenfreude/tlatoolbox-1.5.2- You should see the TLA+ splash screen and eventually the TLA Toolbox.
- Use the TLA Toolbox menu: File/Open Spec/Add New Spec.
- Enter /container/host/path/you/were/in/when/starting/this/container/{foo}.tla as the root-module name. The specification name should auto-complete to {foo}. Click Finish.
- Have fun. Write some specifications. Close the TLA+ Toolbox when you're done, and the container will shut down. Your files will be in the path on the host where you started.
- Reenable X access control:
$ xhost -
WHAT JUST HAPPENED?
- Docker mounted the host's X socket in the continer as the container's X socket; this allows the container's GUI to pass back up to the host.
- Docker mounted the host's working directory in the container at the same path.
WHAT IF IT DOESN'T WORK?
Open an issue.