Hi, 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.
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 Leuschel PS: Here the log showing how the current REPL can be used for a simple TLA specification: $ rlwrap probcli clock.tla -init -repl Parsing file /Users/leuschel/TLA/Full_Clock/clock.tla Parsing file /var/folders/j4/cxrp94290tdg3mgpvg8yjfdc0000/T/Naturals.tla Semantic processing of module Naturals Semantic processing of module clock B-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 58 Executing probcli command: [cli_random_animate(58,true)] ALL OPERATIONS COVERED finished_random_animate(58,[runtime/20,total_runtime/20,walltime/20]) >>> (hours,minutes,seconds) _expression_ Value = ((0|->0)|->58) >>> -animate 2 Executing 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 = 1000 Existentially Quantified Predicate over h,m,s is TRUE Solution: h = 0 & m = 16 & s = 40 >>> h:0..23 & m:0..59 & s: 0..59 & h*60*60+m*60+s = 10000 Existentially Quantified Predicate over h,m,s is TRUE Solution: h = 2 & m = 46 & s = 40 >>> :stats % Type: pred % Eval Time: 0 ms (0 ms walltime) $ more clock.tla ---------------------- MODULE clock ---------------------- EXTENDS Naturals VARIABLES hours, minutes, seconds Init == 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) % 60 Clock == Init /\ [][Next]_{seconds} -------------------------------------------------------------- THEOREM Clock => []Init ============================================================== |