ProB Documentation - User contributions [en]

The ProB Animator and Model Checker

2014-06-03T20:00:58Z

Daniel Plagge: Added link to theory page in news

{| cellpadding="5"
|-valign="top"
|width="60%"|ProB is an animator and model checker for the [http://en.wikipedia.org/wiki/B-Method B-Method] (see the [http://www.clearsy.com/en/our-specific-know-how/b-method/?lang=en B-Method site of Clearsy]). It allows fully automatic animation of many B specifications, and can be used to systematically check a specification for range of errors. The constraint-solving capabilities of ProB can also be used for model finding, deadlock checking and test-case generation.

In addition to B, ProB now also supports [http://www.event-b.org/ Event-B], [http://en.wikipedia.org/wiki/Communicating_sequential_processes CSP-M],
[http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+], and [http://en.wikipedia.org/wiki/Z_notation Z]. ProB can be installed within [http://sourceforge.net/projects/rodin-b-sharp/ Rodin], where it comes with [http://www.stups.uni-duesseldorf.de/BMotionStudio/ BMotionStudio] to easily generate domain specific graphical visualizations.

ProB is now being used within Siemens, Alstom, and several other companies for [http://www.data-validation.fr data validation] of complicated properties. Commercial support is provided by the spin-off company [http://www.formalmind.com Formal Mind].

Part of the research and development was conducted within the [http://www.epsrc.ac.uk/default.htm EPSRC] funded projects [http://users.ecs.soton.ac.uk/phh/abcd/ ABCD] and [http://users.ecs.soton.ac.uk/mal/ISM.html iMoc], and within the EU funded project [http://rodin.cs.ncl.ac.uk/ Rodin]. Development is continued under the EU funded projects [http://www.deploy-project.eu/ Deploy] and [http://www.advance-ict.eu/ Advance] as well as the [http://www.dfg.de/ DFG] project [http://www.gepavas.de/ Gepavas].

Automatically generated test [http://nightly.cobra.cs.uni-duesseldorf.de/coverage/html/ coverage reports are available].

|width="40%" style="background:#EDF2F2;" | '''News'''
'''3/6/2014'''
ProB supports [[Event-B Theories]].

'''4/3/2013'''
[[Download|ProB 1.3.6]] is available. Highlights: improved constraint propagation for division, modulo, intervals, model checking progress bar, performance improvements, improved Kodkod backend and use within REPL, and many more.

'''8/10/2012'''
[[Download|ProB 1.3.5]] is available. Highlights: support for external and recursive functions, optional Kodkod backend, TLA+ support, performance improvements, pragmas, units inference, and many more.

'''30/03/2012'''
A first prototype of an online [[ProB_Logic_Calculator|ProB Logic Calculator]] is available.

'''21/11/2011'''
ProB 1.3.4 is available. Highlights: Evaluation View and Eval window, CSP assertion checking, improved editor, 64-bit version for Mac and Linux, performance improvements, and many more.

''' '''
[[Download#Short Release History|More in Release History]]
|}

== Implementation ==
The core of ProB is implemented in [http://www.sics.se/isl/sicstuswww/site/index.html SICStus Prolog] (but can be run without a SICStus Prolog license). The ProB constraint solver is implemented using co-routining and the CLP(FD) finite domain library of SICStus. An alternate [[Using_ProB_with_KODKOD | constraint solver based on Kodkod (and thus SAT)]] is also available within ProB, as is an alternate [[TLC|model checking engine (TLC)]] for low-level B specifications. The [[ProBLicence | ProB Licence can be found here]].

== Features ==
ProB covers a [[Summary of B Syntax|large part of B]], and we are striving towards full coverage of Atelier B and B4Free constructs. ProB supports B features such as non-deterministic operations, ANY statements, operations with complex arguments, sets, sequences, functions, lambda abstractions, set comprehensions, records, constants and properties, and many more. Not supported are the Atelier B tree operations and there are restrictions on DEFINITIONS. ProB does support multiple machines, refinements, and implementations. ProB can also be used for automated refinement checking and [[LTL Model Checking|LTL model checking]]. It also [[CSP-M|supports almost full CSP-M]] process descriptions (as of version 1.2.7), to be used on their own or to guide B machines for specification and property validation. The state space of the specifications can be [[Graphical Viewer|graphically visualized]].
ProB also supports Z specifications (ProB in this context is sometimes called [[ProZ]]) as well as [[TLA|TLA+ specifications]]. We now also have an online [[ProB Logic Calculator]].

Template:User Manual Index

2014-06-03T19:58:24Z

Daniel Plagge:

* [[Installation]]
* [[Current Limitations]]
* [[General Presentation (tcl/tk)]]
* [[Graphical Viewer]]
* [[Graphical Visualization]]
* [[State Space Visualization]]
* [[Consistency Checking]]
* [[Constraint Based Checking]]
* [[Refinement Checking]]
* [[LTL Model Checking]]
* [[Using ProB with Atelier B]]
* [[CSP-M|Using CSP-M in ProB]]
* [[Event-B Theories|Using ProB for Event-B with the theory plug-in]]
* [[ProZ|Using ProZ for Animation and Model Checking of Z Specifications]]
* [[TLA|Using ProB for TLA Specifications]]
* [[TLC|Using TLC for B Specifications]]
* [[Other languages|Using ProB with Promela and other languages]]
* [[Symmetry Reduction]]
* [[Recursively Defined Functions]]
* [[External Functions]]
* [[Test Case Generation]]
* [[Using ProB with KODKOD]]
* [[FAQ]]
* [[Troubleshooting]]
* [[Tips: Writing Models for ProB]]
* [[Using the Command-Line Version of ProB]]
* [[Summary of B Syntax]]

Event-B Theories

2014-06-03T19:57:21Z

Daniel Plagge: /* Tagging operators */

ProB has (limited) support for theories.

Currently supported are (examples refer to the theory project below):
* recursive datatypes (e.g. the List datatype)
* operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
* special annotated operators (see below)

Axiomatically defined operators are not supported without additional annotations.

== Download Theories ==

An example project with theories: [[media:theories2.zip]]

The project contains the following theories:
; SUMandPRODUCT
: Contains two operators SUM and PRODUCT which take a set of the type POW(T**INT) as argument (with T being a type variable) and return the sum (resp.) product of all element's integer value.
The operators are annotated such that ProB uses an extra implementation.
; Seq
: The theory of sequences provides operators for sequences that are defined by direct definitions, thus supported by ProB.
; Real (unsupported)
: A theory of real numbers, currently unsupported by ProB.
; Natural
: A theory of inductive naturals (defined by a constant zero and a successor function).
The mkinat operator is annotated such that ProB uses an explicit implementation.
; List
: A theory of lists that are either empty or have a head and a tail
; FixPoint (not really supported)
: The theory is defined by direct definitions but they usually get so complex that ProB cannot cope with them.
; closure
: The operator for transitive closures is supported by ProB.
The operator is annotated such that ProB uses an extra implementation.
; Card (contains no operators or data types)
: Contains theorem about set cardinalities.
; BoolOps
: Operators on Booleans (e.g. AND, OR) are defined by direct definitions and as such supported by ProB.
; BinaryTree
: Binary Trees are supported by ProB.

== Tagging operators ==

<div style="background-color:yellow;border-width:thin;border-style:dashed;padding:5pt">'''Please note:''' The use of these tags is for experts only. Normally such annotations are delivered with a theory. If you think ProB should provide specific support for a theory, please contact us.
</div>

ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator.
Such tags are given in a .ptm file ('''P'''roB '''T'''heory '''M'''apping). The file must have the same name as the theory.

For each annotated operator, the file contains a line of the form
operator '''Name''' internal {'''Tag'''}
where '''Name''' is the name of the operator in the theory and '''Tag''' is a ProB internal name.

Currently are the following tags supported (with T being an arbitrary type):
{| class="wikitable"
! Tag || Description || Expected type || Return type
|-
| closure1 || the transitive closure || POW(T**T) || POW(T**T)
|-
| SIGMA || the sum of a set || POW(T**INT) || INT
|-
| PI || the product of a set || POW(T**INT) || INT
|-
| mu || returns the element of a singleton set || POW(T) || T
|-
| choose || returns (deterministically) one element of a non-emtpy set || POW(T) || T
|-
| mkinat(zero,succ) || returns an inductive natural number where zero and succ are the two operators of a natural number datatype with zero having no args and succ having one arg (an inductive natural) || INT || Inductive Nat
|}

Event-B Theories

2014-06-03T19:52:19Z

Daniel Plagge: /* Tagging operators */

ProB has (limited) support for theories.

Currently supported are (examples refer to the theory project below):
* recursive datatypes (e.g. the List datatype)
* operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
* special annotated operators (see below)

Axiomatically defined operators are not supported without additional annotations.

== Download Theories ==

An example project with theories: [[media:theories2.zip]]

The project contains the following theories:
; SUMandPRODUCT
: Contains two operators SUM and PRODUCT which take a set of the type POW(T**INT) as argument (with T being a type variable) and return the sum (resp.) product of all element's integer value.
The operators are annotated such that ProB uses an extra implementation.
; Seq
: The theory of sequences provides operators for sequences that are defined by direct definitions, thus supported by ProB.
; Real (unsupported)
: A theory of real numbers, currently unsupported by ProB.
; Natural
: A theory of inductive naturals (defined by a constant zero and a successor function).
The mkinat operator is annotated such that ProB uses an explicit implementation.
; List
: A theory of lists that are either empty or have a head and a tail
; FixPoint (not really supported)
: The theory is defined by direct definitions but they usually get so complex that ProB cannot cope with them.
; closure
: The operator for transitive closures is supported by ProB.
The operator is annotated such that ProB uses an extra implementation.
; Card (contains no operators or data types)
: Contains theorem about set cardinalities.
; BoolOps
: Operators on Booleans (e.g. AND, OR) are defined by direct definitions and as such supported by ProB.
; BinaryTree
: Binary Trees are supported by ProB.

== Tagging operators ==

'''Please note:''' The use of these tags is for experts only. Normally such annotations are delivered with a theory. If you think ProB should provide specific support for a theory, please contact us.

ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator.
Such tags are given in a .ptm file ('''P'''roB '''T'''heory '''M'''apping). The file must have the same name as the theory.

For each annotated operator, the file contains a line of the form
operator '''Name''' internal {'''Tag'''}
where '''Name''' is the name of the operator in the theory and '''Tag''' is a ProB internal name.

Currently are the following tags supported (with T being an arbitrary type):
{| class="wikitable"
! Tag || Description || Expected type || Return type
|-
| closure1 || the transitive closure || POW(T**T) || POW(T**T)
|-
| SIGMA || the sum of a set || POW(T**INT) || INT
|-
| PI || the product of a set || POW(T**INT) || INT
|-
| mu || returns the element of a singleton set || POW(T) || T
|-
| choose || returns (deterministically) one element of a non-emtpy set || POW(T) || T
|-
| mkinat(zero,succ) || returns an inductive natural number where zero and succ are the two operators of a natural number datatype with zero having no args and succ having one arg (an inductive natural) || INT || Inductive Nat
|}

Event-B Theories

2014-06-03T19:41:56Z

Daniel Plagge: /* Tagging operators */

ProB has (limited) support for theories.

Currently supported are (examples refer to the theory project below):
* recursive datatypes (e.g. the List datatype)
* operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
* special annotated operators (see below)

Axiomatically defined operators are not supported without additional annotations.

== Download Theories ==

An example project with theories: [[media:theories2.zip]]

The project contains the following theories:
; SUMandPRODUCT
: Contains two operators SUM and PRODUCT which take a set of the type POW(T**INT) as argument (with T being a type variable) and return the sum (resp.) product of all element's integer value.
The operators are annotated such that ProB uses an extra implementation.
; Seq
: The theory of sequences provides operators for sequences that are defined by direct definitions, thus supported by ProB.
; Real (unsupported)
: A theory of real numbers, currently unsupported by ProB.
; Natural
: A theory of inductive naturals (defined by a constant zero and a successor function).
The mkinat operator is annotated such that ProB uses an explicit implementation.
; List
: A theory of lists that are either empty or have a head and a tail
; FixPoint (not really supported)
: The theory is defined by direct definitions but they usually get so complex that ProB cannot cope with them.
; closure
: The operator for transitive closures is supported by ProB.
The operator is annotated such that ProB uses an extra implementation.
; Card (contains no operators or data types)
: Contains theorem about set cardinalities.
; BoolOps
: Operators on Booleans (e.g. AND, OR) are defined by direct definitions and as such supported by ProB.
; BinaryTree
: Binary Trees are supported by ProB.

== Tagging operators ==

'''Please note:''' The use of these tags is for experts only. Normally such annotations are delivered with a theory. If you think ProB should provide specific support for a theory, please contact us.

ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator.
Such tags are given in a .ptm file ('''P'''roB '''T'''heory '''M'''apping). The file must have the same name as the theory.

For each annotated operator, the file contains a line of the form
operator '''Name''' internal {'''Tag'''}
where '''Name''' is the name of the operator in the theory and '''Tag''' is a ProB internal name.

Currently are the following tags supported (with T being an arbitrary type):
{| class="wikitable"
! Tag || Description || Expected type || Return type
|-
| closure1 || the transitive closure || POW(T**T) || POW(T**T)
|-
| SIGMA || the sum of a set || POW(T**INT) || INT
|-
| PI || the product of a set || POW(T**INT) || INT
|-
| mu || returns the element of a singleton set || POW(T) || T
|-
| choose || returns (deterministically) one element of a non-emtpy set || POW(T) || T
|-
| mkinat(zero,succ) || returns an inductive natural number where zero and succ are the two operators of a natural number datatype with zero having no args and succ having one arg (an inductive natural) || INT || Inductive Nat
|}

Event-B Theories

2014-06-03T19:41:14Z

Daniel Plagge: /* Download Theories */

ProB has (limited) support for theories.

Currently supported are (examples refer to the theory project below):
* recursive datatypes (e.g. the List datatype)
* operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
* special annotated operators (see below)

Axiomatically defined operators are not supported without additional annotations.

== Download Theories ==

An example project with theories: [[media:theories2.zip]]

The project contains the following theories:
; SUMandPRODUCT
: Contains two operators SUM and PRODUCT which take a set of the type POW(T**INT) as argument (with T being a type variable) and return the sum (resp.) product of all element's integer value.
The operators are annotated such that ProB uses an extra implementation.
; Seq
: The theory of sequences provides operators for sequences that are defined by direct definitions, thus supported by ProB.
; Real (unsupported)
: A theory of real numbers, currently unsupported by ProB.
; Natural
: A theory of inductive naturals (defined by a constant zero and a successor function).
The mkinat operator is annotated such that ProB uses an explicit implementation.
; List
: A theory of lists that are either empty or have a head and a tail
; FixPoint (not really supported)
: The theory is defined by direct definitions but they usually get so complex that ProB cannot cope with them.
; closure
: The operator for transitive closures is supported by ProB.
The operator is annotated such that ProB uses an extra implementation.
; Card (contains no operators or data types)
: Contains theorem about set cardinalities.
; BoolOps
: Operators on Booleans (e.g. AND, OR) are defined by direct definitions and as such supported by ProB.
; BinaryTree
: Binary Trees are supported by ProB.

== Tagging operators ==

'''Please note:''' The use of these tags is usually for experts only. Normally such annotations are delivered with a theory. If you think ProB should provide specific support for a theory, please contact us.

ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator.
Such tags are given in a .ptm file ('''P'''roB '''T'''heory '''M'''apping). The file must have the same name as the theory.

For each annotated operator, the file contains a line of the form
operator '''Name''' internal {'''Tag'''}
where '''Name''' is the name of the operator in the theory and '''Tag''' is a ProB internal name.

Currently are the following tags supported (with T being an arbitrary type):
{| class="wikitable"
! Tag || Description || Expected type || Return type
|-
| closure1 || the transitive closure || POW(T**T) || POW(T**T)
|-
| SIGMA || the sum of a set || POW(T**INT) || INT
|-
| PI || the product of a set || POW(T**INT) || INT
|-
| mu || returns the element of a singleton set || POW(T) || T
|-
| choose || returns (deterministically) one element of a non-emtpy set || POW(T) || T
|-
| mkinat(zero,succ) || returns an inductive natural number where zero and succ are the two operators of a natural number datatype with zero having no args and succ having one arg (an inductive natural) || INT || Inductive Nat
|}

Event-B Theories

2014-06-03T19:28:46Z

Daniel Plagge: /* Tagging operators */

Event-B Theories

2014-06-03T19:19:38Z

Daniel Plagge: Created page with 'ProB has (limited) support for theories. Currently supported are (examples refer to the theory project below): * recursive datatypes (e.g. the List datatype) * operators defined…'

Event-B

2014-06-02T13:20:16Z

Daniel Plagge: /* Tagging operators */

ProB supports animation and model-checking for Event-B specifications.

== Installation ==
To install the ProB plugin for [http://www.event-b.org Rodin], open the "Help" menu in Rodin and click "Install new software".

You see a drop-down list titled "Work with:" at the top of the install dialog. Choose the update site "ProB - ..." and click on "ProB for rodin2" in the field below. Click on the "Next" button at the button on the dialog and proceed with the installation as usual.

Alternativaly, one can use the Tcl/Tk version of ProB but Event-B models must be exported to an .eventb file first (see below).

== Animation and Modelchecking ==
You can start animation of a model (machine or context) by right-clicking on the model in the Event-B explorer. Choose "Start Animation / Model Checking".

'''TODO:''' Here we should add more details about the ProB perspective and views.

== Export for use with the Tcl/Tk version of ProB ==
You can export a model (machine or context) to an .eventb - file by right-clicking on the model in the Event-B explorer. You can find the corresponding menu item right below the animation item.

Such a .eventb file can be opened by the command line and Tcl/Tk version of ProB.

== Theories ==
ProB has (limited) support for theories.

Currently supported are (examples refer to the theory project below):
* recursive datatypes (e.g. the List datatype)
* operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
* special annotated operators (see below)

Axiomatically defined operators are not supported without additional annotations.

=== Tagging operators ===

ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator.
Such tags are given in a .ptm file ('''P'''roB '''T'''heory '''M'''apping). The file must have the same name as the theory.

For each annotated operator, the file contains a line of the form
operator '''Name''' internal {'''Tag'''}
where '''Name''' is the name of the operator in the theory and '''Tag''' is a ProB internal name.

The use of these tags is usually for experts only. In the theory file below, some of the theories are annotated.

Currently are the following tags supported:
{| class="wikitable"
! Tag || Description || Expected type
|-
| closure1 || the transitive closure || POW(T**T)
|-
| SIGMA || the sum of a set || POW(T**INT)
|-
| PI || the product of a set || POW(T**INT)
|-
| mu
|-
| choose
|-
| mkinat(op1,op2)
|}
'''TODO''': to be continued...

=== Download Theories ===

An example project with theories: [[media:theories2.zip]]

'''TODO''': A description of the supported parts.

Template:User Manual Index

2014-06-02T13:19:40Z

Daniel Plagge:

* [[Installation]]
* [[Current Limitations]]
* [[General Presentation (tcl/tk)]]
* [[Graphical Viewer]]
* [[Graphical Visualization]]
* [[State Space Visualization]]
* [[Consistency Checking]]
* [[Constraint Based Checking]]
* [[Refinement Checking]]
* [[LTL Model Checking]]
* [[Using ProB with Atelier B]]
* [[CSP-M|Using CSP-M in ProB]]
* [[Event-B|Using ProB for Event-B]]
* [[ProZ|Using ProZ for Animation and Model Checking of Z Specifications]]
* [[TLA|Using ProB for TLA Specifications]]
* [[TLC|Using TLC for B Specifications]]
* [[Other languages|Using ProB with Promela and other languages]]
* [[Symmetry Reduction]]
* [[Recursively Defined Functions]]
* [[External Functions]]
* [[Test Case Generation]]
* [[Using ProB with KODKOD]]
* [[FAQ]]
* [[Troubleshooting]]
* [[Tips: Writing Models for ProB]]
* [[Using the Command-Line Version of ProB]]
* [[Summary of B Syntax]]

File:Theories2.zip

2014-06-02T13:18:41Z

Daniel Plagge:

Event-B

2014-06-02T13:18:21Z

Daniel Plagge: /* Download Theories */

ProB supports animation and model-checking for Event-B specifications.

== Installation ==
To install the ProB plugin for [http://www.event-b.org Rodin], open the "Help" menu in Rodin and click "Install new software".

You see a drop-down list titled "Work with:" at the top of the install dialog. Choose the update site "ProB - ..." and click on "ProB for rodin2" in the field below. Click on the "Next" button at the button on the dialog and proceed with the installation as usual.

Alternativaly, one can use the Tcl/Tk version of ProB but Event-B models must be exported to an .eventb file first (see below).

== Animation and Modelchecking ==
You can start animation of a model (machine or context) by right-clicking on the model in the Event-B explorer. Choose "Start Animation / Model Checking".

'''TODO:''' Here we should add more details about the ProB perspective and views.

== Export for use with the Tcl/Tk version of ProB ==
You can export a model (machine or context) to an .eventb - file by right-clicking on the model in the Event-B explorer. You can find the corresponding menu item right below the animation item.

Such a .eventb file can be opened by the command line and Tcl/Tk version of ProB.

== Theories ==
ProB has (limited) support for theories.

Currently supported are (examples refer to the theory project below):
* recursive datatypes (e.g. the List datatype)
* operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
* special annotated operators (see below)

Axiomatically defined operators are not supported without additional annotations.

=== Tagging operators ===

ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator.
Such tags are given in a .ptm file ('''P'''roB '''T'''heory '''M'''apping). The file must have the same name as the theory.

For each annotated operator, the file contains a line of the form
operator '''Name''' internal {'''Tag'''}
where '''Name''' is the name of the operator in the theory and '''Tag''' is a ProB internal name.

The use of these tags is usually for experts only. In the theory file below, some of the theories are annotated.

Currently are the following tags supported:
{| class="wikitable"
! Tag || Description || Expected type
|-
| closure1 || the transitive closure || POW(T**T)
|-
| SIGMA || the sum of a set || POW(T**INT)
|-
| PI || the product of a set || POW(T**INT)
|-
| mu
|-
| choose
|-
| mkinat(op1,op2)
|}
TODO: to be continued...

=== Download Theories ===

An example project with theories: [[media:theories2.zip]]

'''TODO''': A description of the supported parts.

Event-B

2014-06-02T13:18:08Z

Daniel Plagge: /* Some theories */

ProB supports animation and model-checking for Event-B specifications.

== Installation ==
To install the ProB plugin for [http://www.event-b.org Rodin], open the "Help" menu in Rodin and click "Install new software".

You see a drop-down list titled "Work with:" at the top of the install dialog. Choose the update site "ProB - ..." and click on "ProB for rodin2" in the field below. Click on the "Next" button at the button on the dialog and proceed with the installation as usual.

Alternativaly, one can use the Tcl/Tk version of ProB but Event-B models must be exported to an .eventb file first (see below).

== Animation and Modelchecking ==
You can start animation of a model (machine or context) by right-clicking on the model in the Event-B explorer. Choose "Start Animation / Model Checking".

'''TODO:''' Here we should add more details about the ProB perspective and views.

== Export for use with the Tcl/Tk version of ProB ==
You can export a model (machine or context) to an .eventb - file by right-clicking on the model in the Event-B explorer. You can find the corresponding menu item right below the animation item.

Such a .eventb file can be opened by the command line and Tcl/Tk version of ProB.

== Theories ==
ProB has (limited) support for theories.

Currently supported are (examples refer to the theory project below):
* recursive datatypes (e.g. the List datatype)
* operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
* special annotated operators (see below)

Axiomatically defined operators are not supported without additional annotations.

=== Tagging operators ===

ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator.
Such tags are given in a .ptm file ('''P'''roB '''T'''heory '''M'''apping). The file must have the same name as the theory.

For each annotated operator, the file contains a line of the form
operator '''Name''' internal {'''Tag'''}
where '''Name''' is the name of the operator in the theory and '''Tag''' is a ProB internal name.

The use of these tags is usually for experts only. In the theory file below, some of the theories are annotated.

Currently are the following tags supported:
{| class="wikitable"
! Tag || Description || Expected type
|-
| closure1 || the transitive closure || POW(T**T)
|-
| SIGMA || the sum of a set || POW(T**INT)
|-
| PI || the product of a set || POW(T**INT)
|-
| mu
|-
| choose
|-
| mkinat(op1,op2)
|}
TODO: to be continued...

=== Download Theories ===

An example project with theories: [[media:theories2.zip theories2.zip]]

'''TODO''': A description of the supported parts.

Event-B

2014-06-02T13:15:43Z

Daniel Plagge: /* Theories */

Event-B

2014-06-02T13:01:53Z

Daniel Plagge: Created page with 'ProB supports animation and model-checking for Event-B specifications. == Installation == To install the ProB plugin for [http://www.event-b.org Rodin], open the "Help" menu in…'

Links

2013-01-28T08:12:23Z

Daniel Plagge: /* Miscellaneous */

__NOTOC__
== Books ==
* [http://www.jpbowen.com/publications/thes-b.html The B-Book: Assigning programs to meanings, by Jean-Raymond Abrial] (link is to a review by Jonathan Bowen)
* [http://www.palgrave.com/science/computing/schneider/ The B-Method: An Introduction, by Steve Schneider]
== Miscellaneous ==
* [http://www.stups.uni-duesseldorf.de/w/Publications:ProB ProB Publications]
* [http://en.wikipedia.org/wiki/B-Method B-Method in Wikipedia]
* [http://www.bmethod.com/ B-Method Site] from ClearSy
* [http://www.fm4industry.org/index.php/Can_FM_tools_manage_large_industrial_problems%3F Can FM tools manage large scale industrial problems ?]

== ProB ==
* [http://www.ecs.soton.ac.uk/~mal/systems/prob.html Old web page of ProB] (in Southampton; use for releases prior to 1.2)
* [http://www.fm4industry.org/index.php/Productivity_Improvement_of_Data_Consistency_in_Transportation_Models Link to Success Story (written by Cetic)]

== Tools ==
* [http://lifc.univ-fcomte.fr/~btatibouet/PERSO/JBTOOLS/InstallPlugIn/InstallPlugIn.html jbtools]
* [http://www.b4free.com/ B4Free] tools for the development of B models
* [http://www.loria.fr/~cansell/cnp.html Click n Prove]
* [http://www.event-b.org/ Event-B and Rodin Wiki] ([http://wiki.event-b.org/index.php/Rodin_Platform_Releases Rodin Platform Releases])
* [http://sourceforge.net/projects/rodin-b-sharp/ Rodin] Eclipse toolset
* [http://www.b-core.com/btoolkit.html B Toolkit]
* [http://www.ecs.soton.ac.uk/~cfs/umlb.html U2B] UML to B translation tool
* [http://www.atelierb.eu/ Atelier B]
* [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+] ([http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html tools for TLA+])

Using ProB with KODKOD

2012-10-31T13:51:19Z

Daniel Plagge: /* When is the Kokod translation used */

[[Category:User Manual]]
[[Category:Stubs]]

As of version 1.3.5 ProB can make use of [http://alloy.mit.edu/kodkod/ Kodkod] as an alternate way of solving constraints.

= How to enable Kodkod =

For the command-line version you need to call prob as follows:
probcli -p KODKOD TRUE

Note: to experiment with Kodkod you may want to try out the command:
probcli -p KODKOD TRUE -repl

For the ProB Tcl/Tk Version you should select the menu command "Enable Kodkod for Properties" in the Preferences menu.

= What can be translated =

* Types:
** Basic Types: Deferred Sets, enumerated sets, integers, booleans
** Sets of basic types
** Relations between basic types
** Higher-order types (sets of sets) are not supported

* Operators:
** Predicates: &, or, =>, <=>, not, !, #, =, /=
** Booleans: TRUE, FALSE, BOOL, bool(...)
** Sets: {..,...} {x|P}, POW, card, Cartesian product, \/, /\, -, :, /:, /<:, <<: /<<:
** Numbers: n..m, >, <, >=, <=, +, -, *, SIGMA(x).(P|x)
** Relations: <->, |->, dom, ran, id, <|, <<|, |>, |>>, ~, [...], <+, prj1, prj2, closure1
** x : S+->T, x:S-->T, ..., lambda
** currently no operations on sequences are supported

* Some limitations:
** If integers are used, a predicate can only be translated if a static analysis can estimate the interval of its possible values.
** Generally only complete predicates are translated or nothing at all, unless you set the <tt>KODKOD_ONLY_FULL</tt> preference to FALSE.

= When is the Kokod translation used =

* for solving PROPERTIES
* constraint-based assertion checking (<tt>-cbc_assertions</tt> command for <tt>probcli</tt> or the "Check Assertions on Constants" command in the menu Verify -> Constraint-Based Checking)
* constraint-based deadlock checking
* in the [[Eval Console]] in the ProB Tcl/Tk version
* for the REPL in probcli (<tt>probcli -p KODKOD TRUE -repl</tt>)

= More details =

* [http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 Plagge, Leuschel. Validating B, Z and TLA+ using ProB and Kodkod. FM'2012, LNCS 7436].

Using ProB with KODKOD

2012-10-31T13:50:46Z

Daniel Plagge: /* What can be translated */

[[Category:User Manual]]
[[Category:Stubs]]

As of version 1.3.5 ProB can make use of [http://alloy.mit.edu/kodkod/ Kodkod] as an alternate way of solving constraints.

= How to enable Kodkod =

For the command-line version you need to call prob as follows:
probcli -p KODKOD TRUE

Note: to experiment with Kodkod you may want to try out the command:
probcli -p KODKOD TRUE -repl

For the ProB Tcl/Tk Version you should select the menu command "Enable Kodkod for Properties" in the Preferences menu.

= What can be translated =

* Types:
** Basic Types: Deferred Sets, enumerated sets, integers, booleans
** Sets of basic types
** Relations between basic types
** Higher-order types (sets of sets) are not supported

* Operators:
** Predicates: &, or, =>, <=>, not, !, #, =, /=
** Booleans: TRUE, FALSE, BOOL, bool(...)
** Sets: {..,...} {x|P}, POW, card, Cartesian product, \/, /\, -, :, /:, /<:, <<: /<<:
** Numbers: n..m, >, <, >=, <=, +, -, *, SIGMA(x).(P|x)
** Relations: <->, |->, dom, ran, id, <|, <<|, |>, |>>, ~, [...], <+, prj1, prj2, closure1
** x : S+->T, x:S-->T, ..., lambda
** currently no operations on sequences are supported

* Some limitations:
** If integers are used, a predicate can only be translated if a static analysis can estimate the interval of its possible values.
** Generally only complete predicates are translated or nothing at all, unless you set the <tt>KODKOD_ONLY_FULL</tt> preference to FALSE.

= When is the Kokod translation used =

* for solving PROPERTIES
* constraint-based assertion checking (<tt>-cbc_assertions</tt> command for <tt>probcli</tt> or the "Check Assertions on Constants" command in the menu Verify -> Constraint-Based Checking)
* in the [[Eval Console]] in the ProB Tcl/Tk version
* for the REPL in probcli (<tt>probcli -p KODKOD TRUE -repl</tt>)

= More details =

* [http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 Plagge, Leuschel. Validating B, Z and TLA+ using ProB and Kodkod. FM'2012, LNCS 7436].

Using the Command-Line Version of ProB

2012-03-20T06:15:19Z

Daniel Plagge: /* -csp-guide File */

[[Category:Tutorial]]
[[Category:User Manual]]

The command-line version of ProB offers many of the feature of the standalone Tcl/Tk Version via the command-line. As such, you can run ProB from your shell scripts or in your Makefiles.
These pages refer to version 1.3.4 of ProB.

== Conventions used ==

The following conventions are used in this guide:

{| cellpadding="10"
| valign="top" | <replaceme>
| All values that should be replaced with some value are shown withing < >
|-
| valign="top" | line breaks
| Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line.
|}

== Synopsis ==

<pre>probcli [--help]
<filename> [ <options> ]</pre>

== Command-line Arguments for ProB Tcl/Tk ==

Note that the stand-alone Tcl/Tk version also supports a limited form of command-line preferences:
* '''FILE''' (the name/path of the file to be loaded)
* '''-prefs PREF_FILE''' (to use a specific preferences file, rather than the default ProB_Preferences.pl in your home folder)
* '''-batch''' (to instruct ProB not to try to bring up windows, but to print information only to the terminal)
* '''-selfcheck''' (to run the standard unit tests)
* '''-t''' (to perform the Trace Check on the default trace file associated with the specification)
* '''-tcl TCL_Command''' (to run a particular pre-defined Tcl command)
* '''-mc''' (to perform model checking)
* '''-c''' (to compute the coverage)
* '''-ref''' (to perform the default trace refinment check)

However, the comand-line version of ProB, called '''probcli''', provides more features. It also does not depend on Tcl/Tk and can therefore be run on systems without Tcl/Tk.

== Options ==

=== -mc <nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| model check; checking at most <nr> states
|}

Example

probcli my.mch -mc 100

Note: with a value of nr=1 ProB will only inspect the "virtual" root node (and compute its outgoing transitions).
Also see the related options -nodead, -noinv, -nogoal, -noass to influence which kinds of errors are reported by -mc.

=== -no<x> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| restrict errors reported by model checking with <x>=dead,inv,goal,ass
-nodead : do not report deadlocks
-noinv : do not report invariant violations
-nogoal : do not stop if a state satisfying the GOAL predicate has been found
-noass : do not report assertion violations
|}

Example

probcli my.mch -mc 1000 -nodead -nogoal

=== -bf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed breadth-first
|}

Example

probcli my.mch -bf -mc 1000

=== -df ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed depth-first
|}

Example

probcli my.mch -df -mc 1000

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

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Global imeout in ms for model checking and refinement checking.
This does not influence the timeout used for computing individual transitions/operations.
This has to be set with the -p TIME_OUT <N>. See the description of the -p option.
|}

Example

probcli my.mch -timeout 10000

=== -t ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| trace check (associated .trace file must exist)
|}

Example

probcli my.mch -t

=== -init ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| initialise specification
|}

Example

probcli my.mch -init
nr_of_components(1)
% checking_component_properties(1,[])
% enumerating_constants_without_constraints([typedval(fd(_24428,ID),global(ID),iv)])
% grounding_wait_flags
grounding_component(1)
grounding_component(2)
% found_enumeration_of_constants(0,2)
% backtrack(found_enumeration_of_constants(0,2))
% found_enumeration_of_constants(0,1)
% backtrack(found_enumeration_of_constants(0,1))
<- 0: SETUP_CONSTANTS :: root
% Could not set up constants with parameters from trace file.
% Will attempt any possible initialisation of constants.
| 0: SETUP_CONSTANTS success -->0
- <- 1: INITIALISATION :: 0
% Could not initialise with parameters from trace file.
% Will attempt any possible initialisation.
ALL OPERATIONS COVERED
- | 1: INITIALISATION success -->2
- - SUCCESS

=== -cbc <OPNAME> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| constraint-based invariant checking for an operation (also use <OPNAME>=all)
|}

Example

probcli my.mch -cbc all

=== -cbc_deadlock ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Perform constraint-based deadlock checking (also use -cbc_deadlock_pred PRED)
|}

This will try to find a state which satisfies the invariant and properties and where no operation/event is enabled.
Note: if ProB finds a counter example then the machine cannot be proven to be deadlock free. However, the particular state may not be reachable from the initial state(s). If you want to find a reachable deadlock you have to use the model checker.

=== -cbc_deadlock_pred <<PRED>> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based deadlock finding given a predicate
|}

This is like -cbc_deadlock but you provide an additional predicate. ProB will only find deadlocks which also make this predicate true.

Example

probcli my.mch -cbc_deadlock_pred "n=15"

=== -strict ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| raise error if mc finds counter example or trace checking fails
|}

Example

probcli my.mch -t -strict

=== -expcterr <ERR> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| expect error to occur (<ERR>=cbc,mc,ltl,...)
Tell ProB that you expect a certain error to occur. Mainly useful for regression tests (in conjunction with the -strict option).
|}

Example

probcli examples/B/Benchmarks/CarlaTravelAgencyErr.mch -mc 1000 -expcterr invariant_violation -strict

=== -animate <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| random animation (max Nr steps)
|}

Animates the machine randomly, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-animate_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-animate_all</tt> could run forever.

Example

probcli my.mch -animate 100

=== -det_check ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if every step of the animation is deterministic (i.e., only one operation is possible, and it can only be executed in one possible way as far as parameters and result is concerned).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -animate 100 -det_check

=== -det_constants ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if the SETUP_CONSTANTS step is deterministic (i.e., only one way to set up the constants is possible).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -init -det_constants
=== -his <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save animation history to a file
|}

Save the animation (or model checking) history to a text file. Operations are separated by semicolons.
The output can be adapted using the -his_option command. With -his_option show_states the -his command will also write out all states to the file (in the form of comments before and after operations). With -his_option show_init only the initial state is written out.
The -sptxt command is executed after the -init, -animate, -t or -mc commands.
See also the -sptxt command to only write the current values of variables and constants to a file.

Example

probcli -animate 5 -his history.txt supersimple.mch

Additionally we can have the initialised variables and constants:

probcli -animate 5 -his history.txt -his_option show_init supersimple.mch

And we can have in addition the values of the variables in between (and at the end):

probcli -animate 5 -his history.txt -his_option show_states supersimple.mch

=== -i ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| interactive animation
|}

After performing the other commands, ProB stays in interactive mode and allows the user to manually animate the loaded specification.

Example

probcli my.mch -i

=== -eval ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start interactive read-eval-loop
|}

Example

probcli my.mch -p CLPFD TRUE -eval

=== -c ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print coverage statistics
|}

Example

probcli my.mch -mc 1000 -c

=== -cc <Nr> <Nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print and check coverage statistics
Print coverage statistics and check that the given number of nodes and transitions have been computed.
|}

Example

probcli my.mch -mc 1000 -cc 10 25

=== -p <PREFERENCE> <VALUE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set <PREFERENCE> to <VALUE>. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

You can also use --pref instead of -p.
Example

probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000

=== -prefs <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set preferences from preference file <FILE>. The file should be created by the Tcl/Tk version of ProB; this version automatically creates a file called ProB_Preferences.pl. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

Example

probcli my.mch -prefs ProB_Preferences.pl

=== -card <GS> <VAL> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set scope of B deferred set
|}

Example

probcli my.mch ...

=== -goal <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set GOAL predicate for model checker
|}

Example

probcli my.mch -mc 10000000 -goal "n=18" -strict -expcterr goal_found

=== -s <PORT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on given port
|}

Example

probcli my.mch ...

=== -ss ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on port 9000
|}

Example

probcli my.mch ...

=== -sf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on some free port
|}

Example

probcli my.mch ...

=== -sptxt <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants and variables to a file
|}

Save the values of constants and variables to a text file in classical B syntax.
The -sptxt command is executed after the -init, -animate, -t or -mc commands.
The values are fully written out (some sets, e.g., infinite sets may be written out symbolically).

See also the -his command.

Example

probcli -animate 5 -sptxt state.txt supersimple.mch

This will write the values of all variables and constants to the file state.txt after animating the machine 5 steps.

=== -l <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in <LogFile>
|}

Example

probcli my.mch -mc 1000 -l my.log

=== -ll ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in /tmp/prob_cli_debug.log
|}

Example

probcli my.mch -mc 1000 -ll

=== -lg <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| analyse <LogFile> using gnuplot
|}

Example

probcli my.mch ...

=== -pp <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>
|}

Example

probcli my.mch -pp my_pp.mch

=== -ppf <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>, force printing of all type infos
|}

Example

probcli my.mch -ppf my_ppf.mch

=== -v ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set ProB into verbose mode
|}

Example

probcli my.mch -mc 1000 -v

=== -version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print version information
|}

There is also an alternate command called -svers which just prints the version number of ProB.
Example

probcli -version
ProB Command Line Interface
VERSION 1.3.4-rc1 (9556:9570M)
$LastChangedDate: 2011-11-16 18:36:18 +0100 (Wed, 16 Nov 2011) $
Prolog: SICStus 4.2.0 (x86_64-darwin-10.6.0): Mon Mar 7 20:03:36 CET 2011
Application Path: /Users/leuschel/svn_root/NewProB

probcli -svers
VERSION 1.3.4-rc1 (9556:9570M)

=== -assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check ASSERTIONS of your machine

If you provide the -t switch, the ASSERTIONS will be checked after executing your trace. Otherwise, they will be checked in an initial state.
ProB will automatically initialize the machine if you have not provide the -init or -t switch.

You can also use -main_assertions to check only the ASSERTIONS found in the main file.

If your ASSERTIONS are all static (i.e., make no reference to variables), then ProB will remove all CONSTANTS and PROPERTIES from your machine which are not linked (directly or indirectly) to the ASSERTIONS.
This optimization will only be made if you provide no other switch, such as -mc or -animate which may require the computation of the variables.
|}

