Impreoved PROMELA transformation

5 files changed, 1804 insertions, 1459 deletions

diff --git a/src/uscxml/transform/ChartToPromela.cpp b/src/uscxml/transform/ChartToPromela.cpp
index a697d99..9a8b999 100644
--- a/src/uscxml/transform/ChartToPromela.cpp
+++ b/src/uscxml/transform/ChartToPromela.cpp
@@ -28,9 +28,42 @@
 
 #include <algorithm>
 
-#define ADAPT_SRC(code) _analyzer.adaptCode(code, _prefix)
+#define ADAPT_SRC(code) _analyzer->adaptCode(code, _prefix)
 #define BIT_WIDTH(number) (number > 1 ? (int)ceil(log((double)number) / log((double)2.0)) : 1)
-#define EVENT_NAME (_analyzer.usesComplexEventStruct() ? "_event.name" : "_event")
+#define EVENT_NAME (_analyzer->usesComplexEventStruct() ? "_event.name" : "_event")
+#define TMP_EVENT_NAME (_analyzer->usesComplexEventStruct() ? "_tmpE.name" : "_tmpE")
+#define MAX(X,Y) ((X) > (Y) ? (X) : (Y))
+
+#undef TRACE_EXECUTION
+
+#ifdef TRACE_EXECUTION
+#define TRACE_EXECUTION_V(fmt, ...) \
+stream << std::endl; \
+stream << "#if TRACE_EXECUTION" << std::endl; \
+if (_machinesAll->size() > 1) {\
+    stream << "printf(\"%d: " fmt "\\n\", _pid, " __VA_ARGS__ ");" << std::endl; \
+} else { \
+    stream << "printf(\"" fmt "\\n\", " __VA_ARGS__ ");" << std::endl; \
+} \
+stream << "#endif" << std::endl; \
+stream << std::endl;
+
+#define TRACE_EXECUTION(fmt) \
+stream << std::endl; \
+stream << "#if TRACE_EXECUTION" << std::endl; \
+if (_machinesAll->size() > 1) {\
+stream << "printf(\"%d: " fmt "\\n\", _pid);" << std::endl; \
+} else { \
+stream << "printf(\"" fmt "\\n\");" << std::endl; \
+} \
+stream << "#endif" << std::endl; \
+stream << std::endl;
+
+#else
+
+#define TRACE_EXECUTION_V(fmt, ...)
+#define TRACE_EXECUTION(fmt)
+#endif
 
 namespace uscxml {
 
@@ -44,148 +77,78 @@ Transformer ChartToPromela::transform(const Interpreter& other) {
 ChartToPromela::~ChartToPromela() {
 }
 
-/**
- The following tests FAILED:
- 1740 - w3c/spin/promela/test150.scxml (Failed)
- 1741 - w3c/spin/promela/test151.scxml (Failed)
- 1742 - w3c/spin/promela/test152.scxml (Failed)
- 1743 - w3c/spin/promela/test153.scxml (Failed)
- 1744 - w3c/spin/promela/test155.scxml (Failed)
- 1745 - w3c/spin/promela/test156.scxml (Failed)
- 1749 - w3c/spin/promela/test173.scxml (Failed)
- 1750 - w3c/spin/promela/test174.scxml (Failed)
- 1752 - w3c/spin/promela/test176.scxml (Failed)
- 1753 - w3c/spin/promela/test178.scxml (Failed)
- 1754 - w3c/spin/promela/test179.scxml (Failed)
- 1757 - w3c/spin/promela/test186.scxml (Failed)
- 1762 - w3c/spin/promela/test192.scxml (Failed)
- 1763 - w3c/spin/promela/test193.scxml (Failed)
- 1765 - w3c/spin/promela/test198.scxml (Failed)
- 1769 - w3c/spin/promela/test205.scxml (Failed)
- 1770 - w3c/spin/promela/test207.scxml (Failed)
- 1771 - w3c/spin/promela/test208.scxml (Failed)
- 1772 - w3c/spin/promela/test210.scxml (Failed)
- 1773 - w3c/spin/promela/test215.scxml (Failed)
- 1774 - w3c/spin/promela/test216.scxml (Failed)
- 1776 - w3c/spin/promela/test223.scxml (Failed)
- 1777 - w3c/spin/promela/test224.scxml (Failed)
- 1778 - w3c/spin/promela/test225.scxml (Failed)
- 1780 - w3c/spin/promela/test228.scxml (Failed)
- 1782 - w3c/spin/promela/test230.scxml (Failed)
- 1783 - w3c/spin/promela/test232.scxml (Failed)
- 1785 - w3c/spin/promela/test234.scxml (Failed)
- 1787 - w3c/spin/promela/test236.scxml (Failed)
- 1788 - w3c/spin/promela/test237.scxml (Failed)
- 1789 - w3c/spin/promela/test239.scxml (Failed)
- 1790 - w3c/spin/promela/test240.scxml (Failed)
- 1791 - w3c/spin/promela/test241.scxml (Failed)
- 1792 - w3c/spin/promela/test242.scxml (Failed)
- 1797 - w3c/spin/promela/test250.scxml (Failed)
- 1798 - w3c/spin/promela/test252.scxml (Failed)
- 1799 - w3c/spin/promela/test253.scxml (Failed)
- 1802 - w3c/spin/promela/test278.scxml (Failed)
- 1803 - w3c/spin/promela/test279.scxml (Failed)
- 1805 - w3c/spin/promela/test286.scxml (Failed)
- 1808 - w3c/spin/promela/test294.scxml (Failed)
- 1809 - w3c/spin/promela/test298.scxml (Failed)
- 1811 - w3c/spin/promela/test302.scxml (Failed)
- 1813 - w3c/spin/promela/test304.scxml (Failed)
- 1814 - w3c/spin/promela/test309.scxml (Failed)
- 1815 - w3c/spin/promela/test310.scxml (Failed)
- 1816 - w3c/spin/promela/test311.scxml (Failed)
- 1817 - w3c/spin/promela/test312.scxml (Failed)
- 1818 - w3c/spin/promela/test313.scxml (Failed)
- 1819 - w3c/spin/promela/test314.scxml (Failed)
- 1820 - w3c/spin/promela/test318.scxml (Failed)
- 1823 - w3c/spin/promela/test322.scxml (Failed)
- 1825 - w3c/spin/promela/test324.scxml (Failed)
- 1827 - w3c/spin/promela/test326.scxml (Failed)
- 1828 - w3c/spin/promela/test329.scxml (Failed)
- 1829 - w3c/spin/promela/test330.scxml (Failed)
- 1830 - w3c/spin/promela/test331.scxml (Failed)
- 1831 - w3c/spin/promela/test332.scxml (Failed)
- 1832 - w3c/spin/promela/test333.scxml (Failed)
- 1833 - w3c/spin/promela/test335.scxml (Failed)
- 1835 - w3c/spin/promela/test337.scxml (Failed)
- 1837 - w3c/spin/promela/test339.scxml (Failed)
- 1838 - w3c/spin/promela/test342.scxml (Failed)
- 1839 - w3c/spin/promela/test343.scxml (Failed)
- 1840 - w3c/spin/promela/test344.scxml (Failed)
- 1841 - w3c/spin/promela/test346.scxml (Failed)
- 1842 - w3c/spin/promela/test347.scxml (Failed)
- 1846 - w3c/spin/promela/test351.scxml (Failed)
- 1847 - w3c/spin/promela/test352.scxml (Failed)
- 1848 - w3c/spin/promela/test354.scxml (Failed)
- 1849 - w3c/spin/promela/test355.scxml (Failed)
- 1850 - w3c/spin/promela/test364.scxml (Failed)
- 1851 - w3c/spin/promela/test372.scxml (Failed)
- 1854 - w3c/spin/promela/test377.scxml (Failed)
- 1855 - w3c/spin/promela/test378.scxml (Failed)
- 1856 - w3c/spin/promela/test387.scxml (Failed)
- 1857 - w3c/spin/promela/test388.scxml (Failed)
- 1858 - w3c/spin/promela/test396.scxml (Failed)
- 1859 - w3c/spin/promela/test399.scxml (Failed)
- 1860 - w3c/spin/promela/test401.scxml (Failed)
- 1861 - w3c/spin/promela/test402.scxml (Failed)
- 1862 - w3c/spin/promela/test403a.scxml (Failed)
- 1863 - w3c/spin/promela/test403b.scxml (Failed)
- 1864 - w3c/spin/promela/test403c.scxml (Failed)
- 1865 - w3c/spin/promela/test404.scxml (Failed)
- 1866 - w3c/spin/promela/test405.scxml (Failed)
- 1867 - w3c/spin/promela/test406.scxml (Failed)
- 1868 - w3c/spin/promela/test407.scxml (Failed)
- 1869 - w3c/spin/promela/test409.scxml (Failed)
- 1870 - w3c/spin/promela/test411.scxml (Failed)
- 1871 - w3c/spin/promela/test412.scxml (Failed)
- 1872 - w3c/spin/promela/test413.scxml (Failed)
- 1873 - w3c/spin/promela/test415.scxml (Failed)
- 1874 - w3c/spin/promela/test416.scxml (Failed)
- 1875 - w3c/spin/promela/test417.scxml (Failed)
- 1877 - w3c/spin/promela/test421.scxml (Failed)
- 1878 - w3c/spin/promela/test422.scxml (Failed)
- 1880 - w3c/spin/promela/test487.scxml (Failed)
- 1881 - w3c/spin/promela/test488.scxml (Failed)
- 1882 - w3c/spin/promela/test495.scxml (Failed)
- 1886 - w3c/spin/promela/test503.scxml (Failed)
- 1887 - w3c/spin/promela/test504.scxml (Failed)
- 1888 - w3c/spin/promela/test505.scxml (Failed)
- 1890 - w3c/spin/promela/test509.scxml (Failed)
- 1892 - w3c/spin/promela/test518.scxml (Failed)
- 1893 - w3c/spin/promela/test519.scxml (Failed)
- 1894 - w3c/spin/promela/test520.scxml (Failed)
- 1897 - w3c/spin/promela/test525.scxml (Failed)
- 1898 - w3c/spin/promela/test527.scxml (Failed)
- 1899 - w3c/spin/promela/test528.scxml (Failed)
- 1900 - w3c/spin/promela/test529.scxml (Failed)
- 1901 - w3c/spin/promela/test530.scxml (Failed)
- 1902 - w3c/spin/promela/test531.scxml (Failed)
- 1903 - w3c/spin/promela/test532.scxml (Failed)
- 1904 - w3c/spin/promela/test533.scxml (Failed)
- 1905 - w3c/spin/promela/test534.scxml (Failed)
- 1906 - w3c/spin/promela/test550.scxml (Failed)
- 1907 - w3c/spin/promela/test551.scxml (Failed)
- 1911 - w3c/spin/promela/test567.scxml (Failed)
- 1912 - w3c/spin/promela/test570.scxml (Failed)
- 1913 - w3c/spin/promela/test576.scxml (Failed)
- 1915 - w3c/spin/promela/test579.scxml (Failed)
- 1916 - w3c/spin/promela/test580.scxml (Failed)
-*/
-
 void ChartToPromela::prepare() {
     if (_machinesAll == NULL) {
-        _machinesAll = new std::map<DOMNode*, ChartToPromela*>();
+        _machinesAll = new std::map<DOMElement*, ChartToPromela*>();
         (*_machinesAll)[_scxml] = this;
     }
 
     if (_machinesAllPerId == NULL)
-        _machinesAllPerId = new std::map<std::string, XERCESC_NS::DOMNode* >();
+        _machinesAllPerId = new std::map<std::string, XERCESC_NS::DOMElement* >();
 
-    if (_parentTopMost == NULL)
+    if (_parentTopMost == NULL) {
         _parentTopMost = this;
+    }
+
+    // are there nested SCXML invokers?
+    std::list<DOMElement*> invokes = DOMUtils::inDocumentOrder({ XML_PREFIX(_scxml).str() + "invoke" }, _scxml);
+    for (auto invoke : invokes) {
+        
+        if (!HAS_ATTR(invoke, "id")) {
+            invoke->setAttribute(X("id"), X("INV_" + UUID::getUUID().substr(0,5)));
+        } else if (HAS_ATTR(invoke, "id") && UUID::isUUID(ATTR(invoke, "id"))) {
+            // shorten UUIDs
+            invoke->setAttribute(X("id"), X("INV_" + ATTR(invoke, "id").substr(0,5)));
+        }
+
+        if (HAS_ATTR(invoke, "type") &&
+            ATTR(invoke, "type") != "scxml" &&
+            ATTR(invoke, "type") != "http://www.w3.org/TR/scxml/" &&
+            ATTR(invoke, "type") != "http://www.w3.org/TR/scxml/#SCXMLEventProcessor")
+            continue;
+        
+        assert(HAS_ATTR(invoke, "id"));
+        invoke->setAttribute(X("name"), invoke->getAttribute(X("id")));
+        
+        Interpreter nested;
+        if (HAS_ATTR(invoke, "src")) {
+            nested = Interpreter::fromURL(URL::resolve(ATTR(invoke, "src"), _baseURL));
+        } else {
+            std::list<DOMElement*> contents = DOMUtils::filterChildElements(XML_PREFIX(invoke).str() + "content", invoke);
+            std::list<DOMElement*> scxmls = DOMUtils::filterChildElements(XML_PREFIX(invoke).str() + "scxml", contents.front());
+
+            assert (scxmls.size() > 0);
+            nested = Interpreter::fromElement(scxmls.front(), _baseURL);
+        }
+        
+        _machinesNested[invoke] = new ChartToPromela(nested);
+        _machinesNested[invoke]->_analyzer = _analyzer;
+        _machinesNested[invoke]->_analyzer->analyze(_machinesNested[invoke]);
+        _machinesNested[invoke]->prepare();
+        _machinesNested[invoke]->_parent = this;
+        _machinesNested[invoke]->_parentTopMost = _parentTopMost;
+        _machinesNested[invoke]->_machinesAll = _machinesAll;
+        (*_machinesAll)[invoke] = _machinesNested[invoke];
+        
+        _machinesNested[invoke]->_invokerid = ATTR(invoke, "id");
+        _analyzer->createMacroName(_machinesNested[invoke]->_invokerid);
+        _analyzer->addEvent("done.invoke." + _machinesNested[invoke]->_invokerid);
+
+        _machinesNested[invoke]->_prefix = _analyzer->macroForLiteral(ATTR(invoke, "id")) + "_";
+        
+        
+        _machinesPerId[ATTR_CAST(invoke, "id")] = invoke;
+        (*_machinesAllPerId)[ATTR(invoke, "id")] = invoke;
+
+    }
+    
+    if (_machinesAll->size() > 1) {
+//        _analyzer->addCode("_event.origin", this);
+        _analyzer->addCode("_event.invokeid", this);
+    }
 
     // transform data / assign json into PROMELA statements
     std::list<DOMElement*> values;
-    
     values.splice(values.end(), DOMUtils::inDocumentOrder({XML_PREFIX(_scxml).str() + "assign"}, _scxml));
     values.splice(values.end(), DOMUtils::inDocumentOrder({XML_PREFIX(_scxml).str() + "data"}, _scxml));
 
@@ -219,7 +182,7 @@ void ChartToPromela::prepare() {
         if (value.size() == 0)
             continue;
         
-        // remove all children, we will replae by suitable promela statements
+        // remove all children, we will replace by suitable promela statements
         while(element->hasChildNodes())
             element->removeChild(element->getFirstChild());
 
@@ -237,57 +200,111 @@ void ChartToPromela::prepare() {
         DOMText* newText = _document->createTextNode(X(newValue));
         element->insertBefore(newText, NULL);
 
-        _analyzer.addCode(newValue, this);
+        _analyzer->addCode(newValue, this);
 
     }
 }
     
 void ChartToPromela::writeTo(std::ostream& stream) {
-
-    _analyzer.analyze(this);
-	// same preparations as the C transformation
+    _prefix = "ROOT_";
+    _invokerid = "ROOT";
+    _analyzer = new PromelaCodeAnalyzer();
+    _analyzer->analyze(this);
+    _analyzer->createMacroName(_invokerid);
     prepare();
 
 	stream << "/** generated from " << std::endl;
 	stream << "  " << std::string(_baseURL) << std::endl;
-	stream << "  Use as:" << std::endl;
+	stream << "  Verify as:" << std::endl;
 	stream << "  $ spin -a this.pml" << std::endl;
-	stream << "  $ gcc pan.c -o pan" << std::endl;
-	stream << "  $ ./pan -a -n -N w3c" << std::endl;
+	stream << "  $ gcc -DMEMLIM=1024 -DVECTORSZ=8192 -O2 -DXUSAFE pan.c -o pan" << std::endl;
+	stream << "  $ ./pan -a -m10000 -n -N w3c" << std::endl;
 	stream << " */" << std::endl;
 	stream << std::endl;
 
 
 	writeMacros(stream);
-	stream << std::endl;
-    writeTypeDefs(stream);
-    stream << std::endl;
-    writeTypes(stream);
     stream << std::endl;
     writeStrings(stream);
     stream << std::endl;
+
+    for (auto machine : *_machinesAll) {
+        machine.second->writeBitHasAndMacro(stream);
+        stream << std::endl;
+        machine.second->writeBitHasAnyMacro(stream);
+        stream << std::endl;
+        machine.second->writeBitOrMacro(stream);
+        stream << std::endl;
+        machine.second->writeBitClearMacro(stream);
+        stream << std::endl;
+        machine.second->writeBitCopyMacro(stream);
+        stream << std::endl;
+        machine.second->writeBitAndMacro(stream);
+        stream << std::endl;
+        machine.second->writeBitAndNotMacro(stream);
+        stream << std::endl;
+        writeTypeDefs(stream);
+        stream << std::endl;
+
+    }
+
+    writeCommonTypeDefs(stream);
+    stream << std::endl;
+
+    for (auto machine : *_machinesAll) {
+        machine.second->writeVariables(stream);
+        stream << std::endl;
+    }
+    writeCommonVariables(stream);
+    stream << std::endl;
+
+    if (_analyzer->usesComplexEventStruct()) {
+        if (_analyzer->usesEventField("delay")) {
+            writeInsertWithDelay(stream);
+            stream << std::endl;
+        }
+        writeAdvanceTime(stream);
+        stream << std::endl;
+        writeScheduleMachines(stream);
+        stream << std::endl;
+        writeRescheduleProcess(stream);
+        stream << std::endl;
+        writeDetermineShortestDelay(stream);
+        stream << std::endl;
+    }
+    
+    if (_machinesAll->size() > 1) {
+        writeRemovePendingEventsFromInvoker(stream);
+        stream << std::endl;
+    }
+    
     writeCancelEvents(stream);
     stream << std::endl;
-	writeFSM(stream);
-	stream << std::endl;
+    
+    for (auto machine : *_machinesAll) {
+        machine.second->writeFSM(stream);
+        stream << std::endl;
+    }
 
 
 	stream << "init {" << std::endl;
     
     stream << "/* initialize state and transition information */" << std::endl;
-	writeTransitions(stream);
-	stream << std::endl;
-	writeStates(stream);
-    stream << std::endl;
+    for (auto machine : *_machinesAll) {
+        machine.second->writeTransitions(stream);
+        stream << std::endl;
+        machine.second->writeStates(stream);
+        stream << std::endl;
 
-    stream << "/* initialize data model variables */" << std::endl;
-	stream << "  " << _prefix << "flags[USCXML_CTX_PRISTINE]  = true;" << std::endl;
-	stream << "  " << _prefix << "flags[USCXML_CTX_SPONTANEOUS] = true;" << std::endl;
+        stream << "/* initialize data model variables */" << std::endl;
+        stream << "  " << machine.second->_prefix << "flags[USCXML_CTX_PRISTINE]  = true;" << std::endl;
+        stream << "  " << machine.second->_prefix << "flags[USCXML_CTX_SPONTANEOUS] = true;" << std::endl;
 
-    for (auto initializer : _varInitializers) {
-        stream << ADAPT_SRC(beautifyIndentation(initializer, 1)) << std::endl;
+        for (auto initializer : machine.second->_varInitializers) {
+            stream << _analyzer->adaptCode(beautifyIndentation(initializer, 1), machine.second->_prefix) << std::endl;
+        }
     }
-
+    
     stream << std::endl;
 
 	stream << "  run " << _prefix << "step() priority 10;" << std::endl;
@@ -297,94 +314,129 @@ void ChartToPromela::writeTo(std::ostream& stream) {
 
 }
 
-void ChartToPromela::bit_clear_all(std::ostream& stream,
-                                   const std::string& identifier,
-                                   size_t length,
-                                   size_t indent) {
-	std::string padding;
-	while (indent--)
-		padding += "  ";
-	stream << std::endl;
-	stream << padding << "/** clearing all bits of " << identifier << " */" << std::endl;
-	for (size_t i = 0; i < length; i++) {
-		stream << padding << identifier << "[" << i << "] = false;" << std::endl;
-	}
+void ChartToPromela::writeBitAndMacro(std::ostream& stream) {
+    stream << "/** and'ing bits in a with mask */" << std::endl;
+    stream << "#define " << _prefix << "TRANS_AND(a, mask) \\" << std::endl;
+    for (size_t i = 0; i < _transitions.size(); i++) {
+        stream << "a[" << i << "] = a[" << i << "] & mask[" << i << "]; \\" << std::endl;
+    }
+    stream << std::endl;
+
+    stream << "#define " << _prefix << "STATES_AND(a, mask) \\" << std::endl;
+    for (size_t i = 0; i < _states.size(); i++) {
+        stream << "a[" << i << "] = a[" << i << "] & mask[" << i << "]; \\" << std::endl;
+    }
+    stream << std::endl;
+
 }
 
-void ChartToPromela::bit_copy(std::ostream& stream,
-                              const std::string& from,
-                              const std::string& to,
-                              size_t length,
-                              size_t indent) {
-	std::string padding;
-	while (indent--)
-		padding += "  ";
-	stream << std::endl;
-	stream << padding << "/** copy bits from " << from << " to " << to << " */" << std::endl;
-	for (size_t i = 0; i < length; i++) {
-		stream << padding << to << "[" << i << "] = "<< from << "[" << i << "];" << std::endl;
-	}
+void ChartToPromela::writeBitAndNotMacro(std::ostream& stream) {
+    stream << "/** not and'ing bits in a with mask */" << std::endl;
+    stream << "#define " << _prefix << "TRANS_AND_NOT(a, mask) \\" << std::endl;
+    for (size_t i = 0; i < _transitions.size(); i++) {
+        stream << "a[" << i << "] = a[" << i << "] & !mask[" << i << "]; \\" << std::endl;
+    }
+    stream << std::endl;
+    
+    stream << "#define " << _prefix << "STATES_AND_NOT(a, mask) \\" << std::endl;
+    for (size_t i = 0; i < _states.size(); i++) {
+        stream << "a[" << i << "] = a[" << i << "] & !mask[" << i << "]; \\" << std::endl;
+    }
+    stream << std::endl;
+    
 }
 
-void ChartToPromela::bit_or(std::ostream& stream,
-                            const std::string& to,
-                            const std::string& mask,
-                            size_t length,
-                            size_t indent) {
-	std::string padding;
-	while (indent--)
-		padding += "  ";
-	stream << std::endl;
-	stream << padding << "/** or'ing bits in " << to << " with mask " << mask << " */" << std::endl;
-	for (size_t i = 0; i < length; i++) {
-		stream << padding << to << "[" << i << "] = "<< to << "[" << i << "] | " << mask << "[" << i << "];" << std::endl;
+void ChartToPromela::writeBitCopyMacro(std::ostream& stream) {
+    stream << "/** copy bits from a to b */" << std::endl;
+    stream << "#define " << _prefix << "TRANS_COPY(a, b) \\" << std::endl;
+    for (size_t i = 0; i < _transitions.size(); i++) {
+        stream << "a[" << i << "] = b[" << i << "]; \\" << std::endl;
+    }
+    stream << std::endl;
+
+    stream << "#define " << _prefix << "STATES_COPY(a, b) \\" << std::endl;
+    for (size_t i = 0; i < _states.size(); i++) {
+        stream << "a[" << i << "] = b[" << i << "]; \\" << std::endl;
+    }
+    stream << std::endl;
+
+    
+}
+    
+void ChartToPromela::writeBitHasAndMacro(std::ostream& stream) {
+    stream << "/** is there a common bit in t1 and t2 */" << std::endl;
+    stream << "#define " << _prefix << "TRANS_HAS_AND(a, b) \\" << std::endl;
+    
+	stream << "(false \\" << std::endl;
+	for (size_t i = 0; i < _transitions.size(); i++) {
+		stream << " || a[" << i << "] & b[" << i << "] \\" << std::endl;
 	}
+	stream << ")" << std::endl;
+    stream << std::endl;
+
+    stream << "#define " << _prefix << "STATES_HAS_AND(a, b) \\" << std::endl;
+    
+    stream << "(false \\" << std::endl;
+    for (size_t i = 0; i < _states.size(); i++) {
+        stream << " || a[" << i << "] & b[" << i << "] \\" << std::endl;
+    }
+    stream << ")" << std::endl;
+    stream << std::endl;
+
 }
 
-void ChartToPromela::bit_and(std::ostream& stream,
-                             const std::string& to,
-                             const std::string& mask,
-                             size_t length,
-                             size_t indent) {
-	std::string padding;
-	while (indent--)
-		padding += "  ";
-	stream << std::endl;
-	stream << padding << "/** and'ing bits in " << to << " with mask " << mask << " */" << std::endl;
-	for (size_t i = 0; i < length; i++) {
-		stream << padding << to << "[" << i << "] = "<< to << "[" << i << "] & " << mask << "[" << i << "];" << std::endl;
-	}
+void ChartToPromela::writeBitHasAnyMacro(std::ostream& stream) {
+    stream << "/** is there bit set in a */" << std::endl;
+    stream << "#define " << _prefix << "TRANS_HAS_ANY(a) \\" << std::endl;
+    
+    stream << "(false \\" << std::endl;
+    for (size_t i = 0; i < _transitions.size(); i++) {
+        stream << " || a[" << i << "] \\" << std::endl;
+    }
+    stream << ")" << std::endl;
+    stream << std::endl;
+    
+    stream << "#define " << _prefix << "STATES_HAS_ANY(a) \\" << std::endl;
+    
+    stream << "(false \\" << std::endl;
+    for (size_t i = 0; i < _states.size(); i++) {
+        stream << " || a[" << i << "] \\" << std::endl;
+    }
+    stream << ")" << std::endl;
+    stream << std::endl;
+    
 }
 
-void ChartToPromela::bit_and_not(std::ostream& stream,
-                                 const std::string& to,
-                                 const std::string& mask,
-                                 size_t length,
-                                 size_t indent) {
-	std::string padding;
-	while (indent--)
-		padding += "  ";
-	stream << std::endl;
-	stream << padding << "/** not and'ing bits in " << to << " with mask " << mask << " */" << std::endl;
-	for (size_t i = 0; i < length; i++) {
-		stream << padding << to << "[" << i << "] = "<< to << "[" << i << "] & !" << mask << "[" << i << "];" << std::endl;
-	}
+void ChartToPromela::writeBitOrMacro(std::ostream& stream) {
+    stream << "/** or'ing bits in a with mask */" << std::endl;
+    stream << "#define " << _prefix << "TRANS_OR(a, mask) \\" << std::endl;
+    for (size_t i = 0; i < _transitions.size(); i++) {
+        stream << "a[" << i << "] = a[" << i << "] | mask[" << i << "]; \\" << std::endl;
+    }
+    stream << std::endl;
+
+    stream << "#define " << _prefix << "STATES_OR(a, mask) \\" << std::endl;
+    for (size_t i = 0; i < _states.size(); i++) {
+        stream << "a[" << i << "] = a[" << i << "] | mask[" << i << "]; \\" << std::endl;
+    }
+    stream << std::endl;
+
 }
 
-void ChartToPromela::bit_has_and(std::ostream& stream,
-                                 const std::string& a,
-                                 const std::string& b,
-                                 size_t length,
-                                 size_t indent) {
-	std::string padding;
-	while (indent--)
-		padding += "  ";
-	stream << "(false /** is there a common bit in " << a << " and " << b << " */" << std::endl;
-	for (size_t i = 0; i < length; i++) {
-		stream << padding << " || " << a << "[" << i << "] & "<< b << "[" << i << "]" << std::endl;
-	}
-	stream << padding << ")";
+void ChartToPromela::writeBitClearMacro(std::ostream& stream) {
+    stream << "/** clearing all bits of a */" << std::endl;
+    stream << "#define " << _prefix << "TRANS_CLEAR(a) \\" << std::endl;
+    for (size_t i = 0; i < _transitions.size(); i++) {
+        stream << "a[" << i << "] = false; \\" << std::endl;
+    }
+    stream << std::endl;
 
+    stream << "#define " << _prefix << "STATES_CLEAR(a) \\" << std::endl;
+    for (size_t i = 0; i < _states.size(); i++) {
+        stream << "a[" << i << "] = false; \\" << std::endl;
+    }
+    stream << std::endl;
+    
 }
 
 void ChartToPromela::printBitArray(std::ostream& stream,
@@ -411,46 +463,45 @@ void ChartToPromela::printBitArray(std::ostream& stream,
 
 void ChartToPromela::writeMacros(std::ostream& stream) {
 	stream << "/* machine state flags */" << std::endl;
-	stream << "#define USCXML_CTX_PRISTINE       0" << std::endl;
-	stream << "#define USCXML_CTX_SPONTANEOUS    1" << std::endl;
-	stream << "#define USCXML_CTX_INITIALIZED    2" << std::endl;
-	stream << "#define USCXML_CTX_TOP_LEVEL_FINAL  3" << std::endl;
-	stream << "#define USCXML_CTX_TRANSITION_FOUND   4" << std::endl;
-	stream << "#define USCXML_CTX_FINISHED       5" << std::endl;
+	stream << "#define USCXML_CTX_PRISTINE          0 /* can be out-factored */" << std::endl;
+	stream << "#define USCXML_CTX_SPONTANEOUS       1" << std::endl;
+	stream << "#define USCXML_CTX_TOP_LEVEL_FINAL   2" << std::endl;
+	stream << "#define USCXML_CTX_TRANSITION_FOUND  3" << std::endl;
+    stream << "#define USCXML_CTX_FINISHED          4" << std::endl;
+    stream << "#define USCXML_CTX_DEQUEUE_EXTERNAL  5" << std::endl;
 	stream << std::endl;
 
-	stream << "#define USCXML_TRANS_SPONTANEOUS    0" << std::endl;
-	stream << "#define USCXML_TRANS_TARGETLESS     1" << std::endl;
-	stream << "#define USCXML_TRANS_INTERNAL     2" << std::endl;
-	stream << "#define USCXML_TRANS_HISTORY      3" << std::endl;
-	stream << "#define USCXML_TRANS_INITIAL      4" << std::endl;
+	stream << "#define USCXML_TRANS_SPONTANEOUS     0" << std::endl;
+	stream << "#define USCXML_TRANS_TARGETLESS      1" << std::endl;
+	stream << "#define USCXML_TRANS_INTERNAL        2" << std::endl;
+	stream << "#define USCXML_TRANS_HISTORY         3" << std::endl;
+	stream << "#define USCXML_TRANS_INITIAL         4" << std::endl;
 	stream << std::endl;
 
-	stream << "#define USCXML_STATE_ATOMIC       0" << std::endl;
-	stream << "#define USCXML_STATE_PARALLEL     1" << std::endl;
-	stream << "#define USCXML_STATE_COMPOUND     2" << std::endl;
-	stream << "#define USCXML_STATE_FINAL      3" << std::endl;
-	stream << "#define USCXML_STATE_HISTORY_DEEP   4" << std::endl;
-	stream << "#define USCXML_STATE_HISTORY_SHALLOW  5" << std::endl;
-	stream << "#define USCXML_STATE_INITIAL      6" << std::endl;
-	stream << "#define USCXML_STATE_HAS_HISTORY    7" << std::endl;
+	stream << "#define USCXML_STATE_ATOMIC          0" << std::endl;
+	stream << "#define USCXML_STATE_PARALLEL        1" << std::endl;
+	stream << "#define USCXML_STATE_COMPOUND        2" << std::endl;
+	stream << "#define USCXML_STATE_FINAL           3" << std::endl;
+	stream << "#define USCXML_STATE_HISTORY_DEEP    4" << std::endl;
+	stream << "#define USCXML_STATE_HISTORY_SHALLOW 5" << std::endl;
+	stream << "#define USCXML_STATE_INITIAL         6" << std::endl;
+	stream << "#define USCXML_STATE_HAS_HISTORY     7" << std::endl;
 	stream << std::endl;
 
-	stream << "#define USCXML_ERR_OK         0" << std::endl;
-	stream << "#define USCXML_ERR_DONE         1" << std::endl;
+	stream << "#define USCXML_ERR_OK                0" << std::endl;
+	stream << "#define USCXML_ERR_DONE              1" << std::endl;
 	stream << std::endl;
 
-	stream << "#define USCXML_EVENT_SPONTANEOUS    0" << std::endl;
+	stream << "#define USCXML_EVENT_SPONTANEOUS     0" << std::endl;
 	stream << std::endl;
-	stream << "#define TRACE_EXECUTION    1" << std::endl;
+	stream << "#define TRACE_EXECUTION              1" << std::endl;
 	stream << std::endl;
 
-
 }
 
-void ChartToPromela::writeTypeDefs(std::ostream& stream) {
-    stream << "/* type definitions */" << std::endl;
-    PromelaCodeAnalyzer::PromelaTypedef typeDefs = _analyzer.getTypes();
+void ChartToPromela::writeCommonTypeDefs(std::ostream& stream) {
+    stream << "/* common type definitions */" << std::endl;
+    PromelaCodeAnalyzer::PromelaTypedef typeDefs = _analyzer->getTypes();
     if (typeDefs.types.size() == 0)
         return;
     
@@ -477,23 +528,27 @@ void ChartToPromela::writeTypeDefs(std::ostream& stream) {
         
         stream << "typedef " << currDef.name << " {" << std::endl;
         if (currDef.name.compare("_event_t") ==0) {
-            if (_analyzer.usesEventField("delay")) {
+            if (_analyzer->usesEventField("delay")) {
                 // make sure delay is the first member for sorted enqueuing to work
-                stream << "  int delay;" << std::endl;
+                stream << "  " << declForRange("delay", 0, _analyzer->largestDelay, true) << ";" << std::endl;
 #if NEW_DELAY_RESHUFFLE
 #else
-                stream << "  int seqNr;" << std::endl;
+                stream << "  short seqNr;" << std::endl;
 #endif
             }
-            stream << "  int name;" << std::endl;
-            if (_analyzer.usesEventField("invokeid")) {
-                stream << "  int invokeid;" << std::endl;
+            stream << "  " << declForRange("name", 0, _analyzer->getTrie().lastIndex, true) << ";" << std::endl;
+            if (_analyzer->usesEventField("invokeid")) {
+                stream << "  " << declForRange("invokeid", 0, _machinesAll->size() + 1, true) << ";" << std::endl;
+            }
+            if (_analyzer->usesEventField("origin")) {
+                stream << "  " << declForRange("origin", 0, _machinesAll->size() + 1, true) << ";" << std::endl;
             }
         }
         for (std::map<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator tIter = currDef.types.begin(); tIter != currDef.types.end(); tIter++) {
             if (currDef.name.compare("_event_t") == 0 && (tIter->first.compare("name") == 0 ||
                                                           tIter->first.compare("seqNr") == 0 ||
                                                           tIter->first.compare("invokeid") == 0 ||
+                                                          tIter->first.compare("origin") == 0 ||
                                                           tIter->first.compare("delay") == 0)) { // special treatment for _event
                 continue;
             }
@@ -522,80 +577,103 @@ void ChartToPromela::writeTypeDefs(std::ostream& stream) {
     
 }
 
+void ChartToPromela::writeTypeDefs(std::ostream& stream) {
+    stream << "/* custom type definitions for " << _prefix << " */" << std::endl;
+
+}
+
+void ChartToPromela::writeCommonVariables(std::ostream& stream) {
+    stream << "hidden int tmpIndex;" << std::endl;
+    if (_analyzer->usesComplexEventStruct()) {
+        stream << "hidden _event_t tmpE;" << std::endl;
+    } else {
+        stream << "hidden int tmpE;" << std::endl;
+    }
+    
+    if (_analyzer->hasIndexLessLoops())
+        stream << "hidden int _index;             /* helper for indexless foreach loops */" << std::endl;
+    
+    if (_analyzer->usesEventField("sendid"))
+        stream << "hidden int _lastSendId = 0;         /* sequential counter for send ids */" << std::endl;
+    
+    if (_analyzer->usesEventField("delay"))
+        stream << "hidden short _lastSeqId = 0;     /* sequential counter for delayed events */"  << std::endl;
+    stream << std::endl;
+
+}
 
-void ChartToPromela::writeTypes(std::ostream& stream) {
-	stream << "/* type definitions and global variables */" << std::endl;
+void ChartToPromela::writeVariables(std::ostream& stream) {
+	stream << "/* custom definitions and global variables */" << std::endl;
 	stream << "bool " << _prefix << "flags[6];" << std::endl;
 	stream << "bool " << _prefix << "config[" << _states.size() << "];" << std::endl;
 	stream << "bool " << _prefix << "history[" << _states.size() << "];" << std::endl;
 	stream << "bool " << _prefix << "invocations[" << _states.size() << "];" << std::endl;
-	stream << "bool " << _prefix << "initialized_data[" << _states.size() << "];" << std::endl;
+//	stream << "bool " << _prefix << "initialized_data[" << _states.size() << "];" << std::endl;
 	
     size_t tolerance = 6;
 
-    if (_analyzer.usesComplexEventStruct()) {
+    if (_analyzer->usesComplexEventStruct()) {
         // event is defined with the typedefs
-        stream << "_event_t " << _prefix << "_event;               /* current event */" << std::endl;
+        stream << "hidden _event_t " << _prefix << "_event;               /* current event */" << std::endl;
+        stream << "hidden _event_t " << _prefix << "_tmpE;          /* temporary event for send */" << std::endl;
         stream << "chan " << _prefix << "iQ   = [" << (std::max)(_internalQueueLength, (size_t)1) << "] of {_event_t}  /* internal queue */" << std::endl;
         stream << "chan " << _prefix << "eQ   = [" << _externalQueueLength + tolerance << "] of {_event_t}  /* external queue */" << std::endl;
         if (_allowEventInterleaving)
             stream << "chan " << _prefix << "tmpQ = [" << (std::max)(_externalQueueLength + tolerance, (size_t)1) << "] of {_event_t}  /* temporary queue for external events in transitions */" << std::endl;
     } else {
-        stream << "unsigned " << _prefix << "_event : " << BIT_WIDTH(_analyzer.getLiterals().size() + 1) << ";                /* current event */" << std::endl;
+        stream << "unsigned " << _prefix << "_event : " << BIT_WIDTH(_analyzer->getLiterals().size() + 1) << ";                /* current event */" << std::endl;
+        stream << "hidden unsigned " << _prefix << "_tmpE : " << BIT_WIDTH(_analyzer->getLiterals().size() + 1) << ";         /* temporary event for send */" << std::endl;
         stream << "chan " << _prefix << "iQ   = [" << (std::max)(_internalQueueLength, (size_t)1) << "] of {int}  /* internal queue */" << std::endl;
         stream << "chan " << _prefix << "eQ   = [" << _externalQueueLength + tolerance << "] of {int}  /* external queue */" << std::endl;
         if (_allowEventInterleaving)
             stream << "chan " << _prefix << "tmpQ = [" << (std::max)(_externalQueueLength + tolerance, (size_t)1) << "] of {int}  /* temporary queue for external events in transitions */" << std::endl;
     }
 
-	stream << std::endl;
-	stream << "typedef transition {" << std::endl;
-	stream << "  unsigned source : " << BIT_WIDTH(_states.size()) << ";" << std::endl;
-	stream << "  bool target[" << _states.size() << "];" << std::endl;
-	stream << "  bool type[5];" << std::endl;
-	stream << "  bool conflicts[" << _transitions.size() << "];" << std::endl;
-	stream << "  bool exit_set[" << _states.size() << "];" << std::endl;
-	stream << "}" << std::endl;
-	if (_transitions.size() > 0) {
-		stream << "hidden transition " << _prefix << "transitions[" << toStr(_transitions.size()) << "];" << std::endl;
+    if (_transitions.size() > 0) {
+        stream << std::endl;
+        stream << "typedef " << _prefix << "transition_t {" << std::endl;
+        stream << "  unsigned source : " << BIT_WIDTH(_states.size()) << ";" << std::endl;
+        stream << "  bool target[" << _states.size() << "];" << std::endl;
+        stream << "  bool type[5];" << std::endl;
+        stream << "  bool conflicts[" << _transitions.size() << "];" << std::endl;
+        stream << "  bool exit_set[" << _states.size() << "];" << std::endl;
+        stream << "}" << std::endl;
+		stream << "hidden " << _prefix << "transition_t " << _prefix << "transitions[" << toStr(_transitions.size()) << "];" << std::endl;
+        stream << std::endl;
 	}
-	stream << std::endl;
 
-	stream << "typedef state {" << std::endl;
-	stream << "  unsigned parent : " << BIT_WIDTH(_states.size()) << ";" << std::endl;
-	stream << "  bool children[" << _states.size() << "];" << std::endl;
-	stream << "  bool completion[" << _states.size() << "];" << std::endl;
-	stream << "  bool ancestors[" << _states.size() << "];" << std::endl;
-	stream << "  bool type[8];" << std::endl;
-	stream << "}" << std::endl;
-	if (_states.size() > 0) {
-		stream << "hidden state " << _prefix << "states[" << toStr(_states.size()) << "];" << std::endl;
+    if (_states.size() > 0) {
+        stream << "typedef " << _prefix << "state_t {" << std::endl;
+        stream << "  unsigned parent : " << BIT_WIDTH(_states.size()) << ";" << std::endl;
+        stream << "  bool children[" << _states.size() << "];" << std::endl;
+        stream << "  bool completion[" << _states.size() << "];" << std::endl;
+        stream << "  bool ancestors[" << _states.size() << "];" << std::endl;
+        stream << "  bool type[8];" << std::endl;
+        stream << "}" << std::endl;
+		stream << "hidden " << _prefix << "state_t " << _prefix << "states[" << toStr(_states.size()) << "];" << std::endl;
+        stream << std::endl;
 	}
-	stream << std::endl;
 
-    stream << "hidden int tmpIndex;" << std::endl;
-    if (_analyzer.usesComplexEventStruct()) {
-        stream << "hidden _event_t tmpE;" << std::endl;
-    } else {
-        stream << "hidden int tmpE;" << std::endl;
+    stream << "typedef " << _prefix << "ctx_t {" << std::endl;
+    if (_transitions.size() > 0) {
+        stream << "  bool conflicts[" << _transitions.size() << "];" << std::endl;
+        stream << "  bool trans_set[" << _transitions.size() << "];" << std::endl;
     }
-
-    if (_analyzer.hasIndexLessLoops())
-        stream << "hidden int " << _prefix << "_index;             /* helper for indexless foreach loops */" << std::endl;
-
-    if (_analyzer.usesEventField("sendid"))
-        stream << "hidden int _lastSendId = 0;         /* sequential counter for send ids */" << std::endl;
     
-    if (_analyzer.usesEventField("delay"))
-        stream << "hidden int _lastSeqId = 0;     /* sequential counter for delayed events */"  << std::endl;
-
+    stream << "  bool target_set[" << _states.size() << "];" << std::endl;
+    stream << "  bool exit_set[" << _states.size() << "];" << std::endl;
+    stream << "  bool entry_set[" << _states.size() << "];" << std::endl;
+    stream << "  bool tmp_states[" << _states.size() << "];" << std::endl;
+    stream << "}" << std::endl;
+    stream << "hidden " << _prefix << "ctx_t " << _prefix << "ctx;" << std::endl;
+    stream << std::endl;
     stream << std::endl;
 
 	std::set<std::string> processedIdentifiers;
 
 	// automatic types
 	std::list<DOMElement*> datas = DOMUtils::inDocumentOrder({ XML_PREFIX(_scxml).str() + "data" }, _scxml, false);
-	PromelaCodeAnalyzer::PromelaTypedef allTypes = _analyzer.getTypes();
+	PromelaCodeAnalyzer::PromelaTypedef allTypes = _analyzer->getTypes();
 
 	for (auto data : datas) {
 		std::string identifier = (HAS_ATTR_CAST(data, "id") ? ATTR_CAST(data, "id") : "");
@@ -665,24 +743,40 @@ void ChartToPromela::writeTypes(std::ostream& stream) {
 		typeIter++;
 	}
 
+    if (_analyzer->getTypes().types.find("_ioprocessors") != _analyzer->getTypes().types.end()) {
+        stream << "hidden _ioprocessors_t " << _prefix << "_ioprocessors;" << std::endl;
+        _varInitializers.push_front("_ioprocessors.scxml.location = " + (_invokerid.size() > 0 ? _analyzer->macroForLiteral(_invokerid) : "1") + ";");
+    }
+
+    stream << "hidden int " << _prefix << "procid;             /* the process id running this machine */" << std::endl;
+
 }
 
+    
 void ChartToPromela::writeStrings(std::ostream& stream) {
     stream << "/* states, events and string literals */" << std::endl;
-    std::set<std::string> literals = _analyzer.getLiterals();
+    std::set<std::string> literals = _analyzer->getLiterals();
     
     {
         for (size_t i = 0; i < _states.size(); i++) {
             if (HAS_ATTR(_states[i], "id")) {
-                stream << "#define " << _prefix << _analyzer.macroForLiteral(ATTR(_states[i], "id")) << " " << toStr(i);
+                stream << "#define " << _prefix << _analyzer->macroForLiteral(ATTR(_states[i], "id")) << " " << toStr(i);
                 stream << " /* index for state " << ATTR(_states[i], "id") << " */" << std::endl;
             }
         }
     }
 
+    {
+        size_t i = 0;
+        for (auto machine : *_machinesAll) {
+            i++;
+            stream << "#define " << _analyzer->macroForLiteral(machine.second->_invokerid) << " " << toStr(i);
+            stream << " /* index for invoker " << machine.second->_invokerid << " */" << std::endl;
+        }
+    }
     
     for (auto literal : literals) {
-        stream << "#define " << _analyzer.macroForLiteral(literal) << " " << _analyzer.indexForLiteral(literal) << " /* " << literal << " */" << std::endl;
+        stream << "#define " << _analyzer->macroForLiteral(literal) << " " << _analyzer->indexForLiteral(literal) << " /* " << literal << " */" << std::endl;
     }
 }
 
@@ -703,19 +797,6 @@ void ChartToPromela::writeTransitions(std::ostream& stream) {
 					stream << "  " << _prefix << "transitions[" << toStr(i) << "].target[" << toStr(j) << "] = 1;" << std::endl;
 			}
 		}
-
-#if 0
-        /** events */
-		if (HAS_ATTR(transition, "event")) {
-			std::list<std::string> events = tokenize(ATTR(transition, "event"), ' ', true);
-			for(auto& event : events) {
-				auto trieNodes = _analyzer.getTrie().getWordsWithPrefix(event);
-				for(auto trieNode : trieNodes) {
-					stream << "  " << _prefix << "transitions[" << toStr(i) << "].event[" << _analyzer.macroForLiteral(trieNode->value) << "] = 1;" << std::endl;
-				}
-			}
-		}
-#endif
         
 		if (!HAS_ATTR(transition, "event"))
 			stream << "  " << _prefix << "transitions[" << toStr(i) << "].type[USCXML_TRANS_SPONTANEOUS] = 1;" << std::endl;
@@ -816,10 +897,65 @@ void ChartToPromela::writeStates(std::ostream& stream) {
 	}
 }
 
+void ChartToPromela::writeRaiseDoneDate(std::ostream& stream, const DOMElement* donedata, size_t indent) {
+    std::string padding;
+    for (size_t i = 0; i < indent; i++) {
+        padding += "  ";
+    }
 
-void ChartToPromela::writeHelpers(std::ostream& stream) {
-
+    std::list<DOMElement*> contents = DOMUtils::filterChildElements(XML_PREFIX(donedata).str() + "content", donedata);
+    if (contents.size() > 0) {
+        auto& content = contents.front();
+        
+        // an expression
+        if (HAS_ATTR(content, "expr")) {
+            stream << dataToAssignments(_prefix + "_tmpE.data", Data(ADAPT_SRC(ATTR(content, "expr")), Data::INTERPRETED));
+            return;
+        }
+        
+        std::list<DOMNode*> textChilds = DOMUtils::filterChildType(DOMNode::TEXT_NODE, content);
+        std::stringstream ss;
+        for (auto text : textChilds) {
+            ss << X(text->getNodeValue()).str();
+        }
+        
+        // text childs
+        std::string value = boost::trim_copy(ss.str());
+        if (value.size() > 0) {
+            Data d = Data::fromJSON(value);
+            if (!d.empty()) {
+                stream << dataToAssignments(_prefix + "_tmpE.data", d);
+            } else {
+                if (!isNumeric(value.c_str(), 10)) {
+                    stream << dataToAssignments(_prefix + "_tmpE.data", Data(value, Data::VERBATIM));
+                } else {
+                    stream << dataToAssignments(_prefix + "_tmpE.data", Data(value, Data::INTERPRETED));
+                }
+            }
+            return;
+        }
+    }
+    
+    std::list<DOMElement*> params = DOMUtils::filterChildElements(XML_PREFIX(donedata).str() + "param", donedata);
+    if (params.size() > 0) {
+        Data d;
+        for (auto& param : params) {
+            if (!HAS_ATTR(param, "name"))
+                continue;
+            std::string name = ATTR(param, "name");
+            std::string expr;
+            if (HAS_ATTR(param, "expr")) {
+                expr = ATTR(param, "expr");
+            } else if (HAS_ATTR(param, "location")) {
+                expr = ATTR(param, "location");
+            }
+            
+            d[name] = Data(expr, Data::INTERPRETED);
+        }
+        stream << dataToAssignments(_prefix + "_tmpE.data", d);
 
+    }
+    
 }
 
 void ChartToPromela::writeExecContent(std::ostream& stream, const XERCESC_NS::DOMNode* node, size_t indent) {
@@ -890,9 +1026,9 @@ void ChartToPromela::writeExecContent(std::ostream& stream, const XERCESC_NS::DO
 		}
 
 	} else if(TAGNAME(element) == "foreach") {
-		stream << padding << "for (" << _prefix << (HAS_ATTR(element, "index") ? ATTR(element, "index") : "_index") << " in " << _prefix << ATTR(element, "array") << ") {" << std::endl;
+		stream << padding << "for (" << (HAS_ATTR(element, "index") ? _prefix + ATTR(element, "index") : "_index") << " in " << _prefix << ATTR(element, "array") << ") {" << std::endl;
 		if (HAS_ATTR(element, "item")) {
-			stream << padding << "  " << _prefix << ATTR(element, "item") << " = " << _prefix << ATTR(element, "array") << "[" << _prefix << (HAS_ATTR(element, "index") ? ATTR(element, "index") : "_index") << "];" << std::endl;
+			stream << padding << "  " << _prefix << ATTR(element, "item") << " = " << _prefix << ATTR(element, "array") << "[" << (HAS_ATTR(element, "index") ? _prefix + ATTR(element, "index") : "_index") << "];" << std::endl;
 		}
 		const XERCESC_NS::DOMNode* child = element->getFirstChild();
 		while(child) {
@@ -916,10 +1052,15 @@ void ChartToPromela::writeExecContent(std::ostream& stream, const XERCESC_NS::DO
         
         std::list<DOMNode*> assignTexts = DOMUtils::filterChildType(DOMNode::TEXT_NODE, element, true);
         assert(assignTexts.size() > 0);
-        stream << beautifyIndentation(ADAPT_SRC(boost::trim_copy(X(assignTexts.front()->getNodeValue()).str())), indent) << std::endl;
+        stream << beautifyIndentation(ADAPT_SRC(boost::trim_copy(X(assignTexts.front()->getNodeValue()).str())), indent + 1) << std::endl;
         
 	} else if(TAGNAME(element) == "send" || TAGNAME(element) == "raise") {
 		std::string targetQueue;
+        
+        stream << padding << "if" << std::endl;
+        stream << padding << ":: !" << _prefix << "flags[USCXML_CTX_FINISHED] || " << _prefix << "flags[USCXML_CTX_TOP_LEVEL_FINAL] -> {" << std::endl;
+
+        padding += "  ";
 		std::string insertOp = "!";
 		if (TAGNAME(element) == "raise") {
 			targetQueue = _prefix + "iQ";
@@ -933,67 +1074,71 @@ void ChartToPromela::writeExecContent(std::ostream& stream, const XERCESC_NS::DO
 			targetQueue = _prefix + "iQ";
 		} else if (ATTR(element, "target").compare("#_parent") == 0) {
 			targetQueue = _parent->_prefix + "eQ";
-		} else if (boost::starts_with(ATTR(element, "target"), "#_") && _machinesPerId.find(ATTR(element, "target").substr(2)) != _machinesPerId.end()) {
-			targetQueue = _machines[_machinesPerId[ATTR(element, "target").substr(2)]]->_prefix + "eQ";
+		} else if (boost::starts_with(ATTR(element, "target"), "#_") && _machinesAllPerId->find(ATTR(element, "target").substr(2)) != _machinesAllPerId->end()) {
+			targetQueue = (*_machinesAll)[(*_machinesAllPerId)[ATTR(element, "target").substr(2)]]->_prefix + "eQ";
 		}
 		if (targetQueue.length() > 0) {
 			// this is for our external queue
 			std::string event;
 
 			if (HAS_ATTR(element, "event")) {
-				event = _analyzer.macroForLiteral(ATTR(element, "event"));
+				event = _analyzer->macroForLiteral(ATTR(element, "event"));
 			} else if (HAS_ATTR(element, "eventexpr")) {
 				event = ADAPT_SRC(ATTR(element, "eventexpr"));
 			}
-			if (_analyzer.usesComplexEventStruct()) {
+			if (_analyzer->usesComplexEventStruct()) {
 				stream << padding << "{" << std::endl;
-				std::string typeReset = _analyzer.getTypeReset(_prefix + "_event", _analyzer.getType("_event"), padding + "  ");
+				std::string typeReset = _analyzer->getTypeReset(_prefix + "_tmpE", _analyzer->getType("_event"), indent + 2);
 				std::stringstream typeAssignSS;
-				typeAssignSS << padding << "  " << _prefix << EVENT_NAME << " = " << event << ";" << std::endl;
+				typeAssignSS << padding << "  " << _prefix << "_tmpE.name = " << event << ";" << std::endl;
 
 				if (HAS_ATTR(element, "idlocation")) {
 					typeAssignSS << padding << "  /* idlocation */" << std::endl;
 					typeAssignSS << padding << "  _lastSendId = _lastSendId + 1;" << std::endl;
 					typeAssignSS << padding << "  " << _prefix << ATTR(element, "idlocation") << " = _lastSendId;" << std::endl;
-					typeAssignSS << padding << "  " << _prefix << "_event.sendid = _lastSendId;" << std::endl;
+					typeAssignSS << padding << "  " << _prefix << "_tmpE.sendid = _lastSendId;" << std::endl;
 					typeAssignSS << padding << "  if" << std::endl;
 					typeAssignSS << padding << "  :: _lastSendId == 2147483647 -> _lastSendId = 0;" << std::endl;
 					typeAssignSS << padding << "  :: else -> skip;" << std::endl;
 					typeAssignSS << padding << "  fi;" << std::endl;
 				} else if (HAS_ATTR(element, "id")) {
-					typeAssignSS << padding << "  " << _prefix << "_event.sendid = " << _analyzer.macroForLiteral(ATTR(element, "id")) << ";" << std::endl;
+					typeAssignSS << padding << "  " << _prefix << "_tmpE.sendid = " << _analyzer->macroForLiteral(ATTR(element, "id")) << ";" << std::endl;
 				}
 
-				if (_invokerid.length() > 0) { // do not send invokeid if we send / raise to ourself
-					typeAssignSS << padding << "  " << _prefix << "_event.invokeid = " << _analyzer.macroForLiteral(_invokerid) << ";" << std::endl;
+				if (_analyzer->usesEventField("invokeid") && _parent != NULL) { // do not send invokeid if we send / raise to ourself
+					typeAssignSS << padding << "  " << _prefix << "_tmpE.invokeid = " << _analyzer->macroForLiteral(_invokerid) << ";" << std::endl;
 				}
 
-				if (_analyzer.usesEventField("origintype") && !boost::ends_with(targetQueue, "iQ")) {
-					typeAssignSS << padding << "  " << _prefix << "_event.origintype = " << _analyzer.macroForLiteral("http://www.w3.org/TR/scxml/#SCXMLEventProcessor") << ";" << std::endl;
+				if (_analyzer->usesEventField("origintype") && !boost::ends_with(targetQueue, "iQ")) {
+					typeAssignSS << padding << "  " << _prefix << "_tmpE.origintype = " << _analyzer->macroForLiteral("http://www.w3.org/TR/scxml/#SCXMLEventProcessor") << ";" << std::endl;
 				}
+                
+                if (_analyzer->usesEventField("origin") && !boost::ends_with(targetQueue, "iQ")) {
+                    typeAssignSS << padding << "  " << _prefix << "_tmpE.origin = " << _analyzer->macroForLiteral(_invokerid) << ";" << std::endl;
+                }
 
-				if (_analyzer.usesEventField("delay")) {
+                if (_analyzer->usesEventField("delay")) {
 #if NEW_DELAY_RESHUFFLE
 #else
-					insertOp += "!";
+//					insertOp += "!";
 					typeAssignSS << padding << "  _lastSeqId = _lastSeqId + 1;" << std::endl;
 #endif
 					if (HAS_ATTR_CAST(element, "delay")) {
-						typeAssignSS << padding << "  " << _prefix << "_event.delay = " << ATTR_CAST(element, "delay") << ";" << std::endl;
+						typeAssignSS << padding << "  " << _prefix << "_tmpE.delay = " << ATTR_CAST(element, "delay") << ";" << std::endl;
 					} else if (HAS_ATTR_CAST(element, "delayexpr")) {
-						typeAssignSS << padding << "  " << _prefix << "_event.delay = " << ADAPT_SRC(ATTR_CAST(element, "delayexpr")) << ";" << std::endl;
+						typeAssignSS << padding << "  " << _prefix << "_tmpE.delay = " << ADAPT_SRC(ATTR_CAST(element, "delayexpr")) << ";" << std::endl;
 					} else {
-						typeAssignSS << padding << "  " << _prefix << "_event.delay = 0;" << std::endl;
+						typeAssignSS << padding << "  " << _prefix << "_tmpE.delay = 0;" << std::endl;
 					}
 #if NEW_DELAY_RESHUFFLE
 #else
-					typeAssignSS << padding << "  " << _prefix << "_event.seqNr = _lastSeqId;" << std::endl;
+					typeAssignSS << padding << "  " << _prefix << "_tmpE.seqNr = _lastSeqId;" << std::endl;
 #endif
 				}
 
-				if (_analyzer.usesEventField("type")) {
-					std::string eventType = (targetQueue.compare("iQ!") == 0 ? _analyzer.macroForLiteral("internal") : _analyzer.macroForLiteral("external"));
-					typeAssignSS << padding << "  " << _prefix << "_event.type = " << eventType << ";" << std::endl;
+				if (_analyzer->usesEventField("type")) {
+					std::string eventType = (targetQueue.compare("iQ!") == 0 ? _analyzer->macroForLiteral("internal") : _analyzer->macroForLiteral("external"));
+					typeAssignSS << padding << "  " << _prefix << "_tmpE.type = " << eventType << ";" << std::endl;
 				}
 
 				std::list<DOMElement*> sendParams = DOMUtils::filterChildElements(XML_PREFIX(element).str() + "param", element);
@@ -1001,14 +1146,14 @@ void ChartToPromela::writeExecContent(std::ostream& stream, const XERCESC_NS::DO
 				std::string sendNameList = ATTR(element, "namelist");
 				if (sendParams.size() > 0) {
 					for (auto sendParam : sendParams) {
-						typeAssignSS << padding << "  " << _prefix << "_event.data." << ATTR(sendParam, "name") << " = " << ADAPT_SRC(ATTR(sendParam, "expr"))  << ";" << std::endl;
+						typeAssignSS << padding << "  " << _prefix << "_tmpE.data." << ATTR(sendParam, "name") << " = " << ADAPT_SRC(ATTR(sendParam, "expr"))  << ";" << std::endl;
 					}
 				}
 				if (sendNameList.size() > 0) {
 					std::list<std::string> nameListIds = tokenize(sendNameList);
 					std::list<std::string>::iterator nameIter = nameListIds.begin();
 					while(nameIter != nameListIds.end()) {
-						typeAssignSS << padding << "  " << _prefix << "_event.data." << *nameIter << " = " << ADAPT_SRC(*nameIter) << ";" << std::endl;
+						typeAssignSS << padding << "  " << _prefix << "_tmpE.data." << *nameIter << " = " << ADAPT_SRC(*nameIter) << ";" << std::endl;
 						nameIter++;
 					}
 				}
@@ -1018,12 +1163,12 @@ void ChartToPromela::writeExecContent(std::ostream& stream, const XERCESC_NS::DO
 					if (contentElem->hasChildNodes() && contentElem->getFirstChild()->getNodeType() == DOMNode::TEXT_NODE) {
 						std::string content = spaceNormalize(X(contentElem->getFirstChild()->getNodeValue()).str());
 						if (!isNumeric(content.c_str(), 10)) {
-							typeAssignSS << padding << "  " << _prefix << "_event.data = " << _analyzer.macroForLiteral(content) << ";" << std::endl;
+							typeAssignSS << padding << "  " << _prefix << "_tmpE.data = " << _analyzer->macroForLiteral(content) << ";" << std::endl;
 						} else {
-							typeAssignSS << padding << "  " << _prefix << "_event.data = " << content << ";" << std::endl;
+							typeAssignSS << padding << "  " << _prefix << "_tmpE.data = " << content << ";" << std::endl;
 						}
 					} else if (HAS_ATTR(contentElem, "expr")) {
-						typeAssignSS << padding << "  " << _prefix << "_event.data = " << ADAPT_SRC(ATTR(contentElem, "expr")) << ";" << std::endl;
+						typeAssignSS << padding << "  " << _prefix << "_tmpE.data = " << ADAPT_SRC(ATTR(contentElem, "expr")) << ";" << std::endl;
 					}
 				}
 
@@ -1053,563 +1198,584 @@ void ChartToPromela::writeExecContent(std::ostream& stream, const XERCESC_NS::DO
 				}
 				stream << typeAssignSS.str();
 
+                stream << "#if TRACE_EXECUTION" << std::endl;
+                if (_analyzer->usesComplexEventStruct()) {
+                    stream << "printf(\"%d: Sending " << event << " (%d) to " << targetQueue << "\\n\", _pid, " << _prefix << TMP_EVENT_NAME << " );" << std::endl;
+                } else {
+                    stream << "printf(\"Sending " << event << " (%d) to " << targetQueue << "\\n\", " << _prefix << TMP_EVENT_NAME << " );" << std::endl;
+                }
+                stream << "#endif" << std::endl;
+                stream << std::endl;
 
-				stream << padding << "  " << targetQueue << insertOp << _prefix <<"_event;" << std::endl;
+				stream << padding << "  " << targetQueue << insertOp << _prefix <<"_tmpE;" << std::endl;
 
-#if NEW_DELAY_RESHUFFLE
 				if (_analyzer->usesEventField("delay") && !boost::ends_with(targetQueue, "iQ")) {
 					stream << padding << "  insertWithDelay(" << targetQueue << ");" << std::endl;
 				}
-#endif
 
 				stream << padding << "}" << std::endl;
 			} else {
 				stream << padding << targetQueue << insertOp << event << ";" << std::endl;
 			}
 		}
+        stream << padding << "skip;" << std::endl;
+
+        padding = padding.substr(0, padding.size() - 2);
+        stream << padding << "}" << std::endl;
+        stream << padding << ":: else -> skip;" << std::endl;
+        stream << padding << "fi" << std::endl;
+
 	} else if(TAGNAME(element) == "cancel") {
 		if (HAS_ATTR(element, "sendid")) {
-			stream << padding << "cancelSendId(" << _analyzer.macroForLiteral(ATTR(element, "sendid")) << ", " << (_invokerid.size() > 0 ? _analyzer.macroForLiteral(_invokerid) : "0") << ");" << std::endl;
+			stream << "  " << padding << "cancelSendId(" << _analyzer->macroForLiteral(ATTR(element, "sendid")) << "," << _analyzer->macroForLiteral(_invokerid) << ");" << std::endl;
 		} else if (HAS_ATTR(element, "sendidexpr")) {
-			stream << padding << "cancelSendId(" << ADAPT_SRC(ATTR(element, "sendidexpr")) << ", " << (_invokerid.size() > 0 ? _analyzer.macroForLiteral(_invokerid) : "0") << ");" << std::endl;
+			stream << "  " << padding << "cancelSendId(" << ADAPT_SRC(ATTR(element, "sendidexpr")) << "," << _analyzer->macroForLiteral(_invokerid) << ");" << std::endl;
 		}
 	} else {
 		std::cerr << "'" << TAGNAME(element) << "' not supported" << std::endl << element << std::endl;
 		assert(false);
 	}
-
-
 }
 
 
 
 void ChartToPromela::writeFSM(std::ostream& stream) {
 	stream << "/* machine microstep function */" << std::endl;
-	stream << "#define USCXML_NUMBER_STATES " << _states.size() << std::endl;
-	stream << "#define USCXML_NUMBER_TRANS " << _transitions.size() << std::endl;
+	stream << "#define " << _prefix << "USCXML_NUMBER_STATES " << _states.size() << std::endl;
+	stream << "#define " << _prefix << "USCXML_NUMBER_TRANS " << _transitions.size() << std::endl;
+    stream << std::endl;
 
 	stream << "proctype " << _prefix << "step() { atomic {" << std::endl;
-	stream << std::endl;
+    stream << std::endl;
+    stream << _prefix << "procid = _pid;" << std::endl;
+
+    size_t largestBitWidth = (_states.size() > _transitions.size() ?
+                              BIT_WIDTH(_states.size() + 1) :
+                              BIT_WIDTH(_transitions.size() + 1));
+    
+    stream << "unsigned";
+    stream << " i : " <<  largestBitWidth << ", ";
+    stream << " j : " <<  largestBitWidth << ", ";
+    stream << " k : " <<  largestBitWidth << ";" << std::endl;
+    stream << std::endl;
+    
+    std::list<DOMElement*> globalScripts = DOMUtils::filterChildElements(XML_PREFIX(_scxml).str() + "script", _scxml, false);
+    if (globalScripts.size() > 0) {
+        stream << "/* run global scripts */" << std::endl;
+        for (auto globalScript : globalScripts) {
+            TRACE_EXECUTION("Processing executable content for global script");
+            
+            writeExecContent(stream, globalScript, 2);
+        }
+        stream << std::endl;
+    }
+    
+    stream << std::endl;
     stream << "/* ---------------------------- */" << std::endl;
-	stream << "MICROSTEP:" << std::endl;
+    stream << _prefix << "MICROSTEP:" << std::endl;
 
 	stream << "do" << std::endl;
 	stream << ":: !" << _prefix << "flags[USCXML_CTX_FINISHED] -> {" << std::endl;
-	stream << std::endl;
-
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Taking a step\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-
-
-	size_t largestBitWidth = (_states.size() > _transitions.size() ?
-	                          BIT_WIDTH(_states.size() + 1) :
-	                          BIT_WIDTH(_transitions.size() + 1));
-    
-	stream << "  unsigned";
-	stream << " i : " <<  largestBitWidth << ", ";
-	stream << " j : " <<  largestBitWidth << ", ";
-	stream << " k : " <<  largestBitWidth << ";" << std::endl;
-
-	stream << "  int err = USCXML_ERR_OK;" << std::endl;
-
-	stream << "  bool conflicts[" << _transitions.size() << "];" << std::endl;
-	stream << "  bool trans_set[" << _transitions.size() << "];" << std::endl;
+    stream << "  /* Run until machine is finished */" << std::endl;
+    stream << std::endl;
 
-	stream << "  bool target_set[" << _states.size() << "];" << std::endl;
-	stream << "  bool exit_set[" << _states.size() << "];" << std::endl;
-	stream << "  bool entry_set[" << _states.size() << "];" << std::endl;
-	stream << "  bool tmp_states[" << _states.size() << "];" << std::endl;
-	stream << std::endl;
+    TRACE_EXECUTION("Taking a step");
 
-#if 0
+    stream << "  /* Dequeue an event */" << std::endl;
+    stream << "  " << _prefix << "flags[USCXML_CTX_DEQUEUE_EXTERNAL] = false;" << std::endl;
 	stream << "  if" << std::endl;
-	stream << "  :: " << _prefix << "flags[USCXML_CTX_FINISHED]" << std::endl;
-	stream << "  ACCEPT: {" << std::endl;
-	stream << "    false;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << "  :: else -> skip;" << std::endl;
-	stream << "  fi;" << std::endl;
-	stream << std::endl;
+	stream << "  ::" << _prefix << "flags[USCXML_CTX_SPONTANEOUS] -> {" << std::endl;
+	stream << "    " << _prefix << EVENT_NAME << " = USCXML_EVENT_SPONTANEOUS;" << std::endl;
 
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Machine not finished\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-#endif
+    TRACE_EXECUTION("Trying with a spontaneous event");
 
-#if 0
-	stream << "  if (ctx->flags & USCXML_CTX_TOP_LEVEL_FINAL) -> {" << std::endl;
-	stream << "    /* exit all remaining states */" << std::endl;
-	stream << "    i = USCXML_NUMBER_STATES;" << std::endl;
-	stream << "    while(i-- > 0) {" << std::endl;
-	stream << "      if (BIT_HAS(i, ctx->config)) {" << std::endl;
-	stream << "        /* call all on exit handlers */" << std::endl;
-	stream << "        if (USCXML_GET_STATE(i).on_exit != NULL) {" << std::endl;
-	stream << "          if unlikely((err = USCXML_GET_STATE(i).on_exit(ctx, &USCXML_GET_STATE(i), ctx->event)) != USCXML_ERR_OK)" << std::endl;
-	stream << "            return err;" << std::endl;
-	stream << "        }" << std::endl;
-	//	stream << "        BIT_CLEAR(i, ctx->config);" << std::endl;
-	stream << "      }" << std::endl;
-	stream << "      if (BIT_HAS(i, ctx->invocations)) {" << std::endl;
-	stream << "        if (USCXML_GET_STATE(i).invoke != NULL)" << std::endl;
-	stream << "          USCXML_GET_STATE(i).invoke(ctx, &USCXML_GET_STATE(i), NULL, 1);" << std::endl;
-	stream << "        BIT_CLEAR(i, ctx->invocations);" << std::endl;
-	stream << "      }" << std::endl;
-	stream << "    }" << std::endl;
-	stream << "    ctx->flags |= USCXML_CTX_FINISHED;" << std::endl;
-	stream << "    return USCXML_ERR_DONE;" << std::endl;
 	stream << "  }" << std::endl;
+    stream << "  :: else -> {" << std::endl;
+    stream << "    if" << std::endl;
+    stream << "    :: len(" << _prefix << "iQ) != 0 -> {" << std::endl;
+    stream << "      " << _prefix << "iQ ? " << _prefix << "_event;" << std::endl;
+    
+    TRACE_EXECUTION("Deqeued an internal event");
+    
+    stream << "    }" << std::endl;
+    stream << "    :: else -> {" << std::endl;
+    stream << "      " << _prefix << "flags[USCXML_CTX_DEQUEUE_EXTERNAL] = true;" << std::endl;
+    stream << "    }" << std::endl;
+    stream << "    fi;" << std::endl;
+    stream << "  }" << std::endl;
+	stream << "  fi;" << std::endl;
 	stream << std::endl;
 
-#endif
+    stream << std::endl;
 
-	stream << "  if" << std::endl;
-	stream << "  ::" << _prefix << "flags[USCXML_CTX_TOP_LEVEL_FINAL] -> {" << std::endl;
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Top level final state reached\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-	stream << "    /* exit all remaining states */" << std::endl;
-	stream << "    i = USCXML_NUMBER_STATES;" << std::endl;
+    stream << "  if" << std::endl;
+    stream << "  :: " << _prefix << "flags[USCXML_CTX_DEQUEUE_EXTERNAL] -> {" << std::endl;
+	stream << "    /* manage invocations */" << std::endl;
+	stream << "    i = 0;" << std::endl;
 	stream << "    do" << std::endl;
-	stream << "    :: i > 0 -> {" << std::endl;
-	stream << "      i = i - 1;" << std::endl;
+	stream << "    :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
+	stream << "      /* uninvoke */" << std::endl;
 	stream << "      if" << std::endl;
-	stream << "      :: " << _prefix << "config[i] -> {" << std::endl;
-	stream << "        /* TODO: call all on exit handlers */" << std::endl;
-	stream << "        skip;" << std::endl;
-	stream << "        " << std::endl;
+	stream << "      :: !" << _prefix << "config[i] && " << _prefix << "invocations[i] -> {" << std::endl;
+
+    TRACE_EXECUTION_V("Uninvoking in state %d", "i");
+
+    stream << "        if" << std::endl;
+
+    for (size_t i = 0; i < _states.size(); i++) {
+        std::list<DOMElement*> invokers = DOMUtils::filterChildElements(XML_PREFIX(_scxml).str() + "invoke" , _states[i]);
+        if (invokers.size() > 0) {
+            stream << "        :: i == " << toStr(i) << " -> {" << std::endl;
+            for (auto invokeElem : invokers) {
+                if (_machinesNested.find(invokeElem) == _machinesNested.end())
+                    continue;
+                ChartToPromela* invoker = _machinesNested[invokeElem];
+                stream << "          " << invoker->_prefix << "flags[USCXML_CTX_FINISHED] = true;" << std::endl;
+            }
+            stream << "        }" << std::endl;
+        }
+    }
+    stream << "        :: else -> skip;" << std::endl;
+    stream << "        fi" << std::endl;
+
+    stream << "        " << _prefix << "invocations[i] = false;" << std::endl;
+    
+    stream << "        skip;" << std::endl;
 	stream << "      }" << std::endl;
 	stream << "      :: else -> skip;" << std::endl;
 	stream << "      fi;" << std::endl;
 	stream << std::endl;
 
+    
+    
+	stream << "      /* invoke */" << std::endl;
 	stream << "      if" << std::endl;
-	stream << "      :: " << _prefix << "invocations[i] -> {" << std::endl;
-	stream << "        /* TODO: cancel invocations */" << std::endl;
-	stream << "        skip;" << std::endl;
-	stream << "        " << std::endl;
+	stream << "      :: " << _prefix << "config[i] && !" << _prefix << "invocations[i] -> {" << std::endl;
+    stream << "        if" << std::endl;
+    
+    for (size_t i = 0; i < _states.size(); i++) {
+        std::list<DOMElement*> invokers = DOMUtils::filterChildElements(XML_PREFIX(_scxml).str() + "invoke" , _states[i]);
+        if (invokers.size() > 0) {
+            stream << "      :: i == " << toStr(i) << " -> {" << std::endl;
+            for (auto invokeElem : invokers) {
+                if (_machinesNested.find(invokeElem) == _machinesNested.end())
+                    continue;
+                ChartToPromela* invoker = _machinesNested[invokeElem];
+                
+                // pass variables via namelist
+                if (HAS_ATTR(invokeElem, "namelist")) {
+                    std::list<std::string> namelist = tokenize(ATTR_CAST(invokeElem, "namelist"));
+                    for (auto name : namelist) {
+                        if (invoker->_dataModelVars.find(name) != invoker->_dataModelVars.end()) {
+                            stream << "          " << invoker->_prefix << name << " = " << _prefix << name << ";" << std::endl;
+                        }
+                    }
+                }
+                
+                // pass variables via params
+                std::list<DOMElement*> invokeParams = DOMUtils::filterChildElements(XML_PREFIX(_scxml).str() + + "param", invokeElem);
+                for (auto param : invokeParams) {
+                    std::string name = ATTR(param, "name");
+                    std::string expression = ATTR(param, "expr");
+                    if (invoker->_dataModelVars.find(name) != invoker->_dataModelVars.end()) {
+                        stream << "          " << invoker->_prefix << name << " = " << ADAPT_SRC(expression) << ";" << std::endl;
+                    }
+                }
+                
+                TRACE_EXECUTION_V("Invoking in state %d", "i");
+
+                stream << "          run " << invoker->_prefix << "step() priority 20;" << std::endl;
+                if (HAS_ATTR(invokeElem, "idlocation")) {
+                    stream << "          " << ADAPT_SRC(ATTR(invokeElem, "idlocation")) << " = ";
+                    stream << _analyzer->macroForLiteral(invoker->_invokerid) << ";" << std::endl;
+                }
+                
+            }
+            stream << "          " << _prefix << "invocations[i] = true;" << std::endl;
+            stream << "          skip;" << std::endl;
+            stream << "        }" << std::endl;
+        }
+    }
+    
+    stream << "        :: else -> skip;" << std::endl;
+    stream << "        fi" << std::endl;
 	stream << "      }" << std::endl;
 	stream << "      :: else -> skip;" << std::endl;
 	stream << "      fi;" << std::endl;
+	stream << "      i = i + 1;" << std::endl;
 	stream << "    }" << std::endl;
 	stream << "    :: else -> break;" << std::endl;
-	stream << "    od;" << std::endl;
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Ending machine!\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-	stream << "    " << _prefix << "flags[USCXML_CTX_FINISHED] = true;" << std::endl;
-	stream << "    goto MICROSTEP;" << std::endl;
-
-	stream << "  }" << std::endl;
-	stream << "  :: else -> skip;" << std::endl;
-	stream << "  fi;" << std::endl;
-	stream << std::endl;
-
-#if 0
-	stream << "  bit_clear_all(target_set, nr_states_bytes);" << std::endl;
-	stream << "  bit_clear_all(trans_set, nr_trans_bytes);" << std::endl;
-	stream << "  if unlikely(ctx->flags == USCXML_CTX_PRISTINE) {" << std::endl;
-	stream << "    if (ctx->machine->script != NULL)" << std::endl;
-	stream << "      ctx->machine->script(ctx, &ctx->machine->states[0], NULL);" << std::endl;
-	stream << "    bit_or(target_set, ctx->machine->states[0].completion, nr_states_bytes);" << std::endl;
-	stream << "    ctx->flags |= USCXML_CTX_SPONTANEOUS | USCXML_CTX_INITIALIZED;" << std::endl;
-	stream << "    goto ESTABLISH_ENTRY_SET;" << std::endl;
-	stream << "  }" << std::endl;
+    stream << "    od;" << std::endl;
 	stream << std::endl;
-#endif
 
-	stream << "  if" << std::endl;
-	stream << "  ::" << _prefix << "flags[USCXML_CTX_PRISTINE] -> {" << std::endl;
-	stream << "    /* run global scripts */" << std::endl;
-    
-    std::list<DOMElement*> globalScripts = DOMUtils::filterChildElements(XML_PREFIX(_scxml).str() + "script", _scxml, false);
-    for (auto globalScript : globalScripts) {
-        writeExecContent(stream, globalScript);
+    if (_analyzer->usesEventField("delay") && _machinesAll->size() > 1) {
+        stream << "    /* Determine machines with smallest delay and set their process priority */" << std::endl;
+        stream << "    scheduleMachines();" << std::endl << std::endl;
     }
-    stream << std::endl;
-
-	stream << "    /* Enter initial configuration */" << std::endl;
-	bit_copy(stream, _prefix + "states[0].completion", "target_set", _states.size(), 2);
-	stream << "    " << _prefix << "flags[USCXML_CTX_SPONTANEOUS] = true;" << std::endl;
-	stream << "    " << _prefix << "flags[USCXML_CTX_PRISTINE] = false;" << std::endl;
-
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Entering initial default completion\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-
-	stream << "    goto ESTABLISH_ENTRY_SET;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << "  :: else -> skip;" << std::endl;
-	stream << "  fi;" << std::endl;
-	stream << std::endl;
-
-
-#if 0
-	stream << "DEQUEUE_EVENT:" << std::endl;
-	stream << "  if (ctx->flags & USCXML_CTX_SPONTANEOUS) {" << std::endl;
-	stream << "    ctx->event = NULL;" << std::endl;
-	stream << "    goto SELECT_TRANSITIONS;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << "  if (ctx->dequeue_internal != NULL && (ctx->event = ctx->dequeue_internal(ctx)) != NULL) {" << std::endl;
-	stream << "    goto SELECT_TRANSITIONS;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << std::endl;
-#endif
-
-
-    stream << "/* ---------------------------- */" << std::endl;
-	stream << "DEQUEUE_EVENT:" << std::endl;
-	stream << "  if" << std::endl;
-	stream << "  ::" << _prefix << "flags[USCXML_CTX_SPONTANEOUS] -> {" << std::endl;
-	stream << "    " << _prefix << EVENT_NAME << " = USCXML_EVENT_SPONTANEOUS;" << std::endl;
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Trying with a spontaneuous event\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-	stream << "    goto SELECT_TRANSITIONS;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << "  :: else -> skip;" << std::endl;
-	stream << "  fi;" << std::endl;
-	stream << std::endl;
+    
+    stream << "    /* we may return to find ourselves terminated */" << std::endl;
+    stream << "    if" << std::endl;
+    stream << "    :: " << _prefix << "flags[USCXML_CTX_FINISHED] -> {" << std::endl;
+    stream << "      goto " << _prefix << "TERMINATE_MACHINE;" << std::endl;
+    stream << "    }" << std::endl;
+    stream << "    :: else -> skip;" << std::endl;
+    stream << "    fi" << std::endl;
 
-	stream << "  if" << std::endl;
-	stream << "  :: len(" << _prefix << "iQ) != 0 -> {" << std::endl;
-	stream << "    " << _prefix << "iQ ? " << _prefix << "_event;" << std::endl;
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Deqeued an internal event\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-	stream << "    goto SELECT_TRANSITIONS;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << "  :: else -> skip;" << std::endl;
-	stream << "  fi;" << std::endl;
+    
+    stream << "    /* Not sure if this should be before the invocation due to auto-forwarding */" << std::endl;
+	stream << "    if" << std::endl;
+	stream << "    :: len(" << _prefix << "eQ) != 0 -> {" << std::endl;
+	stream << "      " << _prefix << "eQ ? " << _prefix << "_event;" << std::endl;
+
+    if (_machinesNested.size() > 0) {
+        stream << std::endl;
+        stream << "      /* auto-forward event */" << std::endl;
+        stream << "      i = 0;" << std::endl;
+        stream << "      do" << std::endl;
+        stream << "      :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
+        stream << "        if" << std::endl;
+        
+        std::string insertOp = "!";
+        if (_analyzer->usesEventField("delay")) {
+//            insertOp += "!";
+        }
 
+        
+        for (auto state : _states) {
+            std::list<DOMElement*> invokers = DOMUtils::filterChildElements(XML_PREFIX(state).str() + "invoke", state, false);
+            if (invokers.size() > 0) {
+                stream << "        :: i == " << ATTR(state, "documentOrder") << " && " << _prefix << "invocations[i] -> { " << std::endl;
+                for (auto invoker : invokers) {
+                    assert(_machinesNested.find(invoker) != _machinesNested.end());
+                    if (HAS_ATTR(invoker, "autoforward") && stringIsTrue(ATTR(invoker, "autoforward"))) {
+                        stream << "          " << _machinesNested[invoker]->_prefix << "eQ " << insertOp << " " << _prefix << "_event;" << std::endl;
+                        if (_analyzer->usesEventField("delay")) {
+                            stream << "          insertWithDelay(" << _machinesNested[invoker]->_prefix << "eQ);" << std::endl;
+                        }
+                        TRACE_EXECUTION("Auto forwarded event");
+                    }
+                }
+                stream << "        skip;" << std::endl;
+                stream << "      }" << std::endl;
+            }
+        }
+        
+        stream << "        :: else -> skip;" << std::endl;
+        stream << "        fi" << std::endl;
+        stream << "        i = i + 1;" << std::endl;
+        stream << "      }" << std::endl;
+        stream << "      :: else -> break;" << std::endl;
+        stream << "      od" << std::endl;
 
-#if 0
-	stream << "  /* manage invocations */" << std::endl;
-	stream << "  for (i = 0; i < USCXML_NUMBER_STATES; i++) {" << std::endl;
-	stream << "    /* uninvoke */" << std::endl;
-	stream << "    if (!BIT_HAS(i, ctx->config) && BIT_HAS(i, ctx->invocations)) {" << std::endl;
-	stream << "      if (USCXML_GET_STATE(i).invoke != NULL)" << std::endl;
-	stream << "        USCXML_GET_STATE(i).invoke(ctx, &USCXML_GET_STATE(i), NULL, 1);" << std::endl;
-	stream << "      BIT_CLEAR(i, ctx->invocations)" << std::endl;
-	stream << "    }" << std::endl;
-	stream << "    /* invoke */" << std::endl;
-	stream << "    if (BIT_HAS(i, ctx->config) && !BIT_HAS(i, ctx->invocations)) {" << std::endl;
-	stream << "      if (USCXML_GET_STATE(i).invoke != NULL)" << std::endl;
-	stream << "        USCXML_GET_STATE(i).invoke(ctx, &USCXML_GET_STATE(i), NULL, 0);" << std::endl;
-	stream << "      BIT_SET_AT(i, ctx->invocations)" << std::endl;
-	stream << "    }" << std::endl;
-	stream << "  }" << std::endl;
-	stream << std::endl;
-#endif
+        stream << std::endl;
+        stream << "      /* finalize event */" << std::endl;
+        stream << "      if" << std::endl;
+        
+        for (auto machine : _machinesNested) {
+            
+            stream << "      :: " << _prefix << "_event.invokeid == " << _analyzer->macroForLiteral(machine.second->_invokerid) << " -> {" << std::endl;
+            std::list<DOMElement*> finalizers = DOMUtils::filterChildElements(XML_PREFIX(machine.first).str() + "finalize", machine.first, false);
+
+            TRACE_EXECUTION("Finalizing event")
+            
+            for (auto finalize : finalizers) {
+                writeExecContent(stream, finalize, 4);
+            }
+            stream << "        skip" << std::endl;
+            stream << "      }" << std::endl;
+        }
+        stream << "      :: else -> skip;" << std::endl;
+        
+        stream << "      fi" << std::endl;
 
-	stream << "  /* manage invocations */" << std::endl;
-	stream << "  i = 0;" << std::endl;
-	stream << "  do" << std::endl;
-	stream << "  :: i < USCXML_NUMBER_STATES -> {" << std::endl;
-	stream << "    /* uninvoke */" << std::endl;
-	stream << "    if" << std::endl;
-	stream << "    :: !" << _prefix << "config[i] && " << _prefix << "invocations[i] -> {" << std::endl;
-	stream << "      skip;" << std::endl;
-	stream << "    }" << std::endl;
-	stream << "    :: else -> skip;" << std::endl;
-	stream << "    fi;" << std::endl;
-	stream << std::endl;
+    }
+    
+    TRACE_EXECUTION("Deqeued an external event");
 
-	stream << "    /* invoke */" << std::endl;
-	stream << "    if" << std::endl;
-	stream << "    :: " << _prefix << "config[i] && !" << _prefix << "invocations[i] -> {" << std::endl;
-	stream << "      skip;" << std::endl;
 	stream << "    }" << std::endl;
-	stream << "    :: else -> skip;" << std::endl;
-	stream << "    fi;" << std::endl;
-	stream << "    i = i + 1;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << "  :: else -> break;" << std::endl;
-	stream << "  od;" << std::endl;
-	stream << std::endl;
-
-#if 0
-	stream << "  if (ctx->dequeue_external != NULL && (ctx->event = ctx->dequeue_external(ctx)) != NULL) {" << std::endl;
-	stream << "    goto SELECT_TRANSITIONS;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << std::endl;
-	stream << "  if (ctx->dequeue_external == NULL) {" << std::endl;
-	stream << "    return USCXML_ERR_DONE;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << "  return USCXML_ERR_IDLE;" << std::endl;
-	stream << std::endl;
-#endif
-
-	stream << "  if" << std::endl;
-	stream << "  :: len(" << _prefix << "eQ) != 0 -> {" << std::endl;
-	stream << "    " << _prefix << "eQ ? " << _prefix << "_event;" << std::endl;
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Deqeued an external event\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-	stream << "    goto SELECT_TRANSITIONS;" << std::endl;
-	stream << "  }" << std::endl;
 //  stream << "  :: else -> quit;" << std::endl;
-	stream << "  fi;" << std::endl;
-	stream << std::endl;
-
-#if 0
-	stream << "SELECT_TRANSITIONS:" << std::endl;
-	stream << "  bit_clear_all(conflicts, nr_trans_bytes);" << std::endl;
-    stream << "  bit_clear_all(exit_set, nr_states_bytes);" << std::endl;
-	stream << "  for (i = 0; i < USCXML_NUMBER_TRANS; i++) {" << std::endl;
-	stream << "    /* never select history or initial transitions automatically */" << std::endl;
-	stream << "    if unlikely(USCXML_GET_TRANS(i).type & (USCXML_TRANS_HISTORY | USCXML_TRANS_INITIAL))" << std::endl;
-	stream << "      continue;" << std::endl;
-	stream << std::endl;
-	stream << "    /* is the transition active? */" << std::endl;
-	stream << "    if (BIT_HAS(USCXML_GET_TRANS(i).source, ctx->config)) {" << std::endl;
-	stream << "      /* is it non-conflicting? */" << std::endl;
-	stream << "      if (!BIT_HAS(i, conflicts)) {" << std::endl;
-	stream << "        /* is it spontaneous with an event or vice versa? */" << std::endl;
-	stream << "        if ((USCXML_GET_TRANS(i).event == NULL && ctx->event == NULL) || " << std::endl;
-	stream << "          (USCXML_GET_TRANS(i).event != NULL && ctx->event != NULL)) {" << std::endl;
-	stream << "          /* is it enabled? */" << std::endl;
-	stream << "          if ((ctx->event == NULL || ctx->is_matched(ctx, &USCXML_GET_TRANS(i), ctx->event) > 0) &&" << std::endl;
-	stream << "            (USCXML_GET_TRANS(i).condition == NULL || " << std::endl;
-	stream << "             USCXML_GET_TRANS(i).is_enabled(ctx, &USCXML_GET_TRANS(i)) > 0)) {" << std::endl;
-	stream << "            /* remember that we found a transition */" << std::endl;
-	stream << "            ctx->flags |= USCXML_CTX_TRANSITION_FOUND;" << std::endl;
+	stream << "    fi;" << std::endl;
+    stream << "  }" << std::endl;
+    stream << "  :: else -> skip;" << std::endl;
+    stream << "  fi" << std::endl;
 	stream << std::endl;
 
-	stream << "            /* transitions that are pre-empted */" << std::endl;
-	stream << "            bit_or(conflicts, USCXML_GET_TRANS(i).conflicts, nr_trans_bytes);" << std::endl;
-	stream << std::endl;
-	stream << "            /* states that are directly targeted (resolve as entry-set later) */" << std::endl;
-	stream << "            bit_or(target_set, USCXML_GET_TRANS(i).target, nr_states_bytes);" << std::endl;
-	stream << std::endl;
-	stream << "            /* states that will be left */" << std::endl;
-	stream << "            bit_or(exit_set, USCXML_GET_TRANS(i).exit_set, nr_states_bytes);" << std::endl;
-	stream << std::endl;
-	stream << "            BIT_SET_AT(i, trans_set);" << std::endl;
-	stream << "          }" << std::endl;
-	stream << "        }" << std::endl;
-	stream << "      }" << std::endl;
-	stream << "    }" << std::endl;
-	stream << "  }" << std::endl;
-	stream << "  bit_and(exit_set, ctx->config, nr_states_bytes);" << std::endl;
-	stream << std::endl;
-#endif
+    stream << "  d_step { skip;" << std::endl;
 
     stream << "/* ---------------------------- */" << std::endl;
-	stream << "SELECT_TRANSITIONS:" << std::endl;
-    bit_clear_all(stream, "conflicts", _transitions.size(), 1);
-    bit_clear_all(stream, "trans_set", _transitions.size(), 1);
-	bit_clear_all(stream, "target_set", _states.size(), 1);
-    bit_clear_all(stream, "exit_set", _states.size(), 1);
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Establishing optimal transition set for event %d\\n\", " << _prefix << EVENT_NAME << ");" << std::endl;
-	stream << "#endif" << std::endl;
-	stream << "  " << _prefix << "flags[USCXML_CTX_TRANSITION_FOUND] = false;" << std::endl;
-	stream << "  i = 0;" << std::endl;
-	stream << "  do" << std::endl;
-	stream << "  :: i < USCXML_NUMBER_TRANS -> {" << std::endl;
-
-	stream << "    /* only select non-history, non-initial transitions */" << std::endl;
-	stream << "    if" << std::endl;
-	stream << "    :: !" << _prefix << "transitions[i].type[USCXML_TRANS_HISTORY] &&" << std::endl;
-	stream << "       !" << _prefix << "transitions[i].type[USCXML_TRANS_INITIAL] -> {" << std::endl;
-
-	stream << "      if" << std::endl;
-	stream << "      :: /* is the transition active? */" << std::endl;
-	stream << "         " << _prefix << "config[" << _prefix << "transitions[i].source] && " << std::endl;
-    stream << std::endl;
-	stream << "         /* is it non-conflicting? */" << std::endl;
-	stream << "         !conflicts[i] && " << std::endl;
-    stream << std::endl;
-	stream << "         /* is it spontaneous with an event or vice versa? */" << std::endl;
-	stream << "         ((" << _prefix << EVENT_NAME << " == USCXML_EVENT_SPONTANEOUS && " << std::endl;
-	stream << "           " << _prefix << "transitions[i].type[USCXML_TRANS_SPONTANEOUS]) || " << std::endl;
-	stream << "          (" << _prefix << EVENT_NAME << " != USCXML_EVENT_SPONTANEOUS && " << std::endl;
-	stream << "           !" << _prefix << "transitions[i].type[USCXML_TRANS_SPONTANEOUS])) &&" << std::endl;
-    stream << std::endl;
-	stream << "         /* is it matching and enabled? */" << std::endl;
-	stream << "         (false " << std::endl;
+	stream << _prefix << "SELECT_TRANSITIONS:" << std::endl;
+    stream << _prefix << "STATES_CLEAR(" << _prefix << "ctx.target_set)" << std::endl;
+    stream << _prefix << "STATES_CLEAR(" << _prefix << "ctx.exit_set)" << std::endl;
 
+    if (_transitions.size() > 0) {
+        stream << _prefix << "TRANS_CLEAR(" << _prefix << "ctx.conflicts)" << std::endl;
+        stream << _prefix << "TRANS_CLEAR(" << _prefix << "ctx.trans_set)" << std::endl;
 
-	for (auto i = 0; i < _transitions.size(); i++) {
-		stream << "          || (i == " << toStr(i);
-		if (HAS_ATTR(_transitions[i], "event") && ATTR(_transitions[i], "event") != "*") {
-			stream << " && (false";
-			std::list<TrieNode*> events =_analyzer.getTrie().getWordsWithPrefix(ATTR(_transitions[i], "event"));
-			for (auto event : events) {
-				stream << " || " << _prefix << EVENT_NAME << " == " << _analyzer.macroForLiteral(event->value);
-			}
-			stream << ")";
-		}
-		if (HAS_ATTR(_transitions[i], "cond")) {
-			stream << " && " << ADAPT_SRC(ATTR(_transitions[i], "cond"));
-		}
-		stream << ")" << std::endl;
-	}
-
-	stream << "         ) -> {" << std::endl;
+        stream << "#if TRACE_EXECUTION" << std::endl;
+        if (_machinesAll->size() > 1) {
+            stream << "printf(\"%d: Establishing optimal transition set for event %d\\n\", _pid, " << _prefix << EVENT_NAME << " );" << std::endl;
+        } else {
+            stream << "printf(\"Establishing optimal transition set for event %d\\n\", " << _prefix << EVENT_NAME << " );" << std::endl;
+        }
+        stream << "#endif" << std::endl;
+        stream << std::endl;
+
+        stream << "#if TRACE_EXECUTION" << std::endl;
+        stream << "printf(\"Configuration: \");" << std::endl;
+        printBitArray(stream, _prefix + "config", _states.size());
+        stream << "printf(\"\\n\");" << std::endl;
+        stream << "#endif" << std::endl;
+        stream << std::endl;
+        stream << "  " << _prefix << "flags[USCXML_CTX_TRANSITION_FOUND] = false;" << std::endl;
+        stream << "  i = 0;" << std::endl;
+        stream << "  do" << std::endl;
+        stream << "  :: i < " << _prefix << "USCXML_NUMBER_TRANS -> {" << std::endl;
+
+        stream << "    /* only select non-history, non-initial transitions */" << std::endl;
+        stream << "    if" << std::endl;
+        stream << "    :: !" << _prefix << "transitions[i].type[USCXML_TRANS_HISTORY] &&" << std::endl;
+        stream << "       !" << _prefix << "transitions[i].type[USCXML_TRANS_INITIAL] -> {" << std::endl;
+
+        stream << "      if" << std::endl;
+        stream << "      :: /* is the transition active? */" << std::endl;
+        stream << "         " << _prefix << "config[" << _prefix << "transitions[i].source] && " << std::endl;
+        stream << std::endl;
+        stream << "         /* is it non-conflicting? */" << std::endl;
+        stream << "         !" << _prefix << "ctx.conflicts[i] && " << std::endl;
+        stream << std::endl;
+        stream << "         /* is it spontaneous with an event or vice versa? */" << std::endl;
+        stream << "         ((" << _prefix << EVENT_NAME << " == USCXML_EVENT_SPONTANEOUS && " << std::endl;
+        stream << "           " << _prefix << "transitions[i].type[USCXML_TRANS_SPONTANEOUS]) || " << std::endl;
+        stream << "          (" << _prefix << EVENT_NAME << " != USCXML_EVENT_SPONTANEOUS && " << std::endl;
+        stream << "           !" << _prefix << "transitions[i].type[USCXML_TRANS_SPONTANEOUS])) &&" << std::endl;
+        stream << std::endl;
+        stream << "         /* is it matching and enabled? */" << std::endl;
+        stream << "         (false " << std::endl;
+
+
+        for (auto i = 0; i < _transitions.size(); i++) {
+            stream << "          || (i == " << toStr(i);
+            if (HAS_ATTR(_transitions[i], "event") && ATTR(_transitions[i], "event") != "*") {
+                stream << " && (false";
+                std::list<std::string> eventLiterals = tokenize(ATTR(_transitions[i], "event"));
+                for (auto eventLiteral : eventLiterals) {
+                    if (boost::ends_with(eventLiteral, ".*")) {
+                        eventLiteral = eventLiteral.substr(0, eventLiteral.size() - 2);
+                    }
+                    if (boost::ends_with(eventLiteral, ".")) {
+                        eventLiteral = eventLiteral.substr(0, eventLiteral.size() - 1);
+                    }
+                    std::list<TrieNode*> events =_analyzer->getTrie().getWordsWithPrefix(eventLiteral);
+                    for (auto event : events) {
+                        stream << " || " << _prefix << EVENT_NAME << " == " << _analyzer->macroForLiteral(event->value);
+                    }
+                }
+                stream << ")";
+            }
+            if (HAS_ATTR(_transitions[i], "cond")) {
+                stream << " && " << ADAPT_SRC(ATTR(_transitions[i], "cond"));
+            }
+            stream << ")" << std::endl;
+        }
 
-	stream << "        /* remember that we found a transition */" << std::endl;
-	stream << "        " << _prefix << "flags[USCXML_CTX_TRANSITION_FOUND] = true;" << std::endl;
-	stream << std::endl;
+        stream << "         ) -> {" << std::endl;
 
-	stream << "        /* transitions that are pre-empted */" << std::endl;
-	bit_or(stream, "conflicts", _prefix + "transitions[i].conflicts", _transitions.size(), 4);
-	stream << std::endl;
+        stream << "        /* remember that we found a transition */" << std::endl;
+        stream << "        " << _prefix << "flags[USCXML_CTX_TRANSITION_FOUND] = true;" << std::endl;
+        stream << std::endl;
 
-	stream << "        /* states that are directly targeted (resolve as entry-set later) */" << std::endl;
-	bit_or(stream, "target_set", _prefix + "transitions[i].target", _states.size(), 4);
-	stream << std::endl;
+        stream << "        /* transitions that are pre-empted */" << std::endl;
+        stream << "        " << _prefix << "TRANS_OR(" << _prefix << "ctx.conflicts, " << _prefix << "transitions[i].conflicts)" << std::endl;
+        stream << std::endl;
 
-	stream << "        /* states that will be left */" << std::endl;
-	bit_or(stream, "exit_set", _prefix + "transitions[i].exit_set", _states.size(), 4);
-	stream << std::endl;
+        stream << "        /* states that are directly targeted (resolve as entry-set later) */" << std::endl;
+        stream << "        " << _prefix << "STATES_OR(" << _prefix << "ctx.target_set, " << _prefix << "transitions[i].target)" << std::endl;
+        stream << std::endl;
 
-	stream << "        trans_set[i] = true;" << std::endl;
+        stream << "        /* states that will be left */" << std::endl;
+        stream << "        " << _prefix << "STATES_OR(" << _prefix << "ctx.exit_set, " << _prefix << "transitions[i].exit_set)" << std::endl;
+        stream << std::endl;
 
+        stream << "        " << _prefix << "ctx.trans_set[i] = true;" << std::endl;
 
-	stream << "      }" << std::endl;
-	stream << "      :: else {" << std::endl;
-	stream << "        skip;" << std::endl;
-	stream << "      }" << std::endl;
-	stream << "      fi" << std::endl;
-	stream << "    }" << std::endl;
-	stream << "    :: else -> break;" << std::endl;
-	stream << "    fi" << std::endl;
-
-	stream << "    i = i + 1;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << "  :: else -> break;" << std::endl;
-	stream << "  od;" << std::endl;
-
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Selected Transitions: \");" << std::endl;
-	printBitArray(stream, "trans_set", _transitions.size());
-	stream << "printf(\"\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
 
+        stream << "      }" << std::endl;
+        stream << "      :: else {" << std::endl;
+        stream << "        skip;" << std::endl;
+        stream << "      }" << std::endl;
+        stream << "      fi" << std::endl;
+        stream << "    }" << std::endl;
+        stream << "    :: else -> {" << std::endl;
+        stream << "      skip;" << std::endl;
+        stream << "    }" << std::endl;
+        stream << "    fi" << std::endl;
+
+        stream << "    i = i + 1;" << std::endl;
+        stream << "  }" << std::endl;
+        stream << "  :: else -> break;" << std::endl;
+        stream << "  od;" << std::endl;
+
+        stream << "  " << _prefix << "STATES_AND(" << _prefix << "ctx.exit_set, " << _prefix << "config)" << std::endl;
+        
+        stream << std::endl;
+        stream << "#if TRACE_EXECUTION" << std::endl;
+        stream << "printf(\"Selected Transitions: \");" << std::endl;
+        printBitArray(stream, _prefix + "ctx.trans_set", _transitions.size());
+        stream << "printf(\"\\n\");" << std::endl;
+        stream << "#endif" << std::endl;
+        stream << std::endl;
+    }
+    stream << std::endl;
 	stream << "#if TRACE_EXECUTION" << std::endl;
 	stream << "printf(\"Target Set: \");" << std::endl;
-	printBitArray(stream, "target_set", _states.size());
+	printBitArray(stream, _prefix + "ctx.target_set", _states.size());
 	stream << "printf(\"\\n\");" << std::endl;
 	stream << "#endif" << std::endl;
+    stream << std::endl;
 
-#if 0
-	stream << "  if (ctx->flags & USCXML_CTX_TRANSITION_FOUND) {" << std::endl;
-	stream << "    ctx->flags |= USCXML_CTX_SPONTANEOUS;" << std::endl;
-	stream << "    ctx->flags &= ~USCXML_CTX_TRANSITION_FOUND;" << std::endl;
-	stream << "  } else {" << std::endl;
-	stream << "    ctx->flags &= ~USCXML_CTX_SPONTANEOUS;" << std::endl;
-	stream << "    goto DEQUEUE_EVENT;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << std::endl;
-#endif
+    stream << std::endl;
+    stream << "#if TRACE_EXECUTION" << std::endl;
+    stream << "printf(\"Exit Set: \");" << std::endl;
+    printBitArray(stream, _prefix + "ctx.exit_set", _states.size());
+    stream << "printf(\"\\n\");" << std::endl;
+    stream << "#endif" << std::endl;
+    stream << std::endl;
+    
 
 	stream << "  if" << std::endl;
+    stream << "  :: !" << _prefix << "STATES_HAS_ANY(" << _prefix << "config) -> {" << std::endl;
+    stream << "    /* Enter initial configuration */" << std::endl;
+    stream << "    " << _prefix << "STATES_COPY(" << _prefix << "ctx.target_set, " << _prefix << "states[0].completion)" << std::endl;
+    stream << "    " << _prefix << "flags[USCXML_CTX_SPONTANEOUS] = true;" << std::endl;
+    stream << "    " << _prefix << "flags[USCXML_CTX_TRANSITION_FOUND] = true;" << std::endl;
+
+    TRACE_EXECUTION("Entering initial default completion");
+    
+//    stream << "    goto " << _prefix << "ESTABLISH_ENTRY_SET;" << std::endl;
+    stream << std::endl;
+    
+    stream << "  }" << std::endl;
 	stream << "  :: " << _prefix << "flags[USCXML_CTX_TRANSITION_FOUND] -> {" << std::endl;
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Found transitions\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-	stream << "    " << _prefix << "flags[USCXML_CTX_SPONTANEOUS] = true;" << std::endl;
-	stream << "    " << _prefix << "flags[USCXML_CTX_TRANSITION_FOUND] = false;" << std::endl;
+
+    TRACE_EXECUTION("Found transitions");
+
+    stream << "    " << _prefix << "flags[USCXML_CTX_SPONTANEOUS] = true;" << std::endl;
 	stream << "  }" << std::endl;
 	stream << "  :: else {" << std::endl;
 	stream << "    " << _prefix << "flags[USCXML_CTX_SPONTANEOUS] = false;" << std::endl;
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Found NO transitions\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-	stream << "    goto DEQUEUE_EVENT;" << std::endl;
+
+    TRACE_EXECUTION("Found NO transitions");
+
+//    stream << "    goto " << _prefix << "MICROSTEP;" << std::endl;
 	stream << "  }" << std::endl;
 	stream << "  fi" << std::endl;
 	stream << std::endl;
 
-#if 0
-	stream << "/* REMEMBER_HISTORY: */" << std::endl;
-	stream << "  for (i = 0; i < USCXML_NUMBER_STATES; i++) {" << std::endl;
-	stream << "    if unlikely(USCXML_STATE_MASK(USCXML_GET_STATE(i).type) == USCXML_STATE_HISTORY_SHALLOW ||" << std::endl;
-	stream << "          USCXML_STATE_MASK(USCXML_GET_STATE(i).type) == USCXML_STATE_HISTORY_DEEP) {" << std::endl;
-	stream << "      /* a history state whose parent is about to be exited */" << std::endl;
-	stream << "      if unlikely(BIT_HAS(USCXML_GET_STATE(i).parent, exit_set)) {" << std::endl;
-	stream << "        bit_copy(tmp_states, USCXML_GET_STATE(i).completion, nr_states_bytes);" << std::endl;
-	stream << std::endl;
-	stream << "        /* set those states who were enabled */" << std::endl;
-	stream << "        bit_and(tmp_states, ctx->config, nr_states_bytes);" << std::endl;
-	stream << std::endl;
-	stream << "        /* clear current history with completion mask */" << std::endl;
-	stream << "        bit_and_not(ctx->history, USCXML_GET_STATE(i).completion, nr_states_bytes);" << std::endl;
-	stream << std::endl;
-	stream << "        /* set history */" << std::endl;
-	stream << "        bit_or(ctx->history, tmp_states, nr_states_bytes);" << std::endl;
-	stream << "      }" << std::endl;
-	stream << "    }" << std::endl;
-	stream << "  }" << std::endl;
-	stream << std::endl;
-#endif
+    stream << "  if" << std::endl;
+    stream << "  :: " << _prefix << "flags[USCXML_CTX_TRANSITION_FOUND] -> {" << std::endl;
+    stream << "    /* only process anything if we found transitions or are on initial entry */" << std::endl;
 
+    
     stream << "/* ---------------------------- */" << std::endl;
 	stream << "/* REMEMBER_HISTORY: */" << std::endl;
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Save history configurations\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-	stream << "  i = 0;" << std::endl;
-	stream << "  do" << std::endl;
-	stream << "  :: i < USCXML_NUMBER_STATES -> {" << std::endl;
+    TRACE_EXECUTION("Save history configurations");
 
-	stream << "  if" << std::endl;
-	stream << "  :: " << _prefix << "states[i].type[USCXML_STATE_HISTORY_SHALLOW] ||" << std::endl;
-	stream << "     " << _prefix << "states[i].type[USCXML_STATE_HISTORY_DEEP] -> {" << std::endl;
-	stream << "    if" << std::endl;
-	stream << "    :: exit_set[" << _prefix << "states[i].parent] -> {" << std::endl;
-	stream << "      /* a history state whose parent is about to be exited */" << std::endl;
+    stream << "  if" << std::endl;
+    stream << "  :: " << _prefix << "STATES_HAS_ANY(" << _prefix << "config) -> {" << std::endl;
+    stream << "    /* only remember history on non-initial entry */" << std::endl;
 
-	bit_copy(stream, _prefix + "states[i].completion", "tmp_states", _states.size(), 3);
-	bit_and(stream, "tmp_states", _prefix + "config", _states.size(), 3);
-	bit_and_not(stream, "tmp_states", _prefix + "states[i].completion", _states.size(), 3);
-	bit_or(stream, _prefix + "history", "tmp_states", _states.size(), 3);
-	stream << std::endl;
+    stream << "    i = 0;" << std::endl;
+	stream << "    do" << std::endl;
+	stream << "    :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
 
-	stream << "    }" << std::endl;
-	stream << "    :: else -> skip;" << std::endl;
-	stream << "    fi;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << "  :: else -> skip;" << std::endl;
-	stream << "  fi;" << std::endl;
+	stream << "      if" << std::endl;
+	stream << "      :: " << _prefix << "states[i].type[USCXML_STATE_HISTORY_SHALLOW] ||" << std::endl;
+	stream << "         " << _prefix << "states[i].type[USCXML_STATE_HISTORY_DEEP] -> {" << std::endl;
+	stream << "        if" << std::endl;
+	stream << "        :: " << _prefix << "ctx.exit_set[" << _prefix << "states[i].parent] -> {" << std::endl;
+    
+	stream << "          /* a history state whose parent is about to be exited */" << std::endl;
+    TRACE_EXECUTION_V("history state %d is about to be exited", "i");
 
+    stream << std::endl;
+    stream << "#if TRACE_EXECUTION" << std::endl;
+    stream << "printf(\"COMPLET: \");" << std::endl;
+    printBitArray(stream, _prefix + "states[i].completion", _states.size());
+    stream << "printf(\"\\n\");" << std::endl;
+    stream << "#endif" << std::endl;
+    stream << std::endl;
 
-	stream << "    i = i + 1;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << "  :: else -> break;" << std::endl;
-	stream << "  od;" << std::endl;
-	stream << std::endl;
+    stream << "          " << _prefix << "STATES_COPY(" << _prefix << "ctx.tmp_states, " << _prefix << "states[i].completion)" << std::endl;
 
-#if 0
-	stream << "ESTABLISH_ENTRY_SET:" << std::endl;
-	stream << "  /* calculate new entry set */" << std::endl;
-	stream << "  bit_copy(entry_set, target_set, nr_states_bytes);" << std::endl;
-	stream << std::endl;
-	stream << "  /* iterate for ancestors */" << std::endl;
-	stream << "  for (i = 0; i < USCXML_NUMBER_STATES; i++) {" << std::endl;
-	stream << "    if (BIT_HAS(i, entry_set)) {" << std::endl;
-	stream << "      bit_or(entry_set, USCXML_GET_STATE(i).ancestors, nr_states_bytes);" << std::endl;
+    stream << std::endl;
+    stream << "          /* set those states who were enabled */" << std::endl;
+    stream << "          " << _prefix << "STATES_AND(" << _prefix << "ctx.tmp_states, " << _prefix << "config)" << std::endl;
+    
+    stream << std::endl;
+    stream << "#if TRACE_EXECUTION" << std::endl;
+    stream << "printf(\"CONFIG : \");" << std::endl;
+    printBitArray(stream, _prefix + "config", _states.size());
+    stream << "printf(\"\\n\");" << std::endl;
+    stream << "#endif" << std::endl;
+    stream << std::endl;
+    
+    stream << std::endl;
+    stream << "#if TRACE_EXECUTION" << std::endl;
+    stream << "printf(\"TMP_STS: \");" << std::endl;
+    printBitArray(stream, _prefix + "ctx.tmp_states", _states.size());
+    stream << "printf(\"\\n\");" << std::endl;
+    stream << "#endif" << std::endl;
+    stream << std::endl;
+
+    stream << std::endl;
+    stream << "          /* clear current history with completion mask */" << std::endl;
+    stream << "          " << _prefix << "STATES_AND_NOT(" << _prefix << "history, " << _prefix << "states[i].completion)" << std::endl;
+    stream << std::endl;
+
+    stream << "          /* set history */" << std::endl;
+    stream << "          " << _prefix << "STATES_OR(" << _prefix << "history, " << _prefix << "ctx.tmp_states)" << std::endl;
+    
+    stream << std::endl;
+
+    stream << "        }" << std::endl;
+	stream << "        :: else -> skip;" << std::endl;
+	stream << "        fi;" << std::endl;
+	stream << "      }" << std::endl;
+	stream << "      :: else -> skip;" << std::endl;
+	stream << "      fi;" << std::endl;
+
+	stream << "      i = i + 1;" << std::endl;
 	stream << "    }" << std::endl;
-	stream << "  }" << std::endl;
+	stream << "    :: else -> break;" << std::endl;
+	stream << "    od;" << std::endl;
 	stream << std::endl;
-#endif
+
+    stream << std::endl;
+    stream << "#if TRACE_EXECUTION" << std::endl;
+    stream << "printf(\"History: \");" << std::endl;
+    printBitArray(stream, _prefix + "history", _states.size());
+    stream << "printf(\"\\n\");" << std::endl;
+    stream << "#endif" << std::endl;
+    stream << "  }" << std::endl;
+    stream << "  :: else -> skip;" << std::endl;
+    stream << "  fi;" << std::endl;
+
+    stream << std::endl;
 
     stream << "/* ---------------------------- */" << std::endl;
-	stream << "ESTABLISH_ENTRY_SET:" << std::endl;
+	stream << _prefix << "ESTABLISH_ENTRY_SET:" << std::endl;
 	stream << "  /* calculate new entry set */" << std::endl;
-	bit_copy(stream, "target_set", "entry_set", _states.size(), 1);
+    stream << "  " << _prefix << "STATES_COPY(" << _prefix << "ctx.entry_set, " << _prefix << "ctx.target_set)" << std::endl;
 	stream << std::endl;
 
 	stream << "  i = 0;" << std::endl;
 	stream << "  do" << std::endl;
-	stream << "  :: i < USCXML_NUMBER_STATES -> {" << std::endl;
+	stream << "  :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
 
 	stream << "    if" << std::endl;
-	stream << "    :: entry_set[i] -> {" << std::endl;
+	stream << "    :: " << _prefix << "ctx.entry_set[i] -> {" << std::endl;
 	stream << "      /* ancestor completion */" << std::endl;
-	bit_or(stream, "entry_set", _prefix + "states[i].ancestors", _states.size(), 3);
+    stream << "      " << _prefix << "STATES_OR(" << _prefix << "ctx.entry_set, " << _prefix << "states[i].ancestors)" << std::endl;
 
 	stream << "    }" << std::endl;
 	stream << "    :: else -> skip;" << std::endl;
@@ -1621,168 +1787,106 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
 	stream << "  od;" << std::endl;
 	stream << std::endl;
 
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Entry Set (after ancestor completion)\");" << std::endl;
-	printBitArray(stream, "entry_set", _states.size());
-	stream << "printf(\"\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-
-#if 0
-	stream << "  /* iterate for descendants */" << std::endl;
-	stream << "  for (i = 0; i < USCXML_NUMBER_STATES; i++) {" << std::endl;
-	stream << "    if (BIT_HAS(i, entry_set)) {" << std::endl;
-	stream << "      switch (USCXML_STATE_MASK(USCXML_GET_STATE(i).type)) {" << std::endl;
-#endif
-
 	stream << "  /* iterate for descendants */" << std::endl;
 	stream << "  i = 0;" << std::endl;
 	stream << "  do" << std::endl;
-	stream << "  :: i < USCXML_NUMBER_STATES -> {" << std::endl;
+	stream << "  :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
 	stream << "    if" << std::endl;
-	stream << "    :: entry_set[i] -> {" << std::endl;
+	stream << "    :: " << _prefix << "ctx.entry_set[i] -> {" << std::endl;
 	stream << "      if" << std::endl;
 
-#if 0
-	stream << "        case USCXML_STATE_PARALLEL: {" << std::endl;
-	stream << "          bit_or(entry_set, USCXML_GET_STATE(i).completion, nr_states_bytes);" << std::endl;
-	stream << "          break;" << std::endl;
-	stream << "        }" << std::endl;
-#endif
-
 	stream << "      :: " << _prefix << "states[i].type[USCXML_STATE_PARALLEL] -> {" << std::endl;
-	bit_or(stream, "entry_set", _prefix + "states[i].completion", _states.size(), 4);
+    stream << "        " << _prefix << "STATES_OR(" << _prefix << "ctx.entry_set, " << _prefix << "states[i].completion)" << std::endl;
 	stream << "      }" << std::endl;
 
 
-#if 0
-	stream << "        case USCXML_STATE_HISTORY_SHALLOW:" << std::endl;
-	stream << "        case USCXML_STATE_HISTORY_DEEP: {" << std::endl;
-	stream << "          if (!bit_has_and(USCXML_GET_STATE(i).completion, ctx->history, nr_states_bytes) &&" << std::endl;
-	stream << "            !BIT_HAS(USCXML_GET_STATE(i).parent, ctx->config)) {" << std::endl;
-	stream << "            /* nothing set for history, look for a default transition */" << std::endl;
-	stream << "            for (j = 0; j < USCXML_NUMBER_TRANS; j++) {" << std::endl;
-	stream << "              if unlikely(ctx->machine->transitions[j].source == i) {" << std::endl;
-	stream << "                bit_or(entry_set, ctx->machine->transitions[j].target, nr_states_bytes);" << std::endl;
-	stream << "                if(USCXML_STATE_MASK(USCXML_GET_STATE(i).type) == USCXML_STATE_HISTORY_DEEP &&" << std::endl;
-	stream << "                   !bit_has_and(ctx->machine->transitions[j].target, USCXML_GET_STATE(i).children, nr_states_bytes)) {" << std::endl;
-	stream << "                  for (k = i + 1; k < USCXML_NUMBER_STATES; k++) {" << std::endl;
-	stream << "                    if (BIT_HAS(k, ctx->machine->transitions[j].target)) {" << std::endl;
-	stream << "                      bit_or(entry_set, ctx->machine->states[k].ancestors, nr_states_bytes);" << std::endl;
-	stream << "                      break;" << std::endl;
-	stream << "                    }" << std::endl;
-	stream << "                  }" << std::endl;
-	stream << "                }" << std::endl;
-	stream << "                BIT_SET_AT(j, trans_set);" << std::endl;
-	stream << "                break;" << std::endl;
-	stream << "              }" << std::endl;
-	stream << "              /* Note: SCXML mandates every history to have a transition! */" << std::endl;
-	stream << "            }" << std::endl;
-	stream << "          } else {" << std::endl;
-	stream << "            bit_copy(tmp_states, USCXML_GET_STATE(i).completion, nr_states_bytes);" << std::endl;
-	stream << "            bit_and(tmp_states, ctx->history, nr_states_bytes);" << std::endl;
-	stream << "            bit_or(entry_set, tmp_states, nr_states_bytes);" << std::endl;
-	stream << "            if (USCXML_GET_STATE(i).type == (USCXML_STATE_HAS_HISTORY | USCXML_STATE_HISTORY_DEEP)) {" << std::endl;
-	stream << "              /* a deep history state with nested histories -> more completion */" << std::endl;
-	stream << "              for (j = i + 1; j < USCXML_NUMBER_STATES; j++) {" << std::endl;
-	stream << "                if (BIT_HAS(j, USCXML_GET_STATE(i).completion) &&" << std::endl;
-	stream << "                  BIT_HAS(j, entry_set) &&" << std::endl;
-	stream << "                  (ctx->machine->states[j].type & USCXML_STATE_HAS_HISTORY)) {" << std::endl;
-	stream << "                  for (k = j + 1; k < USCXML_NUMBER_STATES; k++) {" << std::endl;
-	stream << "                    /* add nested history to entry_set */" << std::endl;
-	stream << "                    if ((USCXML_STATE_MASK(ctx->machine->states[k].type) == USCXML_STATE_HISTORY_DEEP ||" << std::endl;
-	stream << "                       USCXML_STATE_MASK(ctx->machine->states[k].type) == USCXML_STATE_HISTORY_SHALLOW) &&" << std::endl;
-	stream << "                      BIT_HAS(k, ctx->machine->states[j].children)) {" << std::endl;
-	stream << "                      /* a nested history state */" << std::endl;
-	stream << "                      BIT_SET_AT(k, entry_set);" << std::endl;
-	stream << "                    }" << std::endl;
-	stream << "                  }" << std::endl;
-	stream << "                }" << std::endl;
-	stream << "              }" << std::endl;
-	stream << "            }" << std::endl;
-	stream << "          }" << std::endl;
-	stream << "          break;" << std::endl;
-	stream << "        }" << std::endl;
-#endif
-
-
 	stream << "      :: " << _prefix << "states[i].type[USCXML_STATE_HISTORY_SHALLOW] ||" << std::endl;
 	stream << "         " << _prefix << "states[i].type[USCXML_STATE_HISTORY_DEEP] -> {" << std::endl;
-	stream << "        if" << std::endl;
-	stream << "        :: !";
-	bit_has_and(stream, _prefix + "states[i].completion", _prefix + "history", _states.size(), 5);
+
+    TRACE_EXECUTION_V("Descendant completion for history state %d", "i")
+
+    stream << "        if" << std::endl;
+	stream << "        :: !" << _prefix << "STATES_HAS_AND(" << _prefix << "states[i].completion, " << _prefix << "history)";
+//	bit_has_and(stream, _prefix + "states[i].completion", _prefix + "history", _states.size(), 5);
 	stream << " && !" << _prefix << "config[" << _prefix << "states[i].parent]" << " -> {" << std::endl;
     stream << "          /* nothing set for history, look for a default transition */" << std::endl;
-    stream << "          j = 0;" << std::endl;
-    stream << "          do" << std::endl;
-    stream << "          :: j < USCXML_NUMBER_TRANS -> {" << std::endl;
-    stream << "             if" << std::endl;
-    stream << "             :: " << _prefix << "transitions[j].source == i -> {" << std::endl;
-    
-    bit_or(stream, "entry_set", _prefix + "transitions[j].target", _states.size(), 8);
-    stream << std::endl;
-    stream << "               if" << std::endl;
-    stream << "               :: (" << _prefix << "states[i].type[USCXML_STATE_HISTORY_DEEP] &&" << std::endl;
-    stream << "                   !";
-    bit_has_and(stream, _prefix + "transitions[j].target", _prefix + "states[i].children", _states.size(), 10);
-    stream << "                  ) -> {" << std::endl;
-    stream << "                 k = i + 1" << std::endl;
-    stream << "                 do" << std::endl;
-    stream << "                 :: k < USCXML_NUMBER_STATES -> {" << std::endl;
-    stream << "                   if" << std::endl;
-    stream << "                   :: " << _prefix << "transitions[j].target[k] -> {" << std::endl;
-    bit_or(stream, "entry_set", _prefix + "states[k].ancestors", _states.size(), 11);
-    stream << "                     break;" << std::endl;
-    stream << std::endl;
-    stream << "                   }" << std::endl;
-    stream << "                   :: else -> skip;" << std::endl;
-    stream << "                   fi" << std::endl;
-    stream << "                 }" << std::endl;
-    stream << "                 :: else -> break;" << std::endl;
-    stream << "                 od" << std::endl;
-    stream << "                 trans_set[j] = true;" << std::endl;
-    stream << "                 break;" << std::endl;
-    stream << "               }" << std::endl;
-    stream << "               :: else -> skip;" << std::endl;
-    stream << "               fi" << std::endl;
-
-    stream << "             }" << std::endl;
-    stream << "             :: else -> skip;" << std::endl;
-    stream << "             fi" << std::endl;
-    stream << "             j = j + 1;" << std::endl;
-    stream << "          }" << std::endl;
-    stream << "          :: else -> break" << std::endl;
-    stream << "          od" << std::endl;
+    TRACE_EXECUTION("Fresh history in target set")
+    if (_transitions.size() > 0) {
+        stream << "          j = 0;" << std::endl;
+        stream << "          do" << std::endl;
+        stream << "          :: j < " << _prefix << "USCXML_NUMBER_TRANS -> {" << std::endl;
+        stream << "             if" << std::endl;
+        stream << "             :: " << _prefix << "transitions[j].source == i -> {" << std::endl;
+        stream << "               " << _prefix << "ctx.trans_set[j] = true;" << std::endl;
+
+        stream << "               " << _prefix << "STATES_OR(" << _prefix << "ctx.entry_set, " << _prefix << "transitions[j].target)" << std::endl;
+        stream << std::endl;
+        stream << "               if" << std::endl;
+        stream << "               :: (" << _prefix << "states[i].type[USCXML_STATE_HISTORY_DEEP] &&" << std::endl;
+        stream << "                   !" << _prefix << "STATES_HAS_AND(" << _prefix << "transitions[j].target, " << _prefix << "states[i].children)";
+    //    bit_has_and(stream, _prefix + "transitions[j].target", _prefix + "states[i].children", _states.size(), 10);
+        stream << "                  ) -> {" << std::endl;
+        stream << "                 k = i + 1" << std::endl;
+        stream << "                 do" << std::endl;
+        stream << "                 :: k < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
+        stream << "                   if" << std::endl;
+        stream << "                   :: " << _prefix << "transitions[j].target[k] -> {" << std::endl;
+        stream << "                     " << _prefix << "STATES_OR(" << _prefix << "ctx.entry_set, " << _prefix << "states[k].ancestors)" << std::endl;
+        stream << "                     break;" << std::endl;
+        stream << std::endl;
+        stream << "                   }" << std::endl;
+        stream << "                   :: else -> skip;" << std::endl;
+        stream << "                   fi" << std::endl;
+        stream << "                   k = k + 1;" << std::endl;
+        stream << "                 }" << std::endl;
+        stream << "                 :: else -> break;" << std::endl;
+        stream << "                 od" << std::endl;
+        stream << "               }" << std::endl;
+        stream << "               :: else -> skip;" << std::endl;
+        stream << "               fi" << std::endl;
+        stream << "               break;" << std::endl;
+        stream << "             }" << std::endl;
+        stream << "             :: else -> skip;" << std::endl;
+        stream << "             fi" << std::endl;
+        stream << "             j = j + 1;" << std::endl;
+        stream << "          }" << std::endl;
+        stream << "          :: else -> break" << std::endl;
+        stream << "          od" << std::endl;
+    }
 	stream << "          skip;" << std::endl;
 	stream << "        }" << std::endl;
     stream << "        :: else -> {" << std::endl;
-    bit_copy(stream, "tmp_states", _prefix + "states[i].completion", _states.size(), 5);
-    bit_and(stream, "tmp_states", _prefix + "history", _states.size(), 5);
-    bit_or(stream, "entry_set", "tmp_states", _states.size(), 5);
+    
+    TRACE_EXECUTION("Established history in target set")
+    stream << "          " << _prefix << "STATES_COPY(" << _prefix << "ctx.tmp_states, " << _prefix << "states[i].completion)" << std::endl;
+    stream << "          " << _prefix << "STATES_AND(" << _prefix << "ctx.tmp_states, " << _prefix << "history)" << std::endl;
+    stream << "          " << _prefix << "STATES_OR(" << _prefix << "ctx.entry_set, " << _prefix << "ctx.tmp_states)" << std::endl;
     stream << "          if" << std::endl;
     stream << "          :: " << _prefix << "states[i].type[USCXML_STATE_HAS_HISTORY] ||" << std::endl;
     stream << "             " << _prefix << "states[i].type[USCXML_STATE_HISTORY_DEEP] -> { " << std::endl;
     stream << "            /* a deep history state with nested histories -> more completion */" << std::endl;
+    TRACE_EXECUTION("DEEP HISTORY")
     stream << "            j = i + 1;" << std::endl;
     stream << "            do" << std::endl;
-    stream << "            :: j < USCXML_NUMBER_STATES -> {" << std::endl;
+    stream << "            :: j < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
     stream << "              if" << std::endl;
     stream << "              :: (" << _prefix << "states[i].completion[j] &&" << std::endl;
-    stream << "                  entry_set[j] && " << std::endl;
+    stream << "                  " << _prefix << "ctx.entry_set[j] && " << std::endl;
     stream << "                  " << _prefix << "states[j].type[USCXML_STATE_HAS_HISTORY]) -> {" << std::endl;
     stream << "                k = j + 1;" << std::endl;
     stream << "                do" << std::endl;
-    stream << "                :: k < USCXML_NUMBER_STATES -> {" << std::endl;
+    stream << "                :: k < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
     stream << "                  /* add nested history to entry_set */" << std::endl;
-    stream << "                  k = k + 1;" << std::endl;
     stream << "                  if" << std::endl;
     stream << "                  :: (" << _prefix << "states[k].type[USCXML_STATE_HISTORY_DEEP] ||" << std::endl;
     stream << "                      " << _prefix << "states[k].type[USCXML_STATE_HISTORY_SHALLOW]) &&" << std::endl;
     stream << "                     " << _prefix << "states[j].children[k] -> {" << std::endl;
     stream << "                    /* a nested history state */" << std::endl;
-    stream << "                    entry_set[k] = true;" << std::endl;
+    stream << "                    " << _prefix << "ctx.entry_set[k] = true;" << std::endl;
     stream << "                  }" << std::endl;
     stream << "                  :: else -> skip;" << std::endl;
     stream << "                  fi" << std::endl;
+    stream << "                  k = k + 1;" << std::endl;
     stream << "                }" << std::endl;
     stream << "                :: else -> break;" << std::endl;
     stream << "                od" << std::endl;
@@ -1790,6 +1894,7 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
     stream << "              :: else -> skip;" << std::endl;
     stream << "              fi" << std::endl;
     stream << "            }" << std::endl;
+    stream << "            j = j + 1;" << std::endl;
     stream << "            :: else -> break;" << std::endl;
     stream << "            od" << std::endl;
     stream << "          }" << std::endl;
@@ -1801,137 +1906,100 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
 
 	stream << "      }" << std::endl;
 
-#if 0
-	stream << "        case USCXML_STATE_INITIAL: {" << std::endl;
-	stream << "          for (j = 0; j < USCXML_NUMBER_TRANS; j++) {" << std::endl;
-	stream << "            if (ctx->machine->transitions[j].source == i) {" << std::endl;
-	stream << "              BIT_SET_AT(j, trans_set);" << std::endl;
-	stream << "              BIT_CLEAR(i, entry_set);" << std::endl;
-	stream << "              bit_or(entry_set, ctx->machine->transitions[j].target, nr_states_bytes);" << std::endl;
-	stream << "              for (k = i + 1; k < USCXML_NUMBER_STATES; k++) {" << std::endl;
-	stream << "                if (BIT_HAS(k, ctx->machine->transitions[j].target)) {" << std::endl;
-	stream << "                  bit_or(entry_set, ctx->machine->states[k].ancestors, nr_states_bytes);" << std::endl;
-	stream << "                }" << std::endl;
-	stream << "              }" << std::endl;
-	stream << "            }" << std::endl;
-	stream << "          }" << std::endl;
-	stream << "          break;" << std::endl;
-	stream << "        }" << std::endl;
-#endif
+    if (_transitions.size() > 0) {
+        stream << "      :: " << _prefix << "states[i].type[USCXML_STATE_INITIAL] -> {" << std::endl;
 
-	stream << "      :: " << _prefix << "states[i].type[USCXML_STATE_INITIAL] -> {" << std::endl;
-	stream << "        j = 0" << std::endl;
-	stream << "        do" << std::endl;
-	stream << "        :: j < USCXML_NUMBER_TRANS -> {" << std::endl;
-	stream << "          if" << std::endl;
-	stream << "          :: " << _prefix << "transitions[j].source == i -> {" << std::endl;
-	stream << "            trans_set[j] = true;" << std::endl;
-	stream << "            entry_set[i] = false;" << std::endl;
+        TRACE_EXECUTION_V("Descendant completion for initial state %d", "i")
 
-	bit_or(stream, "entry_set", _prefix + "transitions[j].target", _states.size(), 6);
-	stream << std::endl;
+        stream << "        j = 0" << std::endl;
+        stream << "        do" << std::endl;
+        stream << "        :: j < " << _prefix << "USCXML_NUMBER_TRANS -> {" << std::endl;
+        stream << "          if" << std::endl;
+        stream << "          :: " << _prefix << "transitions[j].source == i -> {" << std::endl;
+        stream << "            " << _prefix << "ctx.trans_set[j] = true;" << std::endl;
+        stream << "            " << _prefix << "ctx.entry_set[i] = false;" << std::endl;
 
-	stream << "            k = i + 1;" << std::endl;
-	stream << "            do" << std::endl;
-	stream << "            :: k < USCXML_NUMBER_STATES -> {" << std::endl;
-	stream << "              if" << std::endl;
-	stream << "              :: " << _prefix << "transitions[j].target[k] -> {" << std::endl;
+        TRACE_EXECUTION_V("Adding transition %d!", "j");
 
-	bit_or(stream, "entry_set", _prefix + "states[k].ancestors", _states.size(), 8);
-	stream << std::endl;
+        
+        stream << "            " << _prefix << "STATES_OR(" << _prefix << "ctx.entry_set, " << _prefix << "transitions[j].target)" << std::endl;
+        stream << std::endl;
 
-	stream << "              }" << std::endl;
-	stream << "              :: else -> break;" << std::endl;
-	stream << "              fi" << std::endl;
-	stream << "              k = k + 1;" << std::endl;
-	stream << "            }" << std::endl;
-	stream << "            :: else -> break" << std::endl;
-	stream << "            od" << std::endl;
-	stream << "          }" << std::endl;
-	stream << "          :: else -> break;" << std::endl;
-	stream << "          fi" << std::endl;
-	stream << "          j = j + 1;" << std::endl;
-	stream << "        }" << std::endl;
-	stream << "        :: else -> break" << std::endl;
-	stream << "        od;" << std::endl;
+        stream << "            k = i + 1;" << std::endl;
+        stream << "            do" << std::endl;
+        stream << "            :: k < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
+        stream << "              if" << std::endl;
+        stream << "              :: " << _prefix << "transitions[j].target[k] -> {" << std::endl;
 
-	stream << "      }" << std::endl;
+        stream << "                " << _prefix << "STATES_OR(" << _prefix << "ctx.entry_set, " << _prefix << "states[k].ancestors)" << std::endl;
+        stream << std::endl;
 
+        stream << "              }" << std::endl;
+        stream << "              :: else -> break;" << std::endl;
+        stream << "              fi" << std::endl;
+        stream << "              k = k + 1;" << std::endl;
+        stream << "            }" << std::endl;
+        stream << "            :: else -> break" << std::endl;
+        stream << "            od" << std::endl;
+        stream << "          }" << std::endl;
+        stream << "          :: else -> skip;" << std::endl;
+        stream << "          fi" << std::endl;
+        stream << "          j = j + 1;" << std::endl;
+        stream << "        }" << std::endl;
+        stream << "        :: else -> break" << std::endl;
+        stream << "        od;" << std::endl;
 
-#if 0
-	stream << "        case USCXML_STATE_COMPOUND: { /* we need to check whether one child is already in entry_set */" << std::endl;
-	stream << "          if (!bit_has_and(entry_set, USCXML_GET_STATE(i).children, nr_states_bytes) &&" << std::endl;
-	stream << "            (!bit_has_and(ctx->config, USCXML_GET_STATE(i).children, nr_states_bytes) ||" << std::endl;
-	stream << "             bit_has_and(exit_set, USCXML_GET_STATE(i).children, nr_states_bytes)))" << std::endl;
-	stream << "          {" << std::endl;
-	stream << "            bit_or(entry_set, USCXML_GET_STATE(i).completion, nr_states_bytes);" << std::endl;
-	stream << "            if (!bit_has_and(USCXML_GET_STATE(i).completion, USCXML_GET_STATE(i).children, nr_states_bytes)) {" << std::endl;
-	stream << "              /* deep completion */" << std::endl;
-	stream << "              for (j = i + 1; j < USCXML_NUMBER_STATES; j++) {" << std::endl;
-	stream << "                if (BIT_HAS(j, USCXML_GET_STATE(i).completion)) {" << std::endl;
-	stream << "                  bit_or(entry_set, ctx->machine->states[j].ancestors, nr_states_bytes);" << std::endl;
-	stream << "                  break; /* completion of compound is single state */" << std::endl;
-	stream << "                }" << std::endl;
-	stream << "              }" << std::endl;
-	stream << "            }" << std::endl;
-	stream << "          }" << std::endl;
-	stream << "          break;" << std::endl;
-	stream << "        }" << std::endl;
-	stream << "      }" << std::endl;
-	stream << "    }" << std::endl;
-	stream << "  }" << std::endl;
-	stream << std::endl;
-#endif
+        stream << "      }" << std::endl;
+    }
 
 	stream << "      :: " << _prefix << "states[i].type[USCXML_STATE_COMPOUND] -> {" << std::endl;
 
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Descendant completion for compound state %d\\n\", i);" << std::endl;
-	stream << "#endif" << std::endl;
+//    TRACE_EXECUTION_V("Descendant completion for compound state %d", "i")
 
 	stream << "        /* we need to check whether one child is already in entry_set */" << std::endl;
 	stream << "        if" << std::endl;
 	stream << "        :: (" << std::endl;
-	stream << "          !";
-	bit_has_and(stream, "entry_set", _prefix + "states[i].children", _states.size(), 5);
+	stream << "          !" << _prefix << "STATES_HAS_AND(" << _prefix << "ctx.entry_set, " << _prefix << "states[i].children)";
 	stream << " && " << std::endl;
-	stream << "           (!";
-	bit_has_and(stream, _prefix + "config", _prefix + "states[i].children", _states.size(), 5);
-	stream << " || " << std::endl;
-	bit_has_and(stream, "exit_set", _prefix + "states[i].children", _states.size(), 5);
-	stream << ")) "<< std::endl;
+	stream << "           (!" << _prefix << "STATES_HAS_AND(" << _prefix << "config, " << _prefix << "states[i].children)";
+//	bit_has_and(stream, _prefix + "config", _prefix + "states[i].children", _states.size(), 5);
+	stream << " || " << _prefix << "STATES_HAS_AND(" << _prefix << "ctx.exit_set, " << _prefix << "states[i].children)" << std::endl;
+	stream << ")) " << std::endl;
 	stream << "        -> {" << std::endl;
 
-	bit_or(stream, "entry_set", _prefix + "states[i].completion", _states.size(), 5);
+    stream << "          " << _prefix << "STATES_OR(" << _prefix << "ctx.entry_set, " << _prefix << "states[i].completion)" << std::endl;
 
-	stream << "             if" << std::endl;
-	stream << "             :: (";
-	bit_has_and(stream, _prefix + "states[i].completion", _prefix + "states[i].children", _states.size(), 5);
-	stream << std::endl;
-	stream << "              ) -> {" << std::endl;
-	stream << "                /* deep completion */" << std::endl;
-	stream << "                j = i + 1;" << std::endl;
-	stream << "                do" << std::endl;
-	stream << "                :: j < USCXML_NUMBER_STATES - 1 -> {" << std::endl;
-	stream << "                  j = j + 1;" << std::endl;
-	stream << "                  if" << std::endl;
-	stream << "                  :: " << _prefix << "states[i].completion[j] -> {" << std::endl;
-
-	bit_or(stream, "entry_set", _prefix + "states[j].ancestors", _states.size(), 9);
+	stream << "          if" << std::endl;
+	stream << "          :: (" << _prefix << "STATES_HAS_AND(" << _prefix << "states[i].completion, " << _prefix << "states[i].children)";
+//	bit_has_and(stream, _prefix + "states[i].completion", _prefix + "states[i].children", _states.size(), 6);
+    stream << std::endl;
+	stream << "          ) -> {" << std::endl;
+	stream << "            /* deep completion */" << std::endl;
+	stream << "            j = i + 1;" << std::endl;
+    
+//    TRACE_EXECUTION_V("Deep completion for compound state %d", "i")
+
+    stream << "            do" << std::endl;
+	stream << "            :: j < " << _prefix << "USCXML_NUMBER_STATES - 1 -> {" << std::endl;
+	stream << "              j = j + 1;" << std::endl;
+	stream << "              if" << std::endl;
+	stream << "              :: " << _prefix << "states[i].completion[j] -> {" << std::endl;
+
+    stream << "                " << _prefix << "STATES_OR(" << _prefix << "ctx.entry_set, " << _prefix << "states[j].ancestors)" << std::endl;
 	stream << std::endl;
 
-	stream << "                    /* completion of compound is single state */" << std::endl;
-	stream << "                    break;" << std::endl;
-	stream << "                  } " << std::endl;
-	stream << "                  :: else -> skip;" << std::endl;
-	stream << "                  fi" << std::endl;
-	stream << "                }" << std::endl;
-	stream << "                :: else -> break;" << std::endl;
-	stream << "                od" << std::endl;
+	stream << "                /* completion of compound is single state */" << std::endl;
+	stream << "                break;" << std::endl;
+	stream << "              } " << std::endl;
+	stream << "              :: else -> skip;" << std::endl;
+	stream << "              fi" << std::endl;
+	stream << "            }" << std::endl;
+	stream << "            :: else -> break;" << std::endl;
+	stream << "            od" << std::endl;
 
-	stream << "             }" << std::endl;
-	stream << "             :: else -> skip;" << std::endl;
-	stream << "             fi" << std::endl;
+	stream << "          }" << std::endl;
+	stream << "          :: else -> skip;" << std::endl;
+	stream << "          fi" << std::endl;
 
 	stream << "        }" << std::endl;
 	stream << "        :: else -> skip;" << std::endl;
@@ -1949,53 +2017,41 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
 	stream << "  od;" << std::endl;
 	stream << std::endl;
 
-#if 0
-	stream << "/* EXIT_STATES: */" << std::endl;
-	stream << "  i = USCXML_NUMBER_STATES;" << std::endl;
-	stream << "  while(i-- > 0) {" << std::endl;
-	stream << "    if (BIT_HAS(i, exit_set) && BIT_HAS(i, ctx->config)) {" << std::endl;
-	stream << "      /* call all on exit handlers */" << std::endl;
-	stream << "      if (USCXML_GET_STATE(i).on_exit != NULL) {" << std::endl;
-	stream << "        if unlikely((err = USCXML_GET_STATE(i).on_exit(ctx, &USCXML_GET_STATE(i), ctx->event)) != USCXML_ERR_OK)" << std::endl;
-	stream << "          return err;" << std::endl;
-	stream << "      }" << std::endl;
-	stream << "      BIT_CLEAR(i, ctx->config);" << std::endl;
-	stream << "    }" << std::endl;
-	stream << "  }" << std::endl;
-	stream << std::endl;
-#endif
-
+    stream << std::endl;
 	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Entry Set (after descendant completion)\");" << std::endl;
-	printBitArray(stream, "entry_set", _states.size());
+	stream << "printf(\"Entry Set\");" << std::endl;
+	printBitArray(stream, _prefix + "ctx.entry_set", _states.size());
 	stream << "printf(\"\\n\");" << std::endl;
 	stream << "#endif" << std::endl;
+    stream << std::endl;
 
     stream << "/* ---------------------------- */" << std::endl;
 	stream << "/* EXIT_STATES: */" << std::endl;
-	stream << "  i = USCXML_NUMBER_STATES;" << std::endl;
+	stream << "  i = " << _prefix << "USCXML_NUMBER_STATES;" << std::endl;
 	stream << "  do" << std::endl;
 	stream << "  :: i > 0 -> {" << std::endl;
 	stream << "    i = i - 1;" << std::endl;
 	stream << "    if" << std::endl;
-	stream << "    :: exit_set[i] && " << _prefix << "config[i] -> {" << std::endl;
+	stream << "    :: " << _prefix << "ctx.exit_set[i] && " << _prefix << "config[i] -> {" << std::endl;
 	stream << "      /* call all on-exit handlers */" << std::endl;
-    
+
+    TRACE_EXECUTION_V("Exiting state %d", "i");
+
     stream << "      if" << std::endl;
     for (auto i = 0; i < _states.size(); i++) {
-        std::list<DOMElement*> onentries = DOMUtils::filterChildElements(XML_PREFIX(_states[i]).str() + "onexit" , _states[i]);
-        if (onentries.size() > 0) {
+        std::list<DOMElement*> onexits = DOMUtils::filterChildElements(XML_PREFIX(_states[i]).str() + "onexit" , _states[i]);
+        if (onexits.size() > 0) {
             stream << "      :: i == " << toStr(i) << " -> {" << std::endl;
-            for (auto onentry : onentries)
-                writeExecContent(stream, onentry, 3);
+            TRACE_EXECUTION_V("Processing executable content for exiting state %d", "i");
+            for (auto onexit : onexits)
+                writeExecContent(stream, onexit, 3);
             stream << "      }" << std::endl;
         }
     }
-    stream << "      :: else ->skip;" << std::endl;
+    stream << "      :: else -> skip;" << std::endl;
     stream << "      fi" << std::endl;
     stream << std::endl;
 
-    
 	stream << "      " << _prefix << "config[i] = false;" << std::endl;
 	stream << "      skip;" << std::endl;
 	stream << "    }" << std::endl;
@@ -2006,110 +2062,63 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
 	stream << "  od;" << std::endl;
 	stream << std::endl;
 
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Exited States\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-
-#if 0
-	stream << "/* TAKE_TRANSITIONS: */" << std::endl;
-	stream << "  for (i = 0; i < USCXML_NUMBER_TRANS; i++) {" << std::endl;
-	stream << "    if (BIT_HAS(i, trans_set) && (USCXML_GET_TRANS(i).type & (USCXML_TRANS_HISTORY | USCXML_TRANS_INITIAL)) == 0) {" << std::endl;
-	stream << "      /* call executable content in transition */" << std::endl;
-	stream << "      if (USCXML_GET_TRANS(i).on_transition != NULL) {" << std::endl;
-	stream << "        if unlikely((err = USCXML_GET_TRANS(i).on_transition(ctx," << std::endl;
-	stream << "                                        &ctx->machine->states[USCXML_GET_TRANS(i).source]," << std::endl;
-	stream << "                                        ctx->event)) != USCXML_ERR_OK)" << std::endl;
-	stream << "          return err;" << std::endl;
-	stream << "      }" << std::endl;
-	stream << "    }" << std::endl;
-	stream << "  }" << std::endl;
-	stream << std::endl;
-#endif
+//    TRACE_EXECUTION("Exited States")
 
     stream << "/* ---------------------------- */" << std::endl;
     stream << "/* TAKE_TRANSITIONS: */" << std::endl;
-	stream << "  i = 0;" << std::endl;
-	stream << "  do" << std::endl;
-	stream << "  :: i < USCXML_NUMBER_TRANS -> {" << std::endl;
-	stream << "    if" << std::endl;
-	stream << "    :: trans_set[i] && " << std::endl;
-	stream << "       !" << _prefix << "transitions[i].type[USCXML_TRANS_HISTORY] && " << std::endl;
-	stream << "       !" << _prefix << "transitions[i].type[USCXML_TRANS_INITIAL] -> {" << std::endl;
-    stream << "      /* Call executable content in normal transition */" << std::endl;
-    stream << "      if" << std::endl;
-    for (auto i = 0; i < _transitions.size(); i++) {
-        stream << "      :: i == " << toStr(i) << " -> {" << std::endl;
-        writeExecContent(stream, _transitions[i], 4);
-        stream << "        skip;" << std::endl;
-        stream << "      }" << std::endl;
+    if (_transitions.size() > 0) {
+        stream << "  i = 0;" << std::endl;
+        stream << "  do" << std::endl;
+        stream << "  :: i < " << _prefix << "USCXML_NUMBER_TRANS -> {" << std::endl;
+        stream << "    if" << std::endl;
+        stream << "    :: " << _prefix << "ctx.trans_set[i] && " << std::endl;
+        stream << "       !" << _prefix << "transitions[i].type[USCXML_TRANS_HISTORY] && " << std::endl;
+        stream << "       !" << _prefix << "transitions[i].type[USCXML_TRANS_INITIAL] -> {" << std::endl;
+        stream << "      /* Call executable content in normal transition */" << std::endl;
+        
+        TRACE_EXECUTION_V("Taking transition %d", "i");
+        
+        stream << "      if" << std::endl;
+        for (auto i = 0; i < _transitions.size(); i++) {
+            stream << "      :: i == " << toStr(i) << " -> {" << std::endl;
+            TRACE_EXECUTION_V("Processing executable content for transition %d", "i");
+            writeExecContent(stream, _transitions[i], 4);
+            stream << "        skip;" << std::endl;
+            stream << "      }" << std::endl;
+        }
+        stream << "      :: else ->skip;" << std::endl;
+        stream << "      fi" << std::endl;
+        stream << std::endl;
+        stream << "    }" << std::endl;
+        stream << "    :: else -> skip;" << std::endl;
+        stream << "    fi;" << std::endl;
+        stream << "    i = i + 1;" << std::endl;
+        stream << "  }" << std::endl;
+        stream << "  :: else -> break;" << std::endl;
+        stream << "  od;" << std::endl;
     }
-    stream << "      :: else ->skip;" << std::endl;
-    stream << "      fi" << std::endl;
     stream << std::endl;
-	stream << "    }" << std::endl;
-	stream << "    :: else -> skip;" << std::endl;
-	stream << "    fi;" << std::endl;
-	stream << "    i = i + 1;" << std::endl;
-	stream << "  }" << std::endl;
-	stream << "  :: else -> break;" << std::endl;
-	stream << "  od;" << std::endl;
-	stream << std::endl;
-
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Took Transitions\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-
-#if 0
-	stream << "/* ENTER_STATES: */" << std::endl;
-	stream << "  for (i = 0; i < USCXML_NUMBER_STATES; i++) {" << std::endl;
-	stream << "    if (BIT_HAS(i, entry_set) && !BIT_HAS(i, ctx->config)) {" << std::endl;
-	stream << "      /* these are no proper states */" << std::endl;
-	stream << "      if unlikely(USCXML_STATE_MASK(USCXML_GET_STATE(i).type) == USCXML_STATE_HISTORY_DEEP ||" << std::endl;
-	stream << "            USCXML_STATE_MASK(USCXML_GET_STATE(i).type) == USCXML_STATE_HISTORY_SHALLOW ||" << std::endl;
-	stream << "            USCXML_STATE_MASK(USCXML_GET_STATE(i).type) == USCXML_STATE_INITIAL)" << std::endl;
-	stream << "        continue;" << std::endl;
-	stream << std::endl;
-#endif
 
     stream << "/* ---------------------------- */" << std::endl;
 	stream << "/* ENTER_STATES: */" << std::endl;
 	stream << "  i = 0;" << std::endl;
 	stream << "  do" << std::endl;
-	stream << "  :: i < USCXML_NUMBER_STATES -> {" << std::endl;
+	stream << "  :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
 	stream << "    if" << std::endl;
-	stream << "    :: (entry_set[i] &&" << std::endl;
-	stream << "      !" << _prefix << "config[i] && " << std::endl;
-	stream << "      /* these are no proper states */" << std::endl;
-	stream << "      !" << _prefix << "states[i].type[USCXML_STATE_HISTORY_DEEP] && " << std::endl;
-	stream << "      !" << _prefix << "states[i].type[USCXML_STATE_HISTORY_SHALLOW] && " << std::endl;
-	stream << "      !" << _prefix << "states[i].type[USCXML_STATE_INITIAL]" << std::endl;
+	stream << "    :: (" << _prefix << "ctx.entry_set[i] &&" << std::endl;
+	stream << "        !" << _prefix << "config[i] && " << std::endl;
+	stream << "        /* these are no proper states */" << std::endl;
+	stream << "        !" << _prefix << "states[i].type[USCXML_STATE_HISTORY_DEEP] && " << std::endl;
+	stream << "        !" << _prefix << "states[i].type[USCXML_STATE_HISTORY_SHALLOW] && " << std::endl;
+	stream << "        !" << _prefix << "states[i].type[USCXML_STATE_INITIAL]" << std::endl;
 	stream << "       ) -> {" << std::endl;
 
-#if 0
-	stream << "      BIT_SET_AT(i, ctx->config);" << std::endl;
-	stream << std::endl;
-#endif
-
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Entering State %d\\n\", i);" << std::endl;
-	stream << "#endif" << std::endl;
+    TRACE_EXECUTION_V("Entering state %d", "i");
 
 	stream << "         " << _prefix << "config[i] = true;" << std::endl;
 	stream << std::endl;
 
-
 #if 0
-	stream << "      /* initialize data */" << std::endl;
-	stream << "      if (!BIT_HAS(i, ctx->initialized_data)) {" << std::endl;
-	stream << "        if unlikely(USCXML_GET_STATE(i).data != NULL && ctx->exec_content_init != NULL) {" << std::endl;
-	stream << "          ctx->exec_content_init(ctx, USCXML_GET_STATE(i).data);" << std::endl;
-	stream << "        }" << std::endl;
-	stream << "        BIT_SET_AT(i, ctx->initialized_data);" << std::endl;
-	stream << "      }" << std::endl;
-	stream << std::endl;
-
-#endif
-
 	stream << "         if" << std::endl;
 	stream << "         :: !" << _prefix << "initialized_data[i] -> {" << std::endl;
 	stream << "           /* TODO: late data binding not supported yet */" << std::endl;
@@ -2119,22 +2128,15 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
 	stream << "         :: else -> skip;" << std::endl;
 	stream << "         fi" << std::endl;
 	stream << std::endl;
-
-#if 0
-	stream << "      if (USCXML_GET_STATE(i).on_entry != NULL) {" << std::endl;
-	stream << "        if unlikely((err = USCXML_GET_STATE(i).on_entry(ctx, &USCXML_GET_STATE(i), ctx->event)) != USCXML_ERR_OK)" << std::endl;
-	stream << "          return err;" << std::endl;
-	stream << "      }" << std::endl;
-	stream << std::endl;
-
 #endif
-
+    
 	stream << "         /* Process executable content for entering a state */" << std::endl;
 	stream << "         if" << std::endl;
 	for (auto i = 0; i < _states.size(); i++) {
 		std::list<DOMElement*> onentries = DOMUtils::filterChildElements(XML_PREFIX(_states[i]).str() + "onentry" , _states[i]);
 		if (onentries.size() > 0) {
 			stream << "         :: i == " << toStr(i) << " -> {" << std::endl;
+            TRACE_EXECUTION_V("Processing executable content for entering state %d", "i");
 			for (auto onentry : onentries)
 				writeExecContent(stream, onentry, 5);
 			stream << "         }" << std::endl;
@@ -2144,136 +2146,172 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
 	stream << "         fi" << std::endl;
 	stream << std::endl;
 
-#if 0
-	stream << "      /* take history and initial transitions */" << std::endl;
-	stream << "      for (j = 0; j < USCXML_NUMBER_TRANS; j++) {" << std::endl;
-	stream << "        if unlikely(BIT_HAS(j, trans_set) &&" << std::endl;
-	stream << "              (ctx->machine->transitions[j].type & (USCXML_TRANS_HISTORY | USCXML_TRANS_INITIAL)) &&" << std::endl;
-	stream << "              ctx->machine->states[ctx->machine->transitions[j].source].parent == i) {" << std::endl;
-	stream << "          /* call executable content in transition */" << std::endl;
-	stream << "          if (ctx->machine->transitions[j].on_transition != NULL) {" << std::endl;
-	stream << "            if unlikely((err = ctx->machine->transitions[j].on_transition(ctx," << std::endl;
-	stream << "                                            &USCXML_GET_STATE(i)," << std::endl;
-	stream << "                                            ctx->event)) != USCXML_ERR_OK)" << std::endl;
-	stream << "              return err;" << std::endl;
-	stream << "          }" << std::endl;
-	stream << "        }" << std::endl;
-	stream << "      }" << std::endl;
-	stream << std::endl;
-
-#endif
-
 	stream << "         /* take history and initial transitions */" << std::endl;
-	stream << "         j = 0;" << std::endl;
-	stream << "         do" << std::endl;
-	stream << "         :: j < USCXML_NUMBER_TRANS -> {" << std::endl;
-	stream << "           if" << std::endl;
-	stream << "           :: (trans_set[j] &&" << std::endl;
-	stream << "              (" << _prefix << "transitions[j].type[USCXML_TRANS_HISTORY] ||" << std::endl;
-	stream << "               " << _prefix << "transitions[j].type[USCXML_TRANS_INITIAL]) && " << std::endl;
-	stream << "               " << _prefix << "states[" << _prefix << "transitions[j].source].parent == i) -> {" << std::endl;
-	stream << "              /* Call executable content in history or initial transition */" << std::endl;
-    stream << "              if" << std::endl;
-    for (auto i = 0; i < _transitions.size(); i++) {
-        stream << "              :: j == " << toStr(i) << " -> {" << std::endl;
-        writeExecContent(stream, _transitions[i], 8);
-        stream << "                skip;" << std::endl;
-        stream << "              }" << std::endl;
+    if (_transitions.size() > 0) {
+        stream << "         j = 0;" << std::endl;
+        stream << "         do" << std::endl;
+        stream << "         :: j < " << _prefix << "USCXML_NUMBER_TRANS -> {" << std::endl;
+        stream << "           if" << std::endl;
+        stream << "           :: (" << _prefix << "ctx.trans_set[j] &&" << std::endl;
+        stream << "              (" << _prefix << "transitions[j].type[USCXML_TRANS_HISTORY] ||" << std::endl;
+        stream << "               " << _prefix << "transitions[j].type[USCXML_TRANS_INITIAL]) && " << std::endl;
+        stream << "               " << _prefix << "states[" << _prefix << "transitions[j].source].parent == i) -> {" << std::endl;
+        stream << "              /* Call executable content in history or initial transition */" << std::endl;
+        stream << "              if" << std::endl;
+        for (auto i = 0; i < _transitions.size(); i++) {
+            stream << "              :: j == " << toStr(i) << " -> {" << std::endl;
+            TRACE_EXECUTION_V("Processing executable content for transition %d", "j");
+
+            writeExecContent(stream, _transitions[i], 8);
+            stream << "                skip;" << std::endl;
+            stream << "              }" << std::endl;
+        }
+        stream << "              :: else ->skip;" << std::endl;
+        stream << "              fi" << std::endl;
+        stream << std::endl;
+
+        stream << "           }" << std::endl;
+        stream << "           :: else -> skip;" << std::endl;
+        stream << "           fi" << std::endl;
+        stream << "           j = j + 1;" << std::endl;
+        stream << "         }" << std::endl;
+        stream << "         :: else -> break;" << std::endl;
+        stream << "         od" << std::endl;
     }
-    stream << "              :: else ->skip;" << std::endl;
-    stream << "              fi" << std::endl;
-    stream << std::endl;
-
-	stream << "           }" << std::endl;
-	stream << "           :: else -> skip;" << std::endl;
-	stream << "           fi" << std::endl;
-	stream << "           j = j + 1;" << std::endl;
-	stream << "         }" << std::endl;
-	stream << "         :: else -> break;" << std::endl;
-	stream << "         od" << std::endl;
-
-
-#if 0
-	stream << "      /* handle final states */" << std::endl;
-	stream << "      if unlikely(USCXML_STATE_MASK(USCXML_GET_STATE(i).type) == USCXML_STATE_FINAL) {" << std::endl;
-#endif
 
 	stream << "         /* handle final states */" << std::endl;
 	stream << "         if" << std::endl;
 	stream << "         :: " << _prefix << "states[i].type[USCXML_STATE_FINAL] -> {" << std::endl;
 
-
-#if 0
-	stream << "        if unlikely(USCXML_GET_STATE(i).ancestors[0] == 0x01) {" << std::endl;
-	stream << "          ctx->flags |= USCXML_CTX_TOP_LEVEL_FINAL;" << std::endl;
-	stream << "        } else {" << std::endl;
-	stream << "          /* raise done event */" << std::endl;
-	stream << "          const uscxml_elem_donedata* donedata = &ctx->machine->donedata[0];" << std::endl;
-	stream << "          while(USCXML_ELEM_DONEDATA_IS_SET(donedata)) {" << std::endl;
-	stream << "            if unlikely(donedata->source == i)" << std::endl;
-	stream << "              break;" << std::endl;
-	stream << "            donedata++;" << std::endl;
-	stream << "          }" << std::endl;
-	stream << "          ctx->raise_done_event(ctx, &ctx->machine->states[USCXML_GET_STATE(i).parent], (USCXML_ELEM_DONEDATA_IS_SET(donedata) ? donedata : NULL));" << std::endl;
-	stream << "        }" << std::endl;
-#endif
-
 	stream << "           if" << std::endl;
 	stream << "           :: " << _prefix << "states[" << _prefix << "states[i].parent].children[1] -> {" << std::endl;
-	stream << "            " << _prefix << "flags[USCXML_CTX_TOP_LEVEL_FINAL] = true;" << std::endl;
+    stream << "             /* exit topmost SCXML state */" << std::endl;
+    stream << "             " << _prefix << "flags[USCXML_CTX_TOP_LEVEL_FINAL] = true;" << std::endl;
+    stream << "             " << _prefix << "flags[USCXML_CTX_FINISHED] = true;" << std::endl;
 	stream << "           }" << std::endl;
 	stream << "           :: else -> {" << std::endl;
-	stream << "             /* TODO: raise done event */" << std::endl;
-	stream << "             skip;" << std::endl;
+    stream << "             /* raise done event */" << std::endl;
+    stream << "             if" << std::endl;
+
+    std::string insertOp = "!";
+//    if (_analyzer->usesEventField("delay"))
+//        insertOp += "!";
+
+    for (auto state : _states) {
+        if (state->getParentNode() == NULL || state->getParentNode()->getNodeType() != DOMNode::ELEMENT_NODE)
+            continue;
+        
+        if (!isFinal(state))
+            continue;
+        
+        DOMElement* parent = static_cast<DOMElement*>(state->getParentNode());
+        if (!HAS_ATTR(parent, "id"))
+            continue;
+
+        std::string doneEvent = _analyzer->macroForLiteral("done.state." + ATTR_CAST(state->getParentNode(), "id"));
+
+        stream << "             :: (i == " << ATTR(state, "documentOrder") << ") -> {" << std::endl;
+
+        if (_analyzer->usesComplexEventStruct()) {
+            std::string typeReset = _analyzer->getTypeReset(_prefix + "_tmpE", _analyzer->getType("_event"), 7);
+            stream << typeReset << std::endl;
+            stream << "               " << _prefix << "_tmpE.name = " << doneEvent << ";" << std::endl;
+
+            std::list<DOMElement*> donedatas = DOMUtils::filterChildElements(XML_PREFIX(state).str() + "donedata" , state);
+            if (donedatas.size() > 0) {
+                writeRaiseDoneDate(stream, donedatas.front(), 8);
+            }
+            
+            doneEvent = _prefix + "_tmpE";
+        }
+        
+
+        stream << "               " << _prefix << "iQ" << insertOp << doneEvent << ";" << std::endl;
+        stream << "             }" << std::endl;
+
+    }
+    stream << "             :: else -> skip;" << std::endl;
+    stream << "             fi" << std::endl;
+    
 	stream << "           }" << std::endl;
 	stream << "           fi" << std::endl;
 
+    stream << "           /**" << std::endl;
+    stream << "            * are we the last final state to leave a parallel state?:" << std::endl;
+	stream << "            * 1. Gather all parallel states in our ancestor chain" << std::endl;
+	stream << "            * 2. Find all states for which these parallels are ancestors" << std::endl;
+	stream << "            * 3. Iterate all active final states and remove their ancestors" << std::endl;
+	stream << "            * 4. If a state remains, not all children of a parallel are final" << std::endl;
+	stream << "            */" << std::endl;
+    stream << "            j = 0;" << std::endl;
+    stream << "            do" << std::endl;
+    stream << "            :: j < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
+    stream << "              if" << std::endl;
+    stream << "              :: " << _prefix << "states[j].type[USCXML_STATE_PARALLEL] && " << _prefix << "states[i].ancestors[j] -> {" << std::endl;
+    stream << "                " << _prefix << "STATES_CLEAR(" << _prefix << "ctx.tmp_states)" << std::endl;
 
-#if 0
-	stream << std::endl;
-	stream << "        /**" << std::endl;
-	stream << "         * are we the last final state to leave a parallel state?:" << std::endl;
-	stream << "         * 1. Gather all parallel states in our ancestor chain" << std::endl;
-	stream << "         * 2. Find all states for which these parallels are ancestors" << std::endl;
-	stream << "         * 3. Iterate all active final states and remove their ancestors" << std::endl;
-	stream << "         * 4. If a state remains, not all children of a parallel are final" << std::endl;
-	stream << "         */" << std::endl;
-	stream << "        for (j = 0; j < USCXML_NUMBER_STATES; j++) {" << std::endl;
-	stream << "          if unlikely(USCXML_STATE_MASK(ctx->machine->states[j].type) == USCXML_STATE_PARALLEL &&" << std::endl;
-	stream << "                BIT_HAS(j, USCXML_GET_STATE(i).ancestors)) {" << std::endl;
-	stream << "            bit_clear_all(tmp_states, nr_states_bytes);" << std::endl;
-	stream << "            for (k = 0; k < USCXML_NUMBER_STATES; k++) {" << std::endl;
-	stream << "              if unlikely(BIT_HAS(j, ctx->machine->states[k].ancestors) && BIT_HAS(k, ctx->config)) {" << std::endl;
-	stream << "                if (USCXML_STATE_MASK(ctx->machine->states[k].type) == USCXML_STATE_FINAL) {" << std::endl;
-	stream << "                  bit_and_not(tmp_states, ctx->machine->states[k].ancestors, nr_states_bytes);" << std::endl;
-	stream << "                } else {" << std::endl;
-	stream << "                  BIT_SET_AT(k, tmp_states);" << std::endl;
-	stream << "                }" << std::endl;
-	stream << "              }" << std::endl;
-	stream << "            }" << std::endl;
-	stream << "            if unlikely(!bit_has_any(tmp_states, nr_states_bytes)) {" << std::endl;
-	stream << "              ctx->raise_done_event(ctx, &ctx->machine->states[j], NULL);" << std::endl;
-	stream << "            }" << std::endl;
-	stream << "          }" << std::endl;
-	stream << "        }" << std::endl;
-	stream << "      }" << std::endl;
-	stream << "    }" << std::endl;
-	stream << "  }" << std::endl;
-	stream << std::endl;
+    stream << "                k = 0;" << std::endl;
+    stream << "                do" << std::endl;
+    stream << "                :: k < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
+    stream << "                  if" << std::endl;
+    stream << "                  :: " << _prefix << "states[k].ancestors[j] && " << _prefix << "config[k] -> {" << std::endl;
+    stream << "                    if" << std::endl;
+    stream << "                    :: " << _prefix << "states[k].type[USCXML_STATE_FINAL] -> {" << std::endl;
+    
+    stream << "                      " << _prefix << "STATES_AND_NOT(" << _prefix << "ctx.tmp_states, " << _prefix << "states[k].ancestors)" << std::endl;
+    stream << "                    }" << std::endl;
+    stream << "                    :: else -> {" << std::endl;
+    
+    stream << "                      " << _prefix << "ctx.tmp_states[k] = true;" << std::endl;
+    stream << "                    }" << std::endl;
+    stream << "                    fi" << std::endl;
+    stream << "                  }" << std::endl;
+    stream << "                  :: else -> skip;" << std::endl;
+    stream << "                  fi" << std::endl;
+    stream << "                  k = k + 1;" << std::endl;
+    stream << "                }" << std::endl;
+    stream << "                :: else -> break;" << std::endl;
+    stream << "                od" << std::endl;
+    stream << "                if" << std::endl;
+    stream << "                :: !" << _prefix << "STATES_HAS_ANY(" << _prefix << "ctx.tmp_states) -> {" << std::endl;
+    stream << "                  if" << std::endl;
 
-	stream << "  return USCXML_ERR_OK;" << std::endl;
-	stream << "}" << std::endl;
-	stream << std::endl;
-	stream << std::endl;
-#endif
+    for (auto state : _states) {
+        if (isParallel(state) && HAS_ATTR(state, "id")) {
+            stream << "                  :: j == " << toStr(ATTR(state, "documentOrder")) << " -> {" << std::endl;
+
+            std::string doneEvent = _analyzer->macroForLiteral("done.state." + ATTR(state, "id"));
+
+            if (_analyzer->usesComplexEventStruct()) {
+                std::string typeReset = _analyzer->getTypeReset(_prefix + "_tmpE", _analyzer->getType("_event"), 10);
+                stream << typeReset << std::endl;
+                stream << "                    " << _prefix << "_tmpE.name = " << doneEvent << ";" << std::endl;
+
+                std::list<DOMElement*> donedatas = DOMUtils::filterChildElements(XML_PREFIX(state).str() + "donedata" , state);
+                if (donedatas.size() > 0) {
+                    writeRaiseDoneDate(stream, donedatas.front(), 11);
+                }
+                doneEvent = _prefix + "_tmpE";
+            }
+            
+            stream << "                    " << _prefix << "iQ" << insertOp << doneEvent << ";" << std::endl;
+            stream << "                  }" << std::endl;
+        }
+    }
+    
+    stream << "                  :: else -> skip;" << std::endl;
+    stream << "                  fi" << std::endl;
 
-	stream << "           /** TODO:" << std::endl;
-	stream << "          * are we the last final state to leave a parallel state?:" << std::endl;
-	stream << "          * 1. Gather all parallel states in our ancestor chain" << std::endl;
-	stream << "          * 2. Find all states for which these parallels are ancestors" << std::endl;
-	stream << "          * 3. Iterate all active final states and remove their ancestors" << std::endl;
-	stream << "          * 4. If a state remains, not all children of a parallel are final" << std::endl;
-	stream << "          */" << std::endl;
+    stream << "                }" << std::endl;
+    stream << "                :: else -> skip;" << std::endl;
+    stream << "                fi" << std::endl;
+    stream << "              }" << std::endl;
+    stream << "              :: else -> skip;" << std::endl;
+    stream << "              fi" << std::endl;
+    stream << "              j = j + 1;" << std::endl;
+    stream << "            }" << std::endl;
+    stream << "            :: else -> break;" << std::endl;
+    stream << "            od" << std::endl;
 
 
 	stream << "         }" << std::endl;
@@ -2288,150 +2326,120 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
 	stream << "    fi;" << std::endl;
 	stream << "  }" << std::endl;
 	stream << "  :: else -> break;" << std::endl;
-	stream << "  od;" << std::endl;
-	stream << std::endl;
-
-	stream << "#if TRACE_EXECUTION" << std::endl;
-	stream << "printf(\"Done\\n\");" << std::endl;
-	stream << "#endif" << std::endl;
-
-	stream << "}" << std::endl;
+    stream << "  od;" << std::endl;
+    stream << "  }" << std::endl;
+    stream << "  :: else -> skip;" << std::endl;
+    stream << "  fi" << std::endl;
+    stream << "} }" << std::endl;
 	stream << ":: else -> break;" << std::endl;
 	stream << "od" << std::endl;
+    stream << std::endl;
+    stream << "/* ---------------------------- */" << std::endl;
+    stream << _prefix << "TERMINATE_MACHINE:" << std::endl;
 
+    TRACE_EXECUTION("Machine finished");
+    
+    stream << "/* exit all remaining states */" << std::endl;
+    stream << "i = " << _prefix << "USCXML_NUMBER_STATES;" << std::endl;
+    stream << "do" << std::endl;
+    stream << ":: i > 0 -> {" << std::endl;
+    stream << "  i = i - 1;" << std::endl;
+    stream << "  if" << std::endl;
+    stream << "  :: " << _prefix << "config[i] && " << _prefix << "flags[USCXML_CTX_TOP_LEVEL_FINAL] -> {" << std::endl;
+    stream << "    /* call all on exit handlers */" << std::endl;
+    stream << "   if" << std::endl;
+    for (auto i = 0; i < _states.size(); i++) {
+        std::list<DOMElement*> onentries = DOMUtils::filterChildElements(XML_PREFIX(_states[i]).str() + "onexit" , _states[i]);
+        if (onentries.size() > 0) {
+            stream << "    :: i == " << toStr(i) << " -> {" << std::endl;
+            TRACE_EXECUTION_V("Processing executable content for exiting state %d", "i");
+            for (auto onentry : onentries)
+                writeExecContent(stream, onentry, 2);
+            stream << "    }" << std::endl;
+        }
+    }
+    stream << "    :: else -> skip;" << std::endl;
+    stream << "    fi" << std::endl;
+    stream << std::endl;
+    stream << "    skip;" << std::endl;
+    stream << "    " << std::endl;
+    stream << "  }" << std::endl;
+    stream << "  :: else -> skip;" << std::endl;
+    stream << "  fi;" << std::endl;
+    stream << std::endl;
+    
+    stream << "  if" << std::endl;
+    stream << "  :: " << _prefix << "invocations[i] -> {" << std::endl;
+    stream << "    /* cancel invocations */" << std::endl;
+    stream << "    " << _prefix << "invocations[i] = false;" << std::endl;
+    stream << "    if" << std::endl;
+    
+    for (auto machine : _machinesNested) {
+        stream << "    :: i == " << ATTR_CAST(machine.first->getParentNode(), "documentOrder") << " -> {" << std::endl;
+        stream << "      " << machine.second->_prefix << "flags[USCXML_CTX_FINISHED] = true;" << std::endl;
+        stream << "    }" << std::endl;
+    }
+    stream << "    :: else -> skip;" << std::endl;
+    stream << "    fi" << std::endl;
+    
+    stream << "    skip;" << std::endl;
+    stream << std::endl;
+    stream << "  }" << std::endl;
+    stream << "  :: else -> skip;" << std::endl;
+    stream << "  fi;" << std::endl;
+    stream << "}" << std::endl;
+    stream << ":: else -> break;" << std::endl;
+    stream << "od;" << std::endl;
+    stream << std::endl;
 
-	stream << "} }" << std::endl;
-	stream << std::endl;
-
-}
-
-#if 0
-
-void ChartToPromela::writeProgram(std::ostream& stream) {
-
-	_traceTransitions = envVarIsTrue("USCXML_PROMELA_TRANSITION_TRACE");
-	_writeTransitionPrintfs = envVarIsTrue("USCXML_PROMELA_TRANSITION_DEBUG");
-
-	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;
-	}
-
-	//	std::cerr << _scxml << std::endl;
-
-	stream << "/* " << (std::string)_baseURL << " */" << std::endl;
-	stream << std::endl;
-
-	initNodes();
-
-	for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator nestedIter = _machines.begin(); nestedIter != _machines.end(); nestedIter++) {
-		if (nestedIter->second->_start == NULL) {
-			nestedIter->second->interpret();
-		}
-		nestedIter->second->initNodes();
-	}
-
-	writeEvents(stream);
-	stream << std::endl;
-	writeStates(stream);
-	stream << std::endl;
-	writeStrings(stream);
-	stream << std::endl;
-	if (_analyzer->usesInPredicate()) {
-		writeStateMap(stream);
-		stream << std::endl;
-	}
-	if (_historyMembers.size() > 0) {
-		writeHistoryArrays(stream);
-		stream << std::endl;
-	}
-	writeTypeDefs(stream);
-	stream << std::endl;
-	writeDeclarations(stream);
-	stream << std::endl;
-
-	for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator nestedIter = _machines.begin(); nestedIter != _machines.end(); nestedIter++) {
-		nestedIter->second->writeDeclarations(stream);
-		stream << std::endl;
-	}
-
-	stream << std::endl << "/* global inline functions */" << std::endl;
-
-	if (_analyzer->usesComplexEventStruct()) {
-		stream << "hidden _event_t tmpE;" << std::endl;
-	} else {
-		stream << "hidden int tmpE;" << std::endl;
-	}
-	stream << "hidden int tmpIndex;" << std::endl;
-
+    if (_machinesAll->size() > 1 && _analyzer->usesEventField("delay")) {
+        /* TODO: We nee to clear all events if we were canceled */
+        TRACE_EXECUTION("Removing pending events");
+        stream << "removePendingEventsFromInvoker(" << _analyzer->macroForLiteral(_invokerid) << ")" << std::endl;
+    }
 
-#if NEW_DELAY_RESHUFFLE
-	if (_analyzer->usesEventField("delay")) {
-		writeInsertWithDelay(stream);
-		stream << std::endl;
-	}
-#endif
+    
+    if (_parent != NULL) {
+        stream << "/* send done event */" << std::endl;
+        stream << "if" << std::endl;
+        stream << ":: " << _prefix << "flags[USCXML_CTX_TOP_LEVEL_FINAL] -> {" << std::endl;
+
+        if (_analyzer->usesComplexEventStruct()) {
+            std::string typeReset = _analyzer->getTypeReset(_prefix + "_tmpE", _analyzer->getType("_event"), 2);
+            stream << typeReset << std::endl;
+            stream << "    " << _prefix << "_tmpE.name = " << _analyzer->macroForLiteral("done.invoke." + _invokerid) << std::endl;
+            
+            if (_analyzer->usesEventField("invokeid")) {
+                stream << "    " << _prefix << "_tmpE.invokeid = " << _analyzer->macroForLiteral(_invokerid) << std::endl;
+            }
+            
+        } else {
+            stream << "    " << _prefix << "_tmpE = " << _analyzer->macroForLiteral("done.invoke." + _invokerid) << std::endl;
+        }
+        
+        
+        TRACE_EXECUTION("Sending DONE.INVOKE");
+        
+        stream << "    " << _parent->_prefix << "eQ!" << _prefix << "_tmpE;" << std::endl;
+        if (_analyzer->usesEventField("delay")) {
+            stream << "    insertWithDelay(" << _parent->_prefix << "eQ);" << std::endl;
+        }
+        stream << "}" << std::endl;
+        stream << ":: else -> skip" << std::endl;
+        stream << "fi" << std::endl;
+        stream << std::endl;
 
-	if (_analyzer->usesEventField("delay") && _machines.size() > 0) {
-		writeDetermineShortestDelay(stream);
-		stream << std::endl;
-		writeAdvanceTime(stream);
-		stream << std::endl;
-		writeRescheduleProcess(stream);
-		stream << std::endl;
-		writeScheduleMachines(stream);
-		stream << std::endl;
-	}
+    }
+    
+    stream << std::endl;
+    
+    TRACE_EXECUTION("Done");
 
-	{
-		NodeSet<std::string> cancels = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "cancel", _scxml, true);
-		if (cancels.size() > 0) {
-			writeCancelEvents(stream);
-			stream << std::endl;
-		}
-	}
-	{
-		NodeSet<std::string> invokes = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true);
-		if (invokes.size() > 0 && _analyzer->usesEventField("delay")) {
-			writeRemovePendingEventsFromInvoker(stream);
-			stream << std::endl;
-		}
 
-	}
-	stream << std::endl;
-	writeEventSources(stream);
-	stream << std::endl;
-	writeFSM(stream);
-	stream << std::endl;
-	writeMain(stream);
+	stream << "} }" << std::endl;
 	stream << std::endl;
 
-	for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator nestedIter = _machines.begin(); nestedIter != _machines.end(); nestedIter++) {
-		nestedIter->second->writeFSM(stream);
-		stream << std::endl;
-	}
-
-	// write ltl expression for success
-	std::stringstream acceptingStates;
-	std::string seperator;
-
-	for (std::map<std::string, GlobalState*>::iterator stateIter = _activeConf.begin(); stateIter != _activeConf.end(); stateIter++) {
-		FlatStateIdentifier flatId(stateIter->first);
-		if (std::find(flatId.getActive().begin(), flatId.getActive().end(), "pass") != flatId.getActive().end()) {
-			acceptingStates << seperator << _prefix << "s == s" << stateIter->second->activeIndex;
-			seperator = " || ";
-		}
-	}
-	if (acceptingStates.str().size() > 0) {
-		stream << "ltl { eventually (" << acceptingStates.str() << ") }" << std::endl;
-	}
 }
-#endif
 
 void ChartToPromela::writeIfBlock(std::ostream& stream, std::list<DOMElement*>& condChain, size_t indent) {
 	if (condChain.size() == 0)
@@ -2534,7 +2542,7 @@ std::string ChartToPromela::dataToAssignments(const std::string& prefix, const D
 	std::stringstream retVal;
 	if (data.atom.size() > 0) {
 		if (data.type == Data::VERBATIM) {
-			retVal << prefix << " = " << _analyzer.macroForLiteral(data.atom) << ";" << std::endl;
+			retVal << prefix << " = " << _analyzer->macroForLiteral(data.atom) << ";" << std::endl;
 		} else {
 			retVal << prefix << " = " << data.atom << ";" << std::endl;
 		}
@@ -2588,30 +2596,279 @@ std::string ChartToPromela::declForRange(const std::string& identifier, long min
 	}
 }
 
+void ChartToPromela::writeDetermineShortestDelay(std::ostream& stream, int indent) {
+    std::string padding;
+    for (size_t i = 0; i < indent; i++) {
+        padding += "  ";
+    }
+    
+    stream << padding << "inline determineSmallestDelay(smallestDelay, queue) {" << std::endl;
+    //    stream << padding << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), "  ");
+    stream << padding << "  if" << std::endl;
+    stream << padding << "  :: len(queue) > 0 -> {" << std::endl;
+    stream << padding << "    queue?<tmpE>;" << std::endl;
+    stream << padding << "    if" << std::endl;
+    stream << padding << "    :: (tmpE.delay < smallestDelay) -> { smallestDelay = tmpE.delay; }" << std::endl;
+    stream << padding << "    :: else -> skip;" << std::endl;
+    stream << padding << "    fi;" << std::endl;
+    stream << padding << "  }" << std::endl;
+    stream << padding << "  :: else -> skip;" << std::endl;
+    stream << padding << "  fi;" << std::endl;
+    stream << padding << "}" << std::endl;
+}
+
+void ChartToPromela::writeScheduleMachines(std::ostream& stream, int indent) {
+    std::string padding;
+    for (size_t i = 0; i < indent; i++) {
+        padding += "  ";
+    }
+    
+    stream << padding << "inline scheduleMachines() {" << std::endl;
+    std::list<std::string> queues;
+    queues.push_back("eQ");
+    
+    if (_allowEventInterleaving)
+        queues.push_back("tmpQ");
+    
+    stream << "  /* schedule state-machines with regard to their event's delay */" << std::endl;
+    stream << "  skip;" << std::endl;
+    stream << "  d_step {" << std::endl;
+    
+    stream << std::endl << "/* determine smallest delay */" << std::endl;
+    stream << "    int smallestDelay = 2147483647;" << std::endl;
+    
+    for (auto machine : *_machinesAll) {
+        for (auto queue : queues) {
+            stream << "    determineSmallestDelay(smallestDelay, " << machine.second->_prefix << queue << ");" << std::endl;
+        }
+    }
+    
+    TRACE_EXECUTION_V("Smallest delay is %d", "smallestDelay");
+    
+    stream << std::endl << "/* prioritize processes with lowest delay or internal events */" << std::endl;
+    
+    for (auto machine : *_machinesAll) {
+        stream << "    rescheduleProcess(smallestDelay, "
+        << machine.second->_prefix << "procid, "
+        << machine.second->_prefix << "iQ, "
+        << machine.second->_prefix << "eQ";
+        if (_allowEventInterleaving) {
+            stream << ", " << machine.second->_prefix << "tmpQ);" << std::endl;
+        } else {
+            stream << ");" << std::endl;
+        }
+    }
+    
+    stream << std::endl << "/* advance time by subtracting the smallest delay from all event delays */" << std::endl;
+    stream << "    if" << std::endl;
+    stream << "    :: (smallestDelay > 0) -> {" << std::endl;
+    for (auto machine : *_machinesAll) {
+        for (auto queue : queues) {
+            stream << "      advanceTime(smallestDelay, " << machine.second->_prefix << queue << ");" << std::endl;
+        }
+    }
+    stream << "    }" << std::endl;
+    stream << "    :: else -> skip;" << std::endl;
+    stream << "    fi;" << std::endl;
+    stream << "  }" << std::endl;
+    stream << "  set_priority(_pid, 10);" << std::endl << std::endl;
+    stream << padding << "}" << std::endl;
+}
+
+void ChartToPromela::writeAdvanceTime(std::ostream& stream, int indent) {
+    std::string padding;
+    for (size_t i = 0; i < indent; i++) {
+        padding += "  ";
+    }
+    
+    stream << padding << "inline advanceTime(increment, queue) {" << std::endl;
+    stream << padding << "  tmpIndex = 0;" << std::endl;
+    stream << padding << "  do" << std::endl;
+    stream << padding << "  :: tmpIndex < len(queue) -> {" << std::endl;
+    stream << padding << "    queue?tmpE;" << std::endl;
+    stream << padding << "    if" << std::endl;
+    stream << padding << "    :: tmpE.delay >= increment -> tmpE.delay = tmpE.delay - increment;" << std::endl;
+    stream << padding << "    :: else -> skip;" << std::endl;
+    stream << padding << "    fi" << std::endl;
+    stream << padding << "    queue!tmpE;" << std::endl;
+    stream << padding << "    tmpIndex++;" << std::endl;
+    stream << padding << "  }" << std::endl;
+    stream << padding << "  :: else -> break;" << std::endl;
+    stream << padding << "  od" << std::endl;
+    stream << padding << "}" << std::endl;
+}
+
+void ChartToPromela::writeInsertWithDelay(std::ostream& stream, int indent) {
+    std::string padding;
+    for (size_t i = 0; i < indent; i++) {
+        padding += "  ";
+    }
+    
+    uint32_t maxExternalQueueLength = 1;
+    for(auto machine : *_machinesAll) {
+        maxExternalQueueLength = MAX(maxExternalQueueLength, machine.second->_externalQueueLength);
+    }
+    
+    maxExternalQueueLength += 6;
+    
+    if (maxExternalQueueLength <= 1) {
+        stream << padding << "/* noop for external queues with length <= 1 */" << std::endl;
+        stream << padding << "inline insertWithDelay(queue) {}" << std::endl;
+    }
+    
+    stream << padding << "hidden _event_t _iwdQ[" << maxExternalQueueLength - 1 << "];" << std::endl;
+    stream << padding << "hidden int _iwdQLength = 0;" << std::endl;
+    stream << padding << "hidden int _iwdIdx1 = 0;" << std::endl;
+    stream << padding << "hidden int _iwdIdx2 = 0;" << std::endl;
+    stream << padding << "hidden _event_t _iwdTmpE;" << std::endl;
+    stream << padding << "hidden _event_t _iwdLastE;" << std::endl;
+    stream << padding << "bool _iwdInserted = false;" << std::endl;
+    stream << padding << "" << std::endl;
+    stream << padding << "/* last event in given queue is potentially at wrong position */" << std::endl;
+    stream << padding << "inline insertWithDelay(queue) {" << std::endl;
+    stream << padding << "  d_step {" << std::endl;
+    stream << padding << "" << std::endl;
+    stream << padding << "    /* only process for non-trivial queues */" << std::endl;
+    stream << padding << "    if" << std::endl;
+    stream << padding << "    :: len(queue) > 1 -> {" << std::endl;
+    
+    TRACE_EXECUTION("Reshuffling events")
+    
+    stream << padding << "" << std::endl;
+    stream << padding << "      /* move all events but last over and remember the last one */" << std::endl;
+    stream << padding << "      _iwdIdx1 = 0;" << std::endl;
+    stream << padding << "      _iwdQLength = len(queue) - 1;" << std::endl;
+    stream << padding << "" << std::endl;
+    stream << padding << "      do" << std::endl;
+    stream << padding << "      :: _iwdIdx1 < _iwdQLength -> {" << std::endl;
+    stream << padding << "        queue?_iwdTmpE;" << std::endl;
+    stream << padding << "        _iwdQ[_iwdIdx1].name = _iwdTmpE.name;" << std::endl;
+    
+    stream << _analyzer->getTypeAssignment("_iwdQ[_iwdIdx1]", "_iwdTmpE", _analyzer->getType("_event"), 8);
+    
+    stream << padding << "        _iwdIdx1++;" << std::endl;
+    stream << padding << "      }" << std::endl;
+    stream << padding << "      :: else -> break;" << std::endl;
+    stream << padding << "      od" << std::endl;
+    stream << padding << "" << std::endl;
+    stream << padding << "      queue?_iwdLastE;" << std::endl;
+
+    stream << padding << "" << std::endl;
+    stream << padding << "      /* _iwdQ now contains all but last item in _iwdLastE */" << std::endl;
+    stream << padding << "      assert(len(queue) == 0);" << std::endl;
+    stream << padding << "" << std::endl;
+    stream << padding << "      /* reinsert into queue and place _iwdLastE correctly */" << std::endl;
+    stream << padding << "      _iwdInserted = false;" << std::endl;
+    stream << padding << "      _iwdIdx2 = 0;" << std::endl;
+    stream << padding << "" << std::endl;
+    stream << padding << "      do" << std::endl;
+    stream << padding << "      :: _iwdIdx2 < _iwdIdx1 -> {" << std::endl;
+    stream << padding << "        _iwdTmpE.name = _iwdQ[_iwdIdx2].name;" << std::endl;
+    
+    stream << _analyzer->getTypeAssignment("_iwdTmpE", "_iwdQ[_iwdIdx2]", _analyzer->getType("_event"), 4);
+    
+    stream << padding << "" << std::endl;
+    stream << padding << "        if" << std::endl;
+    stream << padding << "        :: _iwdTmpE.delay > _iwdLastE.delay && !_iwdInserted -> {" << std::endl;
+    stream << padding << "          queue!_iwdLastE;" << std::endl;
+    TRACE_EXECUTION_V("Event %d has delay %d (last)", "_iwdLastE.name, _iwdLastE.delay");
+    
+    stream << padding << "          _iwdInserted = true;" << std::endl;
+    stream << padding << "        }" << std::endl;
+    stream << padding << "        :: else -> skip" << std::endl;
+    stream << padding << "        fi;" << std::endl;
+    stream << padding << "" << std::endl;
+    stream << padding << "        queue!_iwdTmpE;" << std::endl;
+    TRACE_EXECUTION_V("Event %d has delay %d", "_iwdTmpE.name, _iwdTmpE.delay");
+
+    stream << padding << "        _iwdIdx2++;" << std::endl;
+    stream << padding << "      }" << std::endl;
+    stream << padding << "      :: else -> break;" << std::endl;
+    stream << padding << "      od" << std::endl;
+    stream << padding << "" << std::endl;
+    stream << padding << "      if" << std::endl;
+    stream << padding << "      :: !_iwdInserted -> {" << std::endl;
+    stream << padding << "         queue!_iwdLastE;" << std::endl;
+    TRACE_EXECUTION_V("Event %d has delay %d (last)", "_iwdLastE.name, _iwdLastE.delay");
+    stream << padding << "      }" << std::endl;
+    stream << padding << "      :: else -> skip;" << std::endl;
+    stream << padding << "      fi;" << std::endl;
+    stream << padding << "" << std::endl;
+    stream << padding << "    }" << std::endl;
+    stream << padding << "    :: else -> skip;" << std::endl;
+    stream << padding << "    fi;" << std::endl;
+    stream << padding << "  }" << std::endl;
+    stream << padding << "}" << std::endl;
+}
+
+void ChartToPromela::writeRescheduleProcess(std::ostream& stream, int indent) {
+    std::string padding;
+    for (size_t i = 0; i < indent; i++) {
+        padding += "  ";
+    }
+    
+    if (_allowEventInterleaving) {
+        stream << padding << "inline rescheduleProcess(smallestDelay, procId, internalQ, externalQ, tempQ) {" << std::endl;
+    } else {
+        stream << padding << "inline rescheduleProcess(smallestDelay, procId, internalQ, externalQ) {" << std::endl;
+    }
+    //    stream << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), "      ");
+    
+    stream << padding << "  set_priority(procId, 1);" << std::endl;
+    stream << padding << "  if" << std::endl;
+    stream << padding << "  :: len(internalQ) > 0 -> set_priority(procId, 10);" << std::endl;
+    stream << padding << "  :: else {" << std::endl;
+    stream << padding << "    if" << std::endl;
+    
+    stream << padding << "    :: len(externalQ) > 0 -> {" << std::endl;
+    stream << padding << "      externalQ?<tmpE>;" << std::endl;
+    stream << padding << "      if" << std::endl;
+    stream << padding << "      :: smallestDelay == tmpE.delay -> set_priority(procId, 10);" << std::endl;
+    stream << padding << "      :: else -> skip;" << std::endl;
+    stream << padding << "      fi;" << std::endl;
+    stream << padding << "    }" << std::endl;
+    
+    if (_allowEventInterleaving) {
+        stream << padding << "    :: len(tempQ) > 0 -> {" << std::endl;
+        stream << padding << "      tempQ?<tmpE>;" << std::endl;
+        stream << padding << "      if" << std::endl;
+        stream << padding << "      :: smallestDelay == tmpE.delay -> set_priority(procId, 10);" << std::endl;
+        stream << padding << "      :: else -> skip;" << std::endl;
+        stream << padding << "      fi;" << std::endl;
+        stream << padding << "    }" << std::endl;
+    }
+    
+    stream << padding << "    :: else -> skip;" << std::endl;
+    stream << padding << "    fi;" << std::endl;
+    stream << padding << "  }" << std::endl;
+    stream << padding << "  fi;" << std::endl;
+    stream << padding << "}" << std::endl;
+}
+
 void ChartToPromela::writeCancelEvents(std::ostream& stream, int indent) {
     std::list<std::string> queues;
     queues.push_back("eQ");
     if (_allowEventInterleaving)
         queues.push_back("tmpQ");
     
-    stream << "inline cancelSendId(sendIdentifier, invokerIdentifier) {" << std::endl;
+    stream << "inline cancelSendId(sendIdentifier, source) {" << std::endl;
     for (auto machine : *_machinesAll) {
         for (auto queue : queues) {
-            stream << "  cancelSendIdOnQueue(sendIdentifier, " << machine.second->_prefix << queue << ", invokerIdentifier);" << std::endl;
+            stream << "  cancelSendIdOnQueue(sendIdentifier, source, " << machine.second->_prefix << queue << ");" << std::endl;
         }
     }
     stream << "}" << std::endl;
     stream << std::endl;
     
     
-    stream << "inline cancelSendIdOnQueue(sendIdentifier, queue, invokerIdentifier) {" << std::endl;
+    stream << "inline cancelSendIdOnQueue(sendIdentifier, source, queue) {" << std::endl;
     stream << "  tmpIndex = 0;" << std::endl;
     //    stream << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), "  ");
     stream << "  do" << std::endl;
     stream << "  :: tmpIndex < len(queue) -> {" << std::endl;
     stream << "    queue?tmpE;" << std::endl;
     stream << "    if" << std::endl;
-    stream << "    :: tmpE.invokeid != invokerIdentifier || tmpE.sendid != sendIdentifier || tmpE.delay == 0 -> queue!tmpE;" << std::endl;
+    stream << "    :: tmpE.sendid != sendIdentifier || tmpE.origin != source || tmpE.delay == 0 -> queue!tmpE;" << std::endl;
     stream << "    :: else -> skip;" << std::endl;
     stream << "    fi" << std::endl;
     stream << "    tmpIndex++;" << std::endl;
@@ -2621,5 +2878,52 @@ void ChartToPromela::writeCancelEvents(std::ostream& stream, int indent) {
     stream << "}" << std::endl;
 }
 
+void ChartToPromela::writeRemovePendingEventsFromInvoker(std::ostream& stream, int indent) {
+    std::list<std::string> queues;
+    queues.push_back("eQ");
+    if (_allowEventInterleaving)
+        queues.push_back("tmpQ");
+    
+    stream << "inline removePendingEventsFromInvoker(invoker) {" << std::endl;
+    for (auto machine : *_machinesAll) {
+        for (auto queue : queues) {
+            stream << "  removePendingEventsFromInvokerOnQueue(invoker, " << machine.second->_prefix << queue << ");" << std::endl;
+        }
+    }
+    stream << "}" << std::endl;
+    stream << std::endl;
+    
+    stream << "inline removePendingEventsFromInvokerOnQueue(invoker, queue) {" << std::endl;
+    stream << "  tmpIndex = len(queue);" << std::endl;
+    //    stream << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), "  ");
+    stream << "  do" << std::endl;
+    stream << "  :: tmpIndex > 0 -> {" << std::endl;
+    stream << "    queue?tmpE;" << std::endl;
+    stream << "    if" << std::endl;
+    stream << "    :: false || ";
+    if (_analyzer->usesEventField("delay"))
+        stream << "tmpE.delay == 0 || ";
+    if (_analyzer->usesEventField("invokeid"))
+        stream << "tmpE.invokeid != invoker" << std::endl;
+    stream << " -> {" << std::endl;
+    
+    TRACE_EXECUTION_V("Reenqueing event %d", "tmpE.name");
+    
+    stream << "      queue!tmpE;" << std::endl;
+    stream << "    }" << std::endl;
+    stream << "    :: else -> {" << std::endl;
+
+    TRACE_EXECUTION_V("Dropping event %d", "tmpE.name");
+    
+    stream << "      skip;" << std::endl;
+    stream << "    }" << std::endl;
+    stream << "    fi" << std::endl;
+    stream << "    tmpIndex = tmpIndex - 1;" << std::endl;
+    stream << "  }" << std::endl;
+    stream << "  :: else -> break;" << std::endl;
+    stream << "  od" << std::endl;
+    stream << "}" << std::endl;
+}
+
 
 }
diff --git a/src/uscxml/transform/ChartToPromela.h b/src/uscxml/transform/ChartToPromela.h
index cfba760..8df3dca 100644
--- a/src/uscxml/transform/ChartToPromela.h
+++ b/src/uscxml/transform/ChartToPromela.h
@@ -45,72 +45,58 @@ protected:
 
 	void writeTransitions(std::ostream& stream);
 	void writeStates(std::ostream& stream);
+    
+    void writeCommonTypeDefs(std::ostream& stream);
+    void writeCommonVariables(std::ostream& stream);
     void writeTypeDefs(std::ostream& stream);
-	void writeTypes(std::ostream& stream);
+    void writeVariables(std::ostream& stream);
+
+//  void writeTypeDefs(std::ostream& stream);
+//	void writeTypes(std::ostream& stream);
 	void writeMacros(std::ostream& stream);
-	void writeHelpers(std::ostream& stream);
 	void writeFSM(std::ostream& stream);
 	void writeExecContent(std::ostream& stream, const XERCESC_NS::DOMNode* node, size_t indent = 0);
+    void writeRaiseDoneDate(std::ostream& stream, const XERCESC_NS::DOMElement* donedata, size_t indent = 0);
+
     void writeStrings(std::ostream& stream);
 
     void writeCancelEvents(std::ostream& stream, int indent = 0);
+    void writeScheduleMachines(std::ostream& stream, int indent = 0);
+    void writeDetermineShortestDelay(std::ostream& stream, int indent = 0);
+    void writeRescheduleProcess(std::ostream& stream, int indent = 0);
+    void writeInsertWithDelay(std::ostream& stream, int indent = 0);
+    void writeAdvanceTime(std::ostream& stream, int indent = 0);
+    void writeRemovePendingEventsFromInvoker(std::ostream& stream, int indent = 0);
 
     void prepare();
     
-	void bit_clear_all(std::ostream& stream,
-	                   const std::string& identifier,
-	                   size_t length,
-	                   size_t indent = 0);
-
-	void bit_copy(std::ostream& stream,
-	              const std::string& from,
-	              const std::string& to,
-	              size_t length,
-	              size_t indent = 0);
-
-	void bit_or(std::ostream& stream,
-	            const std::string& to,
-	            const std::string& mask,
-	            size_t length,
-	            size_t indent = 0);
-
-	void bit_and(std::ostream& stream,
-	             const std::string& to,
-	             const std::string& mask,
-	             size_t length,
-	             size_t indent = 0);
-
-	void bit_and_not(std::ostream& stream,
-	                 const std::string& to,
-	                 const std::string& mask,
-	                 size_t length,
-	                 size_t indent = 0);
-
-	void bit_has_and(std::ostream& stream,
-	                 const std::string& a,
-	                 const std::string& b,
-	                 size_t length,
-	                 size_t indent = 0);
+    void writeBitClearMacro(std::ostream& stream);
+    void writeBitHasAndMacro(std::ostream& stream);
+    void writeBitHasAnyMacro(std::ostream& stream);
+    void writeBitOrMacro(std::ostream& stream);
+    void writeBitCopyMacro(std::ostream& stream);
+    void writeBitAndMacro(std::ostream& stream);
+    void writeBitAndNotMacro(std::ostream& stream);
 
 	void printBitArray(std::ostream& stream,
 	                   const std::string& array,
 	                   size_t length,
 	                   size_t indent = 0);
 
-	PromelaCodeAnalyzer _analyzer;
+	PromelaCodeAnalyzer* _analyzer = NULL;
 
-	ChartToPromela* _parentTopMost;
-	ChartToPromela* _parent;
+	ChartToPromela* _parentTopMost = NULL;
+	ChartToPromela* _parent = NULL;
 	std::string _invokerid;
 
     size_t _internalQueueLength = 7;
     size_t _externalQueueLength = 7;
     bool _allowEventInterleaving = false;
     
-	std::map<std::string, XERCESC_NS::DOMNode* > _machinesPerId;
-	std::map<std::string, XERCESC_NS::DOMNode* >* _machinesAllPerId = NULL;
-	std::map<XERCESC_NS::DOMNode*, ChartToPromela*> _machines;
-	std::map<XERCESC_NS::DOMNode*, ChartToPromela*>* _machinesAll = NULL;
+	std::map<std::string, XERCESC_NS::DOMElement* > _machinesPerId;
+	std::map<std::string, XERCESC_NS::DOMElement* >* _machinesAllPerId = NULL;
+	std::map<XERCESC_NS::DOMElement*, ChartToPromela*> _machinesNested;
+	std::map<XERCESC_NS::DOMElement*, ChartToPromela*>* _machinesAll = NULL;
 
 	std::set<std::string> _dataModelVars;
     std::list<std::string> _varInitializers; // pending initializations for arrays
diff --git a/src/uscxml/transform/Transformer.h b/src/uscxml/transform/Transformer.h
index fcfda01..5b2fbdb 100644
--- a/src/uscxml/transform/Transformer.h
+++ b/src/uscxml/transform/Transformer.h
@@ -39,11 +39,17 @@ public:
 		_binding = other.getImpl()->_binding;
 	}
 
+    
+    
 	virtual void writeTo(std::ostream& stream) = 0;
 	virtual operator Interpreter() {
 		throw std::runtime_error("Transformer cannot be interpreted as an Interpreter again");
 	}
 
+    virtual XERCESC_NS::DOMDocument* getDocument() const {
+        return _document;
+    }
+
 protected:
 	std::multimap<std::string, std::string> _extensions;
 	std::list<std::string> _options;
diff --git a/src/uscxml/transform/promela/PromelaCodeAnalyzer.cpp b/src/uscxml/transform/promela/PromelaCodeAnalyzer.cpp
index 4d1d8d5..7cb69d7 100644
--- a/src/uscxml/transform/promela/PromelaCodeAnalyzer.cpp
+++ b/src/uscxml/transform/promela/PromelaCodeAnalyzer.cpp
@@ -67,16 +67,25 @@ void PromelaCodeAnalyzer::analyze(ChartToPromela* interpreter) {
 					if (boost::ends_with(eventName, "."))
 						eventName = eventName.substr(0, eventName.size() - 1);
 					if (eventName.size() > 0)
-						_eventTrie.addWord(eventName);
+						addEvent(eventName);
 				}
 			}
 		}
 
 		for (auto state : interpreter->_states) {
 			if (HAS_ATTR(state, "id") && (isCompound(state) || isParallel(state))) {
-				_eventTrie.addWord("done.state." + ATTR(state, "id"));
+				addEvent("done.state." + ATTR(state, "id"));
 			}
 		}
+        
+        std::list<XERCESC_NS::DOMElement*> invokers = DOMUtils::inDocumentOrder({XML_PREFIX(interpreter->_scxml).str() + "invoke"}, interpreter->_scxml, false);
+        for (auto invoker : invokers) {
+            addCode("_event.invokeid", interpreter);
+
+            if (HAS_ATTR(invoker, "id")) {
+                addEvent("done.state." + ATTR(invoker, "id"));
+            }
+        }
 	}
 
     // add event names from trie to string literals
@@ -94,7 +103,9 @@ void PromelaCodeAnalyzer::analyze(ChartToPromela* interpreter) {
 		}, interpreter->_scxml);
 
 		for (auto content : contents) {
-			std::string contentStr = spaceNormalize(X(((DOMElement*)content)->getFirstChild()->getNodeValue()));
+            if (!content->hasChildNodes())
+                continue;
+			std::string contentStr = spaceNormalize(X(content->getFirstChild()->getNodeValue()));
 			if (!isNumeric(contentStr.c_str(), 10)) {
 				addLiteral(contentStr);
 			}
@@ -192,7 +203,7 @@ void PromelaCodeAnalyzer::analyze(ChartToPromela* interpreter) {
             std::list<DOMElement*> cancels = DOMUtils::inDocumentOrder({XML_PREFIX(interpreter->_scxml).str() + "cancel"}, interpreter->_scxml);
             
             if (cancels.size() > 0) {
-                addCode("_event.invokeid", interpreter);
+                addCode("_event.origin", interpreter);
                 _usesCancel = true;
             }
             
@@ -207,6 +218,9 @@ void PromelaCodeAnalyzer::analyze(ChartToPromela* interpreter) {
             
                 // do we need delays?
                 if (HAS_ATTR(send, "delay") || HAS_ATTR(send, "delayexpr")) {
+                    size_t delay = strTo<size_t>(ATTR(send, "delay"));
+                    if (delay > largestDelay)
+                        largestDelay = delay;
                     addCode("_event.delay", interpreter);
 #if NEW_DELAY_RESHUFFLE
 #else
@@ -236,6 +250,11 @@ void PromelaCodeAnalyzer::analyze(ChartToPromela* interpreter) {
 
 }
 
+void PromelaCodeAnalyzer::addEvent(const std::string& eventName) {
+    addLiteral(eventName);
+    _eventTrie.addWord(eventName);
+}
+
 std::string PromelaCodeAnalyzer::sanitizeCode(const std::string& code) {
 	std::string replaced = code;
 	boost::replace_all(replaced, "\"", "'");
@@ -504,6 +523,8 @@ std::string PromelaCodeAnalyzer::adaptCode(const std::string& code, const std::s
             if (std::all_of(token.begin(), token.end(), ::isupper) && false) {
                 // assume it is a state-name macro
                 processedStr << code.substr(lastPos, posIter->first - lastPos) << token;
+            } else if (boost::starts_with(prefix, token)) {
+                processedStr << code.substr(lastPos, posIter->first - lastPos) << token;
             } else {
                 processedStr << code.substr(lastPos, posIter->first - lastPos) << prefix << token;
             }
@@ -572,8 +593,11 @@ std::list<std::pair<size_t, size_t> > PromelaCodeAnalyzer::getTokenPositions(con
 	return posList;
 }
 
-std::string PromelaCodeAnalyzer::getTypeReset(const std::string& var, const PromelaTypedef& type, const std::string padding) {
+std::string PromelaCodeAnalyzer::getTypeReset(const std::string& var, const PromelaTypedef& type, size_t indent) {
 	std::stringstream assignment;
+    std::string padding;
+    for (size_t i = 0; i < indent; i++)
+        padding += "  ";
 
 	std::map<std::string, PromelaTypedef>::const_iterator typeIter = type.types.begin();
 	while(typeIter != type.types.end()) {
@@ -583,7 +607,7 @@ std::string PromelaCodeAnalyzer::getTypeReset(const std::string& var, const Prom
 				assignment << padding << var << "." << typeIter->first << "[" << i << "] = 0;" << std::endl;
 			}
 		} else if (innerType.types.size() > 0) {
-			assignment << getTypeReset(var + "." + typeIter->first, typeIter->second, padding);
+			assignment << getTypeReset(var + "." + typeIter->first, typeIter->second, indent);
 		} else {
 			assignment << padding << var << "." << typeIter->first << " = 0;" << std::endl;
 		}
@@ -593,4 +617,27 @@ std::string PromelaCodeAnalyzer::getTypeReset(const std::string& var, const Prom
 
 }
 
+std::string PromelaCodeAnalyzer::getTypeAssignment(const std::string& varTo, const std::string& varFrom, const PromelaTypedef& type, size_t indent) {
+    std::stringstream assignment;
+    std::string padding;
+    for (size_t i = 0; i < indent; i++)
+        padding += "  ";
+
+    std::map<std::string, PromelaTypedef>::const_iterator typeIter = type.types.begin();
+    while(typeIter != type.types.end()) {
+        const PromelaTypedef& innerType = typeIter->second;
+        if (innerType.arraySize > 0) {
+            for (size_t i = 0; i < innerType.arraySize; i++) {
+                assignment << padding << varTo << "." << typeIter->first << "[" << i << "] = " << varFrom << "." << typeIter->first << "[" << i << "];" << std::endl;
+            }
+        } else if (innerType.types.size() > 0) {
+            assignment << getTypeAssignment(varTo + "." + typeIter->first, varFrom + "." + typeIter->first, typeIter->second, indent);
+        } else {
+            assignment << padding << varTo << "." << typeIter->first << " = " << varFrom << "." << typeIter->first << ";" << std::endl;
+        }
+        typeIter++;
+    }
+    return assignment.str();
+}
+
 }
diff --git a/src/uscxml/transform/promela/PromelaCodeAnalyzer.h b/src/uscxml/transform/promela/PromelaCodeAnalyzer.h
index 656b24e..83ee684 100644
--- a/src/uscxml/transform/promela/PromelaCodeAnalyzer.h
+++ b/src/uscxml/transform/promela/PromelaCodeAnalyzer.h
@@ -76,8 +76,10 @@ public:
 		return false;
 	}
 
-	std::string getTypeAssignment(const std::string& varTo, const std::string& varFrom, const PromelaTypedef& type, const std::string padding = "");
-	std::string getTypeReset(const std::string& var, const PromelaTypedef& type, const std::string padding = "");
+    size_t largestDelay = 0;
+    
+	std::string getTypeAssignment(const std::string& varTo, const std::string& varFrom, const PromelaTypedef& type, size_t indent = 0);
+	std::string getTypeReset(const std::string& var, const PromelaTypedef& type, size_t indent = 0);
 
 	bool usesInPredicate() {
 		return _usesInPredicate;
@@ -119,12 +121,12 @@ public:
 	}
 
 	std::string sanitizeCode(const std::string& code);
+    void addEvent(const std::string& eventName);
+    std::string createMacroName(const std::string& literal);
 
 protected:
-    void addEvent(const std::string& eventName);
     void addState(const std::string& stateName, size_t index);
 
-    std::string createMacroName(const std::string& literal);
 	int enumerateLiteral(const std::string& literal, int forceIndex = -1);
 
 	std::map<std::string, std::string> _strMacros;  // macronames for string literals