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

Re: [tlaplus] Some user feedback


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 <tlapl...@xxxxxxxxx> wrote:

I asked for explicit scenarios that you would like implemented--that
is, exactly what keystrokes and button pushes you would perform to
achieve 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 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 = 

>>> -animate 58
Executing probcli command: [cli_random_animate(58,true)]



>>> (hours,minutes,seconds)
_expression_ Value = 

>>> -animate 2
Executing probcli command: [cli_random_animate(2,true)]
>>> (hours,minutes,seconds)
_expression_ Value = 

>>> card({h,m,s| h:0..23 & m:0..59 & s:0..59})
_expression_ Value = 

>>> 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
       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
       h = 2 &
       m = 46 &
       s = 40
>>> :stats
% Type: pred
% Eval Time: 0 ms (0 ms walltime)

$ more clock.tla
---------------------- MODULE clock ----------------------
EXTENDS Naturals
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