Example

probcli my.mch -init -assertions

=== -properties ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check PROPERTIES
Note: you should probably first initialise the machine (e.g., with -init).
If the constants have not yet been set up, probcli will debug the properties.
|}

Example

probcli my.mch -init -properties

=== -dot_output <PATH> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| define path for generation of dot files for false properties or assertions
|}

This option is applicable to -properties and -assertions. It will result in individual dot files being generated for every false or unknown property or assertion. Assertions are numbered A0,A1,... and properties P0,P1,... You can also force to generate dot files for all properties (i.e., also the true ones) using the -dot_all command-line flag.

Example

probcli my.mch -init -properties -dot_output somewhere/

This will generate files somewhere/my_P0_false.dot, somewhere/my_P1_false.dot, ...

=== -rc ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| runtime checking of types/pre-/post-conditions
|}

Example

probcli my.mch ...

=== -ltlfile <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL formulas in file <FILE>
|}

Example

probcli my.mch ...

=== -ltlassertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL assertions (in DEFINITIONS)
|}

Example

probcli my.mch ...

=== -ltllimit <LIMIT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| explore at most <LIMIT> states when model-checking LTL
|}

Example

probcli my.mch ...

=== -save <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save state space for later refinement check
|}

Example

probcli my.mch ...

=== -refchk <FILE> ===

