ETrice/GSoC/2012/ModelChecking

Architectural Considerations (just to have a place to put it)

the abstract state machine execution algorithm (FSM executor for short) should be able to work on the plain textual model (which is equivalent to an EMF model if it is parsed successfully)
for convenience the FSM executor should operate on a transformed model which already contains inherited states etc. and which has transition chains already computed. All this is already there in form of the generator model (etricegen.ecore in o.e.e.generator)
to avoid lumping the generator model and the FSM executor into the basic ROOM DSL plugin o.e.e.core.room we should introduce an extension point which allows us to generate markers and proposals (or 'quick fixes' how they are often called) for the textual model. This should be possible in a fairly general way. It should be configurable by the extending plugin when this extension should be triggered (e.g. explicitly on full validation as opposed to continuously during typing)
the FSM executor is implemented in a new plugin o.e.e.fsmexecutor. On top of the executor there are specific algorithms like a Protocol Validator and a Connectivity Validator (which detects unreachable parts of the FSM). Both of which extend the above defined extension point
the graphical editor should (configurably) invoke above defined validators and add temporary transitions and states as well as graphical hints for missing messages to be sent. Also unreachable parts of the state machine should indicated graphically (e.g. by changing their color)

Based on that we have the following working packages:

refactor the current generator model plugin into a part which contains just the generator model and the transformation algorithm which creates this model from a given ROOM model and the parts of the plugin which are used only for code generation. Thereby the generator model should be reworked a little bit and renamed to something independent of code generation. (will be done by Henrik)
define and introduce the extension point. To this end it is necessary to understand and extend the way how xtext deals with markers and quick fixes
design and implement the FSM executor in a new plugin
implement the Connectivity and the Protocol Validator using the executor (after that both can already be used on the textual model)
use the new validators in the graphical FSM editor

I think 2) and 3) will be a good first mile stone 4) another mile stone 5) the last one