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.