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)
• verify SPIN models (t.b.d. LTL, Notrace, Never, verify/interact view)
• debug SPIN Models(t.b.d. with LTL)
• GIT source control integration (t.b.d. import edit save compare)
• 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)
• debug c++ test adapters (t.b.d. adapter mutil send)
• run c++ testsuites](t.b.d)
• debug MBT Arranger itself](t.b.d. micksutils iterator example)

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