ProB Documentation - User contributions [en]

TLC

2016-08-11T12:05:41Z

Dominik Hansen:

As of version 1.4.0, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker.
TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].

= How to use TLC =

== Using TLC in ProB Tcl/Tk ==
First you have to open a B specification in the ProB GUI.
Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.

[[File:Model_Checking_With_TLC.png|400px|center]]

You can use TLC to find the following kinds of errors in the B specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations

In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.

[[File:Model_Checking_With_TLC_Trace.png|400px|center]]
=== Requirements ===
On Linux the tlc-thread package is required to run TLC from the tcl/tk ui:
sudo apt-get install tcl-thread

== Using TLC in probcli ==

You can use the following switch to use TLC rather than ProB's model checker:
-mc_with_tlc

Some of the standard probcli options also work for TLC:
* -noinv (no invariant checking)
* -nodead (no deadlock checking)
* -noass (no assertion checking)
* -nogoal (no checking for the optional goal predicate)
In addition you can provide
* -noltl (no checking of LTL assertions)

The preference <tt>TLC_WORKERS</tt> influences the number of workers that will be used by TLC.
So, a call might look like this:
probcli FILE.mch -mc_with_tlc -p TLC_WORKERS 2 -noltl

= When to use TLC =
TLC is extremely valuable when it comes to explicit state model checking for large state spaces.
Otherwise, TLC has no constraint solving abilities.

= Translation from B to TLA+ =

TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

= Limitations =
The following constructs are currently not supported by the TLC4B translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)

= Visited States =
Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this issue:

MACHINE NumberOfStates
CONSTANTS k
PROPERTIES
k : 1..10
VARIABLES x
INVARIANT
x : NATURAL
INITIALISATION x := k
END

ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):
[[File:NumberOfStates.jpeg|800px|left|State space generated by ProB]]

TLC will only report 10 distinct states (10 initialization states).

= More Information =
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].

TLC

2016-08-11T12:02:57Z

Dominik Hansen:

As of version 1.4.0, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker.
TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].

= How to use TLC =

== Using TLC in ProB Tcl/Tk ==
First you have to open a B specification in the ProB GUI.
Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.

[[File:Model_Checking_With_TLC.png|400px|center]]

You can use TLC to find the following kinds of errors in the B specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations

In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.

[[File:Model_Checking_With_TLC_Trace.png|400px|center]]
=== Requirements ===
On Linux the tlc-thread package is required to run TLC from the tcl/tk ui.

the sudo apt-get install tcl-thread
== Using TLC in probcli ==

You can use the following switch to use TLC rather than ProB's model checker:
-mc_with_tlc

Some of the standard probcli options also work for TLC:
* -noinv (no invariant checking)
* -nodead (no deadlock checking)
* -noass (no assertion checking)
* -nogoal (no checking for the optional goal predicate)
In addition you can provide
* -noltl (no checking of LTL assertions)

The preference <tt>TLC_WORKERS</tt> influences the number of workers that will be used by TLC.
So, a call might look like this:
probcli FILE.mch -mc_with_tlc -p TLC_WORKERS 2 -noltl

= When to use TLC =
TLC is extremely valuable when it comes to explicit state model checking for large state spaces.
Otherwise, TLC has no constraint solving abilities.

= Translation from B to TLA+ =

TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

= Limitations =
The following constructs are currently not supported by the TLC4B translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)

= Visited States =
Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this issue:

MACHINE NumberOfStates
CONSTANTS k
PROPERTIES
k : 1..10
VARIABLES x
INVARIANT
x : NATURAL
INITIALISATION x := k
END

ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):
[[File:NumberOfStates.jpeg|800px|left|State space generated by ProB]]

TLC will only report 10 distinct states (10 initialization states).

= More Information =
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].

Editors for ProB

2016-07-07T08:28:16Z

Dominik Hansen: /* Atom */

== ProB Tcl/Tk Editor ==

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models.
The editor of Tcl/Tk, however, has a few limitations:
* it can become very slow with long or very long lines
* the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu).
You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

== Launching the editor in probcli ==

The [[Using_the_Command-Line_Version_of_ProB|probcli]] REPL (read-eval-print-loop) supports the command <tt>:e</tt> to open the current file in the external editor, as specified in the "EDITOR" preference.
You can set this preference using
probcli -repl -p EDITOR PATH
In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

== External Editors ==

=== VIM ===

A [https://github.com/bivab/prob.vim VIM plugin for ProB is available].
It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].

=== Atom ===

There is a package [https://atom.io/packages/language-b-eventb language-b-eventb] available for the Atom editor.
It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.
It integrates with probcli to obtain error markers for syntax and type errors.

=== BBEdit ===

Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available.

=== Emacs ===

A package [[File:b-mode.el.zip]] is available.

File:ProB-Atom-Package.zip

2016-07-06T10:14:38Z

Dominik Hansen: Dominik Hansen uploaded a new version of File:ProB-Atom-Package.zip

Editors for ProB

2016-07-06T10:13:59Z

Dominik Hansen: /* Atom */

== ProB Tcl/Tk Editor ==

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models.
The editor of Tcl/Tk, however, has a few limitations:
* it can become very slow with long or very long lines
* the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu).
You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

== Launching the editor in probcli ==

The [[Using_the_Command-Line_Version_of_ProB|probcli]] REPL (read-eval-print-loop) supports the command <tt>:e</tt> to open the current file in the external editor, as specified in the "EDITOR" preference.
You can set this preference using
probcli -repl -p EDITOR PATH
In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

== External Editors ==

=== VIM ===

A [https://github.com/bivab/prob.vim VIM plugin for ProB is available].
It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].

=== Atom ===

There is a package [https://atom.io/packages/language-b-eventb language-b-eventb] available for the Atom editor.
It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.
It integrates with probcli to obtain error markers for syntax and type errors.

A package [[File:ProB-Atom-Package.zip]] for offline installation is available (should be used if you have restrictive proxy).

=== BBEdit ===

Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available.

=== Emacs ===

A package [[File:b-mode.el.zip]] is available.

Editors for ProB

2016-07-06T10:12:33Z

Dominik Hansen: /* Atom */

== ProB Tcl/Tk Editor ==

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models.
The editor of Tcl/Tk, however, has a few limitations:
* it can become very slow with long or very long lines
* the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu).
You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

== Launching the editor in probcli ==

The [[Using_the_Command-Line_Version_of_ProB|probcli]] REPL (read-eval-print-loop) supports the command <tt>:e</tt> to open the current file in the external editor, as specified in the "EDITOR" preference.
You can set this preference using
probcli -repl -p EDITOR PATH
In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

== External Editors ==

=== VIM ===

A [https://github.com/bivab/prob.vim VIM plugin for ProB is available].
It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].

=== Atom ===

There is a package [https://atom.io/packages/language-b-eventb language-b-eventb] available for the Atom editor.
It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.
It integrates with probcli to obtain error markers for syntax and type errors.

[File:ProB-Atom-Package.zip|Packages] for offline installation (should be used if you have restrictive proxy).

=== BBEdit ===

Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available.

=== Emacs ===

A package [[File:b-mode.el.zip]] is available.

Editors for ProB

2016-07-06T09:37:13Z

Dominik Hansen: /* Atom */

== ProB Tcl/Tk Editor ==

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models.
The editor of Tcl/Tk, however, has a few limitations:
* it can become very slow with long or very long lines
* the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu).
You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

== Launching the editor in probcli ==

The [[Using_the_Command-Line_Version_of_ProB|probcli]] REPL (read-eval-print-loop) supports the command <tt>:e</tt> to open the current file in the external editor, as specified in the "EDITOR" preference.
You can set this preference using
probcli -repl -p EDITOR PATH
In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

== External Editors ==

=== VIM ===

A [https://github.com/bivab/prob.vim VIM plugin for ProB is available].
It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].

=== Atom ===

There is a package [https://atom.io/packages/language-b-eventb language-b-eventb] available for the Atom editor.
It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.
It integrates with probcli to obtain error markers for syntax and type errors.

[[File:ProB-Atom-Package.zip|Packages]] for offline installation (should be used if you have restrictive proxy).

=== BBEdit ===

Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available.

=== Emacs ===

A package [[File:b-mode.el.zip]] is available.

Editors for ProB

2016-07-06T09:36:30Z

Dominik Hansen: /* Atom */

== ProB Tcl/Tk Editor ==

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models.
The editor of Tcl/Tk, however, has a few limitations:
* it can become very slow with long or very long lines
* the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu).
You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

== Launching the editor in probcli ==

The [[Using_the_Command-Line_Version_of_ProB|probcli]] REPL (read-eval-print-loop) supports the command <tt>:e</tt> to open the current file in the external editor, as specified in the "EDITOR" preference.
You can set this preference using
probcli -repl -p EDITOR PATH
In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

== External Editors ==

=== VIM ===

A [https://github.com/bivab/prob.vim VIM plugin for ProB is available].
It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].

=== Atom ===

There is a package [https://atom.io/packages/language-b-eventb language-b-eventb] available for the Atom editor.
It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.
It integrates with probcli to obtain error markers for syntax and type errors.

[[File:ProB-Atom-Package.zip Packages]] for offline installation (should be used if you have restrictive proxy).

=== BBEdit ===

Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available.

=== Emacs ===

A package [[File:b-mode.el.zip]] is available.

File:ProB-Atom-Package.zip

2016-07-06T09:35:15Z

Dominik Hansen: Dominik Hansen uploaded a new version of File:ProB-Atom-Package.zip

File:ProB-Atom-Package.zip

2016-07-06T05:37:05Z

Dominik Hansen:

Editors for ProB

2016-07-06T05:36:39Z

Dominik Hansen: /* Atom */

== ProB Tcl/Tk Editor ==

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models.
The editor of Tcl/Tk, however, has a few limitations:
* it can become very slow with long or very long lines
* the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu).
You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

== Launching the editor in probcli ==

The [[Using_the_Command-Line_Version_of_ProB|probcli]] REPL (read-eval-print-loop) supports the command <tt>:e</tt> to open the current file in the external editor, as specified in the "EDITOR" preference.
You can set this preference using
probcli -repl -p EDITOR PATH
In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

== External Editors ==

=== VIM ===

A [https://github.com/bivab/prob.vim VIM plugin for ProB is available].
It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].

=== Atom ===

There is a package [https://atom.io/packages/language-b-eventb language-b-eventb] available for the Atom editor.
It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.
It integrates with probcli to obtain error markers for syntax and type errors.

Offline installation (should be used if you have restrictive proxy): [[File:ProB-Atom-Package.zip]]

=== BBEdit ===

Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available.

=== Emacs ===

A package [[File:b-mode.el.zip]] is available.

Editors for ProB

2016-07-06T05:34:23Z

Dominik Hansen: /* Atom */

== ProB Tcl/Tk Editor ==

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models.
The editor of Tcl/Tk, however, has a few limitations:
* it can become very slow with long or very long lines
* the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu).
You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

== Launching the editor in probcli ==

The [[Using_the_Command-Line_Version_of_ProB|probcli]] REPL (read-eval-print-loop) supports the command <tt>:e</tt> to open the current file in the external editor, as specified in the "EDITOR" preference.
You can set this preference using
probcli -repl -p EDITOR PATH
In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

== External Editors ==

=== VIM ===

A [https://github.com/bivab/prob.vim VIM plugin for ProB is available].
It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].

=== Atom ===

There is a package [https://atom.io/packages/language-b-eventb language-b-eventb] available for the Atom editor.
It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.
It integrates with probcli to obtain error markers for syntax and type errors.

Windows offline installation (should be used if you have restrictive proxy): [[File:Atom-ProB-Windows-Bundle.zip]]

=== BBEdit ===

Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available.

=== Emacs ===

A package [[File:b-mode.el.zip]] is available.

Editors for ProB

2016-07-06T05:33:22Z

Dominik Hansen: /* Atom */

== ProB Tcl/Tk Editor ==

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models.
The editor of Tcl/Tk, however, has a few limitations:
* it can become very slow with long or very long lines
* the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu).
You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

== Launching the editor in probcli ==

The [[Using_the_Command-Line_Version_of_ProB|probcli]] REPL (read-eval-print-loop) supports the command <tt>:e</tt> to open the current file in the external editor, as specified in the "EDITOR" preference.
You can set this preference using
probcli -repl -p EDITOR PATH
In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

== External Editors ==

=== VIM ===

A [https://github.com/bivab/prob.vim VIM plugin for ProB is available].
It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].

=== Atom ===

There is a package [https://atom.io/packages/language-b-eventb language-b-eventb] available for the Atom editor.
It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.
It integrates with probcli to obtain error markers for syntax and type errors.

Windows offline installation: [[File:Atom-ProB-Windows-Bundle.zip]]

=== BBEdit ===

Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available.

=== Emacs ===

A package [[File:b-mode.el.zip]] is available.

Editors for ProB

2016-07-06T05:33:11Z

Dominik Hansen: /* Atom */

== ProB Tcl/Tk Editor ==

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models.
The editor of Tcl/Tk, however, has a few limitations:
* it can become very slow with long or very long lines
* the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu).
You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

