OBP2 is a multi language model-checker

The new version 0.0.6 is out with tons of new features.

Verification View

Exploration capabilities

  • Simple Simulation of models
  • Exhaustif BFS, DFS and concurrent BFS explorations,


  • Pause, resume and stop any exploration,
Idle Execution Idle 1: Start execution
2: Open the simulation view
Running Execution Running 3: Pause execution
4: Stop execution
Paused Execution Paused 5: Resume execution
Done Execution Done 6: Clear results


  • Native Deadlock verification,
  • LTL verification (See the post on GPSL syntax),

Advanced simulation view

  • Configurations presentation:
Tree View Differences
Configuration Items Configuration Diffs
  • Graph view of visited configuration,
  • Color coding of duplicate configurations,

Simulation View

  • Presentation of counter-example with possibilty to branch.

Counter Example

  • Export of graph views.