Description

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

Example

probcli my.mch ...

=== -mcm_tests <Depth> <MaxStates> <EndPredicate> <FILE> ===

Generate test cases for the given specification. Each test case consists of a sequence of operations resp. events (a so-called trace) that
* start in a state after an initialisation
* contain a requested operation/event
* end in a state where the <EndPredicate> is fulfilled

The user can specify what requested operations/events are with the
option [[#-mcm_cover <Operation(s)>|-mcm_cover]].

ProB uses a "breadth-first" approach to search for test cases. When all requested operations/events are covered by test cases within maximum length M, the algorithm will explore the complete state space with that maximum distance M from the initialisation. It outputs all found traces that satisfy the requirements above.

The algorithm stops if either
* it has covered all required operations/events with the current search depth
* or it has reached the maximum search depth or maximum number of explored states.

The required parameters are:
;Depth
: The maximum length of traces that the algorithm searches for test until it stops without covering all required operations/events.
;MaxStates
: The maximum number of explored states until the algorithm stops without covering all required operations/events.
;EndPredicate
: A predicate in B syntax that the last state of a trace must fulfil. If you do not have any restrictions on that state, use a trivially true predicate like '''1=1'''
;FILE
: The found test cases a written to the XML file <FILE>.

Example

probcli my.mch -mcm_tests 10 2000 "EndStateVar=TRUE" testcases.xml -mcm_cover op1,op2

generates test cases for the operations '''op1''' and '''op2''' of the specification '''my.mch'''. The maximum length of traces is 10, at most 2000 states are explored. Each test case ends in a state where the predicate '''EndStateVar=TRUE''' holds. The found test cases are written to a file '''testcases.xml'''.

=== -mcm_cover <Operation(s)> ===

Specify an operation or event that should be covered when generating test cases with the '''-mcm_test''' option. Multiple operations/events can be specified by seperating them by comma or by using '''-mcm_cover''' several times.

See [[#-mcm_tests <Depth> <MaxStates> <EndPredicate> <FILE>|-mcm-tests]] for further details.

=== -spdot <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Write graph of the state space to a dot <FILE>
|}

Example

probcli my.mch ...

=== -cb_tests Depth EndPredicate File ===
Generate test cases by constraint solving with maximum
length '''Depth''', the last state satisfies '''EndPredicate'''
and the test cases are written to '''File'''.

=== -cb_cover Operation ===
When generating CB test cases, '''Operation''' should be covered.
The option can be given multiple times to specify several operations.
Alternatively, multiple operations can be separated by a comma.

=== -test_description File ===
Read the options for constraint based test case generation from '''File'''.

=== -csp-guide File ===
Use the CSP File '''File''' to guide the B Machine ("CSP||B").
(This feature is included since version 1.3.5-beta7.)

== Preferences ==

You can use these preferences within the command:

-p <PREFERENCE> <VALUE>

{| cellpadding="5" cellspacing="1" width="100%" border="1"
!style="background-color:lightgrey;" | <PREFERENCE>
!style="background-color:lightgrey;" | <VALUE>
|-
| MAXINT
| nat ==> MaxInt, used for expressions such as xx::NAT (2147483647 for 4 byte ints)
|-
| MININT
| neg ==> MinInt, used for expressions such as xx::INT (-2147483648 for 4 byte ints)
|-
| DEFAULT_SETSIZE
| nat ==> Size of unspecified deferred sets in SETS section. Will be used if a set s is neither enumerated, has no no card(s)=nr predicate in the PROPERTIES and has no scope_s == Nr DEFINITION.
|-
| MAX_INITIALISATIONS
| nat ==> Max Number of Initialisations and ways to setup constants computed
|-
| MAX_OPERATIONS
| nat ==> Max Number of Enablings per Operation Computed
|-
| ANIMATE_SKIP_OPERATIONS
| bool ==> Animate operations which are skip or PRE C THEN skip
|-
| COMPRESSION
| bool ==> Use more aggressive COMPRESSION when storing states
|-
| EXPAND_CLOSURES_FOR_STATE
| bool ==> Convert lazy form back into explicit form for Variables, Constants, Operation Arguments. ProB will sometimes try to keep certain sets symbolic. If this preference is TRUE then ProB will try to expand those sets for variables and constants after an operation has been executed.
|-
| SYMBOLIC
| bool ==> Lazy expansion of lambdas and set comprehensions. By default ProB will keep certain sets symbolic (e.g., sets it knows are infinite). When this preference is set to TRUE then all set comprehensions and lambda abstractions will at first be kept symbolic and only expanded into explicit form if needed.
|-
| CLPFD
| bool ==> Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit computers). Setting this preference to TRUE should substantially improve ProB's ability to solve complicated predicates involving integers. However, it may cause CLP(FD) overflows in certain circumstances.
|-
| SMT
| bool ==> Enable SMT-Mode (aggressive treatment of : and /: inside predicates). With this predicate set to TRUE ProB will be better at solving certain constraint solving tasks. It should be enabled when doing constraint-based invariant or deadlock checking. ProB Tcl/Tk will turn this preference on automatically for those checks.
|-
| STATIC_ORDERING
| bool ==> Use static ordering to enumerate constants which occur in most PROPERTIES first
|-
| SYMMETRY_MODE
| [off,flood,nauty,hash] ==> Symmetry Mode: off,flood,canon,nauty,hash
|-
| TIME_OUT
| nat1 ==> Time out for computing enabled transitions (in ms)
|-
| USE_PO
| bool ==> Restrict invariant checking to affected clauses. Also remove clauses that are proven (EventB)
|-
| TRY_FIND_ABORT
| bool ==> Try more aggressively to detect ill-defined expressions (e.g. applying function outside of domain), may slow down animator
|-
| NUMBER_OF_ANIMATED_ABSTRACTIONS
| nat ==> How many levels of refined models are animated by default
|-
| ALLOW_INCOMPLETE_SETUP_CONSTANTS
| bool ==> Allow ProB to proceed even if only part of the CONSTANTS have been found.
|-
| PARTITION_PROPERTIES
| bool ==> Partition predicates (PROPERTIES) into components
|-
| USE_RECORD_CONSTRUCTION
| bool ==> Records: Check if axioms/properties describe a record pattern
|-
| OPERATION_REUSE
| bool ==> Try and reuse previously computed operation effects in B/Event-B
|-
| SHOW_EVENTB_ANY_VALUES
| bool ==> Show top-level ANY variable values of B Operations without parameters as parameters
|-
| RANDOMISE_OPERATION_ORDER
| bool ==> Randomise order of operations when computing successor states
|-
| EXPAND_FORALL_UPTO
| nat ==> When analysing predicates: max. domain size for expansion of foral
|-
| MAX_DISPLAY_SET
| int ==> Max size for pretty-printing sets (-1 means no limit)
|-
| CSP_STRIP_SOURCE_LOC
| bool ==> Strip source location for CSP; will speed up model checking
|-
| WARN_WHEN_EXPANDING_INFINITE_CLOSURES
| int ==> Warn when expanding infinite closures if MAXINT larger than:
|-
| TRACE_INFO
| bool ==> Provide various tracing information on the terminal/console.
|-
| DOUBLE_EVALUATION
| bool ==> Evaluate PREDICATES positively and negatively when analyzing assertions or properties
|-
| RECURSIVE
| bool ==> Lazy expansion of *Recursive* set Comprehensions and lambdas
|-
| IGNORE_HASH_COLLISIONS
| bool ==> Ignore Hash Collisions (if true not all states may be computed, visited states are not memorised !)
|-
| FORGET_STATE_SPACE
| bool ==> Do not remember state space (mainly useful in conjunction with Ignore Hash Collisions)
|-
| NEGATED_INVARIANT_CHECKING
| bool ==> Perform double evaluation (positive and negative) when checking invariants
|}

Example

probcli my.mch -p TIME_OUT 5000 -p CLPFD TRUE -p SYMMETRY_MODE hash -mc 1000

== Some probcli examples ==

To load a file My.mch, setup the constants and initialize it do:
<pre>
probcli -init My.mch
</pre>
To load a file M.mch, setup the constants, initialize and then check all assertions with Atelier-B's default values for MININT and MAXINT and an increased timeout of 5 seconds do:
<pre>
probcli -init -assertions -p MAXINT 2147483647 -p MININT -2147483647 -p TIME_OUT 5000 M.mch
</pre>

To model check a specification M.mch while trying to minimize memory consumption and using symmtery reduction (and accepting hash collisions) do:
<pre>
probcli -p IGNORE_HASH_COLLISIONS TRUE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -mc 999999 M.mch
</pre>

Using the Command-Line Version of ProB

2012-03-20T06:15:02Z

Daniel Plagge: /* -test_description File */

[[Category:Tutorial]]
[[Category:User Manual]]

The command-line version of ProB offers many of the feature of the standalone Tcl/Tk Version via the command-line. As such, you can run ProB from your shell scripts or in your Makefiles.
These pages refer to version 1.3.4 of ProB.

== Conventions used ==

The following conventions are used in this guide:

{| cellpadding="10"
| valign="top" | <replaceme>
| All values that should be replaced with some value are shown withing < >
|-
| valign="top" | line breaks
| Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line.
|}

== Synopsis ==

<pre>probcli [--help]
<filename> [ <options> ]</pre>

== Command-line Arguments for ProB Tcl/Tk ==

Note that the stand-alone Tcl/Tk version also supports a limited form of command-line preferences:
* '''FILE''' (the name/path of the file to be loaded)
* '''-prefs PREF_FILE''' (to use a specific preferences file, rather than the default ProB_Preferences.pl in your home folder)
* '''-batch''' (to instruct ProB not to try to bring up windows, but to print information only to the terminal)
* '''-selfcheck''' (to run the standard unit tests)
* '''-t''' (to perform the Trace Check on the default trace file associated with the specification)
* '''-tcl TCL_Command''' (to run a particular pre-defined Tcl command)
* '''-mc''' (to perform model checking)
* '''-c''' (to compute the coverage)
* '''-ref''' (to perform the default trace refinment check)

However, the comand-line version of ProB, called '''probcli''', provides more features. It also does not depend on Tcl/Tk and can therefore be run on systems without Tcl/Tk.

== Options ==

=== -mc <nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| model check; checking at most <nr> states
|}

Example

probcli my.mch -mc 100

Note: with a value of nr=1 ProB will only inspect the "virtual" root node (and compute its outgoing transitions).
Also see the related options -nodead, -noinv, -nogoal, -noass to influence which kinds of errors are reported by -mc.

=== -no<x> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| restrict errors reported by model checking with <x>=dead,inv,goal,ass
-nodead : do not report deadlocks
-noinv : do not report invariant violations
-nogoal : do not stop if a state satisfying the GOAL predicate has been found
-noass : do not report assertion violations
|}

