summaryrefslogtreecommitdiffstats
path: root/src/uscxml
diff options
context:
space:
mode:
Diffstat (limited to 'src/uscxml')
-rw-r--r--src/uscxml/transform/ChartToPromela.cpp1075
-rw-r--r--src/uscxml/transform/ChartToPromela.h12
2 files changed, 685 insertions, 402 deletions
diff --git a/src/uscxml/transform/ChartToPromela.cpp b/src/uscxml/transform/ChartToPromela.cpp
index a6aeaa0..06c8a92 100644
--- a/src/uscxml/transform/ChartToPromela.cpp
+++ b/src/uscxml/transform/ChartToPromela.cpp
@@ -34,9 +34,9 @@
#define TMP_EVENT_NAME (_analyzer->usesComplexEventStruct() ? "_tmpE.name" : "_tmpE")
#define MAX(X,Y) ((X) > (Y) ? (X) : (Y))
-#undef TRACE_EXECUTION
+#define TRACE
-#ifdef TRACE_EXECUTION
+#ifdef TRACE
#define TRACE_EXECUTION_V(fmt, ...) \
stream << std::endl; \
stream << "#if TRACE_EXECUTION" << std::endl; \
@@ -1262,11 +1262,14 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
std::list<DOMElement*> globalScripts = DOMUtils::filterChildElements(XML_PREFIX(_scxml).str() + "script", _scxml, false);
if (globalScripts.size() > 0) {
stream << "/* run global scripts */" << std::endl;
+ stream << "d_step { " << std::endl;
+
for (auto globalScript : globalScripts) {
TRACE_EXECUTION("Processing executable content for global script");
writeExecContent(stream, globalScript, 2);
}
+ stream << "} /* d_step */" << std::endl;
stream << std::endl;
}
@@ -1281,15 +1284,299 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
TRACE_EXECUTION("Taking a step");
+
+#if 0
+ writeFSMRescheduleMachines(stream);
+ stream << std::endl;
+ writeFSMMacrostep(stream);
+ stream << std::endl;
+ writeFSMDequeueInternalOrSpontaneousEvent(stream);
+#else
+ writeFSMDequeueEvent(stream);
+#endif
+ stream << std::endl;
+ stream << "d_step { skip;" << std::endl;
+
+ stream << std::endl;
+ writeFSMSelectTransitions(stream);
+ stream << std::endl;
+
+
+ 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;
+
+ writeFSMRememberHistory(stream);
+ stream << std::endl;
+ writeFSMEstablishEntrySet(stream);
+ stream << std::endl;
+ writeFSMExitStates(stream);
+ stream << std::endl;
+ writeFSMTakeTransitions(stream);
+ stream << std::endl;
+ writeFSMEnterStates(stream);
+ stream << std::endl;
+
+// TRACE_EXECUTION("Exited States")
+
+
+ stream << " }" << std::endl;
+ stream << " :: else -> skip;" << std::endl;
+ stream << " fi /* USCXML_CTX_TRANSITION_FOUND */" << std::endl;
+ stream << " } skip; /* d_step */" << std::endl;
+
+ stream << "} /* !USCXML_CTX_FINISHED */" << std::endl;
+ stream << ":: else -> break;" << std::endl;
+ stream << "od" << std::endl;
+ stream << std::endl;
+
+ writeFSMTerminateMachine(stream);
+ stream << std::endl;
+
+ TRACE_EXECUTION("Done");
+
+
+ stream << "} } /* atomic, step() */" << std::endl;
+ stream << std::endl;
+
+}
+
+#if 0
+void ChartToPromela::writeFSMRescheduleMachines(std::ostream& stream) {
+ 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 << " /* 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 << std::endl;
+ }
+}
+
+void ChartToPromela::writeFSMMacrostep(std::ostream& stream) {
+
+ stream << " /* Dequeue an external event */" << std::endl;
+ stream << " " << _prefix << "flags[USCXML_CTX_DEQUEUED_EXTERNAL] = false;" << std::endl;
+
+ stream << " if" << std::endl;
+ stream << " :: !" << _prefix << "flags[USCXML_CTX_SPONTANEOUS] && len(" << _prefix << "iQ) == 0 -> {" << std::endl;
+
+ stream << " /* manage invocations */" << std::endl;
+ stream << " i = 0;" << std::endl;
+ stream << " do" << std::endl;
+ stream << " :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
+ stream << " /* uninvoke */" << std::endl;
+ stream << " if" << 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 << "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 << std::endl;
+
+ stream << " /* Not sure if this should be before the invocation due to auto-forwarding */" << std::endl;
+ stream << " do" << 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;
+
+ 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;
+
+ }
+
+ TRACE_EXECUTION("Deqeued an external event");
+ stream << " " << _prefix << "flags[USCXML_CTX_DEQUEUED_EXTERNAL] = true;" << std::endl;
+ stream << " break;" << std::endl;
+ stream << " }" << std::endl;
+ // stream << " :: else -> quit;" << std::endl;
+ stream << " od;" << std::endl;
+
+ stream << " }" << std::endl;
+ stream << " :: else -> skip;" << std::endl;
+ stream << " fi" << std::endl;
+ stream << std::endl;
+}
+
+void ChartToPromela::writeFSMDequeueInternalOrSpontaneousEvent(std::ostream& stream) {
+ stream << " if" << std::endl;
+ stream << " :: !" << _prefix << "flags[USCXML_CTX_DEQUEUED_EXTERNAL] -> {" << std::endl;
+ stream << " /* Try with a spontaneous event or dequeue an internal event */" << std::endl;
+ stream << " if" << std::endl;
+ stream << " :: " << _prefix << "flags[USCXML_CTX_SPONTANEOUS] -> {" << std::endl;
+ stream << " /* We try with a spontaneous event */" << std::endl;
+ stream << " " << _prefix << EVENT_NAME << " = USCXML_EVENT_SPONTANEOUS;" << std::endl;
+ stream << " }" << std::endl;
+ stream << " :: else -> {" << std::endl;
+ stream << " /* We try with an internal event */" << std::endl;
+ stream << " assert(len(" << _prefix << "iQ) > 0);" << std::endl;
+ stream << " " << _prefix << "iQ ? " << _prefix << "_event;" << std::endl;
+ stream << " }" << std::endl;
+ stream << " fi" << std::endl;
+ stream << " }" << std::endl;
+ stream << " :: else -> skip;" << std::endl;
+ stream << " fi" << std::endl;
+
+}
+#endif
+
+#if 1
+void ChartToPromela::writeFSMDequeueEvent(std::ostream& stream) {
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_SPONTANEOUS] -> {" << std::endl;
- stream << " " << _prefix << EVENT_NAME << " = USCXML_EVENT_SPONTANEOUS;" << std::endl;
-
+ stream << " if" << std::endl;
+ stream << " ::" << _prefix << "flags[USCXML_CTX_SPONTANEOUS] -> {" << std::endl;
+ stream << " " << _prefix << EVENT_NAME << " = USCXML_EVENT_SPONTANEOUS;" << std::endl;
+
TRACE_EXECUTION("Trying with a spontaneous event");
-
- stream << " }" << std::endl;
+
+ stream << " }" << std::endl;
stream << " :: else -> {" << std::endl;
stream << " if" << std::endl;
stream << " :: len(" << _prefix << "iQ) != 0 -> {" << std::endl;
@@ -1303,25 +1590,26 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << " }" << std::endl;
stream << " fi;" << std::endl;
stream << " }" << std::endl;
- stream << " fi;" << std::endl;
- stream << std::endl;
-
+ stream << " fi;" << std::endl;
stream << std::endl;
-
+
+ stream << 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 < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
- stream << " /* uninvoke */" << std::endl;
- stream << " if" << std::endl;
- stream << " :: !" << _prefix << "config[i] && " << _prefix << "invocations[i] -> {" << std::endl;
-
+ stream << " /* manage invocations */" << std::endl;
+ stream << " i = 0;" << std::endl;
+ stream << " do" << std::endl;
+ stream << " :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
+ stream << " d_step { " << std::endl;
+ stream << " /* uninvoke */" << std::endl;
+ stream << " if" << 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) {
@@ -1337,20 +1625,22 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
}
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 << " }" << std::endl;
+ stream << " :: else -> skip;" << std::endl;
+ stream << " fi;" << std::endl;
+ stream << " } /* d_step */" << std::endl;
+ stream << std::endl;
- stream << " /* invoke */" << std::endl;
- stream << " if" << std::endl;
- stream << " :: " << _prefix << "config[i] && !" << _prefix << "invocations[i] -> {" << std::endl;
+
+ stream << " /* invoke */" << std::endl;
+ stream << " if" << std::endl;
+ stream << " :: " << _prefix << "config[i] && !" << _prefix << "invocations[i] -> {" << std::endl;
stream << " if" << std::endl;
for (size_t i = 0; i < _states.size(); i++) {
@@ -1383,7 +1673,7 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
}
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")) << " = ";
@@ -1399,15 +1689,16 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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 << " }" << 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 << std::endl;
+
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;
@@ -1420,15 +1711,16 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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;
-
+ 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 << " d_step {" << std::endl;
stream << " /* auto-forward event */" << std::endl;
stream << " i = 0;" << std::endl;
stream << " do" << std::endl;
@@ -1437,9 +1729,9 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
std::string insertOp = "!";
if (_analyzer->usesEventField("delay")) {
-// insertOp += "!";
+ // insertOp += "!";
}
-
+
for (auto state : _states) {
std::list<DOMElement*> invokers = DOMUtils::filterChildElements(XML_PREFIX(state).str() + "invoke", state, false);
@@ -1466,7 +1758,7 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << " }" << std::endl;
stream << " :: else -> break;" << std::endl;
stream << " od" << std::endl;
-
+
stream << std::endl;
stream << " /* finalize event */" << std::endl;
stream << " if" << std::endl;
@@ -1475,7 +1767,7 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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) {
@@ -1487,30 +1779,33 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << " :: else -> skip;" << std::endl;
stream << " fi" << std::endl;
+ stream << " } /* d_step */" << std::endl;
}
TRACE_EXECUTION("Deqeued an external event");
-
- stream << " }" << std::endl;
-// stream << " :: else -> quit;" << std::endl;
- stream << " fi;" << std::endl;
+
+ stream << " }" << std::endl;
+ // stream << " :: else -> quit;" << std::endl;
+ stream << " fi;" << std::endl;
stream << " }" << std::endl;
stream << " :: else -> skip;" << std::endl;
stream << " fi" << std::endl;
- stream << std::endl;
+ stream << std::endl;
+}
+#endif
+void ChartToPromela::writeFSMSelectTransitions(std::ostream& stream) {
stream << "/* ---------------------------- */" << std::endl;
- stream << _prefix << "SELECT_TRANSITIONS:" << std::endl;
- stream << "d_step {" << 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;
-
+
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;
@@ -1519,7 +1814,7 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
}
stream << "#endif" << std::endl;
stream << std::endl;
-
+
stream << "#if TRACE_EXECUTION" << std::endl;
stream << "printf(\"Configuration: \");" << std::endl;
printBitArray(stream, _prefix + "config", _states.size());
@@ -1530,12 +1825,12 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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;
@@ -1551,8 +1846,8 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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") != "*") {
@@ -1577,28 +1872,28 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
}
stream << ")" << std::endl;
}
-
+
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 << " /* 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 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 << " /* 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;
@@ -1609,12 +1904,12 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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;
@@ -1626,13 +1921,13 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << std::endl;
}
stream << std::endl;
- stream << "#if TRACE_EXECUTION" << std::endl;
- stream << "printf(\"Target Set: \");" << std::endl;
- printBitArray(stream, _prefix + "ctx.target_set", _states.size());
- stream << "printf(\"\\n\");" << std::endl;
- stream << "#endif" << std::endl;
+ stream << "#if TRACE_EXECUTION" << std::endl;
+ stream << "printf(\"Target Set: \");" << std::endl;
+ printBitArray(stream, _prefix + "ctx.target_set", _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(\"Exit Set: \");" << std::endl;
@@ -1640,66 +1935,60 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << "printf(\"\\n\");" << std::endl;
stream << "#endif" << std::endl;
stream << std::endl;
-
- stream << " if" << 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 << " goto " << _prefix << "ESTABLISH_ENTRY_SET;" << std::endl;
stream << std::endl;
stream << " }" << std::endl;
- stream << " :: " << _prefix << "flags[USCXML_CTX_TRANSITION_FOUND] -> {" << std::endl;
-
+ stream << " :: " << _prefix << "flags[USCXML_CTX_TRANSITION_FOUND] -> {" << 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 << " }" << std::endl;
+ stream << " :: else {" << std::endl;
+ stream << " " << _prefix << "flags[USCXML_CTX_SPONTANEOUS] = false;" << std::endl;
+
TRACE_EXECUTION("Found NO transitions");
-
-// stream << " goto " << _prefix << "MICROSTEP;" << std::endl;
- stream << " }" << std::endl;
- stream << " fi" << std::endl;
- stream << std::endl;
- stream << "} /* d_step */" << std::endl;
-
- 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 << " goto " << _prefix << "MICROSTEP;" << std::endl;
+ stream << " }" << std::endl;
+ stream << " fi" << std::endl;
+ stream << std::endl;
-
+}
+
+void ChartToPromela::writeFSMRememberHistory(std::ostream& stream) {
stream << "/* ---------------------------- */" << std::endl;
- stream << "/* REMEMBER_HISTORY: */" << std::endl;
- stream << "d_step {" << std::endl;
+ stream << "/* REMEMBER_HISTORY: */" << std::endl;
TRACE_EXECUTION("Save history configurations");
-
+
stream << " if" << std::endl;
stream << " :: " << _prefix << "STATES_HAS_ANY(" << _prefix << "config) -> {" << std::endl;
stream << " /* only remember history on non-initial entry */" << std::endl;
-
+
stream << " i = 0;" << std::endl;
- stream << " do" << std::endl;
- stream << " :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << 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 << " do" << std::endl;
+ stream << " :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
- stream << " /* a history state whose parent is about to be exited */" << 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;
@@ -1707,9 +1996,9 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << "printf(\"\\n\");" << std::endl;
stream << "#endif" << std::endl;
stream << std::endl;
-
+
stream << " " << _prefix << "STATES_COPY(" << _prefix << "ctx.tmp_states, " << _prefix << "states[i].completion)" << 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;
@@ -1729,30 +2018,30 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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 << " :: 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 << " i = i + 1;" << std::endl;
+ stream << " }" << std::endl;
+ stream << " :: else -> break;" << std::endl;
+ stream << " od;" << std::endl;
+ stream << std::endl;
+
stream << std::endl;
stream << "#if TRACE_EXECUTION" << std::endl;
stream << "printf(\"History: \");" << std::endl;
@@ -1762,58 +2051,56 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << " }" << std::endl;
stream << " :: else -> skip;" << std::endl;
stream << " fi;" << std::endl;
- stream << "} /* d_step */" << std::endl;
-
- stream << std::endl;
-
+}
+
+void ChartToPromela::writeFSMEstablishEntrySet(std::ostream& stream) {
stream << "/* ---------------------------- */" << std::endl;
- stream << _prefix << "ESTABLISH_ENTRY_SET:" << std::endl;
- stream << "d_step {" << std::endl;
- stream << " /* calculate new entry set */" << std::endl;
+ stream << _prefix << "ESTABLISH_ENTRY_SET:" << std::endl;
+ stream << " /* calculate new entry set */" << std::endl;
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 < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
-
- stream << " if" << std::endl;
- stream << " :: " << _prefix << "ctx.entry_set[i] -> {" << std::endl;
- stream << " /* ancestor completion */" << std::endl;
+ stream << std::endl;
+
+ stream << " i = 0;" << std::endl;
+ stream << " do" << std::endl;
+ stream << " :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
+
+ stream << " if" << std::endl;
+ stream << " :: " << _prefix << "ctx.entry_set[i] -> {" << std::endl;
+ stream << " /* ancestor completion */" << std::endl;
stream << " " << _prefix << "STATES_OR(" << _prefix << "ctx.entry_set, " << _prefix << "states[i].ancestors)" << 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 << " /* iterate for descendants */" << std::endl;
- stream << " i = 0;" << std::endl;
- stream << " do" << std::endl;
- stream << " :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
- stream << " if" << std::endl;
- stream << " :: " << _prefix << "ctx.entry_set[i] -> {" << std::endl;
- stream << " if" << std::endl;
-
- stream << " :: " << _prefix << "states[i].type[USCXML_STATE_PARALLEL] -> {" << 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 << " /* iterate for descendants */" << std::endl;
+ stream << " i = 0;" << std::endl;
+ stream << " do" << std::endl;
+ stream << " :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
+ stream << " if" << std::endl;
+ stream << " :: " << _prefix << "ctx.entry_set[i] -> {" << std::endl;
+ stream << " if" << std::endl;
+
+ stream << " :: " << _prefix << "states[i].type[USCXML_STATE_PARALLEL] -> {" << std::endl;
stream << " " << _prefix << "STATES_OR(" << _prefix << "ctx.entry_set, " << _prefix << "states[i].completion)" << std::endl;
- stream << " }" << 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 << " }" << std::endl;
+
+
+ stream << " :: " << _prefix << "states[i].type[USCXML_STATE_HISTORY_SHALLOW] ||" << std::endl;
+ stream << " " << _prefix << "states[i].type[USCXML_STATE_HISTORY_DEEP] -> {" << std::endl;
+
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 << " :: !" << _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;
TRACE_EXECUTION("Fresh history in target set")
if (_transitions.size() > 0) {
@@ -1823,13 +2110,13 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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);
+ // 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;
@@ -1858,8 +2145,8 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << " :: else -> break" << std::endl;
stream << " od" << std::endl;
}
- stream << " skip;" << std::endl;
- stream << " }" << std::endl;
+ stream << " skip;" << std::endl;
+ stream << " }" << std::endl;
stream << " :: else -> {" << std::endl;
TRACE_EXECUTION("Established history in target set")
@@ -1905,17 +2192,17 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << " }" << std::endl;
stream << " :: else -> skip;" << std::endl;
stream << " fi" << std::endl;
-
+
stream << " }" << std::endl;
- stream << " fi;" << std::endl;
-
- stream << " }" << std::endl;
-
+ stream << " fi;" << std::endl;
+
+ stream << " }" << std::endl;
+
if (_transitions.size() > 0) {
stream << " :: " << _prefix << "states[i].type[USCXML_STATE_INITIAL] -> {" << std::endl;
-
+
TRACE_EXECUTION_V("Descendant completion for initial state %d", "i")
-
+
stream << " j = 0" << std::endl;
stream << " do" << std::endl;
stream << " :: j < " << _prefix << "USCXML_NUMBER_TRANS -> {" << std::endl;
@@ -1923,22 +2210,22 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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;
-
+
TRACE_EXECUTION_V("Adding transition %d!", "j");
-
+
stream << " " << _prefix << "STATES_OR(" << _prefix << "ctx.entry_set, " << _prefix << "transitions[j].target)" << std::endl;
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 << std::endl;
-
+
stream << " }" << std::endl;
stream << " :: else -> break;" << std::endl;
stream << " fi" << std::endl;
@@ -1953,97 +2240,97 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << " }" << std::endl;
stream << " :: else -> break" << std::endl;
stream << " od;" << std::endl;
-
+
stream << " }" << std::endl;
}
-
- stream << " :: " << _prefix << "states[i].type[USCXML_STATE_COMPOUND] -> {" << 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 << " !" << _prefix << "STATES_HAS_AND(" << _prefix << "ctx.entry_set, " << _prefix << "states[i].children)";
- 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;
-
+
+ stream << " :: " << _prefix << "states[i].type[USCXML_STATE_COMPOUND] -> {" << 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 << " !" << _prefix << "STATES_HAS_AND(" << _prefix << "ctx.entry_set, " << _prefix << "states[i].children)";
+ 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;
+
stream << " " << _prefix << "STATES_OR(" << _prefix << "ctx.entry_set, " << _prefix << "states[i].completion)" << std::endl;
-
- 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 << " 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;
+ stream << " ) -> {" << std::endl;
+ stream << " /* deep completion */" << std::endl;
+ stream << " j = i + 1;" << std::endl;
+
+ // TRACE_EXECUTION_V("Deep completion for compound state %d", "i")
-// 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 << " :: 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 << " }" << 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;
- 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 << std::endl;
-
stream << std::endl;
- stream << "#if TRACE_EXECUTION" << std::endl;
- stream << "printf(\"Entry Set\");" << std::endl;
- printBitArray(stream, _prefix + "ctx.entry_set", _states.size());
- stream << "printf(\"\\n\");" << std::endl;
- stream << "#endif" << 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;
+ 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 << std::endl;
- stream << "} /* d_step */" << std::endl;
+
+ stream << std::endl;
+ stream << "#if TRACE_EXECUTION" << std::endl;
+ 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;
+}
+void ChartToPromela::writeFSMExitStates(std::ostream& stream) {
stream << "/* ---------------------------- */" << std::endl;
- stream << "/* EXIT_STATES: */" << std::endl;
- stream << "d_step {" << 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 << "ctx.exit_set[i] && " << _prefix << "config[i] -> {" << std::endl;
- stream << " /* call all on-exit handlers */" << std::endl;
-
+ stream << "/* EXIT_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 << "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*> onexits = DOMUtils::filterChildElements(XML_PREFIX(_states[i]).str() + "onexit" , _states[i]);
@@ -2058,24 +2345,22 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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;
+ 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 << " " << _prefix << "config[i] = false;" << std::endl;
- stream << " skip;" << 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 << "} /* d_step */" << std::endl;
- stream << std::endl;
-
-// TRACE_EXECUTION("Exited States")
-
+void ChartToPromela::writeFSMTakeTransitions(std::ostream& stream) {
stream << "/* ---------------------------- */" << std::endl;
stream << "/* TAKE_TRANSITIONS: */" << std::endl;
if (_transitions.size() > 0) {
-// stream << "d_step {" << std::endl;
stream << " i = 0;" << std::endl;
stream << " do" << std::endl;
stream << " :: i < " << _prefix << "USCXML_NUMBER_TRANS -> {" << std::endl;
@@ -2105,59 +2390,58 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << " }" << std::endl;
stream << " :: else -> break;" << std::endl;
stream << " od;" << std::endl;
-// stream << "} /* d_step */" << std::endl;
}
- stream << std::endl;
+}
+void ChartToPromela::writeFSMEnterStates(std::ostream& stream) {
stream << "/* ---------------------------- */" << std::endl;
- stream << "/* ENTER_STATES: */" << std::endl;
-// stream << "d_step {" << std::endl;
- stream << " i = 0;" << std::endl;
- stream << " do" << std::endl;
- stream << " :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
- stream << " if" << 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;
-
+ stream << "/* ENTER_STATES: */" << std::endl;
+ stream << " i = 0;" << std::endl;
+ stream << " do" << std::endl;
+ stream << " :: i < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
+ stream << " if" << 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;
+
TRACE_EXECUTION_V("Entering state %d", "i");
-
- stream << " " << _prefix << "config[i] = true;" << std::endl;
- stream << std::endl;
-
+
+ stream << " " << _prefix << "config[i] = true;" << std::endl;
+ stream << std::endl;
+
#if 0
- stream << " if" << std::endl;
- stream << " :: !" << _prefix << "initialized_data[i] -> {" << std::endl;
- stream << " /* TODO: late data binding not supported yet */" << std::endl;
- stream << " " << _prefix << "initialized_data[i] = true;" << std::endl;
- stream << " skip" << std::endl;
- stream << " }" << std::endl;
- stream << " :: else -> skip;" << std::endl;
- stream << " fi" << std::endl;
- stream << std::endl;
+ stream << " if" << std::endl;
+ stream << " :: !" << _prefix << "initialized_data[i] -> {" << std::endl;
+ stream << " /* TODO: late data binding not supported yet */" << std::endl;
+ stream << " " << _prefix << "initialized_data[i] = true;" << std::endl;
+ stream << " skip" << std::endl;
+ stream << " }" << std::endl;
+ stream << " :: else -> skip;" << std::endl;
+ stream << " fi" << 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;
+ 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;
- }
- }
- stream << " :: else ->skip;" << std::endl;
- stream << " fi" << std::endl;
- stream << std::endl;
-
- stream << " /* take history and initial transitions */" << std::endl;
+ for (auto onentry : onentries)
+ writeExecContent(stream, onentry, 5);
+ stream << " }" << std::endl;
+ }
+ }
+ stream << " :: else ->skip;" << std::endl;
+ stream << " fi" << std::endl;
+ stream << std::endl;
+
+ stream << " /* take history and initial transitions */" << std::endl;
if (_transitions.size() > 0) {
stream << " j = 0;" << std::endl;
stream << " do" << std::endl;
@@ -2172,7 +2456,7 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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;
@@ -2180,7 +2464,7 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << " :: else ->skip;" << std::endl;
stream << " fi" << std::endl;
stream << std::endl;
-
+
stream << " }" << std::endl;
stream << " :: else -> skip;" << std::endl;
stream << " fi" << std::endl;
@@ -2189,25 +2473,25 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << " :: else -> break;" << std::endl;
stream << " od" << std::endl;
}
-
- stream << " /* handle final states */" << std::endl;
- stream << " if" << std::endl;
- stream << " :: " << _prefix << "states[i].type[USCXML_STATE_FINAL] -> {" << std::endl;
-
- stream << " if" << std::endl;
- stream << " :: " << _prefix << "states[" << _prefix << "states[i].parent].children[1] -> {" << std::endl;
+
+ stream << " /* handle final states */" << std::endl;
+ stream << " if" << std::endl;
+ stream << " :: " << _prefix << "states[i].type[USCXML_STATE_FINAL] -> {" << std::endl;
+
+ stream << " if" << std::endl;
+ stream << " :: " << _prefix << "states[" << _prefix << "states[i].parent].children[1] -> {" << 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 << " }" << std::endl;
+ stream << " :: else -> {" << std::endl;
stream << " /* raise done event */" << std::endl;
stream << " if" << std::endl;
-
+
std::string insertOp = "!";
-// if (_analyzer->usesEventField("delay"))
-// insertOp += "!";
-
+ // if (_analyzer->usesEventField("delay"))
+ // insertOp += "!";
+
for (auto state : _states) {
if (state->getParentNode() == NULL || state->getParentNode()->getNodeType() != DOMNode::ELEMENT_NODE)
continue;
@@ -2218,16 +2502,16 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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);
@@ -2236,31 +2520,31 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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 << " 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 << " * 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;
-
+
stream << " k = 0;" << std::endl;
stream << " do" << std::endl;
stream << " :: k < " << _prefix << "USCXML_NUMBER_STATES -> {" << std::endl;
@@ -2286,18 +2570,18 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << " if" << std::endl;
stream << " :: !" << _prefix << "STATES_HAS_ANY(" << _prefix << "ctx.tmp_states) -> {" << std::endl;
stream << " if" << std::endl;
-
+
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);
@@ -2312,7 +2596,7 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << " :: else -> skip;" << std::endl;
stream << " fi" << std::endl;
-
+
stream << " }" << std::endl;
stream << " :: else -> skip;" << std::endl;
stream << " fi" << std::endl;
@@ -2323,32 +2607,27 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
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 << " }" << std::endl;
- stream << " :: else -> skip;" << std::endl;
- stream << " i = i + 1;" << std::endl;
- stream << " fi;" << std::endl;
- stream << " }" << std::endl;
- stream << " :: else -> break;" << 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 << " i = i + 1;" << std::endl;
+ stream << " fi;" << std::endl;
+ stream << " }" << std::endl;
+ stream << " :: else -> break;" << std::endl;
stream << " od;" << std::endl;
- stream << "} /* d_step */" << 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;
+void ChartToPromela::writeFSMTerminateMachine(std::ostream& stream) {
stream << "/* ---------------------------- */" << std::endl;
stream << _prefix << "TERMINATE_MACHINE:" << std::endl;
+
stream << "skip; d_step {" << std::endl;
TRACE_EXECUTION("Machine finished");
@@ -2404,21 +2683,21 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
stream << "}" << std::endl;
stream << ":: else -> break;" << std::endl;
stream << "od;" << std::endl;
-
+
stream << 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 (_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;
@@ -2441,22 +2720,14 @@ void ChartToPromela::writeFSM(std::ostream& stream) {
}
stream << "}" << std::endl;
stream << ":: else -> skip" << std::endl;
- stream << "fi" << std::endl;
+ stream << "fi;" << std::endl;
stream << std::endl;
-
+
}
stream << "} /* d_step */" << std::endl;
- stream << std::endl;
-
- TRACE_EXECUTION("Done");
-
-
- stream << "} }" << std::endl;
- stream << std::endl;
-
}
-
+
void ChartToPromela::writeIfBlock(std::ostream& stream, std::list<DOMElement*>& condChain, size_t indent) {
if (condChain.size() == 0)
return;
diff --git a/src/uscxml/transform/ChartToPromela.h b/src/uscxml/transform/ChartToPromela.h
index 8df3dca..b8b513e 100644
--- a/src/uscxml/transform/ChartToPromela.h
+++ b/src/uscxml/transform/ChartToPromela.h
@@ -55,6 +55,18 @@ protected:
// void writeTypes(std::ostream& stream);
void writeMacros(std::ostream& stream);
void writeFSM(std::ostream& stream);
+ void writeFSMDequeueEvent(std::ostream& stream);
+// void writeFSMRescheduleMachines(std::ostream& stream);
+// void writeFSMMacrostep(std::ostream& stream);
+// void writeFSMDequeueInternalOrSpontaneousEvent(std::ostream& stream);
+ void writeFSMSelectTransitions(std::ostream& stream);
+ void writeFSMRememberHistory(std::ostream& stream);
+ void writeFSMEstablishEntrySet(std::ostream& stream);
+ void writeFSMExitStates(std::ostream& stream);
+ void writeFSMTakeTransitions(std::ostream& stream);
+ void writeFSMEnterStates(std::ostream& stream);
+ void writeFSMTerminateMachine(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);
generated by cgit v0.12 at 2024-10-30 04:01:15 (GMT)