summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/uscxml/transform/ChartToPromela.cpp3116
-rw-r--r--src/uscxml/transform/ChartToPromela.h72
-rw-r--r--src/uscxml/transform/Transformer.h6
-rw-r--r--src/uscxml/transform/promela/PromelaCodeAnalyzer.cpp59
-rw-r--r--src/uscxml/transform/promela/PromelaCodeAnalyzer.h10
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