From 31efd06a62d5009f2a279f07bd6884c4ae075019 Mon Sep 17 00:00:00 2001 From: Stefan Radomski Date: Mon, 21 Nov 2016 14:30:05 +0100 Subject: Reduced state space for PROMELA transformation --- src/uscxml/transform/ChartToPromela.cpp | 1075 +++++++++++++++++++------------ src/uscxml/transform/ChartToPromela.h | 12 + 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 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 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 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 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 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 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 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 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 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 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 << " 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; + 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 << std::endl; - stream << "} /* d_step */" << 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 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 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 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(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 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 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& 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); -- cgit v0.12