Using ProB with Atelier B - Revision history

Michael Leuschel: /* Extra Features of ProB */

2026-01-30T10:59:22Z

Extra Features of ProB

← Older revision		Revision as of 10:59, 30 January 2026
Line 92:		Line 92:

	* DEFINITIONS: the definitions and its arguments are checked by ProB. We believe this to be an important feature for a formal method language. However, as such, every DEFINITION must be either a predicate, an expression or a substitution. You '''cannot''' use, for example, lists of identifiers as a definition. Also, for the moment, the arguments to DEFINITIONS have to be expressions. Finally, when replacing DEFINITIONS the associativity is not changed. E.g., with <tt>PLUS(x,y) == x+y</tt>, the expression <tt>PLUS(2,3)*10</tt> will evaluate to 50 (and not to 32 as with Atelier-B). Also, ProB will generate a warning when variable capture may occur. In Version 1.16.0 of ProB there is the new preference HYGIENIC_DEFINITIONS. By setting it to TRUE you avoid most of the variable capture problems (ProB will automatically introduce a LET for parameters if necessary to avoid code duplication and variable capture).		* DEFINITIONS: the definitions and its arguments are checked by ProB. We believe this to be an important feature for a formal method language. However, as such, every DEFINITION must be either a predicate, an expression or a substitution. You '''cannot''' use, for example, lists of identifiers as a definition. Also, for the moment, the arguments to DEFINITIONS have to be expressions. Finally, when replacing DEFINITIONS the associativity is not changed. E.g., with <tt>PLUS(x,y) == x+y</tt>, the expression <tt>PLUS(2,3)*10</tt> will evaluate to 50 (and not to 32 as with Atelier-B). Also, ProB will generate a warning when variable capture may occur. In Version 1.16.0 of ProB there is the new preference HYGIENIC_DEFINITIONS. By setting it to TRUE you avoid most of the variable capture problems (ProB will automatically introduce a LET for parameters if necessary to avoid code duplication and variable capture).
			* In version 1.16.0 ProB will support EXPRESSIONS and PREDICATES sections as a hygienic replacement of DEFINITIONS

	* for a LET substitution, Atelier-B does not allow introduced identifiers to be used in the right-hand side of equations; ProB allows <tt>LET x,y BE x=2 & y=x*x IN ... END</tt> but only if the preference <tt>ALLOW_COMPLEX_LETS</tt> is set to TRUE.		* for a LET substitution, Atelier-B does not allow introduced identifiers to be used in the right-hand side of equations; ProB allows <tt>LET x,y BE x=2 & y=x*x IN ... END</tt> but only if the preference <tt>ALLOW_COMPLEX_LETS</tt> is set to TRUE.
Line 116:		Line 117:

	* ProB supports a special section [[Free_Types\|FREETYPES]] to define inductive data types		* ProB supports a special section [[Free_Types\|FREETYPES]] to define inductive data types

	* In version 1.16.0 ProB will support EXPRESSIONS and PREDICATES sections as a hygienic replacement of DEFINITIONS

	=== Differences ===		=== Differences ===

Michael Leuschel: /* Extra Features of ProB */

2026-01-30T10:59:00Z

Extra Features of ProB

← Older revision		Revision as of 10:59, 30 January 2026
Line 114:		Line 114:

	* ProB comes with several libraries of [[External_Functions \| external functions]] for string manipulations, mathematical functions, Hilbert's choice operator, etc.		* ProB comes with several libraries of [[External_Functions \| external functions]] for string manipulations, mathematical functions, Hilbert's choice operator, etc.

			* ProB supports a special section [[Free_Types\|FREETYPES]] to define inductive data types

			* In version 1.16.0 ProB will support EXPRESSIONS and PREDICATES sections as a hygienic replacement of DEFINITIONS

	=== Differences ===		=== Differences ===

Michael Leuschel: /* Extra Features of ProB */

2026-01-30T09:50:31Z

Extra Features of ProB

