Home

Welcome to the MBT Arranger wiki!

This Eclipse feature provides an Eclipse Plugin that generates C++ testcases from models written in PROMELA and mCRL2. MBT Arranger can be used as an editor, syntax checker, debugger or model checker for PROMELA files and mCRL2 files.

You may get a first glimpse from the videos:

• design test scenarios
• edit SPIN models
• edit mCRL2 models(t.b.d)
• debug SPIN Models(t.b.d)
• generate c++ testsuites from (*.arr)-files(t.b.d)
• generate c++ common types from (*.arr)-files(t.b.d)
• generate c++ testcases from (*.arr)-files(t.b.d)
• run c++ testsuites](t.b.d)

Warning:

This software is in early alpha state. Please read the Readme.txt first, before you use this software.

Where to start

For beginners, Getting Started is recommended.

For the experts

Forgot some of the many details? Have a look [here](ARRANGE language).

Want to get involved or debug? Check [this](Getting Involved).