Home

Welcome to the MBT Arranger wiki!

This Eclipse feature provides an Eclipse Plugin that generates C++ testcases from models written in Promela/mCRL2. With MBT Arranger, one can also edit Promela/mCRL2 files and check those models.

You may get a first glimpse from the videos:

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