== Launching the editor in probcli ==

The [[Using_the_Command-Line_Version_of_ProB|probcli]] REPL (read-eval-print-loop) supports the command <tt>:e</tt> to open the current file in the external editor, as specified in the "EDITOR" preference.
You can set this preference using
probcli -repl -p EDITOR PATH
In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

== External Editors ==

=== VIM ===

A [https://github.com/bivab/prob.vim VIM plugin for ProB is available].
It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].

=== Atom ===

There is a package [https://atom.io/packages/language-b-eventb language-b-eventb] available for the Atom editor.
It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.
It integrates with probcli to obtain error markers for syntax and type errors.

Windows offline Installation: [[File:Atom-ProB-Windows-Bundle.zip]]

=== BBEdit ===

Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available.

=== Emacs ===

A package [[File:b-mode.el.zip]] is available.

Editors for ProB

2016-07-06T05:32:11Z

Dominik Hansen: /* Atom */

== ProB Tcl/Tk Editor ==

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models.
The editor of Tcl/Tk, however, has a few limitations:
* it can become very slow with long or very long lines
* the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu).
You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

== Launching the editor in probcli ==

The [[Using_the_Command-Line_Version_of_ProB|probcli]] REPL (read-eval-print-loop) supports the command <tt>:e</tt> to open the current file in the external editor, as specified in the "EDITOR" preference.
You can set this preference using
probcli -repl -p EDITOR PATH
In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

== External Editors ==

=== VIM ===

A [https://github.com/bivab/prob.vim VIM plugin for ProB is available].
It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].

=== Atom ===

There is a package [https://atom.io/packages/language-b-eventb language-b-eventb] available for the Atom editor.
It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.
It integrates with probcli to obtain error markers for syntax and type errors.

Windows Offline Installation: [[File:Atom-ProB-Windows-Bundle.zip]]

=== BBEdit ===

Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available.

=== Emacs ===

A package [[File:b-mode.el.zip]] is available.

Editors for ProB

2016-07-06T05:31:58Z

Dominik Hansen: /* Atom */

== ProB Tcl/Tk Editor ==

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models.
The editor of Tcl/Tk, however, has a few limitations:
* it can become very slow with long or very long lines
* the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu).
You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

== Launching the editor in probcli ==

The [[Using_the_Command-Line_Version_of_ProB|probcli]] REPL (read-eval-print-loop) supports the command <tt>:e</tt> to open the current file in the external editor, as specified in the "EDITOR" preference.
You can set this preference using
probcli -repl -p EDITOR PATH
In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

== External Editors ==

=== VIM ===

A [https://github.com/bivab/prob.vim VIM plugin for ProB is available].
It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].

=== Atom ===

