User Manual
ProB is a graphical animator and model checker for the B method. The ProB homepage is at https://prob.hhu.de/, where precompiled binaries, installation instructions and documentation are available.
Important notice
If you find a problem with ProB or this documentation 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" section. You can also post a question in our prob-users group or send an email to Michael Leuschel.
Single-page handbook
For those who prefer to read a single long page instead of many small pages, we also have a single-page "handbook" version of the manual. Warning: the page is large and may take a few seconds to load.
Content of this manual
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:
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
- Using ProB with Clingo
- 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
- Using ProB for CNF SAT Files
Advanced Features of ProB:
- Symmetry Reduction
- Parallel Execution of ProB
- Recursively Defined Functions
- Memoization for Functions
- Operation Calls in Expressions
- External Functions
- Strings
- 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:
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).
Modeling Tips
Sample Models
Some of the examples below are now available as Jupyter notebooks and can be launched using binder. Another repository contains notebooks for teaching. An extensive collection of models for benchmarking is maintained in a Github repository.
- TrainSwitchingPuzzle
- Model for Card Trick by Gilbreath
- Rush Hour Puzzle
- Game of Life (Jupyter notebook)
- N-Queens
- Peaceable Armies of Queens
- Die Hard Jugs Puzzle (Jupyter notebook)
- ABZ 2014 Landing Gear Case Study
- Sudoku Solved in the ProB REPL
- Miracle Sudoku (Jupyter notebook)
- 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
- Apples and Oranges (Apple Interview Question) (Jupyter Notebook)
- Bridges Puzzle (Hashiwokakero) (Jupyter notebook)
- Argumentation Theory
- State_space_visualization_examples
- The Jobs Puzzle
- N-Bishops Puzzle
- ABZ 2016 Medical Case Study
- Proving Theorems in the ProB REPL
- SEND-MORE-MONEY (Jupyter notebook)
- Induction Proofs in B
Sample Graphics
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.