diff options
Diffstat (limited to 'src/uscxml/transform')
| -rw-r--r-- | src/uscxml/transform/ChartToFSM.cpp | 281 | ||||
| -rw-r--r-- | src/uscxml/transform/ChartToFSM.h | 16 | ||||
| -rw-r--r-- | src/uscxml/transform/FSMToPromela.cpp | 1115 | ||||
| -rw-r--r-- | src/uscxml/transform/FSMToPromela.h | 120 | ||||
| -rw-r--r-- | src/uscxml/transform/FlatStateIdentifier.h | 67 |
5 files changed, 1300 insertions, 299 deletions
diff --git a/src/uscxml/transform/ChartToFSM.cpp b/src/uscxml/transform/ChartToFSM.cpp index 1971ae2..2c5aacd 100644 --- a/src/uscxml/transform/ChartToFSM.cpp +++ b/src/uscxml/transform/ChartToFSM.cpp @@ -33,17 +33,27 @@ #undef max #include <limits> +#define DUMP_TRANSSET(where) \ +{\ +std::cout << std::endl;\ +std::cout << "** " << transitions.size() << " ** " << where << std::endl;\ + for (int m = 0; m < transitions.size(); m++) {\ + std::cout << transitions[m] << std::endl;\ + }\ +} namespace uscxml { using namespace Arabica::DOM; using namespace Arabica::XPath; -#define CREATE_TRANSIENT_STATE_WITH_CHILDS \ +#define CREATE_TRANSIENT_STATE_WITH_CHILDS(stateId) \ if (childs.size() > 0) { \ Element<std::string> transientState = _flatDoc.createElementNS(_nsInfo.nsURL, "state"); \ _nsInfo.setPrefix(transientState);\ transientState.setAttribute("transient", "true"); \ + if (stateId.length() > 0) \ + transientState.setAttribute("id", stateId); \ for (int i = 0; i < childs.size(); i++) { \ Node<std::string> imported = _flatDoc.importNode(childs[i], true); \ transientState.appendChild(imported); \ @@ -52,6 +62,15 @@ if (childs.size() > 0) { \ } \ childs = NodeSet<std::string>(); +#define DETAIL_EXEC_CONTENT(field, actPtr) \ +std::cerr << " " << #field << " / " << TAGNAME_CAST(actPtr->field) << " ("; \ +NodeSet<std::string> contents = filterChildType(Node_base::ELEMENT_NODE, actPtr->field, true); \ +for (int i = 0; i < contents.size(); i++) { \ + std::cerr << " " << TAGNAME_CAST(contents[i]); \ +} \ +std::cerr << ")"; + + Interpreter ChartToFSM::flatten(const Interpreter& other) { // instantiate a new InterpreterImpl to do the flattening @@ -132,7 +151,7 @@ FlatteningInterpreter::FlatteningInterpreter(const Document<std::string>& doc) { _lastTimeStamp = tthread::chrono::system_clock::now(); _currGlobalTransition = NULL; _lastTransientStateId = 0; - + // just copy given doc into _document an create _flatDoc for the FSM DOMImplementation<std::string> domFactory = Arabica::SimpleDOM::DOMImplementation<std::string>::getDOMImplementation(); _document = domFactory.createDocument(doc.getNamespaceURI(), "", 0); @@ -199,6 +218,12 @@ InterpreterState FlatteningInterpreter::interpret() { _binding = (HAS_ATTR(_scxml, "binding") && iequals(ATTR(_scxml, "binding"), "late") ? LATE : EARLY); + // set invokeid for all invokers to parent state if none given + NodeSet<std::string> invokers = filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true); + for (int i = 0; i < invokers.size(); i++) { + Element<std::string> invokerElem = Element<std::string>(invokers[i]); + invokerElem.setAttribute("parent", ATTR_CAST(invokerElem.getParentNode(), "id")); + } // reset _globalConf.clear(); _currGlobalTransition = NULL; @@ -208,7 +233,7 @@ InterpreterState FlatteningInterpreter::interpret() { _start = new GlobalState(_configuration, _alreadyEntered, _historyValue, _nsInfo.xmlNSPrefix); _globalConf[_start->stateId] = _start; _globalConf[_start->stateId]->index = toStr(GlobalState::gIndex++); - + NodeSet<std::string> initialTransitions; // enter initial configuration @@ -229,7 +254,7 @@ InterpreterState FlatteningInterpreter::interpret() { labelTransitions(); // weightTransitions(); indexTransitions(_scxml); - + // std::cerr << _scxml << std::endl; GlobalTransition* globalTransition = new GlobalTransition(initialTransitions, _dataModel, this); @@ -251,7 +276,9 @@ InterpreterState FlatteningInterpreter::interpret() { #endif createDocument(); - + +// std::cout << _scxml << std::endl; + NodeSet<std::string> elements = InterpreterImpl::filterChildType(Node_base::ELEMENT_NODE, _scxml, true); uint64_t nrStates = 0; for (int i = 0; i < elements.size(); i++) { @@ -279,7 +306,9 @@ void FlatteningInterpreter::executeContent(const Arabica::DOM::Element<std::stri } else if (TAGNAME(content) == "onexit") { action.onExit = content; } else if (TAGNAME(content) == "onentry") { - action.onExit = content; + action.onEntry = content; + } else if (TAGNAME(content) == "history") { + assert(false); } else { // e.g. global script elements return; } @@ -410,7 +439,7 @@ void FlatteningInterpreter::indexTransitions(const Arabica::DOM::Element<std::st for (int i = levelTransitions.size() - 1; i >= 0; i--) { indexedTransitions.push_back(Element<std::string>(levelTransitions[i])); } - + Arabica::XPath::NodeSet<std::string> nextLevel = filterChildType(Arabica::DOM::Node_base::ELEMENT_NODE, root); for (int i = nextLevel.size() - 1; i >= 0; i--) { Element<std::string> stateElem = Element<std::string>(nextLevel[i]); @@ -424,7 +453,7 @@ bool GlobalTransition::operator< (const GlobalTransition& other) const { const std::list<Arabica::DOM::Element<std::string> >& indexedTransitions = interpreter->indexedTransitions; for (std::list<Element<std::string> >::const_reverse_iterator transIter = indexedTransitions.rbegin(); transIter != indexedTransitions.rend(); transIter++) { const Element<std::string>& refTrans = *transIter; - + if (InterpreterImpl::isMember(refTrans, transitions) && !InterpreterImpl::isMember(refTrans, other.transitions)) { return true; } @@ -434,7 +463,7 @@ bool GlobalTransition::operator< (const GlobalTransition& other) const { } return true; // actually, they are equal } - + void FlatteningInterpreter::explode() { @@ -467,14 +496,14 @@ void FlatteningInterpreter::explode() { delete globalState; return; // we have already been here } - + _globalConf[globalState->stateId] = globalState; _globalConf[globalState->stateId]->index = toStr(GlobalState::gIndex++); - assert(isLegalConfiguration(configuration)); +// assert(isLegalConfiguration(configuration)); if(_globalConf[globalState->stateId]->isFinal) return; // done in this branch - + // get all transition elements from states in the current configuration NodeSet<std::string> allTransitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", configuration); @@ -534,7 +563,7 @@ void FlatteningInterpreter::explode() { std::map<std::string, GlobalTransition*> transitionSets; while(1) { - // create the power set of all potential transitions + // create the power set of all potential transitions - this is expensive! // see: http://www.programminglogic.com/powerset-algorithm-in-c/ if (stack[k] < nrElements) { @@ -558,6 +587,19 @@ void FlatteningInterpreter::explode() { } // std::cerr << std::endl; +// transitions.push_back(allTransitions[0]); +// transitions.push_back(allTransitions[4]); +// transitions.push_back(allTransitions[5]); +// transitions.push_back(allTransitions[7]); + + bool dump = false; + +// if (k == 4 && stack[1] == 1 && stack[2] == 5 && stack[3] == 6 && stack[4] == 8) { +// dump = true; +// } + + if (dump) DUMP_TRANSSET("at start"); + _perfTotal++; _perfProcessed++; @@ -574,13 +616,17 @@ void FlatteningInterpreter::explode() { // remove transitions in the same state if(!filterSameState(transitions)) continue; + if (dump) DUMP_TRANSSET("after same state filtered"); // remove those transitions with a child transition if(!filterChildEnabled(transitions)) continue; + if (dump) DUMP_TRANSSET("after child enabled filtered"); // reduce to conflict-free subset + // transitions.to_document_order(); transitions = removeConflictingTransitions(transitions); + if (dump) DUMP_TRANSSET("after conflicting filtered"); // algorithm can never reduce to empty set assert(transitions.size() > 0); @@ -600,49 +646,6 @@ void FlatteningInterpreter::explode() { continue; } -#if 0 - for (int currDepth = 0; currDepth <= maxDepth; currDepth++) { - int lowestOrder = std::numeric_limits<int32_t>::max(); - int nrDepth = 0; - int prioPerLevel = 0; - for (int i = 0; i < transitions.size(); i++) { - int depth = strTo<int>(ATTR_CAST(transitions[i], "depth")); - if (depth != currDepth) - continue; - nrDepth++; - int order = strTo<int>(ATTR_CAST(transitions[i], "order")); - if (order < lowestOrder) - lowestOrder = order; - prioPerLevel += pow(static_cast<double>(maxOrder), maxOrder - order); - } - transition->nrElemPerLevel.push_back(nrDepth); - transition->firstElemPerLevel.push_back(lowestOrder); - transition->prioPerLevel.push_back(prioPerLevel); - } -#endif -#if 0 - // calculate priority - transition->priority = 0; - for (int currDepth = maxDepth; currDepth >= 0; currDepth--) { - // what's the deepest depth of this set? - for (int i = 0; i < transitions.size(); i++) { - int depth = strTo<int>(ATTR(transitions[i], "depth")); - if (depth == currDepth) { - int highestOrder = 0; - // what's the highest order at this depth? - for (int j = 0; j < transitions.size(); j++) { - int order = strTo<int>(ATTR(transitions[j], "order")); - if (order > highestOrder) - highestOrder = order; - } - transition->priority += pow(maxOrder + 1, currDepth); // + (maxOrder - highestOrder); - goto NEXT_DEPTH; - } - } -NEXT_DEPTH: - ; - } -#endif // remember this conflict-free set // std::cerr << "New conflict-free subset: " << transition->transitionId << ":" << transition->eventDesc << std::endl; transitionSets[transition->transitionId] = transition; @@ -666,19 +669,19 @@ NEXT_DEPTH: _currGlobalTransition = *transListIter; microstep((*transListIter)->transitions); - if (!isLegalConfiguration(_configuration)) { - FlatStateIdentifier fromState(configuration, alreadyEntered, historyValue); - FlatStateIdentifier toState(_configuration, _alreadyEntered, _historyValue); - std::cerr << "invalid configuration after transition " << std::endl - << "from \t" << fromState.getStateId() << std::endl - << "to \t" << toState.getStateId() << std::endl - << "via ------" << std::endl; - for (int i = 0; i < (*transListIter)->transitions.size(); i++) { - std::cerr << (*transListIter)->transitions[i] << std::endl; - } - std::cerr << "----------" << std::endl; - assert(false); - } +// if (!isLegalConfiguration(_configuration)) { +// FlatStateIdentifier fromState(configuration, alreadyEntered, historyValue); +// FlatStateIdentifier toState(_configuration, _alreadyEntered, _historyValue); +// std::cerr << "invalid configuration after transition " << std::endl +// << "from \t" << fromState.getStateId() << std::endl +// << "to \t" << toState.getStateId() << std::endl +// << "via ------" << std::endl; +// for (int i = 0; i < (*transListIter)->transitions.size(); i++) { +// std::cerr << (*transListIter)->transitions[i] << std::endl; +// } +// std::cerr << "----------" << std::endl; +// assert(false); +// } explode(); // reset state for next transition set @@ -706,6 +709,10 @@ void FlatteningInterpreter::createDocument() { _scxml.setAttribute("datamodel", ATTR(_origSCXML, "datamodel")); } + if (HAS_ATTR(_origSCXML, "name")) { + _scxml.setAttribute("name", ATTR(_origSCXML, "name")); + } + if (HAS_ATTR(_origSCXML, "binding")) { _scxml.setAttribute("binding", ATTR(_origSCXML, "binding")); } @@ -743,14 +750,14 @@ void FlatteningInterpreter::createDocument() { std::vector<std::pair<std::string,GlobalState*> > sortedStates; sortedStates.insert(sortedStates.begin(), _globalConf.begin(), _globalConf.end()); std::sort(sortedStates.begin(), sortedStates.end(), sortStatesByIndex); - + int index = 0; for (std::list<Element<std::string> >::reverse_iterator transIter = indexedTransitions.rbegin(); transIter != indexedTransitions.rend(); transIter++) { const Element<std::string>& refTrans = *transIter; std::cerr << index++ << ": " << refTrans << std::endl; } std::cerr << std::endl; - + for (std::vector<std::pair<std::string,GlobalState*> >::iterator confIter = sortedStates.begin(); confIter != sortedStates.end(); confIter++) { @@ -761,8 +768,7 @@ void FlatteningInterpreter::createDocument() { } -template <typename T> bool PtrComp(const T * const & a, const T * const & b) -{ +template <typename T> bool PtrComp(const T * const & a, const T * const & b) { return *a < *b; } @@ -794,17 +800,17 @@ bool hasEarlierUnconditionalMatch(GlobalTransition* first, GlobalTransition* sec // for some reason, unique is not quite up to the task std::list<GlobalTransition*> reapplyUniquePredicates(std::list<GlobalTransition*> list) { - + for (std::list<GlobalTransition*>::iterator outerIter = list.begin(); - outerIter != list.end(); - outerIter++) { + outerIter != list.end(); + outerIter++) { for (std::list<GlobalTransition*>::iterator innerIter = outerIter; - innerIter != list.end(); - innerIter++) { - + innerIter != list.end(); + innerIter++) { + if (innerIter == outerIter) continue; - + GlobalTransition* t1 = *outerIter; GlobalTransition* t2 = *innerIter; @@ -874,7 +880,8 @@ Node<std::string> FlatteningInterpreter::globalTransitionToNode(GlobalTransition #if 1 transition.setAttribute("members", globalTransition->members); #endif - + // transition.setAttribute("priority", toStr(globalTransition->priority)); + if (!globalTransition->isEventless) { transition.setAttribute("event", globalTransition->eventDesc); } @@ -883,50 +890,28 @@ Node<std::string> FlatteningInterpreter::globalTransitionToNode(GlobalTransition transition.setAttribute("cond", globalTransition->condition); } -// transition.setAttribute("priority", toStr(globalTransition->priority)); - -#if 0 - std::stringstream feSS; - std::string seperator = ""; - for (int i = 0; i < globalTransition->firstElemPerLevel.size(); i++) { - feSS << seperator << globalTransition->firstElemPerLevel[i]; - seperator = ", "; - } - transition.setAttribute("firstPerLevel", feSS.str()); - - std::stringstream nrSS; - seperator = ""; - for (int i = 0; i < globalTransition->nrElemPerLevel.size(); i++) { - nrSS << seperator << globalTransition->nrElemPerLevel[i]; - seperator = ", "; + if (globalTransition->destination.size() > 0) { + transition.setAttribute("final-target", globalTransition->destination); } - transition.setAttribute("numberPerLevel", nrSS.str()); - - std::stringstream prSS; - seperator = ""; - for (int i = 0; i < globalTransition->prioPerLevel.size(); i++) { - prSS << seperator << globalTransition->prioPerLevel[i]; - seperator = ", "; - } - transition.setAttribute("prioPerLevel", nrSS.str()); -#endif + NodeSet<std::string> transientStateChain; -// std::cerr << " firstPerLevel:" << feSS.str() << " " << globalTransition->transitionId << std::endl; -// std::cerr << "event: " << globalTransition->eventDesc << " firstPerLevel:" << feSS.str() << " numberPerLevel:" << nrSS.str() << " prioPerLevel:" << prSS.str() << " " << globalTransition->transitionId << std::endl; -// std::cerr << globalTransition->transitionId << std::endl; + // current active state set + FlatStateIdentifier flatId(globalTransition->source); + std::list<std::string> currActiveStates = flatId.getActive(); - NodeSet<std::string> transientStateChain; +// std::cerr << "From " << globalTransition->source << " to " << globalTransition->destination << ":" << std::endl; // gather content for new transient state NodeSet<std::string> childs; - // iterate all actions taken during the transition for (std::list<GlobalTransition::Action>::iterator actionIter = globalTransition->actions.begin(); actionIter != globalTransition->actions.end(); actionIter++) { if (actionIter->transition) { +// DETAIL_EXEC_CONTENT(transition, actionIter); + Element<std::string> onexit = _flatDoc.createElementNS(_nsInfo.nsURL, "onexit"); _nsInfo.setPrefix(onexit); Node<std::string> child = actionIter->transition.getFirstChild(); @@ -935,24 +920,31 @@ Node<std::string> FlatteningInterpreter::globalTransitionToNode(GlobalTransition onexit.appendChild(imported); child = child.getNextSibling(); } + // only append if there is something done if (onexit.hasChildNodes()) childs.push_back(onexit); + continue; } if (actionIter->onExit) { +// DETAIL_EXEC_CONTENT(onExit, actionIter); + childs.push_back(actionIter->onExit); continue; } if (actionIter->onEntry) { +// DETAIL_EXEC_CONTENT(onEntry, actionIter); + childs.push_back(actionIter->onEntry); continue; } if (actionIter->invoke) { +// DETAIL_EXEC_CONTENT(invoke, actionIter); if (!globalTransition->isTargetless) { - CREATE_TRANSIENT_STATE_WITH_CHILDS +// CREATE_TRANSIENT_STATE_WITH_CHILDS(FlatStateIdentifier::toStateId(currActiveStates)); } Element<std::string> invokeElem = Element<std::string>(actionIter->invoke); invokeElem.setAttribute("persist", "true"); @@ -961,6 +953,7 @@ Node<std::string> FlatteningInterpreter::globalTransitionToNode(GlobalTransition } if (actionIter->uninvoke) { +// DETAIL_EXEC_CONTENT(uninvoke, actionIter); Element<std::string> uninvokeElem = _flatDoc.createElementNS(_nsInfo.nsURL, "uninvoke"); _nsInfo.setPrefix(uninvokeElem); @@ -980,7 +973,20 @@ Node<std::string> FlatteningInterpreter::globalTransitionToNode(GlobalTransition continue; } + if (actionIter->exited) { +// std::cerr << " exited(" << ATTR_CAST(actionIter->exited, "id") << ")"; + currActiveStates.remove(ATTR_CAST(actionIter->exited, "id")); + if (childs.size() > 0) { + CREATE_TRANSIENT_STATE_WITH_CHILDS(FlatStateIdentifier::toStateId(currActiveStates)); // create a new transient state to update its id + } + } + if (actionIter->entered) { +// std::cerr << " entered(" << ATTR_CAST(actionIter->entered, "id") << ")"; + if (childs.size() > 0) + CREATE_TRANSIENT_STATE_WITH_CHILDS(FlatStateIdentifier::toStateId(currActiveStates)); // create a new transient state to update its id + currActiveStates.push_back(ATTR_CAST(actionIter->entered, "id")); + // we entered a new child - check if it has a datamodel and we entered for the first time if (_binding == InterpreterImpl::LATE) { NodeSet<std::string> datamodel = filterChildElements(_nsInfo.xmlNSPrefix + "datamodel", actionIter->entered); @@ -990,46 +996,58 @@ Node<std::string> FlatteningInterpreter::globalTransitionToNode(GlobalTransition } } if (!globalTransition->isTargetless) { - CREATE_TRANSIENT_STATE_WITH_CHILDS +// CREATE_TRANSIENT_STATE_WITH_CHILDS(FlatStateIdentifier::toStateId(currActiveStates)) } } - if (globalTransition->isTargetless) { - for (int i = 0; i < childs.size(); i++) { - Node<std::string> imported = _flatDoc.importNode(childs[i], true); - transition.appendChild(imported); - } - return transition; - } +// std::cerr << std::endl; + +// if (globalTransition->isTargetless) { +// for (int i = 0; i < childs.size(); i++) { +// Node<std::string> imported = _flatDoc.importNode(childs[i], true); +// transition.appendChild(imported); +// // CREATE_TRANSIENT_STATE_WITH_CHILDS(FlatStateIdentifier::toStateId(currActiveStates)) +// } +// return transition; +// } - CREATE_TRANSIENT_STATE_WITH_CHILDS + CREATE_TRANSIENT_STATE_WITH_CHILDS(FlatStateIdentifier::toStateId(currActiveStates)) if (transientStateChain.size() > 0) { + Element<std::string> prevExitTransitionElem; + for (int i = 0; i < transientStateChain.size(); i++) { Element<std::string> transientStateElem = Element<std::string>(transientStateChain[i]); -// transientStateElem.setAttribute("id", "transient-" + globalTransition->transitionId + "-" + globalTransition->source + "-" + toStr(i)); - transientStateElem.setAttribute("id", globalTransition->destination + "-via-" + toStr(_lastTransientStateId++)); + transientStateElem.setAttribute("id", transientStateElem.getAttribute("id") + "-via-" + toStr(_lastTransientStateId++)); Element<std::string> exitTransition = _flatDoc.createElementNS(_nsInfo.nsURL, "transition"); _nsInfo.setPrefix(exitTransition); - if (i == transientStateChain.size() - 1) { - exitTransition.setAttribute("target", globalTransition->destination); + if (prevExitTransitionElem) { + // point previous to this one + prevExitTransitionElem.setAttribute("target", transientStateElem.getAttribute("id")); } else { -// exitTransition.setAttribute("target", "transient-" + globalTransition->transitionId + "-" + globalTransition->source + "-" + toStr(i + 1)); - exitTransition.setAttribute("target", globalTransition->destination + "-via-" + toStr(_lastTransientStateId)); + // update globalTransition->source target } + transientStateElem.appendChild(exitTransition); + prevExitTransitionElem = exitTransition; if (i == 0) transition.setAttribute("target", transientStateElem.getAttribute("id")); _scxml.appendChild(transientStateElem); } + + // last one points to actual target + assert(prevExitTransitionElem); + prevExitTransitionElem.setAttribute("target", globalTransition->destination); + } else { transition.setAttribute("target", globalTransition->destination); } + assert(HAS_ATTR_CAST(transition, "target")); return transition; } @@ -1101,7 +1119,7 @@ int GlobalState::gIndex = 0; GlobalState::GlobalState(const Arabica::XPath::NodeSet<std::string>& activeStates_, const Arabica::XPath::NodeSet<std::string>& alreadyEnteredStates_, // we need to remember for binding=late const std::map<std::string, Arabica::XPath::NodeSet<std::string> >& historyStates_, - const std::string& xmlNSPrefix) { + const std::string& xmlNSPrefix) { // make copies and sort activeStates = activeStates_; @@ -1117,7 +1135,7 @@ GlobalState::GlobalState(const Arabica::XPath::NodeSet<std::string>& activeState break; } } - + // sort configuration activeStates.to_document_order(); alreadyEnteredStates.to_document_order(); @@ -1176,6 +1194,9 @@ GlobalTransition::GlobalTransition(const Arabica::XPath::NodeSet<std::string>& t index++; } +// if (members == " 4 6 7 ") +// std::cout << "asdfadf"; + /** * Can these events event occur together? They can't if: * 1. event / eventless is mixed diff --git a/src/uscxml/transform/ChartToFSM.h b/src/uscxml/transform/ChartToFSM.h index a60985d..2f97a24 100644 --- a/src/uscxml/transform/ChartToFSM.h +++ b/src/uscxml/transform/ChartToFSM.h @@ -21,7 +21,7 @@ #define CHARTTOFSM_H_IOKPYEBY #include "uscxml/DOMUtils.h" -#include "uscxml/interpreter/InterpreterDraft6.h" +#include "uscxml/interpreter/InterpreterRC.h" #include <DOM/Document.hpp> #include <DOM/Node.hpp> #include <XPath/XPath.hpp> @@ -32,7 +32,7 @@ namespace uscxml { class GlobalState; class GlobalTransition; class FlatteningInterpreter; - + class USCXML_API GlobalState { public: @@ -40,7 +40,7 @@ public: GlobalState(const Arabica::XPath::NodeSet<std::string>& activeStates, const Arabica::XPath::NodeSet<std::string>& alreadyEnteredStates, // we need to remember for binding=late const std::map<std::string, Arabica::XPath::NodeSet<std::string> >& historyStates, - const std::string& xmlNSPrefix); + const std::string& xmlNSPrefix); Arabica::XPath::NodeSet<std::string> activeStates; Arabica::XPath::NodeSet<std::string> alreadyEnteredStates; @@ -51,7 +51,7 @@ public: std::string stateId; static int gIndex; - + std::string index; bool isFinal; }; @@ -103,14 +103,14 @@ public: std::string index; FlatteningInterpreter* interpreter; - + bool operator< (const GlobalTransition& other) const; - + protected: std::list<std::string> getCommonEvents(const Arabica::XPath::NodeSet<std::string>& transitions); }; -class USCXML_API FlatteningInterpreter : public InterpreterDraft6, public InterpreterMonitor { +class USCXML_API FlatteningInterpreter : public InterpreterRC, public InterpreterMonitor { public: FlatteningInterpreter(const Arabica::DOM::Document<std::string>& doc); virtual ~FlatteningInterpreter(); @@ -161,7 +161,7 @@ protected: int maxOrder; size_t _lastTransientStateId; - + Arabica::DOM::Document<std::string> _flatDoc; std::map<std::string, GlobalState*> _globalConf; }; diff --git a/src/uscxml/transform/FSMToPromela.cpp b/src/uscxml/transform/FSMToPromela.cpp index 238e40f..8c2836f 100644 --- a/src/uscxml/transform/FSMToPromela.cpp +++ b/src/uscxml/transform/FSMToPromela.cpp @@ -19,7 +19,10 @@ #include "uscxml/transform/ChartToFSM.h" #include "uscxml/transform/FSMToPromela.h" +#include "uscxml/transform/FlatStateIdentifier.h" #include "uscxml/plugins/datamodel/promela/PromelaParser.h" +#include "uscxml/plugins/datamodel/promela/parser/promela.tab.hpp" + #include <DOM/io/Stream.hpp> #include <iostream> #include "uscxml/UUID.h" @@ -27,6 +30,15 @@ #include <boost/algorithm/string.hpp> #include <glog/logging.h> +#define MAX_MACRO_CHARS 64 +#define MIN_COMMENT_PADDING 60 + +#define BIT_WIDTH(number) (number > 1 ? (int)ceil(log((double)number) / log((double)2.0)) : 1) + +#define INDENT_MIN(stream, start, cols) \ +for (int indentIndex = start; indentIndex < cols; indentIndex++) \ + stream << " "; + namespace uscxml { using namespace Arabica::DOM; @@ -39,7 +51,7 @@ void FSMToPromela::writeProgram(std::ostream& stream, promelaWriter.writeProgram(stream); } -FSMToPromela::FSMToPromela() : _eventTrie(".") { +FSMToPromela::FSMToPromela() { } void PromelaEventSource::writeStartEventSources(std::ostream& stream, int indent) { @@ -126,16 +138,18 @@ void PromelaEventSource::writeEventSource(std::ostream& stream) { stream << " " << ":: " << sourceName << "EventSourceDone -> skip;" << std::endl; stream << " " << ":: else { " << std::endl; + Trie& trie = analyzer->getTrie(); + if (sourceIter->type == PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM) { std::string content = sourceIter->content; boost::replace_all(content, "#REDO#", sourceName + "NewEvent"); boost::replace_all(content, "#DONE#", sourceName + "Done"); - std::list<TrieNode*> eventNames = trie->getChildsWithWords(trie->getNodeWithPrefix("")); + std::list<TrieNode*> eventNames = trie.getChildsWithWords(trie.getNodeWithPrefix("")); std::list<TrieNode*>::iterator eventNameIter = eventNames.begin(); while(eventNameIter != eventNames.end()) { - boost::replace_all(content, "#" + (*eventNameIter)->value + "#", "e" + toStr((*eventNameIter)->identifier)); + boost::replace_all(content, "#" + (*eventNameIter)->value + "#", (*eventNameIter)->identifier); eventNameIter++; } @@ -150,7 +164,7 @@ void PromelaEventSource::writeEventSource(std::ostream& stream) { stream << " " << ":: "; std::list<std::string>::const_iterator evIter = seqIter->begin(); while(evIter != seqIter->end()) { - TrieNode* node = trie->getNodeWithPrefix(*evIter); + TrieNode* node = trie.getNodeWithPrefix(*evIter); stream << "eQ!" << node->identifier << "; "; evIter++; } @@ -173,54 +187,409 @@ void PromelaEventSource::writeEventSource(std::ostream& stream) { PromelaEventSource::PromelaEventSource() { type = PROMELA_EVENT_SOURCE_INVALID; - trie = NULL; + analyzer = NULL; } PromelaEventSource::PromelaEventSource(const PromelaInlines& sources, const Arabica::DOM::Node<std::string>& parent) { type = PROMELA_EVENT_SOURCE_INVALID; - trie = NULL; + analyzer = NULL; eventSources = sources; container = parent; } +void PromelaCodeAnalyzer::addCode(const std::string& code) { + PromelaParser parser(code); + + // find all strings + std::list<PromelaParserNode*> astNodes; + astNodes.push_back(parser.ast); + + while(astNodes.size() > 0) { + PromelaParserNode* node = astNodes.front(); + astNodes.pop_front(); + + switch (node->type) { + case PML_STRING: { + std::string unquoted = node->value; + if (boost::starts_with(unquoted, "'")) { + unquoted = unquoted.substr(1, unquoted.size() - 2); + } + addLiteral(unquoted); + break; + } + case PML_CMPND: { + std::string nameOfType; + std::list<PromelaParserNode*>::iterator opIter = node->operands.begin(); + assert((*opIter)->type == PML_NAME); + + PromelaTypedef* td = &_typeDefs; + std::string seperator; + + while(opIter != node->operands.end()) { + switch ((*opIter)->type) { + case PML_NAME: + td = &td->types[(*opIter)->value]; + nameOfType += seperator + (*opIter)->value; + if (nameOfType.compare("_x") == 0) + _usesPlatformVars = true; + seperator = "_"; + td->name = nameOfType + "_t"; + break; + case PML_VAR_ARRAY: { + PromelaParserNode* name = (*opIter)->operands.front(); + PromelaParserNode* subscript = *(++(*opIter)->operands.begin()); + td = &td->types[name->value]; + nameOfType += seperator + name->value; + td->name = nameOfType + "_t"; + + if (isInteger(subscript->value.c_str(), 10)) { + td->arraySize = strTo<int>(subscript->value); + } + break; + } + default: + node->dump(); + assert(false); + break; + } + + if (nameOfType.compare("_x_states") == 0) { + _usesInPredicate = true; + } + if (nameOfType.compare("_event_type") == 0) { + addLiteral("internal"); + addLiteral("external"); + addLiteral("platform"); + } + if (nameOfType.compare("_event_origintype") == 0) { + addLiteral("http://www.w3.org/TR/scxml/#SCXMLEventProcessor"); + } + opIter++; + } + break; + } + case PML_NAME: { + } + default: + break; +// node->dump(); +// assert(false); + } + + astNodes.merge(node->operands); + } +} + +void PromelaCodeAnalyzer::addEvent(const std::string& eventName) { + if (_events.find(eventName) != _events.end()) + return; + + addLiteral(eventName, _lastEventIndex); + assert(_strIndex.find(eventName) != _strIndex.end()); + + _eventTrie.addWord(eventName); + _events[eventName] = _strIndex[eventName]; + _lastEventIndex++; +} + +void PromelaCodeAnalyzer::addState(const std::string& stateName) { + if (_states.find(stateName) != _states.end()) + return; + + createMacroName(stateName); + +// addLiteral(stateName); +// _states[stateName] = enumerateLiteral(stateName); + if (_origStateMap.find(stateName) == _origStateMap.end()) { + FlatStateIdentifier flatId(stateName); + _origStateMap[stateName] = flatId.getActive(); + for (std::list<std::string>::iterator origIter = _origStateMap[stateName].begin(); origIter != _origStateMap[stateName].end(); origIter++) { + //addLiteral(*origIter); // add original state names as string literals + if (_origStateIndex.find(*origIter) == _origStateIndex.end()) { + _origStateIndex[*origIter] = _lastStateIndex++; + createMacroName(*origIter); + } + } + } +} + +int PromelaCodeAnalyzer::arrayIndexForOrigState(const std::string& stateName) { + if (_origStateIndex.find(stateName) == _origStateIndex.end()) + throw std::runtime_error("No original state " + stateName + " known"); + return _origStateIndex[stateName]; +} + +void PromelaCodeAnalyzer::addLiteral(const std::string& literal, int forceIndex) { + if (boost::starts_with(literal, "'")) + throw std::runtime_error("Literal " + literal + " passed with quotes"); + + if (_strLiterals.find(literal) != _strLiterals.end()) + return; + + _strLiterals.insert(literal); + createMacroName(literal); + enumerateLiteral(literal, forceIndex); +} + +int PromelaCodeAnalyzer::enumerateLiteral(const std::string& literal, int forceIndex) { + if (forceIndex >= 0) { + _strIndex[literal] = forceIndex; + return forceIndex; + } + + if (_strIndex.find(literal) != _strIndex.end()) + return _strIndex[literal]; + + _strIndex[literal] = ++_lastStrIndex; + return _lastStrIndex + 1; +} + +std::string PromelaCodeAnalyzer::createMacroName(const std::string& literal) { + if (_strMacroNames.find(literal) != _strMacroNames.end()) + return _strMacroNames[literal]; + + // find a suitable macro name for the strings + std::string macroName = literal; //literal.substr(1, literal.size() - 2); + + // cannot start with digit + if (isInteger(macroName.substr(0,1).c_str(), 10)) + macroName = "_" + macroName; + + macroName = macroName.substr(0, MAX_MACRO_CHARS); + boost::to_upper(macroName); + + std::string illegalChars = "#\\/:?\"<>| \n\t()[]{}',.-"; + std::string tmp; + std::string::iterator it = macroName.begin(); + while (it < macroName.end()) { + bool found = illegalChars.find(*it) != std::string::npos; + if(found) { + tmp += '_'; + it++; + while(it < macroName.end() && illegalChars.find(*it) != std::string::npos) { + it++; + } + } else { + tmp += *it++; + } + } + macroName = tmp; + + unsigned int index = 2; + while (_macroNameSet.find(macroName) != _macroNameSet.end()) { + std::string suffix = toStr(index); + if (macroName.size() > suffix.size()) { + macroName = macroName.substr(0, macroName.size() - suffix.size()) + suffix; + } else { + macroName = suffix; + } + index++; + } + + _macroNameSet.insert(macroName); + _strMacroNames[literal] = macroName; + return macroName; +} + +std::string PromelaCodeAnalyzer::macroForLiteral(const std::string& literal) { + if (boost::starts_with(literal, "'")) + throw std::runtime_error("Literal " + literal + " passed with quotes"); + + if (_strMacroNames.find(literal) == _strMacroNames.end()) + throw std::runtime_error("No macro for literal " + literal + " known"); + return _strMacroNames[literal]; +} + +int PromelaCodeAnalyzer::indexForLiteral(const std::string& literal) { + if (boost::starts_with(literal, "'")) + throw std::runtime_error("Literal " + literal + " passed with quotes"); + + if (_strIndex.find(literal) == _strIndex.end()) + throw std::runtime_error("No index for literal " + literal + " known"); + return _strIndex[literal]; +} + +std::string PromelaCodeAnalyzer::replaceLiterals(const std::string code) { + std::string replaced = code; + for (std::map<std::string, std::string>::const_iterator litIter = _strMacroNames.begin(); litIter != _strMacroNames.end(); litIter++) { + boost::replace_all(replaced, "'" + litIter->first + "'", litIter->second); + } + return replaced; +} + +std::set<std::string> PromelaCodeAnalyzer::getEventsWithPrefix(const std::string& prefix) { + std::set<std::string> eventNames; + std::list<TrieNode*> trieNodes = _eventTrie.getWordsWithPrefix(prefix); + + std::list<TrieNode*>::iterator trieIter = trieNodes.begin(); + while(trieIter != trieNodes.end()) { + eventNames.insert((*trieIter)->value); + trieIter++; + } + + return eventNames; +} + + void FSMToPromela::writeEvents(std::ostream& stream) { - std::list<TrieNode*> eventNames = _eventTrie.getWordsWithPrefix(""); - std::list<TrieNode*>::iterator eventIter = eventNames.begin(); - stream << "// event name identifiers" << std::endl; - while(eventIter != eventNames.end()) { - stream << "#define " << "e" << (*eventIter)->identifier << " " << (*eventIter)->identifier; - stream << " // from \"" << (*eventIter)->value << "\"" << std::endl; + std::map<std::string, int> events = _analyzer.getEvents(); + std::map<std::string, int>::iterator eventIter = events.begin(); + stream << "/* event name identifiers */" << std::endl; + while(eventIter != events.end()) { + if (eventIter->first.length() > 0) { + stream << "#define " << _analyzer.macroForLiteral(eventIter->first) << " " << _analyzer.indexForLiteral(eventIter->first); + stream << " /* from \"" << eventIter->first << "\" */" << std::endl; + } eventIter++; } } void FSMToPromela::writeStates(std::ostream& stream) { - stream << "// state name identifiers" << std::endl; + stream << "/* state name identifiers */" << std::endl; for (int i = 0; i < _globalStates.size(); i++) { stream << "#define " << "s" << i << " " << i; - stream << " // from \"" << ATTR_CAST(_globalStates[i], "id") << "\"" << std::endl; + stream << " /* from \"" << ATTR_CAST(_globalStates[i], "id") << "\" */" << std::endl; + } +} + +void FSMToPromela::writeStateMap(std::ostream& stream) { + stream << "/* macros for original state names */" << std::endl; + std::map<std::string, int> origStates = _analyzer.getOrigStates(); + for (std::map<std::string, int>::iterator origIter = origStates.begin(); origIter != origStates.end(); origIter++) { + stream << "#define " << _analyzer.macroForLiteral(origIter->first) << " " << origIter->second; + stream << " /* from \"" << origIter->first << "\" */" << std::endl; } +// std::map<std::string, int> states = _analyzer.getStates(); +// size_t stateIndex = 0; +// for (std::map<std::string, int>::iterator stateIter = states.begin(); stateIter != states.end(); stateIter++) { +// stream << "_x" +// std::list<std::string> origStates = _analyzer.getOrigState(stateIter->first); +// size_t origIndex = 0; +// for (std::list<std::string>::iterator origIter = origStates.begin(); origIter != origStates.end(); origIter++) { +// +// } +// } } -Arabica::XPath::NodeSet<std::string> FSMToPromela::getTransientContent(const Arabica::DOM::Element<std::string>& state) { +void FSMToPromela::writeTypeDefs(std::ostream& stream) { + stream << "/* typedefs */" << std::endl; + PromelaCodeAnalyzer::PromelaTypedef typeDefs = _analyzer.getTypes(); + if (typeDefs.types.size() == 0) + return; + + std::list<PromelaCodeAnalyzer::PromelaTypedef> individualDefs; + std::list<PromelaCodeAnalyzer::PromelaTypedef> currDefs; + currDefs.push_back(typeDefs); + + while(currDefs.size() > 0) { + if (std::find(individualDefs.begin(), individualDefs.end(), currDefs.front()) == individualDefs.end()) { + individualDefs.push_back(currDefs.front()); + for (std::map<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator typeIter = currDefs.front().types.begin(); typeIter != currDefs.front().types.end(); typeIter++) { + currDefs.push_back(typeIter->second); + } + } + currDefs.pop_front(); + } + individualDefs.pop_front(); + + for (std::list<PromelaCodeAnalyzer::PromelaTypedef>::reverse_iterator rIter = individualDefs.rbegin(); rIter != individualDefs.rend(); rIter++) { + PromelaCodeAnalyzer::PromelaTypedef currDef = *rIter; + if (currDef.types.size() == 0 || currDef.name.size() == 0) + continue; +// if (currDef.name.compare("_x_t") == 0) { +// stream << "typedef platform_t {" << std::endl; +// if (_analyzer.usesInPredicate()) { +// stream << " bool states[" << _analyzer.getOrigStates().size() << "];" << std::endl; +// } +// stream << "};" << std::endl; +// +// continue; +// } + stream << "typedef " << currDef.name << " {" << std::endl; + if (currDef.name.compare("_event_t") == 0 && currDef.types.find("name") == currDef.types.end()) { // special treatment for _event + stream << " int name;" << std::endl; + } + for (std::map<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator tIter = currDef.types.begin(); tIter != currDef.types.end(); tIter++) { + if (currDef.name.compare("_x_t") == 0 && tIter->first.compare("states") == 0) { + stream << " bool states[" << _analyzer.getOrigStates().size() << "];" << std::endl; + continue; + } + if (tIter->second.types.size() == 0) { + stream << " int " << tIter->first << ";" << std::endl; // not further nested + } else { + stream << " " << tIter->second.name << " " << tIter->first << ";" << std::endl; + } + } + stream << "};" << std::endl << std::endl; + } + + stream << "/* typedef instances */" << std::endl; + PromelaCodeAnalyzer::PromelaTypedef allTypes = _analyzer.getTypes(); + std::map<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator typeIter = allTypes.types.begin(); + while(typeIter != allTypes.types.end()) { + stream << typeIter->second.name << " " << typeIter->first << ";" << std::endl; + typeIter++; + } + +} + +Arabica::XPath::NodeSet<std::string> FSMToPromela::getTransientContent(const Arabica::DOM::Element<std::string>& state, const std::string& source) { Arabica::XPath::NodeSet<std::string> content; Arabica::DOM::Element<std::string> currState = state; + FlatStateIdentifier prevFlatId(source); for (;;) { - if (!HAS_ATTR(currState, "transient") || !DOMUtils::attributeIsTrue(ATTR(currState, "transient"))) + if (_analyzer.usesInPredicate()) { + // insert state assignments into executable content + + std::stringstream stateSetPromela; + stateSetPromela << "#promela-inline " << std::endl; + FlatStateIdentifier currFlatId(ATTR(currState, "id")); + stateSetPromela << " /* from " << prevFlatId.getFlatActive() << " to " << currFlatId.getFlatActive() << " */" << std::endl; + + // add all that are missing from prevFlatId + std::map<std::string, int> allOrigStates = _analyzer.getOrigStates(); + for (std::map<std::string, int>::iterator allOrigIter = allOrigStates.begin(); allOrigIter != allOrigStates.end(); allOrigIter++) { + if (std::find(currFlatId.getActive().begin(), currFlatId.getActive().end(), allOrigIter->first) != currFlatId.getActive().end() && + std::find(prevFlatId.getActive().begin(), prevFlatId.getActive().end(), allOrigIter->first) == prevFlatId.getActive().end()) { + // active now but not previously + stateSetPromela << " _x.states[" << _analyzer.macroForLiteral(allOrigIter->first) << "] = true; " << std::endl; + } else if (std::find(currFlatId.getActive().begin(), currFlatId.getActive().end(), allOrigIter->first) == currFlatId.getActive().end() && + std::find(prevFlatId.getActive().begin(), prevFlatId.getActive().end(), allOrigIter->first) != prevFlatId.getActive().end()) { + // previously active but not now + stateSetPromela << " _x.states[" << _analyzer.macroForLiteral(allOrigIter->first) << "] = false; " << std::endl; + } + } + Comment<std::string> comment = _document.createComment(stateSetPromela.str()); + _document.importNode(comment, true); + currState.insertBefore(comment, currState.getFirstChild()); + prevFlatId = currFlatId; + } + + content.push_back(filterChildType(Node_base::COMMENT_NODE, currState)); + if (_analyzer.usesInPredicate()) assert(content.size() > 0); + + if (!HAS_ATTR(currState, "transient") || !DOMUtils::attributeIsTrue(ATTR(currState, "transient"))) { + // breaking here causes final state assignment to be written break; + } + content.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "invoke", currState)); content.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "onentry", currState)); content.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "onexit", currState)); + NodeSet<std::string> transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", currState); currState = _states[ATTR_CAST(transitions[0], "target")]; } - return content; } Node<std::string> FSMToPromela::getUltimateTarget(const Arabica::DOM::Element<std::string>& transition) { + if (!HAS_ATTR(transition, "target")) { + return transition.getParentNode(); + } + Arabica::DOM::Element<std::string> currState = _states[ATTR_CAST(transition, "target")]; for (;;) { @@ -237,7 +606,7 @@ void FSMToPromela::writeInlineComment(std::ostream& stream, const Arabica::DOM:: std::string comment = node.getNodeValue(); boost::trim(comment); - if (!boost::starts_with(comment, "promela-inline:")) + if (!boost::starts_with(comment, "#promela-inline")) return; std::stringstream ssLine(comment); @@ -250,18 +619,25 @@ void FSMToPromela::writeInlineComment(std::ostream& stream, const Arabica::DOM:: } } -void FSMToPromela::writeExecutableContent(std::ostream& stream, const Arabica::DOM::Element<std::string>& node, int indent) { +void FSMToPromela::writeExecutableContent(std::ostream& stream, const Arabica::DOM::Node<std::string>& node, int indent) { + +// std::cout << std::endl << node << std::endl; + if (!node) + return; std::string padding; for (int i = 0; i < indent; i++) { padding += " "; } +// std::cerr << node << std::endl; + if (node.getNodeType() == Node_base::COMMENT_NODE) { + // we cannot have labels in an atomic block, just process inline promela std::string comment = node.getNodeValue(); boost::trim(comment); std::stringstream inlinePromela; - if (!boost::starts_with(comment, "promela-inline:")) + if (!boost::starts_with(comment, "#promela-inline")) return; std::stringstream ssLine(comment); std::string line; @@ -278,81 +654,166 @@ void FSMToPromela::writeExecutableContent(std::ostream& stream, const Arabica::D if (node.getNodeType() != Node_base::ELEMENT_NODE) return; + Arabica::DOM::Element<std::string> nodeElem = Arabica::DOM::Element<std::string>(node); + if (false) { - } else if(TAGNAME(node) == "state") { - if (HAS_ATTR(node, "transient") && DOMUtils::attributeIsTrue(ATTR(node, "transient"))) { - Arabica::XPath::NodeSet<std::string> execContent = getTransientContent(node); - for (int i = 0; i < execContent.size(); i++) { - writeExecutableContent(stream, Arabica::DOM::Element<std::string>(execContent[i]), indent); - } - } else { - Arabica::DOM::Node<std::string> child = node.getFirstChild(); - while(child) { - writeExecutableContent(stream, Arabica::DOM::Element<std::string>(child), indent); - child = child.getNextSibling(); - } - } - } else if(TAGNAME(node) == "transition") { - stream << "t" << _transitions[node] << ":" << std::endl; +// } else if(TAGNAME(nodeElem) == "state") { +// if (HAS_ATTR(nodeElem, "transient") && DOMUtils::attributeIsTrue(ATTR(nodeElem, "transient"))) { +// Arabica::XPath::NodeSet<std::string> execContent = getTransientContent(nodeElem); +// for (int i = 0; i < execContent.size(); i++) { +// writeExecutableContent(stream, execContent[i], indent); +// } +// } + } else if(TAGNAME(nodeElem) == "transition") { + stream << "t" << _transitions[nodeElem] << ":"; + + int number = _transitions[nodeElem]; + int digits = 0; + do { + number /= 10; + digits++; + } while (number != 0); + + INDENT_MIN(stream, 2 + digits, MIN_COMMENT_PADDING); + + Node<std::string> source = node.getParentNode(); + stream << " /* from state " << ATTR_CAST(source, "id") << " */" << std::endl; + + // gather all executable content + NodeSet<std::string> execContent = getTransientContent(_states[ATTR(nodeElem, "target")], ATTR_CAST(source, "id")); // check for special promela labels - PromelaInlines promInls = getInlinePromela(getTransientContent(_states[ATTR(node, "target")]), true); - - if (promInls.acceptLabels > 0) - stream << padding << "acceptLabelT" << _transitions[node] << ":" << std::endl; - if (promInls.endLabels > 0) - stream << padding << "endLabelT" << _transitions[node] << ":" << std::endl; - if (promInls.progressLabels > 0) - stream << padding << "progressLabelT" << _transitions[node] << ":" << std::endl; + if (HAS_ATTR(nodeElem, "target")) { + PromelaInlines promInls = getInlinePromela(execContent, true); + + if (promInls.acceptLabels > 0) + stream << padding << "acceptLabelT" << _transitions[nodeElem] << ":" << std::endl; + if (promInls.endLabels > 0) + stream << padding << "endLabelT" << _transitions[nodeElem] << ":" << std::endl; + if (promInls.progressLabels > 0) + stream << padding << "progressLabelT" << _transitions[nodeElem] << ":" << std::endl; + } stream << padding << "atomic {" << std::endl; - writeExecutableContent(stream, _states[ATTR(node, "target")], indent+1); +// writeExecutableContent(stream, _states[ATTR(nodeElem, "target")], indent+1); + for (int i = 0; i < execContent.size(); i++) { + writeExecutableContent(stream, execContent[i], indent+1); + } stream << padding << " skip;" << std::endl; - Node<std::string> newState = getUltimateTarget(node); + Node<std::string> newState = getUltimateTarget(nodeElem); for (int i = 0; i < _globalStates.size(); i++) { if (newState != _globalStates[i]) continue; - stream << padding << " s = s" << i << ";" << std::endl; + + std::string stateId = ATTR_CAST(_globalStates[i], "id"); + + stream << padding << " s = s" << i << ";"; + + int number = i; + int digits = 0; + do { + number /= 10; + digits++; + } while (number != 0); + + INDENT_MIN(stream, 10 + digits, MIN_COMMENT_PADDING); + + stream << " /* to state " << stateId << " */" << std::endl; + +// if (_analyzer.usesInPredicate()) { +// FlatStateIdentifier flatId(stateId); +// std::map<std::string, int> allOrigStates = _analyzer.getOrigStates(); +// for (std::map<std::string, int>::iterator allOrigIter = allOrigStates.begin(); allOrigIter != allOrigStates.end(); allOrigIter++) { +// stream << padding << " _x.states[" << _analyzer.macroForLiteral(allOrigIter->first) << "] = "; +// if (std::find(flatId.getActive().begin(), flatId.getActive().end(), allOrigIter->first) != flatId.getActive().end()) { +// stream << "true;" << std::endl; +// } else { +// stream << "false;" << std::endl; +// } +// } +// } + } stream << padding << "}" << std::endl; if (isFinal(Element<std::string>(newState))) { - stream << padding << "goto terminate;" << std::endl; + stream << padding << "goto terminate;"; + INDENT_MIN(stream, padding.length() + 14, MIN_COMMENT_PADDING); + stream << "/* final state */" << std::endl; + } else if (!HAS_ATTR_CAST(node, "event")) { + stream << padding << "goto nextTransition;"; + INDENT_MIN(stream, padding.length() + 19, MIN_COMMENT_PADDING); + stream << "/* spontaneous transition, check for more transitions */" << std::endl; } else { - stream << padding << "goto nextStep;" << std::endl; + stream << padding << "eventLess = true;" << std::endl; + stream << padding << "goto nextTransition;"; + INDENT_MIN(stream, padding.length() + 21, MIN_COMMENT_PADDING); + stream << "/* ordinary transition, check for spontaneous transitions */" << std::endl; } - } else if(TAGNAME(node) == "onentry" || TAGNAME(node) == "onexit") { + } else if(TAGNAME(nodeElem) == "onentry" || TAGNAME(nodeElem) == "onexit") { Arabica::DOM::Node<std::string> child = node.getFirstChild(); while(child) { - writeExecutableContent(stream, Arabica::DOM::Element<std::string>(child), indent); +// std::cerr << node << std::endl; + if (child.getNodeType() == Node_base::TEXT_NODE) { + if (boost::trim_copy(child.getNodeValue()).length() > 0) + stream << beautifyIndentation(_analyzer.replaceLiterals(child.getNodeValue()), indent) << std::endl; + } + if (child.getNodeType() == Node_base::ELEMENT_NODE) { + writeExecutableContent(stream, child, indent); + } child = child.getNextSibling(); } - } else if(TAGNAME(node) == "script") { + } else if(TAGNAME(nodeElem) == "script") { NodeSet<std::string> scriptText = filterChildType(Node_base::TEXT_NODE, node, true); for (int i = 0; i < scriptText.size(); i++) { - stream << beautifyIndentation(scriptText[i].getNodeValue(), indent) << std::endl; + stream << _analyzer.replaceLiterals(beautifyIndentation(scriptText[i].getNodeValue(), indent)) << std::endl; } - } else if(TAGNAME(node) == "log") { - // ignore + } else if(TAGNAME(nodeElem) == "log") { + std::string label = (HAS_ATTR(nodeElem, "label") ? ATTR(nodeElem, "label") : ""); + std::string expr = (HAS_ATTR(nodeElem, "expr") ? ATTR(nodeElem, "expr") : ""); + std::string trimmedExpr = boost::trim_copy(expr); + bool isStringLiteral = (boost::starts_with(trimmedExpr, "\"") || boost::starts_with(trimmedExpr, "'")); + + std::string formatString; + std::string varString; + std::string seperator; - } else if(TAGNAME(node) == "foreach") { - if (HAS_ATTR(node, "index")) - stream << padding << ATTR(node, "index") << " = 0;" << std::endl; - stream << padding << "for (" << ATTR(node, "item") << " in " << ATTR(node, "array") << ") {" << std::endl; + if (label.size() > 0) { + formatString += label + ": "; + } + + if (isStringLiteral) { + formatString += expr; + } else { + formatString += "%d"; + varString += seperator + expr; + } + + if (varString.length() > 0) { + stream << padding << "printf(\"" + formatString + "\", " + varString + ");" << std::endl; + } else { + stream << padding << "printf(\"" + formatString + "\");" << std::endl; + } + + } else if(TAGNAME(nodeElem) == "foreach") { + stream << padding << "for (" << (HAS_ATTR(nodeElem, "index") ? ATTR(nodeElem, "index") : "_index") << " in " << ATTR(nodeElem, "array") << ") {" << std::endl; + if (HAS_ATTR(nodeElem, "item")) { + stream << padding << " " << ATTR(nodeElem, "item") << " = " << ATTR(nodeElem, "array") << "[" << (HAS_ATTR(nodeElem, "index") ? ATTR(nodeElem, "index") : "_index") << "];" << std::endl; + } Arabica::DOM::Node<std::string> child = node.getFirstChild(); while(child) { - writeExecutableContent(stream, Arabica::DOM::Element<std::string>(child), indent + 1); + writeExecutableContent(stream, child, indent + 1); child = child.getNextSibling(); } - if (HAS_ATTR(node, "index")) - stream << padding << " " << ATTR(node, "index") << "++;" << std::endl; + if (HAS_ATTR(nodeElem, "index")) + stream << padding << " " << ATTR(nodeElem, "index") << "++;" << std::endl; stream << padding << "}" << std::endl; - } else if(TAGNAME(node) == "if") { + } else if(TAGNAME(nodeElem) == "if") { NodeSet<std::string> condChain; condChain.push_back(node); condChain.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "elseif", node)); @@ -360,22 +821,102 @@ void FSMToPromela::writeExecutableContent(std::ostream& stream, const Arabica::D writeIfBlock(stream, condChain, indent); - } else if(TAGNAME(node) == "raise") { - TrieNode* trieNode = _eventTrie.getNodeWithPrefix(ATTR(node, "event")); - stream << padding << "iQ!e" << trieNode->identifier << ";" << std::endl; - } else if(TAGNAME(node) == "send") { - if (!HAS_ATTR(node, "target")) { + } else if(TAGNAME(nodeElem) == "assign") { + if (HAS_ATTR(nodeElem, "location")) { + stream << padding << ATTR(nodeElem, "location") << " = "; + } + if (HAS_ATTR(nodeElem, "expr")) { + stream << _analyzer.replaceLiterals(ATTR(nodeElem, "expr")) << ";" << std::endl; + } else { + NodeSet<std::string> assignTexts = filterChildType(Node_base::TEXT_NODE, nodeElem, true); + if (assignTexts.size() > 0) { + stream << _analyzer.replaceLiterals(boost::trim_copy(assignTexts[0].getNodeValue())) << ";" << std::endl; + } + } + } else if(TAGNAME(nodeElem) == "send" || TAGNAME(nodeElem) == "raise") { + std::string targetQueue; + if (TAGNAME(nodeElem) == "raise") { + targetQueue = "iQ!"; + } else if (!HAS_ATTR(nodeElem, "target")) { + targetQueue = "tmpQ!"; + } else if (ATTR(nodeElem, "target").compare("#_internal") == 0) { + targetQueue = "iQ!"; + } + if (targetQueue.length() > 0) { // this is for our external queue - TrieNode* trieNode = _eventTrie.getNodeWithPrefix(ATTR(node, "event")); - stream << padding << "tmpQ!e" << trieNode->identifier << ";" << std::endl; + std::string event; + + if (HAS_ATTR(nodeElem, "event")) { + event = _analyzer.macroForLiteral(ATTR(nodeElem, "event")); + } else if (HAS_ATTR(nodeElem, "eventexpr")) { + event = ATTR(nodeElem, "eventexpr"); + } + if (_analyzer.usesComplexEventStruct()) { + stream << padding << "{" << std::endl; + stream << padding << " _event_t tmpEvent;" << std::endl; + stream << padding << " tmpEvent.name = " << event << ";" << std::endl; + + if (HAS_ATTR(nodeElem, "idlocation")) { + stream << padding << " /* idlocation */" << std::endl; + stream << padding << " _lastSendId = _lastSendId + 1;" << std::endl; + stream << padding << " " << ATTR(nodeElem, "idlocation") << " = _lastSendId;" << std::endl; + stream << padding << " tmpEvent.sendid = _lastSendId;" << std::endl; + stream << padding << " if" << std::endl; + stream << padding << " :: _lastSendId == 2147483647 -> _lastSendId = 0;" << std::endl; + stream << padding << " :: timeout -> skip;" << std::endl; + stream << padding << " fi;" << std::endl; + } else if (HAS_ATTR(nodeElem, "id")) { + stream << padding << " tmpEvent.sendid = " << _analyzer.macroForLiteral(ATTR(nodeElem, "id")) << ";" << std::endl; + } + + if (_analyzer.usesEventField("origintype") && targetQueue.compare("iQ!") != 0) { + stream << padding << " tmpEvent.origintype = " << _analyzer.macroForLiteral("http://www.w3.org/TR/scxml/#SCXMLEventProcessor") << ";" << std::endl; + } + + if (_analyzer.usesEventField("type")) { + std::string eventType = (targetQueue.compare("iQ!") == 0 ? _analyzer.macroForLiteral("internal") : _analyzer.macroForLiteral("external")); + stream << padding << " tmpEvent.type = " << eventType << ";" << std::endl; + } + + NodeSet<std::string> sendParams = filterChildElements(_nsInfo.xmlNSPrefix + "param", nodeElem); + NodeSet<std::string> sendContents = filterChildElements(_nsInfo.xmlNSPrefix + "content", nodeElem); + std::string sendNameList = ATTR(nodeElem, "namelist"); + if (sendParams.size() > 0) { + for (int i = 0; i < sendParams.size(); i++) { + Element<std::string> paramElem = Element<std::string>(sendParams[i]); + stream << padding << " tmpEvent.data." << ATTR(paramElem, "name") << " = " << ATTR(paramElem, "expr") << ";" << std::endl; + } + } + if (sendNameList.size() > 0) { + std::list<std::string> nameListIds = tokenizeIdRefs(sendNameList); + std::list<std::string>::iterator nameIter = nameListIds.begin(); + while(nameIter != nameListIds.end()) { + stream << padding << " tmpEvent.data." << *nameIter << " = " << *nameIter << ";" << std::endl; + nameIter++; + } + } + + if (sendParams.size() == 0 && sendNameList.size() == 0 && sendContents.size() > 0) { + Element<std::string> contentElem = Element<std::string>(sendContents[0]); + if (contentElem.hasChildNodes() && contentElem.getFirstChild().getNodeType() == Node_base::TEXT_NODE) { + stream << padding << " tmpEvent.data = " << spaceNormalize(contentElem.getFirstChild().getNodeValue()) << ";" << std::endl; + } else if (HAS_ATTR(contentElem, "expr")) { + stream << padding << " tmpEvent.data = " << _analyzer.replaceLiterals(ATTR(contentElem, "expr")) << ";" << std::endl; + } + } + stream << padding << " " << targetQueue << "tmpEvent;" << std::endl; + stream << padding << "}" << std::endl; + } else { + stream << padding << targetQueue << event << ";" << std::endl; + } } - } else if(TAGNAME(node) == "invoke") { - _invokers[ATTR(node, "invokeid")].writeStartEventSources(stream, indent); - } else if(TAGNAME(node) == "uninvoke") { - stream << padding << ATTR(node, "invokeid") << "EventSourceDone" << "= 1;" << std::endl; + } else if(TAGNAME(nodeElem) == "invoke") { + _invokers[ATTR(nodeElem, "invokeid")].writeStartEventSources(stream, indent); + } else if(TAGNAME(nodeElem) == "uninvoke") { + stream << padding << ATTR(nodeElem, "invokeid") << "EventSourceDone" << "= 1;" << std::endl; } else { - std::cerr << "'" << TAGNAME(node) << "'" << std::endl << node << std::endl; + std::cerr << "'" << TAGNAME(nodeElem) << "'" << std::endl << nodeElem << std::endl; assert(false); } @@ -492,31 +1033,34 @@ void FSMToPromela::writeIfBlock(std::ostream& stream, const Arabica::XPath::Node stream << padding << "if" << std::endl; // we need to nest the elseifs to resolve promela if semantics - stream << padding << ":: (" << ATTR(ifNode, "cond") << ") -> {" << std::endl; + stream << padding << ":: (" << _analyzer.replaceLiterals(ATTR(ifNode, "cond")) << ") -> {" << std::endl; - Arabica::DOM::Element<std::string> child; + Arabica::DOM::Node<std::string> child; if (TAGNAME(ifNode) == "if") { - child = Arabica::DOM::Element<std::string>(ifNode.getFirstChild()); + child = ifNode.getFirstChild(); } else { - child = Arabica::DOM::Element<std::string>(ifNode.getNextSibling()); + child = ifNode.getNextSibling(); } while(child) { if (child.getNodeType() == Node_base::ELEMENT_NODE) { - if (TAGNAME(child) == "elseif" || TAGNAME(child) == "else") + Arabica::DOM::Element<std::string> childElem = Arabica::DOM::Element<std::string>(child); + if (TAGNAME(childElem) == "elseif" || TAGNAME_CAST(childElem) == "else") break; + writeExecutableContent(stream, childElem, indent + 1); } - writeExecutableContent(stream, child, indent + 1); - child = Arabica::DOM::Element<std::string>(child.getNextSibling()); + child = child.getNextSibling(); } stream << padding << "}" << std::endl; stream << padding << ":: else -> "; if (nextIsElse) { - child = Arabica::DOM::Element<std::string>(condChain[1].getNextSibling()); + child = condChain[1].getNextSibling(); stream << "{" << std::endl; while(child) { - writeExecutableContent(stream, child, indent + 1); - child = Arabica::DOM::Element<std::string>(child.getNextSibling()); + if (child.getNodeType() == Node_base::ELEMENT_NODE) { + writeExecutableContent(stream, child, indent + 1); + } + child = child.getNextSibling(); } stream << padding << "}" << std::endl; @@ -569,30 +1113,115 @@ std::string FSMToPromela::beautifyIndentation(const std::string& code, int inden return beautifiedSS.str(); } +void FSMToPromela::writeStrings(std::ostream& stream) { + stream << "/* string literals */" << std::endl; + std::set<std::string> literals = _analyzer.getLiterals(); + std::map<std::string, int> events = _analyzer.getEvents(); + std::map<std::string, int> origStates = _analyzer.getOrigStates(); + + for (std::set<std::string>::const_iterator litIter = literals.begin(); litIter != literals.end(); litIter++) { + if (events.find(*litIter) == events.end() && (origStates.find(*litIter) == origStates.end() || !_analyzer.usesInPredicate())) + stream << "#define " << _analyzer.macroForLiteral(*litIter) << " " << _analyzer.indexForLiteral(*litIter) << " /* " << *litIter << " */" << std::endl; + } +} + void FSMToPromela::writeDeclarations(std::ostream& stream) { // get all data elements NodeSet<std::string> datas = _xpath.evaluate("//" + _nsInfo.xpathPrefix + "data", _scxml).asNodeSet(); - NodeSet<std::string> dataText = filterChildType(Node_base::TEXT_NODE, datas, true); +// NodeSet<std::string> dataText = filterChildType(Node_base::TEXT_NODE, datas, true); // write their text content - stream << "// datamodel variables" << std::endl; - for (int i = 0; i < dataText.size(); i++) { - Node<std::string> data = dataText[i]; - stream << beautifyIndentation(data.getNodeValue()) << std::endl; + stream << "/* datamodel variables */" << std::endl; + std::set<std::string> processedIdentifiers; + for (int i = 0; i < datas.size(); i++) { + + Node<std::string> data = datas[i]; + if (isInEmbeddedDocument(data)) + continue; + + std::string identifier = (HAS_ATTR_CAST(data, "id") ? ATTR_CAST(data, "id") : ""); + std::string expression = (HAS_ATTR_CAST(data, "expr") ? ATTR_CAST(data, "expr") : ""); + std::string type = boost::trim_copy(HAS_ATTR_CAST(data, "type") ? ATTR_CAST(data, "type") : ""); + + if (processedIdentifiers.find(identifier) != processedIdentifiers.end()) + continue; + processedIdentifiers.insert(identifier); + + if (boost::starts_with(type, "string")) { + type = "int" + type.substr(6, type.length() - 6); + } + std::string arrSize; + + NodeSet<std::string> dataText = filterChildType(Node_base::TEXT_NODE, data, true); + std::string value; + if (dataText.size() > 0) { + value = dataText[0].getNodeValue(); + boost::trim(value); + } + + if (identifier.length() > 0) { + + size_t bracketPos = type.find("["); + if (bracketPos != std::string::npos) { + arrSize = type.substr(bracketPos, type.length() - bracketPos); + type = type.substr(0, bracketPos); + } + std::string decl = type + " " + identifier + arrSize; + + if (arrSize.length() > 0) { + stream << decl << ";" << std::endl; + _varInitializers.push_back(value); + } else { + stream << decl; + if (expression.length() > 0) { + // id and expr given + stream << " = " << _analyzer.replaceLiterals(boost::trim_copy(expression)) << ";" << std::endl; + } else if (value.length() > 0) { + // id and text content given + stream << " = " << _analyzer.replaceLiterals(value) << ";" << std::endl; + } else { + // only id given + stream << ";" << std::endl; + } + } + } else if (value.length() > 0) { + // no id but text content given + stream << beautifyIndentation(value) << std::endl; + } } stream << std::endl; - stream << "// global variables" << std::endl; - stream << "int e; /* current event */" << std::endl; - stream << "int s; /* current state */" << std::endl; - stream << "chan iQ = [100] of {int} /* internal queue */" << std::endl; - stream << "chan eQ = [100] of {int} /* external queue */" << std::endl; - stream << "chan tmpQ = [100] of {int} /* temporary queue for external events in transitions */" << std::endl; - stream << "int tmpQItem;" << std::endl; + stream << "/* global variables */" << std::endl; + + if (_analyzer.usesComplexEventStruct()) { + // event is defined with the typedefs + stream << "unsigned s : " << BIT_WIDTH(_globalStates.size() + 1) << "; /* current state */" << std::endl; + stream << "chan iQ = [10] of {_event_t} /* internal queue */" << std::endl; + stream << "chan eQ = [10] of {_event_t} /* external queue */" << std::endl; + stream << "chan tmpQ = [10] of {_event_t} /* temporary queue for external events in transitions */" << std::endl; + stream << "_event_t tmpQItem;" << std::endl; + } else { + stream << "unsigned _event : " << BIT_WIDTH(_analyzer.getEvents().size() + 1) << "; /* current event */" << std::endl; + stream << "unsigned s : " << BIT_WIDTH(_globalStates.size() + 1) << "; /* current state */" << std::endl; + stream << "chan iQ = [10] of {int} /* internal queue */" << std::endl; + stream << "chan eQ = [10] of {int} /* external queue */" << std::endl; + stream << "chan tmpQ = [10] of {int} /* temporary queue for external events in transitions */" << std::endl; + stream << "unsigned tmpQItem : " << BIT_WIDTH(_analyzer.getEvents().size() + 1) << ";" << std::endl; + } + stream << "bool eventLess = true; /* whether to process event-less only n this step */" << std::endl; + stream << "hidden int _index; /* helper for indexless foreach loops */" << std::endl; + + if (_analyzer.usesEventField("sendid")) { + stream << "hidden int _lastSendId = 0; /* sequential counter for send ids */"; + } + +// if (_analyzer.usesPlatformVars()) { +// stream << "_x_t _x;" << std::endl; +// } stream << std::endl; - stream << "// event sources" << std::endl; + stream << "/* event sources */" << std::endl; if (_globalEventSource) { _globalEventSource.writeDeclarations(stream); @@ -618,10 +1247,8 @@ void FSMToPromela::writeEventSources(std::ostream& stream) { invIter->second.writeEventSource(stream); invIter++; } - } - void FSMToPromela::writeFSM(std::ostream& stream) { NodeSet<std::string> transitions; @@ -629,37 +1256,38 @@ void FSMToPromela::writeFSM(std::ostream& stream) { // write initial transition transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", _startState); assert(transitions.size() == 1); - stream << " // transition's executable content" << std::endl; - writeExecutableContent(stream, Arabica::DOM::Element<std::string>(transitions[0]), 1); + stream << " /* transition's executable content */" << std::endl; + writeExecutableContent(stream, transitions[0], 1); for (int i = 0; i < _globalStates.size(); i++) { if (_globalStates[i] == _startState) continue; NodeSet<std::string> transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", _globalStates[i]); for (int j = 0; j < transitions.size(); j++) { - writeExecutableContent(stream, Arabica::DOM::Element<std::string>(transitions[j]), 1); + writeExecutableContent(stream, transitions[j], 1); } } stream << std::endl; stream << "nextStep:" << std::endl; - stream << " // push send events to external queue" << std::endl; + stream << " /* push send events to external queue */" << std::endl; stream << " if" << std::endl; - stream << " :: len(tmpQ) != 0 -> { tmpQ?e; eQ!e }" << std::endl; + stream << " :: len(tmpQ) != 0 -> { tmpQ?_event; eQ!_event }" << std::endl; stream << " :: else -> skip;" << std::endl; stream << " fi;" << std::endl << std::endl; stream << " /* pop an event */" << std::endl; stream << " if" << std::endl; - stream << " :: len(iQ) != 0 -> iQ ? e /* from internal queue */" << std::endl; - stream << " :: else -> eQ ? e /* from external queue */" << std::endl; - stream << " fi;" << std::endl; + stream << " :: len(iQ) != 0 -> iQ ? _event /* from internal queue */" << std::endl; + stream << " :: else -> eQ ? _event /* from external queue */" << std::endl; + stream << " fi;" << std::endl << std::endl; stream << " /* event dispatching per state */" << std::endl; + stream << "nextTransition:" << std::endl; stream << " if" << std::endl; writeEventDispatching(stream); - stream << " :: else -> goto nextStep;" << std::endl; + stream << " :: else -> assert(false); /* this is an error as we dispatched all valid states */" << std::endl; stream << " fi;" << std::endl; stream << "terminate: skip;" << std::endl; @@ -681,50 +1309,105 @@ void FSMToPromela::writeEventDispatching(std::ostream& stream) { if (_globalStates[i] == _startState) continue; - stream << " :: (s == s" << i << ") -> {" << std::endl; + int number = i; + int digits = 0; + do { + number /= 10; + digits++; + } while (number != 0); + stream << " :: (s == s" << i << ") -> {"; + + INDENT_MIN(stream, 18 + digits, MIN_COMMENT_PADDING); + + stream << " /* from state " << ATTR_CAST(_globalStates[i], "id") << " */" << std::endl; NodeSet<std::string> transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", _globalStates[i]); writeDispatchingBlock(stream, transitions, 2); - stream << " goto nextStep;" << std::endl; +// stream << " goto nextStep;"; stream << " }" << std::endl; } } void FSMToPromela::writeDispatchingBlock(std::ostream& stream, const Arabica::XPath::NodeSet<std::string>& transChain, int indent) { - if (transChain.size() == 0) - return; - std::string padding; for (int i = 0; i < indent; i++) { padding += " "; } - stream << padding << "if" << std::endl; - stream << padding << ":: ((0"; + if (transChain.size() == 0) { + stream << padding << "eventLess = false;" << std::endl; + stream << padding << "goto nextStep;"; + INDENT_MIN(stream, padding.size() + 13, MIN_COMMENT_PADDING); + stream << "/* no transition applicable */" << std::endl; + return; + } + Element<std::string> currTrans = Element<std::string>(transChain[0]); - std::string eventDesc = ATTR(currTrans, "event"); - if (boost::ends_with(eventDesc, "*")) - eventDesc = eventDesc.substr(0, eventDesc.size() - 1); - if (boost::ends_with(eventDesc, ".")) - eventDesc = eventDesc.substr(0, eventDesc.size() - 1); - - if (eventDesc.size() == 0) { - stream << " || 1"; + std::stringstream tmpSS; + + tmpSS << padding << "if" << std::endl; + size_t lineStart = tmpSS.tellp(); + + if (HAS_ATTR(currTrans, "cond")) { + tmpSS << padding << ":: (("; } else { - std::list<TrieNode*> trieNodes = _eventTrie.getWordsWithPrefix(eventDesc); + tmpSS << padding << ":: ("; + } - std::list<TrieNode*>::iterator trieIter = trieNodes.begin(); - while(trieIter != trieNodes.end()) { - stream << " || e == e" << (*trieIter)->identifier; - trieIter++; + if (!HAS_ATTR(currTrans, "event")) { + tmpSS << "eventLess"; + } else { + std::string eventDescs = ATTR(currTrans, "event"); + + std::list<std::string> eventNames = tokenizeIdRefs(eventDescs); + std::set<std::string> eventPrefixes; + std::list<std::string>::iterator eventNameIter = eventNames.begin(); + while(eventNameIter != eventNames.end()) { + std::string eventDesc = *eventNameIter; + if (boost::ends_with(eventDesc, "*")) + eventDesc = eventDesc.substr(0, eventDesc.size() - 1); + if (boost::ends_with(eventDesc, ".")) + eventDesc = eventDesc.substr(0, eventDesc.size() - 1); + if (eventDesc.length() > 0) { + std::set<std::string> tmp = _analyzer.getEventsWithPrefix(*eventNameIter); + eventPrefixes.insert(tmp.begin(), tmp.end()); + } + eventNameIter++; } + + if (eventPrefixes.size() > 0) { + tmpSS << "!eventLess && "; + } else { + tmpSS << "!eventLess"; + } + + std::string seperator; + std::set<std::string>::iterator eventIter = eventPrefixes.begin(); + while(eventIter != eventPrefixes.end()) { + if (_analyzer.usesComplexEventStruct()) { + tmpSS << seperator << "_event.name == " << _analyzer.macroForLiteral(*eventIter); + } else { + tmpSS << seperator << "_event == " << _analyzer.macroForLiteral(*eventIter); + } + seperator = " || "; + eventIter++; + } + } + + tmpSS << ")"; + if (HAS_ATTR(currTrans, "cond")) { + tmpSS << (HAS_ATTR(currTrans, "cond") ? " && " + _analyzer.replaceLiterals(ATTR(currTrans, "cond")) + ")": ""); } + tmpSS << " -> goto t" << _transitions[currTrans] << ";"; + size_t lineEnd = tmpSS.tellp(); + size_t lineLength = lineEnd - lineStart; - stream << ") && "; - stream << (HAS_ATTR(currTrans, "cond") ? ATTR(currTrans, "cond") : "1"); - stream << ") -> goto t" << _transitions[currTrans] << ";" << std::endl; - ; + for (int i = lineLength; i < MIN_COMMENT_PADDING; i++) + tmpSS << " "; + + tmpSS << " /* transition to " << ATTR_CAST(getUltimateTarget(currTrans), "id") << " */" << std::endl; + stream << tmpSS.str(); stream << padding << ":: else {" << std::endl; @@ -734,7 +1417,6 @@ void FSMToPromela::writeDispatchingBlock(std::ostream& stream, const Arabica::XP } writeDispatchingBlock(stream, cdrTransChain, indent + 1); - stream << padding << " goto nextStep;" << std::endl; stream << padding << "}" << std::endl; stream << padding << "fi;" << std::endl; } @@ -743,6 +1425,14 @@ void FSMToPromela::writeDispatchingBlock(std::ostream& stream, const Arabica::XP void FSMToPromela::writeMain(std::ostream& stream) { stream << std::endl; stream << "init {" << std::endl; + if (_varInitializers.size() > 0) { + std::list<std::string>::iterator initIter = _varInitializers.begin(); + while(initIter != _varInitializers.end()) { + stream << beautifyIndentation(*initIter); + initIter++; + } + stream << std::endl; + } if (_globalEventSource) _globalEventSource.writeStartEventSources(stream, 1); stream << " run step();" << std::endl; @@ -750,11 +1440,15 @@ void FSMToPromela::writeMain(std::ostream& stream) { } + void FSMToPromela::initNodes() { // get all states NodeSet<std::string> states = filterChildElements(_nsInfo.xmlNSPrefix + "state", _scxml); for (int i = 0; i < states.size(); i++) { + if (InterpreterImpl::isInEmbeddedDocument(states[i])) + continue; _states[ATTR_CAST(states[i], "id")] = Element<std::string>(states[i]); + _analyzer.addState(ATTR_CAST(states[i], "id")); if (HAS_ATTR_CAST(states[i], "transient") && DOMUtils::attributeIsTrue(ATTR_CAST(states[i], "transient"))) continue; _globalStates.push_back(states[i]); @@ -778,11 +1472,33 @@ void FSMToPromela::initNodes() { eventName = eventName.substr(0, eventName.size() - 1); if (boost::ends_with(eventName, ".")) eventName = eventName.substr(0, eventName.size() - 1); - _eventTrie.addWord(eventName); + if (eventName.size() > 0) + _analyzer.addEvent(eventName); } } } + // do we need sendid / invokeid? + { + NodeSet<std::string> invokes = filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true); + NodeSet<std::string> sends = filterChildElements(_nsInfo.xmlNSPrefix + "send", _scxml, true); + + for (int i = 0; i < invokes.size(); i++) { + if (HAS_ATTR_CAST(invokes[i], "idlocation")) { + } + } + + for (int i = 0; i < sends.size(); i++) { + if (HAS_ATTR_CAST(sends[i], "idlocation")) { + _analyzer.addCode("_event.sendid"); + } + if (HAS_ATTR_CAST(sends[i], "id")) { + _analyzer.addLiteral(ATTR_CAST(sends[i], "id")); + _analyzer.addCode("_event.sendid"); + } + } + + } // external event names from comments NodeSet<std::string> promelaEventSourceComments; NodeSet<std::string> invokers = _xpath.evaluate("//" + _nsInfo.xpathPrefix + "invoke", _scxml).asNodeSet(); @@ -795,7 +1511,7 @@ void FSMToPromela::initNodes() { if (TAGNAME_CAST(promelaEventSourceComments[i].getParentNode()) == "scxml") { promES.type = PromelaEventSource::PROMELA_EVENT_SOURCE_GLOBAL; - promES.trie = &_eventTrie; + promES.analyzer = &_analyzer; promES.name = "global"; _globalEventSource = promES; } else if (TAGNAME_CAST(promelaEventSourceComments[i].getParentNode()) == "invoke") { @@ -805,7 +1521,7 @@ void FSMToPromela::initNodes() { } std::string invokeId = ATTR_CAST(promelaEventSourceComments[i].getParentNode(), "invokeid"); promES.type = PromelaEventSource::PROMELA_EVENT_SOURCE_INVOKER; - promES.trie = &_eventTrie; + promES.analyzer = &_analyzer; promES.name = invokeId; _invokers[invokeId] = promES; } @@ -817,6 +1533,101 @@ void FSMToPromela::initNodes() { for (int i = 0; i < transitions.size(); i++) { _transitions[Element<std::string>(transitions[i])] = index++; } + + // add platform variables as string literals + _analyzer.addLiteral("_sessionid"); + _analyzer.addLiteral("_name"); + + if (HAS_ATTR(_scxml, "name")) { + _analyzer.addLiteral(ATTR(_scxml, "name"), _analyzer.indexForLiteral("_sessionid")); + } + + NodeSet<std::string> contents = filterChildElements(_nsInfo.xmlNSPrefix + "content", _scxml, true); + for (int i = 0; i < contents.size(); i++) { + Element<std::string> contentElem = Element<std::string>(contents[i]); + if (contentElem.hasChildNodes() && contentElem.getFirstChild().getNodeType() == Node_base::TEXT_NODE) { + _analyzer.addLiteral(spaceNormalize(contentElem.getFirstChild().getNodeValue())); + } + } + + + // extract and analyze source code + std::set<std::string> allCode; + std::set<std::string> allStrings; + { + NodeSet<std::string> withCond; + withCond.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "transition", _scxml, true)); + withCond.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "if", _scxml, true)); + withCond.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "elseif", _scxml, true)); + for (int i = 0; i < withCond.size(); i++) { + Element<std::string> elem = Element<std::string>(withCond[i]); + if (HAS_ATTR(elem, "cond")) { + std::string code = ATTR(elem, "cond"); + code = sanitizeCode(code); + elem.setAttribute("cond", code); + allCode.insert(code); + } + } + } + { + NodeSet<std::string> withExpr; + withExpr.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "log", _scxml, true)); + withExpr.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "data", _scxml, true)); + withExpr.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "assign", _scxml, true)); + withExpr.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "content", _scxml, true)); + withExpr.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "param", _scxml, true)); + for (int i = 0; i < withExpr.size(); i++) { + Element<std::string> elem = Element<std::string>(withExpr[i]); + if (HAS_ATTR(elem, "expr")) { + std::string code = ATTR(elem, "expr"); + code = sanitizeCode(code); + elem.setAttribute("expr", code); + allCode.insert(code); + } + } + } + { + NodeSet<std::string> withLocation; + withLocation.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "assign", _scxml, true)); + for (int i = 0; i < withLocation.size(); i++) { + Element<std::string> elem = Element<std::string>(withLocation[i]); + if (HAS_ATTR(elem, "location")) { + std::string code = ATTR(elem, "location"); + code = sanitizeCode(code); + elem.setAttribute("location", code); + allCode.insert(code); + } + } + } + { + NodeSet<std::string> withText; + withText.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "script", _scxml, true)); + withText.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "data", _scxml, true)); + for (int i = 0; i < withText.size(); i++) { + NodeSet<std::string> texts = filterChildType(Node_base::TEXT_NODE, withText[i], true); + for (int j = 0; j < texts.size(); j++) { + if (texts[j].getNodeValue().size() > 0) { + Text<std::string> elem = Text<std::string>(texts[j]); + std::string code = elem.getNodeValue(); + code = sanitizeCode(code); + elem.setNodeValue(code); + allCode.insert(code); + } + } + } + } + for (std::set<std::string>::const_iterator codeIter = allCode.begin(); codeIter != allCode.end(); codeIter++) { + _analyzer.addCode(*codeIter); + } + +} + +std::string FSMToPromela::sanitizeCode(const std::string& code) { + std::string replaced = code; + boost::replace_all(replaced, "\"", "'"); + boost::replace_all(replaced, "_sessionid", "_SESSIONID"); + boost::replace_all(replaced, "_name", "_NAME"); + return replaced; } void PromelaInline::dump() { @@ -849,12 +1660,22 @@ void FSMToPromela::writeProgram(std::ostream& stream) { return; } +// std::cerr << _scxml << std::endl; + initNodes(); writeEvents(stream); stream << std::endl; writeStates(stream); stream << std::endl; + if (_analyzer.usesInPredicate()) { + writeStateMap(stream); + stream << std::endl; + } + writeTypeDefs(stream); + stream << std::endl; + writeStrings(stream); + stream << std::endl; writeDeclarations(stream); stream << std::endl; writeEventSources(stream); @@ -864,6 +1685,28 @@ void FSMToPromela::writeProgram(std::ostream& stream) { writeMain(stream); stream << std::endl; + // write ltl expression for success + std::stringstream acceptingStates; + std::string seperator; + for (int i = 0; i < _globalStates.size(); i++) { + FlatStateIdentifier flatId(ATTR_CAST(_globalStates[i], "id")); + if (std::find(flatId.getActive().begin(), flatId.getActive().end(), "pass") != flatId.getActive().end()) { + acceptingStates << seperator << "s == s" << i; + seperator = " || "; + } + } + if (acceptingStates.str().size() > 0) { + stream << "ltl { eventually (" << acceptingStates.str() << ") }" << std::endl; + } + +// if (_states.find("active:{pass}") != _states.end()) { +// for (int i = 0; i < _globalStates.size(); i++) { +// if (_states["active:{pass}"] != _globalStates[i]) +// continue; +// stream << "ltl { eventually (s == s" << i << ") }"; +// break; +// } +// } } }
\ No newline at end of file diff --git a/src/uscxml/transform/FSMToPromela.h b/src/uscxml/transform/FSMToPromela.h index 62381cd..3a9e263 100644 --- a/src/uscxml/transform/FSMToPromela.h +++ b/src/uscxml/transform/FSMToPromela.h @@ -84,6 +84,108 @@ public: int codes; }; +class USCXML_API PromelaCodeAnalyzer { +public: + class PromelaTypedef { + public: + PromelaTypedef() : arraySize(0) {} + std::string name; + std::string type; + size_t arraySize; + std::map<std::string, PromelaTypedef> types; + + bool operator==(const PromelaTypedef& other) const { + return name == other.name; + } + + }; + + PromelaCodeAnalyzer() : _eventTrie("."), _lastStrIndex(1), _lastStateIndex(0), _lastEventIndex(1), _usesInPredicate(false), _usesPlatformVars(false) { + } + + void addCode(const std::string& code); + void addEvent(const std::string& eventName); + void addState(const std::string& stateName); + void addLiteral(const std::string& stateName, int forceIndex = -1); + + bool usesComplexEventStruct() { + return _typeDefs.types.find("_event") != _typeDefs.types.end(); + } + bool usesEventField(const std::string& fieldName) { + if (usesComplexEventStruct() && _typeDefs.types["_event"].types.find(fieldName) != _typeDefs.types["_event"].types.end()) + return true; + return false; + } + + bool usesInPredicate() { + return _usesInPredicate; + } + bool usesPlatformVars() { + return _usesPlatformVars; + } + + std::string macroForLiteral(const std::string& literal); + int indexForLiteral(const std::string& literal); + int arrayIndexForOrigState(const std::string& stateName); + + std::set<std::string> getLiterals() { + return _strLiterals; + } + std::set<std::string> getEventsWithPrefix(const std::string& prefix); + std::map<std::string, int>& getEvents() { + return _events; + } + + std::map<std::string, int>& getStates() { + return _states; + } + + std::map<std::string, int>& getOrigStates() { + return _origStateIndex; + } + + std::list<std::string>& getOrigStates(const std::string& state) { + if (_origStateMap.find(state) == _origStateMap.end()) + throw std::runtime_error("No original states known for " + state); + return _origStateMap[state]; + } + + Trie& getTrie() { + return _eventTrie; + } + + std::string replaceLiterals(const std::string code); + + PromelaTypedef getTypes() { + return _typeDefs; + } + +protected: + std::string createMacroName(const std::string& literal); + int enumerateLiteral(const std::string& literal, int forceIndex = -1); + + std::set<std::string> _strLiterals; // all string literals + std::map<std::string, std::string> _strMacroNames; // macronames for string literals + std::map<std::string, int> _strIndex; // integer enumeration for string + std::map<std::string, int> _origStateIndex; // state enumeration for original states + + std::map<std::string, int> _states; + std::map<std::string, std::list<std::string> > _origStateMap; // states from the original state chart + std::map<std::string, int> _events; + + PromelaTypedef _typeDefs; + + Trie _eventTrie; + +private: + std::set<std::string> _macroNameSet; // helper set for uniqueness of macros + int _lastStrIndex; + int _lastStateIndex; + int _lastEventIndex; + bool _usesInPredicate; + bool _usesPlatformVars; +}; + class USCXML_API PromelaEventSource { public: @@ -109,7 +211,7 @@ public: PromelaInlines eventSources; Arabica::DOM::Node<std::string> container; PromelaEventSourceType type; - Trie* trie; + PromelaCodeAnalyzer* analyzer; }; class USCXML_API FSMToPromela : public InterpreterDraft6 { @@ -127,9 +229,12 @@ protected: void writeEvents(std::ostream& stream); void writeStates(std::ostream& stream); + void writeStateMap(std::ostream& stream); + void writeTypeDefs(std::ostream& stream); + void writeStrings(std::ostream& stream); void writeDeclarations(std::ostream& stream); void writeEventSources(std::ostream& stream); - void writeExecutableContent(std::ostream& stream, const Arabica::DOM::Element<std::string>& node, int indent = 0); + void writeExecutableContent(std::ostream& stream, const Arabica::DOM::Node<std::string>& node, int indent = 0); void writeInlineComment(std::ostream& stream, const Arabica::DOM::Node<std::string>& node); void writeFSM(std::ostream& stream); void writeEventDispatching(std::ostream& stream); @@ -138,19 +243,26 @@ protected: void writeIfBlock(std::ostream& stream, const Arabica::XPath::NodeSet<std::string>& condChain, int indent = 0); void writeDispatchingBlock(std::ostream& stream, const Arabica::XPath::NodeSet<std::string>& transChain, int indent = 0); - Arabica::XPath::NodeSet<std::string> getTransientContent(const Arabica::DOM::Element<std::string>& state); + Arabica::XPath::NodeSet<std::string> getTransientContent(const Arabica::DOM::Element<std::string>& state, const std::string& source = ""); Arabica::DOM::Node<std::string> getUltimateTarget(const Arabica::DOM::Element<std::string>& transition); static PromelaInlines getInlinePromela(const std::string&); static PromelaInlines getInlinePromela(const Arabica::XPath::NodeSet<std::string>& elements, bool recurse = false); static PromelaInlines getInlinePromela(const Arabica::DOM::Node<std::string>& elements); - Trie _eventTrie; +// std::string replaceStringsInExpression(const std::string& expr); + + std::string sanitizeCode(const std::string& code); + Arabica::XPath::NodeSet<std::string> _globalStates; Arabica::DOM::Node<std::string> _startState; std::map<std::string, Arabica::DOM::Element<std::string> > _states; std::map<Arabica::DOM::Element<std::string>, int> _transitions; + std::list<std::string> _varInitializers; + + PromelaCodeAnalyzer _analyzer; + std::map<std::string, PromelaEventSource> _invokers; PromelaEventSource _globalEventSource; }; diff --git a/src/uscxml/transform/FlatStateIdentifier.h b/src/uscxml/transform/FlatStateIdentifier.h index 0957e34..5cbd5f2 100644 --- a/src/uscxml/transform/FlatStateIdentifier.h +++ b/src/uscxml/transform/FlatStateIdentifier.h @@ -37,9 +37,14 @@ namespace uscxml { class USCXML_API FlatStateIdentifier { public: + + operator bool() const { + return stateId.length() > 0; + } + FlatStateIdentifier(const Arabica::XPath::NodeSet<std::string>& activeStates, - const Arabica::XPath::NodeSet<std::string>& alreadyEnteredStates, - const std::map<std::string, Arabica::XPath::NodeSet<std::string> >& historyStates) { + const Arabica::XPath::NodeSet<std::string>& alreadyEnteredStates, + const std::map<std::string, Arabica::XPath::NodeSet<std::string> >& historyStates) { for (int i = 0; i < activeStates.size(); i++) { active.push_back(ATTR_CAST(activeStates[i], "id")); } @@ -65,17 +70,24 @@ public: histories[histIter->first].push_back(ATTR_CAST(histIter->second[i], "id")); } } - + initStateId(); } - - + + FlatStateIdentifier(const std::list<std::string>& active, - const std::list<std::string>& visited, - const std::map<std::string, std::list<std::string> >& histories) : active(active), visited(visited), histories(histories) { + const std::list<std::string>& visited, + const std::map<std::string, std::list<std::string> >& histories) : active(active), visited(visited), histories(histories) { initStateId(); } - + + static std::string toStateId(const std::list<std::string> active, + const std::list<std::string> visited = std::list<std::string>(), + const std::map<std::string, std::list<std::string> > histories = std::map<std::string, std::list<std::string> >()) { + FlatStateIdentifier tmp(active, visited, histories); + return tmp.getStateId(); + } + FlatStateIdentifier(const std::string& identifier) : stateId(identifier) { std::string parsedName; // parse unique state identifier @@ -87,6 +99,10 @@ public: std::stringstream stateSS(section.substr(8, section.size() - 9)); std::string state; while(std::getline(stateSS, state, ',')) { + size_t closingBracketPos = state.find("}"); + if (closingBracketPos != std::string::npos) { + state = state.substr(0, closingBracketPos); + } if (state.length() > 0) { active.push_back(state); } @@ -96,6 +112,10 @@ public: std::stringstream stateSS(section.substr(9, section.size() - 10)); std::string state; while(std::getline(stateSS, state, ',')) { + size_t closingBracketPos = state.find("}"); + if (closingBracketPos != std::string::npos) { + state = state.substr(0, closingBracketPos); + } if (state.length() > 0) { visited.push_back(state); } @@ -107,31 +127,36 @@ public: std::string state; size_t start = 0; size_t history = 0; - + while((history = histEntries.find(":", start)) != std::string::npos) { std::string histName = histEntries.substr(start, history - start); history++; - + size_t end = histEntries.find("}", start); if (end == std::string::npos) continue; - + std::stringstream stateSS(histEntries.substr(history + 1, end - history - 1)); std::string state; while(std::getline(stateSS, state, ',')) { + size_t closingBracketPos = state.find("}"); + if (closingBracketPos != std::string::npos) { + state = state.substr(0, closingBracketPos); + } histories[histName].push_back(state); } - + start = end + 2; } } } + initStateId(); } const std::string& getStateId() { return stateId; } - + const std::list<std::string>& getActive() { return active; } @@ -157,17 +182,17 @@ protected: std::list<std::string> active; std::list<std::string> visited; std::map<std::string, std::list<std::string> > histories; - + std::string flatActive; std::string flatVisited; std::string flatHistories; - + std::string stateId; void initStateId() { std::stringstream stateIdSS; std::string seperator; - + std::stringstream flatActiveSS; flatActiveSS << "active:{"; for (std::list<std::string>::const_iterator actIter = active.begin(); actIter != active.end(); actIter++) { @@ -177,7 +202,7 @@ protected: flatActiveSS << "}"; flatActive = flatActiveSS.str(); stateIdSS << flatActive; - + if (visited.size() > 0) { std::stringstream flatVisitedSS; seperator = ""; @@ -190,7 +215,7 @@ protected: flatVisited = flatVisitedSS.str(); stateIdSS << ";" << flatVisited; } - + if (histories.size() > 0) { std::stringstream flatHistorySS; seperator = ""; @@ -209,10 +234,10 @@ protected: flatHistories = flatHistorySS.str(); stateIdSS << ";" << flatHistories; } - + stateId = stateIdSS.str(); } - + #if 0 std::string activeId() { std::stringstream activeSS; @@ -224,7 +249,7 @@ protected: } #endif - + }; } |