No edit summary |
No edit summary |
||

(25 intermediate revisions by 3 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]] | * [[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]] | * [[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]] | * [[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:

- 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
- 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:

FAQ, Tips and Troubleshootings: