Hi,I find this discussion very interesting and also relevant for other formal methods communities and tools.We have also added a REPL to ProB some time ago, but it is far from complete (e.g., one can introduce local variables using let but one cannot construct new specifications inside the REPL yet).As such, I am very interested in feature requests and usage scenarios as well.On 23 Nov 2014, at 23:42, Leslie Lamport wrote:I asked for explicit scenarios that you would like implemented--thatis, exactly what keystrokes and button pushes you would perform toachieve the desired tasks.  You can find one particular scenario using the current ProB REPL here:I find the REPL very useful for debugging models and also for developing certain parts of a model from scratch.The REPL is also very useful to test the kernel of our tool (there is actually a “hidden” command to add the last _expression_/predicate as a unit test for ProB).Finally, for teaching, I find the REPL very handy to explain the various B operators during lectures (but maybe the students are of a different opinion ;-)).If there is interest from the TLA community, one could consider using this REPL as a starting point for a REPL for TLA.Indeed, probcli can already load TLA specifications via SANY (see log below). However, beware of the following: - our translator from TLA to B has certain limitations (http://www.stups.uni-duesseldorf.de/ProB/index.php5/TLA). - one currently has to use B syntax in the REPL; this could be remedied with moderate effort by using SANY in place of our B parser. - the output is printed in B syntax; this would take a bit more effort to adapt for TLA (storing TLA type information in the abstract syntax tree and adapting the pretty-printer), - one could call TLC from within the REPL, we already do so for model checking (http://www.stups.uni-duesseldorf.de/ProB/index.php5/TLC). For evaluation, there is the issue of JVM startup time, already discussed in previous messages of this thread.Best regards,Michael LeuschelPS: Here the log showing how the current REPL can be used for a simple TLA specification:$rlwrap probcli clock.tla -init -replParsing file /Users/leuschel/TLA/Full_Clock/clock.tlaParsing file /var/folders/j4/cxrp94290tdg3mgpvg8yjfdc0000/T/Naturals.tlaSemantic processing of module NaturalsSemantic processing of module clockB-Machine /Users/leuschel/TLA/Full_Clock/clock_tla.mch created./Users/leuschel/TLA/Full_Clock/clock.prob created.ProB Interactive _expression_ and Predicate Evaluator Type ":help" for more information.>>> (hours,minutes,seconds)_expression_ Value = ((0|->0)|->0)>>> -animate 58Executing probcli command: [cli_random_animate(58,true)]ALL OPERATIONS COVEREDfinished_random_animate(58,[runtime/20,total_runtime/20,walltime/20])>>> (hours,minutes,seconds)_expression_ Value = ((0|->0)|->58)>>> -animate 2Executing probcli command: [cli_random_animate(2,true)]finished_random_animate(2,[runtime/10,total_runtime/10,walltime/0])>>> (hours,minutes,seconds)_expression_ Value = ((0|->1)|->0)>>> card({h,m,s| h:0..23 & m:0..59 & s:0..59})_expression_ Value = 86400>>> h:0..23 & m:0..59 & s: 0..59 & h*60*60+m*60+s = 1000Existentially Quantified Predicate over h,m,s is TRUESolution: h = 0 & m = 16 & s = 40>>> h:0..23 & m:0..59 & s: 0..59 & h*60*60+m*60+s = 10000Existentially Quantified Predicate over h,m,s is TRUESolution: h = 2 & m = 46 & s = 40>>> :stats% Type: pred% Eval Time: 0 ms (0 ms walltime)$ more clock.tla---------------------- MODULE clock ----------------------EXTENDS NaturalsVARIABLES  hours,  minutes,  secondsInit  ==    hours \in (0 .. 23)               /\ minutes \in (0 .. 59)               /\ seconds \in (0 .. 59) Next  ==    hours' = (IF minutes # 59 THEN hours ELSE (hours + 1) % 24)               /\ minutes' = (IF seconds # 59 THEN minutes ELSE (minutes + 1) % 60)               /\ seconds' = (seconds + 1) % 60Clock  ==  Init /\ [][Next]_{seconds}--------------------------------------------------------------THEOREM  Clock => []Init==============================================================