Example

probcli my.mch -mc 1000 -nodead -nogoal

=== -bf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed breadth-first
|}

Example

probcli my.mch -bf -mc 1000

=== -df ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed depth-first
|}

Example

probcli my.mch -df -mc 1000

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

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Global imeout in ms for model checking and refinement checking.
This does not influence the timeout used for computing individual transitions/operations.
This has to be set with the -p TIME_OUT <N>. See the description of the -p option.
|}

Example

probcli my.mch -timeout 10000

=== -t ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| trace check (associated .trace file must exist)
|}

Example

probcli my.mch -t

=== -init ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| initialise specification
|}

Example

probcli my.mch -init
nr_of_components(1)
% checking_component_properties(1,[])
% enumerating_constants_without_constraints([typedval(fd(_24428,ID),global(ID),iv)])
% grounding_wait_flags
grounding_component(1)
grounding_component(2)
% found_enumeration_of_constants(0,2)
% backtrack(found_enumeration_of_constants(0,2))
% found_enumeration_of_constants(0,1)
% backtrack(found_enumeration_of_constants(0,1))
<- 0: SETUP_CONSTANTS :: root
% Could not set up constants with parameters from trace file.
% Will attempt any possible initialisation of constants.
| 0: SETUP_CONSTANTS success -->0
- <- 1: INITIALISATION :: 0
% Could not initialise with parameters from trace file.
% Will attempt any possible initialisation.
ALL OPERATIONS COVERED
- | 1: INITIALISATION success -->2
- - SUCCESS

=== -cbc <OPNAME> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| constraint-based invariant checking for an operation (also use <OPNAME>=all)
|}

Example

probcli my.mch -cbc all

=== -cbc_deadlock ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Perform constraint-based deadlock checking (also use -cbc_deadlock_pred PRED)
|}

This will try to find a state which satisfies the invariant and properties and where no operation/event is enabled.
Note: if ProB finds a counter example then the machine cannot be proven to be deadlock free. However, the particular state may not be reachable from the initial state(s). If you want to find a reachable deadlock you have to use the model checker.

=== -cbc_deadlock_pred <<PRED>> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based deadlock finding given a predicate
|}

This is like -cbc_deadlock but you provide an additional predicate. ProB will only find deadlocks which also make this predicate true.

Example

probcli my.mch -cbc_deadlock_pred "n=15"

=== -strict ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| raise error if mc finds counter example or trace checking fails
|}

Example

probcli my.mch -t -strict

=== -expcterr <ERR> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| expect error to occur (<ERR>=cbc,mc,ltl,...)
Tell ProB that you expect a certain error to occur. Mainly useful for regression tests (in conjunction with the -strict option).
|}

Example

probcli examples/B/Benchmarks/CarlaTravelAgencyErr.mch -mc 1000 -expcterr invariant_violation -strict

=== -animate <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| random animation (max Nr steps)
|}

Animates the machine randomly, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-animate_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-animate_all</tt> could run forever.

Example

probcli my.mch -animate 100

=== -det_check ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if every step of the animation is deterministic (i.e., only one operation is possible, and it can only be executed in one possible way as far as parameters and result is concerned).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -animate 100 -det_check

=== -det_constants ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if the SETUP_CONSTANTS step is deterministic (i.e., only one way to set up the constants is possible).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -init -det_constants
=== -his <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save animation history to a file
|}

Save the animation (or model checking) history to a text file. Operations are separated by semicolons.
The output can be adapted using the -his_option command. With -his_option show_states the -his command will also write out all states to the file (in the form of comments before and after operations). With -his_option show_init only the initial state is written out.
The -sptxt command is executed after the -init, -animate, -t or -mc commands.
See also the -sptxt command to only write the current values of variables and constants to a file.

Example

probcli -animate 5 -his history.txt supersimple.mch

Additionally we can have the initialised variables and constants:

probcli -animate 5 -his history.txt -his_option show_init supersimple.mch

And we can have in addition the values of the variables in between (and at the end):

probcli -animate 5 -his history.txt -his_option show_states supersimple.mch

=== -i ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| interactive animation
|}

After performing the other commands, ProB stays in interactive mode and allows the user to manually animate the loaded specification.

Example

probcli my.mch -i

=== -eval ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start interactive read-eval-loop
|}

Example

probcli my.mch -p CLPFD TRUE -eval

=== -c ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print coverage statistics
|}

Example

probcli my.mch -mc 1000 -c

=== -cc <Nr> <Nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print and check coverage statistics
Print coverage statistics and check that the given number of nodes and transitions have been computed.
|}

Example

probcli my.mch -mc 1000 -cc 10 25

=== -p <PREFERENCE> <VALUE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set <PREFERENCE> to <VALUE>. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

You can also use --pref instead of -p.
Example

probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000

=== -prefs <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set preferences from preference file <FILE>. The file should be created by the Tcl/Tk version of ProB; this version automatically creates a file called ProB_Preferences.pl. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

Example

probcli my.mch -prefs ProB_Preferences.pl

=== -card <GS> <VAL> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set scope of B deferred set
|}

Example

probcli my.mch ...

=== -goal <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set GOAL predicate for model checker
|}

Example

probcli my.mch -mc 10000000 -goal "n=18" -strict -expcterr goal_found

=== -s <PORT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on given port
|}

Example

probcli my.mch ...

=== -ss ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on port 9000
|}

Example

probcli my.mch ...

=== -sf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on some free port
|}

Example

probcli my.mch ...

=== -sptxt <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants and variables to a file
|}

Save the values of constants and variables to a text file in classical B syntax.
The -sptxt command is executed after the -init, -animate, -t or -mc commands.
The values are fully written out (some sets, e.g., infinite sets may be written out symbolically).

See also the -his command.

Example

probcli -animate 5 -sptxt state.txt supersimple.mch

This will write the values of all variables and constants to the file state.txt after animating the machine 5 steps.

=== -l <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in <LogFile>
|}

Example

probcli my.mch -mc 1000 -l my.log

=== -ll ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in /tmp/prob_cli_debug.log
|}

Example

probcli my.mch -mc 1000 -ll

=== -lg <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| analyse <LogFile> using gnuplot
|}

Example

probcli my.mch ...

=== -pp <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>
|}

Example

probcli my.mch -pp my_pp.mch

=== -ppf <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>, force printing of all type infos
|}

Example

probcli my.mch -ppf my_ppf.mch

=== -v ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set ProB into verbose mode
|}

Example

probcli my.mch -mc 1000 -v

=== -version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print version information
|}

There is also an alternate command called -svers which just prints the version number of ProB.
Example

probcli -version
ProB Command Line Interface
VERSION 1.3.4-rc1 (9556:9570M)
$LastChangedDate: 2011-11-16 18:36:18 +0100 (Wed, 16 Nov 2011) $
Prolog: SICStus 4.2.0 (x86_64-darwin-10.6.0): Mon Mar 7 20:03:36 CET 2011
Application Path: /Users/leuschel/svn_root/NewProB

probcli -svers
VERSION 1.3.4-rc1 (9556:9570M)

=== -assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check ASSERTIONS of your machine

If you provide the -t switch, the ASSERTIONS will be checked after executing your trace. Otherwise, they will be checked in an initial state.
ProB will automatically initialize the machine if you have not provide the -init or -t switch.

You can also use -main_assertions to check only the ASSERTIONS found in the main file.

If your ASSERTIONS are all static (i.e., make no reference to variables), then ProB will remove all CONSTANTS and PROPERTIES from your machine which are not linked (directly or indirectly) to the ASSERTIONS.
This optimization will only be made if you provide no other switch, such as -mc or -animate which may require the computation of the variables.
|}

Example

probcli my.mch -init -assertions

=== -properties ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check PROPERTIES
Note: you should probably first initialise the machine (e.g., with -init).
If the constants have not yet been set up, probcli will debug the properties.
|}

Example

probcli my.mch -init -properties

=== -dot_output <PATH> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| define path for generation of dot files for false properties or assertions
|}

This option is applicable to -properties and -assertions. It will result in individual dot files being generated for every false or unknown property or assertion. Assertions are numbered A0,A1,... and properties P0,P1,... You can also force to generate dot files for all properties (i.e., also the true ones) using the -dot_all command-line flag.

Example

probcli my.mch -init -properties -dot_output somewhere/

This will generate files somewhere/my_P0_false.dot, somewhere/my_P1_false.dot, ...

=== -rc ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| runtime checking of types/pre-/post-conditions
|}

Example

probcli my.mch ...

=== -ltlfile <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL formulas in file <FILE>
|}

Example

probcli my.mch ...

=== -ltlassertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL assertions (in DEFINITIONS)
|}

Example

probcli my.mch ...

=== -ltllimit <LIMIT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| explore at most <LIMIT> states when model-checking LTL
|}

Example

probcli my.mch ...

=== -save <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save state space for later refinement check
|}

Example

probcli my.mch ...

=== -refchk <FILE> ===

Description

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

Example

probcli my.mch ...

=== -mcm_tests <Depth> <MaxStates> <EndPredicate> <FILE> ===

Generate test cases for the given specification. Each test case consists of a sequence of operations resp. events (a so-called trace) that
* start in a state after an initialisation
* contain a requested operation/event
* end in a state where the <EndPredicate> is fulfilled

The user can specify what requested operations/events are with the
option [[#-mcm_cover <Operation(s)>|-mcm_cover]].

ProB uses a "breadth-first" approach to search for test cases. When all requested operations/events are covered by test cases within maximum length M, the algorithm will explore the complete state space with that maximum distance M from the initialisation. It outputs all found traces that satisfy the requirements above.

The algorithm stops if either
* it has covered all required operations/events with the current search depth
* or it has reached the maximum search depth or maximum number of explored states.

The required parameters are:
;Depth
: The maximum length of traces that the algorithm searches for test until it stops without covering all required operations/events.
;MaxStates
: The maximum number of explored states until the algorithm stops without covering all required operations/events.
;EndPredicate
: A predicate in B syntax that the last state of a trace must fulfil. If you do not have any restrictions on that state, use a trivially true predicate like '''1=1'''
;FILE
: The found test cases a written to the XML file <FILE>.

Example

probcli my.mch -mcm_tests 10 2000 "EndStateVar=TRUE" testcases.xml -mcm_cover op1,op2

generates test cases for the operations '''op1''' and '''op2''' of the specification '''my.mch'''. The maximum length of traces is 10, at most 2000 states are explored. Each test case ends in a state where the predicate '''EndStateVar=TRUE''' holds. The found test cases are written to a file '''testcases.xml'''.

=== -mcm_cover <Operation(s)> ===

Specify an operation or event that should be covered when generating test cases with the '''-mcm_test''' option. Multiple operations/events can be specified by seperating them by comma or by using '''-mcm_cover''' several times.

See [[#-mcm_tests <Depth> <MaxStates> <EndPredicate> <FILE>|-mcm-tests]] for further details.

=== -spdot <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Write graph of the state space to a dot <FILE>
|}

Example

probcli my.mch ...

=== -cb_tests Depth EndPredicate File ===
Generate test cases by constraint solving with maximum
length '''Depth''', the last state satisfies '''EndPredicate'''
and the test cases are written to '''File'''.

=== -cb_cover Operation ===
When generating CB test cases, '''Operation''' should be covered.
The option can be given multiple times to specify several operations.
Alternatively, multiple operations can be separated by a comma.

=== -test_description File ===
Read the options for constraint based test case generation from '''File'''.

=== -csp-guide File ===
Use the CSP File '''File''' to guide the B Machine ("CSP||B").

== Preferences ==

You can use these preferences within the command:

-p <PREFERENCE> <VALUE>

{| cellpadding="5" cellspacing="1" width="100%" border="1"
!style="background-color:lightgrey;" | <PREFERENCE>
!style="background-color:lightgrey;" | <VALUE>
|-
| MAXINT
| nat ==> MaxInt, used for expressions such as xx::NAT (2147483647 for 4 byte ints)
|-
| MININT
| neg ==> MinInt, used for expressions such as xx::INT (-2147483648 for 4 byte ints)
|-
| DEFAULT_SETSIZE
| nat ==> Size of unspecified deferred sets in SETS section. Will be used if a set s is neither enumerated, has no no card(s)=nr predicate in the PROPERTIES and has no scope_s == Nr DEFINITION.
|-
| MAX_INITIALISATIONS
| nat ==> Max Number of Initialisations and ways to setup constants computed
|-
| MAX_OPERATIONS
| nat ==> Max Number of Enablings per Operation Computed
|-
| ANIMATE_SKIP_OPERATIONS
| bool ==> Animate operations which are skip or PRE C THEN skip
|-
| COMPRESSION
| bool ==> Use more aggressive COMPRESSION when storing states
|-
| EXPAND_CLOSURES_FOR_STATE
| bool ==> Convert lazy form back into explicit form for Variables, Constants, Operation Arguments. ProB will sometimes try to keep certain sets symbolic. If this preference is TRUE then ProB will try to expand those sets for variables and constants after an operation has been executed.
|-
| SYMBOLIC
| bool ==> Lazy expansion of lambdas and set comprehensions. By default ProB will keep certain sets symbolic (e.g., sets it knows are infinite). When this preference is set to TRUE then all set comprehensions and lambda abstractions will at first be kept symbolic and only expanded into explicit form if needed.
|-
| CLPFD
| bool ==> Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit computers). Setting this preference to TRUE should substantially improve ProB's ability to solve complicated predicates involving integers. However, it may cause CLP(FD) overflows in certain circumstances.
|-
| SMT
| bool ==> Enable SMT-Mode (aggressive treatment of : and /: inside predicates). With this predicate set to TRUE ProB will be better at solving certain constraint solving tasks. It should be enabled when doing constraint-based invariant or deadlock checking. ProB Tcl/Tk will turn this preference on automatically for those checks.
|-
| STATIC_ORDERING
| bool ==> Use static ordering to enumerate constants which occur in most PROPERTIES first
|-
| SYMMETRY_MODE
| [off,flood,nauty,hash] ==> Symmetry Mode: off,flood,canon,nauty,hash
|-
| TIME_OUT
| nat1 ==> Time out for computing enabled transitions (in ms)
|-
| USE_PO
| bool ==> Restrict invariant checking to affected clauses. Also remove clauses that are proven (EventB)
|-
| TRY_FIND_ABORT
| bool ==> Try more aggressively to detect ill-defined expressions (e.g. applying function outside of domain), may slow down animator
|-
| NUMBER_OF_ANIMATED_ABSTRACTIONS
| nat ==> How many levels of refined models are animated by default
|-
| ALLOW_INCOMPLETE_SETUP_CONSTANTS
| bool ==> Allow ProB to proceed even if only part of the CONSTANTS have been found.
|-
| PARTITION_PROPERTIES
| bool ==> Partition predicates (PROPERTIES) into components
|-
| USE_RECORD_CONSTRUCTION
| bool ==> Records: Check if axioms/properties describe a record pattern
|-
| OPERATION_REUSE
| bool ==> Try and reuse previously computed operation effects in B/Event-B
|-
| SHOW_EVENTB_ANY_VALUES
| bool ==> Show top-level ANY variable values of B Operations without parameters as parameters
|-
| RANDOMISE_OPERATION_ORDER
| bool ==> Randomise order of operations when computing successor states
|-
| EXPAND_FORALL_UPTO
| nat ==> When analysing predicates: max. domain size for expansion of foral
|-
| MAX_DISPLAY_SET
| int ==> Max size for pretty-printing sets (-1 means no limit)
|-
| CSP_STRIP_SOURCE_LOC
| bool ==> Strip source location for CSP; will speed up model checking
|-
| WARN_WHEN_EXPANDING_INFINITE_CLOSURES
| int ==> Warn when expanding infinite closures if MAXINT larger than:
|-
| TRACE_INFO
| bool ==> Provide various tracing information on the terminal/console.
|-
| DOUBLE_EVALUATION
| bool ==> Evaluate PREDICATES positively and negatively when analyzing assertions or properties
|-
| RECURSIVE
| bool ==> Lazy expansion of *Recursive* set Comprehensions and lambdas
|-
| IGNORE_HASH_COLLISIONS
| bool ==> Ignore Hash Collisions (if true not all states may be computed, visited states are not memorised !)
|-
| FORGET_STATE_SPACE
| bool ==> Do not remember state space (mainly useful in conjunction with Ignore Hash Collisions)
|-
| NEGATED_INVARIANT_CHECKING
| bool ==> Perform double evaluation (positive and negative) when checking invariants
|}

Example

probcli my.mch -p TIME_OUT 5000 -p CLPFD TRUE -p SYMMETRY_MODE hash -mc 1000

== Some probcli examples ==

To load a file My.mch, setup the constants and initialize it do:
<pre>
probcli -init My.mch
</pre>
To load a file M.mch, setup the constants, initialize and then check all assertions with Atelier-B's default values for MININT and MAXINT and an increased timeout of 5 seconds do:
<pre>
probcli -init -assertions -p MAXINT 2147483647 -p MININT -2147483647 -p TIME_OUT 5000 M.mch
</pre>

To model check a specification M.mch while trying to minimize memory consumption and using symmtery reduction (and accepting hash collisions) do:
<pre>
probcli -p IGNORE_HASH_COLLISIONS TRUE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -mc 999999 M.mch
</pre>

CSP-M

2012-03-20T06:13:27Z

Daniel Plagge: /* Command Line option for guided CSP||B */

[[Category:User Manual]]
__NOTOC__
ProB supports machine readable CSP<ref>M. Butler and M. Leuschel: ''Combining CSP and B for specification and property verification''. FM 2005, LNCS 3582, Springer-Verlag, 2005 [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=1]</ref> as supported by FDR and ProBE. CSP files can be animated and model checked on their own simply by opening a file ending with ".csp".

You can also use a CSP file to guide a B machine by first opening the B machine and then using the "Open Special" sub-menu of the File menu:
* use CSP file: uses the CSP file to control the current B machine (see below)
* use default CSP file: trys to use a CSP with the same name as the current B machine to control it

== Limitations of CSP-M Support ==

ProB now supports FDR and ProBE compatible CSP-M syntax, with the following outstanding issues
* currying and lambda expressions have only been partially tested
* extensions and productions are not yet supported (but {| |} is)
* the priority of rename compared to external choice is unfortunately different than in FDR; please use parentheses
* mixing of closure with other set operations (especially diff) is not yet fully supported
* input patterns can only contain variables, tuples, integers and constants (ch?(x,1) is ok, ch?(y+1,x) not). Also, for a record, all arguments must be provided (e.g., for datatype r.Val.Val you have to write r?x?y you cannot write r?xy). Finally, for the moment within "ch? x.y:Set" the ":Set" associates only with y; if you want to check that "x.y" is in Set you need to write: "ch?(x.y):Set.
* channel declarations can either use associative dot tuples or non-associative tuples but not yet both. Also, sets of tuples as channel types will not work the same way as in FDR. I.e., for channel a:LinkData you should not use LinkData = {0.0, 0.1, 1.0, 1.1} but rather nametype LinkData = {0,1}.{0,1}.

Also, in the first phase we have striven for compatibility and coverage. We still need to tune the animator and model checker for efficiency (there are few known bottlenecks which will be improved, especially with deeply nested CSP synchronization constructs).

== Guiding B Machines with CSP ==

To use this feature of ProB: first open a B Machine, then select "Use CSP File to Guide B..." or "Use Default CSP File" in the "Open Special" submenu of the File menu (you must be in normal user mode to see it).

The CSP file should define a process called "MAIN".
This process will be executed in parallel with the B machine.
The synchronization between the B machine and the CSP specification is as follows:
* CSP events that have the same name as B Operations will synchronize with B; CSP events that have the same name as a B Variable or Constant can be used to inspect the current value of these, all other CSP events can happen independently of B. In CSP terms the CSP and B are composed as follows:<pre> CSP [| {op1,...,opn} |] B</pre> where op1,...,opn are the visible operations defined in the B machine.
* CSP events do not need to provide all arguments of B operations:
add!1 -> will match add(1,1) or add(1,2) or ...
(supposing add has 2 parameters in B)
add -> will match add(1,2), add(2,1), ...
add!1!2 -> will only match add(1,2)</pre>
* B Output arguments are specified at the end<pre>lookup!X!2 will match lookup(X) --> 2</pre>Note however, that for non-deterministic operations you generally should only retrieve the output value using a ? and not match against it using a !. Otherwise, the non-determinism of the B operation will be treated as an external choice for the CSP. So, if lookup is non-deterministic then we should do lookup!X?Res -> Res=2 & Cont rather than lookup!X!2 -> Cont.
* If you have a variable called vv, then you can use vv?VAL to get the value of vv. You can also use, for example, vv!X to check that the value is equal to X. If vv is a relation or function, then you can also use two values on the channel to check for particular tuples in the relation. For example, use vv!3?Y to check whether tuples (3,Y) are in the relation vv (there will be one possible synchronisation per such value).
* see the file "bookstore_guide.csp" in the provided Machines directory for an example.

For the syntax definition see [[CSP-M Syntax]]

====== Command Line option for guided CSP||B ======
From the command line, you can specify a CSP File that should be used to guide the B machine with
-csp-guide <Filename>
(This feature is included since version 1.3.5-beta7.)

== References ==
<references />

CSP-M

2012-03-20T06:09:58Z

Daniel Plagge: /* Guiding B Machines with CSP */

[[Category:User Manual]]
__NOTOC__
ProB supports machine readable CSP<ref>M. Butler and M. Leuschel: ''Combining CSP and B for specification and property verification''. FM 2005, LNCS 3582, Springer-Verlag, 2005 [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=1]</ref> as supported by FDR and ProBE. CSP files can be animated and model checked on their own simply by opening a file ending with ".csp".

You can also use a CSP file to guide a B machine by first opening the B machine and then using the "Open Special" sub-menu of the File menu:
* use CSP file: uses the CSP file to control the current B machine (see below)
* use default CSP file: trys to use a CSP with the same name as the current B machine to control it

== Limitations of CSP-M Support ==

ProB now supports FDR and ProBE compatible CSP-M syntax, with the following outstanding issues
* currying and lambda expressions have only been partially tested
* extensions and productions are not yet supported (but {| |} is)
* the priority of rename compared to external choice is unfortunately different than in FDR; please use parentheses
* mixing of closure with other set operations (especially diff) is not yet fully supported
* input patterns can only contain variables, tuples, integers and constants (ch?(x,1) is ok, ch?(y+1,x) not). Also, for a record, all arguments must be provided (e.g., for datatype r.Val.Val you have to write r?x?y you cannot write r?xy). Finally, for the moment within "ch? x.y:Set" the ":Set" associates only with y; if you want to check that "x.y" is in Set you need to write: "ch?(x.y):Set.
* channel declarations can either use associative dot tuples or non-associative tuples but not yet both. Also, sets of tuples as channel types will not work the same way as in FDR. I.e., for channel a:LinkData you should not use LinkData = {0.0, 0.1, 1.0, 1.1} but rather nametype LinkData = {0,1}.{0,1}.

Also, in the first phase we have striven for compatibility and coverage. We still need to tune the animator and model checker for efficiency (there are few known bottlenecks which will be improved, especially with deeply nested CSP synchronization constructs).

== Guiding B Machines with CSP ==

To use this feature of ProB: first open a B Machine, then select "Use CSP File to Guide B..." or "Use Default CSP File" in the "Open Special" submenu of the File menu (you must be in normal user mode to see it).

The CSP file should define a process called "MAIN".
This process will be executed in parallel with the B machine.
The synchronization between the B machine and the CSP specification is as follows:
* CSP events that have the same name as B Operations will synchronize with B; CSP events that have the same name as a B Variable or Constant can be used to inspect the current value of these, all other CSP events can happen independently of B. In CSP terms the CSP and B are composed as follows:<pre> CSP [| {op1,...,opn} |] B</pre> where op1,...,opn are the visible operations defined in the B machine.
* CSP events do not need to provide all arguments of B operations:
add!1 -> will match add(1,1) or add(1,2) or ...
(supposing add has 2 parameters in B)
add -> will match add(1,2), add(2,1), ...
add!1!2 -> will only match add(1,2)</pre>
* B Output arguments are specified at the end<pre>lookup!X!2 will match lookup(X) --> 2</pre>Note however, that for non-deterministic operations you generally should only retrieve the output value using a ? and not match against it using a !. Otherwise, the non-determinism of the B operation will be treated as an external choice for the CSP. So, if lookup is non-deterministic then we should do lookup!X?Res -> Res=2 & Cont rather than lookup!X!2 -> Cont.
* If you have a variable called vv, then you can use vv?VAL to get the value of vv. You can also use, for example, vv!X to check that the value is equal to X. If vv is a relation or function, then you can also use two values on the channel to check for particular tuples in the relation. For example, use vv!3?Y to check whether tuples (3,Y) are in the relation vv (there will be one possible synchronisation per such value).
* see the file "bookstore_guide.csp" in the provided Machines directory for an example.

For the syntax definition see [[CSP-M Syntax]]

=== Command Line option for guided CSP||B ===
From the command line, you can specify a CSP File that should be used to guide the B machine with
-csp-guide <Filename>

== References ==
<references />

Test Case Generation

2012-03-08T07:26:05Z

Daniel Plagge: /* From the command line */

[[Category:User Manual]]

Constraint based test case generation allows to explore the state space for a
machine and generate traces of operations that cover certain user defined
operations and meet a given condition to end the search.

We will use the following B Machine as an example, which is stored in a file called <tt>simplecounter.mch</tt>.

<pre>
MACHINE SimpleCounter
DEFINITIONS MAX==4
VARIABLES count
INVARIANT
count: 1..MAX
INITIALISATION count := 1
OPERATIONS
Increase(y) = PRE y: 1..(MAX-count) THEN
count := count+y
END;
Reset = BEGIN count := 1 END
END
</pre>

== How To run ==

To start the test case generation there are two alternatives. We can either provide all settings as command line arguments or in a test description file.

=== From the command line ===
From the command line there are four relevant settings to configure the test case
generation
<pre>
-cb_tests Depth EndPredicate File
generate test cases by constraint solving with maximum
length Depth, the last state satisfies EndPredicate
and the test cases are written to File

-cb_cover Operation
when generating CB test cases, Operation should be covered. Each
operation to be covered needs to be specified separately.

-p CLPFD
flag to enable the CLPFD constraint solver to search the state space, which is highly recommended.
-p TIME_OUT
time out in milliseconds to abort the exploration of each possible trace
</pre>

'''Example:'''
To generate test cases that cover the event <tt>Increase</tt> in the machine above, leading to a state where
<tt>count = MAX-1</tt> is true and the explored paths do not have a depth of more than 5 operations we would specify this as follows, where we use CLPFD and have a timeout of 2000 ms. for each explored trace:
<pre>
./probcli.sh simplecounter.mch -cb_tests 5 count=MAX-1 test_results.xml -cb_cover Increase -p CLPFD true -p TIME_OUT 2000
</pre>
The generated test cases are stored in a file called test_results.xml.

=== Test Generation Description ===
The configuration for the test case generation can also be provided as an XML file.
The format is shown below:
<pre>
<test-generation-description>
<output-file>OUTPUT FILE NAME</output-file>
<event-coverage>
<event>EVENT 1</event>
<event>EVENT 2</event>
</event-coverage>
<target>TARGET PREDICATE</target>

<parameters>

<maximum-depth>N</maximum-depth>


</parameters>
</test-generation-description>
</pre>

'''Example:'''
For our example the description file would look as follows.
<pre>
<test-generation-description>
<output-file>test_results.xml</output-file>
<event-coverage>
<event>Increase</event>
</event-coverage>
<target>count = MAX - 1</target>
<parameters>
<maximum-depth>5</maximum-depth>

<preference name="CLPFD" value="true"/>

<preference name="TIME_OUT" value="2000"/>
</parameters>
</test-generation-description>
</pre>

Assuming the test description above is stored in file named
<tt>simple_counter_test_description.xml</tt>, we start the test case generation
with the following call.
<pre>
./probcli.sh simplecounter.mch -test_description simple_counter_test_description.xml
</pre>

Colours of enabled operations

2012-01-06T08:07:06Z

Daniel Plagge:

The enabled operations are shown in different colours, depending on the state where the operation leads to.
If more than one rule of the following list apply, the first colour is taken:

; blue : The operation does not change the state (behaves like skip).
; green : The operation leads to a new, not yet explored state.
; red : The operation leads to a state where the invariant is violated.
; orange : The operation leads to a deadlock state, i.e. a state where no operation is enabled.
; black : Otherwise, the operation leads to a state that is different to the current state, has already been visited and is neither an invariant violating or deadlock state.

Colours of enabled operations

2012-01-06T07:57:57Z

Daniel Plagge: Created page with 'The enabled operations are shown in different colours, depending on the state where the operation leads to. If more than one rule of the following list apply, the first colour is…'

General Presentation (tcl/tk)

2012-01-06T07:25:21Z

Daniel Plagge: /* The ProB Main Window */

{{Template:revision}}

== The ProB Main Window ==

The menu bar contains the various commands to access the features of ProB. It includes the traditional "File" menu with a sub-menu "Recent Files" to quickly access the files previously opened in ProB. Notice the commands "Open\Save", "Reopen\Save" and "Reopen"; the latter reopens the currently opened file and reinitializes the state of the animation and the model checking processes completely. The "About" menu provides help on the tool and includes a command to check if an update is available on the ProB website. By default, ProB starts with a limited set of commands in the Beginner mode. The Normal mode gives access to more features and can be set in the menu "Preferences|User Mode".

Under the menu bar, the main window contains four panes:

* In the top pane, the specification of the B machine is displayed with the syntax highlighted and can also be edited by typing directly in this pane;
* At the bottom, the animation window is composed of three panes which display at the current point during the animation:
*# The current state of the B machine (State Properties), listing the current values of the machine variables;
*# The enabled operations (Enabled Operations), listing the operations whose preconditions and guards are true in this state (see [[Colours of enabled operations|here]] for what the different colours mean);
*# The history of operations leading to this state (History).

== Preferences ==
The "Preferences" menu allows the various features of ProB to be configured. When ProB is started for the first time, it creates a file prob_preferences.pl that stores those preferences.
* The sub-menu "Font" changes the font size of the B specification displayed in the main window.

The next three commands correspond to groups of preferences displayed in separate pop-up windows.

* The command "Animation Preferences" ... configures important aspects of ProB relative to the animation and model checking of the B specifications. These preferences influence directly the way ProB interprets the B specification and are described in "Animation and Visualisation", amongst others.

* The command "Graphical Viewer Preferences" ... allows the user to set the options of the visualization tool used by ProB and the shapes and colors used to display the nodes of the state space.

* The command "Syntax Highlight Preferences" ... allows the user to activate the syntax highlight of the B specification in the main window and also to select the various colors corresponding to the syntactic elements of the B notation.

'''IMPORTANT: Changes in the animation preferences take effect only after reloading the machine.'''

Download

2011-11-21T12:36:58Z

Daniel Plagge: 1.3.4 - final

__NOTOC__
== Latest Release ==

Note: please use the provided start scripts (StartProB.sh or StartProBWin.bat) to start ProB. On Snow Leopard (Mac OS X 10.6.x) you have to install a [http://www.activestate.com/activetcl/downloads/ corrected version of Tcl/Tk] as indicated below (the distribution provided by Apple is broken).

{| border="1"
! Platform
! Release Date
! Download
! Dependencies
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.4-final
|-
| Linux
| 21. Nov 2011
| [http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.3.4/ProB.linux32.tar.gz Tarball (32bit)], [http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.3.4/ProB.linux64.tar.gz Tarball (64bit)], 
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.5
|-
| Windows
| 21. Nov 2011
| [http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.3.4/ProB.windows.32bit.zip Zipfile (with probcli)]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, Snow Leopard, Intel
| coming soon
| 
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Mac OS X, Leopard, Intel
| 21. Nov 2011
| [http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.3.4/ProB.mac_os.10.5.8.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.3-final
|-
| Linux
| 10. Feb 2011
| [http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.3.3/ProB.linux.tar.gz Tarball (32bit)], [http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.3.3/ProB.linux64.tar.gz Tarball (64bit)], [http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.3.3/prob_1.3.3_i386.deb Ubuntu/Debian package (32bit)]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.5
|-
| Windows
| 10. Feb 2011
| [http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.3.3/ProB.windows.32bit.zip Zipfile (with probcli)]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, Snow Leopard, Intel
| 10. Feb 2011
| [http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.3.3/ProB.mac_os.10.6.6.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Mac OS X, Leopard, Intel
| 10. Feb 2011
| [http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.3.3/ProB.mac_os.10.5.8.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.2-final
|-
| Mac OS X, Tiger, Intel
| 30. Jul 2010
| [http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.3.2/ProB_tiger_intel.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.4],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.1-final
|-
| Linux
| 13. Jan 2010
| [http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.3.1final5/ProB-linux-1.3.1final5.tar.gz Tarball]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.4
|-
| Mac OS X, PPC Tiger
| 07. Dec 2009
| [http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.3.1final3/ProB-ppctiger-1.3.1final3.tar.gz Tarball]
| [http://www.tcl.tk/software/tcltk/8.5.html Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|}

== Tcl/Tk ==
Please note that Tcl/Tk 8.6 is not yet supported by SICStus Prolog. Also note that on Mac OS X you may have to reinstall Tcl/Tk using one of the links given above (because the Tcl/Tk provided by Apple crashes after opening a file using the standard file selection dialog). On Snow Leopard (Mac OS X 10.6.x) you have to install Tcl/Tk as indicated above.

== Nightly Build ==
You can download our nightly integration build from
[http://nightly.cobra.cs.uni-duesseldorf.de/tcl/ here].

The latest Tcl/Tk version of ProB requires the text module from tklib. This
should come pre-installed on Mac and often on Windows as well.
On Linux you need to install tklib. On Ubuntu just type <tt>sudo apt-get install
tklib</tt>. If you used the Active Tcl distribution, you need to type

<tt>sudo /opt/ActiveTcl-8.5/bin/teacup install tklib85</tt>

on Linux.

Recently you can use ProB with Tcl/Tk 8.5 on Windows. If you have the older
version of Tcl/Tk 8.4 you have to install the newer one
8.5 (you should be able to also keep the older version). For Windows we recommend installing [http://downloads.activestate.com/ActiveTcl/releases/ ActiveTcl-8.5] (the win32-ix86-threaded version).
ActiveTcl-8.5 installs an additional tool "Teacup", with which you can install
Tcl/Tk library extensions like <tt>tcllib</tt> and <tt>tklib</tt>.
To use the latest Tcl/Tk version of ProB may have to install tklib. This library
can be then installed on Windows with Teacup by typing

<tt>teacup install tklib85</tt>

into the Command Prompt, when you are logged in as an administrator.

== Earlier Releases ==

If you are interested in earlier releases, please have a look at the [http://nightly.cobra.cs.uni-duesseldorf.de/releases/ Download directory].

Using the Command-Line Version of ProB

2011-08-23T11:32:13Z

Daniel Plagge:

[[Category:Tutorial]]
[[Category:User Manual]]

The command-line version of ProB offers many of the feature of the standalone Tcl/Tk Version via the command-line. As such, you can run ProB from your shell scripts or in your Makefiles.

== Conventions used ==

The following conventions are used in this guide:

{| cellpadding="10"
| valign="top" | <replaceme>
| All values that should be replaced with some value are shown withing < >
|-
| valign="top" | line breaks
| Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line.
|}

== Synopsis ==

<pre>probcli [--help]
<filename> [ <options> ]</pre>

== Command-line Arguments for ProB Tcl/Tk ==

Note that the stand-alone Tcl/Tk version also supports a limited form of command-line preferences:
* '''FILE''' (the name/path of the file to be loaded)
* '''-prefs PREF_FILE''' (to use a specific preferences file, rather than the default ProB_Preferences.pl in your home folder)
* '''-batch''' (to instruct ProB not to try to bring up windows, but to print information only to the terminal)
* '''-selfcheck''' (to run the standard unit tests)
* '''-t''' (to perform the Trace Check on the default trace file associated with the specification)
* '''-tcl TCL_Command''' (to run a particular pre-defined Tcl command)
* '''-mc''' (to perform model checking)
* '''-c''' (to compute the coverage)
* '''-ref''' (to perform the default trace refinment check)

However, the comand-line version of ProB, called '''probcli''', provides more features. It also does not depend on Tcl/Tk and can therefore be run on systems without Tcl/Tk.

== Options ==

=== -mc <nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| model check; checking at most <nr> states
|}

Example

probcli my.mch ...

=== -no<x> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| restrict errors reported by model checking with <x>=dead,inv,goal,ass
-nodead : do not report deadlocks
-noinv : do not report invariant violations
-nogoal : do not stop if a state satisfying the GOAL predicate has been found
-noass : do not report assertion violations
|}

Example

probcli my.mch -mc 1000 -nodead -nogoal

=== -bf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed breadth-first
|}

Example

probcli my.mch -bf -mc 1000

=== -df ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed depth-first
|}

Example

probcli my.mch -df -mc 1000

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

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Global imeout in ms for model checking and refinement checking.
This does not influence the timeout used for computing individual transitions/operations.
This has to be set with the -p TIME_OUT <N>. See the description of the -p option.
|}

Example

probcli my.mch -timeout 10000

=== -t ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| trace check (associated .trace file must exist)
|}

Example

probcli my.mch -t

=== -init ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| initialise specification
|}

Example

probcli my.mch -init
nr_of_components(1)
% checking_component_properties(1,[])
% enumerating_constants_without_constraints([typedval(fd(_24428,ID),global(ID),iv)])
% grounding_wait_flags
grounding_component(1)
grounding_component(2)
% found_enumeration_of_constants(0,2)
% backtrack(found_enumeration_of_constants(0,2))
% found_enumeration_of_constants(0,1)
% backtrack(found_enumeration_of_constants(0,1))
<- 0: SETUP_CONSTANTS :: root
% Could not set up constants with parameters from trace file.
% Will attempt any possible initialisation of constants.
| 0: SETUP_CONSTANTS success -->0
- <- 1: INITIALISATION :: 0
% Could not initialise with parameters from trace file.
% Will attempt any possible initialisation.
ALL OPERATIONS COVERED
- | 1: INITIALISATION success -->2
- - SUCCESS

=== -cbc <OPNAME> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| constraint-based invariant checking for an operation (also use <OPNAME>=all)
|}

Example

probcli my.mch -cbc all

=== -cbc_deadlock ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| constraint-based deadlock checking (also use -cbc_deadlock_pred PRED)
|}

=== -cbc_deadlock_pred <<PRED>> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
|
|}

Example

probcli my.mch -cbc_deadlock_pred "n=15"

=== -strict ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| raise error if mc finds counter example or trace checking fails
|}

