User Manual: Difference between revisions

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.

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:

• 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

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

• 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.