Home

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

Development Environment:

1.1. tools listed in (4) 1.2. Eclipse Luna 1.3. JAVA8 1.4. Windows 7 1.5. optional: MSVS2010

Warning

This software is in early alpha state.

Compilation

This MBT Arranger application is compilable as an Eclipse Plugin, use a non-productive Eclipse environment on a separate machine that may break, do not run this plugin in your productive Eclipse environment.

MBT Arranger uses the following opensource tools:

4.1. Eclipse : The Complete source code can be downloaded from http://www.eclipse.org/

4.2. MinGW, GCC : The Complete source code can be downloaded from http://sourceforge.net/projects/mingw/files/MinGW/

4.3. SPIN : The Complete source code can be downloaded from http://spinroot.com/

4.4. Graphviz : The Complete source code can be downloaded from http://www.graphviz.org/

MBT Arranger uses the following opensource code

5.1. ANTLR : The Complete source code can be downloaded from http://www.antlr.org/

5.4. JAutomata : The Complete source code can be downloaded from http://jautomata.sourceforge.net/

5.2. Apache Batik : The Complete source code can be downloaded from http://xmlgraphics.apache.org/batik/

5.3. TopologicalSort : The Complete source code can be downloaded from http://www.keithschwarz.com/