diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/uscxml/transform/ChartToPromela.cpp | 3116 | ||||
| -rw-r--r-- | src/uscxml/transform/ChartToPromela.h | 72 | ||||
| -rw-r--r-- | src/uscxml/transform/Transformer.h | 6 | ||||
| -rw-r--r-- | src/uscxml/transform/promela/PromelaCodeAnalyzer.cpp | 59 | ||||
| -rw-r--r-- | src/uscxml/transform/promela/PromelaCodeAnalyzer.h | 10 |
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 |