From ef4eb9b94078f11a566865741a76f056ae5804c3 Mon Sep 17 00:00:00 2001 From: Stefan Radomski Date: Tue, 21 Oct 2014 09:59:53 +0200 Subject: Optimized Promela generation --- src/uscxml/transform/ChartToFSM.cpp | 237 +++++++++++++++++++++++++++----- src/uscxml/transform/ChartToFSM.h | 20 ++- src/uscxml/transform/ChartToPromela.cpp | 23 ++-- src/uscxml/transform/ChartToPromela.h | 5 +- test/w3c/analyze_promela_tests.pl | 167 ---------------------- test/w3c/analyze_tests.pl | 182 ++++++++++++++++++++++++ test/w3c/graphs/data/pml_states.data | 84 ----------- test/w3c/graphs/promela-states.sh | 10 -- test/w3c/graphs/run_gnuplot.sh | 2 - 9 files changed, 419 insertions(+), 311 deletions(-) delete mode 100755 test/w3c/analyze_promela_tests.pl create mode 100755 test/w3c/analyze_tests.pl delete mode 100644 test/w3c/graphs/data/pml_states.data delete mode 100755 test/w3c/graphs/promela-states.sh delete mode 100755 test/w3c/graphs/run_gnuplot.sh 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 +#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 domFactory = Arabica::SimpleDOM::DOMImplementation::getDOMImplementation(); _flatDoc = domFactory.createDocument(other.getDocument().getNamespaceURI(), "", 0); @@ -187,9 +196,6 @@ ChartToFSM::~ChartToFSM() { } Document 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 state = Element(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 elements = InterpreterImpl::filterChildType(Node_base::ELEMENT_NODE, _scxml, true); - uint64_t nrStates = 0; - for (int i = 0; i < elements.size(); i++) { - Element elem = Element(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& 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(raiseAttr)); + _currGlobalTransition->eventsSent = (sendAttr == "-1" ? UNDECIDABLE : _currGlobalTransition->eventsSent + strTo(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& element) } void ChartToFSM::internalDoneSend(const Arabica::DOM::Element& state) { + if (!isState(state)) + return; - Arabica::DOM::Element stateElem = (Arabica::DOM::Element)state; if (parentIsScxmlState(state)) return; @@ -391,7 +410,7 @@ void ChartToFSM::internalDoneSend(const Arabica::DOM::Element& stat onentry.appendChild(raise); - Arabica::XPath::NodeSet doneDatas = filterChildElements(_nsInfo.xmlNSPrefix + "donedata", stateElem); + Arabica::XPath::NodeSet doneDatas = filterChildElements(_nsInfo.xmlNSPrefix + "donedata", state); if (doneDatas.size() > 0) { Arabica::DOM::Node doneData = doneDatas[0]; Arabica::XPath::NodeSet contents = filterChildElements(_nsInfo.xmlNSPrefix + "content", doneDatas[0]); @@ -406,12 +425,13 @@ void ChartToFSM::internalDoneSend(const Arabica::DOM::Element& 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& transitions) { return true; } +bool ChartToFSM::hasForeachInBetween(const Arabica::DOM::Node& ancestor, const Arabica::DOM::Node& child) { + if (!ancestor || !child) + return false; + + Node 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& root) { + NodeSet 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 execContentElem(execContent[i]); + + int nrRaise = 0; + NodeSet 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 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& root) { // breadth first traversal of transitions Arabica::XPath::NodeSet 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(levelTransitions[i])); } @@ -495,7 +569,6 @@ void ChartToFSM::indexTransitions(const Arabica::DOM::Element& root if (isState(stateElem)) indexTransitions(stateElem); } - } bool GlobalTransition::operator< (const GlobalTransition& other) const { @@ -681,8 +754,8 @@ void ChartToFSM::getPotentialTransitionsForConf(const Arabica::XPath::NodeSet statesRemaining; - statesRemaining.push_back(new GlobalState(_configuration, _alreadyEntered, _historyValue, _nsInfo.xmlNSPrefix, this)); + std::list > 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()); + } delete globalState; _perfStatesSkippedTotal++; _perfStatesSkippedProcessed++; @@ -759,16 +837,32 @@ void ChartToFSM::explode() { _transPerActiveConf[globalState->activeId] = globalState; } - // append resulting new states - for(std::list::iterator transListIter = globalState->sortedOutgoing.begin(); - transListIter != globalState->sortedOutgoing.end(); - transListIter++) { + // take every transition set and append resulting new state + for(std::list::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(); // 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 visited) { + for (std::list::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 ChartToFSM::refsToStates(const std::set& stateRefs) { NodeSet states; for (std::set::const_iterator stateIter = stateRefs.begin(); stateIter != stateRefs.end(); stateIter++) { @@ -807,7 +964,7 @@ Arabica::XPath::NodeSet ChartToFSM::refsToTransitions(const std::se return transitions; } - +#if 0 void ChartToFSM::labelTransitions() { // put a unique id on each transition Arabica::XPath::NodeSet 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& activeState GlobalTransition::GlobalTransition(const Arabica::XPath::NodeSet& 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(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 startTransitionRefs; // indices of eventful transitions that might trigger this transition + std::set transitionRefs; // indizes of constituting transitions Arabica::XPath::NodeSet getTransitions() const; @@ -170,9 +177,16 @@ protected: void explode(); void getPotentialTransitionsForConf(const Arabica::XPath::NodeSet& conf, std::map& outMap); - void labelTransitions(); +// void labelTransitions(); void indexTransitions(const Arabica::DOM::Element& root); + void annotateRaiseAndSend(const Arabica::DOM::Element& root); + bool hasForeachInBetween(const Arabica::DOM::Node& ancestor, const Arabica::DOM::Node& child); + void updateRaisedAndSendChains(GlobalState* state, GlobalTransition* source, std::set visited); + + uint32_t getMinInternalQueueLength(uint32_t defaultVal); + uint32_t getMinExternalQueueLength(uint32_t defaultVal); + std::list sortTransitions(std::list 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 _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::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 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& elements, bool recurse = false); static PromelaInlines getInlinePromela(const Arabica::DOM::Node& 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 _invokers; PromelaEventSource _globalEventSource; diff --git a/test/w3c/analyze_promela_tests.pl b/test/w3c/analyze_promela_tests.pl deleted file mode 100755 index 5e1b96b..0000000 --- a/test/w3c/analyze_promela_tests.pl +++ /dev/null @@ -1,167 +0,0 @@ -#!/usr/bin/perl -w - -use strict; -use File::Spec; -use File::Basename; -use Data::Dumper; - -my $toBaseDir = File::Spec->canonpath(dirname($0)); -my $outDir = File::Spec->catfile($toBaseDir, 'graphs'); -my $testResultFile; - -my @dataQuery; - -# iterate given arguments and populate $dataQuery -foreach my $argnum (0 .. $#ARGV) { - if ($argnum == $#ARGV) { - if (-f $ARGV[$argnum]) { - $testResultFile = $ARGV[$argnum]; - last; - } - if (-f File::Spec->catfile($toBaseDir, $ARGV[$argnum])) { - $testResultFile = File::Spec->catfile($toBaseDir, $ARGV[$argnum]); - last; - } - } - push(@dataQuery, \[split('\.', $ARGV[$argnum])]); -} - -if (!$testResultFile) { - $testResultFile = File::Spec->catfile($toBaseDir, "../../build/cli/Testing/Temporary/LastTest.log"); -} - -open(FILE, $testResultFile) or die $!; -mkdir($outDir) or die($!) if (! -d $outDir); - -my $test; -my $block; -my $currTest; -my $testIndex = 0; - -$/ = '-' x 58 . "\n"; - -while ($block = ) { - chomp($block); - - # Test Preambel ======== - if ($block =~ - / - \n? - (\d+)\/(\d+)\sTesting:\s(.*)\n - (\d+)\/(\d+)\sTest:\s(.*)\n - /x ) { - $currTest = $3; - $test->{$currTest}->{'name'} = $currTest; - $test->{$currTest}->{'number'} = $1; - $test->{$currTest}->{'total'} = $2; - $test->{$currTest}->{'index'} = $testIndex++; - - if ($currTest =~ /test(\d+\w?)\.scxml$/) { - $test->{$currTest}->{'w3c'} = $1; - } - - next; - } - - # Test Epilog ======== - if ($block =~ - / - Test\s(\S+)\sReason:\n - /x ) { - $test->{$currTest}->{'status'} = lc($1); - next; - } - - # Promela Test ======== - if ($block =~ - / - Approximate\sComplexity:\s(\d+)\n - Actual\sComplexity:\s(\d+)\n - /x ) { - $test->{$currTest}->{'flat'}->{'apprComplexity'} = $1; - $test->{$currTest}->{'flat'}->{'actualComplexity'} = $2; - - if ($block =~ /State-vector (\d+) byte, depth reached (\d+), errors: (\d+)/) { - $test->{$currTest}->{'pml'}->{'states'}->{'stateSize'} = $1; - $test->{$currTest}->{'pml'}->{'states'}->{'depth'} = $2; - $test->{$currTest}->{'pml'}->{'states'}->{'errors'} = $3; - } - if ($block =~ - / - \s+(\d+)\sstates,\sstored\s\((\d+)\svisited\)\n - \s+(\d+)\sstates,\smatched\n - \s+(\d+)\stransitions\s\(=\svisited\+matched\)\n - \s+(\d+)\satomic\ssteps\n - hash\sconflicts:\s+(\d+)\s\(resolved\) - /x ) { - $test->{$currTest}->{'pml'}->{'states'}->{'stateStored'} = $1; - $test->{$currTest}->{'pml'}->{'states'}->{'stateVisited'} = $2; - $test->{$currTest}->{'pml'}->{'states'}->{'stateMatched'} = $3; - $test->{$currTest}->{'pml'}->{'states'}->{'transitions'} = $4; - $test->{$currTest}->{'pml'}->{'states'}->{'atomicSteps'} = $5; - $test->{$currTest}->{'pml'}->{'hashConflicts'} = $6; - } - - if ($block =~ - / - \s+([\d\.]+)\sequivalent\smemory\susage\sfor\sstates.* - \s+([\d\.]+)\sactual\smemory\susage\sfor\sstates\n - \s+([\d\.]+)\smemory\sused\sfor\shash\stable\s\(-w(\d+)\)\n - \s+([\d\.]+)\smemory\sused\sfor\sDFS\sstack\s\(-m(\d+)\) - \s+([\d\.]+)\stotal\sactual\smemory\susage - /x ) { - $test->{$currTest}->{'pml'}->{'memory'}->{'states'} = $1; - $test->{$currTest}->{'pml'}->{'memory'}->{'actual'} = $2; - $test->{$currTest}->{'pml'}->{'memory'}->{'hashTable'} = $3; - $test->{$currTest}->{'pml'}->{'memory'}->{'hashLimit'} = $4; - $test->{$currTest}->{'pml'}->{'memory'}->{'dfsStack'} = $5; - $test->{$currTest}->{'pml'}->{'memory'}->{'dfsLimit'} = $6; - $test->{$currTest}->{'pml'}->{'memory'}->{'total'} = $7; - } - - next; - } - -} -close(FILE); - -if (@dataQuery > 0) { - while (my ($name, $data) = each $test) { - my $seperator = ""; - foreach (@dataQuery) { - my $currVal = $data; - my @query = @${$_}; - foreach (@query) { - my $dataKey = $_; - if (defined($currVal->{$dataKey})) { - $currVal = $currVal->{$dataKey}; - } else { - die("no key $dataKey in structure:\n" . Dumper($currVal)); - } - } - print $seperator . $currVal; - $seperator = ", "; - } - print "\n"; - } -} else { - while (my ($name, $data) = each $test) { - # get one $data into scope - print "Available Queries:\n"; - - sub dumpQueries() { - my $structure = shift; - my $path = shift || ""; - while (my ($name, $data) = each $structure) { - if (ref(\$data) eq "SCALAR") { - print "\t" . $path . $name . "\n"; - } else { - &dumpQueries($data, $path . $name . "."); - } - } - } - &dumpQueries($data); - exit; - } -} - diff --git a/test/w3c/analyze_tests.pl b/test/w3c/analyze_tests.pl new file mode 100755 index 0000000..edc53da --- /dev/null +++ b/test/w3c/analyze_tests.pl @@ -0,0 +1,182 @@ +#!/usr/bin/perl -w + +use strict; +use File::Spec; +use File::Basename; +use Data::Dumper; + +my $toBaseDir = File::Spec->canonpath(dirname($0)); +my $outDir = File::Spec->catfile($toBaseDir, 'graphs'); +my $testResultFile; + +my @dataQuery; + +# iterate given arguments and populate $dataQuery +foreach my $argnum (0 .. $#ARGV) { + if ($argnum == $#ARGV) { + if (-f $ARGV[$argnum]) { + $testResultFile = $ARGV[$argnum]; + last; + } + if (-f File::Spec->catfile($toBaseDir, $ARGV[$argnum])) { + $testResultFile = File::Spec->catfile($toBaseDir, $ARGV[$argnum]); + last; + } + } + push(@dataQuery, \[split('\.', $ARGV[$argnum])]); +} + +if (!$testResultFile) { + $testResultFile = File::Spec->catfile($toBaseDir, "../../build/cli/Testing/Temporary/LastTest.log"); +} + +open(FILE, $testResultFile) or die $!; +mkdir($outDir) or die($!) if (! -d $outDir); + +my $test; +my $block; +my $currTest; +my $testIndex = 0; + +$/ = '-' x 58 . "\n"; + +while ($block = ) { + chomp($block); + + # Test Preambel ======== + if ($block =~ + / + \n? + (\d+)\/(\d+)\sTesting:\s(.*)\n + (\d+)\/(\d+)\sTest:\s(.*)\n + /x ) { + $currTest = $3; + $test->{$currTest}->{'name'} = $currTest; + $test->{$currTest}->{'number'} = $1; + $test->{$currTest}->{'total'} = $2; + $test->{$currTest}->{'index'} = $testIndex++; + + if ($currTest =~ /test(\d+\w?)\.scxml$/) { + $test->{$currTest}->{'w3c'} = $1; + } + + next; + } + + # Test Epilog ======== + if ($block =~ + / + Test\s(\S+)\sReason:\n + /x ) { + $test->{$currTest}->{'status'} = lc($1); + next; + } + + # Test Duration ======== + if ($block =~ + / + \\n + Test\stime\s\=\s+([\d\.]+)\s(\w+) + /x ) { + $test->{$currTest}->{'duration'} = $1; + $test->{$currTest}->{'durationUnit'} = $2; + # next; - no next as this is part of the actual test output we need to scan below + } + + # Promela Test ======== + if ($block =~ + / + Approximate\sComplexity:\s(\d+)\n + Actual\sComplexity:\s(\d+)\n + Internal\sQueue:\s(\d+)\n + External\sQueue:\s(\d+)\n + /x ) { + $test->{$currTest}->{'flat'}->{'apprComplexity'} = $1; + $test->{$currTest}->{'flat'}->{'actualComplexity'} = $2; + $test->{$currTest}->{'flat'}->{'internalQueue'} = $3; + $test->{$currTest}->{'flat'}->{'externalQueue'} = $4; + + if ($block =~ /State-vector (\d+) byte, depth reached (\d+), errors: (\d+)/) { + $test->{$currTest}->{'pml'}->{'states'}->{'stateSize'} = $1; + $test->{$currTest}->{'pml'}->{'states'}->{'depth'} = $2; + $test->{$currTest}->{'pml'}->{'states'}->{'errors'} = $3; + } + if ($block =~ + / + \s+(\d+)\sstates,\sstored\s\((\d+)\svisited\)\n + \s+(\d+)\sstates,\smatched\n + \s+(\d+)\stransitions\s\(=\svisited\+matched\)\n + \s+(\d+)\satomic\ssteps\n + hash\sconflicts:\s+(\d+)\s\(resolved\) + /x ) { + $test->{$currTest}->{'pml'}->{'states'}->{'stateStored'} = $1; + $test->{$currTest}->{'pml'}->{'states'}->{'stateVisited'} = $2; + $test->{$currTest}->{'pml'}->{'states'}->{'stateMatched'} = $3; + $test->{$currTest}->{'pml'}->{'states'}->{'transitions'} = $4; + $test->{$currTest}->{'pml'}->{'states'}->{'atomicSteps'} = $5; + $test->{$currTest}->{'pml'}->{'hashConflicts'} = $6; + } + + if ($block =~ + / + \s+([\d\.]+)\sequivalent\smemory\susage\sfor\sstates.* + \s+([\d\.]+)\sactual\smemory\susage\sfor\sstates\n + \s+([\d\.]+)\smemory\sused\sfor\shash\stable\s\(-w(\d+)\)\n + \s+([\d\.]+)\smemory\sused\sfor\sDFS\sstack\s\(-m(\d+)\) + \s+([\d\.]+)\stotal\sactual\smemory\susage + /x ) { + $test->{$currTest}->{'pml'}->{'memory'}->{'states'} = $1; + $test->{$currTest}->{'pml'}->{'memory'}->{'actual'} = $2; + $test->{$currTest}->{'pml'}->{'memory'}->{'hashTable'} = $3; + $test->{$currTest}->{'pml'}->{'memory'}->{'hashLimit'} = $4; + $test->{$currTest}->{'pml'}->{'memory'}->{'dfsStack'} = $5; + $test->{$currTest}->{'pml'}->{'memory'}->{'dfsLimit'} = $6; + $test->{$currTest}->{'pml'}->{'memory'}->{'total'} = $7; + } + + next; + } + +} +close(FILE); + +if (@dataQuery > 0) { + while (my ($name, $data) = each $test) { + my $seperator = ""; + foreach (@dataQuery) { + my $currVal = $data; + my @query = @${$_}; + foreach (@query) { + my $dataKey = $_; + if (defined($currVal->{$dataKey})) { + $currVal = $currVal->{$dataKey}; + } else { + die("no key $dataKey in structure:\n" . Dumper($currVal)); + } + } + print $seperator . $currVal; + $seperator = ", "; + } + print "\n"; + } +} else { + while (my ($name, $data) = each $test) { + # get one $data into scope + print "Available Queries:\n"; + + sub dumpQueries() { + my $structure = shift; + my $path = shift || ""; + while (my ($name, $data) = each $structure) { + if (ref(\$data) eq "SCALAR") { + print "\t" . $path . $name . "\n"; + } else { + &dumpQueries($data, $path . $name . "."); + } + } + } + &dumpQueries($data); + exit; + } +} + diff --git a/test/w3c/graphs/data/pml_states.data b/test/w3c/graphs/data/pml_states.data deleted file mode 100644 index 7381008..0000000 --- a/test/w3c/graphs/data/pml_states.data +++ /dev/null @@ -1,84 +0,0 @@ -147, 108, 0.281, 3 -505, 116, 0.276, 6 -348, 108, 0.284, 3 -349, 204, 0.280, 4 -319, 108, 0.283, 3 -527, 196, 0.278, 5 -337, 196, 0.283, 3 -310, 108, 0.283, 5 -404, 108, 0.272, 10 -405, 108, 0.265, 13 -183, 196, 0.283, 3 -533, 124, 0.270, 9 -407, 108, 0.282, 4 -372, 108, 0.283, 4 -413, 108, 0.280, 11 -335, 196, 0.283, 3 -193, 108, 0.280, 4 -550, 108, 0.284, 4 -303, 108, 0.284, 3 -252, 108, 0.276, 8 -387, 108, 0.276, 18 -333, 196, 0.283, 3 -278, 108, 0.284, 4 -529, 196, 0.278, 5 -189, 108, 0.284, 3 -554, 108, 0.284, 5 -504, 124, 0.267, 11 -576, 108, 0.284, 13 -336, 108, 0.280, 4 -409, 108, 0.275, 6 -158, 108, 0.281, 4 -501, 108, 0.284, 3 -205, 204, 0.280, 4 -419, 108, 0.284, 3 -174, 108, 0.284, 3 -250, 100, 0.286, 6 -200, 108, 0.284, 3 -570, 108, 0.259, 10 -186, 204, 0.280, 4 -201, 108, 0.284, 3 -339, 196, 0.283, 3 -421, 108, 0.280, 5 -579, 108, 0.262, 8 -176, 204, 0.280, 4 -237, 108, 0.282, 7 -242, 108, 0.276, 9 -378, 108, 0.282, 4 -412, 108, 0.262, 8 -288, 108, 0.284, 3 -375, 108, 0.281, 4 -396, 112, 0.283, 3 -423, 108, 0.280, 4 -155, 124, 0.283, 3 -198, 204, 0.283, 3 -551, 116, 0.283, 4 -355, 108, 0.285, 4 -403c, 108, 0.279, 9 -416, 108, 0.279, 6 -417, 108, 0.279, 10 -330, 204, 0.279, 4 -376, 108, 0.284, 3 -506, 116, 0.274, 7 -187, 108, 0.284, 6 -318, 124, 0.281, 4 -149, 108, 0.282, 3 -364, 108, 0.279, 29 -173, 108, 0.284, 3 -279, 108, 0.284, 4 -495, 108, 0.280, 4 -287, 108, 0.284, 3 -406, 108, 0.267, 10 -323, 108, 0.284, 3 -553, 108, 0.284, 3 -153, 132, 0.282, 3 -190, 116, 0.280, 4 -377, 108, 0.278, 5 -403b, 108, 0.282, 6 -503, 116, 0.277, 5 -179, 196, 0.283, 3 -321, 108, 0.284, 3 -148, 108, 0.282, 3 -411, 108, 0.280, 4 -403a, 108, 0.275, 5 -144, 108, 0.281, 4 diff --git a/test/w3c/graphs/promela-states.sh b/test/w3c/graphs/promela-states.sh deleted file mode 100755 index 0cb7589..0000000 --- a/test/w3c/graphs/promela-states.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/bin/bash - -ME=`basename $0` -DIR="$( cd "$( dirname "$0" )" && pwd )" - -mkdir ${DIR}/data &> /dev/null - -${DIR}/../analyze_promela_tests.pl w3c pml.states.stateSize pml.memory.actual flat.actualComplexity > ${DIR}/data/pml_states.data - -cat ${DIR}/data/pml_states.data | gnuplot -p -e 'plot "-" with lines,"-" with lines' \ No newline at end of file diff --git a/test/w3c/graphs/run_gnuplot.sh b/test/w3c/graphs/run_gnuplot.sh deleted file mode 100755 index 26fe407..0000000 --- a/test/w3c/graphs/run_gnuplot.sh +++ /dev/null @@ -1,2 +0,0 @@ -#!/bin/bash -gnuplot test.plot > test.pdf -- cgit v0.12