Re: TLA+ REPL

[frank...@xxxxxxxxx]

I like the code. I think you need to mention that the code only works under the Python 2.7. 


On Monday, January 15, 2018 at 2:26:29 PM UTC-5, William Schultz wrote:
> Hello,
> 
> For anyone who might be interested, I created a simple version of a TLA+ REPL using Python and the TLC model checker, that provides an interactive way to evaluate TLA+ expressions. Right now, it is a bit slow, since it starts up a new TLC instance to evaluate every new expression, but I find that even with a lag of ~1 second per expression evaluation, the speed of the feedback loop for testing out TLA+ expressions is much better than what I can do with the existing Toolbox features. Also, it does not support "persistence" yet. That is, every expression is evaluated in complete isolation, so you cannot define things and use them later on in a REPL sessions. 
> 
> 
> Even with these caveats, I have found it to be quite a useful little tool for experimentation and debugging. Often I find myself forgetting a subtle nuance of how to express something and it would be nice to have a quick way to test things out. If anyone has feedback or suggestions, I would welcome them. I hope that this tool might of use to others who are learning TLA+ or writing larger specifications and want something to aid their development workflow.
> 
> 
> You can clone the REPL from the Github link below. It only requires Python to run. It includes an automated setup script that will download the TLA+ tools for you if you don't already have them installed.
> 
> 
> Link: https://github.com/will62794/tlaplus_repl
> 
> 
> 
> 
> 
> Will
> 
> 
> 
> 
>