From c66fa34eb48f81da05966b947a2e37067318a09f Mon Sep 17 00:00:00 2001 From: Stefan Radomski Date: Tue, 21 Oct 2014 20:45:42 +0200 Subject: More output when transforming --- src/uscxml/transform/ChartToFSM.cpp | 47 ++++++++++++++++++++++++--------- src/uscxml/transform/ChartToFSM.h | 3 +++ src/uscxml/transform/ChartToPromela.cpp | 10 ++++--- test/uscxml/promela/test-ltl.scxml | 16 +++++++++++ 4 files changed, 60 insertions(+), 16 deletions(-) create mode 100644 test/uscxml/promela/test-ltl.scxml diff --git a/src/uscxml/transform/ChartToFSM.cpp b/src/uscxml/transform/ChartToFSM.cpp index ae97d3f..c5ddd80 100644 --- a/src/uscxml/transform/ChartToFSM.cpp +++ b/src/uscxml/transform/ChartToFSM.cpp @@ -39,24 +39,27 @@ #define DUMP_STATS(nrTrans) \ uint64_t now = tthread::chrono::system_clock::now(); \ if (now - _lastTimeStamp > 1000) { \ - std::cerr << "T: " << _perfTransTotal << " [" << _perfTransProcessed << "/sec]"; \ + std::cerr << "## Transition: " << _perfTransUsed << " / " << _perfTransTotal << " [" << _perfTransProcessed << "/sec]"; \ if (nrTrans > 0) { \ std::cerr << " - 2**" << nrTrans << " = " << pow(2.0, static_cast(nrTrans)); \ } \ std::cerr << std::endl; \ - 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 << "Q: " << (_maxEventRaisedChain == UNDECIDABLE ? "UNK" : toStr(_maxEventRaisedChain)) << " / " << (_maxEventSentChain == UNDECIDABLE ? "UNK" : toStr(_maxEventSentChain)) << std::endl; \ - std::cerr << _perfTransTotal << ", " << _perfTransProcessed << ", " << _globalConf.size() << ", " << _perfStatesProcessed << ", " << _perfStatesCachedTotal << ", " << _perfStatesCachedProcessed << ", "; \ - std::cerr << _perfStatesSkippedTotal << ", " << _perfStatesSkippedProcessed << ", "; \ - std::cerr << (_maxEventRaisedChain == UNDECIDABLE ? "UNK" : toStr(_maxEventRaisedChain)) << ", "; \ - std::cerr << (_maxEventSentChain == UNDECIDABLE ? "UNK" : toStr(_maxEventSentChain)) << std::endl; \ + std::cerr << "## State : " << _globalConf.size() << " [" << _perfStatesProcessed << "/sec]" << std::endl; \ + std::cerr << "## Microstep : " << _perfMicroStepTotal << " [" << _perfMicroStepProcessed << "/sec]" << std::endl; \ + std::cerr << "## Cached : " << _perfStatesCachedTotal << " [" << _perfStatesCachedProcessed << "/sec]" << std::endl; \ + std::cerr << "## Skipped : " << _perfStatesSkippedTotal << " [" << _perfStatesSkippedProcessed << "/sec]" << std::endl; \ + std::cerr << "## Queues : " << (_maxEventRaisedChain == UNDECIDABLE ? "UNK" : toStr(_maxEventRaisedChain)) << " / " << (_maxEventSentChain == UNDECIDABLE ? "UNK" : toStr(_maxEventSentChain)) << std::endl; \ + std::cerr << _perfTransUsed << ", " << _perfTransTotal << ", " << _perfTransProcessed << ", "; \ + std::cerr << _globalConf.size() << ", " << _perfStatesProcessed << ", "; \ + std::cerr << _perfMicroStepTotal << ", " << _perfMicroStepProcessed << ", "; \ + std::cerr << _perfStatesCachedTotal << ", " << _perfStatesCachedProcessed << ", " << _perfStatesSkippedTotal << ", " << _perfStatesSkippedProcessed << ", "; \ + std::cerr << (_maxEventRaisedChain == UNDECIDABLE ? "UNK" : toStr(_maxEventRaisedChain)) << ", " << (_maxEventSentChain == UNDECIDABLE ? "UNK" : toStr(_maxEventSentChain)) << std::endl; \ std::cerr << std::endl; \ _perfTransProcessed = 0; \ _perfStatesProcessed = 0; \ _perfStatesCachedProcessed = 0; \ _perfStatesSkippedProcessed = 0; \ + _perfMicroStepProcessed = 0; \ _lastTimeStamp = now; \ } @@ -155,12 +158,15 @@ ChartToFSM::ChartToFSM(const Interpreter& other) { _lastTimeStamp = tthread::chrono::system_clock::now(); _perfTransProcessed = 0; _perfTransTotal = 0; + _perfTransUsed = 0; _perfStatesProcessed = 0; _perfStatesSkippedProcessed = 0; _perfStatesSkippedTotal = 0; _perfStatesCachedProcessed = 0; _perfStatesCachedTotal = 0; - + _perfMicroStepProcessed = 0; + _perfMicroStepTotal = 0; + _start = NULL; _currGlobalTransition = NULL; _lastTransientStateId = 0; @@ -360,8 +366,18 @@ void ChartToFSM::executeContent(const Arabica::DOM::Element& conten GlobalTransition::Action action; + NodeList childs = content.getChildNodes(); + for (unsigned int i = 0; i < childs.getLength(); i++) { + Node_base::Type type = childs.item(i).getNodeType(); + if (type == Node_base::ELEMENT_NODE || type == Node_base::COMMENT_NODE || type == Node_base::TEXT_NODE) { + goto HAS_VALID_CHILDREN; + } + } + return; + +HAS_VALID_CHILDREN: if (false) { - } else if (TAGNAME(content) == "transition" && content.hasChildNodes()) { + } else if (TAGNAME(content) == "transition") { action.transition = content; } else if (TAGNAME(content) == "onexit") { action.onExit = content; @@ -753,7 +769,6 @@ void ChartToFSM::getPotentialTransitionsForConf(const Arabica::XPath::NodeSetindex = _lastTransIndex++; // two combinations might have projected onto the same conflict-free set if (outMap.find(transition->transitionId) != outMap.end()) { @@ -761,6 +776,9 @@ void ChartToFSM::getPotentialTransitionsForConf(const Arabica::XPath::NodeSetindex = _lastTransIndex++; + _perfTransUsed++; // remember this conflict-free set // std::cerr << "New conflict-free subset: " << transition->transitionId << ":" << transition->eventDesc << std::endl; @@ -830,6 +848,7 @@ void ChartToFSM::explode() { while(sortTransIter != _transPerActiveConf[globalState->activeId]->sortedOutgoing.end()) { globalState->sortedOutgoing.push_back(new GlobalTransition(**sortTransIter)); // copy constructor globalState->sortedOutgoing.back()->index = _lastTransIndex++; + _perfTransUsed++; sortTransIter++; } _perfStatesCachedTotal++; @@ -868,6 +887,10 @@ void ChartToFSM::explode() { _currGlobalTransition = outgoingTrans; microstep(refsToTransitions(outgoingTrans->transitionRefs)); + assert(isLegalConfiguration(_configuration)); + + _perfMicroStepProcessed++; + _perfMicroStepTotal++; // if outgoing transition is spontaneous, add number of events to chain if (outgoingTrans->isEventless && diff --git a/src/uscxml/transform/ChartToFSM.h b/src/uscxml/transform/ChartToFSM.h index 919a5b2..f5d7c50 100644 --- a/src/uscxml/transform/ChartToFSM.h +++ b/src/uscxml/transform/ChartToFSM.h @@ -196,11 +196,14 @@ protected: uint64_t _perfTransProcessed; uint64_t _perfTransTotal; + uint64_t _perfTransUsed; uint64_t _perfStatesProcessed; uint64_t _perfStatesSkippedProcessed; uint64_t _perfStatesSkippedTotal; uint64_t _perfStatesCachedProcessed; uint64_t _perfStatesCachedTotal; + uint64_t _perfMicroStepProcessed; + uint64_t _perfMicroStepTotal; uint64_t _lastTimeStamp; size_t _lastTransientStateId; diff --git a/src/uscxml/transform/ChartToPromela.cpp b/src/uscxml/transform/ChartToPromela.cpp index b9b1637..930fb8d 100644 --- a/src/uscxml/transform/ChartToPromela.cpp +++ b/src/uscxml/transform/ChartToPromela.cpp @@ -279,8 +279,8 @@ void PromelaCodeAnalyzer::addCode(const std::string& code) { // break fall through from ASGN break; } - node->dump(); - assert(false); +// node->dump(); +// assert(false); break; } @@ -1664,12 +1664,14 @@ void ChartToPromela::writeFSM(std::ostream& stream) { // write initial transition // transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", _startState); // assert(transitions.size() == 1); - stream << " /* transition's executable content */" << std::endl; + stream << " /* transition to initial state */" << std::endl; assert(_start->sortedOutgoing.size() == 1); // initial transition has to be first one for control flow at start writeTransition(stream, _start->sortedOutgoing.front(), 1); + stream << std::endl; + stream << " /* transition's executable content */" << std::endl; // every other transition for (std::map::iterator stateIter = _globalConf.begin(); stateIter != _globalConf.end(); stateIter++) { for (std::list::iterator transIter = stateIter->second->sortedOutgoing.begin(); transIter != stateIter->second->sortedOutgoing.end(); transIter++) { @@ -1886,7 +1888,7 @@ void ChartToPromela::initNodes() { continue; Element stateElem(states[i]); _analyzer.addOrigState(ATTR(stateElem, "id")); - if (isCompound(stateElem) || isParallel(stateElem)) { + if ((isCompound(stateElem) || isParallel(stateElem)) && !parentIsScxmlState(stateElem)) { _analyzer.addEvent("done.state." + ATTR(stateElem, "id")); } } diff --git a/test/uscxml/promela/test-ltl.scxml b/test/uscxml/promela/test-ltl.scxml new file mode 100644 index 0000000..a584e06 --- /dev/null +++ b/test/uscxml/promela/test-ltl.scxml @@ -0,0 +1,16 @@ + + + + + + + + + + + + + \ No newline at end of file -- cgit v0.12