- Download Version 0.0.4
Plug-OBP alias OBP2 is a LTL model-checker for Fiacre models using the OBP compiler providing much more advanded model-checking capabilities.
The new version
0.0.4 is out with tons of new features.
- 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|
- Native Deadlock verification,
- LTL verification (See the post on GPSL syntax),
Advanced simulation view
- Configurations presentation:
|Tree View||Differences||Filtering with predicates|
- Graph view of visited configuration,
- Color coding of duplicate configurations,
- Presentation of counter-example with possibilty to branch.
- Export of graph views.
- The trace view is a simple and light view that will be opened instead of the graph view if the counter example contains more than 1500 nodes. It also can be enforced if
shiftis pressed when opening the graph view.