Template:User Manual Index: Difference between revisions

No edit summary
No edit summary
 
(22 intermediate revisions by 2 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]]
Line 12: 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:
* [[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]]
* [[Checking CSP Assertions]]
Line 19: Line 38:
* [[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]]
* [[TLC|Using TLC for B 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]]
* [[State Space Coverage Analyses]]
* [[Using ProB with KODKOD]]
* [[Generating Documents with ProB and Latex]]
* [[Using ProB with Z3]]
* [[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]]
* [[Controlling_ProB_Preferences|Setting ProB Preferences]]
Line 34: Line 69:
* [[Tips: Writing Models for ProB]]
* [[Tips: Writing Models for ProB]]
* [[Tips: B Idioms|Tips: Common B Idioms (let, if-then-else,...)]]
* [[Tips: B Idioms|Tips: Common B Idioms (let, if-then-else,...)]]
* [[Using the Command-Line Version of ProB]]
* [[Summary of B Syntax]]
* [[Summary of B Syntax]]
* [[Well-Definedness Checking]]

Latest revision as of 09:05, 23 April 2024

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: