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](t.b.d. Test Scenario Design with MBT Arranger )
• edit SPIN models
• explore SPIN model structure
• edit mCRL2 models
• explore mCRL2 model structure
• debug SPIN Models
• generate c++ testsuites from (*.arr)-files
• generate c++ common types from (*.arr)-files
• generate c++ testcases from (*.arr)-files
• run c++ testsuites

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).