From f02d7e5919f16d8396839fcff1e0588d6ccf3004 Mon Sep 17 00:00:00 2001 From: Stefan Radomski Date: Mon, 6 Jul 2015 01:15:31 +0200 Subject: Various extensions and bug-fixes --- apps/uscxml-analyze.cpp | 166 ++++++++------ contrib/local/create-random-scxml.pl | 15 +- src/uscxml/Interpreter.cpp | 77 ++++++- src/uscxml/Interpreter.h | 2 + src/uscxml/debug/Complexity.cpp | 204 ++++++++++++++++++ src/uscxml/debug/Complexity.h | 78 +++++++ src/uscxml/debug/InterpreterIssue.cpp | 372 ++++++++++++++++++++++++-------- src/uscxml/server/HTTPServer.cpp | 4 +- src/uscxml/transform/ChartToFSM.cpp | 179 +-------------- src/uscxml/transform/ChartToFSM.h | 38 ---- src/uscxml/transform/ChartToPromela.cpp | 288 +++++++++++++++++++++---- src/uscxml/transform/ChartToPromela.h | 10 +- src/uscxml/transform/Transformer.h | 6 +- test/src/test-issue-reporting.cpp | 231 ++++++++++++++++++-- test/w3c/analyze_tests.pl | 53 ++++- test/w3c/run_promela_test.cmake | 18 +- 16 files changed, 1313 insertions(+), 428 deletions(-) create mode 100644 src/uscxml/debug/Complexity.cpp create mode 100644 src/uscxml/debug/Complexity.h diff --git a/apps/uscxml-analyze.cpp b/apps/uscxml-analyze.cpp index 75ec48c..d9db213 100644 --- a/apps/uscxml-analyze.cpp +++ b/apps/uscxml-analyze.cpp @@ -1,5 +1,6 @@ #include "uscxml/config.h" #include "uscxml/Interpreter.h" +#include "uscxml/debug/Complexity.h" #include "uscxml/transform/ChartToFSM.h" #include "uscxml/DOMUtils.h" #include @@ -34,11 +35,18 @@ void printUsageAndExit(const char* progName) { printf("%s version " USCXML_VERSION " (" CMAKE_BUILD_TYPE " build - " CMAKE_COMPILER_STRING ")\n", progStr.c_str()); printf("Usage\n"); - printf("\t%s", progStr.c_str()); + printf("\t%s", progStr.c_str()); + printf(" [-a {ASPECTS}] [-lN]"); #ifdef BUILD_AS_PLUGINS - printf(" [-p pluginPath]"); + printf(" [-p pluginPath]"); #endif - printf(" [URL]"); + printf(" [URL]"); + printf("\n"); + printf("Options\n"); + printf("\t-a {ASPECTS} : analyze with regard to comma seperated aspects\n"); + printf("\t 'issues' - find common pitfalls and syntactical errors\n"); + printf("\t 'metrics' - print metrics about the state-chart's complexity\n"); + printf("\t-lN : Set loglevel to N\n"); printf("\n"); exit(1); } @@ -46,11 +54,9 @@ void printUsageAndExit(const char* progName) { int main(int argc, char** argv) { using namespace uscxml; - std::string outType; std::string pluginPath; std::string inputFile; - std::string outputFile; - std::list annotations; + std::list aspects; #if defined(HAS_SIGNAL_H) && !defined(WIN32) signal(SIGPIPE, SIG_IGN); @@ -66,6 +72,7 @@ int main(int argc, char** argv) { struct option longOptions[] = { {"help", required_argument, 0, 'p'}, {"plugin-path", required_argument, 0, 'p'}, + {"aspect", optional_argument, 0, 'a'}, {"loglevel", required_argument, 0, 'l'}, {0, 0, 0, 0} }; @@ -74,7 +81,7 @@ int main(int argc, char** argv) { int optionInd = 0; int option; for (;;) { - option = getopt_long_only(argc, argv, "p:l:h", longOptions, &optionInd); + option = getopt_long_only(argc, argv, "a:p:l:h", longOptions, &optionInd); if (option == -1) { break; } @@ -87,6 +94,9 @@ int main(int argc, char** argv) { case 'p': pluginPath = optarg; break; + case 'a': + aspects = InterpreterImpl::tokenize(optarg, ','); + break; case 'l': break; case 'h': @@ -132,59 +142,95 @@ int main(int argc, char** argv) { } // analyze here - Arabica::XPath::NodeSet states = interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "state"); - Arabica::XPath::NodeSet final = interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "final"); - Arabica::XPath::NodeSet parallels = interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "parallel"); - Arabica::XPath::NodeSet shallowHistories = interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "history[@type='shallow']"); - shallowHistories.push_back(interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "history[not(@type)]")); - Arabica::XPath::NodeSet deepHistories = interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "history[@type='deep']"); - Arabica::XPath::NodeSet transitions = interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "transition"); - - std::cout << "# Number of elements" << std::endl; - std::cout << "nr_states: " << (states.size() + final.size() + parallels.size()) << std::endl; - std::cout << "nr_parallel: " << parallels.size() << std::endl; - std::cout << "nr_hist_flat: " << shallowHistories.size() << std::endl; - std::cout << "nr_hist_deep: " << deepHistories.size() << std::endl; - std::cout << "nr_trans: " << transitions.size() << std::endl; - - - std::cout << "# Transition Histogram: number of transitions, number of active configurations" << std::endl; - - size_t numberOfLegalConfs = 0; - size_t lastBin = 0; - std::map histogram = Complexity::getTransitionHistogramm(interpreter.getDocument().getDocumentElement()); - for (std::map::iterator binIter = histogram.begin(); binIter != histogram.end(); binIter++) { - while (binIter->first > lastBin) { - std::cout << "th: " << toStr(lastBin++) << ", 0" << std::endl; - } - std::cout << "th: " << toStr(binIter->first) << ", " << binIter->second << std::endl; - numberOfLegalConfs += binIter->second; - lastBin = binIter->first + 1; - } - - std::stringstream transPowerSetSS; - std::string transPowerSetSeperator = ""; - for (std::map::reverse_iterator binIter = histogram.rbegin(); binIter != histogram.rend(); binIter++) { - transPowerSetSS << transPowerSetSeperator << binIter->second << " * " << "2**" << binIter->first; - transPowerSetSeperator = " + "; - } - std::cout << "# Sum of Powersets:" << std::endl; - std::cout << "ps_sum: " << transPowerSetSS.str() << std::endl; - std::cout << "# Upper bounds:" << std::endl; - std::cout << "# \tActive configurations: " << std::endl; - std::cout << "up_ac: " << numberOfLegalConfs << std::endl; - std::cout << "# \tGlobal configurations: " << std::endl; - std::cout << "up_gc: " << Complexity::stateMachineComplexity(interpreter.getDocument().getDocumentElement()) << std::endl; - - std::cout << "# \tGlobal configurations (no history): " << std::endl; - std::cout << "up_gcnh: " << Complexity::stateMachineComplexity(interpreter.getDocument().getDocumentElement(), uscxml::Complexity::IGNORE_HISTORY) << std::endl; - - std::cout << "# \tGlobal configurations (no nested data): " << std::endl; - std::cout << "up_gcnd: " << Complexity::stateMachineComplexity(interpreter.getDocument().getDocumentElement(), uscxml::Complexity::IGNORE_NESTED_DATA) << std::endl; - - std::cout << "# \tGlobal configurations (no nested data, no history): " << std::endl; - std::cout << "up_gcnhd: " << Complexity::stateMachineComplexity(interpreter.getDocument().getDocumentElement(), uscxml::Complexity::IGNORE_HISTORY_AND_NESTED_DATA) << std::endl; - + if (aspects.size() == 0 || std::find(aspects.begin(), aspects.end(), "issues") != aspects.end()) { + std::list issues = interpreter.validate(); + for (std::list::iterator issueIter = issues.begin(); issueIter != issues.end(); issueIter++) { + std::cout << *issueIter << std::endl; + } + } + + if (aspects.size() == 0 || std::find(aspects.begin(), aspects.end(), "metrics") != aspects.end()) { + + Arabica::XPath::NodeSet states = interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "state"); + Arabica::XPath::NodeSet final = interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "final"); + Arabica::XPath::NodeSet parallels = interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "parallel"); + Arabica::XPath::NodeSet shallowHistories = interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "history[@type='shallow']"); + shallowHistories.push_back(interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "history[not(@type)]")); + Arabica::XPath::NodeSet deepHistories = interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "history[@type='deep']"); + Arabica::XPath::NodeSet transitions = interpreter.getNodeSetForXPath("//" + interpreter.getNameSpaceInfo().xpathPrefix + "transition"); + + std::cout << "### Number of XML elements" << std::endl; + std::cout << "# + + + " << std::endl; + std::cout << "nr_states: " << (states.size() + final.size() + parallels.size() + shallowHistories.size() + deepHistories.size()) << std::endl; + std::cout << "# " << std::endl; + std::cout << "nr_parallel: " << parallels.size() << std::endl; + std::cout << "# " << std::endl; + std::cout << "nr_hist_flat: " << shallowHistories.size() << std::endl; + std::cout << "# " << std::endl; + std::cout << "nr_hist_deep: " << deepHistories.size() << std::endl; + std::cout << "# " << std::endl; + std::cout << "nr_trans: " << transitions.size() << std::endl; + std::cout << "#" << std::endl; + + + std::cout << "### Transition Histogram: number of transitions, number of active configurations" << std::endl; + + size_t numberOfLegalConfs = 0; + size_t lastBin = 0; + std::cout << "th: "; + std::string seperator = ""; + std::map histogram = Complexity::getTransitionHistogramm(interpreter.getDocument().getDocumentElement()); + for (std::map::iterator binIter = histogram.begin(); binIter != histogram.end(); binIter++) { + while (binIter->first > lastBin) { + lastBin++; + std::cout << seperator << "0"; + seperator = ", "; + } + std::cout << seperator << binIter->second; + seperator = ", "; + numberOfLegalConfs += binIter->second; + lastBin = binIter->first + 1; + } + std::cout << std::endl << "#" << std::endl; + + + std::stringstream transPowerSetSS; + std::string transPowerSetSeperator = ""; + for (std::map::reverse_iterator binIter = histogram.rbegin(); binIter != histogram.rend(); binIter++) { + transPowerSetSS << transPowerSetSeperator << binIter->second << " * " << "2**" << binIter->first; + transPowerSetSeperator = " + "; + } + std::cout << "# Sum of Powersets:" << std::endl; + std::cout << "ps_sum: " << transPowerSetSS.str() << std::endl; + std::cout << "#" << std::endl; + + std::cout << "### Upper bounds:" << std::endl; + std::cout << "# \tActive configurations: " << std::endl; + std::cout << "up_ac: " << numberOfLegalConfs << std::endl; + std::cout << "# \tGlobal configurations: " << std::endl; + std::cout << "up_gc: " << Complexity::stateMachineComplexity(interpreter) << std::endl; + + std::cout << "# \tGlobal configurations (no history): " << std::endl; + std::cout << "up_gcnh: " << Complexity::stateMachineComplexity(interpreter, uscxml::Complexity::IGNORE_HISTORY) << std::endl; + + std::cout << "# \tGlobal configurations (no nested data): " << std::endl; + std::cout << "up_gcnd: " << Complexity::stateMachineComplexity(interpreter, uscxml::Complexity::IGNORE_NESTED_DATA) << std::endl; + + std::cout << "# \tGlobal configurations (no unreachable): " << std::endl; + std::cout << "up_gcnu: " << Complexity::stateMachineComplexity(interpreter, uscxml::Complexity::IGNORE_UNREACHABLE) << std::endl; + + std::cout << "# \tGlobal configurations (no nested data, no history): " << std::endl; + std::cout << "up_gcnhd: " << Complexity::stateMachineComplexity(interpreter, uscxml::Complexity::IGNORE_HISTORY | uscxml::Complexity::IGNORE_NESTED_DATA) << std::endl; + + std::cout << "# \tGlobal configurations (no history, no unreachable): " << std::endl; + std::cout << "up_gcnhu: " << Complexity::stateMachineComplexity(interpreter, uscxml::Complexity::IGNORE_HISTORY | uscxml::Complexity::IGNORE_UNREACHABLE) << std::endl; + + std::cout << "# \tGlobal configurations (no nested data, no unreachable): " << std::endl; + std::cout << "up_gcndu: " << Complexity::stateMachineComplexity(interpreter, uscxml::Complexity::IGNORE_NESTED_DATA | uscxml::Complexity::IGNORE_UNREACHABLE) << std::endl; + + std::cout << "# \tGlobal configurations (no nested data, no history, no unreachable): " << std::endl; + std::cout << "up_gcnhdu: " << Complexity::stateMachineComplexity(interpreter, uscxml::Complexity::IGNORE_HISTORY | uscxml::Complexity::IGNORE_NESTED_DATA | uscxml::Complexity::IGNORE_UNREACHABLE) << std::endl; + } } catch (Event e) { std::cout << e << std::endl; } diff --git a/contrib/local/create-random-scxml.pl b/contrib/local/create-random-scxml.pl index 7c6a3b8..5674852 100755 --- a/contrib/local/create-random-scxml.pl +++ b/contrib/local/create-random-scxml.pl @@ -25,6 +25,9 @@ my $maxStates = $options{'states-max'} || 60; my $maxTrans = $options{'trans-max'} || 6; my $maxEvents = $options{'trans-max'} || int($maxStates / 3) + 1; +# $maxStates = 8; +# $maxTrans = 8 + srand($seed); my $machine; @@ -33,9 +36,9 @@ my $stateId = 0; my $probs = { 'state' => { 'type' => { - 'history' => 1, + 'history' => 2, 'parallel' => 2, - 'state' => 6, + 'state' => 5, 'final' => 1 } }, @@ -46,7 +49,7 @@ my $probs = { 'execContent' => 0.7, }, 'history' => { - 'deep' => 0.2 + 'deep' => 0.4 } }; @@ -159,9 +162,9 @@ sub writeState { writeState($_); } - foreach (@{$state->{'transitions'}}) { - writeTransition($_); - } + # foreach (@{$state->{'transitions'}}) { + # writeTransition($_); + # } print STDOUT '{'type'} . '>'; diff --git a/src/uscxml/Interpreter.cpp b/src/uscxml/Interpreter.cpp index 1b2ca15..58991e5 100644 --- a/src/uscxml/Interpreter.cpp +++ b/src/uscxml/Interpreter.cpp @@ -1326,7 +1326,7 @@ void InterpreterImpl::setupDOM() { } #endif - // make sure every invoke has an idlocation or id + // make sure every invoke has an idlocation or id - actually required! Arabica::XPath::NodeSet invokes = _xpath.evaluate("//" + _nsInfo.xpathPrefix + "invoke", _scxml).asNodeSet(); for (int i = 0; i < invokes.size(); i++) { Arabica::DOM::Element invokeElem = Arabica::DOM::Element(invokes[i]); @@ -2866,6 +2866,81 @@ Arabica::XPath::NodeSet InterpreterImpl::getInitialStates(Arabica:: return Arabica::XPath::NodeSet(); } +NodeSet InterpreterImpl::getReachableStates() { + /** Check which states are reachable */ + + NodeSet reachable; + reachable.push_back(_scxml); + + bool hasChanges = true; + + while (hasChanges) { + // iterate initials and transitions until stable, unneccerily iterates complete reachable set everytime + + hasChanges = false; + // reachable per initial attribute or document order - size will increase as we append new states + for (int i = 0; i < reachable.size(); i++) { + // get the state's initial states + Element state = Element(reachable[i]); + try { + NodeSet initials = getInitialStates(state); + for (int j = 0; j < initials.size(); j++) { + Element initial = Element(initials[j]); + if (!InterpreterImpl::isMember(initial, reachable)) { + reachable.push_back(initial); + hasChanges = true; + } + } + } catch (Event e) { + } + } + + // reachable per target attribute in transitions + for (int i = 0; i < reachable.size(); i++) { + Element state = Element(reachable[i]); + NodeSet transitions = InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "transition", state, false); + for (int j = 0; j < transitions.size(); j++) { + Element transition = Element(transitions[j]); + try { + NodeSet targets = getTargetStates(transition); + for (int k = 0; k < targets.size(); k++) { + Element target = Element(targets[k]); + if (!InterpreterImpl::isMember(target, reachable)) { + reachable.push_back(target); + hasChanges = true; + } + } + } catch (Event e) { + } + } + } + + // reachable via a reachable child state + for (int i = 0; i < reachable.size(); i++) { + Element state = Element(reachable[i]); + if (InterpreterImpl::isAtomic(state)) { + // iterate the states parents + Node parent = state.getParentNode(); + while(parent && parent.getNodeType() == Node_base::ELEMENT_NODE) { + Element parentElem = Element(parent); + if (!InterpreterImpl::isState(parentElem)) { + break; + } + if (!InterpreterImpl::isMember(parentElem, reachable)) { + reachable.push_back(parent); + hasChanges = true; + } + parent = parent.getParentNode(); + } + } + } + } + + + return reachable; +} + + NodeSet InterpreterImpl::getTargetStates(const Arabica::DOM::Element& transition) { if (_cachedTargets.find(transition) != _cachedTargets.end()) return _cachedTargets[transition]; diff --git a/src/uscxml/Interpreter.h b/src/uscxml/Interpreter.h index bef4c88..5aa4b3f 100644 --- a/src/uscxml/Interpreter.h +++ b/src/uscxml/Interpreter.h @@ -434,6 +434,8 @@ public: Arabica::XPath::NodeSet getDocumentInitialTransitions(); Arabica::XPath::NodeSet getInitialStates(Arabica::DOM::Element state = Arabica::DOM::Element()); + Arabica::XPath::NodeSet getReachableStates(); + static Arabica::XPath::NodeSet getChildStates(const Arabica::DOM::Node& state); static Arabica::XPath::NodeSet getChildStates(const Arabica::XPath::NodeSet& state); static Arabica::DOM::Element getParentState(const Arabica::DOM::Node& element); diff --git a/src/uscxml/debug/Complexity.cpp b/src/uscxml/debug/Complexity.cpp new file mode 100644 index 0000000..8a7d8db --- /dev/null +++ b/src/uscxml/debug/Complexity.cpp @@ -0,0 +1,204 @@ +/** +* @file +* @author 2012-2015 Stefan Radomski (stefan.radomski@cs.tu-darmstadt.de) +* @copyright Simplified BSD +* +* @cond +* This program is free software: you can redistribute it and/or modify +* it under the terms of the FreeBSD license as published by the FreeBSD +* project. +* +* This program is distributed in the hope that it will be useful, +* but WITHOUT ANY WARRANTY; without even the implied warranty of +* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. +* +* You should have received a copy of the FreeBSD license along with this +* program. If not, see . +* @endcond +*/ + +#include "Complexity.h" +#include "uscxml/DOMUtils.h" + +namespace uscxml { + +using namespace Arabica::DOM; +using namespace Arabica::XPath; + +std::list > > Complexity::getAllConfigurations(const Arabica::DOM::Element& root) { + + std::list > > allConfigurations; + std::string nsPrefix = (root.getPrefix().size() > 0 ? root.getPrefix() + ":" : ""); + std::string localName = root.getLocalName(); + bool isAtomic = true; + + NodeList children = root.getChildNodes(); + for (int i = 0; i < children.getLength(); i++) { + if (children.item(i).getNodeType() != Node_base::ELEMENT_NODE) + continue; + Element childElem(children.item(i)); + if (childElem.getTagName() == nsPrefix + "state" || + childElem.getTagName() == nsPrefix + "parallel" || + childElem.getTagName() == nsPrefix + "final") { + // nested child state + std::list > > nestedConfigurations = getAllConfigurations(childElem); + isAtomic = false; + if (localName == "parallel" && allConfigurations.size() > 0) { + // for every nested configuration, every new nested is valid + std::list > > combinedConfigurations; + for (std::list > >::iterator existIter = allConfigurations.begin(); existIter != allConfigurations.end(); existIter++) { + std::set > existingConfig = *existIter; + + for (std::list > >::iterator newIter = nestedConfigurations.begin(); newIter != nestedConfigurations.end(); newIter++) { + + std::set > newConfig = *newIter; + std::set > combinedSet; + combinedSet.insert(existingConfig.begin(), existingConfig.end()); + combinedSet.insert(newConfig.begin(), newConfig.end()); + + combinedConfigurations.push_back(combinedSet); + } + } + allConfigurations = combinedConfigurations; + } else { + // just add nested configurations and this + for (std::list > >::iterator newIter = nestedConfigurations.begin(); newIter != nestedConfigurations.end(); newIter++) { + std::set > newConfig = *newIter; + if (localName != "scxml") + newConfig.insert(root); + allConfigurations.push_back(newConfig); + } + } + } + } + + if (isAtomic) { + std::set > soleConfig; + soleConfig.insert(root); + allConfigurations.push_back(soleConfig); + } + return allConfigurations; +} + +std::map Complexity::getTransitionHistogramm(const Arabica::DOM::Element& root) { + std::map histogram; + std::string nameSpace; + + std::list > > allConfig = Complexity::getAllConfigurations(root); + + // for every legal configuration, count the transitions + for (std::list > >::iterator confIter = allConfig.begin(); confIter != allConfig.end(); confIter++) { + NodeSet configNodeSet; + std::set > config = *confIter; + for (std::set >::iterator elemIter = config.begin(); elemIter != config.end(); elemIter++) { + configNodeSet.push_back(*elemIter); + if (nameSpace.size() == 0 && elemIter->getPrefix().size() > 0) + nameSpace = elemIter->getPrefix() + ":"; + } + NodeSet transitions = InterpreterImpl::filterChildElements(nameSpace + "transition", configNodeSet); + histogram[transitions.size()]++; + } + + return histogram; +} + + +uint64_t Complexity::stateMachineComplexity(InterpreterImpl* interpreter, Variant variant) { + Arabica::DOM::Element root = interpreter->getDocument().getDocumentElement(); + + Arabica::XPath::NodeSet reachable; + + if (variant & IGNORE_UNREACHABLE) { + reachable = interpreter->getReachableStates(); + } + + Complexity complexity = calculateStateMachineComplexity(root, reachable); + uint64_t value = complexity.value; + + if (!(variant & IGNORE_HISTORY)) { + for (std::list::const_iterator histIter = complexity.history.begin(); histIter != complexity.history.end(); histIter++) { + value *= *histIter; + } + } + + if (!(variant & IGNORE_NESTED_DATA)) { + bool ignoreNestedData = false; + if (root.getLocalName() == "scxml" && (!HAS_ATTR_CAST(root, "binding") || boost::to_lower_copy(ATTR_CAST(root, "binding")) == "early")) { + ignoreNestedData = true; + } + + if (!ignoreNestedData) { + uint64_t power = complexity.nestedData; + while(power--) { + value *= 2; + } + } + } + + return value; +} + +Complexity Complexity::calculateStateMachineComplexity(const Arabica::DOM::Element& root, const Arabica::XPath::NodeSet& reachable) { + Complexity complexity; + + bool hasFlatHistory = false; + bool hasDeepHistory = false; + bool hasNestedData = false; + + Arabica::DOM::NodeList childElems = root.getChildNodes(); + for (int i = 0; i < childElems.getLength(); i++) { + if (childElems.item(i).getNodeType() != Node_base::ELEMENT_NODE) + continue; + Element childElem = Element(childElems.item(i)); + if (InterpreterImpl::isHistory(childElem)) { + if (HAS_ATTR(childElem, "type") && ATTR(childElem, "type") == "deep") { + hasDeepHistory = true; + } else { + hasFlatHistory = true; + } + } + if (!hasNestedData && childElem.getLocalName() == "datamodel") { + Arabica::DOM::NodeList dataElemChilds = childElem.getChildNodes(); + for (int j = 0; j < dataElemChilds.getLength(); j++) { + if (dataElemChilds.item(j).getLocalName() == "data") + hasNestedData = true; + } + } + } + + if (hasNestedData) + complexity.nestedData++; + + if (reachable.size() > 0 && !InterpreterImpl::isMember(root, reachable)) { + return 0; + } else if (InterpreterImpl::isCompound(root) || TAGNAME(root) == "scxml") { + // compounds can be in any of the child state -> add + NodeSet childs = InterpreterImpl::getChildStates(root); + for (int i = 0; i < childs.size(); i++) { + complexity += calculateStateMachineComplexity(Element(childs[i]), reachable); + } + if (hasFlatHistory) { + complexity.history.push_back(childs.size()); + } + if (hasDeepHistory) { + complexity.history.push_back(complexity.value); + } + } else if (InterpreterImpl::isParallel(root)) { + // parallels are in all states -> multiply + NodeSet childs = InterpreterImpl::getChildStates(root); + complexity.value = 1; + for (int i = 0; i < childs.size(); i++) { + complexity *= calculateStateMachineComplexity(Element(childs[i]), reachable); + } + if (hasDeepHistory) { + complexity.history.push_back(complexity.value); + } + + } else if (InterpreterImpl::isAtomic(root)) { + return 1; + } + + return complexity; +} + +} \ No newline at end of file diff --git a/src/uscxml/debug/Complexity.h b/src/uscxml/debug/Complexity.h new file mode 100644 index 0000000..76330fd --- /dev/null +++ b/src/uscxml/debug/Complexity.h @@ -0,0 +1,78 @@ +/** + * @file + * @author 2012-2015 Stefan Radomski (stefan.radomski@cs.tu-darmstadt.de) + * @copyright Simplified BSD + * + * @cond + * This program is free software: you can redistribute it and/or modify + * it under the terms of the FreeBSD license as published by the FreeBSD + * project. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. + * + * You should have received a copy of the FreeBSD license along with this + * program. If not, see . + * @endcond + */ + +#ifndef COMPLEXITY_H_F972C065 +#define COMPLEXITY_H_F972C065 + +#include "uscxml/Common.h" // for USCXML_API +#include "uscxml/Interpreter.h" + +namespace uscxml { + +class USCXML_API Complexity { +public: + + enum Variant { + IGNORE_NOTHING = 0x0000, + IGNORE_HISTORY = 0x0001, + IGNORE_NESTED_DATA = 0x0002, + IGNORE_UNREACHABLE = 0x0004, + }; + + Complexity() : value(0), nestedData(0) {} + Complexity(uint64_t value) : value(value), nestedData(0) {} + + Complexity& operator+=(const Complexity& rhs) { + value += rhs.value; + nestedData += rhs.nestedData; + history.insert(history.end(), rhs.history.begin(), rhs.history.end()); + return *this; + } + + Complexity& operator*=(const Complexity& rhs) { + value *= rhs.value; + nestedData += rhs.nestedData; + history.insert(history.end(), rhs.history.begin(), rhs.history.end()); + return *this; + } + + static uint64_t stateMachineComplexity(const Interpreter& interpreter, Complexity::Variant variant = IGNORE_NOTHING) { + return stateMachineComplexity(interpreter.getImpl().get()); + } + static uint64_t stateMachineComplexity(InterpreterImpl* interpreter, Complexity::Variant variant = IGNORE_NOTHING); + + static std::list > > getAllConfigurations(const Arabica::DOM::Element& root); + static std::map getTransitionHistogramm(const Arabica::DOM::Element& root); + +protected: + static Complexity calculateStateMachineComplexity(const Arabica::DOM::Element& root, const Arabica::XPath::NodeSet& reachable); + + uint64_t value; + uint64_t nestedData; + std::list history; +}; + +inline Complexity::Variant operator | ( Complexity::Variant lhs, Complexity::Variant rhs ) { + // Cast to int first otherwise we'll just end up recursing + return static_cast< Complexity::Variant >( static_cast< int >( lhs ) | static_cast< int >( rhs ) ); +} + +} + +#endif /* end of include guard: COMPLEXITY_H_F972C065 */ diff --git a/src/uscxml/debug/InterpreterIssue.cpp b/src/uscxml/debug/InterpreterIssue.cpp index 0bca74e..103211b 100644 --- a/src/uscxml/debug/InterpreterIssue.cpp +++ b/src/uscxml/debug/InterpreterIssue.cpp @@ -21,6 +21,7 @@ #include "InterpreterIssue.h" #include "uscxml/DOMUtils.h" +#include "uscxml/debug/Complexity.h" #include "uscxml/Interpreter.h" #include "uscxml/Factory.h" @@ -53,79 +54,42 @@ void assembleNodeSets(const std::string nsPrefix, const Node& node, } } -NodeSet getReachableStates(const Node& scxml, InterpreterImpl* interpreter, const std::string& nsPrefix) { - /** Check whether this state is reachable */ - - NodeSet reachable; - reachable.push_back(scxml); - - bool hasChanges = true; - - while (hasChanges) { - // iterate initials and transitions until stable - - hasChanges = false; - // reachable per initial attribute or document order - size will increase as we append new states - for (int i = 0; i < reachable.size(); i++) { - // get the state's initial states - Element state = Element(reachable[i]); - try { - NodeSet initials = interpreter->getInitialStates(state); - for (int j = 0; j < initials.size(); j++) { - Element initial = Element(initials[j]); - if (!InterpreterImpl::isMember(initial, reachable)) { - reachable.push_back(initial); - hasChanges = true; - } - } - } catch (Event e) { - } - } - - // reachable per target attribute in transitions - for (int i = 0; i < reachable.size(); i++) { - Element state = Element(reachable[i]); - NodeSet transitions = InterpreterImpl::filterChildElements(nsPrefix + "transition", state, false); - for (int j = 0; j < transitions.size(); j++) { - Element transition = Element(transitions[j]); - try { - NodeSet targets = interpreter->getTargetStates(transition); - for (int k = 0; k < targets.size(); k++) { - Element target = Element(targets[k]); - if (!InterpreterImpl::isMember(target, reachable)) { - reachable.push_back(target); - hasChanges = true; - } - } - } catch (Event e) { - } - } - } - } - - // reachable via a reachable child state - for (int i = 0; i < reachable.size(); i++) { - Element state = Element(reachable[i]); - if (InterpreterImpl::isAtomic(state)) { - // iterate the states parents - Node parent = state.getParentNode(); - while(parent && parent.getNodeType() == Node_base::ELEMENT_NODE) { - Element parentElem = Element(parent); - if (!InterpreterImpl::isState(parentElem)) { - break; - } - if (!InterpreterImpl::isMember(parentElem, reachable)) { - reachable.push_back(parent); - } - parent = parent.getParentNode(); - } - } - } - return reachable; +/** + * Can the given states ever appear in an active configuration? + */ +bool hasLegalCompletion(const NodeSet& states) { + if (states.size() < 2) + return true; + + // iterate every pair + for (unsigned int outer = 0; outer < states.size() - 1; outer++) { + Element s1(states[outer]); + for (unsigned int inner = outer + 1; inner < states.size(); inner++) { + Element s2(states[inner]); + Node parent; + + // ok to be directly ancestorally related + if (InterpreterImpl::isDescendant(s1, s2) || InterpreterImpl::isDescendant(s2, s1)) + goto NEXT_PAIR; + + // find least common ancestor + parent = s1.getParentNode(); + while(parent && parent.getNodeType() == Node_base::ELEMENT_NODE) { + if (InterpreterImpl::isDescendant(s2, parent)) { + if (InterpreterImpl::isParallel(Element(parent))) + goto NEXT_PAIR; + } + parent = parent.getParentNode(); + } + + return false; + NEXT_PAIR:; + } + } + return true; } - std::list InterpreterIssue::forInterpreter(InterpreterImpl* interpreter) { // some things we need to prepare first if (interpreter->_factory == NULL) @@ -156,7 +120,7 @@ std::list InterpreterIssue::forInterpreter(InterpreterImpl* in NodeSet scxmls = nodeSets["scxml"]; scxmls.push_back(_scxml); - NodeSet reachable = getReachableStates(_scxml, interpreter, _nsInfo.xmlNSPrefix); + NodeSet reachable = interpreter->getReachableStates(); NodeSet& states = nodeSets["state"]; NodeSet& parallels = nodeSets["parallel"]; @@ -206,7 +170,8 @@ std::list InterpreterIssue::forInterpreter(InterpreterImpl* in allExecContents.push_back(cancels); NodeSet allElements; - allElements.push_back(allStates); + allElements.push_back(scxmls); + allElements.push_back(allStates); allElements.push_back(allExecContents); allElements.push_back(transitions); allElements.push_back(initials); @@ -222,17 +187,30 @@ std::list InterpreterIssue::forInterpreter(InterpreterImpl* in std::set execContentSet; - execContentSet.insert("raise"); execContentSet.insert("if"); execContentSet.insert("elseif"); execContentSet.insert("else"); execContentSet.insert("foreach"); - execContentSet.insert("log"); + execContentSet.insert("raise"); execContentSet.insert("send"); + execContentSet.insert("cancel"); execContentSet.insert("assign"); execContentSet.insert("script"); - execContentSet.insert("cancel"); - + execContentSet.insert("log"); + + // required attributes per standard + std::map > reqAttr; + reqAttr["scxml"].insert("xmlns"); + reqAttr["scxml"].insert("version"); + reqAttr["raise"].insert("event"); + reqAttr["if"].insert("cond"); + reqAttr["elseif"].insert("cond"); + reqAttr["foreach"].insert("array"); + reqAttr["foreach"].insert("item"); + reqAttr["data"].insert("id"); + reqAttr["assign"].insert("location"); + reqAttr["param"].insert("name"); + // these are the valid children for elements in the SCXML namespace as per specification std::map > validChildren; validChildren["scxml"].insert("state"); @@ -244,13 +222,13 @@ std::list InterpreterIssue::forInterpreter(InterpreterImpl* in validChildren["state"].insert("onentry"); validChildren["state"].insert("onexit"); validChildren["state"].insert("transition"); - validChildren["state"].insert("initial"); validChildren["state"].insert("state"); validChildren["state"].insert("parallel"); - validChildren["state"].insert("final"); - validChildren["state"].insert("history"); - validChildren["state"].insert("datamodel"); - validChildren["state"].insert("invoke"); + validChildren["state"].insert("history"); + validChildren["state"].insert("datamodel"); + validChildren["state"].insert("invoke"); + validChildren["state"].insert("initial"); + validChildren["state"].insert("final"); validChildren["parallel"].insert("onentry"); validChildren["parallel"].insert("onexit"); @@ -305,7 +283,7 @@ std::list InterpreterIssue::forInterpreter(InterpreterImpl* in if (InterpreterImpl::isMember(state, finals) && !HAS_ATTR(state, "id")) // id is not required for finals continue; - // check for existance of id attribute + // check for existance of id attribute - this not actually required! if (!HAS_ATTR(state, "id")) { issues.push_back(InterpreterIssue("State has no 'id' attribute", state, InterpreterIssue::USCXML_ISSUE_FATAL)); continue; @@ -427,6 +405,25 @@ NEXT_TRANSITION: } } + // check for useless history elements + { + for (int i = 0; i < histories.size(); i++) { + Element history = Element(histories[i]); + if (!history.getParentNode() || history.getParentNode().getNodeType() != Node_base::ELEMENT_NODE) + continue; // syntax check will have catched this + Element parent(history.getParentNode()); + if (InterpreterImpl::isAtomic(parent)) { + issues.push_back(InterpreterIssue("Useless history '" + ATTR(history, "id") + "' in atomic state", history, InterpreterIssue::USCXML_ISSUE_INFO)); + continue; + } + std::list > > configs = Complexity::getAllConfigurations(parent); + if (configs.size() <= 1) { + issues.push_back(InterpreterIssue("Useless history '" + ATTR(history, "id") + "' in state with single legal configuration", history, InterpreterIssue::USCXML_ISSUE_INFO)); + continue; + } + } + } + // check for valid initial attribute { NodeSet withInitialAttr; @@ -435,18 +432,115 @@ NEXT_TRANSITION: for (int i = 0; i < withInitialAttr.size(); i++) { Element state = Element(withInitialAttr[i]); + if (HAS_ATTR(state, "initial")) { - std::list intials = InterpreterImpl::tokenizeIdRefs(ATTR(state, "initial")); + NodeSet childs; + childs.push_back(InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "state", state, true)); + childs.push_back(InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "parallel", state, true)); + childs.push_back(InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "final", state, true)); + childs.push_back(InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "history", state, true)); + + std::list intials = InterpreterImpl::tokenizeIdRefs(ATTR(state, "initial")); for (std::list::iterator initIter = intials.begin(); initIter != intials.end(); initIter++) { if (seenStates.find(*initIter) == seenStates.end()) { issues.push_back(InterpreterIssue("Initial attribute has invalid target state with id '" + *initIter + "'", state, InterpreterIssue::USCXML_ISSUE_FATAL)); continue; } + // value of the 'initial' attribute [..] must be descendants of the containing or element + if (!InterpreterImpl::isMember(seenStates[*initIter], childs)) { + issues.push_back(InterpreterIssue("Initial attribute references non-child state '" + *initIter + "'", state, InterpreterIssue::USCXML_ISSUE_FATAL)); + } } } } } + // check for legal configuration of target sets + { + std::map, std::string > targetIdSets; + for (int i = 0; i < transitions.size(); i++) { + Element transition = Element(transitions[i]); + + if (HAS_ATTR(transition, "target")) { + targetIdSets[transition] = ATTR(transition, "target"); + } + } + + for (int i = 0; i < initials.size(); i++) { + Element initial = Element(initials[i]); + + if (HAS_ATTR(initial, "target")) { + targetIdSets[initial] = ATTR(initial, "target"); + } + } + + for (int i = 0; i < allStates.size(); i++) { + Element state = Element(allStates[i]); + + if (HAS_ATTR(state, "initial")) { + targetIdSets[state] = ATTR(state, "initial"); + } + } + + for (std::map, std::string >::iterator setIter = targetIdSets.begin(); + setIter != targetIdSets.end(); + setIter++) { + NodeSet targets; + std::list targetIds = InterpreterImpl::tokenizeIdRefs(setIter->second); + for (std::list::iterator tgtIter = targetIds.begin(); tgtIter != targetIds.end(); tgtIter++) { + if (seenStates.find(*tgtIter) == seenStates.end()) + goto NEXT_SET; + targets.push_back(seenStates[*tgtIter]); + } + if (!hasLegalCompletion(targets)) { + issues.push_back(InterpreterIssue("Target states cause illegal configuration", setIter->first, InterpreterIssue::USCXML_ISSUE_FATAL)); + } + NEXT_SET:; + } + } + + // check for valid initial transition + { + NodeSet initTrans; + initTrans.push_back(InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "transition", initials, true)); + initTrans.push_back(InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "transition", histories, true)); + + for (int i = 0; i < initTrans.size(); i++) { + Element transition = Element(initTrans[i]); + + /* In a conformant SCXML document, this transition must not contain 'cond' or 'event' attributes, and must specify a non-null 'target' + * whose value is a valid state specification consisting solely of descendants of the containing state + */ + + if (HAS_ATTR(transition, "cond")) { + issues.push_back(InterpreterIssue("Initial transition cannot have a condition", transition, InterpreterIssue::USCXML_ISSUE_FATAL)); + } + if (HAS_ATTR(transition, "event")) { + issues.push_back(InterpreterIssue("Initial transition cannot be eventful", transition, InterpreterIssue::USCXML_ISSUE_FATAL)); + } + + if (!transition.getParentNode() || !transition.getParentNode().getParentNode() || transition.getParentNode().getParentNode().getNodeType() != Node_base::ELEMENT_NODE) + continue; // syntax will catch this one + Element state(transition.getParentNode().getParentNode()); + if (!InterpreterImpl::isState(state)) + continue; // syntax will catch this one + + NodeSet childs; + childs.push_back(InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "state", state, true)); + childs.push_back(InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "parallel", state, true)); + childs.push_back(InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "final", state, true)); + childs.push_back(InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "history", state, true)); + + std::list intials = InterpreterImpl::tokenizeIdRefs(ATTR(transition, "target")); + for (std::list::iterator initIter = intials.begin(); initIter != intials.end(); initIter++) { + // the 'target' of a inside an or element: all the states must be descendants of the containing or element + if (!InterpreterImpl::isMember(seenStates[*initIter], childs)) { + issues.push_back(InterpreterIssue("Target of initial transition references non-child state '" + *initIter + "'", transition, InterpreterIssue::USCXML_ISSUE_FATAL)); + } + } + } + } + // check that all invokers exists { @@ -510,11 +604,24 @@ NEXT_TRANSITION: } } - // check that all SCXML elements have valid parents + // check that all SCXML elements have valid parents and required attributes { for (int i = 0; i < allElements.size(); i++) { Element element = Element(allElements[i]); std::string localName = LOCALNAME(element); + + if (reqAttr.find(localName) != reqAttr.end()) { + for (std::set::const_iterator reqIter = reqAttr[localName].begin(); + reqIter != reqAttr[localName].end(); reqIter++) { + if (!HAS_ATTR(element, *reqIter)) { + issues.push_back(InterpreterIssue("Element " + localName + " is missing required attribute '" + *reqIter + "'", element, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + } + } + + if (localName == "scxml") // can be anywhere: , , + continue; + if (!element.getParentNode() || element.getParentNode().getNodeType() != Node_base::ELEMENT_NODE) { issues.push_back(InterpreterIssue("Parent of " + localName + " is no element", element, InterpreterIssue::USCXML_ISSUE_WARNING)); continue; @@ -530,6 +637,103 @@ NEXT_TRANSITION: } } + // check attribute constraints + { + for (int i = 0; i < initials.size(); i++) { + Element initial = Element(initials[i]); + if (initial.getParentNode() && initial.getParentNode().getNodeType() == Node_base::ELEMENT_NODE) { + Element state(initial.getParentNode()); + if (HAS_ATTR(state, "initial")) { + issues.push_back(InterpreterIssue("State with initial attribute cannot have child ", state, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + if (InterpreterImpl::isAtomic(state)) { + issues.push_back(InterpreterIssue("Atomic state cannot have child ", state, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + } + } + for (int i = 0; i < allStates.size(); i++) { + Element state = Element(allStates[i]); + if (InterpreterImpl::isAtomic(state) && HAS_ATTR(state, "initial")) { + issues.push_back(InterpreterIssue("Atomic state cannot have initial attribute ", state, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + } + + for (int i = 0; i < assigns.size(); i++) { + Element assign = Element(assigns[i]); + if (HAS_ATTR(assign, "expr") && assign.getChildNodes().getLength() > 0) { + issues.push_back(InterpreterIssue("Assign element cannot have expr attribute and children", assign, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + } + + for (int i = 0; i < contents.size(); i++) { + Element content = Element(contents[i]); + if (HAS_ATTR(content, "expr") && content.getChildNodes().getLength() > 0) { + issues.push_back(InterpreterIssue("Content element cannot have expr attribute and children", content, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + } + + for (int i = 0; i < params.size(); i++) { + Element param = Element(params[i]); + if (HAS_ATTR(param, "expr") && HAS_ATTR(param, "location")) { + issues.push_back(InterpreterIssue("Param element cannot have both expr and location attribute", param, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + } + + for (int i = 0; i < scripts.size(); i++) { + Element script = Element(scripts[i]); + if (HAS_ATTR(script, "src") && script.getChildNodes().getLength() > 0) { + issues.push_back(InterpreterIssue("Script element cannot have src attribute and children", script, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + } + + for (int i = 0; i < sends.size(); i++) { + Element send = Element(sends[i]); + if (HAS_ATTR(send, "event") && HAS_ATTR(send, "eventexpr")) { + issues.push_back(InterpreterIssue("Send element cannot have both event and eventexpr attribute", send, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + if (HAS_ATTR(send, "target") && HAS_ATTR(send, "targetexpr")) { + issues.push_back(InterpreterIssue("Send element cannot have both target and targetexpr attribute", send, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + if (HAS_ATTR(send, "type") && HAS_ATTR(send, "typeexpr")) { + issues.push_back(InterpreterIssue("Send element cannot have both type and typeexpr attribute", send, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + if (HAS_ATTR(send, "id") && HAS_ATTR(send, "idlocation")) { + issues.push_back(InterpreterIssue("Send element cannot have both id and idlocation attribute", send, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + if (HAS_ATTR(send, "delay") && HAS_ATTR(send, "delayexpr")) { + issues.push_back(InterpreterIssue("Send element cannot have both delay and delayexpr attribute", send, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + if (HAS_ATTR(send, "delay") && HAS_ATTR(send, "target") && ATTR(send, "target")== "_internal") { + issues.push_back(InterpreterIssue("Send element cannot have delay with target _internal", send, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + if (HAS_ATTR(send, "namelist") && InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "content", send, false).size() > 0) { + issues.push_back(InterpreterIssue("Send element cannot have namelist attribute and content child", send, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + } + for (int i = 0; i < cancels.size(); i++) { + Element cancel = Element(cancels[i]); + if (HAS_ATTR(cancel, "sendid") && HAS_ATTR(cancel, "sendidexpr")) { + issues.push_back(InterpreterIssue("Cancel element cannot have both sendid and eventexpr sendidexpr", cancel, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + } + + for (int i = 0; i < invokes.size(); i++) { + Element invoke = Element(invokes[i]); + if (HAS_ATTR(invoke, "type") && HAS_ATTR(invoke, "typeexpr")) { + issues.push_back(InterpreterIssue("Invoke element cannot have both type and typeexpr attribute", invoke, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + if (HAS_ATTR(invoke, "src") && HAS_ATTR(invoke, "srcexpr")) { + issues.push_back(InterpreterIssue("Invoke element cannot have both src and srcexpr attribute", invoke, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + if (HAS_ATTR(invoke, "id") && HAS_ATTR(invoke, "idlocation")) { + issues.push_back(InterpreterIssue("Invoke element cannot have both id and idlocation attribute", invoke, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + if (HAS_ATTR(invoke, "namelist") && InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "param", invoke, false).size() > 0) { + issues.push_back(InterpreterIssue("Invoke element cannot have namelist attribute and param child", invoke, InterpreterIssue::USCXML_ISSUE_WARNING)); + } + } + + } // check that the datamodel is known if not already instantiated if (!interpreter->_dataModel) { diff --git a/src/uscxml/server/HTTPServer.cpp b/src/uscxml/server/HTTPServer.cpp index 37be5a9..f6c1f2e 100644 --- a/src/uscxml/server/HTTPServer.cpp +++ b/src/uscxml/server/HTTPServer.cpp @@ -100,7 +100,7 @@ HTTPServer::HTTPServer(unsigned short port, unsigned short wsPort, SSLConfig* ss if (_port > 0) { _httpHandle = evhttp_bind_socket_with_handle(_http, INADDR_ANY, _port); if (_httpHandle) { - LOG(INFO) << "HTTP server listening on tcp/" << _port; + DLOG(INFO) << "HTTP server listening on tcp/" << _port; } else { LOG(ERROR) << "HTTP server cannot bind to tcp/" << _port; } @@ -110,7 +110,7 @@ HTTPServer::HTTPServer(unsigned short port, unsigned short wsPort, SSLConfig* ss if (_wsPort > 0) { _wsHandle = evws_bind_socket(_evws, _wsPort); if (_wsHandle) { - LOG(INFO) << "WebSocket server listening on tcp/" << _wsPort; + DLOG(INFO) << "WebSocket server listening on tcp/" << _wsPort; } else { LOG(ERROR) << "WebSocket server cannot bind to tcp/" << _wsPort; } diff --git a/src/uscxml/transform/ChartToFSM.cpp b/src/uscxml/transform/ChartToFSM.cpp index 971ee10..ef59d84 100644 --- a/src/uscxml/transform/ChartToFSM.cpp +++ b/src/uscxml/transform/ChartToFSM.cpp @@ -21,6 +21,7 @@ #include "uscxml/transform/FlatStateIdentifier.h" #include "uscxml/Convenience.h" #include "uscxml/Factory.h" +#include "uscxml/debug/Complexity.h" #include #include @@ -91,171 +92,6 @@ for (int i = 0; i < contents.size(); i++) { \ } \ std::cerr << ")"; -std::list > > Complexity::getAllConfigurations(const Arabica::DOM::Element& root) { - - std::list > > allConfigurations; - std::string nsPrefix = (root.getPrefix().size() > 0 ? root.getPrefix() + ":" : ""); - std::string localName = root.getLocalName(); - bool isAtomic = true; - - NodeList children = root.getChildNodes(); - for (int i = 0; i < children.getLength(); i++) { - if (children.item(i).getNodeType() != Node_base::ELEMENT_NODE) - continue; - Element childElem(children.item(i)); - if (childElem.getTagName() == nsPrefix + "state" || - childElem.getTagName() == nsPrefix + "parallel" || - childElem.getTagName() == nsPrefix + "final") { - // nested child state - std::list > > nestedConfigurations = getAllConfigurations(childElem); - isAtomic = false; - if (localName == "parallel" && allConfigurations.size() > 0) { - // for every nested configuration, every new nested is valid - std::list > > combinedConfigurations; - for (std::list > >::iterator existIter = allConfigurations.begin(); existIter != allConfigurations.end(); existIter++) { - std::set > existingConfig = *existIter; - - for (std::list > >::iterator newIter = nestedConfigurations.begin(); newIter != nestedConfigurations.end(); newIter++) { - - std::set > newConfig = *newIter; - std::set > combinedSet; - combinedSet.insert(existingConfig.begin(), existingConfig.end()); - combinedSet.insert(newConfig.begin(), newConfig.end()); - - combinedConfigurations.push_back(combinedSet); - } - } - allConfigurations = combinedConfigurations; - } else { - // just add nested configurations and this - for (std::list > >::iterator newIter = nestedConfigurations.begin(); newIter != nestedConfigurations.end(); newIter++) { - std::set > newConfig = *newIter; - if (localName != "scxml") - newConfig.insert(root); - allConfigurations.push_back(newConfig); - } - } - } - } - - if (isAtomic) { - std::set > soleConfig; - soleConfig.insert(root); - allConfigurations.push_back(soleConfig); - } - return allConfigurations; -} - -std::map Complexity::getTransitionHistogramm(const Arabica::DOM::Element& root) { - std::map histogram; - std::string nameSpace; - - std::list > > allConfig = Complexity::getAllConfigurations(root); - - // for every legal configuration, count the transitions - for (std::list > >::iterator confIter = allConfig.begin(); confIter != allConfig.end(); confIter++) { - NodeSet configNodeSet; - std::set > config = *confIter; - for (std::set >::iterator elemIter = config.begin(); elemIter != config.end(); elemIter++) { - configNodeSet.push_back(*elemIter); - if (nameSpace.size() == 0 && elemIter->getPrefix().size() > 0) - nameSpace = elemIter->getPrefix() + ":"; - } - NodeSet transitions = InterpreterImpl::filterChildElements(nameSpace + "transition", configNodeSet); - histogram[transitions.size()]++; - } - - return histogram; -} - - -uint64_t Complexity::stateMachineComplexity(const Arabica::DOM::Element& root, Variant variant) { - Complexity complexity = calculateStateMachineComplexity(root); - uint64_t value = complexity.value; - - if (variant != IGNORE_HISTORY_AND_NESTED_DATA && variant != IGNORE_HISTORY) { - for (std::list::const_iterator histIter = complexity.history.begin(); histIter != complexity.history.end(); histIter++) { - value *= *histIter; - } - } - - if (variant != IGNORE_HISTORY_AND_NESTED_DATA && variant != IGNORE_NESTED_DATA) { - bool ignoreNestedData = false; - if (root.getLocalName() == "scxml" && (!HAS_ATTR_CAST(root, "binding") || boost::to_lower_copy(ATTR_CAST(root, "binding")) == "early")) { - ignoreNestedData = true; - } - - if (!ignoreNestedData) { - uint64_t power = complexity.nestedData; - while(power--) { - value *= 2; - } - } - } - - return value; -} - -Complexity Complexity::calculateStateMachineComplexity(const Arabica::DOM::Element& root) { - Complexity complexity; - - bool hasFlatHistory = false; - bool hasDeepHistory = false; - bool hasNestedData = false; - - Arabica::DOM::NodeList childElems = root.getChildNodes(); - for (int i = 0; i < childElems.getLength(); i++) { - if (childElems.item(i).getNodeType() != Node_base::ELEMENT_NODE) - continue; - Element childElem = Element(childElems.item(i)); - if (InterpreterImpl::isHistory(childElem)) { - if (HAS_ATTR(childElem, "type") && ATTR(childElem, "type") == "deep") { - hasDeepHistory = true; - } else { - hasFlatHistory = true; - } - } - if (!hasNestedData && childElem.getLocalName() == "datamodel") { - Arabica::DOM::NodeList dataElemChilds = childElem.getChildNodes(); - for (int j = 0; j < dataElemChilds.getLength(); j++) { - if (dataElemChilds.item(j).getLocalName() == "data") - hasNestedData = true; - } - } - } - - if (hasNestedData) - complexity.nestedData++; - - if (InterpreterImpl::isCompound(root) || TAGNAME(root) == "scxml") { - // compounds can be in any of the child state -> add - NodeSet childs = InterpreterImpl::getChildStates(root); - for (int i = 0; i < childs.size(); i++) { - complexity += calculateStateMachineComplexity(Element(childs[i])); - } - if (hasFlatHistory) { - complexity.history.push_back(childs.size()); - } - if (hasDeepHistory) { - complexity.history.push_back(complexity.value); - } - } else if (InterpreterImpl::isParallel(root)) { - // parallels are in all states -> multiply - NodeSet childs = InterpreterImpl::getChildStates(root); - complexity.value = 1; - for (int i = 0; i < childs.size(); i++) { - complexity *= calculateStateMachineComplexity(Element(childs[i])); - } - if (hasDeepHistory) { - complexity.history.push_back(complexity.value); - } - - } else if (InterpreterImpl::isAtomic(root)) { - return 1; - } - - return complexity; -} ChartToFSM::ChartToFSM(const Interpreter& other) { @@ -314,7 +150,6 @@ ChartToFSM::~ChartToFSM() { for (int i = 0; i < allTransitions.size(); i++) { _transParents.erase(allTransitions[i]); } - } Document ChartToFSM::getDocument() const { @@ -325,10 +160,6 @@ Document ChartToFSM::getDocument() const { InterpreterState ChartToFSM::interpret() { - // create a _flatDoc for the FSM - DOMImplementation domFactory = Arabica::SimpleDOM::DOMImplementation::getDOMImplementation(); - _flatDoc = domFactory.createDocument(_document.getNamespaceURI(), "", 0); - init(); setupIOProcessors(); @@ -350,9 +181,9 @@ InterpreterState ChartToFSM::interpret() { std::map histoGramm = Complexity::getTransitionHistogramm(_scxml); // abort(); - uint64_t complexity = Complexity::stateMachineComplexity(_scxml) + 1; + uint64_t complexity = Complexity::stateMachineComplexity(this) + 1; std::cerr << "Approximate Complexity: " << complexity << std::endl; - std::cerr << "Approximate Active Complexity: " << Complexity::stateMachineComplexity(_scxml, Complexity::IGNORE_HISTORY_AND_NESTED_DATA) + 1 << std::endl; + std::cerr << "Approximate Active Complexity: " << Complexity::stateMachineComplexity(this, Complexity::IGNORE_HISTORY | Complexity::IGNORE_NESTED_DATA) + 1 << std::endl; if (complexity > 1000) { _skipEventChainCalculations = true; @@ -478,6 +309,10 @@ InterpreterState ChartToFSM::interpret() { // std::cerr << _scxml << std::endl; + // create a _flatDoc for the FSM + DOMImplementation domFactory = Arabica::SimpleDOM::DOMImplementation::getDOMImplementation(); + _flatDoc = domFactory.createDocument(_document.getNamespaceURI(), "", 0); + GlobalTransition* globalTransition = new GlobalTransition(initialTransitions, _dataModel, this); globalTransition->index = _lastTransIndex++; diff --git a/src/uscxml/transform/ChartToFSM.h b/src/uscxml/transform/ChartToFSM.h index 1dc8813..9d1ed97 100644 --- a/src/uscxml/transform/ChartToFSM.h +++ b/src/uscxml/transform/ChartToFSM.h @@ -33,44 +33,6 @@ class GlobalState; class GlobalTransition; class ChartToFSM; -class USCXML_API Complexity { -public: - - enum Variant { - IGNORE_NOTHING, - IGNORE_HISTORY, - IGNORE_NESTED_DATA, - IGNORE_HISTORY_AND_NESTED_DATA, - }; - - Complexity() : value(0), nestedData(0) {} - Complexity(uint64_t value) : value(value), nestedData(0) {} - - Complexity& operator+=(const Complexity& rhs) { - value += rhs.value; - nestedData += rhs.nestedData; - history.insert(history.end(), rhs.history.begin(), rhs.history.end()); - return *this; - } - - Complexity& operator*=(const Complexity& rhs) { - value *= rhs.value; - nestedData += rhs.nestedData; - history.insert(history.end(), rhs.history.begin(), rhs.history.end()); - return *this; - } - - static uint64_t stateMachineComplexity(const Arabica::DOM::Element& root, Complexity::Variant variant = IGNORE_NOTHING); - static std::list > > getAllConfigurations(const Arabica::DOM::Element& root); - static std::map getTransitionHistogramm(const Arabica::DOM::Element& root); - -protected: - static Complexity calculateStateMachineComplexity(const Arabica::DOM::Element& root); - - uint64_t value; - uint64_t nestedData; - std::list history; -}; class USCXML_API GlobalState { public: diff --git a/src/uscxml/transform/ChartToPromela.cpp b/src/uscxml/transform/ChartToPromela.cpp index 806c1f4..867092d 100644 --- a/src/uscxml/transform/ChartToPromela.cpp +++ b/src/uscxml/transform/ChartToPromela.cpp @@ -17,6 +17,8 @@ * @endcond */ +#define NEW_DELAY_RESHUFFLE 1 + #include "uscxml/transform/ChartToFSM.h" #include "uscxml/transform/ChartToPromela.h" #include "uscxml/transform/FlatStateIdentifier.h" @@ -99,6 +101,16 @@ for (int indentIndex = start; indentIndex < cols; indentIndex++) \ } \ } +#define TRANSITION_TRACE(transList, value) \ +if (_traceTransitions) { \ +for (std::set::iterator transRefIter = transList->transitionRefs.begin(); \ + transRefIter != transList->transitionRefs.end(); \ + transRefIter++) { \ + stream << padding << _prefix << "transitions[" << *transRefIter << "] = "#value"; " << std::endl; \ + } \ +} \ + + #define DUMP_STATS(disregardTime) \ uint64_t now = tthread::chrono::system_clock::now(); \ if (now - _lastTimeStamp > 1000 || disregardTime) { \ @@ -372,6 +384,47 @@ std::string PromelaCodeAnalyzer::createMacroName(const std::string& literal) { return macroName; } +std::string PromelaCodeAnalyzer::getTypeReset(const std::string& var, const PromelaTypedef& type, const std::string padding) { + std::stringstream assignment; + + std::map::const_iterator typeIter = type.types.begin(); + while(typeIter != type.types.end()) { + const PromelaTypedef& innerType = typeIter->second; + if (innerType.arraySize > 0) { + for (int i = 0; i < innerType.arraySize; i++) { + assignment << padding << var << "." << typeIter->first << "[" << i << "] = 0;" << std::endl; + } + } else if (innerType.types.size() > 0) { + assignment << getTypeReset(var + "." + typeIter->first, typeIter->second, padding); + } else { + assignment << padding << var << "." << typeIter->first << " = 0;" << std::endl; + } + typeIter++; + } + return assignment.str(); + +} + +std::string PromelaCodeAnalyzer::getTypeAssignment(const std::string& varTo, const std::string& varFrom, const PromelaTypedef& type, const std::string padding) { + std::stringstream assignment; + + std::map::const_iterator typeIter = type.types.begin(); + while(typeIter != type.types.end()) { + const PromelaTypedef& innerType = typeIter->second; + if (innerType.arraySize > 0) { + for (int i = 0; i < innerType.arraySize; i++) { + assignment << padding << varTo << "." << typeIter->first << "[" << i << "] = " << varFrom << "." << typeIter->first << "[" << i << "];" << std::endl; + } + } else if (innerType.types.size() > 0) { + assignment << getTypeAssignment(varTo + "." + typeIter->first, varFrom + "." + typeIter->first, typeIter->second, padding); + } else { + assignment << padding << varTo << "." << typeIter->first << " = " << varFrom << "." << typeIter->first << ";" << std::endl; + } + typeIter++; + } + return assignment.str(); +} + std::string PromelaCodeAnalyzer::macroForLiteral(const std::string& literal) { if (boost::starts_with(literal, "'")) throw std::runtime_error("Literal " + literal + " passed with quotes"); @@ -617,7 +670,10 @@ void ChartToPromela::writeTypeDefs(std::ostream& stream) { if (_analyzer->usesEventField("delay")) { // make sure delay is the first member for sorted enqueuing to work stream << " int delay;" << std::endl; - stream << " int seqNr;" << std::endl; +#if NEW_DELAY_RESHUFFLE +#else + stream << " int seqNr;" << std::endl; +#endif } stream << " int name;" << std::endl; if (_analyzer->usesEventField("invokeid")) { @@ -1147,11 +1203,13 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra // stream << padding << "}" << std::endl; stream << padding << "fi;" << std::endl; } + + TRANSITION_TRACE(transition, false); - // moved up here for goto from d_step padding = padding.substr(2); - stream << padding << "}" << std::endl; + stream << padding << "}" << std::endl; + // moved up here for goto from d_step writeTransitionClosure(stream, transition, origNewState, indent-1); _perfTransProcessed++; @@ -1409,11 +1467,11 @@ void ChartToPromela::writeTransitionClosure(std::ostream& stream, GlobalTransiti padding += " "; } - if (_traceTransitions) { - for (std::set::iterator transRefIter = transition->transitionRefs.begin(); transRefIter != transition->transitionRefs.end(); transRefIter++) { - stream << padding << _prefix << "transitions[" << *transRefIter << "] = false; " << std::endl; - } - } +// if (_traceTransitions) { +// for (std::set::iterator transRefIter = transition->transitionRefs.begin(); transRefIter != transition->transitionRefs.end(); transRefIter++) { +// stream << padding << _prefix << "transitions[" << *transRefIter << "] = false; " << std::endl; +// } +// } if (state->isFinal) { stream << padding << "goto " << _prefix << "terminate;" << std::endl; @@ -1518,20 +1576,21 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: } else if(TAGNAME(nodeElem) == "send" || TAGNAME(nodeElem) == "raise") { std::string targetQueue; + std::string insertOp = "!"; if (TAGNAME(nodeElem) == "raise") { - targetQueue = _prefix + "iQ!"; + targetQueue = _prefix + "iQ"; } else if (!HAS_ATTR(nodeElem, "target")) { if (_allowEventInterleaving) { - targetQueue = _prefix + "tmpQ!"; + targetQueue = _prefix + "tmpQ"; } else { - targetQueue = _prefix + "eQ!"; + targetQueue = _prefix + "eQ"; } } else if (ATTR(nodeElem, "target").compare("#_internal") == 0) { - targetQueue = _prefix + "iQ!"; + targetQueue = _prefix + "iQ"; } else if (ATTR(nodeElem, "target").compare("#_parent") == 0) { - targetQueue = _parent->_prefix + "eQ!"; + targetQueue = _parent->_prefix + "eQ"; } else if (boost::starts_with(ATTR(nodeElem, "target"), "#_") && _machinesPerId.find(ATTR(nodeElem, "target").substr(2)) != _machinesPerId.end()) { - targetQueue = _machines[_machinesPerId[ATTR(nodeElem, "target").substr(2)]]->_prefix + "eQ!"; + targetQueue = _machines[_machinesPerId[ATTR(nodeElem, "target").substr(2)]]->_prefix + "eQ"; } if (targetQueue.length() > 0) { // this is for our external queue @@ -1544,8 +1603,8 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: } if (_analyzer->usesComplexEventStruct()) { stream << padding << "{" << std::endl; - stream << padding << " _event_t tmpE;" << std::endl; - stream << padding << " tmpE.name = " << event << ";" << std::endl; + stream << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), padding + " "); + stream << padding << " tmpE.name = " << event << ";" << std::endl; if (HAS_ATTR(nodeElem, "idlocation")) { stream << padding << " /* idlocation */" << std::endl; @@ -1564,13 +1623,16 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: stream << padding << " tmpE.invokeid = " << _analyzer->macroForLiteral(_invokerid) << ";" << std::endl; } - if (_analyzer->usesEventField("origintype") && !boost::ends_with(targetQueue, "iQ!")) { + if (_analyzer->usesEventField("origintype") && !boost::ends_with(targetQueue, "iQ")) { stream << padding << " tmpE.origintype = " << _analyzer->macroForLiteral("http://www.w3.org/TR/scxml/#SCXMLEventProcessor") << ";" << std::endl; } if (_analyzer->usesEventField("delay")) { - targetQueue += "!"; +#if NEW_DELAY_RESHUFFLE +#else + insertOp += "!"; stream << padding << " _lastSeqId = _lastSeqId + 1;" << std::endl; +#endif if (HAS_ATTR_CAST(nodeElem, "delay")) { stream << padding << " tmpE.delay = " << ATTR_CAST(nodeElem, "delay") << ";" << std::endl; } else if (HAS_ATTR_CAST(nodeElem, "delayexpr")) { @@ -1578,7 +1640,10 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: } else { stream << padding << " tmpE.delay = 0;" << std::endl; } - stream << padding << " tmpE.seqNr = _lastSeqId;" << std::endl; +#if NEW_DELAY_RESHUFFLE +#else + stream << padding << " tmpE.seqNr = _lastSeqId;" << std::endl; +#endif } if (_analyzer->usesEventField("type")) { @@ -1617,10 +1682,17 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: stream << padding << " tmpE.data = " << ADAPT_SRC(ATTR(contentElem, "expr")) << ";" << std::endl; } } - stream << padding << " " << targetQueue << "tmpE;" << std::endl; + stream << padding << " " << targetQueue << insertOp <<"tmpE;" << std::endl; + +#if NEW_DELAY_RESHUFFLE + if (_analyzer->usesEventField("delay") && !boost::ends_with(targetQueue, "iQ")) { + stream << padding << " insertWithDelay(" << targetQueue << ");" << std::endl; + } +#endif + stream << padding << "}" << std::endl; } else { - stream << padding << targetQueue << event << ";" << std::endl; + stream << padding << targetQueue << insertOp << event << ";" << std::endl; } } } else if(TAGNAME(nodeElem) == "cancel") { @@ -1961,7 +2033,10 @@ void ChartToPromela::writeDeclarations(std::ostream& stream) { } if (_analyzer->usesEventField("delay")) { +#if NEW_DELAY_RESHUFFLE +#else stream << "hidden int _lastSeqId = 0; /* sequential counter for delayed events */" << std::endl; +#endif } } // if (_analyzer->usesPlatformVars()) { @@ -2107,10 +2182,12 @@ void ChartToPromela::writeFSM(std::ostream& stream) { NodeSet transitions; stream << "proctype " << (_prefix.size() == 0 ? "machine_" : _prefix) << "run() {" << std::endl; - stream << " " << _prefix << "done = false;" << std::endl; - stream << " " << _prefix << "canceled = false;" << std::endl; - stream << " " << _prefix << "spontaneous = true;" << std::endl; - stream << " " << _prefix << "procid = _pid;" << std::endl; + stream << " d_step {" << std::endl; + stream << " " << _prefix << "done = false;" << std::endl; + stream << " " << _prefix << "canceled = false;" << std::endl; + stream << " " << _prefix << "spontaneous = true;" << std::endl; + stream << " " << _prefix << "procid = _pid;" << std::endl; + stream << " }" << std::endl; // write initial transition // transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", _startState); // assert(transitions.size() == 1); @@ -2160,8 +2237,12 @@ void ChartToPromela::writeFSM(std::ostream& stream) { stream << " /* push send events to external queue - this needs to be interleavable! */" << std::endl; stream << " do" << std::endl; if (_analyzer->usesEventField("delay")) { - stream << " :: len(" << _prefix << "tmpQ) != 0 -> { " << _prefix << "tmpQ?" << _prefix << "_event; " << _prefix << "eQ!!" << _prefix << "_event }" << std::endl; - } else { +#if NEW_DELAY_RESHUFFLE + stream << " :: len(" << _prefix << "tmpQ) != 0 -> { " << _prefix << "tmpQ?" << _prefix << "_event; " << _prefix << "eQ!" << _prefix << "_event; insertWithDelay(" << _prefix << "eQ); }" << std::endl; +#else + stream << " :: len(" << _prefix << "tmpQ) != 0 -> { " << _prefix << "tmpQ?" << _prefix << "_event; " << _prefix << "eQ!!" << _prefix << "_event }" << std::endl; +#endif + } else { stream << " :: len(" << _prefix << "tmpQ) != 0 -> { " << _prefix << "tmpQ?" << _prefix << "_event; " << _prefix << "eQ!" << _prefix << "_event }" << std::endl; } stream << " :: else -> break;" << std::endl; @@ -2326,7 +2407,11 @@ void ChartToPromela::writeFSM(std::ostream& stream) { stream << " if" << std::endl; stream << " :: " << invIter->second->_prefix << "done -> skip;" << std::endl; stream << " :: " << invIter->second->_prefix << "canceled -> skip;" << std::endl; - stream << " :: else -> { " << invIter->second->_prefix << "eQ!!" << _prefix << "_event" << " }" << std::endl; +#if NEW_DELAY_RESHUFFLE + stream << " :: else -> { " << invIter->second->_prefix << "eQ!" << _prefix << "_event" << "; insertWithDelay(" << invIter->second->_prefix << "eQ" << "); }" << std::endl; +#else + stream << " :: else -> { " << invIter->second->_prefix << "eQ!!" << _prefix << "_event" << " }" << std::endl; +#endif stream << " fi;" << std::endl << std::endl; } @@ -2347,16 +2432,22 @@ void ChartToPromela::writeFSM(std::ostream& stream) { if (_parent != NULL) { stream << " {" << std::endl; - stream << " _event_t tmpE;" << std::endl; + stream << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), " "); stream << " tmpE.name = " << _analyzer->macroForLiteral("done.invoke." + _invokerid) << ";" << std::endl; if (_invokerid.length() > 0) { stream << " tmpE.invokeid = " << _analyzer->macroForLiteral(_invokerid) << ";" << std::endl; } if (_analyzer->usesEventField("delay")) { - stream << " _lastSeqId = _lastSeqId + 1;" << std::endl; - stream << " tmpE.seqNr = _lastSeqId;" << std::endl; - stream << " " << _parent->_prefix << "eQ!!tmpE;" << std::endl; - } else { +#if NEW_DELAY_RESHUFFLE + stream << " " << _parent->_prefix << "eQ!tmpE;" << std::endl; + stream << " insertWithDelay(" << _parent->_prefix << "eQ);" << std::endl; + +#else + stream << " _lastSeqId = _lastSeqId + 1;" << std::endl; + stream << " tmpE.seqNr = _lastSeqId;" << std::endl; + stream << " " << _parent->_prefix << "eQ!!tmpE;" << std::endl; +#endif + } else { stream << " " << _parent->_prefix << "eQ!tmpE;" << std::endl; } stream << " }" << std::endl; @@ -2380,7 +2471,7 @@ void ChartToPromela::writeRescheduleProcess(std::ostream& stream, int indent) { } else { stream << padding << "inline rescheduleProcess(smallestDelay, procId, internalQ, externalQ) {" << std::endl; } - stream << padding << " _event_t tmpE;" << std::endl; +// stream << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), " "); stream << padding << " set_priority(procId, 1);" << std::endl; stream << padding << " if" << std::endl; @@ -2420,7 +2511,7 @@ void ChartToPromela::writeDetermineShortestDelay(std::ostream& stream, int inden } stream << padding << "inline determineSmallestDelay(smallestDelay, queue) {" << std::endl; - stream << padding << " _event_t tmpE;" << std::endl; +// stream << padding << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), " "); stream << padding << " if" << std::endl; stream << padding << " :: len(queue) > 0 -> {" << std::endl; stream << padding << " queue?;" << std::endl; @@ -2434,6 +2525,100 @@ void ChartToPromela::writeDetermineShortestDelay(std::ostream& stream, int inden stream << padding << "}" << std::endl; } +void ChartToPromela::writeInsertWithDelay(std::ostream& stream, int indent) { + std::string padding; + for (int i = 0; i < indent; i++) { + padding += " "; + } + + uint32_t maxExternalQueueLength = 1; + std::map, ChartToPromela*>::iterator machineIter = _machinesAll->begin(); + while(machineIter != _machinesAll->end()) { + maxExternalQueueLength = std::max(maxExternalQueueLength, machineIter->second->_externalQueueLength); + machineIter++; + } + + maxExternalQueueLength += 6; + + if (maxExternalQueueLength <= 1) { + stream << padding << "/* noop for external queues with length <= 1 */" << std::endl; + stream << padding << "inline insertWithDelay(queue) {}" << std::endl; + } + + stream << padding << "hidden _event_t _iwdQ[" << maxExternalQueueLength - 1 << "];" << std::endl; + stream << padding << "hidden int _iwdQLength = 0;" << std::endl; + stream << padding << "hidden int _iwdIdx1 = 0;" << std::endl; + stream << padding << "hidden int _iwdIdx2 = 0;" << std::endl; + stream << padding << "hidden _event_t _iwdTmpE;" << std::endl; + stream << padding << "hidden _event_t _iwdLastE;" << std::endl; + stream << padding << "bool _iwdInserted = false;" << std::endl; + stream << padding << "" << std::endl; + stream << padding << "/* last event in given queue is potentially at wrong position */" << std::endl; + stream << padding << "inline insertWithDelay(queue) {" << std::endl; + stream << padding << " d_step {" << std::endl; + stream << padding << "" << std::endl; + stream << padding << " /* only process for non-trivial queues */" << std::endl; + stream << padding << " if" << std::endl; + stream << padding << " :: len(queue) > 1 -> {" << std::endl; + stream << padding << "" << std::endl; + stream << padding << " /* move all events but last over and remember the last one */" << std::endl; + stream << padding << " _iwdIdx1 = 0;" << std::endl; + stream << padding << " _iwdQLength = len(queue) - 1;" << std::endl; + stream << padding << "" << std::endl; + stream << padding << " do" << std::endl; + stream << padding << " :: _iwdIdx1 < _iwdQLength -> {" << std::endl; + stream << padding << " queue?_iwdTmpE;" << std::endl; + stream << padding << " _iwdQ[_iwdIdx1].name = _iwdTmpE.name;" << std::endl; + + stream << _analyzer->getTypeAssignment("_iwdQ[_iwdIdx1]", "_iwdTmpE", _analyzer->getType("_event"), padding + " "); + + stream << padding << " _iwdIdx1++;" << std::endl; + stream << padding << " }" << std::endl; + stream << padding << " :: else -> break;" << std::endl; + stream << padding << " od" << std::endl; + stream << padding << "" << std::endl; + stream << padding << " queue?_iwdLastE;" << std::endl; + stream << padding << "" << std::endl; + stream << padding << " /* _iwdQ now contains all but last item in _iwdLastE */" << std::endl; + stream << padding << " assert(len(queue) == 0);" << std::endl; + stream << padding << "" << std::endl; + stream << padding << " /* reinsert into queue and place _iwdLastE correctly */" << std::endl; + stream << padding << " _iwdInserted = false;" << std::endl; + stream << padding << " _iwdIdx2 = 0;" << std::endl; + stream << padding << "" << std::endl; + stream << padding << " do" << std::endl; + stream << padding << " :: _iwdIdx2 < _iwdIdx1 -> {" << std::endl; + stream << padding << " _iwdTmpE.name = _iwdQ[_iwdIdx2].name;" << std::endl; + + stream << _analyzer->getTypeAssignment("_iwdTmpE", "_iwdQ[_iwdIdx2]", _analyzer->getType("_event"), padding + " "); + + stream << padding << "" << std::endl; + stream << padding << " if" << std::endl; + stream << padding << " :: _iwdTmpE.delay > _iwdLastE.delay -> {" << std::endl; + stream << padding << " queue!_iwdLastE;" << std::endl; + stream << padding << " _iwdInserted = true;" << std::endl; + stream << padding << " }" << std::endl; + stream << padding << " :: else -> skip" << std::endl; + stream << padding << " fi;" << std::endl; + stream << padding << "" << std::endl; + stream << padding << " queue!_iwdTmpE;" << std::endl; + stream << padding << " _iwdIdx2++;" << std::endl; + stream << padding << " }" << std::endl; + stream << padding << " :: else -> break;" << std::endl; + stream << padding << " od" << std::endl; + stream << padding << "" << std::endl; + stream << padding << " if" << std::endl; + stream << padding << " :: !_iwdInserted -> queue!_iwdLastE;" << std::endl; + stream << padding << " :: else -> skip;" << std::endl; + stream << padding << " fi;" << std::endl; + stream << padding << "" << std::endl; + stream << padding << " }" << std::endl; + stream << padding << " :: else -> skip;" << std::endl; + stream << padding << " fi;" << std::endl; + stream << padding << " }" << std::endl; + stream << padding << "}" << std::endl; +} + void ChartToPromela::writeAdvanceTime(std::ostream& stream, int indent) { std::string padding; for (int i = 0; i < indent; i++) { @@ -2441,8 +2626,7 @@ void ChartToPromela::writeAdvanceTime(std::ostream& stream, int indent) { } stream << padding << "inline advanceTime(increment, queue) {" << std::endl; - stream << padding << " int tmpIndex = 0;" << std::endl; - stream << padding << " _event_t tmpE;" << std::endl; + stream << padding << " tmpIndex = 0;" << std::endl; stream << padding << " do" << std::endl; stream << padding << " :: tmpIndex < len(queue) -> {" << std::endl; stream << padding << " queue?tmpE;" << std::endl; @@ -2474,8 +2658,8 @@ void ChartToPromela::writeRemovePendingEventsFromInvoker(std::ostream& stream, i stream << std::endl; stream << "inline removePendingEventsForInvokerOnQueue(invokeIdentifier, queue) {" << std::endl; - stream << " int tmpIndex = 0;" << std::endl; - stream << " _event_t tmpE;" << std::endl; + stream << " tmpIndex = 0;" << std::endl; +// stream << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), " "); stream << " do" << std::endl; stream << " :: tmpIndex < len(queue) -> {" << std::endl; stream << " queue?tmpE;" << std::endl; @@ -2507,8 +2691,8 @@ void ChartToPromela::writeCancelEvents(std::ostream& stream, int indent) { stream << "inline cancelSendIdOnQueue(sendIdentifier, queue, invokerIdentifier) {" << std::endl; - stream << " int tmpIndex = 0;" << std::endl; - stream << " _event_t tmpE;" << std::endl; + stream << " tmpIndex = 0;" << std::endl; +// stream << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), " "); stream << " do" << std::endl; stream << " :: tmpIndex < len(queue) -> {" << std::endl; stream << " queue?tmpE;" << std::endl; @@ -2709,6 +2893,7 @@ void ChartToPromela::writeDispatchingBlock(std::ostream& stream, std::listactiveIndex << ";" << std::endl; + TRANSITION_TRACE(currTrans, false); writeTransitionClosure(stream, currTrans, newState, indent + 1); stream << padding << "}" << std::endl; } @@ -2979,7 +3164,10 @@ void ChartToPromela::initNodes() { for (int i = 0; i < sends.size(); i++) { if (HAS_ATTR_CAST(sends[i], "delay") || HAS_ATTR_CAST(sends[i], "delayexpr")) { _analyzer->addCode("_event.delay", this); - _analyzer->addCode("_event.seqNr", this); +#if NEW_DELAY_RESHUFFLE +#else + _analyzer->addCode("_event.seqNr", this); +#endif } } } @@ -3287,9 +3475,23 @@ void ChartToPromela::writeProgram(std::ostream& stream) { stream << std::endl << "/* global inline functions */" << std::endl; + if (_analyzer->usesComplexEventStruct()) { + stream << "hidden _event_t tmpE;" << std::endl; + } else { + stream << "hidden int tmpE;" << std::endl; + } + stream << "hidden int tmpIndex;" << std::endl; + + +#if NEW_DELAY_RESHUFFLE + if (_analyzer->usesEventField("delay")) { + writeInsertWithDelay(stream); + stream << std::endl; + } +#endif if (_analyzer->usesEventField("delay") && _machines.size() > 0) { - writeDetermineShortestDelay(stream); + writeDetermineShortestDelay(stream); stream << std::endl; writeAdvanceTime(stream); stream << std::endl; diff --git a/src/uscxml/transform/ChartToPromela.h b/src/uscxml/transform/ChartToPromela.h index 1b0b16d..9c3c99b 100644 --- a/src/uscxml/transform/ChartToPromela.h +++ b/src/uscxml/transform/ChartToPromela.h @@ -205,6 +205,9 @@ public: return false; } + std::string getTypeAssignment(const std::string& varTo, const std::string& varFrom, const PromelaTypedef& type, const std::string padding = ""); + std::string getTypeReset(const std::string& var, const PromelaTypedef& type, const std::string padding = ""); + bool usesInPredicate() { return _usesInPredicate; } @@ -248,6 +251,10 @@ public: return _typeDefs; } + PromelaTypedef& getType(const std::string& typeName) { + return _typeDefs.types.at(typeName); + } + protected: std::string createMacroName(const std::string& literal); int enumerateLiteral(const std::string& literal, int forceIndex = -1); @@ -372,7 +379,8 @@ protected: //void writeRemovePendingEventsFromInvoker(std::ostream& stream, ChartToPromela* invoker, int indent = 0, bool atomic = true); void writeDetermineShortestDelay(std::ostream& stream, int indent = 0); - void writeAdvanceTime(std::ostream& stream, int indent = 0); + void writeInsertWithDelay(std::ostream& stream, int indent = 0); + void writeAdvanceTime(std::ostream& stream, int indent = 0); void writeRescheduleProcess(std::ostream& stream, int indent = 0); void writeScheduleMachines(std::ostream& stream, int indent = 0); void writeCancelEvents(std::ostream& stream, int indent = 0); diff --git a/src/uscxml/transform/Transformer.h b/src/uscxml/transform/Transformer.h index 8ea19d9..313bfaa 100644 --- a/src/uscxml/transform/Transformer.h +++ b/src/uscxml/transform/Transformer.h @@ -36,7 +36,7 @@ public: }; -class USCXML_API Transformer { +class USCXML_API Transformer : public boost::enable_shared_from_this { public: // Transformer(const Interpreter& source) { _impl = new (source) } @@ -69,6 +69,10 @@ public: return _impl->operator Interpreter(); } + boost::shared_ptr getImpl() { + return _impl; + } + protected: boost::shared_ptr _impl; diff --git a/test/src/test-issue-reporting.cpp b/test/src/test-issue-reporting.cpp index 98c2a21..e93ba58 100644 --- a/test/src/test-issue-reporting.cpp +++ b/test/src/test-issue-reporting.cpp @@ -6,7 +6,12 @@ using namespace uscxml; std::set issueLocationsForXML(const std::string xml) { Interpreter interpreter = Interpreter::fromXML(xml, ""); - std::list issues = interpreter.validate(); + + // common xmlns and version requirement on scxml attribute + interpreter.getDocument().getDocumentElement().setAttribute("xmlns", "http://www.w3.org/2005/07/scxml"); + interpreter.getDocument().getDocumentElement().setAttribute("version", "1.0"); + + std::list issues = interpreter.validate(); std::set issueLocations; @@ -61,7 +66,7 @@ int main(int argc, char** argv) { } if (1) { - // Unreachable states + // Unreachable states 1 const char* xml = "" @@ -82,7 +87,6 @@ int main(int argc, char** argv) { if (1) { // Invalid parents - const char* xml = "" " " @@ -97,6 +101,7 @@ int main(int argc, char** argv) { if (1) { // State has no 'id' attribute + // *** This is not actually an error! *** const char* xml = "" " " @@ -137,7 +142,108 @@ int main(int argc, char** argv) { assert(issueLocations.size() == 1); } - + if (1) { + // Useless history 1 + + const char* xml = + "" + " " + " " + " " + " " + " " + " " + " " + ""; + + std::set issueLocations = issueLocationsForXML(xml); + assert(issueLocations.find("//history[@id=\"bar\"]") != issueLocations.end()); + assert(issueLocations.size() == 1); + } + + if (1) { + // Useless history 2 + + const char* xml = + "" + " " + " " + " " + " " + " " + " " + " " + " " + ""; + + std::set issueLocations = issueLocationsForXML(xml); + assert(issueLocations.find("//history[@id=\"bar\"]") != issueLocations.end()); + assert(issueLocations.size() == 1); + } + + if (1) { + // No legal completion + + const char* xml = + "" + " " + " " + " " + " " + " " + ""; + + std::set issueLocations = issueLocationsForXML(xml); + assert(issueLocations.find("//state[@id=\"start\"]") != issueLocations.end()); + assert(issueLocations.find("//state[@id=\"start\"]/transition[1]") != issueLocations.end()); + assert(issueLocations.size() == 2); + } + + if (1) { + // attribute constraints + + { + // initial attribute and child + const char* xml = + "" + " " + " " + " " + " " + ""; + + std::set issueLocations = issueLocationsForXML(xml); + assert(issueLocations.find("//state[@id=\"start\"]") != issueLocations.end()); + assert(issueLocations.size() == 1); + } + { + // initial attribute with atomic state + const char* xml = + "" + " " + ""; + + std::set issueLocations = issueLocationsForXML(xml); + assert(issueLocations.find("//state[@id=\"start\"]") != issueLocations.end()); + assert(issueLocations.size() == 1); + } + { + // initial child with atomic state + const char* xml = + "" + " " + " " + " " + ""; + + std::set issueLocations = issueLocationsForXML(xml); + assert(issueLocations.find("//state[@id=\"start\"]") != issueLocations.end()); + assert(issueLocations.size() == 1); + + } + } + + if (1) { // Transition can never be optimally enabled (conditionless, eventless) @@ -185,21 +291,120 @@ int main(int argc, char** argv) { assert(issueLocations.size() == 1); } - if (1) { - // Invoke with unknown type + if (1) { + // Initial attribute with target outside of children + + const char* xml = + "" + " " + " " + " " + " " + ""; + + std::set issueLocations = issueLocationsForXML(xml); + assert(issueLocations.find("//state[@id=\"start\"]") != issueLocations.end()); + assert(issueLocations.size() == 1); + } + + if (1) { + // Initial transition with target outside of children + + const char* xml = + "" + " " + " " + " " + " " + " " + " " + " " + ""; + + std::set issueLocations = issueLocationsForXML(xml); + assert(issueLocations.find("//state[@id=\"start\"]/initial[1]/transition[1]") != issueLocations.end()); + assert(issueLocations.size() == 1); + } + + if (1) { + // Initial history transition with target outside of children + + const char* xml = + "" + " " + " " + " " + " " + " " + " " + " " + " " + " " + " " + ""; + + std::set issueLocations = issueLocationsForXML(xml); + assert(issueLocations.find("//history[@id=\"bar\"]/transition[1]") != issueLocations.end()); + assert(issueLocations.size() == 1); + } + + if (1) { + // Initial transition with target outside of children + + const char* xml = + "" + " " + " " + " " + " " + " " + " " + " " + ""; + + std::set issueLocations = issueLocationsForXML(xml); + assert(issueLocations.find("//state[@id=\"start\"]/initial[1]/transition[1]") != issueLocations.end()); + assert(issueLocations.size() == 1); + } - const char* xml = - "" - " " - " " - " " - ""; + if (1) { + // Initial transition with event + const char* xml = + "" + " " + " " + " " + " " + " " + " " + " " + " " + ""; std::set issueLocations = issueLocationsForXML(xml); - assert(issueLocations.find("//state[@id=\"start\"]/invoke[1]") != issueLocations.end()); + assert(issueLocations.find("//state[@id=\"start\"]/initial[1]/transition[1]") != issueLocations.end()); assert(issueLocations.size() == 1); } + if (1) { + // Initial transition with condition + const char* xml = + "" + " " + " " + " " + " " + " " + " " + " " + " " + ""; + + std::set issueLocations = issueLocationsForXML(xml); + assert(issueLocations.find("//state[@id=\"start\"]/initial[1]/transition[1]") != issueLocations.end()); + assert(issueLocations.size() == 1); + } + if (1) { // Send to unknown IO Processor diff --git a/test/w3c/analyze_tests.pl b/test/w3c/analyze_tests.pl index a14c129..b891066 100755 --- a/test/w3c/analyze_tests.pl +++ b/test/w3c/analyze_tests.pl @@ -30,6 +30,8 @@ if (!$testResultFile) { $testResultFile = File::Spec->catfile($toBaseDir, "../../build/cli/Testing/Temporary/LastTest.log"); } +print STDERR "Using log file from:\n\t$testResultFile\n"; + open(FILE, $testResultFile) or die $!; mkdir($outDir) or die($!) if (! -d $outDir); @@ -78,8 +80,8 @@ while ($block = ) { \\n Test\stime\s\=\s+([\d\.]+)\s(\w+) /x ) { - $test->{$currTest}->{'duration'} = $1; - $test->{$currTest}->{'durationUnit'} = $2; + $test->{$currTest}->{'duration'}->{'total'} = $1; + $test->{$currTest}->{'duration'}->{'totalUnit'} = $2; # next; - no next as this is part of the actual test output we need to scan below } @@ -174,6 +176,53 @@ while ($block = ) { $test->{$currTest}->{'pml'}->{'memory'}->{'total'} = $7; } + if ($block =~ + / + pan:\selapsed\stime\s(.*)\sseconds\n + /x ) { + $test->{$currTest}->{'pml'}->{'duration'} = $1; + } + + if ($block =~ + / + real\s+([\d\.]+)\n + user\s+([\d\.]+)\n + sys\s+([\d\.]+)\n + --\stime\sfor\stransforming\sto\spromela\n + /x ) { + $test->{$currTest}->{'duration'}->{'toPML'} = $1; + } + + if ($block =~ + / + real\s+([\d\.]+)\n + user\s+([\d\.]+)\n + sys\s+([\d\.]+)\n + --\stime\sfor\stransforming\sto\sc\n + /x ) { + $test->{$currTest}->{'duration'}->{'toC'} = $1; + } + + if ($block =~ + / + real\s+([\d\.]+)\n + user\s+([\d\.]+)\n + sys\s+([\d\.]+)\n + --\stime\sfor\stransforming\sto\sbinary\n + /x ) { + $test->{$currTest}->{'duration'}->{'toBin'} = $1; + } + + if ($block =~ + / + real\s+([\d\.]+)\n + user\s+([\d\.]+)\n + sys\s+([\d\.]+)\n + --\stime\sfor\sverification\n + /x ) { + $test->{$currTest}->{'duration'}->{'toVerif'} = $1; + } + next; } diff --git a/test/w3c/run_promela_test.cmake b/test/w3c/run_promela_test.cmake index e6d2418..b403b7a 100644 --- a/test/w3c/run_promela_test.cmake +++ b/test/w3c/run_promela_test.cmake @@ -6,25 +6,33 @@ execute_process(COMMAND ${CMAKE_COMMAND} -E make_directory ${OUTDIR}) set(ENV{USCXML_PROMELA_TRANSITION_TRACE} "TRUE") set(ENV{USCXML_PROMELA_TRANSITION_DEBUG} "TRUE") -execute_process(COMMAND ${USCXML_TRANSFORM_BIN} -tpml -i ${TESTFILE} -o ${OUTDIR}/${TEST_FILE_NAME}.pml RESULT_VARIABLE CMD_RESULT) +message(STATUS "${USCXML_TRANSFORM_BIN} -tpml -i ${TESTFILE} -o ${OUTDIR}/${TEST_FILE_NAME}.pml") +execute_process(COMMAND time -p ${USCXML_TRANSFORM_BIN} -tpml -i ${TESTFILE} -o ${OUTDIR}/${TEST_FILE_NAME}.pml RESULT_VARIABLE CMD_RESULT) if(CMD_RESULT) message(FATAL_ERROR "Error running ${USCXML_TRANSFORM_BIN}: ${CMD_RESULT}") endif() +message(STATUS "time for transforming to promela") -execute_process(COMMAND ${SPIN_BIN} -a ${OUTDIR}/${TEST_FILE_NAME}.pml WORKING_DIRECTORY ${OUTDIR} RESULT_VARIABLE CMD_RESULT) +message(STATUS "${SPIN_BIN} -a ${OUTDIR}/${TEST_FILE_NAME}.pml") +execute_process(COMMAND time -p ${SPIN_BIN} -a ${OUTDIR}/${TEST_FILE_NAME}.pml WORKING_DIRECTORY ${OUTDIR} RESULT_VARIABLE CMD_RESULT) if(CMD_RESULT) message(FATAL_ERROR "Error running spin ${SPIN_BIN}: ${CMD_RESULT}") endif() +message(STATUS "time for transforming to c") -execute_process(COMMAND ${GCC_BIN} -DMEMLIM=1024 -DVECTORSZ=8192 -O2 -DXUSAFE -w -o ${OUTDIR}/pan ${OUTDIR}/pan.c WORKING_DIRECTORY ${OUTDIR} RESULT_VARIABLE CMD_RESULT) +message(STATUS "${GCC_BIN} -DMEMLIM=1024 -DVECTORSZ=8192 -O2 -DXUSAFE -w -o ${OUTDIR}/pan ${OUTDIR}/pan.c") +execute_process(COMMAND time -p ${GCC_BIN} -DMEMLIM=1024 -DVECTORSZ=8192 -O2 -DXUSAFE -w -o ${OUTDIR}/pan ${OUTDIR}/pan.c WORKING_DIRECTORY ${OUTDIR} RESULT_VARIABLE CMD_RESULT) if(CMD_RESULT) message(FATAL_ERROR "Error running gcc ${GCC_BIN}: ${CMD_RESULT}") endif() +message(STATUS "time for transforming to binary") -execute_process(COMMAND ${OUTDIR}/pan -m10000 -a WORKING_DIRECTORY ${OUTDIR} RESULT_VARIABLE CMD_RESULT) +message(STATUS "${OUTDIR}/pan -m10000 -a") +execute_process(COMMAND time -p ${OUTDIR}/pan -m10000 -a WORKING_DIRECTORY ${OUTDIR} RESULT_VARIABLE CMD_RESULT) if(CMD_RESULT) message(FATAL_ERROR "Error running pan: ${CMD_RESULT}") endif() -# +message(STATUS "time for verification") + # message(STATUS "${TEST_OUT}") # file(WRITE ${OUTDIR}/${TEST_FILE_NAME}.pml.out ${TEST_OUT}) \ No newline at end of file -- cgit v0.12