Using the Command-Line Version of ProB - Revision history

Michael Leuschel: /* -cache */

2026-01-29T14:48:43Z

-cache

← Older revision		Revision as of 14:48, 29 January 2026
Line 621:		Line 621:

	Note: this command can also be used when starting up the ProB Tcl/Tk version.		Note: this command can also be used when starting up the ProB Tcl/Tk version.

			Note: the variation -ccache will create the directory if it does not exist.
			The command -show_cache and -show_cache_verbose can be used to display the cache contents.
			The command -cache_statistics provides statistics about the re-use of the cache.
			The commands -clear_cache and -clear_cache_for MACHINE can be used to force clearing the caching.

	=== -logxml <LogFile> ===		=== -logxml <LogFile> ===

2025-12-24T07:30:49Z

--timeout

← Older revision		Revision as of 07:30, 24 December 2025
Line 132:		Line 132:

	=== --timeout <N> ===		=== --timeout <N> ===

			Deprecated, please use --global-time-out command instead.

			=== --global-time-out <N> ===

	Description		Description
Line 143:		Line 147:
	Example		Example

	probcli my.mch -~~timeout~~ 10000		probcli my.mch -global_timeout 10000

	=== -t ===		=== -t ===

2025-12-24T07:28:31Z

-ref_check

← Older revision		Revision as of 07:28, 24 December 2025
Line 895:		Line 895:

	{\| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"		{\| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
	\| refinement check against previous saved state space using ~~provide~~		\| refinement check against previous saved state space (e.g. using -save) with particular failure/trace/divergence model
	\|}		\|}

	MODE is one of F, FD, T, R, RD, V, VD.		MODE is one of F, FD, T, R, RD, SF, V.
			Meaning of mode: F: Failures, FD: Failure-Divergences, R: Refusals, RD: Refusals-Divergences, SF: Singleton-Failures, T: Traces, V: Revival.
	Default used by -refchck command above is T (traces model).		Default used by -refchck command above is T (traces model).

2025-12-24T07:24:00Z

-refchk

← Older revision		Revision as of 07:24, 24 December 2025
Line 883:		Line 883:

	{\| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"		{\| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
	\| refinement check against previous saved state space		\| refinement check against previous saved state space (e.g. using -save)
	\|}		\|}

2025-12-24T07:23:36Z

-save

← Older revision		Revision as of 07:23, 24 December 2025
Line 876:		Line 876:
	Example		Example

	probcli my.mch ...		probcli my.mch --model_check -save my_saved.P

	=== -refchk <FILE> ===		=== -refchk <FILE> ===

2025-12-24T07:22:31Z

-refchk

@@ Line 888: / Line 888: @@
 Example
-  probcli my.mch ...
+  probcli my.mch -refchk abs_saved.P
 === -mcm_tests <Depth> <MaxStates> <EndPredicate> <FILE> ===

2025-12-23T15:56:55Z

-animate

← Older revision		Revision as of 15:56, 23 December 2025
Line 312:		Line 312:

	probcli my.mch -animate 100		probcli my.mch -animate 100

			Variations
			-animate_all : animate until deadlock reached
			-animate_until_ltl P : animate until LTL property holds on trace
			-animate_until_ltl_state_property P : animate until current state satisifes LTL state property

	=== -execute <Nr>===		=== -execute <Nr>===

2025-12-23T11:17:53Z

-rule_report

@@ Line 970: / Line 970: @@
 DEFINITION (which also works in ProB2-UI).
-=== -rule_report <File>===
+=== -rule_report <File> ===
 Description
@@ Line 983: / Line 983: @@
   probcli myrules.rmch -execute_all -rule_report my_report.html
 == Environment Variables ==

2025-12-23T11:12:19Z

-csp-guide

← Older revision		Revision as of 11:12, 23 December 2025
Line 967:		Line 967:
	Use the CSP File '''File''' to guide the B Machine ("CSP\|\|B").		Use the CSP File '''File''' to guide the B Machine ("CSP\|\|B").
	(This feature is included since version 1.3.5-beta7.)		(This feature is included since version 1.3.5-beta7.)
			As of version 1.15.1 you can also specify a <tt>CSP_GUIDE_FILE</tt>
			DEFINITION (which also works in ProB2-UI).

	=== -rule_report <File>===		=== -rule_report <File>===

2025-12-23T11:11:28Z

-trace_replay

← Older revision		Revision as of 11:11, 23 December 2025
Line 162:		Line 162:

	{\| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"		{\| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
	\| ~~KIND is either~~ json, prolog, B~~. The old ProB format is prolog. The trace files generated by ProB2-UI are json (with .prob2trace extension~~)~~. The B format consists of a sequence of B operation calls~~.		\| Replay a trace file in the given format (json,prolog,B).
	\|}		\|}

			KIND is either json, prolog, B. The old ProB format is prolog. The trace files generated by ProB2-UI are json (with .prob2trace extension). The B format consists of a sequence of B operation calls.
	Example		Example