model-checking

Recent versions of TLC come with a (simple) REPL. It would be great if the REPL was integrated into the VSCode terminal.

markus@avocado:/opt/toolbox$ java -cp tla2tools.jar tlc2.REPL
Welcome to the TLA+ REPL!
TLC2 Version 2.16 of Day Month 20??
Enter a constant-level TLA+ expression.
(tla+) TRUE
TRUE

Multiple operations on programs visit all expressions either to modify or to analyse them.
This yields a series of awkward code duplications that could be reduced by adding a visitor pattern.