← Older revision		Revision as of 09:50, 30 January 2026
Line 111:		Line 111:
	* Some of the sequence operators can be applied to strings (unless you set the preference STRING_AS_SEQUENCE to FALSE): <tt>size</tt>, <tt>rev</tt>, <tt>^</tt>, <tt>conc</tt>		* Some of the sequence operators can be applied to strings (unless you set the preference STRING_AS_SEQUENCE to FALSE): <tt>size</tt>, <tt>rev</tt>, <tt>^</tt>, <tt>conc</tt>

	* As of version 1.12.1 you can write Event-B style set comprehensions with an extra expression like {x•x:1..10\|x*x}. You have to use the middle dot, the bullet (•) or a Unicode dot for this, though.		* As of version 1.12.1 you can write Event-B style set comprehensions with an extra expression like {x•x:1..10\|xx}. You have to use the middle dot, the bullet (•) or a Unicode dot for this, though. You can also put parentheses around the identifiers and use the regular dot: {(x).x:1..10\|xx}.

	* ProB comes with several libraries of [[External_Functions \| external functions]] for string manipulations, mathematical functions, Hilbert's choice operator, etc.		* ProB comes with several libraries of [[External_Functions \| external functions]] for string manipulations, mathematical functions, Hilbert's choice operator, etc.

Michael Leuschel: /* Extra Features of ProB */

2026-01-30T09:49:11Z

Extra Features of ProB

← Older revision		Revision as of 09:49, 30 January 2026
Line 91:		Line 91:
	** As of version 1.12.1 you can apply prj1 and prj2 without providing the type arguments. For example, you can write <tt>prj2(prj1(1\|->2\|->3))</tt> instead of <tt>prj2(INTEGER,INTEGER)(prj1(INTEGER*INTEGER,INTEGER)(1\|->2\|->3))</tt>.		** As of version 1.12.1 you can apply prj1 and prj2 without providing the type arguments. For example, you can write <tt>prj2(prj1(1\|->2\|->3))</tt> instead of <tt>prj2(INTEGER,INTEGER)(prj1(INTEGER*INTEGER,INTEGER)(1\|->2\|->3))</tt>.

	* DEFINITIONS: the definitions and its arguments are checked by ProB. We believe this to be an important feature for a formal method language. However, as such, every DEFINITION must be either a predicate, an expression or a substitution. You '''cannot''' use, for example, lists of identifiers as a definition. Also, for the moment, the arguments to DEFINITIONS have to be expressions. Finally, when replacing DEFINITIONS the associativity is not changed. E.g., with <tt>PLUS(x,y) == x+y</tt>, the expression <tt>PLUS(2,3)*10</tt> will evaluate to 50 (and not to 32 as with Atelier-B).		* DEFINITIONS: the definitions and its arguments are checked by ProB. We believe this to be an important feature for a formal method language. However, as such, every DEFINITION must be either a predicate, an expression or a substitution. You '''cannot''' use, for example, lists of identifiers as a definition. Also, for the moment, the arguments to DEFINITIONS have to be expressions. Finally, when replacing DEFINITIONS the associativity is not changed. E.g., with <tt>PLUS(x,y) == x+y</tt>, the expression <tt>PLUS(2,3)*10</tt> will evaluate to 50 (and not to 32 as with Atelier-B). Also, ProB will generate a warning when variable capture may occur. In Version 1.16.0 of ProB there is the new preference HYGIENIC_DEFINITIONS. By setting it to TRUE you avoid most of the variable capture problems (ProB will automatically introduce a LET for parameters if necessary to avoid code duplication and variable capture).

	* for a LET substitution, Atelier-B does not allow introduced identifiers to be used in the right-hand side of equations; ProB allows <tt>LET x,y BE x=2 & y=x*x IN ... END</tt> but only if the preference <tt>ALLOW_COMPLEX_LETS</tt> is set to TRUE.		* for a LET substitution, Atelier-B does not allow introduced identifiers to be used in the right-hand side of equations; ProB allows <tt>LET x,y BE x=2 & y=x*x IN ... END</tt> but only if the preference <tt>ALLOW_COMPLEX_LETS</tt> is set to TRUE.

