TLA REPL

tla_repl.py

#!/usr/bin/env python

# https://github.com/will62794/tlaplus_repl

import cmd
import os
import subprocess
import tempfile

TEMPLATE = """
------------------------- MODULE %s -------------------------
EXTENDS Naturals, Sequences, Bags, FiniteSets, TLC
ASSUME /\ PrintT("TLAREPL_START")
          /\ PrintT(%s)
          /\ PrintT("TLAREPL_END")
=============================================================
"""

TMP_SPEC_NAME = "Spec"
TLC_CMD = ["tlc"]

def prepare(e):
  tmp_dir = tempfile.mkdtemp()
  os.chdir(tmp_dir)

  with open(("%s.tla" % TMP_SPEC_NAME), "w") as f:
    f.write(TEMPLATE % (TMP_SPEC_NAME, e))

  with open("MC.cfg", "w") as f:
    f.write("")

def eval(e):
  cmd = TLC_CMD + ["-deadlock", "-config", "MC.cfg", ("%s.tla" % TMP_SPEC_NAME)]
  lines = subprocess.check_output(cmd).splitlines()

  begin = lines.index('"TLAREPL_START"') + 1
  end = len(lines) - 1 - lines[::-1].index('"TLAREPL_END"')

  return "\n".join(lines[begin:end])

class TLARepl(cmd.Cmd):
  intro = subprocess.check_output(TLC_CMD).splitlines()[0]
  prompt = "[TLA+] >>> "

  def default(self, e):
    try:
      prepare(e)
      print(eval(e))
    except Exception:
      print("error")
    return False

  def do_quit(self, e):
    return True

if __name__ == '__main__':
  TLARepl().cmdloop()