No edit summary |
No edit summary |
||
| (12 intermediate revisions by 2 users not shown) | |||
| Line 15: | Line 15: | ||
* [[Symbolic Model Checking|Symbolic Model Checking]] | * [[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: | Other Interfaces to ProB: | ||
* [[Using the Command-Line Version of ProB]] | * [[Using the Command-Line Version of ProB]] | ||
* [[ | * [[ProB2-UI]] | ||
ProB and Other Tools: | ProB and Other Tools: | ||
* [[Using ProB with Atelier B]] | * [[Using ProB with Atelier B]] | ||
* [[TLC|Using TLC for B Specifications]] | * [[TLC|Using TLC for B Specifications]] | ||
* [[LTSMin|Using ProB with LTSMin as Model Checking Backend]] | |||
* [[Using ProB with KODKOD]] | * [[Using ProB with KODKOD]] | ||
* [[Using ProB with Z3]] | * [[Using ProB with Z3]] | ||
* [[B2SAT|Using ProB with B2SAT]] | |||
* [[Editors for ProB]] | * [[Editors for ProB]] | ||
| Line 37: | Line 40: | ||
* [[Alloy|Using ProB for Alloy 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: | Advanced Features of ProB: | ||
| Line 43: | Line 47: | ||
* [[Recursively Defined Functions]] | * [[Recursively Defined Functions]] | ||
* [[Memoization for Functions]] | * [[Memoization for Functions]] | ||
* [[Operation Calls in Expressions]] | |||
* [[External Functions]] | * [[External Functions]] | ||
* [[Reals and Floats]] | |||
* [[Debugging]] | * [[Debugging]] | ||
* [[Common Subexpression Elimination]] | * [[Common Subexpression Elimination]] | ||
| Line 49: | Line 55: | ||
* [[State Space Coverage Analyses]] | * [[State Space Coverage Analyses]] | ||
* [[Generating Documents with ProB and Latex]] | * [[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, Tips and Troubleshootings: | ||
| Line 57: | Line 70: | ||
* [[Tips: B Idioms|Tips: Common B Idioms (let, if-then-else,...)]] | * [[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: