User Manual

ProB is a graphical animator and model checker for the B method. The ProB homepage is at http://www.stups.uni-duesseldorf.de/ProB, where precompiled binaries, installation instructions and documentation are available.

Important notice

If you find a problem with ProB please let us know. We are happy to receive suggestions for improvements to ProB or the documentation. More information about submitting bug reports is available in the [Bugs|"bugs" section] or directly in our bug tracker.

Content of this handbook

Animation and Visualisation with ProB:

• Installation
• Current Limitations
• General Presentation (tcl/tk)
• Graphical Viewer
• Graphical Visualization
• State Space Visualization

Validation with ProB:

• Consistency Checking (Finding Invariant Violations using the Model Checker)
• Constraint Based Checking
• Refinement Checking
• LTL Model Checking
• Bounded Model Checking (BMC*)
• Symbolic Model Checking
• Comparing the various ProB Validation Methods
• Well-Definedness Checking

Other Interfaces to ProB:

• Using the Command-Line Version of ProB
• ProB2-UI

ProB and Other Tools:

• Using ProB with Atelier B
• Using TLC for B Specifications
• Using ProB with LTSMin as Model Checking Backend
• Using ProB with KODKOD
• Using ProB with Z3
• Using ProB with B2SAT
• Editors for ProB

ProB for Other Languages:

• Using CSP-M in ProB
• Checking CSP Assertions
• Using ProB for Event-B and Rodin
• Using ProB for Event-B with the theory plug-in
• Using ProZ for Animation and Model Checking of Z Specifications
• Using ProB for TLA Specifications
• Using ProB for Alloy Specifications
• Using ProB with Promela and other languages
• Using the B Rules DSL Language

Advanced Features of ProB:

• Symmetry Reduction
• Parallel Execution of ProB
• Recursively Defined Functions
• Memoization for Functions
• Operation Calls in Expressions
• External Functions
• Reals and Floats
• Debugging
• Common Subexpression Elimination
• Test Case Generation
• State Space Coverage Analyses
• Generating Documents with ProB and Latex
• Caching Constants and Operations
• Monte Carlo Tree Search Game Play

Advanced Visualization Features of ProB:

• Generating UML Sequence Charts
• Custom Graph Visualization
• VisB SVG-based Visualization

FAQ, Tips and Troubleshootings:

• FAQ
• Setting ProB Preferences
• Troubleshooting
• Tips: Writing Models for ProB
• Tips: Common B Idioms (let, if-then-else,...)
• Summary of B Syntax

(Also have a look at the tutorial; in particular Starting ProB and first animation steps).

Sample Models

• TrainSwitchingPuzzle
• Model for Card Trick by Gilbreath
• Rush Hour Puzzle
• Game of Life
• N-Queens
• Peaceable Armies of Queens
• ABZ 2014 Landing Gear Case Study
• Sudoku Solved in the ProB REPL
• Euler Problem 67 - Maximum Path Sum II
• Mutual Exclusion (Fairness)
• Cheryl's Birthday
• Blocks World (Directed Model Checking)
• Nine Prisoners Puzzle by Dudeney and Gardner

Sample Graphics

• Siemens Complicated Property Visualized

Feedback

Please help us to improve this documentation by providing feedback in our bug tracker, asking questions in our prob-users group or sending an email to Michael Leuschel.