OBP2 Version 0.0.6 is out
- Download Version 0.0.6
OBP2 is a multi language model-checker
- Fiacre models using the OBP compiler
- TLA models using the tlatools for TLA model compilation
The new version 0.0.6
is out with tons of new features.
Exploration capabilities
- Simple Simulation of models
- Exhaustif BFS, DFS and concurrent BFS explorations,
- Pause, resume and stop any exploration,
Idle | ![]() |
1: Start execution 2: Open the simulation view |
Running | ![]() |
3: Pause execution 4: Stop execution |
Paused | ![]() |
5: Resume execution |
Done | ![]() |
6: Clear results |
Model-checking
- Native Deadlock verification,
- LTL verification (See the post on GPSL syntax),
Advanced simulation view
- Configurations presentation:
Tree View | Differences |
![]() |
![]() |
- Graph view of visited configuration,
- Color coding of duplicate configurations,
- Presentation of counter-example with possibilty to branch.
- Export of graph views.