Example

probcli my.mch -t -strict

=== -expcterr <ERR> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| expect error to occur (<ERR>=cbc,mc,ltl,...)
Tell ProB that you expect a certain error to occur. Mainly useful for regression tests (in conjunction with the -strict option).
|}

Example

probcli examples/B/Benchmarks/CarlaTravelAgencyErr.mch -mc 1000 -expcterr invariant_violation -strict

=== -animate <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| random animation (max Nr steps)
|}

Animates the machine randomly, maximally Nr of steps. It will stop if a deadlock is reached.

Example

probcli my.mch -animate 100

=== -det_check ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if every step of the animation is deterministic (i.e., only one operation is possible, and it can only be executed in one possible way as far as parameters and result is concerned).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -animate 100 -det_check

=== -det_constants ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if the SETUP_CONSTANTS step is deterministic (i.e., only one way to set up the constants is possible).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -init -det_constants
=== -his <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save animation history to a file
|}

Save the animation (or model checking) history to a text file. Operations are separated by semicolons.
The output can be adapted using the -his_option command. See also the -sptxt command.

Example

probcli -animate 5 -his history.txt supersimple.mch

Additionally we can have the initialised variables and constants:

probcli -animate 5 -his history.txt -his_option show_init supersimple.mch

And we can have the values of the variables in between:

./probcli -animate 5 -his history.txt -his_option show_init -his_option show_states supersimple.mch

=== -i ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| interactive animation
|}

After performing the other commands, ProB stays in interactive mode and allows the user to manually animate the loaded specification.

Example

probcli my.mch -i

=== -eval ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start interactive read-eval-loop
|}

Example

probcli my.mch -p CLPFD TRUE -eval

=== -c ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print coverage statistics
|}

Example

probcli my.mch -mc 1000 -c

=== -cc <Nr> <Nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print and check coverage statistics
Print coverage statistics and check that the given number of nodes and transitions have been computed.
|}

Example

probcli my.mch -mc 1000 -cc 10 25

=== -p <PREFERENCE> <VALUE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set <PREFERENCE> to <VALUE>. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

You can also use --pref instead of -p.
Example

probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000

=== -prefs <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set preferences from preference file <FILE>. The file should be created by the Tcl/Tk version of ProB; this version automatically creates a file called ProB_Preferences.pl. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

Example

probcli my.mch -prefs ProB_Preferences.pl

=== -card <GS> <VAL> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set scope of B deferred set
|}

Example

probcli my.mch ...

=== -goal <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set GOAL predicate for model checker
|}

Example

probcli my.mch -mc 10000000 -goal "n=18" -strict -expcterr goal_found

=== -s <PORT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on given port
|}

Example

probcli my.mch ...

=== -ss ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on port 9000
|}

Example

probcli my.mch ...

=== -sf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on some free port
|}

Example

probcli my.mch ...

=== -sptxt <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants and variables to a file
|}

Save the values of constants and variables to a text file. See also the -his command.

Example

probcli -animate 5 -sptxt state.txt supersimple.mch

=== -l <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in <LogFile>
|}

Example

probcli my.mch -mc 1000 -l my.log

=== -ll ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in /tmp/prob_cli_debug.log
|}

Example

probcli my.mch -mc 1000 -ll

=== -lg <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| analyse <LogFile> using gnuplot
|}

Example

probcli my.mch ...

=== -pp <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>
|}

Example

probcli my.mch -pp my_pp.mch

=== -ppf <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>, force printing of all type infos
|}

Example

probcli my.mch -ppf my_ppf.mch

=== -v ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set ProB into verbose mode
|}

Example

probcli my.mch -mc 1000 -v

=== -version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print version information
|}

There is also an alternate command called -svers which just prints the version number of ProB.
Example

probcli -version
ProB Command Line Interface
VERSION 1.3.4-beta9 (8475:8485M)
$LastChangedDate: 2011-07-18 17:41:16 +0200 (Mon, 18 Jul 2011) $
Prolog: SICStus 4.2.0 (x86_64-darwin-10.6.0): Mon Mar 7 20:03:36 CET 2011
Application Path: /Users/leuschel/svn_root/NewProB

probcli -svers
VERSION 1.3.4-beta9 (8475:8485M)

=== -assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check ASSERTIONS
Note: you should probably first initialise the machine (e.g., with -init).
You can also use -main_assertions to check only the ASSERTIONS found in the main file.
|}

Example

probcli my.mch -init -assertions

=== -properties ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check PROPERTIES
Note: you should probably first initialise the machine (e.g., with -init).
If the constants have not yet been set up, probcli will debug the properties.
|}

Example

probcli my.mch -init -properties

=== -dot_output <PATH> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| define path for generation of dot files for false properties or assertions
|}

This option is applicable to -properties and -assertions. It will result in individual dot files being generated for every false or unknown property or assertion. Assertions are numbered A0,A1,... and properties P0,P1,... You can also force to generate dot files for all properties (i.e., also the true ones) using the -dot_all command-line flag.

Example

probcli my.mch -init -properties -dot_output somewhere/

This will generate files somewhere/my_P0_false.dot, somewhere/my_P1_false.dot, ...

=== -rc ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| runtime checking of types/pre-/post-conditions
|}

Example

probcli my.mch ...

=== -ltlfile <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL formulas in file <FILE>
|}

Example

probcli my.mch ...

=== -ltlassertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL assertions (in DEFINITIONS)
|}

Example

probcli my.mch ...

=== -ltllimit <LIMIT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| explore at most <LIMIT> states when model-checking LTL
|}

Example

probcli my.mch ...

=== -save <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save state space for later refinement check
|}

Example

probcli my.mch ...

=== -refchk <FILE> ===

Description

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

Example

probcli my.mch ...

=== -mcm_tests <Depth> <MaxStates> <EndPredicate> <FILE> ===

Generate test cases for the given specification. Each test case consists of a sequence of operations resp. events (a so-called trace) that
* start in a state after an initialisation
* contain a requested operation/event
* end in a state where the <EndPredicate> is fulfilled

