ProB REPL

The REPL of ProB

ProB provides various consoles, also called REPL (Read-Eval-Print-Loop). A REPL (Read-Eval-Print-Loop) or console can be used to evaluate formulas with ProB or issue other commands. ProB provides various REPLs, depending on which version of ProB you use:

The REPL in probcli can be started with the command -repl
The REPL in ProB Tcl/Tk is the Eval Console.
ProB2-UI also provides a console view

Below we describe the REPL of probcli, which is the most powerful. Some (but not all) of the commands are available in the other consoles as well.

Starting the REPL

You can start the REPL simply by typing:

probcli -repl

If you wish you can instruct probcli to also load and initialise a B machine and set other preferences before starting the REPL:

probcli MYFILE.mch -repl -p REPL_UNICODE TRUE -pref-group integer int32

Here we have loaded a B machine MYFILE.mch and set MININT/MAXINT for 32 bit systems. The preference -p REPL_UNICODE TRUE instructs the REPL to display the formula again using Unicode operators (warning: this can slow down certain terminal applications).

We also recommend you use the rlwrap tool available under Unix and Linux to start probcli, so that you have a command history:

rlwrap probcli -repl

Using the REPL

Every character following the >>> until the end of the line is typed by the user. The next line, starting with ⇝, shows the Unicode rendering of the ASCII expression or predicate typed by the user.

probcli -repl -p REPL_UNICODE TRUE
ProB Interactive Expression and Predicate Evaluator 
Type ":help" for more information.

Examples: see Sudoku Solved in the ProB REPL or Proving_Theorems_in_the_ProB_REPL.