ProB REPL - Revision history

Michael Leuschel at 10:31, 27 February 2025

2025-02-27T10:31:50Z

← Older revision		Revision as of 10:31, 27 February 2025
Line 52:		Line 52:
	#file=MYFILE to evaluate the formula in MYFILE		#file=MYFILE to evaluate the formula in MYFILE
	@INVARIANT to evaluate or obtain invariant predicate		@INVARIANT to evaluate or obtain invariant predicate
	@PROPERTIES, @GUARD-OpName ditto for properties and guards		@PROPERTIES, @GUARD-OpName ditto for properties and guards
	:b or :b Prefix to browse the available identifiers		:b or :b Prefix to browse the available identifiers
	:t E to get the type of an expression		:t E to get the type of an expression

Michael Leuschel at 10:31, 27 February 2025

2025-02-27T10:31:40Z

← Older revision		Revision as of 10:31, 27 February 2025
Line 51:		Line 51:
	:unlet x to un-define a local variable		:unlet x to un-define a local variable
	#file=MYFILE to evaluate the formula in MYFILE		#file=MYFILE to evaluate the formula in MYFILE
			@INVARIANT to evaluate or obtain invariant predicate
			@PROPERTIES, @GUARD-OpName ditto for properties and guards
	:b or :b Prefix to browse the available identifiers		:b or :b Prefix to browse the available identifiers
	:t E to get the type of an expression		:t E to get the type of an expression

Michael Leuschel at 11:53, 26 February 2025

2025-02-26T11:53:52Z

← Older revision		Revision as of 11:53, 26 February 2025
Line 49:		Line 49:
	You can also type one of the following commands:		You can also type one of the following commands:
	:let x = E to define a new local variable x		:let x = E to define a new local variable x
			:unlet x to un-define a local variable
	#file=MYFILE to evaluate the formula in MYFILE		#file=MYFILE to evaluate the formula in MYFILE
	:b or :b Prefix to browse the available identifiers		:b or :b Prefix to browse the available identifiers

Michael Leuschel: /* The REPL of ProB */

2025-02-08T07:49:55Z

The REPL of ProB

← Older revision		Revision as of 07:49, 8 February 2025
Line 7:		Line 7:
	* The REPL in ProB Tcl/Tk is the [[Eval_Console\|Eval Console]].		* The REPL in ProB Tcl/Tk is the [[Eval_Console\|Eval Console]].
	* ProB2-UI also provides a console view		* ProB2-UI also provides a console view
			* Inside the [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel ProB kernel for Jupyter]

	Below we describe the REPL of [[Using_the_Command-Line_Version_of_ProB\|probcli]], which is the most powerful. Some (but not all) of the commands are available in the other consoles as well.		Below we describe the REPL of [[Using_the_Command-Line_Version_of_ProB\|probcli]], which is the most powerful. Some (but not all) of the commands are available in the other consoles as well.

Michael Leuschel: /* Using the REPL */

2025-02-08T07:48:19Z

Using the REPL

Michael Leuschel: /* Using the REPL */

2025-02-08T07:31:22Z

Using the REPL

@@ Line 34: / Line 34: @@
 === Using the REPL ===
   probcli -repl -p REPL_UNICODE TRUE
@@ Line 41: / Line 39: @@
   Type ":help" for more information.
 Examples: see  [[Sudoku Solved in the ProB REPL]] or [[Proving_Theorems_in_the_ProB_REPL]].

Michael Leuschel: /* The REPL of ProB */

2025-02-08T07:24:22Z

The REPL of ProB

@@ Line 4: / Line 4: @@
 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 <tt>-repl</tt>
+* The REPL in [[Using_the_Command-Line_Version_of_ProB|probcli]] can be started with the command <tt>-repl</tt>
 * The REPL in ProB Tcl/Tk is the  [[Eval_Console|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.
+Below we describe the REPL of [[Using_the_Command-Line_Version_of_ProB|probcli]], which is the most powerful. Some (but not all) of the commands are available in the other consoles as well.
 Examples: see  [[Sudoku Solved in the ProB REPL]] or [[Proving_Theorems_in_the_ProB_REPL]].

Michael Leuschel: Created page with "== 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 th..."

2025-02-08T07:17:24Z

Created page with "== 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 <tt>-repl</tt> * The REPL in ProB Tcl/Tk is the Eval Console. * ProB2-UI also provides a console view Below we describe th..."

New page

== 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 <tt>-repl</tt>
* The REPL in ProB Tcl/Tk is the [[Eval_Console|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.

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

← Older revision		Revision as of 07:48, 8 February 2025
Line 50:		Line 50:
	#file=MYFILE to evaluate the formula in MYFILE		#file=MYFILE to evaluate the formula in MYFILE
	:b or :b Prefix to browse the available identifiers		:b or :b Prefix to browse the available identifiers
	:t E to get the type of an expression ~~and~~ :r to reload the machine		: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)		:show to display the last result as a table (if possible)
	:list CAT to display information with CAT : {files,variables,help,...}		:list CAT to display information with CAT : {files,variables,help,...}
	:* P to display constants/variables containing pattern P		:* P to display constants/variables containing pattern P
	:core Pred to compute the unsat core for Pred		:core Pred to compute the unsat core for Pred
	:u to compute the unsat core for last ~~evaulated~~ result		:u to compute the unsat core for last evaluated result
	:stats to print the type and evaluation time for last query		:stats to print the type and evaluation time for last query
	-PROBCLIARGS to pass command-line probcli arguments to the REPL		-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.		:ctl F or :ltl F to check a CTL or LTL formula.
	:f F to find a state satisfying LTL atomic property.		: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.		:exec S to execute an operation or substitution S.
	:replay FILE to replay a file of commands.		:replay FILE to replay a file of commands.
Line 71:		Line 74:
	:help CMD to obtain more help about a command.		:help CMD to obtain more help about a command.
	:state, :statespace, :states,		:state, :statespace, :states,
	:machine, :files, :source, :orgin,		:machine, :files, :source, :orgin, :machine-stats,
			:apropos, :hbrowse, :abstract_constants, :det_check_constants,
	:dot, :dotty, :sfdp, :trim, :comp - use :help CMD for more info		:dot, :dotty, :sfdp, :trim, :comp - use :help CMD for more info
	:syntax to show a summary of the B syntax accepted by the REPL		:syntax to show a summary of the B syntax accepted by the REPL