The user can specify what requested operations/events are with the
option [[#-mcm_cover <Operation(s)>|-mcm_cover]].

ProB uses a "breadth-first" approach to search for test cases. When all requested operations/events are covered by test cases within maximum length M, the algorithm will explore the complete state space with that maximum distance M from the initialisation. It outputs all found traces that satisfy the requirements above.

The algorithm stops if either
* it has covered all required operations/events with the current search depth
* or it has reached the maximum search depth or maximum number of explored states.

The required parameters are:
;Depth
: The maximum length of traces that the algorithm searches for test until it stops without covering all required operations/events.
;MaxStates
: The maximum number of explored states until the algorithm stops without covering all required operations/events.
;EndPredicate
: A predicate in B syntax that the last state of a trace must fulfil. If you do not have any restrictions on that state, use a trivially true predicate like '''1=1'''
;FILE
: The found test cases a written to the XML file <FILE>.

Example

probcli my.mch -mcm_tests 10 2000 "EndStateVar=TRUE" testcases.xml -mcm_cover op1,op2

generates test cases for the operations '''op1''' and '''op2''' of the specification '''my.mch'''. The maximum length of traces is 10, at most 2000 states are explored. Each test case ends in a state where the predicate '''EndStateVar=TRUE''' holds. The found test cases are written to a file '''testcases.xml'''.

=== -mcm_cover <Operation(s)> ===

Specify an operation or event that should be covered when generating test cases with the '''-mcm_test''' option. Multiple operations/events can be specified by seperating them by comma or by using '''-mcm_cover''' several times.

See [[#-mcm_tests <Depth> <MaxStates> <EndPredicate> <FILE>|-mcm-tests]] for further details.

=== -spdot <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Write graph of the state space to a dot <FILE>
|}

Example

probcli my.mch ...

=== -cb_tests Depth EndPredicate File ===
Generate test cases by constraint solving with maximum
length '''Depth''', the last state satisfies '''EndPredicate'''
and the test cases are written to '''File'''.

=== -cb_cover Operation ===
When generating CB test cases, '''Operation''' should be covered.
The option can be given multiple times to specify several operations.
Alternatively, multiple operations can be separated by a comma.

=== -test_description File ===
Read the options for constraint based test case generation from '''File'''.

== Preferences ==

You can use these preferences within the command:

-p <PREFERENCE> <VALUE>

{| cellpadding="5" cellspacing="1" width="100%" border="1"
!style="background-color:lightgrey;" | <PREFERENCE>
!style="background-color:lightgrey;" | <VALUE>
|-
| MAXINT
| nat ==> MaxInt, used for expressions such as xx::NAT (2147483647 for 4 byte ints)
|-
| MININT
| neg ==> MinInt, used for expressions such as xx::INT (-2147483648 for 4 byte ints)
|-
| DEFAULT_SETSIZE
| nat ==> Size of unspecified deferred sets in SETS section
|-
| MAX_INITIALISATIONS
| nat ==> Max Number of Initialisations Computed
|-
| MAX_OPERATIONS
| nat ==> Max Number of Enablings per Operation Computed
|-
| ANIMATE_SKIP_OPERATIONS
| bool ==> Animate operations which are skip or PRE C THEN skip
|-
| EXPAND_CLOSURES_FOR_STATE
| bool ==> Convert lazy form back into explicit form for Variables, Constants, Operation Arguments
|-
| SYMBOLIC
| bool ==> Lazy expansion of lambdas and set comprehensions
|-
| CLPFD
| bool ==> Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit computers)
|-
| SMT
| bool ==> Enable SMT-Mode (aggressive treatment of : and /: inside predicates)
|-
| STATIC_ORDERING
| bool ==> Use static ordering to enumerate constants which occur in most PROPERTIES first
|-
| SYMMETRY_MODE
| [off,flood,nauty,hash] ==> Symmetry Mode: off,flood,canon,nauty,hash
|-
| TIME_OUT
| nat1 ==> Time out for computing enabled transitions (in ms)
|-
| USE_PO
| bool ==> Restrict invariant checking to affected clauses. Also remove clauses that are proven (EventB)
|-
| TRY_FIND_ABORT
| bool ==> Try more aggressively to detect ill-defined expressions (e.g. applying function outside of domain), may slow down animator
|-
| NUMBER_OF_ANIMATED_ABSTRACTIONS
| nat ==> How many levels of refined models are animated by default
|-
| ALLOW_INCOMPLETE_SETUP_CONSTANTS
| bool ==> Allow ProB to proceed even if only part of the CONSTANTS have been found.
|-
| PARTITION_PROPERTIES
| bool ==> Partition predicates (PROPERTIES) into components
|-
| USE_RECORD_CONSTRUCTION
| bool ==> Records: Check if axioms/properties describe a record pattern
|-
| OPERATION_REUSE
| bool ==> Try and reuse previously computed operation effects in B/Event-B
|-
| SHOW_EVENTB_ANY_VALUES
| bool ==> Show top-level ANY variable values of B Operations without parameters as parameters
|-
| RANDOMISE_OPERATION_ORDER
| bool ==> Randomise order of operations when computing successor states
|-
| EXPAND_FORALL_UPTO
| nat ==> When analysing predicates: max. domain size for expansion of foral
|-
| MAX_DISPLAY_SET
| int ==> Max size for pretty-printing sets (-1 means no limit)
|-
| ABSTRACT_DOMAIN_MODULE
| string ==> Module name with abstract domain and operations
|-
| USE_WIDENING
| bool ==> Use widening for abstract interpretation
|-
| SOFT_WIDENING
| bool ==> Use soft widening for every transition
|-
| HOW_MANY_STATES_FOR_WIDEN
| nat1 ==> Extrapolation threshold (Number of loop iterations until widening will be used)
|-
| WARN_WHEN_EXPANDING_INFINITE_CLOSURES
| int ==> Warn when expanding infinite closures if MAXINT larger than:
|-
| TRACE_INFO
| bool ==> Provide various tracing information on the terminal/console.
|-
| DOUBLE_EVALUATION
| bool ==> Evaluate PREDICATES positively and negatively when analysing:
|-
| RECURSIVE
| bool ==> Lazy expansion of *Recursive* set Comprehensions and lambdas
|-
| IGNORE_HASH_COLLISIONS
| bool ==> Ignore Hash Collisions (if true not all states may be computed, visited states are not memorised !)
|-
| FORGET_STATE_SPACE
| bool ==> Do not remember state space (mainly useful in conjunction with Ignore Hash Collisions)
|}

Example

probcli my.mch -p TIME_OUT 5000 -p CLPFD TRUE -p SYMMETRY_MODE hash -mc 1000

== Some probcli examples ==

To load a file My.mch, setup the constants and initialize it do:
<pre>
probcli -init My.mch
</pre>
To load a file M.mch, setup the constants, initialize and then check all assertions with Atelier-B's default values for MININT and MAXINT and an increased timeout of 5 seconds do:
<pre>
probcli -init -assertions -p MAXINT 2147483647 -p MININT -2147483647 -p TIME_OUT 5000 M.mch
</pre>

To model check a specification M.mch while trying to minimize memory consumption and using symmtery reduction (and accepting hash collisions) do:
<pre>
probcli -p IGNORE_HASH_COLLISIONS TRUE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -mc 999999 M.mch
</pre>

ProZ

2011-08-23T10:06:25Z

Daniel Plagge:

[[Category:User Manual]]__NOTOC__
ProZ is a extension of the ProB animator and model checker to support Z specifications. It uses the [http://spivey.oriel.ox.ac.uk/mike/fuzz Fuzz Type Checker] by Mike Spivey for extracting the formal specification from a LaTeX file. On the website you can also find documentation about the syntax of Z specifications.

= Preferences =
A Z specification frequently makes use of comprehension sets, which are often introduced by the underlying translation process from Z to B. Normally those comprehension sets should be treated symbolically. To support this, you should set the following in the preferences menu:
Animation Preferences ->
- Lazy expansion of lambdas & set comprehensions: True
- Convert lazy form back into explicit form for Variables and Constants: False

= Structure of the Z Specification =

== State and Initialization ==
To identify the components (like state, initialization, operations)
of a Z specification, ProZ expects a certain structure of the
specification: There must be a schema called "Init".
"Init" describes the initialization of the state.
"Init" must include exactly one schema in the declaration part. This schema is assumed to be the state schema.

For example, let S be the state schema (= is used for \defs):
S = [ x,y:N ]
There are two supported styles for the initialization:

a) Init = [ S | x=0 /\ y=1]

b) Init = [ S'| x'=0 /\ y'=1 ]

If you want to use the logic of other schemas besides the state schema
in the initialization, you can do that by including those schemas in the predicate part.

=== Operations ===

ProZ identifies schemas as operations if they satisfy the following properties:
* All variables of the state and their primed counterpart are declared in the operation. Usually this is done by including "\Delta S" in the operation (with S being the state schema).
* The operation is not referenced by any other schema in the specification

Example: Let S be defined as above:

A = [ \Delta S | x'=x+1 /\ y'=y ]
B = [ x,y,x',y':N | x'=x+1 /\ y'=y ]
C = [ x,x':N | x'=x+1 ]
D = [ y,y':N | y'=y ]
E = C /\ D
F = [ \Xi S | x=0 ]

Then the schemas A,B and E describe all the same operation. F is also identified as an operation that leaves the state unchanged.

=== Axiomatic definitions ===

If axiomatic definitions are present, the declared variables are treated like constants. In the first step of the animation, ProB searches for values that satisfy all predicates of the axiomatic definitions are searched.
After the first step, the predicates of the axiomatic definitions
are ignored.
If you want to define functions in an axiomatic definition, consider that ProB can treat lambda expressions and set comprehensions symbolically.
Example: The definition of a function "square" could be

a)
| square : Z -> Z
|-----------------------
| square = (\lambda x:Z @ x*x)

b)
| square : Z -> Z
|-----------------------
| \forall x:Z @ square x = x*x

When using ProZ, it is preferable to use the method "a" because the lambda expression can be interpreted symbolically. If "b" is used, ProB will try to find a explicit set that will satisfy the given property.

=== Invariant ===

You can add a B-style invariant to the specification by defining a schema "Invariant" that declares a subset of the state variables. In each explored state the invariant will be checked. The model checking feature of ProB will try to find states that violate the invariant.

=== Scope ===

It is possible to limit the search space of the model checker by adding a schema "Scope" that declares a subset of the state variables. If such a schema is present, each explored state is checked, if it satisfies the predicate. If not, the state is not further explored.

=== Abbreviation Definitions ===

Abbreviation definitions (e.g. Abbr == {1,2,3}) are used like macros by
ProZ. A reference to an abbreviation is replaced by its definition in
a preprocessor phase.
Thereby schemas defined by abbreviation definitions are ignored when
ProZ tries to identify components. So, it is recommended to use schema definitions instead of abbreviation definitions (\defs instead of ==) when defining state, initialization, operations, etc.

== Graphical animation ==

('''Please note that this functionality is part of the next version. If you want to use graphical animation, please download a version from the [[Download#Nightly Build|Nightly build]].''')

Analogous to the graphical animation for B specifications, you can define a function that maps a coordinate to an image.
Then ProZ will display the grid of images while animating the specification.

To use this feature, add a schema '''Proz_Settings''' that contains a variable
'''animation\_function'''. The animation function should map a coordinate to an image. A coordinate is a pair of numbers or given sets.

The type used for images must be an enumerated set where the names of the elements denote their file names (without the suffix .gif).

Please see the specification '''jars.tex''' in the examples section.

== Special constructs ==

=== prozignore ===

Sometimes it is not desired to check properties of some variables.
E.g. ProZ checks if the square function in 2.3.a is a total function by enumerating it (it checks the function only for a limited interval). For more complex definitions the number of entries is often too large to check.
When the user is sure that those properties are satisfied (like in our example), a solution is relaxing the declaration from "square : Z -> Z" to "square : Z <-> Z".
Sometimes this is not easy to do, for instance if schema types are used which imply other constraints.

ProZ supports an operation \prozignore that instructs ProZ to ignore all constraints on the type and to use just the underlying type. For example, the square function could be defined by:

| square : \prozignore( Z -> Z )
|-----------------------
| square = (\lambda x:Z @ x*x)

If you want to use \prozignore, you must first define a TeX command \prozignore:
\newcommand{\prozignore}{ignore_\textsl{\tiny ProZ}}

You can change the definition of the macro as you like because the content is ignored by ProZ. Then you must introduce a generic definition of \prozignore. The definition is ignored by ProB, but Fuzz needs it for type checking.

%%pregen \prozignore
\begin{gendef}[X]
\prozignore~\_ : \power X
\end{gendef}

It is also possible to append these lines to the "fuzzlib" in the fuzz distribution.

=== Translation to B ===

You can inspect the result of the translation process with "Show internal representation" in the "Debug" menu.
Please note that the shown B machine is normally not syntactically correct because of
* additional constructs like free types
* additional type information of the form "var:type"
* names with primes (') or question marks, etc.
* lack of support from the pretty printer for every construct

== Known Limitations ==
* Generic definitions are not supported yet.
* Miscellaneous unsupported constructs
** reflexive-transitive closure
** probably other?
* The error messages are not very helpful yet.

ProZ

2011-05-11T07:01:38Z

Daniel Plagge: /* Known Limitations */

[[Category:User Manual]]__NOTOC__
ProZ is a extension of the ProB animator and model checker to support Z specifications. It uses the [http://spivey.oriel.ox.ac.uk/mike/fuzz Fuzz Type Checker] by Mike Spivey for extracting the formal specification from a LaTeX file. On the website you can also find documentation about the syntax of Z specifications.

= Preferences =
A Z specification frequently makes use of comprehension sets, which are often introduced by the underlying translation process from Z to B. Normally those comprehension sets should be treated symbolically. To support this, you should set the following in the preferences menu:
Animation Preferences ->
- Lazy expansion of lambdas & set comprehensions: True
- Convert lazy form back into explicit form for Variables and Constants: False

= Structure of the Z Specification =

== State and Initialization ==
To identify the components (like state, initialization, operations)
of a Z specification, ProZ expects a certain structure of the
specification: There must be a schema called "Init".
"Init" describes the initialization of the state.
"Init" must include exactly one schema in the declaration part. This schema is assumed to be the state schema.

For example, let S be the state schema (= is used for \defs):
S = [ x,y:N ]
There are two supported styles for the initialization:

a) Init = [ S | x=0 /\ y=1]

b) Init = [ S'| x'=0 /\ y'=1 ]

If you want to use the logic of other schemas besides the state schema
in the initialization, you can do that by including those schemas in the predicate part.

=== Operations ===

ProZ identifies schemas as operations if they satisfy the following properties:
* All variables of the state and their primed counterpart are declared in the operation. Usually this is done by including "\Delta S" in the operation (with S being the state schema).
* The operation is not referenced by any other schema in the specification

Example: Let S be defined as above:

A = [ \Delta S | x'=x+1 /\ y'=y ]
B = [ x,y,x',y':N | x'=x+1 /\ y'=y ]
C = [ x,x':N | x'=x+1 ]
D = [ y,y':N | y'=y ]
E = C /\ D
F = [ \Xi S | x=0 ]

Then the schemas A,B and E describe all the same operation. F is also identified as an operation that leaves the state unchanged.

=== Axiomatic definitions ===

If axiomatic definitions are present, the declared variables are treated like constants. In the first step of the animation, ProB searches for values that satisfy all predicates of the axiomatic definitions are searched.
After the first step, the predicates of the axiomatic definitions
are ignored.
If you want to define functions in an axiomatic definition, consider that ProB can treat lambda expressions and set comprehensions symbolically.
Example: The definition of a function "square" could be

a)
| square : Z -> Z
|-----------------------
| square = (\lambda x:Z @ x*x)

b)
| square : Z -> Z
|-----------------------
| \forall x:Z @ square x = x*x

When using ProZ, it is preferable to use the method "a" because the lambda expression can be interpreted symbolically. If "b" is used, ProB will try to find a explicit set that will satisfy the given property.

=== Invariant ===

You can add a B-style invariant to the specification by defining a schema "Invariant" that declares a subset of the state variables. In each explored state the invariant will be checked. The model checking feature of ProB will try to find states that violate the invariant.

=== Scope ===

It is possible to limit the search space of the model checker by adding a schema "Scope" that declares a subset of the state variables. If such a schema is present, each explored state is checked, if it satisfies the predicate. If not, the state is not further explored.

=== Abbreviation Definitions ===

Abbreviation definitions (e.g. Abbr == {1,2,3}) are used like macros by
ProZ. A reference to an abbreviation is replaced by its definition in
a preprocessor phase.
Thereby schemas defined by abbreviation definitions are ignored when
ProZ tries to identify components. So, it is recommended to use schema definitions instead of abbreviation definitions (\defs instead of ==) when defining state, initialization, operations, etc.

== Special constructs ==

=== prozignore ===

Sometimes it is not desired to check properties of some variables.
E.g. ProZ checks if the square function in 2.3.a is a total function by enumerating it (it checks the function only for a limited interval). For more complex definitions the number of entries is often too large to check.
When the user is sure that those properties are satisfied (like in our example), a solution is relaxing the declaration from "square : Z -> Z" to "square : Z <-> Z".
Sometimes this is not easy to do, for instance if schema types are used which imply other constraints.

ProZ supports an operation \prozignore that instructs ProZ to ignore all constraints on the type and to use just the underlying type. For example, the square function could be defined by:

| square : \prozignore( Z -> Z )
|-----------------------
| square = (\lambda x:Z @ x*x)

If you want to use \prozignore, you must first define a TeX command \prozignore:
\newcommand{\prozignore}{ignore_\textsl{\tiny ProZ}}

You can change the definition of the macro as you like because the content is ignored by ProZ. Then you must introduce a generic definition of \prozignore. The definition is ignored by ProB, but Fuzz needs it for type checking.

%%pregen \prozignore
\begin{gendef}[X]
\prozignore~\_ : \power X
\end{gendef}

It is also possible to append these lines to the "fuzzlib" in the fuzz distribution.

=== Translation to B ===