There is a package [https://atom.io/packages/language-b-eventb language-b-eventb] available for the Atom editor.
It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.
It integrates with probcli to obtain error markers for syntax and type errors.

Windows Offline Installation [[File:Atom-ProB-Windows-Bundle.zip]]

=== BBEdit ===

Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available.

=== Emacs ===

A package [[File:b-mode.el.zip]] is available.

ProB for TLA

2016-03-31T09:15:08Z

Dominik Hansen: Redirected page to TLA

#REDIRECT [[TLA]]

File:ProBWindowsDownload.png

2016-03-30T15:14:00Z

Dominik Hansen: Dominik Hansen uploaded a new version of File:ProBWindowsDownload.png

File:ProBWindowsDownload.png

2016-03-30T15:13:38Z

Dominik Hansen: Dominik Hansen uploaded a new version of File:ProBWindowsDownload.png

File:ProBWindowsDownload.png

2016-03-30T15:10:49Z

Dominik Hansen: Dominik Hansen uploaded a new version of File:ProBWindowsDownload.png

Windows Installation Instructions

2016-03-30T15:06:34Z

Dominik Hansen: /* Install Java */

Windows Specific Download Instructions

=== Go to the ProB Downloads site ===

* Go to the page [http://www.stups.uni-duesseldorf.de/ProB/index.php5/Download http://www.stups.uni-duesseldorf.de/ProB/index.php5/Download], this should look as follows:

[[File:ProBWindowsDownload.png|center||600px]]

=== Install Tcl/Tk 8.5 ===

If Tcl/Tk 8.5 is already installed you can skip this step.

* Click on the "[http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.5 for Windows]," link provided in the "Dependencies" column and the "Windows" row above
* Choose the most recent Tcl/Tk 8.5 distribution available for windows; be sure to choose a version matching ProB, e.g. a 32-bit version (the file highlighted in blue below) if you want to use the 32-bit version of ProB.
* Download and follow the installation instructions

[[File:TkWindowsDownload.png|center||600px]]

=== Install Java ===

If Java 7 or newer is already installed you can skip this step.

* Click on the "[http://java.com/en/ Java Runtime Environment (7.0 or newer)]" link provided in the "Dependencies" column and the "Windows" row above
* Follow the installation instructions

=== Download the ProB for Windows Zipfile ===

* Click on the "[http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.4.1/ProB.windows.zip Zipfile (with probcli)]" link in the [[Download|Download]] column and Windows row
* Decompress and expand the ProB directory if necessary. Do not change the location and structure of the files and directories within ProB (apart from the Machines directory)! The contents of the ProB directory should look something like this:

[[File:ProBWindowsFolder.png|center]]

The subfolder called "Microsoft.VC80.CRT" contains the DLLs for the Microsoft C runtime.

=== Optionally Download GraphViz ===

* Install the "dot" program and "dotty" viewer from AT&T's Graphviz package (http://www.graphviz.org/ or http://www.research.att.com/sw/tools/graphviz/)

=== Start ProB ===

* Start ProB by double-clicking on the ProBWin icon above
* Try to open some of the examples provided in the Examples folder shown above
* Contact us if you have problems

=== Checklist/Troubleshooting ===

* Java: be sure to have Java 1.7 or newer installed. Otherwise you will not be able to parse your own classical B machines as our parser is written in Java.

* Tcl/Tk: be sure to have a matching version of TclTk 8.5 installed

* In case you cannot start neither ProBWin nor probcli, you should to install the [http://www.microsoft.com/en-us/download/details.aspx?id=3387 Microsoft Visual C++ 2005 Redistributable Package (x86)] for yourself (rather than rely on the ones we provide in the "Microsoft.VC80.CRT" folder mentioned above).

* Try starting ProBWin or probcli from the Windows Command Prompt; the error messages may help you or us uncover the problem

* You can also try and obtain information from the main Windows Event/Error Log, by following these steps:
** Click Start, and then click Control Panel.
** Click Performance and Maintenance, then click Administrative Tools, and then double-click Computer Management. Or, open the MMC containing the Event Viewer snap-in.
** In the console tree, expand Event Viewer, and then click the log that contains the event that you want to view.
** In the details pane, double-click the event that you want to view.
** The Event Properties dialog box containing header information and a description of the event is displayed.

Editors for ProB

2016-02-26T14:19:33Z

Dominik Hansen:

== ProB Tcl/Tk Editor ==

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models.
The editor of Tcl/Tk, however, has a few limitations:
* it can become very slow with long or very long lines
* the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu).
You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

== Launching the editor in probcli ==

The [[Using_the_Command-Line_Version_of_ProB|probcli]] REPL (read-eval-print-loop) supports the command <tt>:e</tt> to open the current file in the external editor, as specified in the "EDITOR" preference.
You can set this preference using
probcli -repl -p EDITOR PATH
In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

== External Editors ==

=== VIM ===

A [https://github.com/bivab/prob.vim VIM plugin for ProB is available].
It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].

=== Atom ===

There is a package [https://atom.io/packages/language-b-eventb language-b-eventb] available for the Atom editor.
It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.

=== BBEdit ===

Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available.

=== Emacs ===

A package [[File:b-mode.el.zip]] is available.

Die Hard Jugs Puzzle

2016-02-03T12:34:42Z

Dominik Hansen: /* TLA+ Version */

This is the B model of a puzzle from the movie "Die Hard with a Vengeance".
This [https://www.youtube.com/watch?v=BVtQNK_ZUJg clip shows Bruce Willis and Samuel Jackson having a go at the puzzle].
A [http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm more detailed explanation can be found here].
At start we have one 3 gallon and one 5 gallon jug, and we need to measure precisely 4 gallons by filling, emptying or transferring water from the jugs.

<pre>
MACHINE Jars
DEFINITIONS
GOAL == (4 : ran(level));
SETS Jars = {j3,j5}
CONSTANTS maxf
PROPERTIES maxf : Jars --> NATURAL &
maxf = {j3 |-> 3, j5 |-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */
VARIABLES level
INVARIANT
level: Jars --> NATURAL
INITIALISATION level := Jars * {0} /* all jars start out empty */
OPERATIONS
FillJar(j) = /* we can completely fill a jar j */
PRE j:Jars & level(j)<maxf(j) THEN
level(j) := maxf(j)
END;
EmptyJar(j) = /* we can completely empty a jar j */
PRE j:Jars & level(j)>0 THEN
level(j) := 0
END;
Transfer(j1,amount,j2) = /* we can transfer from jar j1 to j2 until either j2 is full or j1 is empty */
PRE j1:Jars & j2:Jars & j1 /= j2 & amount>0 &
amount = min({level(j1), maxf(j2)-level(j2)}) THEN
level := level <+ { j1|-> level(j1)-amount, j2 |-> level(j2)+amount }
END
END
</pre>

After opening the file in ProB, choose the Model Check command in the Verify menu and then check the "Find Define GOAL" check box.
This instructs ProB to search for states satisfying the GOAL predicate <tt>(4:ran(level))</tt> defined above.

[[File:ProB_ModelCheckGoalBox.png|300px|center]]

Now press the model check button and you should now obtain the following message:
[[File:ProB_Goal_Found.png|300px|center]]

The main window of ProB now contains the following information:

[[File:Jars_Panes.png|700px|center]]

You can see that the second jug contains exactly 4 gallons. The steps required to reach this state can be found in the history pane on the right (in reverse order).

== Graphical Animation ==

This machine above is actually included in the ProB distribution (inside the examples/B/GraphicalAnimation/ directory).
It also contains the following lines in the DEFINITIONS section, which defines a quick-and-dirty [[Graphical_Visualization|graphical visualisation]] of the state.
The images can be found in the subfolder images along the file Jars.mch.

<pre>
ANIMATION_IMG1 == "images/Filled.gif";
ANIMATION_IMG2 == "images/Empty.gif";
ANIMATION_IMG3 == "images/Void.gif";
gmax == max(ran(maxf));
ANIMATION_FUNCTION_DEFAULT == {r,c,i | c:Jars & r:1..gmax & i=3};
ri == (gmax+1-r);
ANIMATION_FUNCTION == {r,c,i | c:Jars & ri:1..maxf(c) &
(ri<=level(c) => i=1 ) & (ri>level(c) => i=2)}
</pre>

Here is a screenshot of ProB Tcl/Tk after loading the model and having found the goal:

[[File:ProB_DieHard_Screenshot.png|600px|center]]

== Using probcli (command-line version) ==

To find the solution using probcli you just need to type:

probcli -model_check Jars.mch

The output will be as follows:

<pre>
$ probcli -model_check Jars.mch
% found_enumeration_of_constants(30,40)
% backtrack(found_enumeration_of_constants(30,40))

ALL OPERATIONS COVERED

found_error(goal_found,10)
finding_trace_from_to(root)
.
Model Checking Time: 60 ms (60 ms walltime)
States analysed: 10
Transitions fired: 36
*** COUNTER EXAMPLE FOUND ***

goal_found
*** TRACE:
1: SETUP_CONSTANTS({(j3|->3),(j5|->5)}):
2: INITIALISATION({(j3|->0),(j5|->0)}):
3: FillJar(j5):
4: Transfer(j5,3,j3):
5: EmptyJar(j3):
6: Transfer(j5,2,j3):
7: FillJar(j5):
8: Transfer(j5,1,j3):
! *** error occurred ***
! goal_found
</pre>

== TLA+ Version ==
A TLA+ version of the puzzle is also included with ProB (inside the examples/TLA+/ directory).
The specification was developed by Leslie Lamport. It is possible to load TLA+ specifications with ProB as shown on the [[TLA]] wiki page.
<pre>
------------------------------ MODULE DieHard -------------------------------
(***************************************************************************)
(* In the movie Die Hard 3, the heros must obtain exactly 4 gallons of *)
(* water using a 5 gallon jug, a 3 gallon jug, and a water faucet. Our *)
(* goal: to get TLC to solve the problem for us. *)
(* *)
(* First, we write a spec that describes all allowable behaviors of our *)
(* heros. *)
(***************************************************************************)
EXTENDS Naturals
(*************************************************************************)
(* This statement imports the definitions of the ordinary operators on *)
(* natural numbers, such as +. *)
(*************************************************************************)

(***************************************************************************)
(* We next declare the specification's variables. *)
(***************************************************************************)
VARIABLES big, \* The number of gallons of water in the 5 gallon jug.
small \* The number of gallons of water in the 3 gallon jug.

(***************************************************************************)
(* We now define TypeOK to be the type invariant, asserting that the value *)
(* of each variable is an element of the appropriate set. A type *)
(* invariant like this is not part of the specification, but it's *)
(* generally a good idea to include it because it helps the reader *)
(* understand the spec. Moreover, having TLC check that it is an *)
(* invariant of the spec catches errors that, in a typed language, are *)
(* caught by type checking. *)
(* *)
(* Note: TLA+ uses the convention that a list of formulas bulleted by /\ *)
(* or \/ denotes the conjunction or disjunction of those formulas. *)
(* Indentation of subitems is significant, allowing one to eliminate lots *)
(* of parentheses. This makes a large formula much easier to read. *)
(* However, it does mean that you have to be careful with your indentation.*)
(***************************************************************************)
TypeOK == /\ small \in 0..3
/\ big \in 0..5

(***************************************************************************)
(* Now we define of the initial predicate, that specifies the initial *)
(* values of the variables. I like to name this predicate Init, but the *)
(* name doesn't matter. *)
(***************************************************************************)
Init == /\ big = 0
/\ small = 0

(***************************************************************************)
(* Now we define the actions that our hero can perform. There are three *)
(* things they can do: *)
(* *)
(* - Pour water from the faucet into a jug. *)
(* *)
(* - Pour water from a jug onto the ground. *)
(* *)
(* - Pour water from one jug into another *)
(* *)
(* We now consider the first two. Since the jugs are not calibrated, *)
(* partially filling or partially emptying a jug accomplishes nothing. *)
(* So, the first two possibilities yield the following four possible *)
(* actions. *)
(***************************************************************************)
FillSmallJug == /\ small' = 3
/\ big' = big

FillBigJug == /\ big' = 5
/\ small' = small

EmptySmallJug == /\ small' = 0
/\ big' = big

EmptyBigJug == /\ big' = 0
/\ small' = small

(***************************************************************************)
(* We now consider pouring water from one jug into another. Again, since *)
(* the jugs are not callibrated, when pouring from jug A to jug B, it *)
(* makes sense only to either fill B or empty A. And there's no point in *)
(* emptying A if this will cause B to overflow, since that could be *)
(* accomplished by the two actions of first filling B and then emptying A. *)
(* So, pouring water from A to B leaves B with the lesser of (i) the water *)
(* contained in both jugs and (ii) the volume of B. To express this *)
(* mathematically, we first define Min(m,n) to equal the minimum of the *)
(* numbers m and n. *)
(***************************************************************************)
Min(m,n) == IF m < n THEN m ELSE n

(***************************************************************************)
(* Now we define the last two pouring actions. From the observation *)
(* above, these definitions should be clear. *)
(***************************************************************************)
SmallToBig == /\ big' = Min(big + small, 5)
/\ small' = small - (big' - big)

BigToSmall == /\ small' = Min(big + small, 3)
/\ big' = big - (small' - small)

(***************************************************************************)
(* We define the next-state relation, which I like to call Next. A Next *)
(* step is a step of one of the six actions defined above. Hence, Next is *)
(* the disjunction of those actions. *)
(***************************************************************************)
Next == \/ FillSmallJug
\/ FillBigJug
\/ EmptySmallJug
\/ EmptyBigJug
\/ SmallToBig
\/ BigToSmall

-----------------------------------------------------------------------------

(***************************************************************************)
(* Remember that our heros must measure out 4 gallons of water. *)
(* Obviously, those 4 gallons must be in the 5 gallon jug. So, they have *)
(* solved their problem when they reach a state with big = 4. So, we *)
(* define NotSolved to be the predicate asserting that big # 4. *)
(***************************************************************************)
NotSolved == big # 4

(***************************************************************************)
(* We find a solution by having TLC check if NotSolved is an invariant, *)
(* which will cause it to print out an "error trace" consisting of a *)
(* behavior ending in a states where NotSolved is false. Such a *)
(* behavior is the desired solution. (Because TLC uses a breadth-first *)
(* search, it will find the shortest solution.) *)
(***************************************************************************)
=============================================================================

</pre>

== Z Version ==

A Z version of the puzzle is also included with ProB (inside the examples/Z/GraphicalAnimation/ directory) and shown on the [[ProZ]] wiki page.

Here is how the animation of the Z specification should look like:

[[File:ProZ_jars.png|600px|center]]

Die Hard Jugs Puzzle

2016-02-03T11:11:40Z

Dominik Hansen:

This is the B model of a puzzle from the movie "Die Hard with a Vengeance".
This [https://www.youtube.com/watch?v=BVtQNK_ZUJg clip shows Bruce Willis and Samuel Jackson having a go at the puzzle].
A [http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm more detailed explanation can be found here].
At start we have one 3 gallon and one 5 gallon jug, and we need to measure precisely 4 gallons by filling, emptying or transferring water from the jugs.

<pre>
MACHINE Jars
DEFINITIONS
GOAL == (4 : ran(level));
SETS Jars = {j3,j5}
CONSTANTS maxf
PROPERTIES maxf : Jars --> NATURAL &
maxf = {j3 |-> 3, j5 |-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */
VARIABLES level
INVARIANT
level: Jars --> NATURAL
INITIALISATION level := Jars * {0} /* all jars start out empty */
OPERATIONS
FillJar(j) = /* we can completely fill a jar j */
PRE j:Jars & level(j)<maxf(j) THEN
level(j) := maxf(j)
END;
EmptyJar(j) = /* we can completely empty a jar j */
PRE j:Jars & level(j)>0 THEN
level(j) := 0
END;
Transfer(j1,amount,j2) = /* we can transfer from jar j1 to j2 until either j2 is full or j1 is empty */
PRE j1:Jars & j2:Jars & j1 /= j2 & amount>0 &
amount = min({level(j1), maxf(j2)-level(j2)}) THEN
level := level <+ { j1|-> level(j1)-amount, j2 |-> level(j2)+amount }
END
END
</pre>

After opening the file in ProB, choose the Model Check command in the Verify menu and then check the "Find Define GOAL" check box.
This instructs ProB to search for states satisfying the GOAL predicate <tt>(4:ran(level))</tt> defined above.

[[File:ProB_ModelCheckGoalBox.png|300px|center]]

Now press the model check button and you should now obtain the following message:
[[File:ProB_Goal_Found.png|300px|center]]

The main window of ProB now contains the following information:

[[File:Jars_Panes.png|700px|center]]

You can see that the second jug contains exactly 4 gallons. The steps required to reach this state can be found in the history pane on the right (in reverse order).

== Graphical Animation ==

This machine above is actually included in the ProB distribution (inside the examples/B/GraphicalAnimation/ directory).
It also contains the following lines in the DEFINITIONS section, which defines a quick-and-dirty [[Graphical_Visualization|graphical visualisation]] of the state.
The images can be found in the subfolder images along the file Jars.mch.

<pre>
ANIMATION_IMG1 == "images/Filled.gif";
ANIMATION_IMG2 == "images/Empty.gif";
ANIMATION_IMG3 == "images/Void.gif";
gmax == max(ran(maxf));
ANIMATION_FUNCTION_DEFAULT == {r,c,i | c:Jars & r:1..gmax & i=3};
ri == (gmax+1-r);
ANIMATION_FUNCTION == {r,c,i | c:Jars & ri:1..maxf(c) &
(ri<=level(c) => i=1 ) & (ri>level(c) => i=2)}
</pre>

Here is a screenshot of ProB Tcl/Tk after loading the model and having found the goal:

[[File:ProB_DieHard_Screenshot.png|600px|center]]

== Using probcli (command-line version) ==

To find the solution using probcli you just need to type:

probcli -model_check Jars.mch

The output will be as follows:

<pre>
$ probcli -model_check Jars.mch
% found_enumeration_of_constants(30,40)
% backtrack(found_enumeration_of_constants(30,40))

ALL OPERATIONS COVERED

found_error(goal_found,10)
finding_trace_from_to(root)
.
Model Checking Time: 60 ms (60 ms walltime)
States analysed: 10
Transitions fired: 36
*** COUNTER EXAMPLE FOUND ***

goal_found
*** TRACE:
1: SETUP_CONSTANTS({(j3|->3),(j5|->5)}):
2: INITIALISATION({(j3|->0),(j5|->0)}):
3: FillJar(j5):
4: Transfer(j5,3,j3):
5: EmptyJar(j3):
6: Transfer(j5,2,j3):
7: FillJar(j5):
8: Transfer(j5,1,j3):
! *** error occurred ***
! goal_found
</pre>

== TLA+ Version ==
A TLA+ version of the puzzle is also included with ProB (inside the examples/TLA+/ directory).
The specification was developed by Leslie Lamport in order to be validated by the TLC model checker. However, it is possible to load TLA+ specifications with ProB as shown on the [[TLA]] wiki page.
<pre>
------------------------------ MODULE DieHard -------------------------------
(***************************************************************************)
(* In the movie Die Hard 3, the heros must obtain exactly 4 gallons of *)
(* water using a 5 gallon jug, a 3 gallon jug, and a water faucet. Our *)
(* goal: to get TLC to solve the problem for us. *)
(* *)
(* First, we write a spec that describes all allowable behaviors of our *)
(* heros. *)
(***************************************************************************)
EXTENDS Naturals
(*************************************************************************)
(* This statement imports the definitions of the ordinary operators on *)
(* natural numbers, such as +. *)
(*************************************************************************)

(***************************************************************************)
(* We next declare the specification's variables. *)
(***************************************************************************)
VARIABLES big, \* The number of gallons of water in the 5 gallon jug.
small \* The number of gallons of water in the 3 gallon jug.

(***************************************************************************)
(* We now define TypeOK to be the type invariant, asserting that the value *)
(* of each variable is an element of the appropriate set. A type *)
(* invariant like this is not part of the specification, but it's *)
(* generally a good idea to include it because it helps the reader *)
(* understand the spec. Moreover, having TLC check that it is an *)
(* invariant of the spec catches errors that, in a typed language, are *)
(* caught by type checking. *)
(* *)
(* Note: TLA+ uses the convention that a list of formulas bulleted by /\ *)
(* or \/ denotes the conjunction or disjunction of those formulas. *)
(* Indentation of subitems is significant, allowing one to eliminate lots *)
(* of parentheses. This makes a large formula much easier to read. *)
(* However, it does mean that you have to be careful with your indentation.*)
(***************************************************************************)
TypeOK == /\ small \in 0..3
/\ big \in 0..5

(***************************************************************************)
(* Now we define of the initial predicate, that specifies the initial *)
(* values of the variables. I like to name this predicate Init, but the *)
(* name doesn't matter. *)
(***************************************************************************)
Init == /\ big = 0
/\ small = 0

(***************************************************************************)
(* Now we define the actions that our hero can perform. There are three *)
(* things they can do: *)
(* *)
(* - Pour water from the faucet into a jug. *)
(* *)
(* - Pour water from a jug onto the ground. *)
(* *)
(* - Pour water from one jug into another *)
(* *)
(* We now consider the first two. Since the jugs are not calibrated, *)
(* partially filling or partially emptying a jug accomplishes nothing. *)
(* So, the first two possibilities yield the following four possible *)
(* actions. *)
(***************************************************************************)
FillSmallJug == /\ small' = 3
/\ big' = big

FillBigJug == /\ big' = 5
/\ small' = small

EmptySmallJug == /\ small' = 0
/\ big' = big

EmptyBigJug == /\ big' = 0
/\ small' = small

(***************************************************************************)
(* We now consider pouring water from one jug into another. Again, since *)
(* the jugs are not callibrated, when pouring from jug A to jug B, it *)
(* makes sense only to either fill B or empty A. And there's no point in *)
(* emptying A if this will cause B to overflow, since that could be *)
(* accomplished by the two actions of first filling B and then emptying A. *)
(* So, pouring water from A to B leaves B with the lesser of (i) the water *)
(* contained in both jugs and (ii) the volume of B. To express this *)
(* mathematically, we first define Min(m,n) to equal the minimum of the *)
(* numbers m and n. *)
(***************************************************************************)
Min(m,n) == IF m < n THEN m ELSE n

(***************************************************************************)
(* Now we define the last two pouring actions. From the observation *)
(* above, these definitions should be clear. *)
(***************************************************************************)
SmallToBig == /\ big' = Min(big + small, 5)
/\ small' = small - (big' - big)

BigToSmall == /\ small' = Min(big + small, 3)
/\ big' = big - (small' - small)

(***************************************************************************)
(* We define the next-state relation, which I like to call Next. A Next *)
(* step is a step of one of the six actions defined above. Hence, Next is *)
(* the disjunction of those actions. *)
(***************************************************************************)
Next == \/ FillSmallJug
\/ FillBigJug
\/ EmptySmallJug
\/ EmptyBigJug
\/ SmallToBig
\/ BigToSmall

-----------------------------------------------------------------------------

(***************************************************************************)
(* Remember that our heros must measure out 4 gallons of water. *)
(* Obviously, those 4 gallons must be in the 5 gallon jug. So, they have *)
(* solved their problem when they reach a state with big = 4. So, we *)
(* define NotSolved to be the predicate asserting that big # 4. *)
(***************************************************************************)
NotSolved == big # 4

(***************************************************************************)
(* We find a solution by having TLC check if NotSolved is an invariant, *)
(* which will cause it to print out an "error trace" consisting of a *)
(* behavior ending in a states where NotSolved is false. Such a *)
(* behavior is the desired solution. (Because TLC uses a breadth-first *)
(* search, it will find the shortest solution.) *)
(***************************************************************************)
=============================================================================

</pre>

== Z Version ==

A Z version of the puzzle is also included with ProB (inside the examples/Z/GraphicalAnimation/ directory) and shown on the [[ProZ]] wiki page.

Here is how the animation of the Z specification should look like:

[[File:ProZ_jars.png|600px|center]]

Die Hard Jugs Puzzle

2016-02-03T11:11:09Z

Dominik Hansen:

This is the B model of a puzzle from the movie "Die Hard with a Vengeance".
This [https://www.youtube.com/watch?v=BVtQNK_ZUJg clip shows Bruce Willis and Samuel Jackson having a go at the puzzle].
A [http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm|more detailed explanation can be found here].
At start we have one 3 gallon and one 5 gallon jug, and we need to measure precisely 4 gallons by filling, emptying or transferring water from the jugs.

<pre>
MACHINE Jars
DEFINITIONS
GOAL == (4 : ran(level));
SETS Jars = {j3,j5}
CONSTANTS maxf
PROPERTIES maxf : Jars --> NATURAL &
maxf = {j3 |-> 3, j5 |-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */
VARIABLES level
INVARIANT
level: Jars --> NATURAL
INITIALISATION level := Jars * {0} /* all jars start out empty */
OPERATIONS
FillJar(j) = /* we can completely fill a jar j */
PRE j:Jars & level(j)<maxf(j) THEN
level(j) := maxf(j)
END;
EmptyJar(j) = /* we can completely empty a jar j */
PRE j:Jars & level(j)>0 THEN
level(j) := 0
END;
Transfer(j1,amount,j2) = /* we can transfer from jar j1 to j2 until either j2 is full or j1 is empty */
PRE j1:Jars & j2:Jars & j1 /= j2 & amount>0 &
amount = min({level(j1), maxf(j2)-level(j2)}) THEN
level := level <+ { j1|-> level(j1)-amount, j2 |-> level(j2)+amount }
END
END
</pre>

After opening the file in ProB, choose the Model Check command in the Verify menu and then check the "Find Define GOAL" check box.
This instructs ProB to search for states satisfying the GOAL predicate <tt>(4:ran(level))</tt> defined above.

[[File:ProB_ModelCheckGoalBox.png|300px|center]]

Now press the model check button and you should now obtain the following message:
[[File:ProB_Goal_Found.png|300px|center]]

The main window of ProB now contains the following information:

[[File:Jars_Panes.png|700px|center]]

You can see that the second jug contains exactly 4 gallons. The steps required to reach this state can be found in the history pane on the right (in reverse order).

== Graphical Animation ==

This machine above is actually included in the ProB distribution (inside the examples/B/GraphicalAnimation/ directory).
It also contains the following lines in the DEFINITIONS section, which defines a quick-and-dirty [[Graphical_Visualization|graphical visualisation]] of the state.
The images can be found in the subfolder images along the file Jars.mch.

<pre>
ANIMATION_IMG1 == "images/Filled.gif";
ANIMATION_IMG2 == "images/Empty.gif";
ANIMATION_IMG3 == "images/Void.gif";
gmax == max(ran(maxf));
ANIMATION_FUNCTION_DEFAULT == {r,c,i | c:Jars & r:1..gmax & i=3};
ri == (gmax+1-r);
ANIMATION_FUNCTION == {r,c,i | c:Jars & ri:1..maxf(c) &
(ri<=level(c) => i=1 ) & (ri>level(c) => i=2)}
</pre>

Here is a screenshot of ProB Tcl/Tk after loading the model and having found the goal:

[[File:ProB_DieHard_Screenshot.png|600px|center]]

== Using probcli (command-line version) ==

To find the solution using probcli you just need to type:

probcli -model_check Jars.mch

The output will be as follows:

<pre>
$ probcli -model_check Jars.mch
% found_enumeration_of_constants(30,40)
% backtrack(found_enumeration_of_constants(30,40))

ALL OPERATIONS COVERED

found_error(goal_found,10)
finding_trace_from_to(root)
.
Model Checking Time: 60 ms (60 ms walltime)
States analysed: 10
Transitions fired: 36
*** COUNTER EXAMPLE FOUND ***

goal_found
*** TRACE:
1: SETUP_CONSTANTS({(j3|->3),(j5|->5)}):
2: INITIALISATION({(j3|->0),(j5|->0)}):
3: FillJar(j5):
4: Transfer(j5,3,j3):
5: EmptyJar(j3):
6: Transfer(j5,2,j3):
7: FillJar(j5):
8: Transfer(j5,1,j3):
! *** error occurred ***
! goal_found
</pre>

== TLA+ Version ==
A TLA+ version of the puzzle is also included with ProB (inside the examples/TLA+/ directory).
The specification was developed by Leslie Lamport in order to be validated by the TLC model checker. However, it is possible to load TLA+ specifications with ProB as shown on the [[TLA]] wiki page.
<pre>
------------------------------ MODULE DieHard -------------------------------
(***************************************************************************)
(* In the movie Die Hard 3, the heros must obtain exactly 4 gallons of *)
(* water using a 5 gallon jug, a 3 gallon jug, and a water faucet. Our *)
(* goal: to get TLC to solve the problem for us. *)
(* *)
(* First, we write a spec that describes all allowable behaviors of our *)
(* heros. *)
(***************************************************************************)
EXTENDS Naturals
(*************************************************************************)
(* This statement imports the definitions of the ordinary operators on *)
(* natural numbers, such as +. *)
(*************************************************************************)

(***************************************************************************)
(* We next declare the specification's variables. *)
(***************************************************************************)
VARIABLES big, \* The number of gallons of water in the 5 gallon jug.
small \* The number of gallons of water in the 3 gallon jug.

(***************************************************************************)
(* We now define TypeOK to be the type invariant, asserting that the value *)
(* of each variable is an element of the appropriate set. A type *)
(* invariant like this is not part of the specification, but it's *)
(* generally a good idea to include it because it helps the reader *)
(* understand the spec. Moreover, having TLC check that it is an *)
(* invariant of the spec catches errors that, in a typed language, are *)
(* caught by type checking. *)
(* *)
(* Note: TLA+ uses the convention that a list of formulas bulleted by /\ *)
(* or \/ denotes the conjunction or disjunction of those formulas. *)
(* Indentation of subitems is significant, allowing one to eliminate lots *)
(* of parentheses. This makes a large formula much easier to read. *)
(* However, it does mean that you have to be careful with your indentation.*)
(***************************************************************************)
TypeOK == /\ small \in 0..3
/\ big \in 0..5

(***************************************************************************)
(* Now we define of the initial predicate, that specifies the initial *)
(* values of the variables. I like to name this predicate Init, but the *)
(* name doesn't matter. *)
(***************************************************************************)
Init == /\ big = 0
/\ small = 0

(***************************************************************************)
(* Now we define the actions that our hero can perform. There are three *)
(* things they can do: *)
(* *)
(* - Pour water from the faucet into a jug. *)
(* *)
(* - Pour water from a jug onto the ground. *)
(* *)
(* - Pour water from one jug into another *)
(* *)
(* We now consider the first two. Since the jugs are not calibrated, *)
(* partially filling or partially emptying a jug accomplishes nothing. *)
(* So, the first two possibilities yield the following four possible *)
(* actions. *)
(***************************************************************************)
FillSmallJug == /\ small' = 3
/\ big' = big

FillBigJug == /\ big' = 5
/\ small' = small

EmptySmallJug == /\ small' = 0
/\ big' = big

EmptyBigJug == /\ big' = 0
/\ small' = small

(***************************************************************************)
(* We now consider pouring water from one jug into another. Again, since *)
(* the jugs are not callibrated, when pouring from jug A to jug B, it *)
(* makes sense only to either fill B or empty A. And there's no point in *)
(* emptying A if this will cause B to overflow, since that could be *)
(* accomplished by the two actions of first filling B and then emptying A. *)
(* So, pouring water from A to B leaves B with the lesser of (i) the water *)
(* contained in both jugs and (ii) the volume of B. To express this *)
(* mathematically, we first define Min(m,n) to equal the minimum of the *)
(* numbers m and n. *)
(***************************************************************************)
Min(m,n) == IF m < n THEN m ELSE n

(***************************************************************************)
(* Now we define the last two pouring actions. From the observation *)
(* above, these definitions should be clear. *)
(***************************************************************************)
SmallToBig == /\ big' = Min(big + small, 5)
/\ small' = small - (big' - big)

BigToSmall == /\ small' = Min(big + small, 3)
/\ big' = big - (small' - small)

(***************************************************************************)
(* We define the next-state relation, which I like to call Next. A Next *)
(* step is a step of one of the six actions defined above. Hence, Next is *)
(* the disjunction of those actions. *)
(***************************************************************************)
Next == \/ FillSmallJug
\/ FillBigJug
\/ EmptySmallJug
\/ EmptyBigJug
\/ SmallToBig
\/ BigToSmall

-----------------------------------------------------------------------------

(***************************************************************************)
(* Remember that our heros must measure out 4 gallons of water. *)
(* Obviously, those 4 gallons must be in the 5 gallon jug. So, they have *)
(* solved their problem when they reach a state with big = 4. So, we *)
(* define NotSolved to be the predicate asserting that big # 4. *)
(***************************************************************************)
NotSolved == big # 4

(***************************************************************************)
(* We find a solution by having TLC check if NotSolved is an invariant, *)
(* which will cause it to print out an "error trace" consisting of a *)
(* behavior ending in a states where NotSolved is false. Such a *)
(* behavior is the desired solution. (Because TLC uses a breadth-first *)
(* search, it will find the shortest solution.) *)
(***************************************************************************)
=============================================================================

</pre>

== Z Version ==

A Z version of the puzzle is also included with ProB (inside the examples/Z/GraphicalAnimation/ directory) and shown on the [[ProZ]] wiki page.

Here is how the animation of the Z specification should look like:

[[File:ProZ_jars.png|600px|center]]

Die Hard Jugs Puzzle

2016-02-03T11:03:47Z

Dominik Hansen: /* TLA+ Version */

This is the B model of a puzzle from the movie "Die Hard with a Vengeance".
This [https://www.youtube.com/watch?v=BVtQNK_ZUJg|clip shows Bruce Willis and Samuel Jackson having a go at the puzzle].
A [http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm|more detailed explanation can be found here].
At start we have one 3 gallon and one 5 gallon jug, and we need to measure precisely 4 gallons by filling, emptying or transferring water from the jugs.

<pre>
MACHINE Jars
DEFINITIONS
GOAL == (4 : ran(level));
SETS Jars = {j3,j5}
CONSTANTS maxf
PROPERTIES maxf : Jars --> NATURAL &
maxf = {j3 |-> 3, j5 |-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */
VARIABLES level
INVARIANT
level: Jars --> NATURAL
INITIALISATION level := Jars * {0} /* all jars start out empty */
OPERATIONS
FillJar(j) = /* we can completely fill a jar j */
PRE j:Jars & level(j)<maxf(j) THEN
level(j) := maxf(j)
END;
EmptyJar(j) = /* we can completely empty a jar j */
PRE j:Jars & level(j)>0 THEN
level(j) := 0
END;
Transfer(j1,amount,j2) = /* we can transfer from jar j1 to j2 until either j2 is full or j1 is empty */
PRE j1:Jars & j2:Jars & j1 /= j2 & amount>0 &
amount = min({level(j1), maxf(j2)-level(j2)}) THEN
level := level <+ { j1|-> level(j1)-amount, j2 |-> level(j2)+amount }
END
END
</pre>

After opening the file in ProB, choose the Model Check command in the Verify menu and then check the "Find Define GOAL" check box.
This instructs ProB to search for states satisfying the GOAL predicate <tt>(4:ran(level))</tt> defined above.

[[File:ProB_ModelCheckGoalBox.png|300px|center]]

Now press the model check button and you should now obtain the following message:
[[File:ProB_Goal_Found.png|300px|center]]

The main window of ProB now contains the following information:

[[File:Jars_Panes.png|700px|center]]

You can see that the second jug contains exactly 4 gallons. The steps required to reach this state can be found in the history pane on the right (in reverse order).

== Graphical Animation ==

This machine above is actually included in the ProB distribution (inside the examples/B/GraphicalAnimation/ directory).
It also contains the following lines in the DEFINITIONS section, which defines a quick-and-dirty [[Graphical_Visualization|graphical visualisation]] of the state.
The images can be found in the subfolder images along the file Jars.mch.

<pre>
ANIMATION_IMG1 == "images/Filled.gif";
ANIMATION_IMG2 == "images/Empty.gif";
ANIMATION_IMG3 == "images/Void.gif";
gmax == max(ran(maxf));
ANIMATION_FUNCTION_DEFAULT == {r,c,i | c:Jars & r:1..gmax & i=3};
ri == (gmax+1-r);
ANIMATION_FUNCTION == {r,c,i | c:Jars & ri:1..maxf(c) &
(ri<=level(c) => i=1 ) & (ri>level(c) => i=2)}
</pre>

Here is a screenshot of ProB Tcl/Tk after loading the model and having found the goal:

[[File:ProB_DieHard_Screenshot.png|600px|center]]

== Using probcli (command-line version) ==

To find the solution using probcli you just need to type:

probcli -model_check Jars.mch

The output will be as follows:

<pre>
$ probcli -model_check Jars.mch
% found_enumeration_of_constants(30,40)
% backtrack(found_enumeration_of_constants(30,40))

ALL OPERATIONS COVERED

found_error(goal_found,10)
finding_trace_from_to(root)
.
Model Checking Time: 60 ms (60 ms walltime)
States analysed: 10
Transitions fired: 36
*** COUNTER EXAMPLE FOUND ***

goal_found
*** TRACE:
1: SETUP_CONSTANTS({(j3|->3),(j5|->5)}):
2: INITIALISATION({(j3|->0),(j5|->0)}):
3: FillJar(j5):
4: Transfer(j5,3,j3):
5: EmptyJar(j3):
6: Transfer(j5,2,j3):
7: FillJar(j5):
8: Transfer(j5,1,j3):
! *** error occurred ***
! goal_found
</pre>

== TLA+ Version ==
A TLA+ version of the puzzle is also included with ProB (inside the examples/TLA+/ directory).
The specification was developed by Leslie Lamport in order to be validated by the TLC model checker. However, it is possible to load TLA+ specifications with ProB as shown on the [[TLA]] wiki page.
<pre>
------------------------------ MODULE DieHard -------------------------------
(***************************************************************************)
(* In the movie Die Hard 3, the heros must obtain exactly 4 gallons of *)
(* water using a 5 gallon jug, a 3 gallon jug, and a water faucet. Our *)
(* goal: to get TLC to solve the problem for us. *)
(* *)
(* First, we write a spec that describes all allowable behaviors of our *)
(* heros. *)
(***************************************************************************)
EXTENDS Naturals
(*************************************************************************)
(* This statement imports the definitions of the ordinary operators on *)
(* natural numbers, such as +. *)
(*************************************************************************)

(***************************************************************************)
(* We next declare the specification's variables. *)
(***************************************************************************)
VARIABLES big, \* The number of gallons of water in the 5 gallon jug.
small \* The number of gallons of water in the 3 gallon jug.

(***************************************************************************)
(* We now define TypeOK to be the type invariant, asserting that the value *)
(* of each variable is an element of the appropriate set. A type *)
(* invariant like this is not part of the specification, but it's *)
(* generally a good idea to include it because it helps the reader *)
(* understand the spec. Moreover, having TLC check that it is an *)
(* invariant of the spec catches errors that, in a typed language, are *)
(* caught by type checking. *)
(* *)
(* Note: TLA+ uses the convention that a list of formulas bulleted by /\ *)
(* or \/ denotes the conjunction or disjunction of those formulas. *)
(* Indentation of subitems is significant, allowing one to eliminate lots *)
(* of parentheses. This makes a large formula much easier to read. *)
(* However, it does mean that you have to be careful with your indentation.*)
(***************************************************************************)
TypeOK == /\ small \in 0..3
/\ big \in 0..5

(***************************************************************************)
(* Now we define of the initial predicate, that specifies the initial *)
(* values of the variables. I like to name this predicate Init, but the *)
(* name doesn't matter. *)
(***************************************************************************)
Init == /\ big = 0
/\ small = 0

(***************************************************************************)
(* Now we define the actions that our hero can perform. There are three *)
(* things they can do: *)
(* *)
(* - Pour water from the faucet into a jug. *)
(* *)
(* - Pour water from a jug onto the ground. *)
(* *)
(* - Pour water from one jug into another *)
(* *)
(* We now consider the first two. Since the jugs are not calibrated, *)
(* partially filling or partially emptying a jug accomplishes nothing. *)
(* So, the first two possibilities yield the following four possible *)
(* actions. *)
(***************************************************************************)
FillSmallJug == /\ small' = 3
/\ big' = big

FillBigJug == /\ big' = 5
/\ small' = small

EmptySmallJug == /\ small' = 0
/\ big' = big

EmptyBigJug == /\ big' = 0
/\ small' = small

(***************************************************************************)
(* We now consider pouring water from one jug into another. Again, since *)
(* the jugs are not callibrated, when pouring from jug A to jug B, it *)
(* makes sense only to either fill B or empty A. And there's no point in *)
(* emptying A if this will cause B to overflow, since that could be *)
(* accomplished by the two actions of first filling B and then emptying A. *)
(* So, pouring water from A to B leaves B with the lesser of (i) the water *)
(* contained in both jugs and (ii) the volume of B. To express this *)
(* mathematically, we first define Min(m,n) to equal the minimum of the *)
(* numbers m and n. *)
(***************************************************************************)
Min(m,n) == IF m < n THEN m ELSE n

(***************************************************************************)
(* Now we define the last two pouring actions. From the observation *)
(* above, these definitions should be clear. *)
(***************************************************************************)
SmallToBig == /\ big' = Min(big + small, 5)
/\ small' = small - (big' - big)

BigToSmall == /\ small' = Min(big + small, 3)
/\ big' = big - (small' - small)

(***************************************************************************)
(* We define the next-state relation, which I like to call Next. A Next *)
(* step is a step of one of the six actions defined above. Hence, Next is *)
(* the disjunction of those actions. *)
(***************************************************************************)
Next == \/ FillSmallJug
\/ FillBigJug
\/ EmptySmallJug
\/ EmptyBigJug
\/ SmallToBig
\/ BigToSmall

-----------------------------------------------------------------------------

(***************************************************************************)
(* Remember that our heros must measure out 4 gallons of water. *)
(* Obviously, those 4 gallons must be in the 5 gallon jug. So, they have *)
(* solved their problem when they reach a state with big = 4. So, we *)
(* define NotSolved to be the predicate asserting that big # 4. *)
(***************************************************************************)
NotSolved == big # 4

(***************************************************************************)
(* We find a solution by having TLC check if NotSolved is an invariant, *)
(* which will cause it to print out an "error trace" consisting of a *)
(* behavior ending in a states where NotSolved is false. Such a *)
(* behavior is the desired solution. (Because TLC uses a breadth-first *)
(* search, it will find the shortest solution.) *)
(***************************************************************************)
=============================================================================

</pre>

== Z Version ==

A Z version of the puzzle is also included with ProB (inside the examples/Z/GraphicalAnimation/ directory) and shown on the [[ProZ]] wiki page.

Here is how the animation of the Z specification should look like:

[[File:ProZ_jars.png|600px|center]]

Die Hard Jugs Puzzle

2016-02-03T09:18:25Z

Dominik Hansen:

This is the B model of a puzzle from the movie "Die Hard with a Vengeance".
This [https://www.youtube.com/watch?v=BVtQNK_ZUJg|clip shows Bruce Willis and Samuel Jackson having a go at the puzzle].
A [http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm|more detailed explanation can be found here].
At start we have one 3 gallon and one 5 gallon jug, and we need to measure precisely 4 gallons by filling, emptying or transferring water from the jugs.

<pre>
MACHINE Jars
DEFINITIONS
GOAL == (4 : ran(level));
SETS Jars = {j3,j5}
CONSTANTS maxf
PROPERTIES maxf : Jars --> NATURAL &
maxf = {j3 |-> 3, j5 |-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */
VARIABLES level
INVARIANT
level: Jars --> NATURAL
INITIALISATION level := Jars * {0} /* all jars start out empty */
OPERATIONS
FillJar(j) = /* we can completely fill a jar j */
PRE j:Jars & level(j)<maxf(j) THEN
level(j) := maxf(j)
END;
EmptyJar(j) = /* we can completely empty a jar j */
PRE j:Jars & level(j)>0 THEN
level(j) := 0
END;
Transfer(j1,amount,j2) = /* we can transfer from jar j1 to j2 until either j2 is full or j1 is empty */
PRE j1:Jars & j2:Jars & j1 /= j2 & amount>0 &
amount = min({level(j1), maxf(j2)-level(j2)}) THEN
level := level <+ { j1|-> level(j1)-amount, j2 |-> level(j2)+amount }
END
END
</pre>

After opening the file in ProB, choose the Model Check command in the Verify menu and then check the "Find Define GOAL" check box.
This instructs ProB to search for states satisfying the GOAL predicate <tt>(4:ran(level))</tt> defined above.

[[File:ProB_ModelCheckGoalBox.png|300px|center]]

Now press the model check button and you should now obtain the following message:
[[File:ProB_Goal_Found.png|300px|center]]

The main window of ProB now contains the following information:

[[File:Jars_Panes.png|700px|center]]

You can see that the second jug contains exactly 4 gallons. The steps required to reach this state can be found in the history pane on the right (in reverse order).

== Graphical Animation ==

This machine above is actually included in the ProB distribution (inside the examples/B/GraphicalAnimation/ directory).
It also contains the following lines in the DEFINITIONS section, which defines a quick-and-dirty [[Graphical_Visualization|graphical visualisation]] of the state.
The images can be found in the subfolder images along the file Jars.mch.

<pre>
ANIMATION_IMG1 == "images/Filled.gif";
ANIMATION_IMG2 == "images/Empty.gif";
ANIMATION_IMG3 == "images/Void.gif";
gmax == max(ran(maxf));
ANIMATION_FUNCTION_DEFAULT == {r,c,i | c:Jars & r:1..gmax & i=3};
ri == (gmax+1-r);
ANIMATION_FUNCTION == {r,c,i | c:Jars & ri:1..maxf(c) &
(ri<=level(c) => i=1 ) & (ri>level(c) => i=2)}
</pre>

Here is a screenshot of ProB Tcl/Tk after loading the model and having found the goal:

[[File:ProB_DieHard_Screenshot.png|600px|center]]

== Using probcli (command-line version) ==

To find the solution using probcli you just need to type:

probcli -model_check Jars.mch

The output will be as follows:

<pre>
$ probcli -model_check Jars.mch
% found_enumeration_of_constants(30,40)
% backtrack(found_enumeration_of_constants(30,40))

ALL OPERATIONS COVERED

found_error(goal_found,10)
finding_trace_from_to(root)
.
Model Checking Time: 60 ms (60 ms walltime)
States analysed: 10
Transitions fired: 36
*** COUNTER EXAMPLE FOUND ***

goal_found
*** TRACE:
1: SETUP_CONSTANTS({(j3|->3),(j5|->5)}):
2: INITIALISATION({(j3|->0),(j5|->0)}):
3: FillJar(j5):
4: Transfer(j5,3,j3):
5: EmptyJar(j3):
6: Transfer(j5,2,j3):
7: FillJar(j5):
8: Transfer(j5,1,j3):
! *** error occurred ***
! goal_found
</pre>

== TLA+ Version ==
A TLA+ version of the puzzle is also included with ProB (inside the examples/TLA+/ directory).
The specification was developed by Leslie Lamport in order to be validated by the TLC model checker. However, it possible to load TLA+ specifications with ProB as shown on the [[TLA]] wiki page.
<pre>
------------------------------ MODULE DieHard -------------------------------
(***************************************************************************)
(* In the movie Die Hard 3, the heros must obtain exactly 4 gallons of *)
(* water using a 5 gallon jug, a 3 gallon jug, and a water faucet. Our *)
(* goal: to get TLC to solve the problem for us. *)
(* *)
(* First, we write a spec that describes all allowable behaviors of our *)
(* heros. *)
(***************************************************************************)
EXTENDS Naturals
(*************************************************************************)
(* This statement imports the definitions of the ordinary operators on *)
(* natural numbers, such as +. *)
(*************************************************************************)

(***************************************************************************)
(* We next declare the specification's variables. *)
(***************************************************************************)
VARIABLES big, \* The number of gallons of water in the 5 gallon jug.
small \* The number of gallons of water in the 3 gallon jug.

(***************************************************************************)
(* We now define TypeOK to be the type invariant, asserting that the value *)
(* of each variable is an element of the appropriate set. A type *)
(* invariant like this is not part of the specification, but it's *)
(* generally a good idea to include it because it helps the reader *)
(* understand the spec. Moreover, having TLC check that it is an *)
(* invariant of the spec catches errors that, in a typed language, are *)
(* caught by type checking. *)
(* *)
(* Note: TLA+ uses the convention that a list of formulas bulleted by /\ *)
(* or \/ denotes the conjunction or disjunction of those formulas. *)
(* Indentation of subitems is significant, allowing one to eliminate lots *)
(* of parentheses. This makes a large formula much easier to read. *)
(* However, it does mean that you have to be careful with your indentation.*)
(***************************************************************************)
TypeOK == /\ small \in 0..3
/\ big \in 0..5

(***************************************************************************)
(* Now we define of the initial predicate, that specifies the initial *)
(* values of the variables. I like to name this predicate Init, but the *)
(* name doesn't matter. *)
(***************************************************************************)
Init == /\ big = 0
/\ small = 0

(***************************************************************************)
(* Now we define the actions that our hero can perform. There are three *)
(* things they can do: *)
(* *)
(* - Pour water from the faucet into a jug. *)
(* *)
(* - Pour water from a jug onto the ground. *)
(* *)
(* - Pour water from one jug into another *)
(* *)
(* We now consider the first two. Since the jugs are not calibrated, *)
(* partially filling or partially emptying a jug accomplishes nothing. *)
(* So, the first two possibilities yield the following four possible *)
(* actions. *)
(***************************************************************************)
FillSmallJug == /\ small' = 3
/\ big' = big

FillBigJug == /\ big' = 5
/\ small' = small

EmptySmallJug == /\ small' = 0
/\ big' = big

EmptyBigJug == /\ big' = 0
/\ small' = small

(***************************************************************************)
(* We now consider pouring water from one jug into another. Again, since *)
(* the jugs are not callibrated, when pouring from jug A to jug B, it *)
(* makes sense only to either fill B or empty A. And there's no point in *)
(* emptying A if this will cause B to overflow, since that could be *)
(* accomplished by the two actions of first filling B and then emptying A. *)
(* So, pouring water from A to B leaves B with the lesser of (i) the water *)
(* contained in both jugs and (ii) the volume of B. To express this *)
(* mathematically, we first define Min(m,n) to equal the minimum of the *)
(* numbers m and n. *)
(***************************************************************************)
Min(m,n) == IF m < n THEN m ELSE n

(***************************************************************************)
(* Now we define the last two pouring actions. From the observation *)
(* above, these definitions should be clear. *)
(***************************************************************************)
SmallToBig == /\ big' = Min(big + small, 5)
/\ small' = small - (big' - big)

BigToSmall == /\ small' = Min(big + small, 3)
/\ big' = big - (small' - small)

(***************************************************************************)
(* We define the next-state relation, which I like to call Next. A Next *)
(* step is a step of one of the six actions defined above. Hence, Next is *)
(* the disjunction of those actions. *)
(***************************************************************************)
Next == \/ FillSmallJug
\/ FillBigJug
\/ EmptySmallJug
\/ EmptyBigJug
\/ SmallToBig
\/ BigToSmall

-----------------------------------------------------------------------------

(***************************************************************************)
(* Remember that our heros must measure out 4 gallons of water. *)
(* Obviously, those 4 gallons must be in the 5 gallon jug. So, they have *)
(* solved their problem when they reach a state with big = 4. So, we *)
(* define NotSolved to be the predicate asserting that big # 4. *)
(***************************************************************************)
NotSolved == big # 4

(***************************************************************************)
(* We find a solution by having TLC check if NotSolved is an invariant, *)
(* which will cause it to print out an "error trace" consisting of a *)
(* behavior ending in a states where NotSolved is false. Such a *)
(* behavior is the desired solution. (Because TLC uses a breadth-first *)
(* search, it will find the shortest solution.) *)
(***************************************************************************)
=============================================================================

</pre>

== Z Version ==

A Z version of the puzzle is also included with ProB (inside the examples/Z/GraphicalAnimation/ directory) and shown on the [[ProZ]] wiki page.

Here is how the animation of the Z specification should look like:

[[File:ProZ_jars.png|600px|center]]

Die Hard Jugs Puzzle

2016-02-03T08:53:52Z

Dominik Hansen:

TLC

2016-01-13T14:09:41Z

Dominik Hansen:

As of version 1.4.0, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker.
TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].

= How to use TLC =

First you have to open a B specification in the ProB GUI.
Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.

[[File:Model_Checking_With_TLC.png|400px|center]]

You can use TLC to find the following kinds of errors in the B specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations

In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.

[[File:Model_Checking_With_TLC_Trace.png|400px|center]]

= When to use TLC =
TLC is extremely valuable when it comes to explicit state model checking for large state spaces.
Otherwise, TLC has no constraint solving abilities.

= Translation from B to TLA+ =

TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

= Limitations =
The following constructs are currently not supported by the TLC4B translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)

= Visited States =
Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this issue:

MACHINE NumberOfStates
CONSTANTS k
PROPERTIES
k : 1..10
VARIABLES x
INVARIANT
x : NATURAL
INITIALISATION x := k
END

ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):
[[File:NumberOfStates.jpeg|800px|left|State space generated by ProB]]

TLC will only report 10 distinct states (10 initialization states).

= More Information =
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].

State space visualization examples

2015-12-18T18:07:59Z

Dominik Hansen: /* Alternating Bit Protocol */

(This page is under construction)
== Alternating Bit Protocol ==

This is a visualisation of 3643 states and 11115 transitions of a TLA+ model of the alternating bit protocol, as distributed with the [http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html TLA+ tools].
This model (MCAlternatingBit.tla) was loaded with ProB, the model checker run for a few seconds and then the command "State Space Fast Rendering" with options (scale,fast) was used.

The goal predicate rBit=1 was used; those states satisfying this predicate are shown in orange.

[[File:MCAlternatingBit_sfdp.png|1000px|center]]

The main file of the model is:
<PRE>
--------------------------- MODULE MCAlternatingBit -------------------------
EXTENDS AlternatingBit, TLC

INSTANCE ABCorrectness

CONSTANTS msgQLen, ackQLen

SeqConstraint == /\ Len(msgQ) \leq msgQLen
/\ Len(ackQ) \leq ackQLen

SentLeadsToRcvd == \A d \in Data : (sent = d) /\ (sBit # sAck) ~> (rcvd = d)
=============================================================================

ImpliedAction == [ABCNext]_cvars

TNext == WF_msgQ(~ABTypeInv')
TProp == \A d \in Data : (sent = d) => [](sent = d)

CSpec == ABSpec /\ TNext

DataPerm == Permutations(Data)
==============================================================
</PRE>

State space visualization examples

2015-12-18T18:03:46Z

Dominik Hansen: /* Alternating Bit Protocol */

(This page is under construction)
== Alternating Bit Protocol ==

This is a visualisation of 3643 states and 11115 transitions of a TLA+ model of the alternating bit protocol, as distributed with the [http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html | TLC model checker].
This model (MCAlternatingBit.tla) was loaded with ProB, the model checker run for a few seconds and then the command "State Space Fast Rendering" with options (scale,fast) was used.

The goal predicate rBit=1 was used; those states satisfying this predicate are shown in orange.

[[File:MCAlternatingBit_sfdp.png|1000px|center]]

The main file of the model is:
<PRE>
--------------------------- MODULE MCAlternatingBit -------------------------
EXTENDS AlternatingBit, TLC

INSTANCE ABCorrectness

CONSTANTS msgQLen, ackQLen

SeqConstraint == /\ Len(msgQ) \leq msgQLen
/\ Len(ackQ) \leq ackQLen

SentLeadsToRcvd == \A d \in Data : (sent = d) /\ (sBit # sAck) ~> (rcvd = d)
=============================================================================

ImpliedAction == [ABCNext]_cvars

TNext == WF_msgQ(~ABTypeInv')
TProp == \A d \in Data : (sent = d) => [](sent = d)

CSpec == ABSpec /\ TNext

DataPerm == Permutations(Data)
==============================================================
</PRE>

TLA

2014-11-21T19:56:51Z

Dominik Hansen: /* Using ProB for Animation and Model Checking of TLA+ specifications */

As of version 1.3.5, ProB supports [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].

= Using ProB for Animation and Model Checking of TLA+ specifications =

The [http://nightly.cobra.cs.uni-duesseldorf.de/tcl/ latest version of ProB] uses the translator TLA2B, which translates the non temporal part of a [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+] module to a B machine.
To use ProB for TLA+ you have to download the TLA tools. They are released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].
In the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.

[[File:Download_TLA_Tools.png|400px|center]]

When you open a TLA+ module ProB generates the translated B machine in the same folder and loads it in the background.
If there is a valid translation you can animate and model check the TLA+ specification.
There are many working examples in the 'ProB/Examples/TLA+/'-directory.

There is also an [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschelTLA2012 iFM'2012 paper] that describes our approach and performs some comparison with TLC.
Our [[ProB_Logic_Calculator|online ProB Logic Calculator]] now also supports TLA syntax and you can experiment with its predicate and expression evaluation capabilities.

= TLA2B =

The parser and semantic analyzer [http://research.microsoft.com/en-us/um/people/lamport/tla/sany.html SANY] serves as the front end of TLA2B. SANY was written by Jean-Charles Grégoire
and David Jefferson and is also the front end of the model checker [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC].
After parsing there is type checking phase, in which types of variables and constants are inferred.
So there is no need to especially declare types in a invariant clause (in the manner of the B method).
Moreover it checks if a TLA+ module is translatable (see Limitations of Translation).

To tell TLA2B the name of a specification of a TLA+ module you can use a configuration file, just like for TLC.
The configuration file must have the same name as the name of the module and the filename extension 'cfg'.
The configuration file parser is the same as for TLC so you can look up the syntax in the [http://research.microsoft.com/en-us/um/people/lamport/tla/book.html 'Specifying Systems'-book] (Leslie Lamport).
If there is no configuration file available TLA2B looks for a TLA+ definition named 'Spec'
or alternatively for a 'Init' and a 'Next' definition describing the initial state and the next state relation.
Besides that in the configuration file you can give a constant a value but this is not mandatory, in contrast to TLC.
Otherwise ProB lets you choose during the animation process a value for the constant which satisfy the assumptions under the ASSUME clause.
TLA2B supports furthermore overriding of a constant or definition by another definition in the configuration file.

= Supported TLA+ syntax =
<pre>
Logic
-----
P /\ Q conjunction
P \/ Q disjunction
~ or \lnot or \neg negation
=> implication
<=> or \equiv equivalence
TRUE
FALSE
BOOLEAN set containing TRUE and FALSE
\A x \in S : P universal quantification
\E x \in S : P existential quantification

Equality:
------
e = f equality
e # f or e /= f inequality

Sets
------
{d, e} set consisting of elements d, e
{x \in S : P} set of elements x in S satisfying p
{e : x \in S} set of elements e such that x in S
e \in S element of
e \notin S not element of
S \cup T or S \union T set union
S \cap T or S \intersect set intersection
S \subseteq T equality or subset of
S \ t set difference
SUBSET S set of subsets of S
UNION S union of all elements of S

Functions
------
f[e] function application
DOMAIN f domain of function f
[x \in S |-> e] function f such that f[x] = e for x in S
[S -> T] Set of functions f with f[x] in T for x in S
[f EXCEPT ![e] = d] the function equal to f except f[e] = d

Records
-------
r.id the id-field of record r
[id_1|->e_1,...,id_n|->e_n] construct a record with given field names and values
[id_1:S_1,...,id_n:S_n] set of records with given fields and field types
[r EXCEPT !.id = e] the record equal to r except r.id = e

Strings and Numbers
-------------------
"abc" a string
STRING set of a strings
123 a number

Miscellaneous constructs
------------------------
IF P THEN e_1 ELSE e_2
CASE P_1 -> e_1 [] ... [] P_n ->e_n
CASE P_1 -> e_1 [] ... [] P_n ->e_n [] OTHER -> e
LET d_1 == e_1 ... d_n == e_n IN e

Action Operators
----------------
v' prime operator (only variables are able to be primed)
UNCHANGED v v'=v
UNCHANGED <<v_1, v_2>> v_1'=v_1 /\ v_2=v_2

Supported standard modules
--------------------------
Naturals
--------
x + y addition
x - y difference
x * y multiplication
x \div y division
x % y remainder of division
x ^ y exponentiation
x > y greater than
x < y less than
x \geq y greater than or equal
x \leq y less than or equal
x .. y set of numbers from x to y
Nat set of natural numbers

Integers
--------
-x unary minus
Int set of integers

Sequences
---------
SubSeq(s,m,n) subsequence of s from component m to n
Append(s, e) appending e to sequence s
Len(s) length of sequence s
Seq(s) set of sequences
s_1 \o s_2 or s_1 \circ s_2 concatenation of s_1 and s_2
Head(s)
Tail(s)

FiniteSets
----------
Cardinality(S)
IsFiniteSet(S) (ProB can only handle certain infinite sets as argument)

typical structure of a TLA+ module
--------------------------

---- MODULE m ----
EXTENDS m_1, m_2
CONSTANTS c_1, c_2
ASSUME c_1 = ...
VARIABLES v_1, v_2
foo == ...
Init == ...
Next == ...
Spec == ...
=====================

</pre>
Temporal formulas and unused definitions are ignored by TLA2B (they are also ignored by the type inference algorithm).

= Limitations of the translation =
* due to the strict type system of the B method there are several restrictions to TLA+ modules.
** the elements of a set must have the same type (domain and range of a function are sets)
** TLA+ tuples are translated as sequences in B, hence all components of the tuple must have the same type
* TLA2B do not support 2nd-order operators, i.e. operators that take a operator with arguments as argument (e.g.: foo(bar(_),p))

= TLA+ Actions =
-----------
TLA2B divides the next state relation into different actions if a disjunction occurs.
IF a existential quantification occurs TLA2B searches for further actions in the predicate
of the quantification and adds the bounded variables as arguments to these actions.
IF a definition call occurs and the definition has no arguments TLA2B goes into the definition
searching for further actions.
The displayed actions by ProB are not necessarily identical with the actions determined by TLC.

= Understanding the type checker =

Corresponding B types to TLA+ data values (let type(e) be the type of the expression e):
<pre>
TLA+ data B Type
--------------------------------------------------
number e.g. 123 INTEGER
string e.g. "abc" STRING
bool value e.g. TRUE BOOL
set e.g. {e,f} POW(type(e)), type(e) = type(f)
function e.g. [x \in S |-> e] POW(type(x)*type(e)), type(S) = POW(type(x))
sequence e.g. <<a,b>> POW(INTEGER*type(a)), type(a) = type(b)
record e.g. [id_1|->e_1,...,id_n|->e_n] struct(id_1:type(e_1),...,id_n:type(e_n))
model value ENUM
(only definable in config file)

Nat POW(INTEGER)
Int POW(INTEGER)
STRING POW(STRING)
BOOLEAN POW(BOOL)
SUBSET S POW(type(S))
</pre>
You can only compare data values with the same type.

TLA

2014-11-21T19:53:24Z

Dominik Hansen:

As of version 1.3.5, ProB supports [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].

= Using ProB for Animation and Model Checking of TLA+ specifications =

The [http://nightly.cobra.cs.uni-duesseldorf.de/tcl/ latest version of ProB] uses the translator TLA2B, which translates the non temporal part of a [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+] module to a B machine.
To use ProB for TLA+ you have to download the TLA tools. They are released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].
In the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.

[[File:Download_TLA_Tools.png|400px|center]]

When you then open a TLA+ module ProB then generates the translated B machine in the same folder and loads it in the background.
If there is a valid translation you can animate and model check the TLA+ specification.
There are many working examples in the 'ProB/Examples/TLA+/'-directory.

There is also an [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschelTLA2012 iFM'2012 paper] that describes our approach and performs some comparison with TLC.
Our [[ProB_Logic_Calculator|online ProB Logic Calculator]] now also supports TLA syntax and you can experiment with its predicate and expression evaluation capabilities.

= TLA2B =

The parser and semantic analyzer [http://research.microsoft.com/en-us/um/people/lamport/tla/sany.html SANY] serves as the front end of TLA2B. SANY was written by Jean-Charles Grégoire
and David Jefferson and is also the front end of the model checker [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC].
After parsing there is type checking phase, in which types of variables and constants are inferred.
So there is no need to especially declare types in a invariant clause (in the manner of the B method).
Moreover it checks if a TLA+ module is translatable (see Limitations of Translation).

To tell TLA2B the name of a specification of a TLA+ module you can use a configuration file, just like for TLC.
The configuration file must have the same name as the name of the module and the filename extension 'cfg'.
The configuration file parser is the same as for TLC so you can look up the syntax in the [http://research.microsoft.com/en-us/um/people/lamport/tla/book.html 'Specifying Systems'-book] (Leslie Lamport).
If there is no configuration file available TLA2B looks for a TLA+ definition named 'Spec'
or alternatively for a 'Init' and a 'Next' definition describing the initial state and the next state relation.
Besides that in the configuration file you can give a constant a value but this is not mandatory, in contrast to TLC.
Otherwise ProB lets you choose during the animation process a value for the constant which satisfy the assumptions under the ASSUME clause.
TLA2B supports furthermore overriding of a constant or definition by another definition in the configuration file.

= Supported TLA+ syntax =
<pre>
Logic
-----
P /\ Q conjunction
P \/ Q disjunction
~ or \lnot or \neg negation
=> implication
<=> or \equiv equivalence
TRUE
FALSE
BOOLEAN set containing TRUE and FALSE
\A x \in S : P universal quantification
\E x \in S : P existential quantification

Equality:
------
e = f equality
e # f or e /= f inequality

Sets
------
{d, e} set consisting of elements d, e
{x \in S : P} set of elements x in S satisfying p
{e : x \in S} set of elements e such that x in S
e \in S element of
e \notin S not element of
S \cup T or S \union T set union
S \cap T or S \intersect set intersection
S \subseteq T equality or subset of
S \ t set difference
SUBSET S set of subsets of S
UNION S union of all elements of S

Functions
------
f[e] function application
DOMAIN f domain of function f
[x \in S |-> e] function f such that f[x] = e for x in S
[S -> T] Set of functions f with f[x] in T for x in S
[f EXCEPT ![e] = d] the function equal to f except f[e] = d

Records
-------
r.id the id-field of record r
[id_1|->e_1,...,id_n|->e_n] construct a record with given field names and values
[id_1:S_1,...,id_n:S_n] set of records with given fields and field types
[r EXCEPT !.id = e] the record equal to r except r.id = e

Strings and Numbers
-------------------
"abc" a string
STRING set of a strings
123 a number

Miscellaneous constructs
------------------------
IF P THEN e_1 ELSE e_2
CASE P_1 -> e_1 [] ... [] P_n ->e_n
CASE P_1 -> e_1 [] ... [] P_n ->e_n [] OTHER -> e
LET d_1 == e_1 ... d_n == e_n IN e

Action Operators
----------------
v' prime operator (only variables are able to be primed)
UNCHANGED v v'=v
UNCHANGED <<v_1, v_2>> v_1'=v_1 /\ v_2=v_2

Supported standard modules
--------------------------
Naturals
--------
x + y addition
x - y difference
x * y multiplication
x \div y division
x % y remainder of division
x ^ y exponentiation
x > y greater than
x < y less than
x \geq y greater than or equal
x \leq y less than or equal
x .. y set of numbers from x to y
Nat set of natural numbers

Integers
--------
-x unary minus
Int set of integers

Sequences
---------
SubSeq(s,m,n) subsequence of s from component m to n
Append(s, e) appending e to sequence s
Len(s) length of sequence s
Seq(s) set of sequences
s_1 \o s_2 or s_1 \circ s_2 concatenation of s_1 and s_2
Head(s)
Tail(s)

FiniteSets
----------
Cardinality(S)
IsFiniteSet(S) (ProB can only handle certain infinite sets as argument)

typical structure of a TLA+ module
--------------------------

---- MODULE m ----
EXTENDS m_1, m_2
CONSTANTS c_1, c_2
ASSUME c_1 = ...
VARIABLES v_1, v_2
foo == ...
Init == ...
Next == ...
Spec == ...
=====================

</pre>
Temporal formulas and unused definitions are ignored by TLA2B (they are also ignored by the type inference algorithm).

= Limitations of the translation =
* due to the strict type system of the B method there are several restrictions to TLA+ modules.
** the elements of a set must have the same type (domain and range of a function are sets)
** TLA+ tuples are translated as sequences in B, hence all components of the tuple must have the same type
* TLA2B do not support 2nd-order operators, i.e. operators that take a operator with arguments as argument (e.g.: foo(bar(_),p))

= TLA+ Actions =
-----------
TLA2B divides the next state relation into different actions if a disjunction occurs.
IF a existential quantification occurs TLA2B searches for further actions in the predicate
of the quantification and adds the bounded variables as arguments to these actions.
IF a definition call occurs and the definition has no arguments TLA2B goes into the definition
searching for further actions.
The displayed actions by ProB are not necessarily identical with the actions determined by TLC.

= Understanding the type checker =

Corresponding B types to TLA+ data values (let type(e) be the type of the expression e):
<pre>
TLA+ data B Type
--------------------------------------------------
number e.g. 123 INTEGER
string e.g. "abc" STRING
bool value e.g. TRUE BOOL
set e.g. {e,f} POW(type(e)), type(e) = type(f)
function e.g. [x \in S |-> e] POW(type(x)*type(e)), type(S) = POW(type(x))
sequence e.g. <<a,b>> POW(INTEGER*type(a)), type(a) = type(b)
record e.g. [id_1|->e_1,...,id_n|->e_n] struct(id_1:type(e_1),...,id_n:type(e_n))
model value ENUM
(only definable in config file)

Nat POW(INTEGER)
Int POW(INTEGER)
STRING POW(STRING)
BOOLEAN POW(BOOL)
SUBSET S POW(type(S))
</pre>
You can only compare data values with the same type.

TLC

2014-11-10T10:11:57Z

Dominik Hansen: /* Visited States */

As of version 1.4.0, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker.

= Download and Installation =

TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].
To use TLC in the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.

[[File:Download_TLA_Tools.png|400px|center]]

= How to use TLC =

First you have to open a B specification in the ProB GUI.
Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.

[[File:Model_Checking_With_TLC.png|400px|center]]

You can use TLC to find the following kinds of errors in the B specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations

In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.

[[File:Model_Checking_With_TLC_Trace.png|400px|center]]

= When to use TLC =
TLC is extremely valuable when it comes to explicit state model checking for large state spaces.
Otherwise, TLC has no constraint solving abilities.

= Translation from B to TLA+ =

TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

= Limitations =
The following constructs are currently not supported by the TLC4B translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)

= Visited States =
Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this issue:

MACHINE NumberOfStates
CONSTANTS k
PROPERTIES
k : 1..10
VARIABLES x
INVARIANT
x : NATURAL
INITIALISATION x := k
END

ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):
[[File:NumberOfStates.jpeg|800px|left|State space generated by ProB]]

TLC will only report 10 distinct states (10 initialization states).

= More Information =
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].

TLC

2014-11-10T10:10:47Z

Dominik Hansen: /* Visited States */

As of version 1.4.0, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker.

= Download and Installation =

TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].
To use TLC in the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.

[[File:Download_TLA_Tools.png|400px|center]]

= How to use TLC =

First you have to open a B specification in the ProB GUI.
Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.

[[File:Model_Checking_With_TLC.png|400px|center]]

You can use TLC to find the following kinds of errors in the B specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations

In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.

[[File:Model_Checking_With_TLC_Trace.png|400px|center]]

= When to use TLC =
TLC is extremely valuable when it comes to explicit state model checking for large state spaces.
Otherwise, TLC has no constraint solving abilities.

= Translation from B to TLA+ =

TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

= Limitations =
The following constructs are currently not supported by the TLC4B translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)

= Visited States =
Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this issue:

MACHINE NumberOfStates
CONSTANTS k
PROPERTIES
k : 1..10
VARIABLES x
INVARIANT
x : 1..10
INITIALISATION x:=k
END

ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):
[[File:NumberOfStates.jpeg|800px|left|State space generated by ProB]]

TLC will only report 10 distinct states (10 initialization states).

= More Information =
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].

TLC

2014-11-10T10:09:08Z

Dominik Hansen: /* Visited States */

As of version 1.4.0, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker.

= Download and Installation =

TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].
To use TLC in the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.

[[File:Download_TLA_Tools.png|400px|center]]

= How to use TLC =

First you have to open a B specification in the ProB GUI.
Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.

[[File:Model_Checking_With_TLC.png|400px|center]]

You can use TLC to find the following kinds of errors in the B specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations

In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.

[[File:Model_Checking_With_TLC_Trace.png|400px|center]]

= When to use TLC =
TLC is extremely valuable when it comes to explicit state model checking for large state spaces.
Otherwise, TLC has no constraint solving abilities.

= Translation from B to TLA+ =

TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

= Limitations =
The following constructs are currently not supported by the TLC4B translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)

= Visited States =
Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this issue:

MACHINE NumberOfStates
CONSTANTS k
PROPERTIES
k : 1..10
VARIABLES x
INVARIANT
x : 1..10
INITIALISATION x:=k
END

ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):
[[File:NumberOfStates.jpeg|800px|left|State space generated by ProB]]

TLC will only report 10 distinct states (10 initialization states).

= More Information =
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].

TLC

2014-11-10T10:06:55Z

Dominik Hansen: /* Visited States */

As of version 1.4.0, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker.

= Download and Installation =

TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].
To use TLC in the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.

[[File:Download_TLA_Tools.png|400px|center]]

= How to use TLC =

First you have to open a B specification in the ProB GUI.
Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.

[[File:Model_Checking_With_TLC.png|400px|center]]

You can use TLC to find the following kinds of errors in the B specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations

In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.

[[File:Model_Checking_With_TLC_Trace.png|400px|center]]

= When to use TLC =
TLC is extremely valuable when it comes to explicit state model checking for large state spaces.
Otherwise, TLC has no constraint solving abilities.

= Translation from B to TLA+ =

TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

= Limitations =
The following constructs are currently not supported by the TLC4B translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)

= Visited States =
Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this issue:

MACHINE NumberOfStates
CONSTANTS k
PROPERTIES
k : 1..10
VARIABLES x
INVARIANT
x : 1..10
INITIALISATION x:=k
END

ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):
[[File:NumberOfStates.jpeg|800px|left|State space generated by ProB]]
TLC will only report 10 distinct states (10 initialization states).

= More Information =
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].

File:NumberOfStates.jpeg

2014-11-10T10:06:31Z

Dominik Hansen: uploaded a new version of "File:NumberOfStates.jpeg"

TLC

2014-11-10T10:02:39Z

Dominik Hansen: /* Visited States */

As of version 1.4.0, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker.

= Download and Installation =

TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].
To use TLC in the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.

[[File:Download_TLA_Tools.png|400px|center]]

= How to use TLC =

First you have to open a B specification in the ProB GUI.
Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.

[[File:Model_Checking_With_TLC.png|400px|center]]

You can use TLC to find the following kinds of errors in the B specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations

In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.

[[File:Model_Checking_With_TLC_Trace.png|400px|center]]

= When to use TLC =
TLC is extremely valuable when it comes to explicit state model checking for large state spaces.
Otherwise, TLC has no constraint solving abilities.

= Translation from B to TLA+ =

TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

= Limitations =
The following constructs are currently not supported by the TLC4B translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)

= Visited States =
Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this issue:

MACHINE NumberOfStates
CONSTANTS k
PROPERTIES
k : 1..10
VARIABLES x
INVARIANT
x : 1..10
INITIALISATION x:=1
END

ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):
[[File:NumberOfStates.jpeg|1000px|thumb|left|State space generated by ProB]]
TLC will only report 10 distinct states (10 initialization states).

= More Information =
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].

TLC

2014-11-10T10:01:34Z

Dominik Hansen: /* Visited States */

As of version 1.4.0, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker.

= Download and Installation =

TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].
To use TLC in the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.

[[File:Download_TLA_Tools.png|400px|center]]

= How to use TLC =

First you have to open a B specification in the ProB GUI.
Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.

[[File:Model_Checking_With_TLC.png|400px|center]]

You can use TLC to find the following kinds of errors in the B specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations

In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.

[[File:Model_Checking_With_TLC_Trace.png|400px|center]]

= When to use TLC =
TLC is extremely valuable when it comes to explicit state model checking for large state spaces.
Otherwise, TLC has no constraint solving abilities.

= Translation from B to TLA+ =

TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

= Limitations =
The following constructs are currently not supported by the TLC4B translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)

= Visited States =
Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this issue:

MACHINE NumberOfStates
CONSTANTS k
PROPERTIES
k : 1..10
VARIABLES x
INVARIANT
x : 1..10
INITIALISATION x:=1
END

ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):
[[File:NumberOfStates.jpeg|200px|thumb|left|State space generated by ProB]]
TLC will report 10 states (10 initialization states).

= More Information =
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].

TLC

2014-11-10T10:00:20Z

Dominik Hansen: /* Visited States */

As of version 1.4.0, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker.

= Download and Installation =

TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].
To use TLC in the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.

[[File:Download_TLA_Tools.png|400px|center]]

= How to use TLC =

First you have to open a B specification in the ProB GUI.
Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.

[[File:Model_Checking_With_TLC.png|400px|center]]

You can use TLC to find the following kinds of errors in the B specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations

In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.

[[File:Model_Checking_With_TLC_Trace.png|400px|center]]

= When to use TLC =
TLC is extremely valuable when it comes to explicit state model checking for large state spaces.
Otherwise, TLC has no constraint solving abilities.

= Translation from B to TLA+ =

TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

= Limitations =
The following constructs are currently not supported by the TLC4B translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)

= Visited States =
Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this issue:

MACHINE NumberOfStates
CONSTANTS k
PROPERTIES
k : 1..10
VARIABLES x
INVARIANT
x : 1..10
INITIALISATION x:=1
END

ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):
[[File:NumberOfStates.jpeg]]
TLC will report 10 states (10 initialization states).

= More Information =
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].

File:NumberOfStates.jpeg

2014-11-10T10:00:01Z

Dominik Hansen:

File:NumberOfStates.pdf

2014-11-10T09:54:39Z

Dominik Hansen:

TLC

2014-11-10T09:51:51Z

Dominik Hansen: /* Visited States */

As of version 1.4.0, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker.

= Download and Installation =

TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].
To use TLC in the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.

[[File:Download_TLA_Tools.png|400px|center]]

= How to use TLC =

First you have to open a B specification in the ProB GUI.
Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.

[[File:Model_Checking_With_TLC.png|400px|center]]

You can use TLC to find the following kinds of errors in the B specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations

In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.

[[File:Model_Checking_With_TLC_Trace.png|400px|center]]

= When to use TLC =
TLC is extremely valuable when it comes to explicit state model checking for large state spaces.
Otherwise, TLC has no constraint solving abilities.

= Translation from B to TLA+ =

TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

= Limitations =
The following constructs are currently not supported by the TLC4B translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)

= Visited States =
Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this issue:

MACHINE NumberOfStates
CONSTANTS k
PROPERTIES
k : 1..10
VARIABLES x
INVARIANT
x : 1..10
INITIALISATION x:=1
END

ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states).
TLC will report 10 states (10 initialization states).

= More Information =
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].

TLC

2014-11-10T09:47:19Z

Dominik Hansen:

As of version 1.4.0, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker.

= Download and Installation =

TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].
To use TLC in the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.

[[File:Download_TLA_Tools.png|400px|center]]

= How to use TLC =

First you have to open a B specification in the ProB GUI.
Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.

[[File:Model_Checking_With_TLC.png|400px|center]]

You can use TLC to find the following kinds of errors in the B specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations

In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.

[[File:Model_Checking_With_TLC_Trace.png|400px|center]]

= When to use TLC =
TLC is extremely valuable when it comes to explicit state model checking for large state spaces.
Otherwise, TLC has no constraint solving abilities.

= Translation from B to TLA+ =

TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

= Limitations =
The following constructs are currently not supported by the TLC4B translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)

