ProB REPL: Difference between revisions

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
• Inside the ProB kernel for Jupyter

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

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

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.

>>> :help
ProB Interactive Expression and Predicate Evaluator 
Type a valid B expressions or predicates, followed by RETURN or ENTER.
You can spread input over multiple lines by ending lines with "\".
You can also type one of the following commands: 
    :let x = E to define a new local variable x
    #file=MYFILE to evaluate the formula in MYFILE
    :b or :b Prefix to browse the available identifiers
    :t E to get the type of an expression
    :r to reload the machine
    :show to display the last result as a table (if possible)
    :list CAT to display information with CAT : {files,variables,help,...}
    :* P to display constants/variables containing pattern P
    :core Pred to compute the unsat core for Pred
    :u to compute the unsat core for last evaluated result
    :stats to print the type and evaluation time for last query
    -PROBCLIARGS to pass command-line probcli arguments to the REPL
      (e.g., -v to switch to verbose mode or -p PREF VAL to set a preference)
    :ctl F or :ltl F to check a CTL or LTL formula.
    :f F to find a state satisfying LTL atomic property.
    :find-value PAT to find a value in current state matching PAT.
    :exec S to execute an operation or substitution S.
    :replay FILE to replay a file of commands.
    :z3 P, :cvc4 P, :kodkod P to solve predicate P using alternate solver
    :forall P to prove predicate P as universally quantified with default solver
    :prove P to prove predicate P using ProB's own WD prover
    :print P to pretty print predicate in a nested fashion
    :min P, :max P to find a minimal/maximal model for predicate P or %x.(P|E)
    :prefs to print current value of preferences
    :reset to reset the state space of the animator.
    :help CMD to obtain more help about a command.
    :state, :statespace, :states,
            :machine, :files, :source, :orgin, :machine-stats,
            :apropos, :hbrowse, :abstract_constants, :det_check_constants,
            :dot, :dotty, :sfdp, :trim, :comp - use :help CMD for more info
    :syntax  to show a summary of the B syntax accepted by the REPL
    :q to exit.
>>> 

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