You can inspect the result of the translation process with "Show internal representation" in the "Debug" menu.
Please note that the shown B machine is normally not syntactically correct because of
* additional constructs like free types
* additional type information of the form "var:type"
* names with primes (') or question marks, etc.
* lack of support from the pretty printer for every construct

== Known Limitations ==
* Generic definitions are not supported yet.
* Miscellaneous unsupported constructs
** reflexive-transitive closure
** probably other?
* The error messages are not very helpful yet.

Using the Command-Line Version of ProB

2011-05-11T06:55:44Z

Daniel Plagge: /* -mcm_tests */

Using the Command-Line Version of ProB

2011-05-11T06:53:52Z

Daniel Plagge: /* -mcm_tests */

Using the Command-Line Version of ProB

2011-05-11T06:53:04Z

Daniel Plagge: /* -mcm_tests */

Using the Command-Line Version of ProB

2011-05-11T06:52:25Z

Daniel Plagge: /* -mcm_cover */

Using the Command-Line Version of ProB

2011-05-11T06:51:29Z

Daniel Plagge: /* -mcm_cover */

Using the Command-Line Version of ProB

2011-05-11T06:50:27Z

Daniel Plagge: /* -mcm_cover */

Using the Command-Line Version of ProB

2011-05-11T06:46:07Z

Daniel Plagge: /* -mcm_tests */

Using the Command-Line Version of ProB

2011-05-11T06:17:28Z

Daniel Plagge: /* -mcm_tests */

User talk:Lukas Ladenberger

2011-05-06T07:15:28Z

Daniel Plagge: Welcome!

'''Welcome to ''ProB Documentation''!'''
We hope you will contribute much and well.
You will probably want to read the [[Help:Contents|help pages]].
Again, welcome and have fun! [[User:Daniel Plagge|Daniel Plagge]] 07:15, 6 May 2011 (UTC)

User:Lukas Ladenberger

2011-05-06T07:15:28Z

Daniel Plagge: Creating user page with biography of new user.

Plan LTL Visualisation

2011-04-06T10:38:52Z

Daniel Plagge:

= Wichtige Punkte =
Diese Teile müssen bei der Implementation / Beschreibung in der Arbeit beachtet werden.

== Schleifen, Deadlocks, und gekürzte Gegenbeispiele ==
Der Modelchecker liefert drei Arten von Gegenbeispielen:
* Schleifen, der Einstiegspunkt wird mitgeliefert. Eine Schleife repräsentiert einen unendlichen Pfad.
* Pfade, die im Deadlock enden. Beispiele: Im letzten Zustand des Gegenbeispiels ist X(f) immer falsch, unabhängig von f. G(f) ist im letzten Zustand war, wenn f dort wahr ist.
* Gekürzte Pfade. Als Gegenbeispiel reicht ein Teil der ursprünglich berechneten Schleife aus. Beispiele: X(f) ist im letzten Zustand nicht ermittelbar. Auch G(f) nicht, wenn f dort wahr ist.

== Verwaltung von LTL-Formeln ==
* Speichern von zuvor eingegebener Formeln (Model-abhängig?)
* Evtl. mehrere Reiter für verschiedene Formeln

== Anzeige ==
* Wie kann der Benutzer die Schleife erkennen, bzw. den Unterschied zwischen Deadlock und gekürztem Pfad?
* Formeln sollten evtl. durch den Rodin-UTF8-Konverter geschickt werden:
RodinKeyboardPlugin.getDefault().translate(...)
Dann muss allerdings der Rodin-Font verwendet werden.
* Bei Auswahl einer Zelle sollte mittels Farben (oder was besseres?) angezeigt werden, wie es zu dem Wert gekommen ist.

Beispiel: Hier wird die blau hinterlegte Zelle vom Benutzer markiert. In der nächsten Spalte färben sich einige Zellen gelb und rot. "G(not q)" ist in 7 unwahr wegen der Folge 7(not q: true), 8(not q: true), 9(not q:false).
[[File:ltl1.png|600px|center]]

* Alternativ könnte man die einen Schleifendurchlauf noch einmal hinten dran hängen, um den Benutzer zu entlasten.
* Die Anzeige der Zustandsnummern bringt dem Benutzer nicht wirklich etwas (wird sonst nirgendwo anders verwendet)

== Semantik vom Release-Operator ==

(pi,i) |= fRg genau dann wenn
* ein j>=i existiert mit (pi,j) |= f&g und für alle k mit i<=k<j (pi,k) |= g gilt
* oder (pi,j) |= g für alle j>=i gilt

= Ideen zu GUI =

* Interaktion mit der aktuellen Historie: Evtl. sollte das Gegenbeispiel auch in die aktuelle Historie geladen werden und der aktuell ausgewählte Zustand dort auch angezeigt werden.
* Gleichzeitig in mehreren Reitern verschiedene Pfade speichern
* Evtl. könnte der Benutzer einen Knopf gebrauchen, mit dem er den Einstiegs-Zustand der Schleife (wenn eine existiert) wieder hinten anhängen kann. Dann verschiebt sich der Einstiegspunkt um 1.
* Den LTL-Button in der Event-View und den LTL-Dialog entfernen und die Eingabe der Formeln komplett in der LTL-View erledigen.
* Atomare Aussagen sollten in der StateView analysierbar werden, z.B. mittels Kontextmenü. Analog zum "grünen Plus" in der StateView. Ideal wäre DnD.

=Interaktion mit anderen ProB-Komponenten=
Bisher ist man als Benutzer noch relativ verloren, wenn man das Gegenbeispiel mit dem ursprünglichen Modell in Verbindung bringen will. Die bestehenden Anzeigen sollten mit benutzt werden, um den Benutzer zu helfen.

Wenn in der LTL-View ein Zustand angewählt wird (oder explizit mittels Doppelklick oder so ähnlich), sollte der aktuelle Zustand und History auf
den Zustand gesetzt werden:
* In der State-View wird der aktuelle Zustand angezeigt und auswertbar gemacht.
* In der History-View wird das komplette LTL-Gegenbeispiel angezeigt
* In der Event-View werden alle möglichen Events angezeigt werden. Der Benutzer kann dann mit den vor-zurück-Buttons durch das Gegenbeispiel navigieren. Wählt er ein Event explizit, bekommt er eine neue History (wie bisher auch)
* Atomare Aussagen sollten als Formeln in die State-View anzuzeigen sein.

Umgekehrt sollte es möglich sein, die aktuelle Historie auf eine LTL-Formel hin zu überprüfen. Was machen wir in dem Fall mit dem Beispiels-Ende (also Deadlock, abgeschnitten oder Schleife?)

Tutorial Complete Model Checking

2011-03-01T10:34:43Z

Daniel Plagge: fixed typo

[[Category:User Manual]]

We assume that you have completed [[Tutorial First Model Checking]]. There we have seen how to find invariant violations using the model checker.

In this part we use the following B Machine:
<pre>
DEFINITIONS
MACHINE SimpleCounterForMC
DEFINITIONS MAX==4; SET_PREF_MAX_OPERATIONS==5
VARIABLES count
INVARIANT
count: 1..MAX
INITIALISATION count := 1
OPERATIONS
Increase(y) = PRE y: 1..(MAX-count) THEN
count := count+y
END;
Reset = BEGIN count :: 1..MAX END
END
</pre>

To load this machine into ProB you can select "New..." from the "File" menu, choose a file name (e.g., "SimpleCounterForMC.mch") and then paste the text above into the ProB source pane and choose "Save and Reopen" from the "File" menu.

Note that the DEFINITION SET_PREF_MAX_OPERATIONS==5 means that ProB will compute at most 5 possible ways to execute any given operation (i.e., Increase and Reset in this case). We return to this issue below.

== Successful Model Checking ==

Now select the "Model Check..." command in the "Verify" menu which brings up the model checking dialog box:
[[file:ProBWinModelCheckDialog.png|center]]
Now click the "Model Check" button. After a short while, ProB will give you the following message:
[[file:ProBModelCheckNoCounterExampleFound.png|center]]

This message means that ProB has examine all possible states of your B model and has found no invariant violation and no deadlock. (In this case there are 4 states and one root node.)

Does this mean that the B machine is guaranteed to be correct? Does this mean that the AtelierB provers will be able to prove the B machine correct?
In this case yes, but in general we have to be very careful about interpreting a completed model check.
Below we examine several issues that have to be considered.

== Computing All Transitions ==

Let us now adapt the above B machine by changing the DEFINITION of MAX to 6.
Now repeat the model checking exercise above. This time ProB will produce the following message:
[[file:ProBModelCheckNoCounterExampleFoundTrans.png|center]]

Again no invariant violations or deadlocks were found, but this time ProB warns us that not all transitions were computed. Indeed, the SET_PREF_MAX_OPERATIONS definition tells ProB to compute at most 5 ways to execute an operation. In this case, there are 6 ways to execute the Reset operation. As such, ProB may have missed certain states and thus may have missed an invariant violation.

Indeed, when you double click on the "INITIALISATION(1)" entry in the "EnabledOperations" pane, you will see the following:
[[file:ProBSimpleCounterForMC_Max.png|center]]

The orange "max" button tells us that not all operations were computed.

In this case, there was no error, but assume we change the definition of the Reset operation to
<Pre>
Reset = BEGIN count :: 1..MAX+1 END
</Pre>
and repeat the model checking. We will get the exact same result as above, but this time the machine is actually incorrect.
The only way to solve ensure that ProB checks the entire state space is to increase the "MAX_OPERATIONS" preference to a suitably large value, e.g., SET_PREF_MAX_OPERATIONS==8 in this case.
Now model checking will find a counter example:
[[file:ProBSimpleCounterForMC_InvViol.png|center]]

== Deferred Sets ==

Let us now use the following simple machine:
<Pre>
MACHINE SimpleCountDefSet
SETS ID
VARIABLES s
INVARIANT s <: ID & card(s)<10
INITIALISATION s := {}
OPERATIONS
Add(x) = PRE x:ID & x/:s THEN s := s\/{x} END;
Remove(x) = PRE x:s THEN s:= s - {x} END
END
</Pre>

Here model checking with ProB will give you the following message:
[[file:ProBModelCheckNoCounterExampleFound_Unbounded.png|center]]

Unfortunately this does not guarantee that your machine is correct. Indeed, ProB has checked your machine only for one specific cardinality of the deferred set ID (probably 2 or 3).
Indeed, if you look at the ProB window after loading the above machine you will see:
[[file:ProBSimpleCountDefSet_BeforeInit.png|center]]
In the "State Properties" pane you can see that the cardinality of ID was set to 3.
There are various ways you can influence the cardinality chosen by ProB; one is by adding a DEFINITION of the form:
<Pre>
DEFINITIONS scope_ID == 10
</Pre>
If you add this definition, ProB will now find an invariant violation:
[[file:ProBSimpleCountDefSet_InvViol.png|center]]

However, if you remove the above DEFINITION and add the following instead:
<Pre>
PROPERTIES card(ID) = 5
</Pre>
ProB will give you the message we have already seen:
[[file:ProBModelCheckNoCounterExampleFound.png|center]]
Indeed, you have now explicitly declare ID to be of size 5, and ProB has checked all states for that instantiation of ID. Another solution is to replace the deferred set ID by an enumerated set (this will, however, reduce the potential for symmetry reduction):
<Pre>
SETS ID={id1,id2,id3,id4,id5}
</Pre>

== Infinite Types ==

It could be that your B machine makes use of the mathematical integers (INTEGER) or infinite subsets thereof (NATURAL, NATURAL1). Note that some derived types (such as seq(.)) are defined in terms of INTEGER.
In this case there could be no way to explore all states of your system.
For example, the following operation
<Pre>
Choose = BEGIN x :: NATURAL END
</Pre>
can be executed in infinitely many ways. ProB will in this case only find values between 0 and MAXINT for x. As such, a complete model checking does not indicate that your machine's state space has been fully explored.
Note: ProB prints a warning on the console when an infinite type (like NATURAL) was "expanded" into a finite subset of it. This information is not yet fed back to the graphical user interface (but we are working on it).

== Model Checking and Proof ==

Finally, even if ProB was able to successfully check the entire state space of your model, this does not imply that you can prove your machine correct with AtelierB (or Rodin).
We dedicate another tutorial page to this: [[Tutorial Model Checking, Proof and CBC|Model Checking, Proof and CBC]]

Download

2011-02-11T09:22:47Z

Daniel Plagge: /* Latest Release */

== Latest Release ==

Note: please use the provided start scripts (StartProB.sh or StartProBWin.bat) to start ProB.

{| border="1"
! Platform
! Release Date
! Download
! Dependencies
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.3-final
|-
| Linux
| 10.02.2011
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB.linux.tar.gz Tarball (32bit)], [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB.linux64.tar.gz Tarball (64bit)], [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/prob_1.3.3_i386.deb Ubuntu/Debian package (32bit)]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.5
|-
| Windows
| 10.02.2011
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB.windows.32bit.zip Zipfile (with probcli)]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, Snow Leopard, Intel
| 10.02.2011
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB.mac_os.10.6.6.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Mac OS X, Leopard, Intel
| 10.02.2011
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB.mac_os.10.5.8.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.2-final
|-
| Linux
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_linux.tar.gz Tarball (32bit)], [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_linux64.tar.gz Tarball (64bit)], [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/prob_1.3.2final1_i386.deb Ubuntu/Debian package (32bit)]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.5
|-
| Windows
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_Win.zip Zipfile (with probcli)]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, Snow Leopard, Intel
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_snowleopard.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Mac OS X, Leopard, Intel
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_leopard_intel.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]

|-
| Mac OS X, Tiger, Intel
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_tiger_intel.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.4],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.1-final
|-
| Mac OS X, Snow Leopard
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-snowleopard-1.3.1final5.tar.gz Tarball]
| [http://www.tcl.tk/software/tcltk/8.5.html Tcl/TK 8.5 (for Leopard)],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Linux
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-linux-1.3.1final5.tar.gz Tarball]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.4
|-
| Windows
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-win-1.3.1final5.zip Zipfile]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, PPC Tiger
| 07.12.2009
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final3/ProB-ppctiger-1.3.1final3.tar.gz Tarball]
| [http://www.tcl.tk/software/tcltk/8.5.html Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|}

== tcl/tk ==
Please note that Tcl/Tk 8.6 is not yet supported by SICStus Prolog. Also note that on Mac OS X you may have to reinstall Tcl/Tk using one of the links given above (because the Tcl/Tk provided by Apple crashes after opening a file using the standard file selection dialog).

== Earlier Releases ==

If you are interested in earlier releases, please have a look at the [http://www.stups.uni-duesseldorf.de/ProB_Releases/ Download directory].

Download

2011-02-10T15:50:11Z

Daniel Plagge: /* Latest Release */

== Latest Release ==

Note: please use the provided start scripts (StartProB.sh or StartProBWin.bat) to start ProB.

{| border="1"
! Platform
! Release Date
! Download
! Dependencies
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.3-final
|-
| Linux
| 10.02.2011
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB.linux.tar.gz Tarball], [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/prob_1.3.3_i386.deb Ubuntu/Debian package], [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB.linux64.tar.gz Tarball (64bit)]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.5
|-
| Windows
| 10.02.2011
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB.windows.32bit.zip Zipfile (with probcli)]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, Snow Leopard, Intel
| 10.02.2011
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB.mac_os.10.6.6.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Mac OS X, Leopard, Intel
| 10.02.2011
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB.mac_os.10.5.8.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.2-final
|-
| Linux
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_linux.tar.gz Tarball], [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/prob_1.3.2final1_i386.deb Ubuntu/Debian package], [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_linux64.tar.gz Tarball (64bit)]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.5
|-
| Windows
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_Win.zip Zipfile (with probcli)]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, Snow Leopard, Intel
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_snowleopard.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Mac OS X, Leopard, Intel
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_leopard_intel.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]

|-
| Mac OS X, Tiger, Intel
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_tiger_intel.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.4],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.1final
|-
| Mac OS X, Snow Leopard
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-snowleopard-1.3.1final5.tar.gz Tarball]
| [http://www.tcl.tk/software/tcltk/8.5.html Tcl/TK 8.5 (for Leopard)],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Linux
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-linux-1.3.1final5.tar.gz Tarball]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.4
|-
| Windows
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-win-1.3.1final5.zip Zipfile]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, PPC Tiger
| 07.12.2009
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final3/ProB-ppctiger-1.3.1final3.tar.gz Tarball]
| [http://www.tcl.tk/software/tcltk/8.5.html Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|}

== tcl/tk ==
Please note that tcl/tk 8.6 is not yet supported by SICStus Prolog.

== Earlier Releases ==

If you are interested in earlier releases, please have a look at the [http://www.stups.uni-duesseldorf.de/ProB_Releases/ Download directory].

Download

2011-02-10T15:49:02Z

Daniel Plagge: /* Latest Release */

== Latest Release ==

Note: please use the provided start scripts (StartProB.sh or StartProBWin.bat) to start ProB.

{| border="1"
! Platform
! Release Date
! Download
! Dependencies
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.3-final
|-
| Linux
| 10.02.2011
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB_linux.tar.gz Tarball], [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/prob_1.3.3_i386.deb Ubuntu/Debian package], [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB_linux64.tar.gz Tarball (64bit)]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.5
|-
| Windows
| 10.02.2011
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB.windows.32bit.zip Zipfile (with probcli)]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, Snow Leopard, Intel
| 10.02.2011
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB.mac_os.10.6.6.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Mac OS X, Leopard, Intel
| 10.02.2011
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.3/ProB.mac_os.10.5.8.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.2-final
|-
| Linux
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_linux.tar.gz Tarball], [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/prob_1.3.2final1_i386.deb Ubuntu/Debian package], [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_linux64.tar.gz Tarball (64bit)]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.5
|-
| Windows
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_Win.zip Zipfile (with probcli)]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, Snow Leopard, Intel
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_snowleopard.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Mac OS X, Leopard, Intel
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_leopard_intel.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]

|-
| Mac OS X, Tiger, Intel
| 30.07.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_tiger_intel.tar.gz Tarball (with probcli)]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.4],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.1final
|-
| Mac OS X, Snow Leopard
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-snowleopard-1.3.1final5.tar.gz Tarball]
| [http://www.tcl.tk/software/tcltk/8.5.html Tcl/TK 8.5 (for Leopard)],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Linux
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-linux-1.3.1final5.tar.gz Tarball]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.4
|-
| Windows
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-win-1.3.1final5.zip Zipfile]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, PPC Tiger
| 07.12.2009
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final3/ProB-ppctiger-1.3.1final3.tar.gz Tarball]
| [http://www.tcl.tk/software/tcltk/8.5.html Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|}

== tcl/tk ==
Please note that tcl/tk 8.6 is not yet supported by SICStus Prolog.

== Earlier Releases ==

If you are interested in earlier releases, please have a look at the [http://www.stups.uni-duesseldorf.de/ProB_Releases/ Download directory].

Plan LTL Visualisation

2011-02-03T12:41:28Z

Daniel Plagge: /* Ideen zu GUI */

Plan LTL Visualisation

2011-02-03T12:39:27Z

Daniel Plagge: /* Ideen zu GUI */

Plan LTL Visualisation

2011-01-19T13:47:28Z

Daniel Plagge: /* Anzeige */

Plan LTL Visualisation

2011-01-19T13:29:57Z

Daniel Plagge: /* Wichtige Punkte */

Plan LTL Visualisation

2011-01-19T13:08:49Z

Daniel Plagge: /* Ideen zu GUI */