= Visited States =
Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this issue:

MACHINE NumberOfStates
CONSTANTS k
PROPERTIES
k : 1..10
VARIABLES x
INVARIANT
x : 1..10
INITIALISATION x:=1
END

= More Information =
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].

Team

2014-10-31T13:42:27Z

Dominik Hansen:

ProB is based in research and implemention effort by:
* [http://www.stups.uni-duesseldorf.de/~leuschel/ Michael Leuschel],
* Michael Butler,
* [http://www.stups.uni-duesseldorf.de/w/Jens_Bendisposto Jens Bendisposto],
* [http://www.stups.uni-duesseldorf.de/w/Daniel_Plagge Daniel Plagge],
* [http://www.stups.uni-duesseldorf.de/w/Lukas_Ladenberger Lukas Ladenberger],
* [http://www.stups.uni-duesseldorf.de/w/Ivaylo_Miroslavov_Dobrikov Ivaylo Dobrikov],
* [http://www.stups.uni-duesseldorf.de/w/Marc_Fontaine Marc Fontaine],
* [http://www.stups.uni-duesseldorf.de/w/Fabian_Fritz Fabian Fritz],
* [http://www.stups.uni-duesseldorf.de/w/Corinna_Spermann Corina Spermann],
* [http://www.stups.uni-duesseldorf.de/w/Michael_Jastram Michael Jastram],
* [http://www.stups.uni-duesseldorf.de/w/Dominik_Hansen Dominik Hansen],
* [http://www.stups.uni-duesseldorf.de/w/Sebastian_Krings Sebastian Krings],
* Philipp Körner,
* Joy Clark,
* Edward Turner,
* Dennis Winter,
* Sonja Holl,
* Jens Krüger,
* Michael Birkhoff,
* Carla Ferreira,
* Stéphane Lo Presti,
* Leonid Mikhailov,
* Laksono Adhianto, ...

ABZ14

2014-10-28T12:22:06Z

Dominik Hansen:

{{DISPLAYTITLE:ABZ 2014 Case Study}}
__NOTOC__
This page provides additional resources for the paper we have submitted for the [http://www.irit.fr/ABZ2014/casestudy.html ABZ 2014 case study track].
The full description of the case study can be found [[Media:landing_system.pdf|here]].

=== ProB Live Visualization (click to join) ===
<html><a href="http://cobra.cs.uni-duesseldorf.de:8083/bms/0d7c3566-40f0-4cc0-bfff-c1425dab219e/landinggear.html">
<img src="http://www.stups.uni-duesseldorf.de/ProB/images/7/7b/Landing_gear.png" width="600" /><a>
</html>

=== ProB BMotion Studio Video ===
{{#ev:youtube|wFr_pEjbpqo|640}}

=== Resources ===
* [http://www.stups.hhu.de/w/Special:Publication/abz14casestudy Case Study Paper]
* [[Media:LandingGear.zip|Landing Gear Model EventB Model]]

=== Links ===
* [https://github.com/bendisposto/prob2 ProB 2.0 Sourcecode]
* [http://nightly.cobra.cs.uni-duesseldorf.de/experimental/updatesite/ ProB 2.0 Nightly Build Updatesite]
* [[Tutorial13|ProB 2.0 Tutorial]]
* [[ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example|BMotionStudio Simple Example]]

File:Landing system.pdf

2014-10-28T12:19:11Z

Dominik Hansen: Landing Gear Requirements Document

Landing Gear Requirements Document

ABZ14

2014-10-28T12:03:20Z

Dominik Hansen: /* Ressources */

{{DISPLAYTITLE:ABZ 2014 Case Study}}
__NOTOC__
This page provides additional resources for the paper we have submitted for the [http://www.irit.fr/ABZ2014/casestudy.html ABZ 2014 case study track].
The full description of the case study can be found [http://www.irit.fr/ABZ2014/landing_system.pdf here].

=== ProB Live Visualization (click to join) ===
<html><a href="http://cobra.cs.uni-duesseldorf.de:8083/bms/0d7c3566-40f0-4cc0-bfff-c1425dab219e/landinggear.html">
<img src="http://www.stups.uni-duesseldorf.de/ProB/images/7/7b/Landing_gear.png" width="600" /><a>
</html>

=== ProB BMotion Studio Video ===
{{#ev:youtube|wFr_pEjbpqo|640}}

=== Resources ===
* [http://www.stups.hhu.de/w/Special:Publication/abz14casestudy Case Study Paper]
* [[Media:LandingGear.zip|Landing Gear Model EventB Model]]

=== Links ===
* [https://github.com/bendisposto/prob2 ProB 2.0 Sourcecode]
* [http://nightly.cobra.cs.uni-duesseldorf.de/experimental/updatesite/ ProB 2.0 Nightly Build Updatesite]
* [[Tutorial13|ProB 2.0 Tutorial]]
* [[ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example|BMotionStudio Simple Example]]

TLC

2014-10-17T08:40:33Z

Dominik Hansen: /* Limitations */

As of version 1.3.7-beta, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications.

= Download and Installation =

TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License].
To use TLC in the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.

[[File:Download_TLA_Tools.png|400px|center]]

= How to use TLC =

First you have to open a B specification in the ProB GUI.
Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.

[[File:Model_Checking_With_TLC.png|400px|center]]

You can use TLC to find the following kinds of errors in the B specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations

In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.

[[File:Model_Checking_With_TLC_Trace.png|400px|center]]

= When to use TLC =
TLC is extremely valuable when it comes to explicit state model checking for large state spaces.
Otherwise, TLC has no constraint solving abilities.

= Translation from B to TLA+ =

TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

= Limitations =
The following constructs are currently not supported by the TLC4B translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)