Jan Gruteser: /* Atelier B Plugin */

2025-10-12T15:44:28Z

Atelier B Plugin

← Older revision		Revision as of 15:44, 12 October 2025
Line 10:		Line 10:

	Note: as the layout of Atelier-B's directories has changed, you need to use ProB 1.12.0 or newer for Atelier-B 4.7.1 or newer on macOS.		Note: as the layout of Atelier-B's directories has changed, you need to use ProB 1.12.0 or newer for Atelier-B 4.7.1 or newer on macOS.
	You can also create ~~the~~ the above file yourself.		You can also create the above file yourself.

	Here is a typical <tt>probtclk.etool</tt> file (where PathToProB depends on your location of the ProB installation folder containing the prob and probcli binaries):		Here is a typical <tt>probtclk.etool</tt> file (where PathToProB depends on your location of the ProB installation folder containing the prob and probcli binaries):

Michael Leuschel: /* Reflexive Closure */

2025-03-14T11:47:40Z

Reflexive Closure

← Older revision		Revision as of 11:47, 14 March 2025
Line 129:		Line 129:
	The previous definition was closure(X) = id(ran(X)\/dom(X)) \/ closure1(X) and		The previous definition was closure(X) = id(ran(X)\/dom(X)) \/ closure1(X) and
	the definition in Atelier-B was closure(X) = id(dom(X)) \/ closure1(X).		the definition in Atelier-B was closure(X) = id(dom(X)) \/ closure1(X).
	However, both were not compatible with the following law in the B-Book on page 169		However, both were not compatible with the following law in the B-Book on page 169:
	<pre> (r[a] <: a => closure(r)[a]=a)		<pre> r[a] <: a => closure(r)[a]=a
	</pre>		</pre>
	Take r = {1\|->2}, then r[{3}] <: {3}.		Take r = {1\|->2}, then r[{3}] <: {3}.

Michael Leuschel: /* Reflexive Closure */

2025-03-14T11:47:20Z

Reflexive Closure

← Older revision		Revision as of 11:47, 14 March 2025
Line 134:		Line 134:
	Take r = {1\|->2}, then r[{3}] <: {3}.		Take r = {1\|->2}, then r[{3}] <: {3}.
	So, according to the law we have: <tt> closure(r)[{3}] = {3}</tt>.		So, according to the law we have: <tt> closure(r)[{3}] = {3}</tt>.

			In the next version of Atelier-B in 2025 closure(R) will be defined as "the smallest relation
			that contains R that is transitive and reflexive."
			This corresponds to ProB's definition prior to version 1.8.0 closure(X) = id(ran(X)\/dom(X)) \/ closure1(X) and is thus different to the B-Book.
			ProB may provide a preference in the next release to allow the user to choose between the two interpretations.


	=== Limitations ===		=== Limitations ===

Michael Leuschel: /* Reflexive Closure */

2025-03-14T10:54:41Z

Reflexive Closure

← Older revision		Revision as of 10:54, 14 March 2025
Line 124:		Line 124:
	In version 1.8.0 (March 2018) ProB changed the definition of the transitive and reflexive closure operator of B.		In version 1.8.0 (March 2018) ProB changed the definition of the transitive and reflexive closure operator of B.
	PorB now uses to the mathematical definition:		PorB now uses to the mathematical definition:
	<pre>		<pre> closure(X) = id(TypeOfX) \/ closure1(X)
	closure(X) = id(TypeOfX) \/ closure1(X)
	</pre>		</pre>
	This means that <tt>closure({1\|->2}) </tt>is now infinite and contains for example the pair <tt>3\|->3</tt>. The same holds for <tt> iterate({1\|->2},0)</tt>.		This means that <tt>closure({1\|->2}) </tt>is now infinite and contains for example the pair <tt>3\|->3</tt>. The same holds for <tt> iterate({1\|->2},0)</tt>.
