SCXML -> Promela skips intermediate explicit flat SCXML for ridiculous better memory footprint

1 files changed, 2146 insertions, 0 deletions

diff --git a/src/uscxml/transform/ChartToPromela.cpp b/src/uscxml/transform/ChartToPromela.cpp
new file mode 100644
index 0000000..1ae6c8d
--- /dev/null
+++ b/src/uscxml/transform/ChartToPromela.cpp
@@ -0,0 +1,2146 @@
+/**
+ *  @file
+ *  @author     2012-2014 Stefan Radomski (stefan.radomski@cs.tu-darmstadt.de)
+ *  @copyright  Simplified BSD
+ *
+ *  @cond
+ *  This program is free software: you can redistribute it and/or modify
+ *  it under the terms of the FreeBSD license as published by the FreeBSD
+ *  project.
+ *
+ *  This program is distributed in the hope that it will be useful,
+ *  but WITHOUT ANY WARRANTY; without even the implied warranty of
+ *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
+ *
+ *  You should have received a copy of the FreeBSD license along with this
+ *  program. If not, see <http://www.opensource.org/licenses/bsd-license>.
+ *  @endcond
+ */
+
+#include "uscxml/transform/ChartToFSM.h"
+#include "uscxml/transform/ChartToPromela.h"
+#include "uscxml/transform/FlatStateIdentifier.h"
+#include "uscxml/plugins/datamodel/promela/PromelaParser.h"
+#include "uscxml/plugins/datamodel/promela/parser/promela.tab.hpp"
+
+#include <DOM/io/Stream.hpp>
+#include <iostream>
+#include "uscxml/UUID.h"
+#include <math.h>
+#include <boost/algorithm/string.hpp>
+#include <glog/logging.h>
+
+#define MSG_QUEUE_LENGTH 5
+#define MAX_MACRO_CHARS 64
+#define MIN_COMMENT_PADDING 60
+
+#define BIT_WIDTH(number) (number > 1 ? (int)ceil(log((double)number) / log((double)2.0)) : 1)
+#define LENGTH_FOR_NUMBER(input, output) \
+{ \
+	int number = input; \
+	int output = 0; \
+	do { \
+		number /= 10; \
+		output++; \
+	} while (number != 0); \
+}
+
+#define INDENT_MIN(stream, start, cols) \
+for (int indentIndex = start; indentIndex < cols; indentIndex++) \
+	stream << " ";
+
+namespace uscxml {
+
+using namespace Arabica::DOM;
+using namespace Arabica::XPath;
+
+Transformer ChartToPromela::transform(const Interpreter& other) {
+	return boost::shared_ptr<TransformerImpl>(new ChartToPromela(other));
+}
+
+void ChartToPromela::writeTo(std::ostream& stream) {
+	writeProgram(stream);
+}
+
+void PromelaEventSource::writeStartEventSources(std::ostream& stream, int indent) {
+	std::string padding;
+	for (int i = 0; i < indent; i++) {
+		padding += "  ";
+	}
+
+	std::list<PromelaInline>::iterator sourceIter = eventSources.inlines.begin();
+	int i = 0;
+	while(sourceIter != eventSources.inlines.end()) {
+		if (sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM && sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE) {
+			sourceIter++;
+			continue;
+		}
+		std::string sourceName = name + "_"+ toStr(i);
+		stream << padding << "run " << sourceName << "EventSource();" << std::endl;
+
+		i++;
+		sourceIter++;
+	}
+
+}
+
+void PromelaEventSource::writeStopEventSources(std::ostream& stream, int indent) {
+	std::string padding;
+	for (int i = 0; i < indent; i++) {
+		padding += "  ";
+	}
+
+	std::list<PromelaInline>::iterator sourceIter = eventSources.inlines.begin();
+	int i = 0;
+	while(sourceIter != eventSources.inlines.end()) {
+		if (sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM && sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE) {
+			sourceIter++;
+			continue;
+		}
+		std::string sourceName = name + "_"+ toStr(i);
+		stream << padding << sourceName << "EventSourceDone = 1;" << std::endl;
+
+		i++;
+		sourceIter++;
+	}
+
+}
+
+void PromelaEventSource::writeDeclarations(std::ostream& stream, int indent) {
+	std::string padding;
+	for (int i = 0; i < indent; i++) {
+		padding += "  ";
+	}
+
+	std::list<PromelaInline>::iterator sourceIter = eventSources.inlines.begin();
+	int i = 0;
+	while(sourceIter != eventSources.inlines.end()) {
+		if (sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM && sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE) {
+			sourceIter++;
+			continue;
+		}
+		std::string sourceName = name + "_"+ toStr(i);
+		stream << "bool " << sourceName << "EventSourceDone = 0;" << std::endl;
+
+		i++;
+		sourceIter++;
+	}
+}
+
+void PromelaEventSource::writeEventSource(std::ostream& stream) {
+
+	std::list<PromelaInline>::iterator sourceIter = eventSources.inlines.begin();
+	int i = 0;
+	while(sourceIter != eventSources.inlines.end()) {
+		if (sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM && sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE) {
+			sourceIter++;
+			continue;
+		}
+
+		std::string sourceName = name + "_"+ toStr(i);
+
+		stream << "proctype " << sourceName << "EventSource() {" << std::endl;
+		stream << "  " << sourceName << "EventSourceDone = 0;" << std::endl;
+		stream << "  " << sourceName << "NewEvent:" << std::endl;
+		stream << "  " << "if" << std::endl;
+		stream << "  " << ":: " << sourceName << "EventSourceDone -> skip;" << std::endl;
+		stream << "  " << ":: else { " << std::endl;
+
+		Trie& trie = analyzer->getTrie();
+
+		if (sourceIter->type == PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM) {
+			std::string content = sourceIter->content;
+
+			boost::replace_all(content, "#REDO#", sourceName + "NewEvent");
+			boost::replace_all(content, "#DONE#", sourceName + "Done");
+
+			std::list<TrieNode*> eventNames = trie.getChildsWithWords(trie.getNodeWithPrefix(""));
+			std::list<TrieNode*>::iterator eventNameIter = eventNames.begin();
+			while(eventNameIter != eventNames.end()) {
+				boost::replace_all(content, "#" + (*eventNameIter)->value + "#", (*eventNameIter)->identifier);
+				eventNameIter++;
+			}
+
+			stream << ChartToPromela::beautifyIndentation(content, 2) << std::endl;
+
+		} else {
+			stream << "  " << "  if" << std::endl;
+//			stream << "  " << "  :: 1 -> " << "goto " << sourceName << "NewEvent;" << std::endl;
+
+			std::list<std::list<std::string> >::const_iterator seqIter = sourceIter->sequences.begin();
+			while(seqIter != sourceIter->sequences.end()) {
+				stream << "    " << ":: ";
+				std::list<std::string>::const_iterator evIter = seqIter->begin();
+				while(evIter != seqIter->end()) {
+					TrieNode* node = trie.getNodeWithPrefix(*evIter);
+					stream << "eQ!" << node->identifier << "; ";
+					evIter++;
+				}
+				stream << "goto " << sourceName << "NewEvent;" << std::endl;
+				seqIter++;
+			}
+
+			stream << "  " << "  fi;" << std::endl;
+		}
+
+		stream << "  " << "}" << std::endl;
+		stream << "  " << "fi;" << std::endl;
+		stream << sourceName << "Done:" << " skip;" << std::endl;
+		stream << "}" << std::endl;
+
+		i++;
+		sourceIter++;
+	}
+}
+
+PromelaEventSource::PromelaEventSource() {
+	type = PROMELA_EVENT_SOURCE_INVALID;
+	analyzer = NULL;
+}
+
+PromelaEventSource::PromelaEventSource(const PromelaInlines& sources, const Arabica::DOM::Node<std::string>& parent) {
+	type = PROMELA_EVENT_SOURCE_INVALID;
+	analyzer = NULL;
+
+	eventSources = sources;
+	container = parent;
+}
+
+void PromelaCodeAnalyzer::addCode(const std::string& code) {
+	PromelaParser parser(code);
+
+	// find all strings
+	std::list<PromelaParserNode*> astNodes;
+	astNodes.push_back(parser.ast);
+
+	while(astNodes.size() > 0) {
+		PromelaParserNode* node = astNodes.front();
+		astNodes.pop_front();
+
+		bool hasValue = false;
+		int assignedValue = 0;
+
+		switch (node->type) {
+		case PML_STRING: {
+			std::string unquoted = node->value;
+			if (boost::starts_with(unquoted, "'")) {
+				unquoted = unquoted.substr(1, unquoted.size() - 2);
+			}
+			addLiteral(unquoted);
+			break;
+		}
+		case PML_ASGN:
+//			node->dump();
+			if (node->operands.back()->type == PML_CONST) {
+				hasValue = true;
+				if (isInteger(node->operands.back()->value.c_str(), 10)) {
+					assignedValue = strTo<int>(node->operands.back()->value);
+				}
+			}
+			if (node->operands.front()->type == PML_CMPND)
+				node = node->operands.front();
+		case PML_CMPND: {
+			std::string nameOfType;
+			std::list<PromelaParserNode*>::iterator opIter = node->operands.begin();
+			if ((*opIter)->type != PML_NAME) {
+				node->dump();
+				assert(false);
+			}
+
+			PromelaTypedef* td = &_typeDefs;
+			std::string seperator;
+
+			while(opIter != node->operands.end()) {
+				switch ((*opIter)->type) {
+				case PML_NAME:
+					td = &td->types[(*opIter)->value];
+					nameOfType += seperator + (*opIter)->value;
+					if (nameOfType.compare("_x") == 0)
+						_usesPlatformVars = true;
+					seperator = "_";
+					td->name = nameOfType + "_t";
+					break;
+				case PML_VAR_ARRAY: {
+					PromelaParserNode* name = (*opIter)->operands.front();
+					PromelaParserNode* subscript = *(++(*opIter)->operands.begin());
+					td = &td->types[name->value];
+					nameOfType += seperator + name->value;
+					td->name = nameOfType + "_t";
+
+					if (isInteger(subscript->value.c_str(), 10)) {
+						td->arraySize = strTo<int>(subscript->value);
+					}
+					break;
+				}
+				default:
+					if ((*opIter)->type == PML_CONST) {
+						// break fall through from ASGN
+						break;
+					}
+					node->dump();
+					assert(false);
+					break;
+				}
+
+				if (nameOfType.compare("_x_states") == 0) {
+					_usesInPredicate = true;
+				}
+				if (nameOfType.compare("_event_type") == 0) {
+					addLiteral("internal");
+					addLiteral("external");
+					addLiteral("platform");
+				}
+				if (nameOfType.compare("_event_origintype") == 0) {
+					addLiteral("http://www.w3.org/TR/scxml/#SCXMLEventProcessor");
+				}
+				opIter++;
+			}
+			
+			if (hasValue) {
+				if (td->maxValue < assignedValue)
+					td->maxValue = assignedValue;
+				if (td->minValue > assignedValue)
+					td->minValue = assignedValue;
+			}
+			
+			continue; // skip processing nested AST nodes
+		}
+		case PML_NAME: {
+			_typeDefs.types[node->value].minValue = 0;
+			_typeDefs.types[node->value].maxValue = 1;
+			break;
+		}
+
+		default:
+//			node->dump();
+			break;
+//				assert(false);
+		}
+
+		astNodes.merge(node->operands);
+	}
+}
+
+void PromelaCodeAnalyzer::addEvent(const std::string& eventName) {
+	if (_events.find(eventName) != _events.end())
+		return;
+
+	addLiteral(eventName, _lastEventIndex);
+	assert(_strIndex.find(eventName) != _strIndex.end());
+
+	_eventTrie.addWord(eventName);
+	_events[eventName] = _strIndex[eventName];
+	_lastEventIndex++;
+}
+
+void PromelaCodeAnalyzer::addOrigState(const std::string& stateName) {
+	if (_origStateIndex.find(stateName) == _origStateIndex.end()) {
+		_origStateIndex[stateName] = _lastStateIndex++;
+		createMacroName(stateName);
+	}
+}
+	
+void PromelaCodeAnalyzer::addState(const std::string& stateName) {
+	if (_states.find(stateName) != _states.end())
+		return;
+
+	createMacroName(stateName);
+
+#if 0
+//	addLiteral(stateName);
+//	_states[stateName] = enumerateLiteral(stateName);
+	if (_origStateMap.find(stateName) == _origStateMap.end()) {
+		FlatStateIdentifier flatId(stateName);
+		_origStateMap[stateName] = flatId.getActive();
+		for (std::list<std::string>::iterator origIter = _origStateMap[stateName].begin(); origIter != _origStateMap[stateName].end(); origIter++) {
+			//addLiteral(*origIter); // add original state names as string literals
+			if (_origStateIndex.find(*origIter) == _origStateIndex.end()) {
+				_origStateIndex[*origIter] = _lastStateIndex++;
+				createMacroName(*origIter);
+			}
+		}
+	}
+#endif
+}
+
+#if 0
+int PromelaCodeAnalyzer::arrayIndexForOrigState(const std::string& stateName) {
+	if (_origStateIndex.find(stateName) == _origStateIndex.end())
+		throw std::runtime_error("No original state " + stateName + " known");
+	return _origStateIndex[stateName];
+}
+#endif
+
+void PromelaCodeAnalyzer::addLiteral(const std::string& literal, int forceIndex) {
+	if (boost::starts_with(literal, "'"))
+		throw std::runtime_error("Literal " + literal + " passed with quotes");
+
+	if (_strLiterals.find(literal) != _strLiterals.end())
+		return;
+
+	_strLiterals.insert(literal);
+	createMacroName(literal);
+	enumerateLiteral(literal, forceIndex);
+}
+
+int PromelaCodeAnalyzer::enumerateLiteral(const std::string& literal, int forceIndex) {
+	if (forceIndex >= 0) {
+		_strIndex[literal] = forceIndex;
+		return forceIndex;
+	}
+
+	if (_strIndex.find(literal) != _strIndex.end())
+		return _strIndex[literal];
+
+	_strIndex[literal] = ++_lastStrIndex;
+	return _lastStrIndex + 1;
+}
+
+std::string PromelaCodeAnalyzer::createMacroName(const std::string& literal) {
+	if (_strMacroNames.find(literal) != _strMacroNames.end())
+		return _strMacroNames[literal];
+
+	// find a suitable macro name for the strings
+	std::string macroName = literal; //literal.substr(1, literal.size() - 2);
+
+	// cannot start with digit
+	if (isInteger(macroName.substr(0,1).c_str(), 10))
+		macroName = "_" + macroName;
+
+	macroName = macroName.substr(0, MAX_MACRO_CHARS);
+	boost::to_upper(macroName);
+
+	std::string illegalChars = "#\\/:?\"<>| \n\t()[]{}',.-";
+	std::string tmp;
+	std::string::iterator it = macroName.begin();
+	while (it < macroName.end()) {
+		bool found = illegalChars.find(*it) != std::string::npos;
+		if(found) {
+			tmp += '_';
+			it++;
+			while(it < macroName.end() && illegalChars.find(*it) != std::string::npos) {
+				it++;
+			}
+		} else {
+			tmp += *it++;
+		}
+	}
+	macroName = tmp;
+
+	unsigned int index = 2;
+	while (_macroNameSet.find(macroName) != _macroNameSet.end()) {
+		std::string suffix = toStr(index);
+		if (macroName.size() > suffix.size()) {
+			macroName = macroName.substr(0, macroName.size() - suffix.size()) + suffix;
+		} else {
+			macroName = suffix;
+		}
+		index++;
+	}
+
+	_macroNameSet.insert(macroName);
+	_strMacroNames[literal] = macroName;
+	return macroName;
+}
+
+std::string PromelaCodeAnalyzer::macroForLiteral(const std::string& literal) {
+	if (boost::starts_with(literal, "'"))
+		throw std::runtime_error("Literal " + literal + " passed with quotes");
+
+	if (_strMacroNames.find(literal) == _strMacroNames.end())
+		throw std::runtime_error("No macro for literal " + literal + " known");
+	return _strMacroNames[literal];
+}
+
+int PromelaCodeAnalyzer::indexForLiteral(const std::string& literal) {
+	if (boost::starts_with(literal, "'"))
+		throw std::runtime_error("Literal " + literal + " passed with quotes");
+
+	if (_strIndex.find(literal) == _strIndex.end())
+		throw std::runtime_error("No index for literal " + literal + " known");
+	return _strIndex[literal];
+}
+
+std::string PromelaCodeAnalyzer::replaceLiterals(const std::string code) {
+	std::string replaced = code;
+	for (std::map<std::string, std::string>::const_iterator litIter = _strMacroNames.begin(); litIter != _strMacroNames.end(); litIter++) {
+		boost::replace_all(replaced, "'" + litIter->first + "'", litIter->second);
+	}
+	return replaced;
+}
+
+std::set<std::string> PromelaCodeAnalyzer::getEventsWithPrefix(const std::string& prefix) {
+	std::set<std::string> eventNames;
+	std::list<TrieNode*> trieNodes = _eventTrie.getWordsWithPrefix(prefix);
+
+	std::list<TrieNode*>::iterator trieIter = trieNodes.begin();
+	while(trieIter != trieNodes.end()) {
+		eventNames.insert((*trieIter)->value);
+		trieIter++;
+	}
+
+	return eventNames;
+}
+
+
+void ChartToPromela::writeEvents(std::ostream& stream) {
+	std::map<std::string, int> events = _analyzer.getEvents();
+	std::map<std::string, int>::iterator eventIter = events.begin();
+	stream << "/* event name identifiers */" << std::endl;
+	while(eventIter != events.end()) {
+		if (eventIter->first.length() > 0) {
+			stream << "#define " << _analyzer.macroForLiteral(eventIter->first) << " " << _analyzer.indexForLiteral(eventIter->first);
+			stream << " /* from \"" << eventIter->first << "\" */" << std::endl;
+		}
+		eventIter++;
+	}
+}
+
+void ChartToPromela::writeStates(std::ostream& stream) {
+	stream << "/* state name identifiers */" << std::endl;
+	
+	std::map<std::string, GlobalState*>::iterator stateIter = _globalConf.begin();
+	while(stateIter != _globalConf.end()) {
+		stream << "#define " << "s" << stateIter->second->index << " " << stateIter->second->index;
+		stream << " /* from \"" << stateIter->first << "\" */" << std::endl;
+		stateIter++;
+	}
+	
+//	for (int i = 0; i < _globalConf.size(); i++) {
+//		stream << "#define " << "s" << i << " " << i;
+//		stream << " /* from \"" << ATTR_CAST(_globalStates[i], "id") << "\" */" << std::endl;
+//	}
+}
+
+void ChartToPromela::writeStateMap(std::ostream& stream) {
+	stream << "/* macros for original state names */" << std::endl;
+	std::map<std::string, int> origStates = _analyzer.getOrigStates();
+	for (std::map<std::string, int>::iterator origIter = origStates.begin(); origIter != origStates.end(); origIter++) {
+		stream << "#define " << _analyzer.macroForLiteral(origIter->first) << " " << origIter->second;
+		stream << " /* from \"" << origIter->first << "\" */" << std::endl;
+	}
+
+//	std::map<std::string, int> states = _analyzer.getStates();
+//	size_t stateIndex = 0;
+//	for (std::map<std::string, int>::iterator stateIter = states.begin(); stateIter != states.end(); stateIter++) {
+//		stream << "_x"
+//		std::list<std::string> origStates = _analyzer.getOrigState(stateIter->first);
+//		size_t origIndex = 0;
+//		for (std::list<std::string>::iterator origIter = origStates.begin(); origIter != origStates.end(); origIter++) {
+//
+//		}
+//	}
+}
+
+void ChartToPromela::writeTypeDefs(std::ostream& stream) {
+	stream << "/* typedefs */" << std::endl;
+	PromelaCodeAnalyzer::PromelaTypedef typeDefs = _analyzer.getTypes();
+	if (typeDefs.types.size() == 0)
+		return;
+
+	std::list<PromelaCodeAnalyzer::PromelaTypedef> individualDefs;
+	std::list<PromelaCodeAnalyzer::PromelaTypedef> currDefs;
+	currDefs.push_back(typeDefs);
+
+	while(currDefs.size() > 0) {
+		if (std::find(individualDefs.begin(), individualDefs.end(), currDefs.front()) == individualDefs.end()) {
+			individualDefs.push_back(currDefs.front());
+			for (std::map<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator typeIter = currDefs.front().types.begin(); typeIter != currDefs.front().types.end(); typeIter++) {
+				currDefs.push_back(typeIter->second);
+			}
+		}
+		currDefs.pop_front();
+	}
+	individualDefs.pop_front();
+
+	for (std::list<PromelaCodeAnalyzer::PromelaTypedef>::reverse_iterator rIter = individualDefs.rbegin(); rIter != individualDefs.rend(); rIter++) {
+		PromelaCodeAnalyzer::PromelaTypedef currDef = *rIter;
+		if (currDef.types.size() == 0 || currDef.name.size() == 0)
+			continue;
+
+		stream << "typedef " << currDef.name << " {" << std::endl;
+		if (currDef.name.compare("_event_t") == 0 && currDef.types.find("name") == currDef.types.end()) { // special treatment for _event
+			stream << "  int name;" << std::endl;
+		}
+		for (std::map<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator tIter = currDef.types.begin(); tIter != currDef.types.end(); tIter++) {
+			if (currDef.name.compare("_x_t") == 0 && tIter->first.compare("states") == 0) {
+				stream << "  bool states[" << _analyzer.getOrigStates().size() << "];" << std::endl;
+				continue;
+			}
+			if (tIter->second.types.size() == 0) {
+				stream << "  " << declForRange(tIter->first, tIter->second.minValue, tIter->second.maxValue, true) << ";" << std::endl; // not further nested
+//				stream << "  int " << tIter->first << ";" << std::endl; // not further nested
+			} else {
+				stream << "  " << tIter->second.name << " " << tIter->first << ";" << std::endl;
+			}
+		}
+		stream << "};" << std::endl << std::endl;
+	}
+
+//	stream << "/* typedef instances */" << std::endl;
+//	PromelaCodeAnalyzer::PromelaTypedef allTypes = _analyzer.getTypes();
+//	std::map<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator typeIter = allTypes.types.begin();
+//	while(typeIter != allTypes.types.end()) {
+//		if (typeIter->second.types.size() > 0) {
+//			// an actual typedef
+//			stream << "hidden " << typeIter->second.name << " " << typeIter->first << ";" << std::endl;
+//		} else {
+//			stream << "hidden " << declForRange(typeIter->first, typeIter->second.minValue, typeIter->second.maxValue) << ";" << std::endl;
+//		}
+//		typeIter++;
+//	}
+
+}
+
+std::string ChartToPromela::declForRange(const std::string& identifier, long minValue, long maxValue, bool nativeOnly) {
+//	return "int " + identifier; // just for testing
+
+	// we know nothing about this type
+	if (minValue == 0 && maxValue == 0)
+		return "int " + identifier;
+
+	if (minValue < 0) {
+		// only short or int for negatives
+		if (minValue < -32769 || maxValue > 32767)
+			return "int " + identifier;
+		return "short " + identifier;
+	}
+	
+	// type is definitely positive
+	if (nativeOnly) {
+		if (maxValue > 32767)
+			return "int " + identifier;
+		if (maxValue > 255)
+			return "short " + identifier;
+		if (maxValue > 1)
+			return "byte " + identifier;
+		return "bool " + identifier;
+	} else {
+		return "unsigned " + identifier + " : " + toStr(BIT_WIDTH(maxValue));
+	}
+}
+
+	
+#if 0
+Arabica::XPath::NodeSet<std::string> ChartToPromela::getTransientContent(const Arabica::DOM::Element<std::string>& state, const std::string& source) {
+	Arabica::XPath::NodeSet<std::string> content;
+	Arabica::DOM::Element<std::string> currState = state;
+	FlatStateIdentifier prevFlatId(source);
+	for (;;) {
+		if (_analyzer.usesInPredicate()) {
+			// insert state assignments into executable content
+
+			std::stringstream stateSetPromela;
+			stateSetPromela << "#promela-inline " << std::endl;
+			FlatStateIdentifier currFlatId(ATTR(currState, "id"));
+			stateSetPromela << "  /* from " << prevFlatId.getFlatActive() << " to " << currFlatId.getFlatActive() << " */" << std::endl;
+
+			// add all that are missing from prevFlatId
+			std::map<std::string, int> allOrigStates = _analyzer.getOrigStates();
+			for (std::map<std::string, int>::iterator allOrigIter = allOrigStates.begin(); allOrigIter != allOrigStates.end(); allOrigIter++) {
+				if (std::find(currFlatId.getActive().begin(), currFlatId.getActive().end(), allOrigIter->first) != currFlatId.getActive().end() &&
+				        std::find(prevFlatId.getActive().begin(), prevFlatId.getActive().end(), allOrigIter->first) == prevFlatId.getActive().end()) {
+					// active now but not previously
+					stateSetPromela << "  _x.states[" << _analyzer.macroForLiteral(allOrigIter->first) << "] = true; " << std::endl;
+				} else if (std::find(currFlatId.getActive().begin(), currFlatId.getActive().end(), allOrigIter->first) == currFlatId.getActive().end() &&
+				           std::find(prevFlatId.getActive().begin(), prevFlatId.getActive().end(), allOrigIter->first) != prevFlatId.getActive().end()) {
+					// previously active but not now
+					stateSetPromela << "  _x.states[" << _analyzer.macroForLiteral(allOrigIter->first) << "] = false; " << std::endl;
+				}
+			}
+			Comment<std::string> comment = _document.createComment(stateSetPromela.str());
+			_document.importNode(comment, true);
+			currState.insertBefore(comment, currState.getFirstChild());
+			prevFlatId = currFlatId;
+		}
+
+		content.push_back(filterChildType(Node_base::COMMENT_NODE, currState));
+		if (_analyzer.usesInPredicate()) assert(content.size() > 0);
+
+		if (!HAS_ATTR(currState, "transient") || !DOMUtils::attributeIsTrue(ATTR(currState, "transient"))) {
+			// breaking here causes final state assignment to be written
+			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_CAST(transitions[0], "target")];
+	}
+	return content;
+}
+#endif
+	
+#if 0
+Node<std::string> ChartToPromela::getUltimateTarget(const Arabica::DOM::Element<std::string>& transition) {
+	if (!HAS_ATTR(transition, "target")) {
+		return transition.getParentNode();
+	}
+
+	Arabica::DOM::Element<std::string> currState = _states[ATTR_CAST(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_CAST(transitions[0], "target")];
+	}
+}
+#endif
+
+void ChartToPromela::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 ChartToPromela::writeTransition(std::ostream& stream, const GlobalTransition* transition, int indent) {
+	std::string padding;
+	for (int i = 0; i < indent; i++) {
+		padding += "  ";
+	}
+
+	stream << "t" << transition->index << ":";
+	int digits = 0;
+	LENGTH_FOR_NUMBER(transition->index, digits);
+	
+	INDENT_MIN(stream, 2 + digits, MIN_COMMENT_PADDING);
+	stream << " /* from state " << transition->source << " */" << std::endl;
+
+	stream << padding << "atomic {" << std::endl;
+	indent++;
+	
+	for (std::list<GlobalTransition::Action>::const_iterator actionIter = transition->actions.begin(); actionIter != transition->actions.end(); actionIter++) {
+		if (actionIter->transition) {
+			// this is executable content from a transition
+			writeExecutableContent(stream, actionIter->transition, indent);
+			continue;
+		}
+		
+		if (actionIter->onExit) {
+			// executable content from an onexit element
+			writeExecutableContent(stream, actionIter->onExit, indent);
+			continue;
+		}
+		
+		if (actionIter->onEntry) {
+			// executable content from an onentry element
+			writeExecutableContent(stream, actionIter->onEntry, indent);
+			continue;
+		}
+		
+		if (actionIter->invoke) {
+			// an invoke element
+			continue;
+		}
+		
+		if (actionIter->uninvoke) {
+			// an invoke element to uninvoke
+			continue;
+		}
+		
+		if (actionIter->exited) {
+			// we left a state
+			if (_analyzer.usesInPredicate()) {
+				stream << padding << "_x.states[" << _analyzer.macroForLiteral(ATTR(actionIter->exited, "id")) << "] = false; " << std::endl;
+			}
+			continue;
+		}
+		
+		if (actionIter->entered) {
+			// we entered a state
+			if (_analyzer.usesInPredicate()) {
+				stream << padding << "_x.states[" << _analyzer.macroForLiteral(ATTR(actionIter->entered, "id")) << "] = true; " << std::endl;
+			}
+			continue;
+		}
+	}
+	
+	GlobalState* newState = _globalConf[transition->destination];
+	assert(newState != NULL);
+	
+	stream << padding << "  s = s" << newState->index << ";";
+	LENGTH_FOR_NUMBER(newState->index, digits);
+	INDENT_MIN(stream, 10 + digits, MIN_COMMENT_PADDING);
+	
+	stream << " /* to state " << transition->destination << " */" << std::endl;
+
+	
+	if (newState->isFinal) {
+		stream << padding << "  goto terminate;";
+		INDENT_MIN(stream, padding.length() + 14, MIN_COMMENT_PADDING);
+		stream << "/* final state */" << std::endl;
+	} else if (transition->isEventless) {
+		stream << padding << "  goto nextTransition;";
+		INDENT_MIN(stream, padding.length() + 19, MIN_COMMENT_PADDING);
+		stream << "/* spontaneous transition, check for more transitions */" << std::endl;
+	} else {
+		stream << padding << "  eventLess = true;" << std::endl;
+		stream << padding << "  goto nextTransition;";
+		INDENT_MIN(stream, padding.length() + 21, MIN_COMMENT_PADDING);
+		stream << "/* ordinary transition, check for spontaneous transitions */" << std::endl;
+	}
+	stream << padding << "}" << std::endl;
+
+}
+	
+void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica::DOM::Node<std::string>& node, int indent) {
+	if (!node)
+		return;
+
+	std::string padding;
+	for (int i = 0; i < indent; i++) {
+		padding += "  ";
+	}
+
+	if (node.getNodeType() == Node_base::COMMENT_NODE) {
+		// we cannot have labels in an atomic block, just process inline promela
+		PromelaInlines promInls = getInlinePromela(boost::trim_copy(node.getNodeValue()));
+		//		TODO!
+		//		if (promInls) {
+		//		stream << padding << "skip;" << std::endl;
+		//		stream << beautifyIndentation(inlinePromela.str(), indent) << std::endl;
+		//		}
+	}
+
+	if (node.getNodeType() == Node_base::TEXT_NODE) {
+		if (boost::trim_copy(node.getNodeValue()).length() > 0)
+			stream << beautifyIndentation(_analyzer.replaceLiterals(node.getNodeValue()), indent) << std::endl;
+	}
+	
+	if (node.getNodeType() != Node_base::ELEMENT_NODE)
+		return; // skip anything not an element
+
+	Arabica::DOM::Element<std::string> nodeElem = Arabica::DOM::Element<std::string>(node);
+
+	if (false) {
+	} else if(TAGNAME(nodeElem) == "onentry" || TAGNAME(nodeElem) == "onexit" || TAGNAME(nodeElem) == "transition") {
+		// descent into childs and write their contents
+		Arabica::DOM::Node<std::string> child = node.getFirstChild();
+		while(child) {
+			writeExecutableContent(stream, child, indent);
+			child = child.getNextSibling();
+		}
+	} else if(TAGNAME(nodeElem) == "script") {
+		NodeSet<std::string> scriptText = filterChildType(Node_base::TEXT_NODE, node, true);
+		for (int i = 0; i < scriptText.size(); i++) {
+			stream << _analyzer.replaceLiterals(beautifyIndentation(scriptText[i].getNodeValue(), indent)) << std::endl;
+		}
+		
+	} else if(TAGNAME(nodeElem) == "log") {
+		std::string label = (HAS_ATTR(nodeElem, "label") ? ATTR(nodeElem, "label") : "");
+		std::string expr = (HAS_ATTR(nodeElem, "expr") ? ATTR(nodeElem, "expr") : "");
+		std::string trimmedExpr = boost::trim_copy(expr);
+		bool isStringLiteral = (boost::starts_with(trimmedExpr, "\"") || boost::starts_with(trimmedExpr, "'"));
+		
+		std::string formatString;
+		std::string varString;
+		std::string seperator;
+		
+		if (label.size() > 0) {
+			formatString += label + ": ";
+		}
+		
+		if (isStringLiteral) {
+			formatString += expr;
+		} else {
+			formatString += "%d";
+			varString += seperator + expr;
+		}
+		
+		if (varString.length() > 0) {
+			stream << padding << "printf(\"" + formatString + "\", " + varString + ");" << std::endl;
+		} else {
+			stream << padding << "printf(\"" + formatString + "\");" << std::endl;
+		}
+		
+	} else if(TAGNAME(nodeElem) == "foreach") {
+		stream << padding << "for (" << (HAS_ATTR(nodeElem, "index") ? ATTR(nodeElem, "index") : "_index") << " in " << ATTR(nodeElem, "array") << ") {" << std::endl;
+		if (HAS_ATTR(nodeElem, "item")) {
+			stream << padding << "  " << ATTR(nodeElem, "item") << " = " << ATTR(nodeElem, "array") << "[" << (HAS_ATTR(nodeElem, "index") ? ATTR(nodeElem, "index") : "_index") << "];" << std::endl;
+		}
+		Arabica::DOM::Node<std::string> child = node.getFirstChild();
+		while(child) {
+			writeExecutableContent(stream, child, indent + 1);
+			child = child.getNextSibling();
+		}
+		if (HAS_ATTR(nodeElem, "index"))
+			stream << padding << "  " << ATTR(nodeElem, "index") << "++;" << std::endl;
+		stream << padding << "}" << std::endl;
+		
+	} else if(TAGNAME(nodeElem) == "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(nodeElem) == "assign") {
+		if (HAS_ATTR(nodeElem, "location")) {
+			stream << padding << ATTR(nodeElem, "location") << " = ";
+		}
+		if (HAS_ATTR(nodeElem, "expr")) {
+			stream << _analyzer.replaceLiterals(ATTR(nodeElem, "expr")) << ";" << std::endl;
+		} else {
+			NodeSet<std::string> assignTexts = filterChildType(Node_base::TEXT_NODE, nodeElem, true);
+			if (assignTexts.size() > 0) {
+				stream << _analyzer.replaceLiterals(boost::trim_copy(assignTexts[0].getNodeValue())) << ";" << std::endl;
+			}
+		}
+	} else if(TAGNAME(nodeElem) == "send" || TAGNAME(nodeElem) == "raise") {
+		std::string targetQueue;
+		if (TAGNAME(nodeElem) == "raise") {
+			targetQueue = "iQ!";
+		} else if (!HAS_ATTR(nodeElem, "target")) {
+			targetQueue = "tmpQ!";
+		} else if (ATTR(nodeElem, "target").compare("#_internal") == 0) {
+			targetQueue = "iQ!";
+		}
+		if (targetQueue.length() > 0) {
+			// this is for our external queue
+			std::string event;
+			
+			if (HAS_ATTR(nodeElem, "event")) {
+				event = _analyzer.macroForLiteral(ATTR(nodeElem, "event"));
+			} else if (HAS_ATTR(nodeElem, "eventexpr")) {
+				event = ATTR(nodeElem, "eventexpr");
+			}
+			if (_analyzer.usesComplexEventStruct()) {
+				stream << padding << "{" << std::endl;
+				stream << padding << "  _event_t tmpEvent;" << std::endl;
+				stream << padding << "  tmpEvent.name = " << event << ";" << std::endl;
+				
+				if (HAS_ATTR(nodeElem, "idlocation")) {
+					stream << padding << "  /* idlocation */" << std::endl;
+					stream << padding << "  _lastSendId = _lastSendId + 1;" << std::endl;
+					stream << padding << "  " << ATTR(nodeElem, "idlocation") << " = _lastSendId;" << std::endl;
+					stream << padding << "  tmpEvent.sendid = _lastSendId;" << std::endl;
+					stream << padding << "  if" << std::endl;
+					stream << padding << "  :: _lastSendId == 2147483647 -> _lastSendId = 0;" << std::endl;
+					stream << padding << "  :: timeout -> skip;" << std::endl;
+					stream << padding << "  fi;" << std::endl;
+				} else if (HAS_ATTR(nodeElem, "id")) {
+					stream << padding << "  tmpEvent.sendid = " << _analyzer.macroForLiteral(ATTR(nodeElem, "id")) << ";" << std::endl;
+				}
+				
+				if (_analyzer.usesEventField("origintype") && targetQueue.compare("iQ!") != 0) {
+					stream << padding << "  tmpEvent.origintype = " << _analyzer.macroForLiteral("http://www.w3.org/TR/scxml/#SCXMLEventProcessor") << ";" << std::endl;
+				}
+				
+				if (_analyzer.usesEventField("type")) {
+					std::string eventType = (targetQueue.compare("iQ!") == 0 ? _analyzer.macroForLiteral("internal") : _analyzer.macroForLiteral("external"));
+					stream << padding << "  tmpEvent.type = " << eventType << ";" << std::endl;
+				}
+				
+				NodeSet<std::string> sendParams = filterChildElements(_nsInfo.xmlNSPrefix + "param", nodeElem);
+				NodeSet<std::string> sendContents = filterChildElements(_nsInfo.xmlNSPrefix + "content", nodeElem);
+				std::string sendNameList = ATTR(nodeElem, "namelist");
+				if (sendParams.size() > 0) {
+					for (int i = 0; i < sendParams.size(); i++) {
+						Element<std::string> paramElem = Element<std::string>(sendParams[i]);
+						stream << padding << "  tmpEvent.data." << ATTR(paramElem, "name") << " = " << ATTR(paramElem, "expr")  << ";" << std::endl;
+					}
+				}
+				if (sendNameList.size() > 0) {
+					std::list<std::string> nameListIds = tokenizeIdRefs(sendNameList);
+					std::list<std::string>::iterator nameIter = nameListIds.begin();
+					while(nameIter != nameListIds.end()) {
+						stream << padding << "  tmpEvent.data." << *nameIter << " = " << *nameIter << ";" << std::endl;
+						nameIter++;
+					}
+				}
+				
+				if (sendParams.size() == 0 && sendNameList.size() == 0 && sendContents.size() > 0) {
+					Element<std::string> contentElem = Element<std::string>(sendContents[0]);
+					if (contentElem.hasChildNodes() && contentElem.getFirstChild().getNodeType() == Node_base::TEXT_NODE) {
+						stream << padding << "  tmpEvent.data = " << spaceNormalize(contentElem.getFirstChild().getNodeValue()) << ";" << std::endl;
+					} else if (HAS_ATTR(contentElem, "expr")) {
+						stream << padding << "  tmpEvent.data = " << _analyzer.replaceLiterals(ATTR(contentElem, "expr")) << ";" << std::endl;
+					}
+				}
+				stream << padding << "  " << targetQueue << "tmpEvent;" << std::endl;
+				stream << padding << "}" << std::endl;
+			} else {
+				stream << padding << targetQueue << event << ";" << std::endl;
+			}
+		}
+	} else if(TAGNAME(nodeElem) == "invoke") {
+		_invokers[ATTR(nodeElem, "invokeid")].writeStartEventSources(stream, indent);
+	} else if(TAGNAME(nodeElem) == "uninvoke") {
+		stream << padding << ATTR(nodeElem, "invokeid") << "EventSourceDone" << "= 1;" << std::endl;
+	} else if(TAGNAME(nodeElem) == "cancel") {
+		// noop
+	} else {
+		std::cerr << "'" << TAGNAME(nodeElem) << "'" << std::endl << nodeElem << std::endl;
+		assert(false);
+	}
+}
+
+#if 0
+void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica::DOM::Node<std::string>& node, int indent) {
+
+//	std::cout << std::endl << node << std::endl;
+	if (!node)
+		return;
+
+	std::string padding;
+	for (int i = 0; i < indent; i++) {
+		padding += "  ";
+	}
+
+//	std::cerr << node << std::endl;
+
+	if (node.getNodeType() == Node_base::COMMENT_NODE) {
+		// we cannot have labels in an atomic block, just process inline promela
+		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;
+
+	Arabica::DOM::Element<std::string> nodeElem = Arabica::DOM::Element<std::string>(node);
+
+	if (false) {
+//	} else if(TAGNAME(nodeElem) == "state") {
+//		if (HAS_ATTR(nodeElem, "transient") && DOMUtils::attributeIsTrue(ATTR(nodeElem, "transient"))) {
+//			Arabica::XPath::NodeSet<std::string> execContent = getTransientContent(nodeElem);
+//			for (int i = 0; i < execContent.size(); i++) {
+//				writeExecutableContent(stream, execContent[i], indent);
+//			}
+//		}
+	} else if(TAGNAME(nodeElem) == "transition") {
+		stream << "t" << _transitions[nodeElem] << ":";
+
+		int number = _transitions[nodeElem];
+		int digits = 0;
+		do {
+			number /= 10;
+			digits++;
+		} while (number != 0);
+
+		INDENT_MIN(stream, 2 + digits, MIN_COMMENT_PADDING);
+
+		Node<std::string> source = node.getParentNode();
+		stream << " /* from state " << ATTR_CAST(source, "id") << " */" << std::endl;
+
+		// gather all executable content
+		NodeSet<std::string> execContent = getTransientContent(_states[ATTR(nodeElem, "target")], ATTR_CAST(source, "id"));
+
+		// check for special promela labels
+		if (HAS_ATTR(nodeElem, "target")) {
+			PromelaInlines promInls = getInlinePromela(execContent, true);
+
+			if (promInls.acceptLabels > 0)
+				stream << padding << "acceptLabelT" << _transitions[nodeElem] << ":" << std::endl;
+			if (promInls.endLabels > 0)
+				stream << padding << "endLabelT" << _transitions[nodeElem] << ":" << std::endl;
+			if (promInls.progressLabels > 0)
+				stream << padding << "progressLabelT" << _transitions[nodeElem] << ":" << std::endl;
+		}
+
+		stream << padding << "atomic {" << std::endl;
+//		writeExecutableContent(stream, _states[ATTR(nodeElem, "target")], indent+1);
+		for (int i = 0; i < execContent.size(); i++) {
+			writeExecutableContent(stream, execContent[i], indent+1);
+		}
+		stream << padding << "  skip;" << std::endl;
+
+		Node<std::string> newState = getUltimateTarget(nodeElem);
+		for (int i = 0; i < _globalStates.size(); i++) {
+			if (newState != _globalStates[i])
+				continue;
+
+			std::string stateId = ATTR_CAST(_globalStates[i], "id");
+
+			stream << padding << "  s = s" << i << ";";
+
+			int number = i;
+			int digits = 0;
+			do {
+				number /= 10;
+				digits++;
+			} while (number != 0);
+
+			INDENT_MIN(stream, 10 + digits, MIN_COMMENT_PADDING);
+
+			stream << " /* to state " << stateId << " */" << std::endl;
+
+//			if (_analyzer.usesInPredicate()) {
+//				FlatStateIdentifier flatId(stateId);
+//				std::map<std::string, int> allOrigStates = _analyzer.getOrigStates();
+//				for (std::map<std::string, int>::iterator allOrigIter = allOrigStates.begin(); allOrigIter != allOrigStates.end(); allOrigIter++) {
+//					stream << padding << "  _x.states[" << _analyzer.macroForLiteral(allOrigIter->first) << "] = ";
+//					if (std::find(flatId.getActive().begin(), flatId.getActive().end(), allOrigIter->first) != flatId.getActive().end()) {
+//						stream << "true;" << std::endl;
+//					} else {
+//						stream << "false;" << std::endl;
+//					}
+//				}
+//			}
+
+		}
+
+		stream << padding << "}" << std::endl;
+		if (isFinal(Element<std::string>(newState))) {
+			stream << padding << "goto terminate;";
+			INDENT_MIN(stream, padding.length() + 14, MIN_COMMENT_PADDING);
+			stream << "/* final state */" << std::endl;
+		} else if (!HAS_ATTR_CAST(node, "event")) {
+			stream << padding << "goto nextTransition;";
+			INDENT_MIN(stream, padding.length() + 19, MIN_COMMENT_PADDING);
+			stream << "/* spontaneous transition, check for more transitions */" << std::endl;
+		} else {
+			stream << padding << "eventLess = true;" << std::endl;
+			stream << padding << "goto nextTransition;";
+			INDENT_MIN(stream, padding.length() + 21, MIN_COMMENT_PADDING);
+			stream << "/* ordinary transition, check for spontaneous transitions */" << std::endl;
+		}
+
+	} else if(TAGNAME(nodeElem) == "onentry" || TAGNAME(nodeElem) == "onexit") {
+		Arabica::DOM::Node<std::string> child = node.getFirstChild();
+		while(child) {
+//			std::cerr << node << std::endl;
+			if (child.getNodeType() == Node_base::TEXT_NODE) {
+				if (boost::trim_copy(child.getNodeValue()).length() > 0)
+					stream << beautifyIndentation(_analyzer.replaceLiterals(child.getNodeValue()), indent) << std::endl;
+			}
+			if (child.getNodeType() == Node_base::ELEMENT_NODE) {
+				writeExecutableContent(stream, child, indent);
+			}
+			child = child.getNextSibling();
+		}
+
+	} else if(TAGNAME(nodeElem) == "script") {
+		NodeSet<std::string> scriptText = filterChildType(Node_base::TEXT_NODE, node, true);
+		for (int i = 0; i < scriptText.size(); i++) {
+			stream << _analyzer.replaceLiterals(beautifyIndentation(scriptText[i].getNodeValue(), indent)) << std::endl;
+		}
+
+	} else if(TAGNAME(nodeElem) == "log") {
+		std::string label = (HAS_ATTR(nodeElem, "label") ? ATTR(nodeElem, "label") : "");
+		std::string expr = (HAS_ATTR(nodeElem, "expr") ? ATTR(nodeElem, "expr") : "");
+		std::string trimmedExpr = boost::trim_copy(expr);
+		bool isStringLiteral = (boost::starts_with(trimmedExpr, "\"") || boost::starts_with(trimmedExpr, "'"));
+
+		std::string formatString;
+		std::string varString;
+		std::string seperator;
+
+		if (label.size() > 0) {
+			formatString += label + ": ";
+		}
+
+		if (isStringLiteral) {
+			formatString += expr;
+		} else {
+			formatString += "%d";
+			varString += seperator + expr;
+		}
+
+		if (varString.length() > 0) {
+			stream << padding << "printf(\"" + formatString + "\", " + varString + ");" << std::endl;
+		} else {
+			stream << padding << "printf(\"" + formatString + "\");" << std::endl;
+		}
+
+	} else if(TAGNAME(nodeElem) == "foreach") {
+		stream << padding << "for (" << (HAS_ATTR(nodeElem, "index") ? ATTR(nodeElem, "index") : "_index") << " in " << ATTR(nodeElem, "array") << ") {" << std::endl;
+		if (HAS_ATTR(nodeElem, "item")) {
+			stream << padding << "  " << ATTR(nodeElem, "item") << " = " << ATTR(nodeElem, "array") << "[" << (HAS_ATTR(nodeElem, "index") ? ATTR(nodeElem, "index") : "_index") << "];" << std::endl;
+		}
+		Arabica::DOM::Node<std::string> child = node.getFirstChild();
+		while(child) {
+			writeExecutableContent(stream, child, indent + 1);
+			child = child.getNextSibling();
+		}
+		if (HAS_ATTR(nodeElem, "index"))
+			stream << padding << "  " << ATTR(nodeElem, "index") << "++;" << std::endl;
+		stream << padding << "}" << std::endl;
+
+	} else if(TAGNAME(nodeElem) == "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(nodeElem) == "assign") {
+		if (HAS_ATTR(nodeElem, "location")) {
+			stream << padding << ATTR(nodeElem, "location") << " = ";
+		}
+		if (HAS_ATTR(nodeElem, "expr")) {
+			stream << _analyzer.replaceLiterals(ATTR(nodeElem, "expr")) << ";" << std::endl;
+		} else {
+			NodeSet<std::string> assignTexts = filterChildType(Node_base::TEXT_NODE, nodeElem, true);
+			if (assignTexts.size() > 0) {
+				stream << _analyzer.replaceLiterals(boost::trim_copy(assignTexts[0].getNodeValue())) << ";" << std::endl;
+			}
+		}
+	} else if(TAGNAME(nodeElem) == "send" || TAGNAME(nodeElem) == "raise") {
+		std::string targetQueue;
+		if (TAGNAME(nodeElem) == "raise") {
+			targetQueue = "iQ!";
+		} else if (!HAS_ATTR(nodeElem, "target")) {
+			targetQueue = "tmpQ!";
+		} else if (ATTR(nodeElem, "target").compare("#_internal") == 0) {
+			targetQueue = "iQ!";
+		}
+		if (targetQueue.length() > 0) {
+			// this is for our external queue
+			std::string event;
+
+			if (HAS_ATTR(nodeElem, "event")) {
+				event = _analyzer.macroForLiteral(ATTR(nodeElem, "event"));
+			} else if (HAS_ATTR(nodeElem, "eventexpr")) {
+				event = ATTR(nodeElem, "eventexpr");
+			}
+			if (_analyzer.usesComplexEventStruct()) {
+				stream << padding << "{" << std::endl;
+				stream << padding << "  _event_t tmpEvent;" << std::endl;
+				stream << padding << "  tmpEvent.name = " << event << ";" << std::endl;
+
+				if (HAS_ATTR(nodeElem, "idlocation")) {
+					stream << padding << "  /* idlocation */" << std::endl;
+					stream << padding << "  _lastSendId = _lastSendId + 1;" << std::endl;
+					stream << padding << "  " << ATTR(nodeElem, "idlocation") << " = _lastSendId;" << std::endl;
+					stream << padding << "  tmpEvent.sendid = _lastSendId;" << std::endl;
+					stream << padding << "  if" << std::endl;
+					stream << padding << "  :: _lastSendId == 2147483647 -> _lastSendId = 0;" << std::endl;
+					stream << padding << "  :: timeout -> skip;" << std::endl;
+					stream << padding << "  fi;" << std::endl;
+				} else if (HAS_ATTR(nodeElem, "id")) {
+					stream << padding << "  tmpEvent.sendid = " << _analyzer.macroForLiteral(ATTR(nodeElem, "id")) << ";" << std::endl;
+				}
+
+				if (_analyzer.usesEventField("origintype") && targetQueue.compare("iQ!") != 0) {
+					stream << padding << "  tmpEvent.origintype = " << _analyzer.macroForLiteral("http://www.w3.org/TR/scxml/#SCXMLEventProcessor") << ";" << std::endl;
+				}
+
+				if (_analyzer.usesEventField("type")) {
+					std::string eventType = (targetQueue.compare("iQ!") == 0 ? _analyzer.macroForLiteral("internal") : _analyzer.macroForLiteral("external"));
+					stream << padding << "  tmpEvent.type = " << eventType << ";" << std::endl;
+				}
+
+				NodeSet<std::string> sendParams = filterChildElements(_nsInfo.xmlNSPrefix + "param", nodeElem);
+				NodeSet<std::string> sendContents = filterChildElements(_nsInfo.xmlNSPrefix + "content", nodeElem);
+				std::string sendNameList = ATTR(nodeElem, "namelist");
+				if (sendParams.size() > 0) {
+					for (int i = 0; i < sendParams.size(); i++) {
+						Element<std::string> paramElem = Element<std::string>(sendParams[i]);
+						stream << padding << "  tmpEvent.data." << ATTR(paramElem, "name") << " = " << ATTR(paramElem, "expr")  << ";" << std::endl;
+					}
+				}
+				if (sendNameList.size() > 0) {
+					std::list<std::string> nameListIds = tokenizeIdRefs(sendNameList);
+					std::list<std::string>::iterator nameIter = nameListIds.begin();
+					while(nameIter != nameListIds.end()) {
+						stream << padding << "  tmpEvent.data." << *nameIter << " = " << *nameIter << ";" << std::endl;
+						nameIter++;
+					}
+				}
+
+				if (sendParams.size() == 0 && sendNameList.size() == 0 && sendContents.size() > 0) {
+					Element<std::string> contentElem = Element<std::string>(sendContents[0]);
+					if (contentElem.hasChildNodes() && contentElem.getFirstChild().getNodeType() == Node_base::TEXT_NODE) {
+						stream << padding << "  tmpEvent.data = " << spaceNormalize(contentElem.getFirstChild().getNodeValue()) << ";" << std::endl;
+					} else if (HAS_ATTR(contentElem, "expr")) {
+						stream << padding << "  tmpEvent.data = " << _analyzer.replaceLiterals(ATTR(contentElem, "expr")) << ";" << std::endl;
+					}
+				}
+				stream << padding << "  " << targetQueue << "tmpEvent;" << std::endl;
+				stream << padding << "}" << std::endl;
+			} else {
+				stream << padding << targetQueue << event << ";" << std::endl;
+			}
+		}
+	} else if(TAGNAME(nodeElem) == "invoke") {
+		_invokers[ATTR(nodeElem, "invokeid")].writeStartEventSources(stream, indent);
+	} else if(TAGNAME(nodeElem) == "uninvoke") {
+		stream << padding << ATTR(nodeElem, "invokeid") << "EventSourceDone" << "= 1;" << std::endl;
+	} else if(TAGNAME(nodeElem) == "cancel") {
+		// noop
+	} else {
+
+		std::cerr << "'" << TAGNAME(nodeElem) << "'" << std::endl << nodeElem << std::endl;
+		assert(false);
+	}
+
+}
+#endif
+	
+PromelaInlines ChartToPromela::getInlinePromela(const std::string& content) {
+	PromelaInlines prom;
+
+	std::stringstream ssLine(content);
+	std::string line;
+
+	bool isInPromelaCode = false;
+	bool isInPromelaEventSource = false;
+	PromelaInline promInl;
+
+	while(std::getline(ssLine, line)) {
+		std::string trimLine = boost::trim_copy(line);
+		if (trimLine.length() == 0)
+			continue;
+		if (boost::starts_with(trimLine, "#promela")) {
+			if (isInPromelaCode || isInPromelaEventSource) {
+				prom.inlines.push_back(promInl);
+				isInPromelaCode = false;
+				isInPromelaEventSource = false;
+			}
+			promInl = PromelaInline();
+		}
+
+		if (false) {
+		} else if (boost::starts_with(trimLine, "#promela-progress")) {
+			prom.progressLabels++;
+			promInl.type = PromelaInline::PROMELA_PROGRESS_LABEL;
+			promInl.content = line;
+			prom.inlines.push_back(promInl);
+		} else if (boost::starts_with(trimLine, "#promela-accept")) {
+			prom.acceptLabels++;
+			promInl.type = PromelaInline::PROMELA_ACCEPT_LABEL;
+			promInl.content = line;
+			prom.inlines.push_back(promInl);
+		} else if (boost::starts_with(trimLine, "#promela-end")) {
+			prom.endLabels++;
+			promInl.type = PromelaInline::PROMELA_END_LABEL;
+			promInl.content = line;
+			prom.inlines.push_back(promInl);
+		} else if (boost::starts_with(trimLine, "#promela-inline")) {
+			prom.codes++;
+			isInPromelaCode = true;
+			promInl.type = PromelaInline::PROMELA_CODE;
+		} else if (boost::starts_with(trimLine, "#promela-event-source-custom")) {
+			prom.customEventSources++;
+			isInPromelaCode = true;
+			promInl.type = PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM;
+		} else if (boost::starts_with(trimLine, "#promela-event-source")) {
+			prom.eventSources++;
+			isInPromelaEventSource = true;
+			promInl.type = PromelaInline::PROMELA_EVENT_SOURCE;
+		} else if (isInPromelaCode) {
+			promInl.content += line;
+			promInl.content += "\n";
+		} else if (isInPromelaEventSource) {
+			std::list<std::string> seq;
+			std::stringstream ssToken(trimLine);
+			std::string token;
+			while(std::getline(ssToken, token, ' ')) {
+				if (token.length() == 0)
+					continue;
+				seq.push_back(token);
+			}
+			promInl.sequences.push_back(seq);
+		}
+	}
+	// inline code ends with comment
+	if (isInPromelaCode || isInPromelaEventSource) {
+		prom.inlines.push_back(promInl);
+	}
+
+	return prom;
+}
+
+PromelaInlines ChartToPromela::getInlinePromela(const Arabica::DOM::Node<std::string>& node) {
+	if (node.getNodeType() != Node_base::COMMENT_NODE)
+		return getInlinePromela(std::string());
+	return getInlinePromela(node.getNodeValue());
+}
+
+PromelaInlines ChartToPromela::getInlinePromela(const Arabica::XPath::NodeSet<std::string>& elements, bool recurse) {
+	PromelaInlines allPromInls;
+
+	Arabica::XPath::NodeSet<std::string> comments = filterChildType(Node_base::COMMENT_NODE, elements, recurse);
+	for (int i = 0; i < comments.size(); i++) {
+		allPromInls.merge(getInlinePromela(comments[i]));
+	}
+	return allPromInls;
+}
+
+void ChartToPromela::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_CAST(condChain[1]) == "else") {
+			nextIsElse = true;
+		}
+	}
+
+	Element<std::string> ifNode = Element<std::string>(condChain[0]);
+
+	stream << padding << "if" << std::endl;
+	// we need to nest the elseifs to resolve promela if semantics
+	stream << padding << ":: (" << _analyzer.replaceLiterals(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) {
+			Arabica::DOM::Element<std::string> childElem = Arabica::DOM::Element<std::string>(child);
+			if (TAGNAME(childElem) == "elseif" || TAGNAME_CAST(childElem) == "else")
+				break;
+			writeExecutableContent(stream, childElem, indent + 1);
+		}
+		child = child.getNextSibling();
+	}
+	stream << padding << "}" << std::endl;
+	stream << padding << ":: else -> ";
+
+	if (nextIsElse) {
+		child = condChain[1].getNextSibling();
+		stream << "{" << std::endl;
+		while(child) {
+			if (child.getNodeType() == Node_base::ELEMENT_NODE) {
+				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 ChartToPromela::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 ChartToPromela::writeStrings(std::ostream& stream) {
+	stream << "/* string literals */" << std::endl;
+	std::set<std::string> literals = _analyzer.getLiterals();
+	std::map<std::string, int> events = _analyzer.getEvents();
+	std::map<std::string, int> origStates = _analyzer.getOrigStates();
+
+	for (std::set<std::string>::const_iterator litIter = literals.begin(); litIter != literals.end(); litIter++) {
+		if (events.find(*litIter) == events.end() && (origStates.find(*litIter) == origStates.end() || !_analyzer.usesInPredicate()))
+			stream << "#define " << _analyzer.macroForLiteral(*litIter) << " " << _analyzer.indexForLiteral(*litIter) << " /* " << *litIter << " */" << std::endl;
+	}
+}
+
+void ChartToPromela::writeDeclarations(std::ostream& stream) {
+
+	stream << "/* global variables */" << std::endl;
+
+	if (_analyzer.usesComplexEventStruct()) {
+		// event is defined with the typedefs
+		stream << "_event_t _event;            /* current state */" << std::endl;
+		stream << "unsigned s : " << BIT_WIDTH(_globalConf.size() + 1) << ";            /* current state */" << std::endl;
+		stream << "chan iQ   = [" << MSG_QUEUE_LENGTH << "] of {_event_t}  /* internal queue */" << std::endl;
+		stream << "chan eQ   = [" << MSG_QUEUE_LENGTH << "] of {_event_t}  /* external queue */" << std::endl;
+		stream << "chan tmpQ = [" << MSG_QUEUE_LENGTH << "] of {_event_t}  /* temporary queue for external events in transitions */" << std::endl;
+		stream << "hidden _event_t tmpQItem;" << std::endl;
+	} else {
+		stream << "unsigned _event : " << BIT_WIDTH(_analyzer.getEvents().size() + 1) << ";                /* current event */" << std::endl;
+		stream << "unsigned s : " << BIT_WIDTH(_globalConf.size() + 1) << ";            /* current state */" << std::endl;
+		stream << "chan iQ   = [" << MSG_QUEUE_LENGTH << "] of {int}  /* internal queue */" << std::endl;
+		stream << "chan eQ   = [" << MSG_QUEUE_LENGTH << "] of {int}  /* external queue */" << std::endl;
+		stream << "chan tmpQ = [" << MSG_QUEUE_LENGTH << "] of {int}  /* temporary queue for external events in transitions */" << std::endl;
+		stream << "hidden unsigned tmpQItem : " << BIT_WIDTH(_analyzer.getEvents().size() + 1) << ";" << std::endl;
+	}
+	stream << "bool eventLess = true;       /* whether to process event-less only n this step */" << std::endl;
+	stream << "hidden int _index;                  /* helper for indexless foreach loops */" << std::endl;
+
+	if (_analyzer.getTypes().types.find("_ioprocessors") != _analyzer.getTypes().types.end()) {
+		stream << "hidden _ioprocessors_t _ioprocessors;" << std::endl;
+	}
+	
+	if (_analyzer.usesEventField("sendid")) {
+		stream << "hidden int _lastSendId = 0;         /* sequential counter for send ids */";
+	}
+
+//	if (_analyzer.usesPlatformVars()) {
+//		stream << "_x_t _x;" << std::endl;
+//	}
+
+	stream << std::endl;
+
+	// 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;
+	std::set<std::string> processedIdentifiers;
+	for (int i = 0; i < datas.size(); i++) {
+		
+		Node<std::string> data = datas[i];
+		if (isInEmbeddedDocument(data))
+			continue;
+		
+		std::string identifier = (HAS_ATTR_CAST(data, "id") ? ATTR_CAST(data, "id") : "");
+		std::string expression = (HAS_ATTR_CAST(data, "expr") ? ATTR_CAST(data, "expr") : "");
+		std::string type = boost::trim_copy(HAS_ATTR_CAST(data, "type") ? ATTR_CAST(data, "type") : "");
+		
+		if (processedIdentifiers.find(identifier) != processedIdentifiers.end())
+			continue;
+		processedIdentifiers.insert(identifier);
+		
+		if (boost::starts_with(type, "string")) {
+			type = "int" + type.substr(6, type.length() - 6);
+		}
+		std::string arrSize;
+		
+		NodeSet<std::string> dataText = filterChildType(Node_base::TEXT_NODE, data, true);
+		std::string value;
+		if (dataText.size() > 0) {
+			value = dataText[0].getNodeValue();
+			boost::trim(value);
+		}
+		
+		if (identifier.length() > 0) {
+			
+			size_t bracketPos = type.find("[");
+			if (bracketPos != std::string::npos) {
+				arrSize = type.substr(bracketPos, type.length() - bracketPos);
+				type = type.substr(0, bracketPos);
+			}
+			std::string decl = type + " " + identifier + arrSize;
+			
+			if (arrSize.length() > 0) {
+				stream << decl << ";" << std::endl;
+				_varInitializers.push_back(value);
+			} else {
+				stream << decl;
+				if (expression.length() > 0) {
+					// id and expr given
+					stream << " = " << _analyzer.replaceLiterals(boost::trim_copy(expression)) << ";" << std::endl;
+				} else if (value.length() > 0) {
+					// id and text content given
+					stream << " = " << _analyzer.replaceLiterals(value) << ";" << std::endl;
+				} else {
+					// only id given
+					stream << ";" << std::endl;
+				}
+			}
+		} else if (value.length() > 0) {
+			// no id but text content given
+			stream << beautifyIndentation(value) << std::endl;
+		}
+	}
+	
+	PromelaCodeAnalyzer::PromelaTypedef allTypes = _analyzer.getTypes();
+	std::map<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator typeIter = allTypes.types.begin();
+	while(typeIter != allTypes.types.end()) {
+		if (processedIdentifiers.find(typeIter->first) != processedIdentifiers.end()) {
+			typeIter++;
+			continue;
+		}
+		if (typeIter->first == "_event" || typeIter->first == "_ioprocessors" || typeIter->first == "_SESSIONID" || typeIter->first == "_NAME") {
+			typeIter++;
+			continue;
+		}
+		
+		processedIdentifiers.insert(typeIter->first);
+		
+		if (typeIter->second.types.size() == 0) {
+			stream << "hidden " << declForRange(typeIter->first, typeIter->second.minValue, typeIter->second.maxValue) << ";" << std::endl;
+		} else {
+			stream << "hidden " << typeIter->second.name << " " << typeIter->first << ";" << std::endl;
+		}
+		typeIter++;
+	}
+
+	stream << std::endl;
+	stream << "/* event sources */" << std::endl;
+
+	if (_globalEventSource) {
+		_globalEventSource.writeDeclarations(stream);
+	}
+
+	std::map<std::string, PromelaEventSource>::iterator invIter = _invokers.begin();
+	while(invIter != _invokers.end()) {
+		invIter->second.writeDeclarations(stream);
+		invIter++;
+	}
+
+}
+
+void ChartToPromela::writeEventSources(std::ostream& stream) {
+	std::list<PromelaInline>::iterator inlineIter;
+
+	if (_globalEventSource) {
+		_globalEventSource.writeEventSource(stream);
+	}
+
+	std::map<std::string, PromelaEventSource>::iterator invIter = _invokers.begin();
+	while(invIter != _invokers.end()) {
+		invIter->second.writeEventSource(stream);
+		invIter++;
+	}
+}
+
+void ChartToPromela::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;
+
+	assert(_start->sortedOutgoing.size() == 1);
+	// initial transition has to be first one for control flow at start
+	writeTransition(stream, _start->sortedOutgoing.front(), 1);
+	
+	// every other transition
+	for (std::map<std::string, GlobalState*>::iterator stateIter = _globalConf.begin(); stateIter != _globalConf.end(); stateIter++) {
+		for (std::list<GlobalTransition*>::iterator transIter = stateIter->second->sortedOutgoing.begin(); transIter != stateIter->second->sortedOutgoing.end(); transIter++) {
+			// don't write initial transition
+			if (_start->sortedOutgoing.front() == *transIter)
+				continue;
+			// don't write trivial transitions
+			if ((*transIter)->hasExecutableContent)
+				writeTransition(stream, *transIter, 1);
+		}
+	}
+
+	stream << std::endl;
+	stream << "nextStep:" << std::endl;
+	stream << "  /* push send events to external queue */" << std::endl;
+	stream << "  if" << std::endl;
+	stream << "  :: len(tmpQ) != 0 -> { tmpQ?_event; eQ!_event }" << std::endl;
+	stream << "  :: else -> skip;" << std::endl;
+	stream << "  fi;" << std::endl << std::endl;
+
+	stream << "  /* pop an event */" << std::endl;
+	stream << "  if" << std::endl;
+	stream << "  :: len(iQ) != 0 -> iQ ? _event   /* from internal queue */" << std::endl;
+	stream << "  :: else -> eQ ? _event           /* from external queue */" << std::endl;
+	stream << "  fi;" << std::endl << std::endl;
+	stream << "  /* event dispatching per state */" << std::endl;
+	stream << "nextTransition:" << std::endl;
+	stream << "  if" << std::endl;
+
+	writeEventDispatching(stream);
+
+	stream << "  :: else -> assert(false);   /* this is an error as we dispatched all valid states */" << std::endl;
+	stream << "  fi;" << std::endl;
+	stream << "terminate: skip;" << std::endl;
+
+	// stop all event sources
+	if (_globalEventSource)
+		_globalEventSource.writeStopEventSources(stream, 1);
+
+	std::map<std::string, PromelaEventSource>::iterator invIter = _invokers.begin();
+	while(invIter != _invokers.end()) {
+		invIter->second.writeStopEventSources(stream, 1);
+		invIter++;
+	}
+
+	stream << "}" << std::endl;
+}
+
+void ChartToPromela::writeEventDispatching(std::ostream& stream) {
+	for (std::map<std::string, GlobalState*>::iterator stateIter = _globalConf.begin(); stateIter != _globalConf.end(); stateIter++) {
+//		if (_globalStates[i] == _startState)
+//			continue;
+
+		const std::string& stateId = stateIter->first;
+		const GlobalState* state = stateIter->second;
+		
+		int digits = 0;
+		LENGTH_FOR_NUMBER(state->index, digits);
+		stream << "  :: (s == s" << state->index << ") -> {";
+
+		INDENT_MIN(stream, 18 + digits, MIN_COMMENT_PADDING);
+
+		stream << " /* from state " << stateId << " */" << std::endl;
+
+		writeDispatchingBlock(stream, state->sortedOutgoing, 2);
+//		stream << "    goto nextStep;";
+		stream << "  }" << std::endl;
+	}
+}
+	
+void ChartToPromela::writeDispatchingBlock(std::ostream& stream, std::list<GlobalTransition*> transitions, int indent) {
+	std::string padding;
+	for (int i = 0; i < indent; i++) {
+		padding += "  ";
+	}
+
+	if (transitions.size() == 0) {
+		stream << padding << "eventLess = false;" << std::endl;
+		stream << padding << "goto nextStep;";
+		INDENT_MIN(stream, padding.size() + 13, MIN_COMMENT_PADDING);
+		stream << "/* no transition applicable */" << std::endl;
+		return;
+	}
+
+
+	GlobalTransition* currTrans = transitions.front();
+	transitions.pop_front();
+	std::stringstream tmpSS;
+
+	tmpSS << padding << "if" << std::endl;
+	size_t lineStart = tmpSS.tellp();
+
+	if (currTrans->condition.size() > 0) {
+		tmpSS << padding << ":: ((";
+	} else {
+		tmpSS << padding << ":: (";
+	}
+
+	if (currTrans->isEventless) {
+		tmpSS << "eventLess";
+	} else {
+		std::string eventDescs = currTrans->eventDesc;
+
+		std::list<std::string> eventNames = tokenizeIdRefs(eventDescs);
+		std::set<std::string> eventPrefixes;
+		std::list<std::string>::iterator eventNameIter = eventNames.begin();
+		while(eventNameIter != eventNames.end()) {
+			std::string eventDesc = *eventNameIter;
+			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.length() > 0) {
+				std::set<std::string> tmp = _analyzer.getEventsWithPrefix(*eventNameIter);
+				eventPrefixes.insert(tmp.begin(), tmp.end());
+			}
+			eventNameIter++;
+		}
+
+		if (eventPrefixes.size() > 0) {
+			tmpSS << "!eventLess && ";
+		} else {
+			tmpSS << "!eventLess";
+		}
+
+		std::string seperator;
+		std::set<std::string>::iterator eventIter = eventPrefixes.begin();
+		while(eventIter != eventPrefixes.end()) {
+			if (_analyzer.usesComplexEventStruct()) {
+				tmpSS << seperator << "_event.name == " << _analyzer.macroForLiteral(*eventIter);
+			} else {
+				tmpSS << seperator << "_event == " << _analyzer.macroForLiteral(*eventIter);
+			}
+			seperator = " || ";
+			eventIter++;
+		}
+	}
+
+	tmpSS << ")";
+	if (currTrans->condition.size() > 0) {
+		tmpSS << " && " + _analyzer.replaceLiterals(currTrans->condition) + ")";
+	}
+	if (currTrans->hasExecutableContent) {
+		tmpSS << " -> goto t" << currTrans->index << ";";
+		size_t lineEnd = tmpSS.tellp();
+		size_t lineLength = lineEnd - lineStart;
+		
+		for (int i = lineLength; i < MIN_COMMENT_PADDING; i++)
+			tmpSS << " ";
+		
+		tmpSS << " /* transition to " << currTrans->destination << " */" << std::endl;
+	} else {
+		
+		tmpSS << " -> {" << std::endl;
+		GlobalState* newState = _globalConf[currTrans->destination];
+		assert(newState != NULL);
+		tmpSS << padding << "  s = s" << newState->index << ";" << std::endl;
+
+		if (newState->isFinal) {
+			tmpSS << padding << "  goto terminate;";
+			INDENT_MIN(tmpSS, padding.length() + 14, MIN_COMMENT_PADDING);
+			tmpSS << "/* final state */" << std::endl;
+		} else if (currTrans->isEventless) {
+			tmpSS << padding << "  goto nextTransition;";
+			INDENT_MIN(tmpSS, padding.length() + 19, MIN_COMMENT_PADDING);
+			tmpSS << "/* spontaneous transition, check for more transitions */" << std::endl;
+		} else {
+			tmpSS << padding << "  eventLess = true;" << std::endl;
+			tmpSS << padding << "  goto nextTransition;";
+			INDENT_MIN(tmpSS, padding.length() + 21, MIN_COMMENT_PADDING);
+			tmpSS << "/* ordinary transition, check for spontaneous transitions */" << std::endl;
+		}
+
+		tmpSS << padding << "}" << std::endl;
+	}
+	stream << tmpSS.str();
+
+	stream << padding << ":: else {" << std::endl;
+
+	writeDispatchingBlock(stream, transitions, indent + 1);
+
+	stream << padding << "}" << std::endl;
+	stream << padding << "fi;" << std::endl;
+}
+
+void ChartToPromela::writeMain(std::ostream& stream) {
+	stream << std::endl;
+	stream << "init {" << std::endl;
+	if (_varInitializers.size() > 0) {
+		std::list<std::string>::iterator initIter = _varInitializers.begin();
+		while(initIter != _varInitializers.end()) {
+			stream << beautifyIndentation(*initIter);
+			initIter++;
+		}
+		stream << std::endl;
+	}
+	if (_globalEventSource)
+		_globalEventSource.writeStartEventSources(stream, 1);
+	stream << "  run step();" << std::endl;
+	stream << "}" << std::endl;
+
+}
+
+
+void ChartToPromela::initNodes() {
+		
+	// get all states
+	NodeSet<std::string> states = getAllStates();
+	for (int i = 0; i < states.size(); i++) {
+		if (InterpreterImpl::isInEmbeddedDocument(states[i]))
+			continue;
+		Element<std::string> stateElem(states[i]);
+		_analyzer.addOrigState(ATTR(stateElem, "id"));
+		if (isCompound(stateElem) || isParallel(stateElem)) {
+			_analyzer.addEvent("done.state." + ATTR(stateElem, "id"));
+		}
+	}
+	
+	// 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_CAST(internalEventNames[i], "event")) {
+			std::string eventNames = ATTR_CAST(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);
+				if (eventName.size() > 0)
+					_analyzer.addEvent(eventName);
+			}
+		}
+	}
+
+	// do we need sendid / invokeid?
+	{
+		NodeSet<std::string> invokes = filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true);
+		NodeSet<std::string> sends = filterChildElements(_nsInfo.xmlNSPrefix + "send", _scxml, true);
+
+		for (int i = 0; i < invokes.size(); i++) {
+			if (HAS_ATTR_CAST(invokes[i], "idlocation")) {
+			}
+		}
+
+		for (int i = 0; i < sends.size(); i++) {
+			if (HAS_ATTR_CAST(sends[i], "idlocation")) {
+				_analyzer.addCode("_event.sendid");
+			}
+			if (HAS_ATTR_CAST(sends[i], "id")) {
+				_analyzer.addLiteral(ATTR_CAST(sends[i], "id"));
+				_analyzer.addCode("_event.sendid");
+			}
+		}
+
+	}
+	
+	// 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, false)); // 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++) {
+		PromelaInlines promInls = getInlinePromela(promelaEventSourceComments[i]);
+		PromelaEventSource promES(promInls, promelaEventSourceComments[i].getParentNode());
+
+		if (TAGNAME_CAST(promelaEventSourceComments[i].getParentNode()) == "scxml") {
+			promES.type = PromelaEventSource::PROMELA_EVENT_SOURCE_GLOBAL;
+			promES.analyzer = &_analyzer;
+			promES.name = "global";
+			_globalEventSource = promES;
+		} else if (TAGNAME_CAST(promelaEventSourceComments[i].getParentNode()) == "invoke") {
+			if (!HAS_ATTR_CAST(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_CAST(promelaEventSourceComments[i].getParentNode(), "invokeid");
+			promES.type = PromelaEventSource::PROMELA_EVENT_SOURCE_INVOKER;
+			promES.analyzer = &_analyzer;
+			promES.name = invokeId;
+			_invokers[invokeId] = promES;
+		}
+	}
+
+#if 0
+	// enumerate transitions
+	NodeSet<std::string> transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", _scxml, true);
+	int index = 0;
+	for (int i = 0; i < transitions.size(); i++) {
+		_transitions[Element<std::string>(transitions[i])] = index++;
+	}
+#endif
+	
+	// add platform variables as string literals
+	_analyzer.addLiteral("_sessionid");
+	_analyzer.addLiteral("_name");
+
+	if (HAS_ATTR(_scxml, "name")) {
+		_analyzer.addLiteral(ATTR(_scxml, "name"), _analyzer.indexForLiteral("_sessionid"));
+	}
+
+	NodeSet<std::string> contents = filterChildElements(_nsInfo.xmlNSPrefix + "content", _scxml, true);
+	for (int i = 0; i < contents.size(); i++) {
+		Element<std::string> contentElem = Element<std::string>(contents[i]);
+		if (contentElem.hasChildNodes() && contentElem.getFirstChild().getNodeType() == Node_base::TEXT_NODE) {
+			_analyzer.addLiteral(spaceNormalize(contentElem.getFirstChild().getNodeValue()));
+		}
+	}
+
+
+	// extract and analyze source code
+	std::set<std::string> allCode;
+	std::set<std::string> allStrings;
+	{
+		NodeSet<std::string> withCond;
+		withCond.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "transition", _scxml, true));
+		withCond.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "if", _scxml, true));
+		withCond.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "elseif", _scxml, true));
+		for (int i = 0; i < withCond.size(); i++) {
+			Element<std::string> elem = Element<std::string>(withCond[i]);
+			if (HAS_ATTR(elem, "cond")) {
+				std::string code = ATTR(elem, "cond");
+				code = sanitizeCode(code);
+				elem.setAttribute("cond", code);
+				allCode.insert(code);
+			}
+		}
+	}
+	{
+		NodeSet<std::string> withExpr;
+		withExpr.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "log", _scxml, true));
+		withExpr.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "data", _scxml, true));
+		withExpr.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "assign", _scxml, true));
+		withExpr.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "content", _scxml, true));
+		withExpr.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "param", _scxml, true));
+		for (int i = 0; i < withExpr.size(); i++) {
+			Element<std::string> elem = Element<std::string>(withExpr[i]);
+			if (HAS_ATTR(elem, "expr")) {
+				std::string code = ATTR(elem, "expr");
+				code = sanitizeCode(code);
+				elem.setAttribute("expr", code);
+				allCode.insert(code);
+			}
+		}
+	}
+	{
+		NodeSet<std::string> withLocation;
+		withLocation.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "assign", _scxml, true));
+		for (int i = 0; i < withLocation.size(); i++) {
+			Element<std::string> elem = Element<std::string>(withLocation[i]);
+			if (HAS_ATTR(elem, "location")) {
+				std::string code = ATTR(elem, "location");
+				code = sanitizeCode(code);
+				elem.setAttribute("location", code);
+				allCode.insert(code);
+			}
+		}
+	}
+	{
+		NodeSet<std::string> withText;
+		withText.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "script", _scxml, true));
+		withText.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "data", _scxml, true));
+		for (int i = 0; i < withText.size(); i++) {
+			NodeSet<std::string> texts = filterChildType(Node_base::TEXT_NODE, withText[i], true);
+			for (int j = 0; j < texts.size(); j++) {
+				if (texts[j].getNodeValue().size() > 0) {
+					Text<std::string> elem = Text<std::string>(texts[j]);
+					std::string code = elem.getNodeValue();
+					code = sanitizeCode(code);
+					elem.setNodeValue(code);
+					allCode.insert(code);
+				}
+			}
+		}
+	}
+	for (std::set<std::string>::const_iterator codeIter = allCode.begin(); codeIter != allCode.end(); codeIter++) {
+		_analyzer.addCode(*codeIter);
+	}
+
+}
+
+std::string ChartToPromela::sanitizeCode(const std::string& code) {
+	std::string replaced = code;
+	boost::replace_all(replaced, "\"", "'");
+	boost::replace_all(replaced, "_sessionid", "_SESSIONID");
+	boost::replace_all(replaced, "_name", "_NAME");
+	return replaced;
+}
+
+void PromelaInline::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 ChartToPromela::writeProgram(std::ostream& stream) {
+
+	if (!HAS_ATTR(_scxml, "datamodel") || ATTR(_scxml, "datamodel") != "promela") {
+		LOG(ERROR) << "Can only convert SCXML documents with \"promela\" datamodel";
+		return;
+	}
+
+	if (_start == NULL) {
+		interpret();
+	}
+
+	if (HAS_ATTR(_scxml, "binding") && ATTR(_scxml, "binding") != "early") {
+		LOG(ERROR) << "Can only convert for early data bindings";
+		return;
+	}
+
+//	std::cerr << _scxml << std::endl;
+
+	initNodes();
+
+	writeEvents(stream);
+	stream << std::endl;
+	writeStates(stream);
+	stream << std::endl;
+	if (_analyzer.usesInPredicate()) {
+		writeStateMap(stream);
+		stream << std::endl;
+	}
+	writeTypeDefs(stream);
+	stream << std::endl;
+	writeStrings(stream);
+	stream << std::endl;
+	writeDeclarations(stream);
+	stream << std::endl;
+	writeEventSources(stream);
+	stream << std::endl;
+	writeFSM(stream);
+	stream << std::endl;
+	writeMain(stream);
+	stream << std::endl;
+
+	// write ltl expression for success
+	std::stringstream acceptingStates;
+	std::string seperator;
+	
+	for (std::map<std::string, GlobalState*>::iterator stateIter = _globalConf.begin(); stateIter != _globalConf.end(); stateIter++) {
+		FlatStateIdentifier flatId(stateIter->first);
+		if (std::find(flatId.getActive().begin(), flatId.getActive().end(), "pass") != flatId.getActive().end()) {
+			acceptingStates << seperator << "s == s" << stateIter->second->index;
+			seperator = " || ";
+		}
+	}
+	if (acceptingStates.str().size() > 0) {
+		stream << "ltl { eventually (" << acceptingStates.str() << ") }" << std::endl;
+	}
+
+//	if (_states.find("active:{pass}") != _states.end()) {
+//		for (int i = 0; i < _globalStates.size(); i++) {
+//			if (_states["active:{pass}"] != _globalStates[i])
+//				continue;
+//			stream << "ltl { eventually (s == s" << i << ") }";
+//			break;
+//		}
+//	}
+}
+
+}
\ No newline at end of file