diff options
author | Stefan Radomski <radomski@tk.informatik.tu-darmstadt.de> | 2014-10-21 07:59:53 (GMT) |
---|---|---|
committer | Stefan Radomski <radomski@tk.informatik.tu-darmstadt.de> | 2014-10-21 07:59:53 (GMT) |
commit | ef4eb9b94078f11a566865741a76f056ae5804c3 (patch) | |
tree | da90ee5abca165f3aec869ebfb27ac6eba81b310 /src | |
parent | 59c9ae81b4911c6458cbe8a5ed78554bdcc82861 (diff) | |
download | uscxml-ef4eb9b94078f11a566865741a76f056ae5804c3.zip uscxml-ef4eb9b94078f11a566865741a76f056ae5804c3.tar.gz uscxml-ef4eb9b94078f11a566865741a76f056ae5804c3.tar.bz2 |
Optimized Promela generation
Diffstat (limited to 'src')
-rw-r--r-- | src/uscxml/transform/ChartToFSM.cpp | 237 | ||||
-rw-r--r-- | src/uscxml/transform/ChartToFSM.h | 20 | ||||
-rw-r--r-- | src/uscxml/transform/ChartToPromela.cpp | 23 | ||||
-rw-r--r-- | src/uscxml/transform/ChartToPromela.h | 5 |
4 files changed, 237 insertions, 48 deletions
diff --git a/src/uscxml/transform/ChartToFSM.cpp b/src/uscxml/transform/ChartToFSM.cpp index 8eda0a5..32d74a4 100644 --- a/src/uscxml/transform/ChartToFSM.cpp +++ b/src/uscxml/transform/ChartToFSM.cpp @@ -33,6 +33,9 @@ #undef max #include <limits> +#define UNDECIDABLE 2147483647 +#define MIN(X,Y) ((X) < (Y) ? (X) : (Y)) + #define DUMP_STATS(nrTrans) \ uint64_t now = tthread::chrono::system_clock::now(); \ if (now - _lastTimeStamp > 1000) { \ @@ -44,6 +47,8 @@ if (now - _lastTimeStamp > 1000) { \ std::cerr << "S: " << _globalConf.size() << " [" << _perfStatesProcessed << "/sec]" << std::endl; \ std::cerr << "C: " << _perfStatesCachedTotal << " [" << _perfStatesCachedProcessed << "/sec]" << std::endl; \ std::cerr << "X: " << _perfStatesSkippedTotal << " [" << _perfStatesSkippedProcessed << "/sec]" << std::endl; \ + std::cerr << _perfTransTotal << ", " << _perfTransProcessed << ", " << _globalConf.size() << ", " << _perfStatesProcessed << ", "; \ + std::cerr <<_perfStatesCachedTotal << ", " << _perfStatesCachedProcessed << ", " << _perfStatesSkippedTotal << ", " << _perfStatesSkippedProcessed << std::endl; \ std::cerr << std::endl; \ _perfTransProcessed = 0; \ _perfStatesProcessed = 0; \ @@ -159,6 +164,10 @@ ChartToFSM::ChartToFSM(const Interpreter& other) { _lastStateIndex = 0; _lastTransIndex = 0; + _maxEventSentChain = 0; + _maxEventRaisedChain = 0; + _doneEventRaiseTolerance = 0; + // create a _flatDoc for the FSM DOMImplementation<std::string> domFactory = Arabica::SimpleDOM::DOMImplementation<std::string>::getDOMImplementation(); _flatDoc = domFactory.createDocument(other.getDocument().getNamespaceURI(), "", 0); @@ -187,9 +196,6 @@ ChartToFSM::~ChartToFSM() { } Document<std::string> ChartToFSM::getDocument() const { -// std::cerr << "######################" << std::endl; -// std::cerr << _flatDoc << std::endl; -// std::cerr << "######################" << std::endl; return _flatDoc; } @@ -265,8 +271,11 @@ InterpreterState ChartToFSM::interpret() { _scxml.appendChild(initialElem); initialTransitions.push_back(transitionElem); } - labelTransitions(); -// weightTransitions(); + + annotateRaiseAndSend(_scxml); + +// std::cout << _scxml << std::endl; + indexTransitions(_scxml); // reverse indices for most prior to be in front @@ -294,6 +303,12 @@ InterpreterState ChartToFSM::interpret() { indexedStates.resize(allStates.size()); for (int i = 0; i < allStates.size(); i++) { Element<std::string> state = Element<std::string>(allStates[i]); + + // while we are iterating, determine deepest nested level + size_t nrAncs = getProperAncestors(state, _scxml).size(); + if (_doneEventRaiseTolerance < nrAncs) + _doneEventRaiseTolerance = nrAncs; + state.setAttribute("index", toStr(i)); indexedStates[i] = state; } @@ -322,19 +337,9 @@ InterpreterState ChartToFSM::interpret() { std::cerr << _globalConf.size() << std::endl; #endif - - NodeSet<std::string> elements = InterpreterImpl::filterChildType(Node_base::ELEMENT_NODE, _scxml, true); - uint64_t nrStates = 0; - for (int i = 0; i < elements.size(); i++) { - Element<std::string> elem = Element<std::string>(elements[i]); - if (isState(elem) && !HAS_ATTR(elem, "transient")) - nrStates++; - if (elem.getLocalName() == "transition" && elem.hasAttribute("id")) { - elem.removeAttribute("id"); - } - } - - std::cerr << "Actual Complexity: " << nrStates << std::endl; + std::cerr << "Actual Complexity: " << _globalConf.size() << std::endl; + std::cerr << "Internal Queue: " << _maxEventRaisedChain << std::endl; + std::cerr << "External Queue: " << _maxEventSentChain << std::endl; return _state; } @@ -356,6 +361,19 @@ void ChartToFSM::executeContent(const Arabica::DOM::Element<std::string>& conten } else { // e.g. global script elements return; } + assert(content.hasAttribute("raise") && content.hasAttribute("send")); + + std::string raiseAttr = content.getAttribute("raise"); + std::string sendAttr = content.getAttribute("send"); + + _currGlobalTransition->eventsRaised = (raiseAttr == "-1" ? UNDECIDABLE : _currGlobalTransition->eventsRaised + strTo<uint32_t>(raiseAttr)); + _currGlobalTransition->eventsSent = (sendAttr == "-1" ? UNDECIDABLE : _currGlobalTransition->eventsSent + strTo<uint32_t>(sendAttr)); + + if (_currGlobalTransition->eventsRaised > _maxEventRaisedChain) + _maxEventRaisedChain = _currGlobalTransition->eventsRaised; + if (_currGlobalTransition->eventsSent > _maxEventSentChain) + _maxEventSentChain = _currGlobalTransition->eventsSent; + _currGlobalTransition->actions.push_back(action); _currGlobalTransition->hasExecutableContent = true; } @@ -375,8 +393,9 @@ void ChartToFSM::cancelInvoke(const Arabica::DOM::Element<std::string>& element) } void ChartToFSM::internalDoneSend(const Arabica::DOM::Element<std::string>& state) { + if (!isState(state)) + return; - Arabica::DOM::Element<std::string> stateElem = (Arabica::DOM::Element<std::string>)state; if (parentIsScxmlState(state)) return; @@ -391,7 +410,7 @@ void ChartToFSM::internalDoneSend(const Arabica::DOM::Element<std::string>& stat onentry.appendChild(raise); - Arabica::XPath::NodeSet<std::string> doneDatas = filterChildElements(_nsInfo.xmlNSPrefix + "donedata", stateElem); + Arabica::XPath::NodeSet<std::string> doneDatas = filterChildElements(_nsInfo.xmlNSPrefix + "donedata", state); if (doneDatas.size() > 0) { Arabica::DOM::Node<std::string> doneData = doneDatas[0]; Arabica::XPath::NodeSet<std::string> contents = filterChildElements(_nsInfo.xmlNSPrefix + "content", doneDatas[0]); @@ -406,12 +425,13 @@ void ChartToFSM::internalDoneSend(const Arabica::DOM::Element<std::string>& stat } } - raise.setAttribute("event", "done.state." + ATTR_CAST(stateElem.getParentNode(), "id")); // parent?! + raise.setAttribute("event", "done.state." + ATTR_CAST(state.getParentNode(), "id")); // parent?! GlobalTransition::Action action; action.onEntry = onentry; _currGlobalTransition->actions.push_back(action); + _currGlobalTransition->eventsRaised++; _currGlobalTransition->hasExecutableContent = true; } @@ -481,11 +501,65 @@ static bool filterChildEnabled(const NodeSet<std::string>& transitions) { return true; } +bool ChartToFSM::hasForeachInBetween(const Arabica::DOM::Node<std::string>& ancestor, const Arabica::DOM::Node<std::string>& child) { + if (!ancestor || !child) + return false; + + Node<std::string> currChild = child; + while(currChild != ancestor) { + if (!currChild.getParentNode()) + return false; + if (TAGNAME_CAST(currChild) == "foreach") + return true; + currChild = currChild.getParentNode(); + } + return false; +} + +void ChartToFSM::annotateRaiseAndSend(const Arabica::DOM::Element<std::string>& root) { + NodeSet<std::string> execContent; + execContent.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "transition", _scxml, true)); + execContent.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "onentry", _scxml, true)); + execContent.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "onexit", _scxml, true)); + for (int i = 0; i < execContent.size(); i++) { + Element<std::string> execContentElem(execContent[i]); + + int nrRaise = 0; + NodeSet<std::string> raise = filterChildElements(_nsInfo.xmlNSPrefix + "raise", execContent[i], true); + for (int j = 0; j < raise.size(); j++) { + if (hasForeachInBetween(execContent[i], raise[j])) { + execContentElem.setAttribute("raise", "-1"); + goto DONE_COUNT_RAISE; + } else { + nrRaise++; + } + } + execContentElem.setAttribute("raise", toStr(nrRaise)); + + DONE_COUNT_RAISE: + + int nrSend = 0; + NodeSet<std::string> sends = filterChildElements(_nsInfo.xmlNSPrefix + "send", execContent[i], true); + for (int j = 0; j < sends.size(); j++) { + if (hasForeachInBetween(execContent[i], sends[j])) { + execContentElem.setAttribute("send", "-1"); + goto DONE_COUNT_SEND; + } else { + nrSend++; + } + } + execContentElem.setAttribute("send", toStr(nrSend)); + + DONE_COUNT_SEND: + ; + } +} void ChartToFSM::indexTransitions(const Arabica::DOM::Element<std::string>& root) { // breadth first traversal of transitions Arabica::XPath::NodeSet<std::string> levelTransitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", root); for (int i = levelTransitions.size() - 1; i >= 0; i--) { + // push into index starting with least prior indexedTransitions.push_back(Element<std::string>(levelTransitions[i])); } @@ -495,7 +569,6 @@ void ChartToFSM::indexTransitions(const Arabica::DOM::Element<std::string>& root if (isState(stateElem)) indexTransitions(stateElem); } - } bool GlobalTransition::operator< (const GlobalTransition& other) const { @@ -681,8 +754,8 @@ void ChartToFSM::getPotentialTransitionsForConf(const Arabica::XPath::NodeSet<st void ChartToFSM::explode() { - std::list<GlobalState*> statesRemaining; - statesRemaining.push_back(new GlobalState(_configuration, _alreadyEntered, _historyValue, _nsInfo.xmlNSPrefix, this)); + std::list<std::pair<GlobalTransition*, GlobalState*> > statesRemaining; + statesRemaining.push_back(std::make_pair(_currGlobalTransition, new GlobalState(_configuration, _alreadyEntered, _historyValue, _nsInfo.xmlNSPrefix, this))); // add all invokers for initial transition for (unsigned int i = 0; i < _statesToInvoke.size(); i++) { @@ -701,13 +774,18 @@ void ChartToFSM::explode() { while(statesRemaining.size() > 0) { DUMP_STATS(0); - GlobalState* globalState = statesRemaining.front(); + GlobalState* globalState = statesRemaining.front().second; + _currGlobalTransition = statesRemaining.front().first; statesRemaining.pop_front(); - // used to be conditionalized, we will just assum + // used to be conditionalized, we will just assume assert(_currGlobalTransition); if (_globalConf.find(globalState->stateId) != _globalConf.end()) { + if (_currGlobalTransition->isEventless) { + // we arrived via a spontaneaous transition, do we need to update? + updateRaisedAndSendChains(_globalConf[globalState->stateId], _currGlobalTransition, std::set<GlobalTransition*>()); + } delete globalState; _perfStatesSkippedTotal++; _perfStatesSkippedProcessed++; @@ -759,16 +837,32 @@ void ChartToFSM::explode() { _transPerActiveConf[globalState->activeId] = globalState; } - // append resulting new states - for(std::list<GlobalTransition*>::iterator transListIter = globalState->sortedOutgoing.begin(); - transListIter != globalState->sortedOutgoing.end(); - transListIter++) { + // take every transition set and append resulting new state + for(std::list<GlobalTransition*>::iterator transIter = globalState->sortedOutgoing.begin(); + transIter != globalState->sortedOutgoing.end(); + transIter++) { - (*transListIter)->source = globalState->stateId; - _currGlobalTransition = *transListIter; + GlobalTransition* incomingTrans = _currGlobalTransition; + GlobalTransition* outgoingTrans = *transIter; + + outgoingTrans->source = globalState->stateId; + _currGlobalTransition = outgoingTrans; + + microstep(refsToTransitions(outgoingTrans->transitionRefs)); + + // if outgoing transition is spontaneous, add number of events to chain + if (outgoingTrans->isEventless) { + outgoingTrans->eventsChainRaised = MIN(incomingTrans->eventsChainRaised + outgoingTrans->eventsRaised, UNDECIDABLE); + outgoingTrans->eventsChainSent = MIN(incomingTrans->eventsChainSent + outgoingTrans->eventsSent, UNDECIDABLE); + + if (outgoingTrans->eventsChainRaised > _maxEventRaisedChain) + _maxEventRaisedChain = outgoingTrans->eventsChainRaised; + if (outgoingTrans->eventsChainSent > _maxEventSentChain) + _maxEventSentChain = outgoingTrans->eventsChainSent; + + } - microstep(refsToTransitions((*transListIter)->transitionRefs)); - statesRemaining.push_back(new GlobalState(_configuration, _alreadyEntered, _historyValue, _nsInfo.xmlNSPrefix, this)); + statesRemaining.push_back(std::make_pair(outgoingTrans, new GlobalState(_configuration, _alreadyEntered, _historyValue, _nsInfo.xmlNSPrefix, this))); // add all invokers for (unsigned int i = 0; i < _statesToInvoke.size(); i++) { @@ -780,7 +874,7 @@ void ChartToFSM::explode() { _statesToInvoke = NodeSet<std::string>(); // remember that the last transition lead here - (*transListIter)->destination = statesRemaining.back()->stateId; + outgoingTrans->destination = statesRemaining.back().second->stateId; // reset state for next transition set _configuration = globalState->getActiveStates(); @@ -791,6 +885,69 @@ void ChartToFSM::explode() { } +void ChartToFSM::updateRaisedAndSendChains(GlobalState* state, GlobalTransition* source, std::set<GlobalTransition*> visited) { + for (std::list<GlobalTransition*>::iterator transIter = state->sortedOutgoing.begin(); transIter != state->sortedOutgoing.end(); transIter++) { + GlobalTransition* transition = *transIter; + + if (!transition->isEventless) + continue; // we do not care for eventful transitions + + // source leads to spontaneous transition -> update event chains + bool eventChainsNeedUpdated = false; + + if (visited.find(transition) != visited.end()) { + // potential spontaneous transition cycle! + if (transition->eventsChainRaised > 0) + _maxEventRaisedChain = UNDECIDABLE; + if (transition->eventsChainSent > 0) + _maxEventSentChain = UNDECIDABLE; + return; + } + + // UNDECIDABLE means "undecidable / endless" + + // will source increase our event chain? + if (transition->eventsChainRaised != UNDECIDABLE && + transition->eventsChainRaised < source->eventsChainRaised + transition->eventsRaised) { + // taking transition after source causes more events in chain + transition->eventsChainRaised = MIN(source->eventsChainRaised + transition->eventsRaised, UNDECIDABLE); + eventChainsNeedUpdated = true; + } + if (transition->eventsChainSent != UNDECIDABLE && + transition->eventsChainSent < source->eventsChainSent + transition->eventsSent) { + // taking transition after source causes more events in chain + transition->eventsChainSent = MIN(source->eventsChainSent + transition->eventsSent, UNDECIDABLE); + eventChainsNeedUpdated = true; + } + + if (eventChainsNeedUpdated && + transition->destination.length() > 0 && + _globalConf.find(transition->destination) != _globalConf.end()) { + + visited.insert(transition); + // iterate all spontaneous transitions in destination and update event chains + updateRaisedAndSendChains(_globalConf[transition->destination], transition, visited); + } + + if (transition->eventsChainRaised > _maxEventRaisedChain) + _maxEventRaisedChain = transition->eventsChainRaised; + if (transition->eventsChainSent > _maxEventSentChain) + _maxEventSentChain = transition->eventsChainSent; + } +} + +uint32_t ChartToFSM::getMinInternalQueueLength(uint32_t defaultVal) { + if (_maxEventRaisedChain != UNDECIDABLE) + return _maxEventRaisedChain + _doneEventRaiseTolerance; + return defaultVal; +} + +uint32_t ChartToFSM::getMinExternalQueueLength(uint32_t defaultVal) { + if (_maxEventSentChain != UNDECIDABLE) + return _maxEventSentChain; + return defaultVal; +} + Arabica::XPath::NodeSet<std::string> ChartToFSM::refsToStates(const std::set<int>& stateRefs) { NodeSet<std::string> states; for (std::set<int>::const_iterator stateIter = stateRefs.begin(); stateIter != stateRefs.end(); stateIter++) { @@ -807,7 +964,7 @@ Arabica::XPath::NodeSet<std::string> ChartToFSM::refsToTransitions(const std::se return transitions; } - +#if 0 void ChartToFSM::labelTransitions() { // put a unique id on each transition Arabica::XPath::NodeSet<std::string> states = getAllStates(); @@ -825,7 +982,8 @@ void ChartToFSM::labelTransitions() { } } } - +#endif + void ChartToFSM::beforeMicroStep(Interpreter interpreter) { } void ChartToFSM::onStableConfiguration(Interpreter interpreter) { @@ -885,6 +1043,11 @@ GlobalState::GlobalState(const Arabica::XPath::NodeSet<std::string>& activeState GlobalTransition::GlobalTransition(const Arabica::XPath::NodeSet<std::string>& transitionSet, DataModel dataModel, ChartToFSM* flattener) { interpreter = flattener; + eventsRaised = 0; + eventsSent = 0; + eventsChainRaised = 0; + eventsChainSent = 0; + for (int i = 0; i < transitionSet.size(); i++) { transitionRefs.insert(strTo<int>(ATTR_CAST(transitionSet[i], "index"))); } diff --git a/src/uscxml/transform/ChartToFSM.h b/src/uscxml/transform/ChartToFSM.h index 9e583b1..6698889 100644 --- a/src/uscxml/transform/ChartToFSM.h +++ b/src/uscxml/transform/ChartToFSM.h @@ -109,6 +109,13 @@ public: bool isSubset; // there is a superset to this set bool hasExecutableContent; + uint32_t eventsRaised; // internal events this transition will raise + uint32_t eventsSent; // external events this transition will send + uint32_t eventsChainRaised; // maximum number of internal events raised when taking this transition in a chain + uint32_t eventsChainSent; // maximum number of external events raised when taking this transition in a chain + + std::set<int> startTransitionRefs; // indices of eventful transitions that might trigger this transition + std::set<int> transitionRefs; // indizes of constituting transitions Arabica::XPath::NodeSet<std::string> getTransitions() const; @@ -170,9 +177,16 @@ protected: void explode(); void getPotentialTransitionsForConf(const Arabica::XPath::NodeSet<std::string>& conf, std::map<std::string, GlobalTransition*>& outMap); - void labelTransitions(); +// void labelTransitions(); void indexTransitions(const Arabica::DOM::Element<std::string>& root); + void annotateRaiseAndSend(const Arabica::DOM::Element<std::string>& root); + bool hasForeachInBetween(const Arabica::DOM::Node<std::string>& ancestor, const Arabica::DOM::Node<std::string>& child); + void updateRaisedAndSendChains(GlobalState* state, GlobalTransition* source, std::set<GlobalTransition*> visited); + + uint32_t getMinInternalQueueLength(uint32_t defaultVal); + uint32_t getMinExternalQueueLength(uint32_t defaultVal); + std::list<GlobalTransition*> sortTransitions(std::list<GlobalTransition*> list); // we need this static as we use it in a sort function @@ -193,6 +207,10 @@ protected: size_t _lastStateIndex; size_t _lastTransIndex; + size_t _maxEventSentChain; + size_t _maxEventRaisedChain; + size_t _doneEventRaiseTolerance; + GlobalState* _start; GlobalTransition* _currGlobalTransition; Arabica::DOM::Document<std::string> _flatDoc; diff --git a/src/uscxml/transform/ChartToPromela.cpp b/src/uscxml/transform/ChartToPromela.cpp index 1ae6c8d..b9b1637 100644 --- a/src/uscxml/transform/ChartToPromela.cpp +++ b/src/uscxml/transform/ChartToPromela.cpp @@ -33,6 +33,7 @@ #define MSG_QUEUE_LENGTH 5 #define MAX_MACRO_CHARS 64 #define MIN_COMMENT_PADDING 60 +#define MAX(X,Y) ((X) > (Y) ? (X) : (Y)) #define BIT_WIDTH(number) (number > 1 ? (int)ceil(log((double)number) / log((double)2.0)) : 1) #define LENGTH_FOR_NUMBER(input, output) \ @@ -230,7 +231,6 @@ void PromelaCodeAnalyzer::addCode(const std::string& code) { break; } case PML_ASGN: -// node->dump(); if (node->operands.back()->type == PML_CONST) { hasValue = true; if (isInteger(node->operands.back()->value.c_str(), 10)) { @@ -239,6 +239,8 @@ void PromelaCodeAnalyzer::addCode(const std::string& code) { } if (node->operands.front()->type == PML_CMPND) node = node->operands.front(); + if (node->operands.front()->type != PML_NAME) + break; // this will skip array assignments case PML_CMPND: { std::string nameOfType; std::list<PromelaParserNode*>::iterator opIter = node->operands.begin(); @@ -1506,21 +1508,21 @@ void ChartToPromela::writeStrings(std::ostream& stream) { void ChartToPromela::writeDeclarations(std::ostream& stream) { stream << "/* global variables */" << std::endl; - + if (_analyzer.usesComplexEventStruct()) { // event is defined with the typedefs stream << "_event_t _event; /* current state */" << std::endl; stream << "unsigned s : " << BIT_WIDTH(_globalConf.size() + 1) << "; /* current state */" << std::endl; - stream << "chan iQ = [" << MSG_QUEUE_LENGTH << "] of {_event_t} /* internal queue */" << std::endl; - stream << "chan eQ = [" << MSG_QUEUE_LENGTH << "] of {_event_t} /* external queue */" << std::endl; - stream << "chan tmpQ = [" << MSG_QUEUE_LENGTH << "] of {_event_t} /* temporary queue for external events in transitions */" << std::endl; + stream << "chan iQ = [" << MAX(_internalQueueLength, 1) << "] of {_event_t} /* internal queue */" << std::endl; + stream << "chan eQ = [" << _externalQueueLength + 1 << "] of {_event_t} /* external queue */" << std::endl; + stream << "chan tmpQ = [" << MAX(_externalQueueLength, 1) << "] of {_event_t} /* temporary queue for external events in transitions */" << std::endl; stream << "hidden _event_t tmpQItem;" << std::endl; } else { stream << "unsigned _event : " << BIT_WIDTH(_analyzer.getEvents().size() + 1) << "; /* current event */" << std::endl; stream << "unsigned s : " << BIT_WIDTH(_globalConf.size() + 1) << "; /* current state */" << std::endl; - stream << "chan iQ = [" << MSG_QUEUE_LENGTH << "] of {int} /* internal queue */" << std::endl; - stream << "chan eQ = [" << MSG_QUEUE_LENGTH << "] of {int} /* external queue */" << std::endl; - stream << "chan tmpQ = [" << MSG_QUEUE_LENGTH << "] of {int} /* temporary queue for external events in transitions */" << std::endl; + stream << "chan iQ = [" << MAX(_internalQueueLength, 1) << "] of {int} /* internal queue */" << std::endl; + stream << "chan eQ = [" << _externalQueueLength + 1 << "] of {int} /* external queue */" << std::endl; + stream << "chan tmpQ = [" << MAX(_externalQueueLength, 1) << "] of {int} /* temporary queue for external events in transitions */" << std::endl; stream << "hidden 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; @@ -1873,7 +1875,10 @@ void ChartToPromela::writeMain(std::ostream& stream) { void ChartToPromela::initNodes() { - + + _internalQueueLength = getMinInternalQueueLength(MSG_QUEUE_LENGTH); + _externalQueueLength = getMinExternalQueueLength(MSG_QUEUE_LENGTH); + // get all states NodeSet<std::string> states = getAllStates(); for (int i = 0; i < states.size(); i++) { diff --git a/src/uscxml/transform/ChartToPromela.h b/src/uscxml/transform/ChartToPromela.h index 75e3339..a8ebe75 100644 --- a/src/uscxml/transform/ChartToPromela.h +++ b/src/uscxml/transform/ChartToPromela.h @@ -252,7 +252,7 @@ protected: 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); - + static std::string declForRange(const std::string& identifier, long minValue, long maxValue, bool nativeOnly = false); // std::string replaceStringsInExpression(const std::string& expr); @@ -268,6 +268,9 @@ protected: PromelaCodeAnalyzer _analyzer; + uint32_t _externalQueueLength; + uint32_t _internalQueueLength; + std::map<std::string, PromelaEventSource> _invokers; PromelaEventSource _globalEventSource; |