Line 131:		Line 130:
	the definition in Atelier-B was closure(X) = id(dom(X)) \/ closure1(X).		the definition in Atelier-B was closure(X) = id(dom(X)) \/ closure1(X).
	However, both were not compatible with the following law in the B-Book on page 169		However, both were not compatible with the following law in the B-Book on page 169
	<pre>		<pre> (r[a] <: a => closure(r)[a]=a)
	(r[a] <: a => closure(r)[a]=a)
	</pre>		</pre>
	Take r = {1\|->2}, then r[{3}] <: {3}.		Take r = {1\|->2}, then r[{3}] <: {3}.

Michael Leuschel: /* Differences */

2025-03-14T10:54:26Z

Differences

← Older revision		Revision as of 10:54, 14 March 2025
Line 119:		Line 119:

	* [[Well-Definedness_Checking\|Well-definedness]]: ProB will try to check if your predicates are well-defined during animation or model checking, but there is currently no guarantee that all well-definedness errors will be detected. To be on the safe side, you should ensure that your formulas are well-defined according to the left-to-right definition of well-definedness employed in Rodin for Event-B. ProB now has a [[Well-Definedness_Checking\|static checker for well-definedness]] which you can use for this. Note, however, that ProB may re-order conjuncts if this improves well-definedness. For example, for <tt>x:0..3 & y=10/x & x /=0</tt> ProB will not report an error as the conjunct <tt>x/=0</tt> is processed before the division. Indeed, while this predicate is not well-defined according to Rodin's left-to-right rule, it is well-defined according to the more liberal commutative definition of well-definedness.		* [[Well-Definedness_Checking\|Well-definedness]]: ProB will try to check if your predicates are well-defined during animation or model checking, but there is currently no guarantee that all well-definedness errors will be detected. To be on the safe side, you should ensure that your formulas are well-defined according to the left-to-right definition of well-definedness employed in Rodin for Event-B. ProB now has a [[Well-Definedness_Checking\|static checker for well-definedness]] which you can use for this. Note, however, that ProB may re-order conjuncts if this improves well-definedness. For example, for <tt>x:0..3 & y=10/x & x /=0</tt> ProB will not report an error as the conjunct <tt>x/=0</tt> is processed before the division. Indeed, while this predicate is not well-defined according to Rodin's left-to-right rule, it is well-defined according to the more liberal commutative definition of well-definedness.

			== Reflexive Closure ==

			In version 1.8.0 (March 2018) ProB changed the definition of the transitive and reflexive closure operator of B.
			PorB now uses to the mathematical definition:
			<pre>
			closure(X) = id(TypeOfX) \/ closure1(X)
			</pre>
			This means that <tt>closure({1\|->2}) </tt>is now infinite and contains for example the pair <tt>3\|->3</tt>. The same holds for <tt> iterate({1\|->2},0)</tt>.
			The previous definition was closure(X) = id(ran(X)\/dom(X)) \/ closure1(X) and
			the definition in Atelier-B was closure(X) = id(dom(X)) \/ closure1(X).
			However, both were not compatible with the following law in the B-Book on page 169
			<pre>
			(r[a] <: a => closure(r)[a]=a)
			</pre>
			Take r = {1\|->2}, then r[{3}] <: {3}.
			So, according to the law we have: <tt> closure(r)[{3}] = {3}</tt>.

	=== Limitations ===		=== Limitations ===

Michael Leuschel: /* Using the Atelier B Provers inside ProB */

2025-02-07T13:45:45Z

Using the Atelier B Provers inside ProB

← Older revision		Revision as of 13:45, 7 February 2025
Line 72:		Line 72:
	== Using the Atelier B Provers inside ProB ==		== Using the Atelier B Provers inside ProB ==

	In the REPL of probcli you can [[Proving_Theorems_in_the_ProB_REPL#Calling_Atelier-B_Provers call the provers ML and PP of Atelier-B]].		In the REPL of probcli you can [[Proving_Theorems_in_the_ProB_REPL#Calling_Atelier-B_Provers \| call the provers ML and PP of Atelier-B]].

	== Differences with Atelier B ==		== Differences with Atelier B ==