Home

Here are some tips for using tla-tools.

Set up compilation

I add mrc-tla-mode to tla-pcal-mode-hook, to set up compile commands and auto revert after PlusCal translation.

(defun mrc-tla-mode ()
  (interactive)
  (make-local-variable 'compile-command)
  (let ((tlc-command "/usr/local/bin/tlc")
	(pcal-command "/usr/local/bin/pcal")
	(module (file-name-base (buffer-file-name))))
    (setq compile-command (concat
			   pcal-command " " module
			   " && "
			   tlc-command " " module)))
  (local-set-key (kbd "C-c C-c") #'recompile)
  (auto-revert-mode t)) ;; enable auto-revert because pcal modifies the file

Evaluating expressions

The TLA+ Toolbox has this neat feature to evaluate expressions. It works by creating files MC.tla/MC.cfg, documented here, and adding the expression and a PrintT there. The code that generates MC.tla/MC.cfg is here, and it adds stuff like Init/Next as needed to "override" the source TLA+ module (I think -- still figuring this out!) There's some gotchas here which I don't yet understand, but here's a basic MC.tla/MC.cfg which works for me:

MC.tla:

---- MODULE MC ----

EXTENDS wire, TLC

VARIABLE var_unique

expr_unique == \A x \in 1..10: x > 5

ASSUME PrintT(<<"unique", expr_unique>>)

init_unique == FALSE/\var_unique
next_unique == FALSE/\var_unique

====

MC.cfg:

INIT init_unique
NEXT next_unique

Gosh it would be nice if there was a nice way of doing this in Emacs -- something like ielm, or eval-print-last-sexp, that could auto generate MC.tla/MC.cfg, parse back in the output of PrintT, and display it nicely? What about a posframe that appeared next to the expression to display its result?! Could go full Bret Victor on this!