[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] REPL enhancements

Hi, I'm very excited to see that a REPL has been added last year.  However it doesn't appear to have been developed much since then beyond the basic _expression_ evaluation functionality in the initial import.

Would I be stepping on any toes if I started working on some enhanced functionality for it?  I have a few ideas I've been kicking around in a hacky shell-script-based REPL I made a few years ago that I'd be interested in porting over.  Namely:

1) The ability to define operators and instantiate modules.

2) The ability to declare variables, and initialize and update them (one iteration) via a specified predicate and user input to resolve nondeterminism (as with TLCExt!PickSuccessor).

3) The ability to define constants (same as in a TLC config file) to support model values, and extending modules which declare constants.

4) The ability to modify, list, and save to file what's been defined in the session.

I think these enhancements would help make the REPL a really useful tool for those learning the language, or those wanting to test and explore functionality of modules they are developing.

- Chris

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7e444bd5-9dc5-441e-81b0-1ed772459c48n%40googlegroups.com.