Major refactoring

- Moved tests
- Changes to promela datamodel
- Implemented Trie

4 files changed, 994 insertions, 242 deletions

diff --git a/src/uscxml/transform/ChartToFSM.cpp b/src/uscxml/transform/ChartToFSM.cpp
index d962481..8b1725c 100644
--- a/src/uscxml/transform/ChartToFSM.cpp
+++ b/src/uscxml/transform/ChartToFSM.cpp
@@ -19,6 +19,8 @@
 
 #include "uscxml/transform/ChartToFSM.h"
 #include <DOM/io/Stream.hpp>
+#include <glog/logging.h>
+
 #include <iostream>
 #include "uscxml/UUID.h"
 #include <math.h>
@@ -34,7 +36,9 @@ using namespace Arabica::XPath;
 
 #define CREATE_TRANSIENT_STATE_WITH_CHILDS \
 if (childs.size() > 0) { \
-	Element<std::string> transientState = _flatDoc.createElementNS(xmlNs, "state"); \
+	Element<std::string> transientState = _flatDoc.createElementNS(_nsInfo.nsURL, "state"); \
+	_nsInfo.setPrefix(transientState);\
+	transientState.setAttribute("transient", "true"); \
 	for (int i = 0; i < childs.size(); i++) { \
 		Node<std::string> imported = _flatDoc.importNode(childs[i], true); \
 		transientState.appendChild(imported); \
@@ -43,19 +47,24 @@ if (childs.size() > 0) { \
 } \
 childs = NodeSet<std::string>();
 
-Document<std::string> ChartToFSM::flatten(const Document<std::string>& doc, const std::map<std::string, std::string>& nameSpaceInfo) {
-	boost::shared_ptr<InterpreterImpl> flatInterpreter = boost::shared_ptr<InterpreterImpl>(new FlatteningInterpreter(doc));
-	flatInterpreter->setNameSpaceInfo(nameSpaceInfo);
-	flatInterpreter->interpret();
-  return flatInterpreter->getDocument();
+Interpreter ChartToFSM::flatten(const Interpreter& other) {
+
+	// instantiate a new InterpreterImpl to do the flattening
+	boost::shared_ptr<InterpreterImpl> flattener = boost::shared_ptr<InterpreterImpl>(new FlatteningInterpreter(other.getDocument()));
+	flattener->setNameSpaceInfo(other.getNameSpaceInfo());
+	flattener->interpret();
+
+	// clone the flattener implementation to a new interpreter
+	Interpreter flat = Interpreter::fromClone(flattener);
+	return flat;
 }
 
 
 FlatteningInterpreter::FlatteningInterpreter(const Document<std::string>& doc) {
-	
+
 	_currGlobalTransition = NULL;
-	
-	// kust copy given doc into _document an create _flatDoc for the FSM
+
+	// just copy given doc into _document an create _flatDoc for the FSM
 	DOMImplementation<std::string> domFactory = Arabica::SimpleDOM::DOMImplementation<std::string>::getDOMImplementation();
 	_document = domFactory.createDocument(doc.getNamespaceURI(), "", 0);
 	_flatDoc = domFactory.createDocument(doc.getNamespaceURI(), "", 0);
@@ -70,10 +79,24 @@ FlatteningInterpreter::FlatteningInterpreter(const Document<std::string>& doc) {
 	addMonitor(this);
 }
 
-Document<std::string>& FlatteningInterpreter::getDocument() {
-	std::cout << "######################" << std::endl;
-	std::cout << _flatDoc << std::endl;
-	std::cout << "######################" << std::endl;
+FlatteningInterpreter::~FlatteningInterpreter() {
+	std::map<std::string, GlobalState*>::iterator confIter = _globalConf.begin();
+	while(confIter != _globalConf.end()) {
+		std::map<std::string, GlobalTransition*>::iterator transIter = confIter->second->outgoing.begin();
+		while (transIter != confIter->second->outgoing.end()) {
+			delete transIter->second;
+			transIter++;
+		}
+		delete confIter->second;
+		confIter++;
+	}
+
+}
+
+Document<std::string> FlatteningInterpreter::getDocument() const {
+//	std::cout << "######################" << std::endl;
+//	std::cout << _flatDoc << std::endl;
+//	std::cout << "######################" << std::endl;
 	return _flatDoc;
 }
 
@@ -81,7 +104,7 @@ void FlatteningInterpreter::interpret() {
 
 	init();
 	setupIOProcessors();
-	
+
 	// initialize the datamodel
 	std::string datamodelName;
 	if (datamodelName.length() == 0 && HAS_ATTR(_scxml, "datamodel"))
@@ -99,20 +122,19 @@ void FlatteningInterpreter::interpret() {
 		_dataModel = _factory->createDataModel("null", this);
 	}
 	if(datamodelName.length() > 0  && !_dataModel) {
-		std::cout << "No datamodel for " << datamodelName << " registered";
-	}
-	
-	if (_dataModel) {
-		_dataModel.assign("_x.args", _cmdLineOptions);
+		LOG(ERROR) << "No datamodel for " << datamodelName << " registered";
 	}
-	
+
 	_binding = (HAS_ATTR(_scxml, "binding") && iequals(ATTR(_scxml, "binding"), "late") ? LATE : EARLY);
 
-	
+	// reset
+	_globalConf.clear();
+	_currGlobalTransition = NULL;
+
 	// very first state
 	_start = new GlobalState(_configuration, _alreadyEntered, _historyValue);
 	_globalConf[_start->stateId] = _start;
-	
+
 	NodeSet<std::string> initialTransitions;
 
 	// enter initial configuration
@@ -120,9 +142,11 @@ void FlatteningInterpreter::interpret() {
 	initialStates = getInitialStates();
 	assert(initialStates.size() > 0);
 	for (int i = 0; i < initialStates.size(); i++) {
-		Element<std::string> initialElem = _document.createElementNS(_nsURL, "initial");
+		Element<std::string> initialElem = _document.createElementNS(_nsInfo.nsURL, "initial");
+		_nsInfo.setPrefix(initialElem);
 		initialElem.setAttribute("generated", "true");
-		Element<std::string> transitionElem = _document.createElementNS(_nsURL, "transition");
+		Element<std::string> transitionElem = _document.createElementNS(_nsInfo.nsURL, "transition");
+		_nsInfo.setPrefix(transitionElem);
 		transitionElem.setAttribute("target", ATTR(initialStates[i], "id"));
 		initialElem.appendChild(transitionElem);
 		_scxml.appendChild(initialElem);
@@ -130,8 +154,8 @@ void FlatteningInterpreter::interpret() {
 	}
 	labelTransitions();
 	weightTransitions();
-	
-	std::cout << _scxml << std::endl;
+
+//	std::cout << _scxml << std::endl;
 
 	GlobalTransition* globalTransition = new GlobalTransition(initialTransitions, _dataModel);
 	_start->outgoing[globalTransition->transitionId] = globalTransition;
@@ -140,22 +164,22 @@ void FlatteningInterpreter::interpret() {
 
 	enterStates(initialTransitions);
 	explode();
-		
+
 #if 0
 	// print set of global configurations
 	for(std::map<std::string, GlobalState*>::iterator globalConfIter = _globalConf.begin();
-			globalConfIter != _globalConf.end();
-			globalConfIter++) {
+	        globalConfIter != _globalConf.end();
+	        globalConfIter++) {
 		std::cout << globalConfIter->first << std::endl;
 	}
 	std::cout << _globalConf.size() << std::endl;
 #endif
-	
+
 	createDocument();
 }
 
 void FlatteningInterpreter::executeContent(const Arabica::DOM::Node<std::string>& content, bool rethrow) {
-	std::cout << content << std::endl;
+//	std::cout << content << std::endl;
 	GlobalTransition::Action action;
 
 	if (false) {
@@ -199,51 +223,55 @@ void FlatteningInterpreter::cancelInvoke(const Arabica::DOM::Node<std::string>&
 }
 
 void FlatteningInterpreter::internalDoneSend(const Arabica::DOM::Node<std::string>& state) {
-	
+
 	if (!isState(state))
 		return;
 	Arabica::DOM::Element<std::string> stateElem = (Arabica::DOM::Element<std::string>)state;
 
 //	if (parentIsScxmlState(state))
 //		return;
-	
+
 //	std::cout << "internalDoneSend: " << state << std::endl;
-	
+
 	// create onentry with a raise element
-	Element<std::string> onentry = _flatDoc.createElement("onentry");
-	Element<std::string> raise = _flatDoc.createElement("raise");
+	Element<std::string> onentry = _flatDoc.createElementNS(_nsInfo.nsURL, "onentry");
+	_nsInfo.setPrefix(onentry);
+
+	Element<std::string> raise = _flatDoc.createElementNS(_nsInfo.nsURL, "raise");
+	_nsInfo.setPrefix(raise);
+
 	onentry.appendChild(raise);
 
-	Arabica::XPath::NodeSet<std::string> doneDatas = filterChildElements(_xmlNSPrefix + "donedata", stateElem);
+	Arabica::XPath::NodeSet<std::string> doneDatas = filterChildElements(_nsInfo.xmlNSPrefix + "donedata", stateElem);
 	if (doneDatas.size() > 0) {
 		Arabica::DOM::Node<std::string> doneData = doneDatas[0];
-		Arabica::XPath::NodeSet<std::string> contents = filterChildElements(_xmlNSPrefix + "content", doneDatas[0]);
+		Arabica::XPath::NodeSet<std::string> contents = filterChildElements(_nsInfo.xmlNSPrefix + "content", doneDatas[0]);
 		if (contents.size() > 0) {
 			Node<std::string> imported = _flatDoc.importNode(contents[0], true);
 			raise.appendChild(imported);
 		}
-		Arabica::XPath::NodeSet<std::string> params = filterChildElements(_xmlNSPrefix + "param", doneDatas[0]);
+		Arabica::XPath::NodeSet<std::string> params = filterChildElements(_nsInfo.xmlNSPrefix + "param", doneDatas[0]);
 		if (params.size() > 0) {
 			Node<std::string> imported = _flatDoc.importNode(params[0], true);
 			raise.appendChild(imported);
 		}
 	}
-	
+
 	raise.setAttribute("event", "done.state." + ATTR(stateElem.getParentNode(), "id")); // parent?!
-	
+
 	GlobalTransition::Action action;
 	action.onEntry = onentry;
-	
+
 	_currGlobalTransition->actions.push_back(action);
-	
+
 }
 
 static bool isSuperset(const GlobalTransition* t1, const GlobalTransition* t2) {
 	bool isSuperset = true;
-	
+
 	if (t1->transitions.size() >= t2->transitions.size())
 		return false;
-	
+
 	for (int i = 0; i < t1->transitions.size(); i++) {
 		if (!InterpreterImpl::isMember(t1->transitions[i], t2->transitions)) {
 			isSuperset = false;
@@ -251,7 +279,7 @@ static bool isSuperset(const GlobalTransition* t1, const GlobalTransition* t2) {
 	}
 	return isSuperset;
 }
-	
+
 static NodeSet<std::string> filterChildEnabled(const NodeSet<std::string>& transitions) {
 	// drop any transition that is already enabled by a child
 	NodeSet<std::string> filteredTransitions;
@@ -269,7 +297,7 @@ static NodeSet<std::string> filterChildEnabled(const NodeSet<std::string>& trans
 					std::string eventDesc1 = ATTR(t1, "event");
 					std::string eventDesc2 = ATTR(t2, "event");
 					if (InterpreterImpl::nameMatch(eventDesc1, eventDesc2)) {
-						std::cout << "Dropping " << t1 << std::endl << "for " << t2 << std::endl;
+//						std::cout << "Dropping " << t1 << std::endl << "for " << t2 << std::endl;
 						goto SKIP_TRANSITION;
 					}
 				}
@@ -277,7 +305,8 @@ static NodeSet<std::string> filterChildEnabled(const NodeSet<std::string>& trans
 			}
 		}
 		filteredTransitions.push_back(t1);
-	SKIP_TRANSITION:;
+SKIP_TRANSITION:
+		;
 	}
 	return filteredTransitions;
 }
@@ -286,14 +315,14 @@ static std::list<GlobalTransition*> sortTransitions(std::list<GlobalTransition*>
 	bool stable = false;
 	while(!stable) {
 		for (std::list<GlobalTransition*>::iterator outerIter = list.begin();
-				 outerIter != list.end();
-				 outerIter++) {
+		        outerIter != list.end();
+		        outerIter++) {
 			for (std::list<GlobalTransition*>::iterator innerIter = outerIter;
-					 innerIter != list.end();
-					 innerIter++) {
+			        innerIter != list.end();
+			        innerIter++) {
 				GlobalTransition* t1 = *outerIter;
 				GlobalTransition* t2 = *innerIter;
-				
+
 				if (isSuperset(t1, t2)) {
 //					std::cout << "swapping " << t1->transitionId << " / " << t2->transitionId << std::endl;
 					std::swap(*innerIter, *outerIter);
@@ -313,7 +342,8 @@ static std::list<GlobalTransition*> sortTransitions(std::list<GlobalTransition*>
 			}
 		}
 		stable = true;
-	NEXT_ITER:;
+NEXT_ITER:
+		;
 	}
 	return list;
 }
@@ -321,7 +351,7 @@ static std::list<GlobalTransition*> sortTransitions(std::list<GlobalTransition*>
 
 
 void FlatteningInterpreter::explode() {
-	
+
 	// save global configuration elements to restore after recursive explode
 	Arabica::XPath::NodeSet<std::string> configuration = _configuration;
 	Arabica::XPath::NodeSet<std::string> alreadyEntered = _alreadyEntered;
@@ -334,19 +364,19 @@ void FlatteningInterpreter::explode() {
 	if (_currGlobalTransition) {
 		_currGlobalTransition->destination = globalState->stateId;
 		globalState->incoming[_currGlobalTransition->transitionId] = _currGlobalTransition;
-		
+
 //		if (!_currGlobalTransition->isEventless) {
-			// if it was an eventful transition, add all invokers
-			for (unsigned int i = 0; i < _statesToInvoke.size(); i++) {
-				NodeSet<std::string> invokes = filterChildElements(_xmlNSPrefix + "invoke", _statesToInvoke[i]);
-				for (unsigned int j = 0; j < invokes.size(); j++) {
-					invoke(invokes[j]);
-				}
+		// if it was an eventful transition, add all invokers
+		for (unsigned int i = 0; i < _statesToInvoke.size(); i++) {
+			NodeSet<std::string> invokes = filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _statesToInvoke[i]);
+			for (unsigned int j = 0; j < invokes.size(); j++) {
+				invoke(invokes[j]);
 			}
-			_statesToInvoke = NodeSet<std::string>();
+		}
+		_statesToInvoke = NodeSet<std::string>();
 //		}
 	}
-	
+
 	if (_globalConf.find(globalState->stateId) != _globalConf.end()) {
 		delete globalState;
 		return; // we have already been here
@@ -354,8 +384,8 @@ void FlatteningInterpreter::explode() {
 	_globalConf[globalState->stateId] = globalState;
 
 	// get all transition elements from states in the current configuration
-	NodeSet<std::string> allTransitions = filterChildElements(_xmlNSPrefix + "transition", configuration);
-	
+	NodeSet<std::string> allTransitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", configuration);
+
 	/**
 	 * From http://www.w3.org/TR/scxml/#SelectingTransitions
 	 *
@@ -365,8 +395,8 @@ void FlatteningInterpreter::explode() {
 	 *   c) T lacks a 'cond' attribute or its 'cond' attribute evaluates to "true"
 	 *
 	 * A transition is enabled by NULL in atomic state S if
-	 *   a) T lacks an 'event' attribute 
-	 *   b) T's source state is S or an ancestor of S 
+	 *   a) T lacks an 'event' attribute
+	 *   b) T's source state is S or an ancestor of S
 	 *   c) T lacks an 'cond' attribute or its 'cond' attribute evaluates to "true"
 	 *
 	 * The _source state_ of a transition is the <state> or <parallel> element that it occurs in.
@@ -380,14 +410,14 @@ void FlatteningInterpreter::explode() {
 	 *
 	 * Two transitions T1 and T2 conflict in state configuration C if their exit sets in C have a non-null intersection.
 	 *   let transitions T1 and T2 conflict:
-	 *     T1 is optimally enabled in atomic state S1 
+	 *     T1 is optimally enabled in atomic state S1
 	 *     T2 is optimally enabled in atomic state S2
 	 *     S1 and S2 are both active
 	 *   T1 has a higher priority than T2 if:
 	 *     a) T1's source state is a descendant of T2's source state, or
 	 *     b) S1 precedes S2 in document order
 	 *
-	 * The _optimal transition set_ enabled by event E in state configuration C is 
+	 * The _optimal transition set_ enabled by event E in state configuration C is
 	 * the largest set of transitions such that:
 	 *   a) each transition in the set is optimally enabled by E in an atomic state in C
 	 *   b) no transition conflicts with another transition in the set
@@ -395,14 +425,14 @@ void FlatteningInterpreter::explode() {
 	 *
 	 * A _microstep_ consists of the execution of the transitions in an optimal enabled transition set
 	 *
-	 * A _macrostep_ is a series of one or more microsteps ending in a configuration 
+	 * A _macrostep_ is a series of one or more microsteps ending in a configuration
 	 * where the internal event queue is empty and no transitions are enabled by NULL
 	 */
-	
-	
+
+
 	if (allTransitions.size() == 0)
 		return; // no transitions
-	
+
 	int nrElements = allTransitions.size();
 	int k = 0;
 	int* stack = (int*)malloc((nrElements + 1) * sizeof(int));
@@ -414,17 +444,17 @@ void FlatteningInterpreter::explode() {
 	while(1) {
 		// create the power set of all potential transitions
 		// see: http://www.programminglogic.com/powerset-algorithm-in-c/
-		
-		if (stack[k] < nrElements){
+
+		if (stack[k] < nrElements) {
 			stack[k+1] = stack[k] + 1;
 			k++;
 		}
-		
+
 		else {
 			stack[k-1]++;
 			k--;
 		}
-		
+
 		if (k==0)
 			break;
 
@@ -438,10 +468,10 @@ void FlatteningInterpreter::explode() {
 
 		// reduce to conflict-free subset
 		transitions = filterPreempted(transitions);
-				
+
 		// algorithm can never reduce to empty set
 		assert(transitions.size() > 0);
-		
+
 		// create a GlobalTransition object from the set
 		GlobalTransition* transition = new GlobalTransition(transitions, _dataModel);
 		if (!transition->isValid) {
@@ -452,7 +482,7 @@ void FlatteningInterpreter::explode() {
 
 		// two combinations might have projected onto the same conflict-free set
 		if (transitionSets.find(transition->transitionId) != transitionSets.end()) {
-			std::cout << "skipping as projected onto existing conflict-free subset" << std::endl;
+//			std::cout << "skipping as projected onto existing conflict-free subset" << std::endl;
 			delete transition;
 			continue;
 		}
@@ -475,7 +505,7 @@ void FlatteningInterpreter::explode() {
 			transition->firstElemPerLevel.push_back(lowestOrder);
 			transition->prioPerLevel.push_back(prioPerLevel);
 		}
-		
+
 #if 0
 		// calculate priority
 		transition->priority = 0;
@@ -495,25 +525,26 @@ void FlatteningInterpreter::explode() {
 					goto NEXT_DEPTH;
 				}
 			}
-		NEXT_DEPTH:;
+NEXT_DEPTH:
+			;
 		}
 #endif
 		// remember this conflict-free set
-		std::cout << "New conflict-free subset: " << transition->transitionId << ":" << transition->eventDesc << std::endl;
+//		std::cout << "New conflict-free subset: " << transition->transitionId << ":" << transition->eventDesc << std::endl;
 		transitionSets[transition->transitionId] = transition;
 	}
 
 	// TODO: reduce and sort transition sets
 	std::list<GlobalTransition*> transitionList;
 	for(std::map<std::string, GlobalTransition*>::iterator transSetIter = transitionSets.begin();
-			transSetIter != transitionSets.end();
-			transSetIter++) {
+	        transSetIter != transitionSets.end();
+	        transSetIter++) {
 		transitionList.push_back(transSetIter->second);
 	}
-	
+
 	for(std::list<GlobalTransition*>::iterator transListIter = transitionList.begin();
-			transListIter != transitionList.end();
-			transListIter++) {
+	        transListIter != transitionList.end();
+	        transListIter++) {
 
 		// add transition set to current global state
 		globalState->outgoing[(*transListIter)->transitionId] = *transListIter;
@@ -522,7 +553,7 @@ void FlatteningInterpreter::explode() {
 		_currGlobalTransition = *transListIter;
 		microstep((*transListIter)->transitions);
 		explode();
-		
+
 		// reset state for next transition set
 		_configuration = configuration;
 		_alreadyEntered = alreadyEntered;
@@ -530,12 +561,13 @@ void FlatteningInterpreter::explode() {
 
 	}
 }
-	
+
 void FlatteningInterpreter::createDocument() {
-	std::string xmlNs = _nsURL;
 	Node<std::string> _origSCXML = _scxml;
-	
-	_scxml = _flatDoc.createElementNS(xmlNs, "scxml");
+
+	_scxml = _flatDoc.createElementNS(_nsInfo.nsURL, "scxml");
+	_nsInfo.setPrefix(_scxml);
+
 	_scxml.setAttribute("flat", "true");
 	_flatDoc.appendChild(_scxml);
 
@@ -546,16 +578,16 @@ void FlatteningInterpreter::createDocument() {
 	if (HAS_ATTR(_origSCXML, "binding")) {
 		_scxml.setAttribute("binding", ATTR(_origSCXML, "binding"));
 	}
-	
+
 	_scxml.setAttribute("initial", _start->stateId);
 
 	NodeSet<std::string> datas;
 	if (_binding == InterpreterImpl::LATE) {
 		// with late binding, just copy direct datamodel childs
-		datas = filterChildElements(_xmlNSPrefix + "datamodel", _origSCXML);
+		datas = filterChildElements(_nsInfo.xmlNSPrefix + "datamodel", _origSCXML);
 	} else {
 		// with early binding, copy all datamodel elements into scxml element
-		datas = _xpath.evaluate("//" + _xpathPrefix + "datamodel", _origSCXML).asNodeSet();
+		datas = _xpath.evaluate("//" + _nsInfo.xpathPrefix + "datamodel", _origSCXML).asNodeSet();
 	}
 	for (int i = 0; i < datas.size(); i++) {
 		if (isInEmbeddedDocument(datas[i]))
@@ -564,25 +596,33 @@ void FlatteningInterpreter::createDocument() {
 		_scxml.appendChild(imported);
 	}
 
-	
-	NodeSet<std::string> scripts = filterChildElements(_xmlNSPrefix + "script", _origSCXML);
+
+	NodeSet<std::string> scripts = filterChildElements(_nsInfo.xmlNSPrefix + "script", _origSCXML);
 	for (int i = 0; i < scripts.size(); i++) {
 		Node<std::string> imported = _flatDoc.importNode(scripts[i], true);
 		_scxml.appendChild(imported);
 	}
 
+	NodeSet<std::string> comments = filterChildType(Node_base::COMMENT_NODE, _origSCXML);
+	for (int i = 0; i < comments.size(); i++) {
+		Node<std::string> imported = _flatDoc.importNode(comments[i], true);
+		_scxml.appendChild(imported);
+	}
+
 	for (std::map<std::string, GlobalState*>::iterator confIter = _globalConf.begin();
-			 confIter != _globalConf.end();
-			 confIter++) {
-		Node<std::string> state = globalStateToNode(confIter->second, xmlNs);
+	        confIter != _globalConf.end();
+	        confIter++) {
+		Node<std::string> state = globalStateToNode(confIter->second);
 		_scxml.appendChild(state);
 	}
 //	exit(0);
 
 }
 
-Node<std::string> FlatteningInterpreter::globalStateToNode(GlobalState* globalState, const std::string& xmlNs) {
-	Element<std::string> state = _flatDoc.createElementNS(xmlNs, "state");
+Node<std::string> FlatteningInterpreter::globalStateToNode(GlobalState* globalState) {
+	Element<std::string> state = _flatDoc.createElementNS(_nsInfo.nsURL, "state");
+	_nsInfo.setPrefix(state);
+
 	state.setAttribute("id", globalState->stateId);
 
 	if (globalState->isFinal)
@@ -590,20 +630,20 @@ Node<std::string> FlatteningInterpreter::globalStateToNode(GlobalState* globalSt
 
 	std::list<GlobalTransition*> transitionList;
 	for (std::map<std::string, GlobalTransition*>::iterator outIter = globalState->outgoing.begin();
-			 outIter != globalState->outgoing.end();
-			 outIter++) {
+	        outIter != globalState->outgoing.end();
+	        outIter++) {
 		transitionList.push_back(outIter->second);
 	}
 
 	transitionList = sortTransitions(transitionList);
-	
-	std::cout << "/////////////////" << std::endl;
+
+//	std::cout << "/////////////////" << std::endl;
 	for (std::list<GlobalTransition*>::iterator outIter = transitionList.begin();
-			 outIter != transitionList.end();
-			 outIter++) {
-		state.appendChild(globalTransitionToNode(*outIter, xmlNs));
+	        outIter != transitionList.end();
+	        outIter++) {
+		state.appendChild(globalTransitionToNode(*outIter));
 	}
-	std::cout << "/////////////////" << std::endl;
+//	std::cout << "/////////////////" << std::endl;
 
 	return state;
 }
@@ -611,8 +651,9 @@ Node<std::string> FlatteningInterpreter::globalStateToNode(GlobalState* globalSt
 /**
  * Creates transient states for executable content as a side-effect
  */
-Node<std::string> FlatteningInterpreter::globalTransitionToNode(GlobalTransition* globalTransition, const std::string& xmlNs) {
-	Element<std::string> transition = _flatDoc.createElementNS(xmlNs, "transition");
+Node<std::string> FlatteningInterpreter::globalTransitionToNode(GlobalTransition* globalTransition) {
+	Element<std::string> transition = _flatDoc.createElementNS(_nsInfo.nsURL, "transition");
+	_nsInfo.setPrefix(transition);
 
 	if (!globalTransition->isEventless) {
 		transition.setAttribute("event", globalTransition->eventDesc);
@@ -649,25 +690,26 @@ Node<std::string> FlatteningInterpreter::globalTransitionToNode(GlobalTransition
 	}
 	transition.setAttribute("prioPerLevel", nrSS.str());
 #endif
-	
+
 	transition.setAttribute("id", globalTransition->transitionId);
-	
+
 //	std::cout << " firstPerLevel:" << feSS.str() << " " << globalTransition->transitionId << std::endl;
 //	std::cout << "event: " << globalTransition->eventDesc << " firstPerLevel:" << feSS.str() << " numberPerLevel:" << nrSS.str() << " prioPerLevel:" << prSS.str() << " " << globalTransition->transitionId << std::endl;
 //	std::cout << globalTransition->transitionId << std::endl;
-		
+
 	NodeSet<std::string> transientStateChain;
 
 	// gather content for new transient state
 	NodeSet<std::string> childs;
-	
+
 	// iterate all actions taken during the transition
 	for (std::list<GlobalTransition::Action>::iterator actionIter = globalTransition->actions.begin();
-			 actionIter != globalTransition->actions.end();
-			 actionIter++) {
-		
+	        actionIter != globalTransition->actions.end();
+	        actionIter++) {
+
 		if (actionIter->transition) {
-			Element<std::string> onexit = _flatDoc.createElementNS(xmlNs, "onexit");
+			Element<std::string> onexit = _flatDoc.createElementNS(_nsInfo.nsURL, "onexit");
+			_nsInfo.setPrefix(onexit);
 			Node<std::string> child = actionIter->transition.getFirstChild();
 			while(child) {
 				Node<std::string> imported = _flatDoc.importNode(child, true);
@@ -700,7 +742,9 @@ Node<std::string> FlatteningInterpreter::globalTransitionToNode(GlobalTransition
 		}
 
 		if (actionIter->uninvoke) {
-			Element<std::string> uninvokeElem = _flatDoc.createElementNS(xmlNs, "uninvoke");
+			Element<std::string> uninvokeElem = _flatDoc.createElementNS(_nsInfo.nsURL, "uninvoke");
+			_nsInfo.setPrefix(uninvokeElem);
+
 			if (HAS_ATTR(actionIter->uninvoke, "type")) {
 				uninvokeElem.setAttribute("type", ATTR(actionIter->uninvoke, "type"));
 			}
@@ -720,7 +764,7 @@ Node<std::string> FlatteningInterpreter::globalTransitionToNode(GlobalTransition
 		if (actionIter->entered) {
 			// we entered a new child - check if it has a datamodel and we entered for the first time
 			if (_binding == InterpreterImpl::LATE) {
-				NodeSet<std::string> datamodel = filterChildElements(_xmlNSPrefix + "datamodel", actionIter->entered);
+				NodeSet<std::string> datamodel = filterChildElements(_nsInfo.xmlNSPrefix + "datamodel", actionIter->entered);
 				if (datamodel.size() > 0 && !isMember(actionIter->entered, _globalConf[globalTransition->source]->alreadyEnteredStates)) {
 					childs.push_back(datamodel);
 				}
@@ -740,43 +784,44 @@ Node<std::string> FlatteningInterpreter::globalTransitionToNode(GlobalTransition
 	}
 
 	CREATE_TRANSIENT_STATE_WITH_CHILDS
-	
+
 	if (transientStateChain.size() > 0) {
 		for (int i = 0; i < transientStateChain.size(); i++) {
 			Element<std::string> transientStateElem = Element<std::string>(transientStateChain[i]);
 			transientStateElem.setAttribute("id", "transient-" + globalTransition->transitionId + "-" + globalTransition->source + "-" + toStr(i));
 
-			Element<std::string> exitTransition = _flatDoc.createElementNS(xmlNs, "transition");
-			
+			Element<std::string> exitTransition = _flatDoc.createElementNS(_nsInfo.nsURL, "transition");
+			_nsInfo.setPrefix(exitTransition);
+
 			if (i == transientStateChain.size() - 1) {
 				exitTransition.setAttribute("target", globalTransition->destination);
 			} else {
 				exitTransition.setAttribute("target", "transient-" + globalTransition->transitionId + "-" + globalTransition->source + "-" + toStr(i + 1));
 			}
 			transientStateElem.appendChild(exitTransition);
-			
+
 			if (i == 0)
 				transition.setAttribute("target", transientStateElem.getAttribute("id"));
-			
+
 			_scxml.appendChild(transientStateElem);
 		}
 	} else {
 		transition.setAttribute("target", globalTransition->destination);
 	}
-		
+
 	return transition;
 }
 
 void FlatteningInterpreter::weightTransitions() {
 	maxDepth = 0;
 	maxOrder = 0;
-	
+
 	int depth = 0;
 	Arabica::XPath::NodeSet<std::string> states = getChildStates(_scxml);
 	while(states.size() > 0) {
-		NodeSet<std::string> transitions = filterChildElements(_xmlNSPrefix + "transition", states);
-		NodeSet<std::string> initials = filterChildElements(_xmlNSPrefix + "initial", states);
-		transitions.push_back(filterChildElements(_xmlNSPrefix + "transition", initials));
+		NodeSet<std::string> transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", states);
+		NodeSet<std::string> initials = filterChildElements(_nsInfo.xmlNSPrefix + "initial", states);
+		transitions.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "transition", initials));
 
 		for (int j = 0; j < transitions.size(); j++) {
 			if (depth > maxDepth)
@@ -791,24 +836,24 @@ void FlatteningInterpreter::weightTransitions() {
 		states = getChildStates(states);
 	}
 }
-	
+
 void FlatteningInterpreter::labelTransitions() {
 	// put a unique id on each transition
 	Arabica::XPath::NodeSet<std::string> states = getAllStates();
 	states.push_back(_scxml);
 	for (int i = 0; i < states.size(); i++) {
 		std::string stateId = ATTR(states[i], "id");
-		NodeSet<std::string> transitions = filterChildElements(_xmlNSPrefix + "transition", states[i]);
+		NodeSet<std::string> transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", states[i]);
 		// some transitions are in the inital elements
-		NodeSet<std::string> initials = filterChildElements(_xmlNSPrefix + "initial", states[i]);
-		transitions.push_back(filterChildElements(_xmlNSPrefix + "transition", initials));
+		NodeSet<std::string> initials = filterChildElements(_nsInfo.xmlNSPrefix + "initial", states[i]);
+		transitions.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "transition", initials));
 		for (int j = 0; j < transitions.size(); j++) {
 			Element<std::string> transition = Element<std::string>(transitions[j]);
 			transition.setAttribute("id", stateId + ":"+ toStr(j + 1));
 		}
 	}
 }
-	
+
 void FlatteningInterpreter::beforeMicroStep(Interpreter interpreter) {
 }
 void FlatteningInterpreter::onStableConfiguration(Interpreter interpreter) {
@@ -828,31 +873,31 @@ void FlatteningInterpreter::beforeEnteringState(Interpreter interpreter, const A
 void FlatteningInterpreter::beforeTakingTransition(Interpreter interpreter, const Arabica::DOM::Element<std::string>& transition, bool moreComing) {
 }
 
-	
+
 GlobalState::GlobalState(const Arabica::XPath::NodeSet<std::string>& activeStates_,
-												 const Arabica::XPath::NodeSet<std::string>& alreadyEnteredStates_, // we need to remember for binding=late
-												 const std::map<std::string, Arabica::XPath::NodeSet<std::string> >& historyStates_) {
-	
+                         const Arabica::XPath::NodeSet<std::string>& alreadyEnteredStates_, // we need to remember for binding=late
+                         const std::map<std::string, Arabica::XPath::NodeSet<std::string> >& historyStates_) {
+
 	// make copies and sort
 	activeStates = activeStates_;
 	alreadyEnteredStates = alreadyEnteredStates_;
 	historyStates = historyStates_;
 	isFinal = true; // is set to false if we contain a non-final state
-	
+
 	// start state is not final
 	if (activeStates.size() == 0) {
 		isFinal = false;
 	}
-	
+
 	// sort configuration
 	activeStates.to_document_order();
 	alreadyEnteredStates.to_document_order();
 	for(std::map<std::string, Arabica::XPath::NodeSet<std::string> >::iterator historyIter = historyStates.begin();
-			historyIter != historyStates.end();
-			historyIter++) {
+	        historyIter != historyStates.end();
+	        historyIter++) {
 		historyIter->second.to_document_order();
 	}
-	
+
 	// create a unique identifier for a global configuration
 	std::ostringstream idSS;
 	idSS << "active-";
@@ -867,10 +912,10 @@ GlobalState::GlobalState(const Arabica::XPath::NodeSet<std::string>& activeState
 		idSS << ATTR(alreadyEnteredStates[i], "id") << "-";
 	}
 	idSS << ";";
-	
+
 	for(std::map<std::string, Arabica::XPath::NodeSet<std::string> >::const_iterator histIter = historyStates.begin();
-			histIter != historyStates.end();
-			histIter++) {
+	        histIter != historyStates.end();
+	        histIter++) {
 		const Arabica::XPath::NodeSet<std::string>& histStates = histIter->second;
 		idSS << "history-";
 		idSS << histIter->first << "-";
@@ -878,7 +923,7 @@ GlobalState::GlobalState(const Arabica::XPath::NodeSet<std::string>& activeState
 			idSS << ATTR(histStates[i], "id") << "-";
 		}
 	}
-	
+
 	stateId = idSS.str();
 }
 
@@ -886,7 +931,7 @@ GlobalTransition::GlobalTransition(const Arabica::XPath::NodeSet<std::string>& t
 	transitions = transitionSet;
 	isValid = true;
 	isEventless = true;
-	
+
 #if 0
 	std::cout << "################" << std::endl;
 	for (int i = 0; i < transitions.size(); i++) {
@@ -894,14 +939,14 @@ GlobalTransition::GlobalTransition(const Arabica::XPath::NodeSet<std::string>& t
 	}
 	std::cout << "################" << std::endl;
 #endif
-	
+
 	std::list<std::string> conditions;
 	std::ostringstream setId; // also build id for subset
 	for (int i = 0; i < transitions.size(); i++) {
 		// get a unique string for the transition - we assume it is sorted
 		assert(HAS_ATTR(transitions[i], "id"));
 		setId << ATTR(transitions[i], "id") << "-";
-		
+
 		// gather conditions while we are iterating anyway
 		if (HAS_ATTR(transitions[i], "cond")) {
 			conditions.push_back(ATTR(transitions[i], "cond"));
@@ -920,7 +965,7 @@ GlobalTransition::GlobalTransition(const Arabica::XPath::NodeSet<std::string>& t
 	bool foundEventLess = false;
 	bool foundWithTarget = false;
 	bool foundTargetLess = false;
-	
+
 	for (int i = 0; i < transitions.size(); i++) {
 		if (HAS_ATTR(transitions[i], "eventexpr")) {
 			Event e("error.execution", Event::PLATFORM);
@@ -947,7 +992,7 @@ GlobalTransition::GlobalTransition(const Arabica::XPath::NodeSet<std::string>& t
 		}
 
 	}
-	
+
 	// do not mix eventless and event transitions
 	if (foundEventLess && foundWithEvent) {
 		isValid = false;
@@ -962,20 +1007,20 @@ GlobalTransition::GlobalTransition(const Arabica::XPath::NodeSet<std::string>& t
 
 	isEventless = foundEventLess;
 	isTargetless = !foundWithTarget;
-	
+
 	// is there a set of event names that would enable this conflict-free transition set?
 	if (foundWithEvent) {
 		// get the set of longest event descriptors that will enable this transition set
 		eventNames = getCommonEvents(transitions);
 		if (eventNames.size() == 0) {
-			std::cout << "No event will activate this conflict-free subset" << std::endl;
+//			LOG(INFO) << "No event will activate this conflict-free subset" << std::endl;
 			isValid = false;
 			return;
 		} else {
 			std::string seperator = "";
 			for (std::list<std::string>::iterator eventIter = eventNames.begin();
-					 eventIter != eventNames.end();
-					 eventIter++) {
+			        eventIter != eventNames.end();
+			        eventIter++) {
 				eventDesc += seperator + *eventIter;
 				seperator = " ";
 			}
@@ -983,35 +1028,35 @@ GlobalTransition::GlobalTransition(const Arabica::XPath::NodeSet<std::string>& t
 		if (eventDesc.size() == 0)
 			eventDesc = "*";
 	}
-	
+
 	if (conditions.size() > 0) {
 		condition = dataModel.andExpressions(conditions);
 		if (condition.size() == 0) {
-			std::cout << "Datamodel does not support to conjungate expressions!" << std::endl;
+			LOG(ERROR) << "Datamodel does not support to conjungate expressions!" << std::endl;
 		}
 	}
 }
-	
+
 std::list<std::string> GlobalTransition::getCommonEvents(const NodeSet<std::string>& transitions) {
 	std::list<std::string> prefixes;
 	std::list<std::string> longestPrefixes;
-	
+
 	for (int i = 0; i < transitions.size(); i++) {
 		// for every transition
 		std::list<std::string> eventNames = Interpreter::tokenizeIdRefs(ATTR(transitions[i], "event"));
-		
+
 		for (std::list<std::string>::iterator eventNameIter = eventNames.begin();
-				 eventNameIter != eventNames.end();
-				 eventNameIter++) {
+		        eventNameIter != eventNames.end();
+		        eventNameIter++) {
 			// for every event descriptor
 			std::string eventName = *eventNameIter;
-			
+
 			// remove trailing .*
 			if (eventName.find("*", eventName.size() - 1) != std::string::npos)
 				eventName = eventName.substr(0, eventName.size() - 1);
 			if (eventName.find(".", eventName.size() - 1) != std::string::npos)
 				eventName = eventName.substr(0, eventName.size() - 1);
-			
+
 			bool isMatching = true;
 			for (int j = 0; j < transitions.size(); j++) {
 				// check if token would activate all other transitions
@@ -1027,20 +1072,20 @@ std::list<std::string> GlobalTransition::getCommonEvents(const NodeSet<std::stri
 			}
 		}
 	}
-	
+
 	// from the set of event names, remove those that are prefixes
 	for (std::list<std::string>::iterator outerEventNameIter = prefixes.begin();
-			 outerEventNameIter != prefixes.end();
-			 outerEventNameIter++) {
+	        outerEventNameIter != prefixes.end();
+	        outerEventNameIter++) {
 		for (std::list<std::string>::iterator innerEventNameIter = prefixes.begin();
-				 innerEventNameIter != prefixes.end();
-				 innerEventNameIter++) {
+		        innerEventNameIter != prefixes.end();
+		        innerEventNameIter++) {
 			if (!iequals(*outerEventNameIter, *innerEventNameIter) && Interpreter::nameMatch(*outerEventNameIter, *innerEventNameIter)) {
 				goto IS_PREFIX;
 			}
 		}
 		longestPrefixes.push_back(*outerEventNameIter);
-	IS_PREFIX:
+IS_PREFIX:
 		;
 	}
 	return longestPrefixes;
diff --git a/src/uscxml/transform/ChartToFSM.h b/src/uscxml/transform/ChartToFSM.h
index 14ec4e7..80f532a 100644
--- a/src/uscxml/transform/ChartToFSM.h
+++ b/src/uscxml/transform/ChartToFSM.h
@@ -37,21 +37,21 @@ public:
 
 	GlobalState() {}
 	GlobalState(const Arabica::XPath::NodeSet<std::string>& activeStates,
-							const Arabica::XPath::NodeSet<std::string>& alreadyEnteredStates, // we need to remember for binding=late
-							const std::map<std::string, Arabica::XPath::NodeSet<std::string> >& historyStates);
-		
+	            const Arabica::XPath::NodeSet<std::string>& alreadyEnteredStates, // we need to remember for binding=late
+	            const std::map<std::string, Arabica::XPath::NodeSet<std::string> >& historyStates);
+
 	Arabica::XPath::NodeSet<std::string> activeStates;
 	Arabica::XPath::NodeSet<std::string> alreadyEnteredStates;
 	std::map<std::string, Arabica::XPath::NodeSet<std::string> > historyStates;
-	
+
 	std::map<std::string, GlobalTransition*> incoming;
 	std::map<std::string, GlobalTransition*> outgoing;
 	std::string stateId;
-	
+
 	bool isFinal;
 };
 
-	
+
 class GlobalTransition {
 public:
 	class Action {
@@ -64,24 +64,24 @@ public:
 		Arabica::DOM::Node<std::string> invoke;
 		Arabica::DOM::Node<std::string> uninvoke;
 	};
-	
+
 	GlobalTransition(const Arabica::XPath::NodeSet<std::string>& transitions, DataModel dataModel);
-	
+
 	bool isValid; // constructor will determine, calling code will delete if not
 	bool isEventless; // whether or not all our transitions are eventless
 	bool isTargetless; // whether or not all our transitions are eventless
 	bool isSubset; // there is a superset to this set
-	
+
 	std::vector<long> firstElemPerLevel;
 	std::vector<long> nrElemPerLevel;
 	std::vector<long> prioPerLevel;
-	
+
 	Arabica::XPath::NodeSet<std::string> transitions; // constituting transitions
 
 	std::list<std::string> eventNames; // the list of longest event names that will enable this set
 	std::string eventDesc; // space-seperated eventnames for convenience
 	std::string condition; // conjunction of all the set's conditions
-	
+
 	// executable content we gathered when we took the transition
 	std::list<Action> actions;
 
@@ -90,19 +90,21 @@ public:
 
 	Arabica::XPath::NodeSet<std::string> invoke;
 	Arabica::XPath::NodeSet<std::string> uninvoke;
-	
+
 	std::string transitionId;
 	std::string source;
 	std::string destination;
-	
+
 protected:
-	std::list<std::string> getCommonEvents(const Arabica::XPath::NodeSet<std::string>& transitions);	
+	std::list<std::string> getCommonEvents(const Arabica::XPath::NodeSet<std::string>& transitions);
 };
-	
+
 class FlatteningInterpreter : public InterpreterDraft6, public InterpreterMonitor {
 public:
 	FlatteningInterpreter(const Arabica::DOM::Document<std::string>& doc);
-	Arabica::DOM::Document<std::string>& getDocument(); // overwrite to return flat FSM
+	virtual ~FlatteningInterpreter();
+
+	Arabica::DOM::Document<std::string> getDocument() const; // overwrite to return flat FSM
 	void interpret();
 
 protected:
@@ -131,22 +133,22 @@ protected:
 	void weightTransitions();
 	void createDocument();
 
-	Arabica::DOM::Node<std::string> globalStateToNode(GlobalState* globalState, const std::string& xmlNs);
-	Arabica::DOM::Node<std::string> globalTransitionToNode(GlobalTransition* globalTransition, const std::string& xmlNs);
+	Arabica::DOM::Node<std::string> globalStateToNode(GlobalState* globalState);
+	Arabica::DOM::Node<std::string> globalTransitionToNode(GlobalTransition* globalTransition);
 
 	GlobalState* _start;
 	GlobalTransition* _currGlobalTransition;
-	
+
 	int maxDepth;
 	int maxOrder;
-	
+
 	Arabica::DOM::Document<std::string> _flatDoc;
 	std::map<std::string, GlobalState*> _globalConf;
 };
-	
+
 class ChartToFSM {
 public:
-	static Arabica::DOM::Document<std::string> flatten(const Arabica::DOM::Document<std::string>& doc, const std::map<std::string, std::string>& nameSpaceInfo);
+	static Interpreter flatten(const Interpreter& other);
 };
 
 }
diff --git a/src/uscxml/transform/FSMToPromela.cpp b/src/uscxml/transform/FSMToPromela.cpp
index 0c61900..dc3b581 100644
--- a/src/uscxml/transform/FSMToPromela.cpp
+++ b/src/uscxml/transform/FSMToPromela.cpp
@@ -19,10 +19,13 @@
 
 #include "uscxml/transform/ChartToFSM.h"
 #include "uscxml/transform/FSMToPromela.h"
+#include "uscxml/plugins/datamodel/promela/PromelaParser.h"
 #include <DOM/io/Stream.hpp>
 #include <iostream>
 #include "uscxml/UUID.h"
 #include <math.h>
+#include <boost/algorithm/string.hpp>
+#include <glog/logging.h>
 
 namespace uscxml {
 
@@ -30,47 +33,696 @@ using namespace Arabica::DOM;
 using namespace Arabica::XPath;
 
 void FSMToPromela::writeProgram(std::ostream& stream,
-																const Arabica::DOM::Document<std::string>& doc,
-																const std::map<std::string, std::string>& namespaceInfo) {
+                                const Interpreter& interpreter) {
+	FSMToPromela promelaWriter;
+	interpreter.getImpl()->copyTo(&promelaWriter);
+	promelaWriter.writeProgram(stream);
+}
+
+FSMToPromela::FSMToPromela() : _eventTrie(".") {
+}
+
+void FSMToPromela::writeEvents(std::ostream& stream) {
+	std::list<TrieNode*> eventNames = _eventTrie.getWordsWithPrefix("");
+	std::list<TrieNode*>::iterator eventIter = eventNames.begin();
+	stream << "// event name identifiers" << std::endl;
+	while(eventIter != eventNames.end()) {
+		stream << "#define " << "e" << (*eventIter)->identifier << " " << (*eventIter)->identifier;
+		stream << " // from \"" << (*eventIter)->value << "\"" << std::endl;
+		eventIter++;
+	}
+}
+
+void FSMToPromela::writeStates(std::ostream& stream) {
+	stream << "// state name identifiers" << std::endl;
+	for (int i = 0; i < _globalStates.size(); i++) {
+		stream << "#define " << "s" << i << " " << i;
+		stream << " // from \"" << ATTR(_globalStates[i], "id") << "\"" << std::endl;
+	}
+
+}
+
+Arabica::XPath::NodeSet<std::string> FSMToPromela::getTransientContent(const Arabica::DOM::Node<std::string>& state) {
+	Arabica::XPath::NodeSet<std::string> content;
+	Arabica::DOM::Node<std::string> currState = state;
+	for (;;) {
+		if (!HAS_ATTR(currState, "transient") || !DOMUtils::attributeIsTrue(ATTR(currState, "transient")))
+			break;
+		content.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "invoke", currState));
+		content.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "onentry", currState));
+		content.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "onexit", currState));
+		NodeSet<std::string> transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", currState);
+		currState = _states[ATTR(transitions[0], "target")];
+	}
+
+	return content;
+}
+
+Node<std::string> FSMToPromela::getUltimateTarget(const Arabica::DOM::Node<std::string>& transition) {
+	Arabica::DOM::Node<std::string> currState = _states[ATTR(transition, "target")];
+
+	for (;;) {
+		if (!HAS_ATTR(currState, "transient") || !DOMUtils::attributeIsTrue(ATTR(currState, "transient")))
+			return currState;
+		NodeSet<std::string> transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", currState);
+		currState = _states[ATTR(transitions[0], "target")];
+	}
+}
+	
+void FSMToPromela::writeInlineComment(std::ostream& stream, const Arabica::DOM::Node<std::string>& node) {
+	if (node.getNodeType() != Node_base::COMMENT_NODE)
+		return;
+
+	std::string comment = node.getNodeValue();
+	boost::trim(comment);
+	if (!boost::starts_with(comment, "promela-inline:"))
+		return;
+
+	std::stringstream ssLine(comment);
+	std::string line;
+	std::getline(ssLine, line); // consume first line
+	while(std::getline(ssLine, line)) {
+		if (line.length() == 0)
+			continue;
+		stream << line;
+	}
+}
+
+void FSMToPromela::writeExecutableContent(std::ostream& stream, const Arabica::DOM::Node<std::string>& node, int indent) {
+
+	std::string padding;
+	for (int i = 0; i < indent; i++) {
+		padding += "  ";
+	}
+	
+	if (node.getNodeType() == Node_base::COMMENT_NODE) {
+		std::string comment = node.getNodeValue();
+		boost::trim(comment);
+		std::stringstream inlinePromela;
+		if (!boost::starts_with(comment, "promela-inline:"))
+			return;
+		std::stringstream ssLine(comment);
+		std::string line;
+		std::getline(ssLine, line); // consume first line
+		while(std::getline(ssLine, line)) {
+			if (line.length() == 0)
+				continue;
+			inlinePromela << line << std::endl;
+		}
+		stream << padding << "skip;" << std::endl;
+		stream << beautifyIndentation(inlinePromela.str(), indent) << std::endl;
+	}
+	
+	if (node.getNodeType() != Node_base::ELEMENT_NODE)
+		return;
+
+	if (false) {
+	} else if(TAGNAME(node) == "state") {
+		if (HAS_ATTR(node, "transient") && DOMUtils::attributeIsTrue(ATTR(node, "transient"))) {
+			Arabica::XPath::NodeSet<std::string> execContent = getTransientContent(node);
+			for (int i = 0; i < execContent.size(); i++) {
+				writeExecutableContent(stream, execContent[i], indent);
+			}
+		} else {
+			Arabica::DOM::Node<std::string> child = node.getFirstChild();
+			while(child) {
+				writeExecutableContent(stream, child, indent);
+				child = child.getNextSibling();
+			}
+		}
+	} else if(TAGNAME(node) == "transition") {
+		stream << "t" << _transitions[node] << ":" << std::endl;
+		
+		// check for special promela labels
+		PromelaInlines promInls = getInlinePromela(getTransientContent(_states[ATTR(node, "target")]), true);
+
+		if (promInls.hasAcceptLabel)
+			stream << padding << "acceptLabelT" << _transitions[node] << ":" << std::endl;
+		if (promInls.hasEndLabel)
+			stream << padding << "endLabelT" << _transitions[node] << ":" << std::endl;
+		if (promInls.hasProgressLabel)
+			stream << padding << "progressLabelT" << _transitions[node] << ":" << std::endl;
+		
+		stream << padding << "atomic {" << std::endl;
+		writeExecutableContent(stream, _states[ATTR(node, "target")], indent+1);
+		stream << padding << "  skip;" << std::endl;
+		
+		Node<std::string> newState = getUltimateTarget(node);
+		for (int i = 0; i < _globalStates.size(); i++) {
+			if (newState != _globalStates[i])
+				continue;
+			stream << padding << "  s = s" << i << ";" << std::endl;
+		}
+
+		stream << padding << "}" << std::endl;
+		if (isFinal(newState)) {
+			stream << padding << "goto terminate;" << std::endl;
+		} else {
+			stream << padding << "goto nextStep;" << std::endl;
+		}
+		
+	} else if(TAGNAME(node) == "onentry" || TAGNAME(node) == "onexit") {
+		Arabica::DOM::Node<std::string> child = node.getFirstChild();
+		while(child) {
+			writeExecutableContent(stream, child, indent);
+			child = child.getNextSibling();
+		}
+		
+	} else if(TAGNAME(node) == "script") {
+		NodeSet<std::string> scriptText = filterChildType(Node_base::TEXT_NODE, node, true);
+		for (int i = 0; i < scriptText.size(); i++) {
+			stream << beautifyIndentation(scriptText[i].getNodeValue(), indent) << std::endl;
+		}
+		
+	} else if(TAGNAME(node) == "log") {
+		// ignore
+		
+	} else if(TAGNAME(node) == "foreach") {
+		if (HAS_ATTR(node, "index"))
+			stream << padding << ATTR(node, "index") << " = 0;" << std::endl;
+		stream << padding << "for (" << ATTR(node, "item") << " in " << ATTR(node, "array") << ") {" << std::endl;
+		Arabica::DOM::Node<std::string> child = node.getFirstChild();
+		while(child) {
+			writeExecutableContent(stream, child, indent + 1);
+			child = child.getNextSibling();
+		}
+		if (HAS_ATTR(node, "index"))
+			stream << padding << "  " << ATTR(node, "index") << "++;" << std::endl;
+		stream << padding << "}" << std::endl;
+
+	} else if(TAGNAME(node) == "if") {
+		NodeSet<std::string> condChain;
+		condChain.push_back(node);
+		condChain.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "elseif", node));
+		condChain.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "else", node));
+
+		writeIfBlock(stream, condChain, indent);
+		
+	} else if(TAGNAME(node) == "raise") {
+		TrieNode* trieNode = _eventTrie.getNodeWithPrefix(ATTR(node, "event"));
+		stream << padding << "iQ!e" << trieNode->identifier << ";" << std::endl;
+	} else if(TAGNAME(node) == "invoke") {
+		stream << padding << "run " << ATTR(node, "invokeid") << "EventSource();" << std::endl;
+	} else if(TAGNAME(node) == "uninvoke") {
+		stream << padding << ATTR(node, "invokeid") << "EventSourceDone" << "= 1;" << std::endl;
+	} else {
+
+		std::cerr << "'" << TAGNAME(node) << "'" << std::endl << node << std::endl;
+		assert(false);
+	}
+
+}
+
+PromelaInlines FSMToPromela::getInlinePromela(const Arabica::XPath::NodeSet<std::string>& elements, bool recurse) {
+	PromelaInlines prom;
+
+	if (elements.size() == 0)
+		return prom;
+
+	Arabica::XPath::NodeSet<std::string> comments = filterChildType(Node_base::COMMENT_NODE, elements, recurse);
+	for (int i = 0; i < comments.size(); i++) {
+		std::stringstream ssLine(comments[i].getNodeValue());
+		std::string line;
+
+		bool isInPromelaCode = false;
+		PromelaInline promInl;
+
+		while(std::getline(ssLine, line)) {
+			std::string trimLine = boost::trim_copy(line);
+			if (line.length() == 0)
+				continue;
+			if (false) {
+			} else if (boost::starts_with(trimLine, "promela-progress")) {
+				prom.hasProgressLabel = true;
+				if (isInPromelaCode) {
+					prom.inlines.push_back(promInl);
+					isInPromelaCode = false;
+				}
+				promInl.type = PromelaInline::PROMELA_PROGRESS_LABEL;
+				promInl.content = line;
+				prom.inlines.push_back(promInl);
+			} else if (boost::starts_with(trimLine, "promela-accept")) {
+				prom.hasAcceptLabel = true;
+				if (isInPromelaCode) {
+					prom.inlines.push_back(promInl);
+					isInPromelaCode = false;
+				}
+				promInl.type = PromelaInline::PROMELA_ACCEPT_LABEL;
+				promInl.content = line;
+				prom.inlines.push_back(promInl);
+			} else if (boost::starts_with(trimLine, "promela-end")) {
+				prom.hasEndLabel = true;
+				if (isInPromelaCode) {
+					prom.inlines.push_back(promInl);
+					isInPromelaCode = false;
+				}
+				promInl.type = PromelaInline::PROMELA_END_LABEL;
+				promInl.content = line;
+				prom.inlines.push_back(promInl);
+			} else if (boost::starts_with(trimLine, "promela-inline")) {
+				prom.hasCode = true;
+				isInPromelaCode = true;
+				promInl.type = PromelaInline::PROMELA_CODE;
+			} else if (isInPromelaCode) {
+				promInl.content += line;
+			}
+		}
+		// inline code ends with comment
+		if (isInPromelaCode) {
+			prom.inlines.push_back(promInl);
+		}
+	}
+	return prom;
+}
+	
+void FSMToPromela::writeIfBlock(std::ostream& stream, const Arabica::XPath::NodeSet<std::string>& condChain, int indent) {
+	if (condChain.size() == 0)
+		return;
+	
+	std::string padding;
+	for (int i = 0; i < indent; i++) {
+		padding += "  ";
+	}
+	
+	bool noNext = condChain.size() == 1;
+	bool nextIsElse = false;
+	if (condChain.size() > 1) {
+		if (TAGNAME(condChain[1]) == "else") {
+			nextIsElse = true;
+		}
+	}
+	
+	Node<std::string> ifNode = condChain[0];
+	
+	stream << padding << "if" << std::endl;
+	// we need to nest the elseifs to resolve promela if semantics
+	stream << padding << ":: (" << ATTR(ifNode, "cond") << ") -> {" << std::endl;
+	
+	Arabica::DOM::Node<std::string> child;
+	if (TAGNAME(ifNode) == "if") {
+		child = ifNode.getFirstChild();
+	} else {
+		child = ifNode.getNextSibling();
+	}
+	while(child) {
+		if (child.getNodeType() == Node_base::ELEMENT_NODE) {
+			if (TAGNAME(child) == "elseif" || TAGNAME(child) == "else")
+				break;
+		}
+		writeExecutableContent(stream, child, indent + 1);
+		child = child.getNextSibling();
+	}
+	stream << padding << "}" << std::endl;
+	stream << padding << ":: else -> ";
+
+	if (nextIsElse) {
+		child = condChain[1].getNextSibling();
+		stream << "{" << std::endl;
+		while(child) {
+			writeExecutableContent(stream, child, indent + 1);
+			child = child.getNextSibling();
+		}
+		stream << padding << "}" << std::endl;
+
+	} else if (noNext) {
+		stream << "skip;" << std::endl;
+	} else {
+		stream << "{" << std::endl;
+		
+		Arabica::XPath::NodeSet<std::string> cdrCondChain;
+		for (int i = 1; i < condChain.size(); i++) {
+			cdrCondChain.push_back(condChain[i]);
+		}
+		writeIfBlock(stream, cdrCondChain, indent + 1);
+		stream << padding << "}" << std::endl;
+
+	}
+	
+	stream << padding << "fi;" << std::endl;
+
+}
+
+std::string FSMToPromela::beautifyIndentation(const std::string& code, int indent) {
+
+	std::string padding;
+	for (int i = 0; i < indent; i++) {
+		padding += "  ";
+	}
+
+	// remove topmost indentation from every line and reindent
+	std::stringstream beautifiedSS;
+	
+	std::string initialIndent;
+	bool gotIndent = false;
+	bool isFirstLine = true;
+	std::stringstream ssLine(code);
+	std::string line;
+
+	while(std::getline(ssLine, line)) {
+		size_t firstChar = line.find_first_not_of(" \t\r\n");
+		if (firstChar != std::string::npos) {
+			if (!gotIndent) {
+				initialIndent = line.substr(0, firstChar);
+				gotIndent = true;
+			}
+			beautifiedSS << (isFirstLine ? "" : "\n") << padding << boost::replace_first_copy(line, initialIndent, "");
+			isFirstLine = false;
+		}
+	}
+	
+	return beautifiedSS.str();
+}
+	
+void FSMToPromela::writeDeclarations(std::ostream& stream) {
+	
+	// get all data elements
+	NodeSet<std::string> datas = _xpath.evaluate("//" + _nsInfo.xpathPrefix + "data", _scxml).asNodeSet();
+	NodeSet<std::string> dataText = filterChildType(Node_base::TEXT_NODE, datas, true);
+
+	// write their text content
+	stream << "// datamodel variables" << std::endl;
+	for (int i = 0; i < dataText.size(); i++) {
+		Node<std::string> data = dataText[i];
+		stream << beautifyIndentation(data.getNodeValue()) << std::endl;
+	}
+	
+	stream << std::endl;
+	stream << "// global variables" << std::endl;
+	stream << "int e;                   /* current event */" << std::endl;
+	stream << "int s;                   /* current state */" << std::endl;
+	stream << "chan iQ = [100] of {int} /* internal queue */" << std::endl;
+	stream << "chan eQ = [100] of {int} /* external queue */" << std::endl;
+
+	stream << std::endl;
+	stream << "// event sources" << std::endl;
+	if (_globalEventSource)
+		stream << "bool globalEventSourceDone;" << std::endl;
+	
+	std::map<std::string, PromelaEventSource>::iterator invIter = _invokers.begin();
+	while(invIter != _invokers.end()) {
+		stream << "bool " << invIter->first << "EventSourceDone;" << std::endl;
+		stream << std::endl;
+		invIter++;
+	}
+
+}
+
+void FSMToPromela::writeEventSources(std::ostream& stream) {
+	if (_globalEventSource)
+		writeEventSource(stream, "global", _globalEventSource);
+
+	std::map<std::string, PromelaEventSource>::iterator invIter = _invokers.begin();
+	while(invIter != _invokers.end()) {
+		writeEventSource(stream, invIter->first, invIter->second);
+		invIter++;
+	}
+
+}
+
+void FSMToPromela::writeEventSource(std::ostream& stream, const std::string& name, const PromelaEventSource& source) {
+	stream << "proctype " << name << "EventSource() {" << std::endl;
+	stream << "  " << name << "EventSourceDone = 0;" << std::endl;
+	stream << "  " << name << "NewEvent:" << std::endl;
+	stream << "  " << "if" << std::endl;
+	stream << "  " << ":: " << name << "EventSourceDone -> skip;" << std::endl;
+	stream << "  " << ":: else { " << std::endl;
+	stream << "  " << "  if" << std::endl;
+	stream << "  " << "  :: 1 -> " << "goto " << name << "NewEvent;" << std::endl;
+
+	std::list<std::list<std::string> >::const_iterator seqIter = source.sequences.begin();
+	while(seqIter != source.sequences.end()) {
+		stream << "    " << ":: ";
+		std::list<std::string>::const_iterator evIter = seqIter->begin();
+		while(evIter != seqIter->end()) {
+			TrieNode* node = _eventTrie.getNodeWithPrefix(*evIter);
+			stream << "eQ!" << node->identifier << "; ";
+			evIter++;
+		}
+		stream << "goto " << name << "NewEvent;" << std::endl;
+		seqIter++;
+	}
+	stream << "  " << "  fi" << std::endl;
+	stream << "  " << "}" << std::endl;
+	stream << "  " << "fi" << std::endl;
+	stream << "}" << std::endl;
+}
+
+	
+void FSMToPromela::writeFSM(std::ostream& stream) {
+	NodeSet<std::string> transitions;
+	
+	stream << "proctype step() {" << std::endl;
+	// write initial transition
+	transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", _startState);
+	assert(transitions.size() == 1);
+	stream << "  // transition's executable content" << std::endl;
+	writeExecutableContent(stream, transitions[0], 1);
+
+	for (int i = 0; i < _globalStates.size(); i++) {
+		if (_globalStates[i] == _startState)
+			continue;
+		NodeSet<std::string> transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", _globalStates[i]);
+		for (int j = 0; j < transitions.size(); j++) {
+			writeExecutableContent(stream, transitions[j], 1);
+		}
+	}
+	
+	stream << std::endl;
+	stream << "nextStep: /* pop an event */" << std::endl;
+  stream << "  if" << std::endl;
+	stream << "  :: len(iQ) != 0 -> iQ ? e /* from internal queue */" << std::endl;
+	stream << "  :: else -> eQ ? e         /* from external queue */" << std::endl;
+	stream << "  fi;" << std::endl;
+	stream << "  /* event dispatching per state */" << std::endl;
+	stream << "  if" << std::endl;
+
+	writeEventDispatching(stream);
+	
+	stream << "  :: else -> goto nextStep;" << std::endl;
+  stream << "  fi;" << std::endl;
+  stream << "terminate: skip;" << std::endl;
+	
+	// stop all event sources
+	if (_globalEventSource)
+		stream << "  globalEventSourceDone = 1;" << std::endl;
+	
+	std::map<std::string, PromelaEventSource>::iterator invIter = _invokers.begin();
+	while(invIter != _invokers.end()) {
+		stream << "  " << invIter->first << "EventSourceDone = 1;" << std::endl;
+		invIter++;
+	}
+
+	
+	stream << "}" << std::endl;
+}
+
+void FSMToPromela::writeEventDispatching(std::ostream& stream) {
+	for (int i = 0; i < _globalStates.size(); i++) {
+		if (_globalStates[i] == _startState)
+			continue;
+
+		stream << "  :: (s == s" << i << ") -> {" << std::endl;
 
+		NodeSet<std::string> transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", _globalStates[i]);
+		writeDispatchingBlock(stream, transitions, 2);
+		stream << "    goto nextStep;" << std::endl;
+		stream << "  }" << std::endl;
+	}
 }
 
-FSMToPromela::FSMToPromela(const Arabica::DOM::Document<std::string>& doc,
-													 const std::map<std::string, std::string>& namespaceInfo) {
+void FSMToPromela::writeDispatchingBlock(std::ostream& stream, const Arabica::XPath::NodeSet<std::string>& transChain, int indent) {
+	if (transChain.size() == 0)
+		return;
 		
-	std::map<std::string, std::string>::const_iterator nsIter = namespaceInfo.begin();
-	while(nsIter != namespaceInfo.end()) {
-		std::string uri = nsIter->first;
-		std::string prefix = nsIter->second;
-		if (iequals(uri, "http://www.w3.org/2005/07/scxml")) {
-			_nsURL = uri;
-			if (prefix.size() == 0) {
-				_xpathPrefix = "scxml:";
-				_nsContext.addNamespaceDeclaration(uri, "scxml");
-				_nsToPrefix[uri] = "scxml";
-			} else {
-				_xpathPrefix = prefix + ":";
-				_xmlNSPrefix = _xpathPrefix;
-				_nsContext.addNamespaceDeclaration(uri, prefix);
-				_nsToPrefix[uri] = prefix;
+	std::string padding;
+	for (int i = 0; i < indent; i++) {
+		padding += "  ";
+	}
+	
+	stream << padding << "if" << std::endl;
+	stream << padding << ":: ((0";
+	
+	Node<std::string> currTrans = transChain[0];
+	std::string eventDesc = ATTR(currTrans, "event");
+	if (boost::ends_with(eventDesc, "*"))
+		eventDesc = eventDesc.substr(0, eventDesc.size() - 1);
+	if (boost::ends_with(eventDesc, "."))
+		eventDesc = eventDesc.substr(0, eventDesc.size() - 1);
+
+	if (eventDesc.size() == 0) {
+		stream << " || 1";
+	} else {
+		std::list<TrieNode*> trieNodes = _eventTrie.getWordsWithPrefix(eventDesc);
+		
+		std::list<TrieNode*>::iterator trieIter = trieNodes.begin();
+		while(trieIter != trieNodes.end()) {
+			stream << " || e == e" << (*trieIter)->identifier;
+			trieIter++;
+		}
+	}
+	
+	stream << ") && ";
+	stream << (HAS_ATTR(currTrans, "cond") ? ATTR(currTrans, "cond") : "1");
+	stream << ") -> goto t" << _transitions[currTrans] << ";" << std::endl;
+;
+
+	stream << padding << ":: else {" << std::endl;
+	
+	Arabica::XPath::NodeSet<std::string> cdrTransChain;
+	for (int i = 1; i < transChain.size(); i++) {
+		cdrTransChain.push_back(transChain[i]);
+	}
+	writeDispatchingBlock(stream, cdrTransChain, indent + 1);
+
+	stream << padding << "  goto nextStep;" << std::endl;
+	stream << padding << "}" << std::endl;
+	stream << padding << "fi;" << std::endl;
+}
+
+
+void FSMToPromela::writeMain(std::ostream& stream) {
+	stream << std::endl;
+	stream << "init {" << std::endl;
+	if (_globalEventSource)
+		stream << "  run globalEventSource();" << std::endl;
+	stream << "  run step();" << std::endl;
+	stream << "}" << std::endl;
+
+}
+
+void FSMToPromela::initNodes() {
+	// get all states
+	NodeSet<std::string> states = filterChildElements(_nsInfo.xmlNSPrefix + "state", _scxml);
+	for (int i = 0; i < states.size(); i++) {
+		_states[ATTR(states[i], "id")] = states[i];
+		if (HAS_ATTR(states[i], "transient") && DOMUtils::attributeIsTrue(ATTR(states[i], "transient")))
+			continue;
+		_globalStates.push_back(states[i]);
+	}
+	_startState = _states[ATTR(_scxml, "initial")];
+
+	// initialize event trie with all events that might occur
+	NodeSet<std::string> internalEventNames;
+	internalEventNames.push_back(_xpath.evaluate("//" + _nsInfo.xpathPrefix + "transition", _scxml).asNodeSet());
+	internalEventNames.push_back(_xpath.evaluate("//" + _nsInfo.xpathPrefix + "raise", _scxml).asNodeSet());
+	internalEventNames.push_back(_xpath.evaluate("//" + _nsInfo.xpathPrefix + "send", _scxml).asNodeSet());
+
+	for (int i = 0; i < internalEventNames.size(); i++) {
+		if (HAS_ATTR(internalEventNames[i], "event")) {
+			std::string eventNames = ATTR(internalEventNames[i], "event");
+			std::list<std::string> events = tokenizeIdRefs(eventNames);
+			for (std::list<std::string>::iterator eventIter = events.begin();
+			        eventIter != events.end(); eventIter++) {
+				std::string eventName = *eventIter;
+				if (boost::ends_with(eventName, "*"))
+					eventName = eventName.substr(0, eventName.size() - 1);
+				if (boost::ends_with(eventName, "."))
+					eventName = eventName.substr(0, eventName.size() - 1);
+				_eventTrie.addWord(eventName);
+			}
+		}
+	}
+
+	// external event names from comments
+	NodeSet<std::string> promelaEventSourceComments;
+	NodeSet<std::string> invokers = _xpath.evaluate("//" + _nsInfo.xpathPrefix + "invoke", _scxml).asNodeSet();
+	promelaEventSourceComments.push_back(filterChildType(Node_base::COMMENT_NODE, invokers, true)); // comments in invoke elements
+	promelaEventSourceComments.push_back(filterChildType(Node_base::COMMENT_NODE, _scxml, false)); // comments in scxml element
+
+	for (int i = 0; i < promelaEventSourceComments.size(); i++) {
+		std::string comment = promelaEventSourceComments[i].getNodeValue();
+		boost::trim(comment);
+		if (!boost::starts_with(comment, "promela-event-source:"))
+			continue;
+		PromelaEventSource* eventSource = NULL;
+		if (false) {
+		} else if (TAGNAME(promelaEventSourceComments[i].getParentNode()) == "scxml") {
+			eventSource = &_globalEventSource;
+		} else if (TAGNAME(promelaEventSourceComments[i].getParentNode()) == "invoke") {
+			if (!HAS_ATTR(promelaEventSourceComments[i].getParentNode(), "invokeid")) {
+				Element<std::string> invoker = Element<std::string>(promelaEventSourceComments[i].getParentNode());
+				invoker.setAttribute("invokeid", "invoker" + toStr(_invokers.size()));
 			}
+			std::string invokeId = ATTR(promelaEventSourceComments[i].getParentNode(), "invokeid");
+			eventSource = &_invokers[invokeId];
 		} else {
-			_nsContext.addNamespaceDeclaration(uri, prefix);
-			_nsToPrefix[uri] = prefix;
+			assert(false);
+		}
+		if (!eventSource)
+			continue;
+		std::stringstream ssLine(comment);
+		std::string line;
+		std::getline(ssLine, line); // consume first line
+		while(std::getline(ssLine, line)) {
+			if (line.length() == 0)
+				continue;
+			std::list<std::string> currSeq;
+
+			std::stringstream ssToken(line);
+			std::string token;
+			while(std::getline(ssToken, token, ' ')) {
+				if (token.length() == 0)
+					continue;
+				currSeq.push_back(token);
+				_eventTrie.addWord(token);
+			}
+			eventSource->sequences.push_back(currSeq);
 		}
-		nsIter++;
 	}
-	_xpath.setNamespaceContext(_nsContext);
+	
+	// enumerate transitions
+	NodeSet<std::string> transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", _scxml, true);
+	int index = 0;
+	for (int i = 0; i < transitions.size(); i++) {
+		_transitions[transitions[i]] = index++;
+	}
+}
 
-	_document = doc;
-	NodeList<std::string> scxmls = _document.getElementsByTagNameNS(_nsURL, "scxml");
-	if (scxmls.getLength() > 0) {
-		_scxml = (Arabica::DOM::Element<std::string>)scxmls.item(0);
+void PromelaEventSource::dump() {
+	std::list<std::list<std::string> >::iterator outerIter = sequences.begin();
+	while(outerIter != sequences.end()) {
+		std::list<std::string>::iterator innerIter = outerIter->begin();
+		while(innerIter != outerIter->end()) {
+			std::cout << *innerIter << " ";
+			innerIter++;
+		}
+		std::cout << std::endl;
+		outerIter++;
 	}
 }
 
 void FSMToPromela::writeProgram(std::ostream& stream) {
-	stream << "foo";
+
+	if (!HAS_ATTR(_scxml, "flat") || !DOMUtils::attributeIsTrue(ATTR(_scxml, "flat"))) {
+		LOG(ERROR) << "Given SCXML document was not flattened";
+		return;
+	}
+
+	if (!HAS_ATTR(_scxml, "datamodel") || ATTR(_scxml, "datamodel") != "promela") {
+		LOG(ERROR) << "Can only convert SCXML documents with \"promela\" datamodel";
+		return;
+	}
+
+	if (HAS_ATTR(_scxml, "binding") && ATTR(_scxml, "binding") != "early") {
+		LOG(ERROR) << "Can only convert for early data bindings";
+		return;
+	}
+
+	initNodes();
+
+	writeEvents(stream);
+	stream << std::endl;
+	writeStates(stream);
+	stream << std::endl;
+	writeDeclarations(stream);
+	stream << std::endl;
+	writeEventSources(stream);
+	stream << std::endl;
+	writeFSM(stream);
+	stream << std::endl;
+	writeMain(stream);
+	stream << std::endl;
+
 }
 
 }
\ No newline at end of file
diff --git a/src/uscxml/transform/FSMToPromela.h b/src/uscxml/transform/FSMToPromela.h
index c3324bb..adb0f6a 100644
--- a/src/uscxml/transform/FSMToPromela.h
+++ b/src/uscxml/transform/FSMToPromela.h
@@ -21,37 +21,90 @@
 #define FSMTOPROMELA_H_RP48RFDJ
 
 #include "uscxml/DOMUtils.h"
+#include "uscxml/util/Trie.h"
+
 #include <DOM/Document.hpp>
 #include <DOM/Node.hpp>
 #include <XPath/XPath.hpp>
 #include <ostream>
 
 namespace uscxml {
+
+class PromelaInline {
+public:
+	enum PromelaInlineType {
+		PROMELA_CODE,
+		PROMELA_EVENT_SOURCE,
+		PROMELA_PROGRESS_LABEL,
+		PROMELA_ACCEPT_LABEL,
+		PROMELA_END_LABEL
+	};
 	
-class FSMToPromela {
+	std::string content;
+	PromelaInlineType type;
+};
+
+class PromelaInlines {
+public:
+	PromelaInlines() : hasProgressLabel(false), hasAcceptLabel(false), hasEndLabel(false), hasEventSource(false), hasCode(false) {}
+	
+	std::list<PromelaInline> inlines;
+	bool hasProgressLabel;
+	bool hasAcceptLabel;
+	bool hasEndLabel;
+	bool hasEventSource;
+	bool hasCode;
+};
+
+struct PromelaEventSource {
+	std::list<std::list<std::string> > sequences;
+	void dump();
+	operator bool() {
+		return sequences.size() > 0;
+	}
+};
+
+class FSMToPromela : public InterpreterDraft6 {
 public:
 	static void writeProgram(std::ostream& stream,
-													 const Arabica::DOM::Document<std::string>& doc,
-													 const std::map<std::string, std::string>& namespaceInfo);
+	                         const Interpreter& interpreter);
 protected:
-	FSMToPromela(const Arabica::DOM::Document<std::string>& doc,
-							 const std::map<std::string, std::string>& namespaceInfo);
-	
+	FSMToPromela();
 	void writeProgram(std::ostream& stream);
+
+	void initNodes();
+
+	void writeEvents(std::ostream& stream);
+	void writeStates(std::ostream& stream);
+	void writeDeclarations(std::ostream& stream);
+	void writeEventSources(std::ostream& stream);
+	void writeEventSource(std::ostream& stream, const std::string& name, const PromelaEventSource& source);
+	void writeExecutableContent(std::ostream& stream, const Arabica::DOM::Node<std::string>& node, int indent = 0);
+	void writeInlineComment(std::ostream& stream, const Arabica::DOM::Node<std::string>& node);
+	void writeFSM(std::ostream& stream);
+	void writeEventDispatching(std::ostream& stream);
+	void writeMain(std::ostream& stream);
 	
-	Arabica::DOM::Document<std::string> _document;
-	Arabica::DOM::Node<std::string> _scxml;
 	
-	Arabica::XPath::XPath<std::string> _xpath;
-	Arabica::XPath::StandardNamespaceContext<std::string> _nsContext;
-	std::string _xmlNSPrefix; // the actual prefix for elements in the xml file
-	std::string _xpathPrefix; // prefix mapped for xpath, "scxml" is _xmlNSPrefix is empty but _nsURL set
-	std::string _nsURL;       // ough to be "http://www.w3.org/2005/07/scxml"
-	std::map<std::string, std::string> _nsToPrefix;
-	std::map<std::string, std::string> _nameSpaceInfo;
+	void writeIfBlock(std::ostream& stream, const Arabica::XPath::NodeSet<std::string>& condChain, int indent = 0);
+	void writeDispatchingBlock(std::ostream& stream, const Arabica::XPath::NodeSet<std::string>& transChain, int indent = 0);
 
-};
+	std::string beautifyIndentation(const std::string& code, int indent = 0);
+		
+	Arabica::XPath::NodeSet<std::string> getTransientContent(const Arabica::DOM::Node<std::string>& state);
+	Arabica::DOM::Node<std::string> getUltimateTarget(const Arabica::DOM::Node<std::string>& transition);
+	PromelaInlines getInlinePromela(const Arabica::XPath::NodeSet<std::string>& elements, bool recurse = false);
 	
+	Trie _eventTrie;
+	Arabica::XPath::NodeSet<std::string> _globalStates;
+	Arabica::DOM::Node<std::string> _startState;
+	std::map<std::string, Arabica::DOM::Node<std::string> > _states;
+	std::map<Arabica::DOM::Node<std::string>, int> _transitions;
+
+	std::map<std::string, PromelaEventSource> _invokers;
+	PromelaEventSource _globalEventSource;
+};
+
 }
 
 #endif /* end of include guard: FSMTOPROMELA_H_RP48RFDJ */