No edit summary |
No edit summary |
||
| (30 intermediate revisions by 4 users not shown) | |||
| Line 1: | Line 1: | ||
Animation and Visualisation with ProB: | |||
* [[Installation]] | * [[Installation]] | ||
* [[Current Limitations]] | * [[Current Limitations]] | ||
| Line 5: | Line 6: | ||
* [[Graphical Visualization]] | * [[Graphical Visualization]] | ||
* [[State Space Visualization]] | * [[State Space Visualization]] | ||
Validation with ProB: | |||
* [[Consistency Checking|Consistency Checking (Finding Invariant Violations using the Model Checker)]] | * [[Consistency Checking|Consistency Checking (Finding Invariant Violations using the Model Checker)]] | ||
* [[Constraint Based Checking]] | * [[Constraint Based Checking]] | ||
* [[Refinement Checking]] | * [[Refinement Checking]] | ||
* [[LTL Model Checking]] | * [[LTL Model Checking]] | ||
* [[Bounded Model Checking]] | * [[Bounded Model Checking|Bounded Model Checking (BMC*)]] | ||
* [[Symbolic Model Checking|Symbolic Model Checking]] | |||
* [[ProB Validation Methods|Comparing the various ProB Validation Methods]] | * [[ProB Validation Methods|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 ProB with Atelier B]] | ||
* [[TLC|Using TLC for B Specifications]] | |||
* [[LTSMin|Using ProB with LTSMin as Model Checking Backend]] | |||
* [[Using ProB with KODKOD]] | |||
* [[Using ProB with Z3]] | |||
* [[B2SAT|Using ProB with B2SAT]] | |||
* [[Editors for ProB]] | |||
ProB for Other Languages: | |||
* [[CSP-M|Using CSP-M in ProB]] | * [[CSP-M|Using CSP-M in ProB]] | ||
* [[Checking CSP Assertions]] | |||
* [[ProB for Event-B|Using ProB for Event-B and Rodin]] | |||
* [[Event-B Theories|Using ProB for Event-B with the theory plug-in]] | * [[Event-B Theories|Using ProB for Event-B with the theory plug-in]] | ||
* [[ProZ|Using ProZ for Animation and Model Checking of Z Specifications]] | * [[ProZ|Using ProZ for Animation and Model Checking of Z Specifications]] | ||
* [[TLA|Using ProB for TLA Specifications]] | * [[TLA|Using ProB for TLA Specifications]] | ||
* [[ | * [[Alloy|Using ProB for Alloy Specifications]] | ||
* [[Other languages|Using ProB with Promela and other languages]] | * [[Other languages|Using ProB with Promela and other languages]] | ||
* [[Rules-DSL|Using the B Rules DSL Language]] | |||
Advanced Features of ProB: | |||
* [[Symmetry Reduction]] | * [[Symmetry Reduction]] | ||
* [[ParB|Parallel Execution of ProB]] | |||
* [[Recursively Defined Functions]] | * [[Recursively Defined Functions]] | ||
* [[Memoization for Functions]] | |||
* [[Operation Calls in Expressions]] | |||
* [[External Functions]] | * [[External Functions]] | ||
* [[Reals and Floats]] | |||
* [[Debugging]] | |||
* [[Common Subexpression Elimination]] | * [[Common Subexpression Elimination]] | ||
* [[Test Case Generation]] | * [[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|Custom Graph Visualization]] | |||
* [[VisB|VisB SVG-based Visualization]] | |||
FAQ, Tips and Troubleshootings: | |||
* [[FAQ]] | * [[FAQ]] | ||
* [[Controlling_ProB_Preferences|Setting ProB Preferences]] | |||
* [[Troubleshooting]] | * [[Troubleshooting]] | ||
* [[Tips: Writing Models for ProB]] | * [[Tips: Writing Models for ProB]] | ||
* [[ | * [[Tips: B Idioms|Tips: Common B Idioms (let, if-then-else,...)]] | ||
* [[Summary of B Syntax]] | * [[Summary of B Syntax]] | ||
Animation and Visualisation with ProB:
Validation with ProB:
Other Interfaces to ProB:
ProB and Other Tools:
ProB for Other Languages:
Advanced Features of ProB:
Advanced Visualization Features of ProB:
FAQ, Tips and Troubleshootings: