Template:User Manual Index
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: