From 42437db418574f2a80d098e568b9498a21343800 Mon Sep 17 00:00:00 2001 From: Stefan Radomski Date: Fri, 26 Dec 2014 23:29:22 +0100 Subject: Plenty of smaller bug-fixes for uscxml-transform and PROMELA datamodel --- apps/uscxml-transform.cpp | 30 +- contrib/local/prune_promela.pl | 42 ++ src/bindings/swig/uscxml_ignores.i | 1 + src/uscxml/Interpreter.cpp | 64 ++- src/uscxml/Interpreter.h | 16 + src/uscxml/debug/InterpreterIssue.cpp | 10 + .../plugins/datamodel/promela/PromelaDataModel.cpp | 100 +++- .../plugins/datamodel/promela/PromelaDataModel.h | 2 +- .../plugins/datamodel/promela/parser/promela.l | 2 +- .../datamodel/promela/parser/promela.lex.yy.cpp | 168 +++--- src/uscxml/transform/ChartToFSM.cpp | 14 +- src/uscxml/transform/ChartToFSM.h | 31 +- src/uscxml/transform/ChartToFlatSCXML.cpp | 52 +- src/uscxml/transform/ChartToFlatSCXML.h | 4 +- src/uscxml/transform/ChartToMinimalSCXML.cpp | 265 +++++++++ src/uscxml/transform/ChartToMinimalSCXML.h | 84 +++ src/uscxml/transform/ChartToPromela.cpp | 603 +++++++++++++-------- src/uscxml/transform/ChartToPromela.h | 15 +- test/CMakeLists.txt | 51 +- test/ctest/CTestCustom.ctest.in | 9 + test/src/test-w3c.cpp | 76 +-- test/w3c/analyze_tests.pl | 33 +- test/w3c/run_minimized_flat_test.cmake | 21 + test/w3c/run_minimized_test.cmake | 16 + test/w3c/run_promela_test.cmake | 14 +- 25 files changed, 1282 insertions(+), 441 deletions(-) create mode 100755 contrib/local/prune_promela.pl create mode 100644 src/uscxml/transform/ChartToMinimalSCXML.cpp create mode 100644 src/uscxml/transform/ChartToMinimalSCXML.h create mode 100644 test/w3c/run_minimized_flat_test.cmake create mode 100644 test/w3c/run_minimized_test.cmake diff --git a/apps/uscxml-transform.cpp b/apps/uscxml-transform.cpp index 3d68242..d8a9013 100644 --- a/apps/uscxml-transform.cpp +++ b/apps/uscxml-transform.cpp @@ -1,6 +1,7 @@ #include "uscxml/config.h" #include "uscxml/Interpreter.h" #include "uscxml/transform/ChartToFlatSCXML.h" +#include "uscxml/transform/ChartToMinimalSCXML.h" #include "uscxml/transform/ChartToPromela.h" #include "uscxml/DOMUtils.h" #include @@ -66,6 +67,7 @@ void printUsageAndExit(const char* progName) { printf("Options\n"); printf("\t-t flat : flatten to SCXML state-machine\n"); printf("\t-t pml : convert to spin/promela program\n"); + printf("\t-t min : minimize SCXML state-chart\n"); printf("\t-v : be verbose\n"); printf("\t-lN : Set loglevel to N\n"); printf("\t-i URL : Input file (defaults to STDIN)\n"); @@ -154,7 +156,7 @@ int main(int argc, char** argv) { if (outType.length() == 0) printUsageAndExit(argv[0]); - if (outType != "flat" && outType != "scxml" && outType != "pml") + if (outType != "flat" && outType != "scxml" && outType != "pml" && outType != "min") printUsageAndExit(argv[0]); // register plugins @@ -185,6 +187,7 @@ int main(int argc, char** argv) { exit(EXIT_FAILURE); } + if (outType == "pml") { if (outputFile.size() == 0 || outputFile == "-") { ChartToPromela::transform(interpreter).writeTo(std::cout); @@ -195,18 +198,6 @@ int main(int argc, char** argv) { outStream.close(); } exit(EXIT_SUCCESS); - -// Interpreter flatInterpreter = ChartToPromela::transform(interpreter); -// -// if (outputFile.size() == 0 || outputFile == "-") { -// ChartToPromela::writeProgram(std::cout, flatInterpreter); -// } else { -// std::ofstream outStream; -// outStream.open(outputFile.c_str()); -// ChartToPromela::writeProgram(outStream, flatInterpreter); -// outStream.close(); -// } -// exit(EXIT_SUCCESS); } if (outType == "scxml" || outType == "flat") { @@ -220,6 +211,19 @@ int main(int argc, char** argv) { } exit(EXIT_SUCCESS); } + + if (outType == "min") { + if (outputFile.size() == 0 || outputFile == "-") { + ChartToMinimalSCXML::transform(interpreter).writeTo(std::cout); + } else { + std::ofstream outStream; + outStream.open(outputFile.c_str()); + ChartToMinimalSCXML::transform(interpreter).writeTo(outStream); + outStream.close(); + } + exit(EXIT_SUCCESS); + } + } catch (Event e) { std::cout << e << std::endl; } diff --git a/contrib/local/prune_promela.pl b/contrib/local/prune_promela.pl new file mode 100755 index 0000000..684afaa --- /dev/null +++ b/contrib/local/prune_promela.pl @@ -0,0 +1,42 @@ +#!/usr/bin/perl -w + +die("Not practical as spin reports superfluous line numbers after preprocessing - minimize SCXML instead"); + +use strict; +use File::Spec; +use File::Basename; + +my $pmlIn = shift or die("Expected *.pml file as input"); + +# absolutize and split into components +$pmlIn = File::Spec->rel2abs($pmlIn) or die($!); +my($filename, $dirs, $suffix) = fileparse($pmlIn) or die($!); + +my $spinOut = `spin -a $pmlIn`; +my $gccOut = `gcc -DMEMLIM=1024 -O2 -DVECTORSZ=2048 -DXUSAFE -w -o pan pan.c`; +my $panOut = `./pan -m10000 -a`; + +my %unvisited; + +for (split /^/, $panOut) { + # /Users/sradomski/Desktop/foo.pml:128, state 12, "foreachIndex1 = 0" + if (/$pmlIn:(\d+), state (\d+), "(.*)"/) { + $unvisited{$1} = $3; + } +} + +open(my $fh, "<", $pmlIn) or die($!); +my $line = 0; +while(<$fh>) { + if (exists($unvisited{$line}) && m/$unvisited{$line}/ ) { + print "/* removed as unvisited */\n"; + } elsif (exists($unvisited{$line})) { + chomp($_); + chomp($unvisited{$line}); + print STDERR "$_ vs $unvisited{$line} \n"; + } else { + print; + } + $line++; +} +close($fh); \ No newline at end of file diff --git a/src/bindings/swig/uscxml_ignores.i b/src/bindings/swig/uscxml_ignores.i index e445bd9..69c7767 100644 --- a/src/bindings/swig/uscxml_ignores.i +++ b/src/bindings/swig/uscxml_ignores.i @@ -56,6 +56,7 @@ %ignore uscxml::Interpreter::getNodeSetForXPath(const std::string&); %ignore uscxml::Interpreter::isLegalConfiguration(const Arabica::XPath::NodeSet&); %ignore uscxml::Interpreter::getInstances(); +%ignore uscxml::Interpreter::addInstance; // InterpreterIssues %ignore uscxml::InterpreterIssue::node; diff --git a/src/uscxml/Interpreter.cpp b/src/uscxml/Interpreter.cpp index cd6472b..6888d0e 100644 --- a/src/uscxml/Interpreter.cpp +++ b/src/uscxml/Interpreter.cpp @@ -329,6 +329,53 @@ void NameSpaceInfo::init(const std::map& namespaceInfo } } +void StateTransitionMonitor::beforeTakingTransition(uscxml::Interpreter interpreter, const Arabica::DOM::Element& transition, bool moreComing) { + std::cout << "Transition: " << uscxml::DOMUtils::xPathForNode(transition) << std::endl; +} + +void StateTransitionMonitor::onStableConfiguration(uscxml::Interpreter interpreter) { + std::cout << "Config: {"; + printNodeSet(interpreter.getConfiguration()); + std::cout << "}" << std::endl; +} + +void StateTransitionMonitor::beforeProcessingEvent(uscxml::Interpreter interpreter, const uscxml::Event& event) { + std::cout << "Event: " << event.name << std::endl; +} + +void StateTransitionMonitor::beforeExecutingContent(Interpreter interpreter, const Arabica::DOM::Element& element) { + std::cout << "Executable Content: " << DOMUtils::xPathForNode(element) << std::endl; +} + +void StateTransitionMonitor::beforeExitingState(uscxml::Interpreter interpreter, const Arabica::DOM::Element& state, bool moreComing) { + exitingStates.push_back(state); + if (!moreComing) { + std::cout << "Exiting: {"; + printNodeSet(exitingStates); + std::cout << "}" << std::endl; + exitingStates = Arabica::XPath::NodeSet(); + } +} + +void StateTransitionMonitor::beforeEnteringState(uscxml::Interpreter interpreter, const Arabica::DOM::Element& state, bool moreComing) { + enteringStates.push_back(state); + if (!moreComing) { + std::cout << "Entering: {"; + printNodeSet(enteringStates); + std::cout << "}" << std::endl; + enteringStates = Arabica::XPath::NodeSet(); + } + +} + +void StateTransitionMonitor::printNodeSet(const Arabica::XPath::NodeSet& config) { + std::string seperator; + for (int i = 0; i < config.size(); i++) { + std::cout << seperator << ATTR_CAST(config[i], "id"); + seperator = ", "; + } +} + std::map > Interpreter::_instances; tthread::recursive_mutex Interpreter::_instanceMutex; @@ -345,6 +392,11 @@ std::map > Interpreter::getInstanc return _instances; } +void Interpreter::addInstance(boost::shared_ptr interpreterImpl) { + tthread::lock_guard lock(_instanceMutex); + assert(_instances.find(interpreterImpl->getSessionId()) == _instances.end()); + _instances[interpreterImpl->getSessionId()] = interpreterImpl; +} InterpreterImpl::InterpreterImpl() { _state = USCXML_INSTANTIATED; @@ -467,7 +519,7 @@ Interpreter Interpreter::fromInputSource(Arabica::SAX::InputSource& if (parser.errorsReported()) { ERROR_PLATFORM_THROW(parser.errors()) } else { - ERROR_PLATFORM_THROW("Failed to create interpreter"); + ERROR_PLATFORM_THROW("Failed to create interpreter from " + sourceURL); // interpreterImpl->setInterpreterState(USCXML_FAULTED, parser.errors()); } } @@ -481,7 +533,7 @@ Interpreter Interpreter::fromClone(const Interpreter& other) { interpreterImpl->cloneFrom(other.getImpl()); Interpreter interpreter(interpreterImpl); - _instances[interpreterImpl->getSessionId()] = interpreterImpl; + addInstance(interpreterImpl); return interpreter; } @@ -733,7 +785,7 @@ InterpreterState InterpreterImpl::step(int waitForMS) { setInterpreterState(USCXML_MICROSTEPPED); } - //assert(isLegalConfiguration(_configuration)); + assert(isLegalConfiguration(_configuration)); // are there spontaneous transitions? if (!_stable) { @@ -1243,6 +1295,8 @@ void InterpreterImpl::setupDOM() { _baseURL[_scxml] = URL::asBaseURL(_sourceURL); } + _binding = (HAS_ATTR(_scxml, "binding") && iequals(ATTR(_scxml, "binding"), "late") ? LATE : EARLY); + if (_nsInfo.getNSContext() != NULL) _xpath.setNamespaceContext(*_nsInfo.getNSContext()); @@ -1471,8 +1525,6 @@ void InterpreterImpl::init() { std::cout << "running " << this << std::endl; #endif - _binding = (HAS_ATTR(_scxml, "binding") && iequals(ATTR(_scxml, "binding"), "late") ? LATE : EARLY); - if (_binding == EARLY) { // initialize all data elements NodeSet dataElems = _xpath.evaluate("//" + _nsInfo.xpathPrefix + "data", _scxml).asNodeSet(); @@ -2104,6 +2156,8 @@ void InterpreterImpl::invoke(const Arabica::DOM::Element& element) LOG(ERROR) << "Exception caught while sending invoke request to invoker " << invokeReq.invokeid << ": " << e.what(); } catch (const std::exception &e) { LOG(ERROR) << "Unknown exception caught while sending invoke request to invoker " << invokeReq.invokeid << ": " << e.what(); + } catch (Event &e) { + LOG(ERROR) << e; } catch(...) { LOG(ERROR) << "Unknown exception caught while sending invoke request to invoker " << invokeReq.invokeid; } diff --git a/src/uscxml/Interpreter.h b/src/uscxml/Interpreter.h index abccb0a..c509684 100644 --- a/src/uscxml/Interpreter.h +++ b/src/uscxml/Interpreter.h @@ -840,6 +840,7 @@ public: } static std::map > getInstances(); + static void addInstance(boost::shared_ptr instance); protected: @@ -890,6 +891,21 @@ public: }; +class StateTransitionMonitor : public uscxml::InterpreterMonitor { +public: + virtual void beforeTakingTransition(uscxml::Interpreter interpreter, const Arabica::DOM::Element& transition, bool moreComing); + virtual void beforeExecutingContent(Interpreter interpreter, const Arabica::DOM::Element& element); + virtual void onStableConfiguration(uscxml::Interpreter interpreter); + virtual void beforeProcessingEvent(uscxml::Interpreter interpreter, const uscxml::Event& event); + virtual void beforeExitingState(uscxml::Interpreter interpreter, const Arabica::DOM::Element& state, bool moreComing); + virtual void beforeEnteringState(uscxml::Interpreter interpreter, const Arabica::DOM::Element& state, bool moreComing); + +protected: + void printNodeSet(const Arabica::XPath::NodeSet& config); + Arabica::XPath::NodeSet exitingStates; + Arabica::XPath::NodeSet enteringStates; +}; + } #endif diff --git a/src/uscxml/debug/InterpreterIssue.cpp b/src/uscxml/debug/InterpreterIssue.cpp index 3e207e9..1bd416c 100644 --- a/src/uscxml/debug/InterpreterIssue.cpp +++ b/src/uscxml/debug/InterpreterIssue.cpp @@ -310,6 +310,12 @@ std::list InterpreterIssue::forInterpreter(InterpreterImpl* in issues.push_back(InterpreterIssue("State has no 'id' attribute", state, InterpreterIssue::USCXML_ISSUE_FATAL)); continue; } + + if (ATTR(state, "id").size() == 0) { + issues.push_back(InterpreterIssue("State has empty 'id' attribute", state, InterpreterIssue::USCXML_ISSUE_FATAL)); + continue; + } + std::string stateId = ATTR(state, "id"); if (!InterpreterImpl::isMember(state, reachable)) { @@ -331,6 +337,10 @@ std::list InterpreterIssue::forInterpreter(InterpreterImpl* in // check for valid target std::list targetIds = InterpreterImpl::tokenizeIdRefs(ATTR(transition, "target")); + if (targetIds.size() == 0) { + issues.push_back(InterpreterIssue("Transition has empty target state list", transition, InterpreterIssue::USCXML_ISSUE_FATAL)); + } + for (std::list::iterator targetIter = targetIds.begin(); targetIter != targetIds.end(); targetIter++) { if (seenStates.find(*targetIter) == seenStates.end()) { issues.push_back(InterpreterIssue("Transition has non-existant target state with id '" + *targetIter + "'", transition, InterpreterIssue::USCXML_ISSUE_FATAL)); diff --git a/src/uscxml/plugins/datamodel/promela/PromelaDataModel.cpp b/src/uscxml/plugins/datamodel/promela/PromelaDataModel.cpp index 9edd505..679177a 100644 --- a/src/uscxml/plugins/datamodel/promela/PromelaDataModel.cpp +++ b/src/uscxml/plugins/datamodel/promela/PromelaDataModel.cpp @@ -329,6 +329,7 @@ void PromelaDataModel::evaluateStmnt(const std::string& expr) { void PromelaDataModel::evaluateDecl(void* ast) { PromelaParserNode* node = (PromelaParserNode*)ast; +// node->dump(); if (false) { } else if (node->type == PML_DECL) { std::list::iterator opIter = node->operands.begin(); @@ -398,6 +399,7 @@ void PromelaDataModel::evaluateDecl(void* ast) { evaluateDecl(*declIter); } } else { + node->dump(); ERROR_EXECUTION_THROW("Declaring variables via " + PromelaParserNode::typeToDesc(node->type) + " not implemented"); } } @@ -446,8 +448,9 @@ Data PromelaDataModel::evaluateExpr(void* ast) { case PML_CMPND: return getVariable(node); case PML_STRING: { - std::string stripped = node->value.substr(1, node->value.size() - 2); - return Data(stripped, Data::VERBATIM); +// std::string stripped = node->value.substr(1, node->value.size() - 2); +// return Data(stripped, Data::VERBATIM); + return Data(node->value, Data::INTERPRETED); } case PML_PLUS: return dataToInt(evaluateExpr(*opIter++)) + dataToInt(evaluateExpr(*opIter++)); @@ -549,29 +552,33 @@ void PromelaDataModel::evaluateStmnt(void* ast) { } } -void PromelaDataModel::setVariable(void* ast, Data value) { + +void PromelaDataModel::setVariable(void* ast, const Data& value) { PromelaParserNode* node = (PromelaParserNode*)ast; - std::list::iterator opIter = node->operands.begin(); + if (INVALID_ASSIGNMENT(node->value)) { + ERROR_EXECUTION_THROW("Cannot assign to " + node->value); + } + +// if (_variables.compound.find(name->value) == _variables.compound.end()) { +// // declare implicitly / convenience +// evaluateDecl(ast); +// } + switch (node->type) { case PML_VAR_ARRAY: { + std::list::iterator opIter = node->operands.begin(); + PromelaParserNode* name = *opIter++; PromelaParserNode* expr = *opIter++; - if (INVALID_ASSIGNMENT(name->value)) { - ERROR_EXECUTION_THROW("Cannot assign to " + name->value); - } - - int index = dataToInt(evaluateExpr(expr)); - - if (_variables.compound.find(name->value) == _variables.compound.end()) { - ERROR_EXECUTION_THROW("No variable " + name->value + " was declared"); - } - + // is the location an array? if (!_variables[name->value].hasKey("size")) { ERROR_EXECUTION_THROW("Variable " + name->value + " is no array"); } + // is the array large enough? + int index = dataToInt(evaluateExpr(expr)); if (strTo(_variables[name->value]["size"].atom) <= index) { ERROR_EXECUTION_THROW("Index " + toStr(index) + " in array " + name->value + "[" + _variables[name->value]["size"].atom + "] is out of bounds"); } @@ -580,19 +587,51 @@ void PromelaDataModel::setVariable(void* ast, Data value) { break; } - case PML_NAME: - if (INVALID_ASSIGNMENT(node->value)) { - ERROR_EXECUTION_THROW("Cannot assign to " + node->value); + case PML_NAME: { + // location is an array, but no array was passed + if (_variables[node->value].hasKey("size")) { + if (value.compound.size() > 0 || value.atom.size() > 0) + ERROR_EXECUTION_THROW("Variable " + node->value + " is an array"); + + if (_variables[node->value].compound["size"] < value.array.size()) + ERROR_EXECUTION_THROW("Array assigned to " + node->value + " is too large"); } + _variables.compound[node->value].compound["value"] = value; break; + } + case PML_CMPND: { + std::list::iterator opIter = node->operands.begin(); + PromelaParserNode* name = *opIter++; + + // location is no array + if (_variables[name->value].hasKey("size")) { + ERROR_EXECUTION_THROW("Variable " + name->value + " is an array"); + } + +// std::cout << Data::toJSON(_variables) << std::endl;; + + Data* var = &_variables[name->value].compound["value"]; + var->compound["type"] = Data("compound", Data::VERBATIM); + var->compound["vis"] = Data("", Data::VERBATIM); + + while(opIter != node->operands.end()) { + name = *opIter; opIter++; + var = &(var->compound[name->value]); + } + *var = value; + + break; + } default: + node->dump(); + ERROR_EXECUTION_THROW("No support for " + PromelaParserNode::typeToDesc(node->type) + " variables implemented"); break; } // std::cout << Data::toJSON(_variables) << std::endl; } - + Data PromelaDataModel::getVariable(void* ast) { PromelaParserNode* node = (PromelaParserNode*)ast; // node->dump(); @@ -628,7 +667,6 @@ Data PromelaDataModel::getVariable(void* ast) { case PML_CMPND: { // node->dump(); // std::cout << Data::toJSON(_variables["_event"]); - std::stringstream idPath; PromelaParserNode* name = *opIter++; @@ -711,7 +749,7 @@ void PromelaDataModel::init(const Element& dataElem, // from if (HAS_ATTR(dataElem, "id")) { std::string identifier = ATTR(dataElem, "id"); - std::string type = (HAS_ATTR(dataElem, "type") ? ATTR(dataElem, "type") : "int"); + std::string type = (HAS_ATTR(dataElem, "type") ? ATTR(dataElem, "type") : "auto"); std::string arrSize; size_t bracketPos = type.find("["); @@ -719,7 +757,7 @@ void PromelaDataModel::init(const Element& dataElem, arrSize = type.substr(bracketPos, type.length() - bracketPos); type = type.substr(0, bracketPos); } - + std::string expr = type + " " + identifier + arrSize; PromelaParser parser(expr, 1, PromelaParser::PROMELA_DECL); evaluateDecl(parser.ast); @@ -733,9 +771,29 @@ void PromelaDataModel::init(const std::string& location, const Data& data) { bool PromelaDataModel::isDeclared(const std::string& expr) { PromelaParser parser(expr); +// parser.dump(); if (parser.ast->type == PML_VAR_ARRAY) return _variables.compound.find(parser.ast->operands.front()->value) != _variables.compound.end(); + if (parser.ast->type == PML_CMPND) { + // JSON declaration + std::list::iterator opIter = parser.ast->operands.begin(); + Data* var = &_variables; + + while(opIter != parser.ast->operands.end()) { + std::string name = (*opIter)->value; opIter++; + if (var->compound.find(name) != var->compound.end()) { + var = &(var->compound.at(name)); + } else if (var->compound.find("value") != var->compound.end() && var->compound.at("value").compound.find(name) != var->compound.at("value").compound.end()) { + var = &(var->compound.at("value").compound.at(name)); + } else { + return false; + } + } + return true; + + } + return _variables.compound.find(expr) != _variables.compound.end(); } diff --git a/src/uscxml/plugins/datamodel/promela/PromelaDataModel.h b/src/uscxml/plugins/datamodel/promela/PromelaDataModel.h index b286f4b..581c761 100644 --- a/src/uscxml/plugins/datamodel/promela/PromelaDataModel.h +++ b/src/uscxml/plugins/datamodel/promela/PromelaDataModel.h @@ -93,7 +93,7 @@ protected: Data evaluateExpr(const std::string& expr); void evaluateStmnt(const std::string& expr); - void setVariable(void* ast, Data value); + void setVariable(void* ast, const Data& value); Data getVariable(void* ast); void adaptType(Data& data); diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.l b/src/uscxml/plugins/datamodel/promela/parser/promela.l index d247d74..1edc625 100644 --- a/src/uscxml/plugins/datamodel/promela/parser/promela.l +++ b/src/uscxml/plugins/datamodel/promela/parser/promela.l @@ -43,7 +43,7 @@ L [a-zA-Z_] \/\*([^*]|\*[^/])*\*+\/ /* multiline comments */ -bit|bool|byte|int|mtype|short|unsigned|string { +bit|bool|byte|int|mtype|short|unsigned|string|auto { yylval->value = strdup(yytext); return PML_TYPE; } diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.lex.yy.cpp b/src/uscxml/plugins/datamodel/promela/parser/promela.lex.yy.cpp index 842efe6..2cd66f2 100644 --- a/src/uscxml/plugins/datamodel/promela/parser/promela.lex.yy.cpp +++ b/src/uscxml/plugins/datamodel/promela/parser/promela.lex.yy.cpp @@ -456,7 +456,7 @@ struct yy_trans_info flex_int32_t yy_verify; flex_int32_t yy_nxt; }; -static yyconst flex_int16_t yy_accept[124] = +static yyconst flex_int16_t yy_accept[126] = { 0, 0, 0, 47, 45, 44, 44, 8, 45, 14, 25, 45, 33, 34, 12, 15, 31, 16, 30, 13, 42, @@ -465,13 +465,13 @@ static yyconst flex_int16_t yy_accept[124] = 27, 38, 9, 44, 23, 0, 40, 0, 28, 0, 41, 0, 10, 11, 0, 42, 17, 19, 24, 20, 18, 43, 0, 0, 43, 43, 43, 43, 43, 43, - 43, 43, 43, 43, 43, 43, 43, 43, 43, 29, - 0, 41, 0, 0, 0, 43, 2, 43, 43, 43, - 3, 43, 43, 43, 43, 43, 43, 43, 43, 0, + 43, 43, 43, 43, 43, 43, 43, 43, 43, 43, + 29, 0, 41, 0, 0, 0, 43, 43, 2, 43, + 43, 43, 3, 43, 43, 43, 43, 43, 43, 43, - 1, 43, 43, 43, 43, 43, 4, 43, 43, 43, - 1, 43, 43, 43, 43, 43, 7, 5, 43, 43, - 6, 43, 0 + 43, 0, 1, 43, 43, 43, 43, 43, 4, 43, + 43, 43, 1, 43, 43, 43, 43, 43, 7, 5, + 43, 43, 6, 43, 0 } ; static yyconst flex_int32_t yy_ec[256] = @@ -515,43 +515,43 @@ static yyconst flex_int32_t yy_meta[51] = 2, 2, 2, 2, 2, 2, 1, 1, 1, 1 } ; -static yyconst flex_int16_t yy_base[129] = +static yyconst flex_int16_t yy_base[131] = { 0, - 0, 0, 169, 170, 49, 51, 148, 50, 170, 160, - 48, 170, 170, 170, 154, 170, 151, 170, 153, 146, - 170, 38, 142, 39, 0, 56, 170, 170, 170, 118, - 28, 132, 120, 127, 113, 114, 33, 20, 116, 170, - 106, 170, 170, 68, 170, 60, 170, 150, 170, 64, - 170, 73, 170, 170, 141, 134, 170, 170, 170, 170, - 170, 0, 74, 70, 107, 105, 108, 103, 109, 101, - 105, 97, 107, 101, 105, 97, 93, 96, 93, 170, - 72, 75, 79, 124, 75, 103, 0, 96, 101, 88, - 0, 89, 90, 86, 86, 91, 94, 93, 88, 77, - - 170, 80, 90, 89, 75, 74, 0, 78, 86, 82, - 103, 69, 71, 69, 70, 57, 0, 0, 62, 61, - 0, 60, 170, 104, 106, 82, 108, 110 + 0, 0, 172, 173, 49, 51, 151, 50, 173, 163, + 48, 173, 173, 173, 157, 173, 154, 173, 156, 149, + 173, 38, 145, 39, 0, 56, 173, 173, 173, 20, + 31, 136, 124, 131, 117, 118, 34, 30, 120, 173, + 110, 173, 173, 77, 173, 57, 173, 154, 173, 59, + 173, 66, 173, 173, 145, 138, 173, 173, 173, 173, + 173, 0, 76, 75, 111, 109, 108, 111, 106, 112, + 104, 108, 100, 110, 104, 108, 100, 96, 99, 96, + 173, 77, 78, 84, 127, 77, 106, 96, 0, 98, + 103, 90, 0, 91, 92, 88, 88, 93, 96, 95, + + 90, 78, 173, 82, 92, 91, 77, 76, 0, 80, + 88, 75, 96, 62, 73, 71, 68, 59, 0, 0, + 65, 65, 0, 65, 173, 109, 111, 88, 113, 115 } ; -static yyconst flex_int16_t yy_def[129] = +static yyconst flex_int16_t yy_def[131] = { 0, - 123, 1, 123, 123, 123, 123, 123, 124, 123, 123, - 125, 123, 123, 123, 123, 123, 123, 123, 123, 123, - 123, 123, 123, 123, 126, 126, 123, 123, 123, 126, - 126, 126, 126, 126, 126, 126, 126, 126, 126, 123, - 123, 123, 123, 123, 123, 124, 123, 124, 123, 125, - 123, 127, 123, 123, 128, 123, 123, 123, 123, 123, - 123, 126, 124, 125, 126, 126, 126, 126, 126, 126, - 126, 126, 126, 126, 126, 126, 126, 126, 126, 123, - 125, 125, 127, 128, 128, 126, 126, 126, 126, 126, - 126, 126, 126, 126, 126, 126, 126, 126, 126, 128, - - 123, 126, 126, 126, 126, 126, 126, 126, 126, 126, - 128, 126, 126, 126, 126, 126, 126, 126, 126, 126, - 126, 126, 0, 123, 123, 123, 123, 123 + 125, 1, 125, 125, 125, 125, 125, 126, 125, 125, + 127, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 128, 128, 125, 125, 125, 128, + 128, 128, 128, 128, 128, 128, 128, 128, 128, 125, + 125, 125, 125, 125, 125, 126, 125, 126, 125, 127, + 125, 129, 125, 125, 130, 125, 125, 125, 125, 125, + 125, 128, 126, 127, 128, 128, 128, 128, 128, 128, + 128, 128, 128, 128, 128, 128, 128, 128, 128, 128, + 125, 127, 127, 129, 130, 130, 128, 128, 128, 128, + 128, 128, 128, 128, 128, 128, 128, 128, 128, 128, + + 128, 130, 125, 128, 128, 128, 128, 128, 128, 128, + 128, 128, 130, 128, 128, 128, 128, 128, 128, 128, + 128, 128, 128, 128, 0, 125, 125, 125, 125, 125 } ; -static yyconst flex_int16_t yy_nxt[221] = +static yyconst flex_int16_t yy_nxt[224] = { 0, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, @@ -559,27 +559,28 @@ static yyconst flex_int16_t yy_nxt[221] = 25, 32, 25, 25, 33, 25, 34, 35, 25, 25, 36, 25, 37, 38, 39, 25, 40, 41, 42, 43, 44, 44, 44, 44, 47, 51, 57, 58, 60, 61, - 63, 77, 66, 64, 47, 78, 74, 67, 75, 44, - 44, 51, 52, 68, 48, 50, 76, 51, 47, 51, - 82, 50, 51, 62, 48, 100, 82, 85, 52, 87, - 101, 122, 111, 121, 52, 120, 52, 83, 48, 52, - - 119, 87, 118, 83, 46, 46, 50, 50, 81, 81, - 84, 84, 117, 85, 116, 115, 114, 87, 113, 87, - 107, 112, 110, 109, 107, 108, 107, 106, 105, 104, - 103, 87, 87, 102, 85, 99, 98, 97, 96, 95, - 94, 93, 92, 91, 87, 90, 89, 88, 87, 86, - 56, 85, 123, 80, 79, 73, 72, 71, 70, 69, - 65, 59, 56, 55, 54, 53, 49, 45, 123, 3, - 123, 123, 123, 123, 123, 123, 123, 123, 123, 123, - 123, 123, 123, 123, 123, 123, 123, 123, 123, 123, - 123, 123, 123, 123, 123, 123, 123, 123, 123, 123, - - 123, 123, 123, 123, 123, 123, 123, 123, 123, 123, - 123, 123, 123, 123, 123, 123, 123, 123, 123, 123 + 63, 47, 65, 64, 66, 67, 51, 75, 50, 76, + 68, 78, 52, 83, 48, 79, 69, 77, 44, 44, + 47, 48, 51, 52, 51, 51, 50, 102, 86, 62, + 84, 83, 103, 113, 89, 124, 123, 122, 121, 52, + + 48, 52, 52, 89, 120, 119, 86, 118, 84, 46, + 46, 50, 50, 82, 82, 85, 85, 117, 116, 89, + 115, 89, 109, 114, 112, 111, 109, 110, 109, 108, + 107, 106, 105, 89, 89, 89, 104, 86, 101, 100, + 99, 98, 97, 96, 95, 94, 93, 89, 92, 91, + 90, 89, 88, 87, 56, 86, 125, 81, 80, 74, + 73, 72, 71, 70, 59, 56, 55, 54, 53, 49, + 45, 125, 3, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125 } ; -static yyconst flex_int16_t yy_chk[221] = +static yyconst flex_int16_t yy_chk[224] = { 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, @@ -587,24 +588,25 @@ static yyconst flex_int16_t yy_chk[221] = 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 5, 5, 6, 6, 8, 11, 22, 22, 24, 24, - 26, 38, 31, 26, 46, 38, 37, 31, 37, 44, - 44, 50, 11, 31, 8, 52, 37, 64, 63, 81, - 52, 83, 82, 126, 46, 85, 83, 100, 50, 122, - 85, 120, 100, 119, 64, 116, 81, 52, 63, 82, - - 115, 114, 113, 83, 124, 124, 125, 125, 127, 127, - 128, 128, 112, 111, 110, 109, 108, 106, 105, 104, - 103, 102, 99, 98, 97, 96, 95, 94, 93, 92, - 90, 89, 88, 86, 84, 79, 78, 77, 76, 75, - 74, 73, 72, 71, 70, 69, 68, 67, 66, 65, - 56, 55, 48, 41, 39, 36, 35, 34, 33, 32, - 30, 23, 20, 19, 17, 15, 10, 7, 3, 123, - 123, 123, 123, 123, 123, 123, 123, 123, 123, 123, - 123, 123, 123, 123, 123, 123, 123, 123, 123, 123, - 123, 123, 123, 123, 123, 123, 123, 123, 123, 123, - - 123, 123, 123, 123, 123, 123, 123, 123, 123, 123, - 123, 123, 123, 123, 123, 123, 123, 123, 123, 123 + 26, 46, 30, 26, 30, 31, 50, 37, 52, 37, + 31, 38, 11, 52, 8, 38, 31, 37, 44, 44, + 63, 46, 64, 50, 82, 83, 84, 86, 102, 128, + 52, 84, 86, 102, 124, 122, 121, 118, 117, 64, + + 63, 82, 83, 116, 115, 114, 113, 112, 84, 126, + 126, 127, 127, 129, 129, 130, 130, 111, 110, 108, + 107, 106, 105, 104, 101, 100, 99, 98, 97, 96, + 95, 94, 92, 91, 90, 88, 87, 85, 80, 79, + 78, 77, 76, 75, 74, 73, 72, 71, 70, 69, + 68, 67, 66, 65, 56, 55, 48, 41, 39, 36, + 35, 34, 33, 32, 23, 20, 19, 17, 15, 10, + 7, 3, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125 } ; /* Table of booleans, true if rule could match eol. */ @@ -655,7 +657,7 @@ static yyconst flex_int16_t yy_rule_linenum[46] = yycolumn = yycolumn + yyleng; \ } -#line 659 "promela.lex.yy.cpp" +#line 661 "promela.lex.yy.cpp" #define INITIAL 0 @@ -964,7 +966,7 @@ YY_DECL #line 42 "promela.l" -#line 968 "promela.lex.yy.cpp" +#line 970 "promela.lex.yy.cpp" yylval = yylval_param; @@ -1031,13 +1033,13 @@ yy_match: while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state ) { yy_current_state = (int) yy_def[yy_current_state]; - if ( yy_current_state >= 124 ) + if ( yy_current_state >= 126 ) yy_c = yy_meta[(unsigned int) yy_c]; } yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c]; ++yy_cp; } - while ( yy_current_state != 123 ); + while ( yy_current_state != 125 ); yy_cp = yyg->yy_last_accepting_cpos; yy_current_state = yyg->yy_last_accepting_state; @@ -1330,7 +1332,7 @@ YY_RULE_SETUP #line 118 "promela.l" ECHO; YY_BREAK -#line 1334 "promela.lex.yy.cpp" +#line 1336 "promela.lex.yy.cpp" case YY_STATE_EOF(INITIAL): yyterminate(); @@ -1646,7 +1648,7 @@ static int yy_get_next_buffer (yyscan_t yyscanner) while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state ) { yy_current_state = (int) yy_def[yy_current_state]; - if ( yy_current_state >= 124 ) + if ( yy_current_state >= 126 ) yy_c = yy_meta[(unsigned int) yy_c]; } yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c]; @@ -1680,11 +1682,11 @@ static int yy_get_next_buffer (yyscan_t yyscanner) while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state ) { yy_current_state = (int) yy_def[yy_current_state]; - if ( yy_current_state >= 124 ) + if ( yy_current_state >= 126 ) yy_c = yy_meta[(unsigned int) yy_c]; } yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c]; - yy_is_jam = (yy_current_state == 123); + yy_is_jam = (yy_current_state == 125); return yy_is_jam ? 0 : yy_current_state; } diff --git a/src/uscxml/transform/ChartToFSM.cpp b/src/uscxml/transform/ChartToFSM.cpp index d220638..8597211 100644 --- a/src/uscxml/transform/ChartToFSM.cpp +++ b/src/uscxml/transform/ChartToFSM.cpp @@ -197,7 +197,6 @@ ChartToFSM::ChartToFSM(const Interpreter& other) { _start = NULL; _currGlobalTransition = NULL; - _lastTransientStateId = 0; _lastStateIndex = 0; _lastActiveIndex = 0; @@ -289,7 +288,13 @@ InterpreterState ChartToFSM::interpret() { } _binding = (HAS_ATTR(_scxml, "binding") && iequals(ATTR(_scxml, "binding"), "late") ? LATE : EARLY); + _alreadyFlat = (HAS_ATTR(_scxml, "flat") && DOMUtils::attributeIsTrue(ATTR(_scxml, "flat"))); + if (_alreadyFlat) { + reassembleFromFlat(); + return _state; + } + // set invokeid for all invokers to parent state if none given NodeSet invokers = filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true); for (int i = 0; i < invokers.size(); i++) { @@ -1043,6 +1048,11 @@ uint32_t ChartToFSM::getMinExternalQueueLength(uint32_t defaultVal) { return defaultVal; } +void ChartToFSM::reassembleFromFlat() { + LOG(ERROR) << "Cannot flatten flat SCXML document"; + abort(); +} + Arabica::XPath::NodeSet ChartToFSM::refsToStates(const std::set& stateRefs) { NodeSet states; for (std::set::const_iterator stateIter = stateRefs.begin(); stateIter != stateRefs.end(); stateIter++) { @@ -1239,7 +1249,7 @@ GlobalTransition::GlobalTransition(const Arabica::XPath::NodeSet& t Arabica::DOM::Element transElem = Arabica::DOM::Element(transitionSet[i]); // gather conditions while we are iterating anyway if (HAS_ATTR(transElem, "cond")) { - conditions.push_back(ATTR(transElem, "cond")); + conditions.push_back(boost::trim_copy(ATTR(transElem, "cond"))); } std::list targets = InterpreterImpl::tokenizeIdRefs(ATTR(transElem, "target")); diff --git a/src/uscxml/transform/ChartToFSM.h b/src/uscxml/transform/ChartToFSM.h index 006e73b..c4d2da3 100644 --- a/src/uscxml/transform/ChartToFSM.h +++ b/src/uscxml/transform/ChartToFSM.h @@ -74,6 +74,7 @@ class USCXML_API GlobalState { public: GlobalState() {} + GlobalState(const Arabica::DOM::Node& globalState); GlobalState(const Arabica::XPath::NodeSet& activeStates, const Arabica::XPath::NodeSet& alreadyEnteredStates, // we need to remember for binding=late const std::map >& historyStates, @@ -84,10 +85,6 @@ public: std::set alreadyEnteredStatesRefs; std::map > historyStatesRefs; - Arabica::XPath::NodeSet getActiveStates(); - Arabica::XPath::NodeSet getAlreadyEnteredStates(); - std::map > getHistoryStates(); - std::list sortedOutgoing; std::string stateId; std::string activeId; @@ -97,6 +94,12 @@ public: bool isFinal; ChartToFSM* interpreter; + + Arabica::XPath::NodeSet getActiveStates(); + Arabica::XPath::NodeSet getAlreadyEnteredStates(); + std::map > getHistoryStates(); + +// friend class ChartToFSM; }; @@ -197,6 +200,16 @@ protected: Arabica::DOM::Document getDocument() const; // overwrite to return flat FSM InterpreterState interpret(); + GlobalState* _start; + Arabica::DOM::Document _flatDoc; + std::map _globalConf; + std::map _activeConf; // potentially enabled transition sets per active configuration + std::map > _historyTargets; // ids of all history states + + uint32_t getMinInternalQueueLength(uint32_t defaultVal); + uint32_t getMinExternalQueueLength(uint32_t defaultVal); + +private: Arabica::XPath::NodeSet refsToStates(const std::set&); Arabica::XPath::NodeSet refsToTransitions(const std::set&); @@ -230,8 +243,7 @@ protected: bool hasForeachInBetween(const Arabica::DOM::Node& ancestor, const Arabica::DOM::Node& child); void updateRaisedAndSendChains(GlobalState* state, GlobalTransition* source, std::set visited); - uint32_t getMinInternalQueueLength(uint32_t defaultVal); - uint32_t getMinExternalQueueLength(uint32_t defaultVal); + void reassembleFromFlat(); std::list sortTransitions(std::list list); @@ -257,17 +269,14 @@ protected: size_t _lastActiveIndex; size_t _lastTransIndex; + bool _alreadyFlat; + bool _skipEventChainCalculations; size_t _maxEventSentChain; size_t _maxEventRaisedChain; size_t _doneEventRaiseTolerance; - GlobalState* _start; GlobalTransition* _currGlobalTransition; - Arabica::DOM::Document _flatDoc; - std::map _globalConf; - std::map _activeConf; // potentially enabled transition sets per active configuration - std::map > _historyTargets; // ids of all history states friend class GlobalTransition; friend class GlobalState; diff --git a/src/uscxml/transform/ChartToFlatSCXML.cpp b/src/uscxml/transform/ChartToFlatSCXML.cpp index f279a67..d9e2586 100644 --- a/src/uscxml/transform/ChartToFlatSCXML.cpp +++ b/src/uscxml/transform/ChartToFlatSCXML.cpp @@ -44,6 +44,7 @@ ChartToFlatSCXML::operator Interpreter() { if (!HAS_ATTR(_scxml, "flat") || !DOMUtils::attributeIsTrue(ATTR(_scxml, "flat"))) { createDocument(); } + return Interpreter::fromClone(shared_from_this()); } @@ -55,6 +56,27 @@ void ChartToFlatSCXML::writeTo(std::ostream& stream) { if (!HAS_ATTR(_scxml, "flat") || !DOMUtils::attributeIsTrue(ATTR(_scxml, "flat"))) { createDocument(); } + + char* withDebugAttrs = getenv("USCXML_FLAT_WITH_DEBUG_ATTRS"); + if (withDebugAttrs == NULL || !DOMUtils::attributeIsTrue(withDebugAttrs)) { + // remove all debug attributes + NodeSet elementNodes = filterChildType(Node_base::ELEMENT_NODE, _scxml, true); + for (int i = 0; i < elementNodes.size(); i++) { + Element element(elementNodes[i]); + if (HAS_ATTR(element, "send")) + element.removeAttribute("send"); + if (HAS_ATTR(element, "raise")) + element.removeAttribute("raise"); + if (HAS_ATTR(element, "members")) + element.removeAttribute("members"); + if (HAS_ATTR(element, "ref")) + element.removeAttribute("ref"); + if (HAS_ATTR(element, "final-target")) + element.removeAttribute("final-target"); + } + } + + stream << _scxml; } @@ -63,6 +85,17 @@ void ChartToFlatSCXML::createDocument() { if (HAS_ATTR(_scxml, "flat") && DOMUtils::attributeIsTrue(ATTR(_scxml, "flat"))) return; + { + NodeSet allElements = filterChildType(Node_base::ELEMENT_NODE, _scxml, true); + size_t nrElements = 0; + for (int i = 0; i < allElements.size(); i++) { + if (!isInEmbeddedDocument(allElements[i])) + nrElements++; + } + std::cerr << "Number of elements before flattening: " << nrElements + 1 << std::endl; + } + + if (_start == NULL) interpret(); // only if not already flat! @@ -134,6 +167,23 @@ void ChartToFlatSCXML::createDocument() { } _document = _flatDoc; + + NodeSet scxmls = filterChildElements(_nsInfo.xmlNSPrefix + "scxml", _document); + if (scxmls.size() > 0) { + _scxml = Element(scxmls[0]); + } + + { + NodeSet allElements = filterChildType(Node_base::ELEMENT_NODE, _scxml, true); + size_t nrElements = 0; + for (int i = 0; i < allElements.size(); i++) { + if (!isInEmbeddedDocument(allElements[i])) + nrElements++; + } + std::cerr << "Number of elements after flattening: " << nrElements + 1 << std::endl; + } + + } void ChartToFlatSCXML::appendGlobalStateNode(GlobalState* globalState) { @@ -222,14 +272,12 @@ Node ChartToFlatSCXML::globalTransitionToNode(GlobalTransition* glo if (actionIter->onExit) { // DETAIL_EXEC_CONTENT(onExit, actionIter); - childs.push_back(actionIter->onExit); continue; } if (actionIter->onEntry) { // DETAIL_EXEC_CONTENT(onEntry, actionIter); - childs.push_back(actionIter->onEntry); continue; } diff --git a/src/uscxml/transform/ChartToFlatSCXML.h b/src/uscxml/transform/ChartToFlatSCXML.h index b6dd616..f611a7c 100644 --- a/src/uscxml/transform/ChartToFlatSCXML.h +++ b/src/uscxml/transform/ChartToFlatSCXML.h @@ -39,13 +39,15 @@ public: protected: void writeTo(std::ostream& stream); - ChartToFlatSCXML(const Interpreter& other) : TransformerImpl(), ChartToFSM(other) {} + ChartToFlatSCXML(const Interpreter& other) : TransformerImpl(), ChartToFSM(other), _lastTransientStateId(0) {} void createDocument(); void appendGlobalStateNode(GlobalState* globalState); Arabica::DOM::Node globalTransitionToNode(GlobalTransition* globalTransition); static bool sortStatesByIndex(const std::pair& s1, const std::pair& s2); + size_t _lastTransientStateId; + }; } diff --git a/src/uscxml/transform/ChartToMinimalSCXML.cpp b/src/uscxml/transform/ChartToMinimalSCXML.cpp new file mode 100644 index 0000000..270794d --- /dev/null +++ b/src/uscxml/transform/ChartToMinimalSCXML.cpp @@ -0,0 +1,265 @@ +/** + * @file + * @author 2012-2014 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 "uscxml/transform/ChartToMinimalSCXML.h" +#include "uscxml/transform/FlatStateIdentifier.h" +#include "uscxml/Convenience.h" +#include "uscxml/Factory.h" + +#include +#include + +#include + +namespace uscxml { + +using namespace Arabica::XPath; +using namespace Arabica::DOM; + +Transformer ChartToMinimalSCXML::transform(const Interpreter& other) { + return boost::shared_ptr(new ChartToMinimalSCXML(other)); +} + +ChartToMinimalSCXML::ChartToMinimalSCXML(const Interpreter& other) : TransformerImpl(), _retainAsComments(false) { + cloneFrom(other.getImpl()); + + // a bit messy but needed for SCXML IO Processor with session id target + _selfPtr = boost::shared_ptr(this, Deleter()); + Interpreter::addInstance(_selfPtr); +} + +void ChartToMinimalSCXML::writeTo(std::ostream& stream) { + + addMonitor(this); + + { + NodeSet allElements = filterChildType(Node_base::ELEMENT_NODE, _scxml, true); + size_t nrElements = 0; + for (int i = 0; i < allElements.size(); i++) { + if (!isInEmbeddedDocument(allElements[i])) + nrElements++; + } + std::cerr << "Number of elements before reduction: " << nrElements + 1 << std::endl; + } + + // test 278 - move embedded datas to topmost datamodel + if (_binding == EARLY) { + // move all data elements into topmost datamodel element + NodeSet datas = filterChildElements(_nsInfo.xmlNSPrefix + "data", _scxml, true); + + if (datas.size() > 0) { + Node topMostDatamodel; + NodeSet datamodels = filterChildElements(_nsInfo.xmlNSPrefix + "datamodel", _scxml, false); + if (datamodels.size() > 0) { + topMostDatamodel = datamodels[0]; + } else { + topMostDatamodel = _document.createElementNS(_nsInfo.nsURL, "datamodel"); + _scxml.insertBefore(topMostDatamodel, _scxml.getFirstChild()); + } + + while(topMostDatamodel.hasChildNodes()) + topMostDatamodel.removeChild(topMostDatamodel.getFirstChild()); + + for (int i = 0; i < datas.size(); i++) { + if (!isInEmbeddedDocument(datas[i])) { + topMostDatamodel.appendChild(datas[i]); + } + } + } + } + + char* waitForEnv = getenv("USCXML_MINIMIZE_WAIT_MS"); + char* waitForCmpl = getenv("USCXML_MINIMIZE_WAIT_FOR_COMPLETION"); + char* retainAsComments = getenv("USCXML_MINIMIZE_RETAIN_AS_COMMENTS"); + if (retainAsComments != NULL && DOMUtils::attributeIsTrue(retainAsComments)) + _retainAsComments = true; + + long waitFor = -1; + + if (waitForEnv != NULL) { + try { + waitFor = strTo(waitForEnv); + } catch (...) { + waitFor = 0; + } + } + + if (waitForCmpl != NULL && DOMUtils::attributeIsTrue(waitForCmpl)) { + interpret(); + } else { + start(); + if (waitFor < 0) { + // wait for EOF / CTRL+D + char c; + while(true) { + std::cin >> c; + if(std::cin.eof()) + break; + } + } else { + tthread::this_thread::sleep_for(tthread::chrono::milliseconds(waitFor)); + } + } + stop(); + + removeUnvisited(_scxml); + + { + NodeSet allElements = filterChildType(Node_base::ELEMENT_NODE, _scxml, true); + size_t nrElements = 0; + for (int i = 0; i < allElements.size(); i++) { + if (!isInEmbeddedDocument(allElements[i])) + nrElements++; + } + std::cerr << "Number of elements after reduction: " << nrElements + 1 << std::endl; + } + + // unset data model + _dmCopy = DataModel(); + + stream << _scxml; +} + +void ChartToMinimalSCXML::removeUnvisited(Arabica::DOM::Node& node) { + if (node.getNodeType() != Node_base::ELEMENT_NODE) + return; + + Element elem(node); + + if (isInEmbeddedDocument(elem) || + (TAGNAME(elem) == _nsInfo.xmlNSPrefix + "param") || + (TAGNAME(elem) == _nsInfo.xmlNSPrefix + "donedata") || + (TAGNAME(elem) == _nsInfo.xmlNSPrefix + "datamodel") || + (TAGNAME(elem) == _nsInfo.xmlNSPrefix + "data") || + (TAGNAME(elem) == _nsInfo.xmlNSPrefix + "content")) { + return; + } + + // special handling for conditional blocks with if + if (TAGNAME(elem) == _nsInfo.xmlNSPrefix + "if") { + NodeSet ifChilds = filterChildType(Node_base::ELEMENT_NODE, elem, false); + Element lastConditional = elem; + bool hadVisitedChild = false; + for (int j = 0; j < ifChilds.size(); j++) { + Element ifChildElem(ifChilds[j]); + if (TAGNAME(ifChildElem) == _nsInfo.xmlNSPrefix + "else" || TAGNAME(ifChildElem) == _nsInfo.xmlNSPrefix + "elseif") { + if (!hadVisitedChild && HAS_ATTR(lastConditional, "cond")) { + lastConditional.setAttribute("cond", "false"); + } + lastConditional = ifChildElem; + hadVisitedChild = false; + } + if (_visited.find(ifChildElem) != _visited.end()) { + _visited.insert(lastConditional); + hadVisitedChild = true; + } + } + } + + // test344 + if (_dmCopy && + TAGNAME(elem) == _nsInfo.xmlNSPrefix + "transition" && + HAS_ATTR(elem, "cond") && + !_dmCopy.isValidSyntax(ATTR(elem, "cond"))) + return; + + // detach unvisited nodes from DOM + if (_visited.find(node) == _visited.end()) { + std::cout << DOMUtils::xPathForNode(node) << std::endl; + if (_retainAsComments) { + std::stringstream oldContent; + oldContent << node; + node.getParentNode().replaceChild(_document.createComment(boost::replace_all_copy(oldContent.str(),"--", "-")), node); + } else { + // removeChildren is not working as expected + node.getParentNode().replaceChild(_document.createTextNode(""), node); + } + return; + } + + // iterate and remove unvisited children + NodeList children = node.getChildNodes(); + for (int i = 0; i < children.getLength(); i++) { + Node child(children.item(i)); + removeUnvisited(child); + } +} + +void ChartToMinimalSCXML::markAsVisited(const Arabica::DOM::Element& element) { + if (_visited.find(element) != _visited.end()) + return; + + Arabica::DOM::Element elem = const_cast&>(element); + + _visited.insert(element); + Node parent = element.getParentNode(); + if (parent && parent.getNodeType() == Node_base::ELEMENT_NODE) { + Arabica::DOM::Element parentElem(parent); + markAsVisited(parentElem); + } +} + +void ChartToMinimalSCXML::beforeExecutingContent(Interpreter interpreter, const Arabica::DOM::Element& element) { + markAsVisited(element); + StateTransitionMonitor::beforeExecutingContent(interpreter, element); +} + +void ChartToMinimalSCXML::beforeUninvoking(Interpreter interpreter, const Arabica::DOM::Element& invokeElem, const std::string& invokeid) { + markAsVisited(invokeElem); +} + +void ChartToMinimalSCXML::beforeTakingTransition(Interpreter interpreter, const Arabica::DOM::Element& transition, bool moreComing) { + NodeSet targets = getTargetStates(transition); + // we need this for history pseudo states + for (int i = 0; i < targets.size(); i++) { + markAsVisited(Arabica::DOM::Element(targets[i])); + } + markAsVisited(transition); + StateTransitionMonitor::beforeTakingTransition(interpreter, transition, moreComing); +} + +void ChartToMinimalSCXML::beforeEnteringState(Interpreter interpreter, const Arabica::DOM::Element& state, bool moreComing) { + markAsVisited(state); + StateTransitionMonitor::beforeEnteringState(interpreter, state, moreComing); +} + +void ChartToMinimalSCXML::beforeInvoking(Interpreter interpreter, const Arabica::DOM::Element& invokeElem, const std::string& invokeid) { + markAsVisited(invokeElem); +} + +void ChartToMinimalSCXML::beforeCompletion(Interpreter interpreter) { + _dmCopy = _dataModel; // retain a copy; +} + +void ChartToMinimalSCXML::executeContent(const Arabica::DOM::Element& content, bool rethrow) { + markAsVisited(content); + InterpreterRC::executeContent(content, rethrow); +} + +void ChartToMinimalSCXML::invoke(const Arabica::DOM::Element& element) { + markAsVisited(element); + InterpreterRC::invoke(element); +} + +void ChartToMinimalSCXML::cancelInvoke(const Arabica::DOM::Element& element) { + markAsVisited(element); + InterpreterRC::cancelInvoke(element); +} + +} \ No newline at end of file diff --git a/src/uscxml/transform/ChartToMinimalSCXML.h b/src/uscxml/transform/ChartToMinimalSCXML.h new file mode 100644 index 0000000..31dfd64 --- /dev/null +++ b/src/uscxml/transform/ChartToMinimalSCXML.h @@ -0,0 +1,84 @@ +/** + * @file + * @author 2012-2014 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 CHARTTOMINIMALSCXML_H_7B97677A +#define CHARTTOMINIMALSCXML_H_7B97677A + +#include "uscxml/DOMUtils.h" +#include "uscxml/interpreter/InterpreterRC.h" +#include +#include +#include +#include +#include +#include + +#include "Transformer.h" + +namespace uscxml { + +class USCXML_API ChartToMinimalSCXML : public InterpreterRC, public StateTransitionMonitor, public TransformerImpl { +public: + virtual ~ChartToMinimalSCXML() {} + static Transformer transform(const Interpreter& other); + + // InterpreterMonitor + virtual void beforeExecutingContent(Interpreter interpreter, const Arabica::DOM::Element& element); + virtual void beforeUninvoking(Interpreter interpreter, const Arabica::DOM::Element& invokeElem, const std::string& invokeid); + virtual void beforeTakingTransition(Interpreter interpreter, const Arabica::DOM::Element& transition, bool moreComing); + virtual void beforeEnteringState(Interpreter interpreter, const Arabica::DOM::Element& state, bool moreComing); + virtual void beforeInvoking(Interpreter interpreter, const Arabica::DOM::Element& invokeElem, const std::string& invokeid); + virtual void beforeCompletion(Interpreter interpreter); + + // gather executable content per microstep + void executeContent(const Arabica::DOM::Element& content, bool rethrow = false); + + // invoke and uninvoke + virtual void invoke(const Arabica::DOM::Element& element); + virtual void cancelInvoke(const Arabica::DOM::Element& element); + +protected: + void writeTo(std::ostream& stream); + + ChartToMinimalSCXML(const Interpreter& other); + + void markAsVisited(const Arabica::DOM::Element& element); + void removeUnvisited(Arabica::DOM::Node& node); + + std::set > _visited; + DataModel _dmCopy; + bool _retainAsComments; + +private: + // we need this to register as an instance at Interpreter::_instances + boost::shared_ptr _selfPtr; + + // prevent deletion from shared_ptr + class Deleter { + public: + void operator()(ChartToMinimalSCXML* p) { /* do nothing */ } + }; + friend class ChartToMinimalSCXML; + +}; + +} + + +#endif /* end of include guard: CHARTTOMINIMALSCXML_H_7B97677A */ diff --git a/src/uscxml/transform/ChartToPromela.cpp b/src/uscxml/transform/ChartToPromela.cpp index dba8d90..3e920be 100644 --- a/src/uscxml/transform/ChartToPromela.cpp +++ b/src/uscxml/transform/ChartToPromela.cpp @@ -418,7 +418,7 @@ void PromelaCodeAnalyzer::addCode(const std::string& code, ChartToPromela* inter case PML_NAME: { _typeDefs.types[node->value].occurrences.insert(interpreter); _typeDefs.types[node->value].minValue = 0; - _typeDefs.types[node->value].maxValue = 1; + _typeDefs.types[node->value].maxValue = 0; // test325 if (node->value.compare("_ioprocessors") == 0) { addCode("_ioprocessors.scxml.location", interpreter); @@ -717,7 +717,7 @@ void ChartToPromela::writeStates(std::ostream& stream) { } void ChartToPromela::writeStateMap(std::ostream& stream) { - stream << "/* macros for original state names */" << std::endl; + stream << "/* original state names */" << std::endl; std::map origStates = _analyzer->getOrigStates(); for (std::map::iterator origIter = origStates.begin(); origIter != origStates.end(); origIter++) { stream << "#define " << _analyzer->macroForLiteral(origIter->first) << " " << origIter->second; @@ -737,24 +737,23 @@ void ChartToPromela::writeStateMap(std::ostream& stream) { } void ChartToPromela::writeHistoryArrays(std::ostream& stream) { - stream << "/* history assignments */" << std::endl; std::map >::iterator histNameIter = _historyMembers.begin(); while(histNameIter != _historyMembers.end()) { - stream << "bool _hist_" << boost::to_lower_copy(histNameIter->first) << "[" << histNameIter->second.size() << "];"; - - stream << " /* "; + stream << "/* history assignments for " << histNameIter->first << std::endl; std::map::iterator histMemberIter = histNameIter->second.begin(); while(histMemberIter != histNameIter->second.end()) { - stream << " " << histMemberIter->second << ":" << histMemberIter->first; + stream << " " << histMemberIter->second << ": " << histMemberIter->first << std::endl;; histMemberIter++; } - stream << " */" << std::endl; + stream << "*/" << std::endl; + stream << "bool " << _prefix << "_hist_" << boost::replace_all_copy(boost::to_lower_copy(histNameIter->first), ".", "_") << "[" << histNameIter->second.size() << "];" << std::endl; + histNameIter++; } } void ChartToPromela::writeTypeDefs(std::ostream& stream) { - stream << "/* typedefs */" << std::endl; + stream << "/* type definitions */" << std::endl; PromelaCodeAnalyzer::PromelaTypedef typeDefs = _analyzer->getTypes(); if (typeDefs.types.size() == 0) return; @@ -930,7 +929,7 @@ std::string ChartToPromela::conditionalizeForHist(const std::setsecond.end()) { assert(_historyMembers.find(relevanthistIter->first) != _historyMembers.end()); assert(_historyMembers[relevanthistIter->first].find(*histItemIter) != _historyMembers[relevanthistIter->first].end()); - condition << itemSep << "_hist_" << boost::to_lower_copy(_analyzer->macroForLiteral(relevanthistIter->first)) << "[" << _historyMembers[relevanthistIter->first][*histItemIter] << "]"; + condition << itemSep << _prefix << "_hist_" << boost::to_lower_copy(_analyzer->macroForLiteral(relevanthistIter->first)) << "[" << _historyMembers[relevanthistIter->first][*histItemIter] << "]"; itemSep = " && "; histItemIter++; } @@ -945,7 +944,23 @@ std::string ChartToPromela::conditionalizeForHist(const std::set ChartToPromela::getTransientContent(GlobalTransition* transition) { +// std::list content; +// GlobalTransition* currTrans = transition; +// for (;;) { +// if (!HAS_ATTR(currState, "transient") || !DOMUtils::attributeIsTrue(ATTR(currState, "transient"))) +// break; +// content.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "invoke", currState)); +// content.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "onentry", currState)); +// content.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "onexit", currState)); +// NodeSet transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", currState); +// currState = _globalConf[ATTR_CAST(transitions[0], "target")]; +// } +// +// return content; +//} + void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* transition, int indent) { std::string padding; for (int i = 0; i < indent; i++) { @@ -953,19 +968,24 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra } stream << std::endl << _prefix << "t" << transition->index << ": /* ######################## " << std::endl; - stream << " from state: "; FlatStateIdentifier flatActiveSource(transition->source); + stream << " from state: "; PRETTY_PRINT_LIST(stream, flatActiveSource.getActive()); stream << std::endl; - stream << " on event: " << (transition->eventDesc.size() > 0 ? transition->eventDesc : "SPONTANEOUS") << std::endl; + stream << " with history: " << flatActiveSource.getFlatHistory() << std::endl; + stream << " ----- on event: " << (transition->eventDesc.size() > 0 ? transition->eventDesc : "SPONTANEOUS") << " --" << std::endl; + stream << " to state: "; + FlatStateIdentifier flatActiveDest(transition->destination); + PRETTY_PRINT_LIST(stream, flatActiveDest.getActive()); + stream << std::endl; + stream << " with history: " << flatActiveDest.getFlatHistory() << std::endl; + stream << "############################### */" << std::endl; stream << std::endl; - stream << padding << "atomic {" << std::endl; -// stream << padding << " if" << std::endl; -// stream << padding << " :: " << _prefix << "done -> goto " << _prefix << "terminate;" << std::endl; -// stream << padding << " :: else -> skip;" << std::endl; -// stream << padding << " fi" << std::endl; + stream << padding << "skip;" << std::endl; + stream << padding << "d_step {" << std::endl; + stream << padding << " printf(\"Taking Transition " << _prefix << "t" << transition->index << "\\n\");" << std::endl; padding += " "; indent++; @@ -1099,18 +1119,24 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra if (action.transition) { // this is executable content from a transition + stream << std::endl << "/* executable content for transition */" << std::endl; writeExecutableContent(stream, action.transition, indent); // continue; } if (action.onExit) { +// std::cout<< action.onExit << std::endl; // executable content from an onexit element + if (action.onExit.getParentNode()) // this should not be necessary? + stream << std::endl << "/* executable content for exiting state " << ATTR_CAST(action.onExit.getParentNode(), "id") << " */" << std::endl; writeExecutableContent(stream, action.onExit, indent); // continue; } if (action.onEntry) { // executable content from an onentry element + if (action.onEntry.getParentNode()) // this should not be necessary? + stream << std::endl << "/* executable content for entering state " << ATTR_CAST(action.onEntry.getParentNode(), "id") << " */" << std::endl; writeExecutableContent(stream, action.onEntry, indent); // continue; } @@ -1183,10 +1209,13 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra if (_machines.find(action.uninvoke) != _machines.end()) { // nested SCXML document stream << padding << _machines[action.uninvoke]->_prefix << "canceled = true;" << std::endl; - writeRemovePendingEventsFromInvoker(stream, _machines[action.uninvoke], indent, false); + if (_analyzer->usesEventField("delay")) + stream << padding << "removePendingEventsForInvoker(" << _analyzer->macroForLiteral(_machines[action.uninvoke]->_invokerid) << ");" << std::endl; +// writeRemovePendingEventsFromInvoker(stream, _machines[action.uninvoke], indent, false); #if 0 stream << padding << "do" << std::endl; - stream << padding << ":: len(" << _machines[action.uninvoke]->_prefix << "tmpQ) > 0 -> " << _machines[action.uninvoke]->_prefix << "tmpQ?_;" << std::endl; + if (_allowEventInterleaving) + stream << padding << ":: len(" << _machines[action.uninvoke]->_prefix << "tmpQ) > 0 -> " << _machines[action.uninvoke]->_prefix << "tmpQ?_;" << std::endl; stream << padding << ":: len(" << _machines[action.uninvoke]->_prefix << "eQ) > 0 -> " << _machines[action.uninvoke]->_prefix << "eQ?_;" << std::endl; stream << padding << ":: else -> break;" << std::endl; stream << padding << "od" << std::endl; @@ -1247,7 +1276,7 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra stream << padding << " " << _prefix << "s = s" << histNewState->activeIndex << ";" << std::endl; - writeTransitionClosure(stream, *histTargetIter->second.begin(), histNewState, indent + 1); // is this correct for everyone in set? +// writeTransitionClosure(stream, *histTargetIter->second.begin(), histNewState, indent + 1); // is this correct for everyone in set? stream << padding << "}" << std::endl; hasHistoryTarget = true; @@ -1261,17 +1290,13 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra origNewState = _activeConf[transition->activeDestination]; assert(origNewState != NULL); - - + stream << std::endl << "/* to state "; - FlatStateIdentifier flatActiveDest(transition->activeDestination); PRETTY_PRINT_LIST(stream, flatActiveDest.getActive()); stream << " */" << std::endl; stream << padding << _prefix << "s = s" << origNewState->activeIndex << ";" << std::endl; - writeTransitionClosure(stream, transition, origNewState, indent); - if (hasHistoryTarget) { padding = padding.substr(2); indent--; @@ -1279,9 +1304,12 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra stream << padding << "fi;" << std::endl; } + // moved up here for goto from d_step padding = padding.substr(2); stream << padding << "}" << std::endl; + writeTransitionClosure(stream, transition, origNewState, indent-1); + } void ChartToPromela::writeHistoryAssignments(std::ostream& stream, GlobalTransition* transition, int indent) { @@ -1366,7 +1394,7 @@ void ChartToPromela::writeHistoryAssignments(std::ostream& stream, GlobalTransit while(forgetIter != histClassIter->toForget.end()) { std::set::iterator forgetMemberIter = forgetIter->second.begin(); while(forgetMemberIter != forgetIter->second.end()) { - stream << padding << "_hist_" << boost::to_lower_copy(_analyzer->macroForLiteral(forgetIter->first)); + stream << padding << _prefix << "_hist_" << boost::to_lower_copy(_analyzer->macroForLiteral(forgetIter->first)); stream << "[" << _historyMembers[forgetIter->first][*forgetMemberIter] << "] = 0;"; stream << " \t/* " << *forgetMemberIter << " */" << std::endl; forgetMemberIter++; @@ -1380,7 +1408,7 @@ void ChartToPromela::writeHistoryAssignments(std::ostream& stream, GlobalTransit while(rememberIter != histClassIter->toRemember.end()) { std::set::iterator rememberMemberIter = rememberIter->second.begin(); while(rememberMemberIter != rememberIter->second.end()) { - stream << padding << "_hist_" << boost::to_lower_copy(_analyzer->macroForLiteral(rememberIter->first)); + stream << padding << _prefix << "_hist_" << boost::to_lower_copy(_analyzer->macroForLiteral(rememberIter->first)); stream << "[" << _historyMembers[rememberIter->first][*rememberMemberIter] << "] = 1;"; stream << " \t/* " << *rememberMemberIter << " */" << std::endl; rememberMemberIter++; @@ -1586,12 +1614,16 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: std::string seperator; if (label.size() > 0) { - formatString += label + ": "; + if (expr.size() > 0) { + formatString += label + ": "; + } else { + formatString += label; + } } if (isStringLiteral) { formatString += expr; - } else { + } else if (expr.size() > 0) { formatString += "%d"; varString += seperator + expr; } @@ -1612,8 +1644,8 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: writeExecutableContent(stream, child, indent + 1); child = child.getNextSibling(); } - if (HAS_ATTR(nodeElem, "index")) - stream << padding << " " << _prefix << ATTR(nodeElem, "index") << "++;" << std::endl; +// if (HAS_ATTR(nodeElem, "index")) +// stream << padding << " " << _prefix << ATTR(nodeElem, "index") << "++;" << std::endl; stream << padding << "}" << std::endl; } else if(TAGNAME(nodeElem) == "if") { @@ -1627,14 +1659,18 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: } else if(TAGNAME(nodeElem) == "assign") { NodeSet assignTexts = filterChildType(Node_base::TEXT_NODE, nodeElem, true); assert(assignTexts.size() > 0); - stream << ADAPT_SRC(boost::trim_copy(assignTexts[0].getNodeValue())) << std::endl; + stream << beautifyIndentation(ADAPT_SRC(boost::trim_copy(assignTexts[0].getNodeValue())), indent) << std::endl; } else if(TAGNAME(nodeElem) == "send" || TAGNAME(nodeElem) == "raise") { std::string targetQueue; if (TAGNAME(nodeElem) == "raise") { targetQueue = _prefix + "iQ!"; } else if (!HAS_ATTR(nodeElem, "target")) { - targetQueue = _prefix + "tmpQ!"; + if (_allowEventInterleaving) { + targetQueue = _prefix + "tmpQ!"; + } else { + targetQueue = _prefix + "eQ!"; + } } else if (ATTR(nodeElem, "target").compare("#_internal") == 0) { targetQueue = _prefix + "iQ!"; } else if (ATTR(nodeElem, "target").compare("#_parent") == 0) { @@ -1663,13 +1699,13 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: stream << padding << " tmpE.sendid = _lastSendId;" << std::endl; stream << padding << " if" << std::endl; stream << padding << " :: _lastSendId == 2147483647 -> _lastSendId = 0;" << std::endl; - stream << padding << " :: timeout -> skip;" << std::endl; + stream << padding << " :: else -> skip;" << std::endl; stream << padding << " fi;" << std::endl; } else if (HAS_ATTR(nodeElem, "id")) { stream << padding << " tmpE.sendid = " << _analyzer->macroForLiteral(ATTR(nodeElem, "id")) << ";" << std::endl; } - if (_invokerid.length() > 0 && !boost::starts_with(targetQueue, _prefix)) { // do not send invokeid if we send / raise to ourself + if (_invokerid.length() > 0) { // do not send invokeid if we send / raise to ourself stream << padding << " tmpE.invokeid = " << _analyzer->macroForLiteral(_invokerid) << ";" << std::endl; } @@ -1733,82 +1769,17 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: } } } else if(TAGNAME(nodeElem) == "cancel") { - writeCancelWithIdOrExpr(stream, nodeElem, this, indent); + if (HAS_ATTR(nodeElem, "sendid")) { + stream << padding << "cancelSendId(" << _analyzer->macroForLiteral(ATTR(nodeElem, "sendid")) << "," << (_invokerid.size() > 0 ? _analyzer->macroForLiteral(_invokerid) : "0") << ");" << std::endl; + } else if (HAS_ATTR(nodeElem, "sendidexpr")) { + stream << padding << "cancelSendId(" << ADAPT_SRC(ATTR(nodeElem, "sendidexpr")) << "," << (_invokerid.size() > 0 ? _analyzer->macroForLiteral(_invokerid) : "0") << ");" << std::endl; + } } else { std::cerr << "'" << TAGNAME(nodeElem) << "'" << std::endl << nodeElem << std::endl; assert(false); } } -void ChartToPromela::writeCancelWithIdOrExpr(std::ostream& stream, const Arabica::DOM::Element& cancel, ChartToPromela* invoker, int indent) { - std::string padding; - for (int i = 0; i < indent; i++) { - padding += " "; - } - - ChartToPromela* topMachine = (invoker->_parent != NULL ? invoker->_parent : invoker); - - std::list others; - others.push_back(topMachine); - for (std::map, ChartToPromela*>::iterator queueIter = topMachine->_machines.begin(); queueIter != topMachine->_machines.end(); queueIter++) { - others.push_back(queueIter->second); - } - - if (HAS_ATTR(cancel, "sendid")) { - stream << padding << "/* cancel event given by sendid */" << std::endl; - stream << padding << "atomic {" << std::endl; - stream << padding << " _event_t tmpE;" << std::endl; - stream << padding << " do" << std::endl; - for (std::list::iterator queueIter = others.begin(); queueIter != others.end(); queueIter++) { - stream << padding << " :: " << (*queueIter)->_prefix << "eQ?\?" << (_analyzer->usesEventField("delay") ? "tmpE.delay, tmpE.seqNr," : "") << " tmpE.name, " << _analyzer->macroForLiteral(ATTR(cancel, "sendid")) << ";" << std::endl; - stream << padding << " :: " << (*queueIter)->_prefix << "tmpQ?\?" << (_analyzer->usesEventField("delay") ? "tmpE.delay, tmpE.seqNr," : "") << " tmpE.name, " << _analyzer->macroForLiteral(ATTR(cancel, "sendid")) << ";" << std::endl; - } - stream << padding << " :: else -> break;" << std::endl; - stream << padding << " od" << std::endl; - stream << padding << "}" << std::endl; - - } else if (HAS_ATTR(cancel, "sendidexpr")) { - stream << padding << "/* cancel event given by sendidexpr */" << std::endl; - stream << padding << "atomic {" << std::endl; - stream << padding << " _event_t tmpE;" << std::endl; - - stream << padding << " do" << std::endl; - stream << padding << " :: (len(" << _prefix << "tmpQ) > 0) -> { " << _prefix << "tmpQ?tmpE; sendIdQ!tmpE; }" << std::endl; - stream << padding << " :: else -> break;" << std::endl; - stream << padding << " od" << std::endl; - - stream << padding << " do" << std::endl; - stream << padding << " :: (len(sendIdQ) > 0) -> {" << std::endl; - stream << padding << " sendIdQ?tmpE;" << std::endl; - stream << padding << " if" << std::endl; - stream << padding << " :: (tmpE.sendid != " << ADAPT_SRC(ATTR(cancel, "sendidexpr")) << ") -> " << _prefix << "tmpQ!tmpE" << std::endl; - stream << padding << " :: else -> skip;" << std::endl; - stream << padding << " fi" << std::endl; - stream << padding << " }" << std::endl; - stream << padding << " :: else -> break;" << std::endl; - stream << padding << " od" << std::endl; - - for (std::list::iterator queueIter = others.begin(); queueIter != others.end(); queueIter++) { - stream << padding << " do" << std::endl; - stream << padding << " :: (len(" << (*queueIter)->_prefix << "eQ) > 0) -> { " << (*queueIter)->_prefix << "eQ?tmpE; sendIdQ!tmpE; }" << std::endl; - stream << padding << " :: else -> break;" << std::endl; - stream << padding << " od" << std::endl; - - stream << padding << " do" << std::endl; - stream << padding << " :: (len(sendIdQ) > 0) -> {" << std::endl; - stream << padding << " sendIdQ?tmpE;" << std::endl; - stream << padding << " if" << std::endl; - stream << padding << " :: (tmpE.sendid != " << ADAPT_SRC(ATTR(cancel, "sendidexpr")) << ") -> " << (*queueIter)->_prefix << "eQ!tmpE" << std::endl; - stream << padding << " :: else -> skip;" << std::endl; - stream << padding << " fi" << std::endl; - stream << padding << " }" << std::endl; - stream << padding << " :: else -> break;" << std::endl; - stream << padding << " od" << std::endl; - } - stream << padding << "}" << std::endl; - } - -} PromelaInlines PromelaInlines::fromNodeSet(const NodeSet& node, bool recurse) { PromelaInlines allPromInls; @@ -2012,7 +1983,7 @@ void ChartToPromela::writeStrings(std::ostream& stream) { void ChartToPromela::writeDeclarations(std::ostream& stream) { - stream << "/* global variables */" << std::endl; + stream << "/* global variables " << (_prefix.size() > 0 ? "for " + _prefix : "") << " */" << std::endl; // we cannot know our event queue with nested invokers? Adding some for test422 size_t tolerance = 6; @@ -2023,14 +1994,15 @@ void ChartToPromela::writeDeclarations(std::ostream& stream) { stream << "unsigned " << _prefix << "s : " << BIT_WIDTH(_activeConf.size() + 1) << "; /* current state */" << std::endl; stream << "chan " << _prefix << "iQ = [" << MAX(_internalQueueLength, 1) << "] of {_event_t} /* internal queue */" << std::endl; stream << "chan " << _prefix << "eQ = [" << _externalQueueLength + tolerance << "] of {_event_t} /* external queue */" << std::endl; - stream << "chan " << _prefix << "tmpQ = [" << MAX(_externalQueueLength + tolerance, 1) << "] of {_event_t} /* temporary queue for external events in transitions */" << std::endl; -// stream << "hidden " << "_event_t " << _prefix << "tmpQItem;" << std::endl; + if (_allowEventInterleaving) + stream << "chan " << _prefix << "tmpQ = [" << MAX(_externalQueueLength + tolerance, 1) << "] of {_event_t} /* temporary queue for external events in transitions */" << std::endl; } else { stream << "unsigned " << _prefix << "_event : " << BIT_WIDTH(_analyzer->getEvents().size() + 1) << "; /* current event */" << std::endl; stream << "unsigned " << _prefix << "s : " << BIT_WIDTH(_activeConf.size() + 1) << "; /* current state */" << std::endl; stream << "chan " << _prefix << "iQ = [" << MAX(_internalQueueLength, 1) << "] of {int} /* internal queue */" << std::endl; stream << "chan " << _prefix << "eQ = [" << _externalQueueLength + tolerance << "] of {int} /* external queue */" << std::endl; - stream << "chan " << _prefix << "tmpQ = [" << MAX(_externalQueueLength + tolerance, 1) << "] of {int} /* temporary queue for external events in transitions */" << std::endl; + if (_allowEventInterleaving) + stream << "chan " << _prefix << "tmpQ = [" << MAX(_externalQueueLength + tolerance, 1) << "] of {int} /* temporary queue for external events in transitions */" << std::endl; // stream << "hidden unsigned " << _prefix << "tmpQItem : " << BIT_WIDTH(_analyzer->getEvents().size() + 1) << ";" << std::endl; } if (_machines.size() > 0) { @@ -2051,11 +2023,11 @@ void ChartToPromela::writeDeclarations(std::ostream& stream) { if (_prefix.size() == 0 || _prefix == "MAIN_") { if (_analyzer->usesEventField("sendid")) { stream << "chan sendIdQ = [" << MAX(_externalQueueLength + 1, 1) << "] of {_event_t} /* temporary queue to cancel events per sendidexpr */" << std::endl; - stream << "hidden int _lastSendId = 0; /* sequential counter for send ids */"; + stream << "hidden int _lastSendId = 0; /* sequential counter for send ids */" << std::endl; } if (_analyzer->usesEventField("delay")) { - stream << "hidden int _lastSeqId = 0; /* sequential counter for delayed events */"; + stream << "hidden int _lastSeqId = 0; /* sequential counter for delayed events */" << std::endl; } } // if (_analyzer->usesPlatformVars()) { @@ -2181,7 +2153,8 @@ void ChartToPromela::writeDeclarations(std::ostream& stream) { } stream << std::endl; - stream << "/* event sources */" << std::endl; + if (_globalEventSource || _invokers.size() > 0) + stream << "/* event sources */" << std::endl; if (_globalEventSource) { _globalEventSource.writeDeclarations(stream); @@ -2220,7 +2193,7 @@ void ChartToPromela::writeStartInvoker(std::ostream& stream, const Arabica::DOM: std::list namelist = tokenize(ATTR_CAST(node, "namelist")); for (std::list::iterator nlIter = namelist.begin(); nlIter != namelist.end(); nlIter++) { if (invoker->_dataModelVars.find(*nlIter) != invoker->_dataModelVars.end()) { - stream << padding << invoker->_prefix << *nlIter << " = " << _prefix << *nlIter << std::endl; + stream << padding << invoker->_prefix << *nlIter << " = " << _prefix << *nlIter << ";" << std::endl; } } } @@ -2254,14 +2227,16 @@ void ChartToPromela::writeFSM(std::ostream& stream) { // transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", _startState); // assert(transitions.size() == 1); - stream << std::endl << "/* global scripts */" << std::endl; NodeSet scripts = filterChildElements(_nsInfo.xmlNSPrefix + "script", _scxml, false); - for (int i = 0; i < scripts.size(); i++) { - writeExecutableContent(stream, scripts[i], 1); + if (scripts.size() > 0) { + stream << std::endl << "/* global scripts */" << std::endl; + for (int i = 0; i < scripts.size(); i++) { + writeExecutableContent(stream, scripts[i], 1); + } + stream << std::endl; } - stream << std::endl; - - stream << "/* transition to initial state */" << std::endl; + + stream << std::endl << "/* 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); @@ -2281,77 +2256,40 @@ void ChartToPromela::writeFSM(std::ostream& stream) { } stream << std::endl; - stream << _prefix << "macroStep:" << std::endl; - stream << " /* push send events to external queue */" << 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 { - stream << " :: len(" << _prefix << "tmpQ) != 0 -> { " << _prefix << "tmpQ?" << _prefix << "_event; " << _prefix << "eQ!" << _prefix << "_event }" << std::endl; + stream << _prefix << "macroStep: skip;" << std::endl; + if (_allowEventInterleaving) { + stream << " /* push send events to external queue */" << 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 { + stream << " :: len(" << _prefix << "tmpQ) != 0 -> { " << _prefix << "tmpQ?" << _prefix << "_event; " << _prefix << "eQ!" << _prefix << "_event }" << std::endl; + } + stream << " :: else -> break;" << std::endl; + stream << " od;" << std::endl << std::endl; } - stream << " :: else -> break;" << std::endl; - stream << " od;" << std::endl << std::endl; - + if (_machines.size() > 0) { stream << " /* start pending invokers */" << std::endl; stream << " int invokerId;" << std::endl; stream << " do" << std::endl; stream << " :: " << _prefix << "start?invokerId -> {" << std::endl; - stream << " if " << std::endl; + stream << " if " << std::endl; for (std::map, ChartToPromela*>::iterator machIter = _machines.begin(); machIter != _machines.end(); machIter++) { - stream << " :: invokerId == " << _analyzer->macroForLiteral(machIter->second->_invokerid) << " -> {" << std::endl; - writeStartInvoker(stream, machIter->first, machIter->second, 2); - stream << " }" << std::endl; + stream << " :: invokerId == " << _analyzer->macroForLiteral(machIter->second->_invokerid) << " -> {" << std::endl; + writeStartInvoker(stream, machIter->first, machIter->second, 3); + stream << " }" << std::endl; } - stream << " :: else -> skip; " << std::endl; - stream << " fi " << std::endl; - stream << " } " << std::endl; - stream << " :: else -> break;" << std::endl; - stream << " od" << std::endl; - } - - if (_analyzer->usesEventField("delay")) { - stream << " /* find machine with next event due */" << std::endl; - stream << " if" << std::endl; - stream << " :: len(" << _prefix << "iQ) != 0 -> skip; /* internal queue not empty -> do not reduce our priority */" << std::endl; - stream << " :: " << _prefix << "eQ?\? <0> -> skip; /* at least one event without delay -> do not reduce our priority */" << std::endl; - stream << " :: timeout -> { "<< std::endl; - // stream << " /* determine queue with shortest delay in front */" << std::endl; - stream << " atomic {" << std::endl; - stream << " int nextPid;" << std::endl; - stream << " int lowestDelay = 0;" << std::endl; - stream << " _event_t tmpE;" << std::endl; - - for (std::map, ChartToPromela*>::iterator queueIter = _machinesAll->begin(); queueIter != _machinesAll->end(); queueIter++) { - std::list queues; - queues.push_back("eQ"); - queues.push_back("tmpQ"); - for (std::list::iterator qIter = queues.begin(); qIter != queues.end(); qIter++) { - stream << " if" << std::endl; - stream << " :: len(" << queueIter->second->_prefix << *qIter << ") > 0 -> {" << std::endl; - stream << " " << queueIter->second->_prefix << *qIter << "?;" << std::endl; - stream << " if" << std::endl; - stream << " :: (tmpE.delay < lowestDelay || lowestDelay == 0) -> {" << std::endl; - stream << " lowestDelay = tmpE.delay;" << std::endl; - stream << " nextPid = " << queueIter->second->_prefix << "procid;" << std::endl; - stream << " }" << std::endl; - stream << " :: else -> skip;" << std::endl; - stream << " fi;" << std::endl; - stream << " }" << std::endl; - stream << " :: else -> skip;;" << std::endl; - stream << " fi;" << std::endl; - } - } - - stream << " set_priority(nextPid, 10);" << std::endl; - stream << " if" << std::endl; - stream << " :: (nextPid != _pid) -> set_priority(_pid, 1);" << std::endl; - stream << " :: else -> skip;" << std::endl; - stream << " fi;" << std::endl; - stream << " }" << std::endl; + stream << " :: else -> skip; " << std::endl; + stream << " fi " << std::endl; stream << " }" << std::endl; - stream << " fi;" << std::endl; - stream << " set_priority(_pid, 10);" << std::endl << std::endl; + stream << " :: else -> break;" << std::endl; + stream << " od" << std::endl << std::endl; + } + + if (_analyzer->usesEventField("delay") && _machinesAll->size() > 1) { + stream << "/* Determine machines with smallest delay and set their process priority */" << std::endl; + stream << " scheduleMachines();" << std::endl << std::endl; } stream << " /* pop an event */" << std::endl; @@ -2359,7 +2297,21 @@ void ChartToPromela::writeFSM(std::ostream& stream) { stream << " :: len(" << _prefix << "iQ) != 0 -> " << _prefix << "iQ ? " << _prefix << "_event /* from internal queue */" << std::endl; stream << " :: else -> " << _prefix << "eQ ? " << _prefix << "_event /* from external queue */" << std::endl; stream << " fi;" << std::endl << std::endl; - + +#if 0 + if (!_analyzer->usesComplexEventStruct()) { + stream << " printf(\"======= Process %d dequeued %d\\n\", _pid, " << _prefix << "_event);" << std::endl; + } else { + stream << " printf(\"======= Process %d dequeued %d\\n\", _pid, " << _prefix << "_event.name);" << std::endl; + if (_analyzer->usesEventField("sendid")) + stream << " printf(\" sendid: %d\\n\", " << _prefix << "_event.sendid);" << std::endl; + if (_analyzer->usesEventField("invokeid")) + stream << " printf(\" invokeid: %d\\n\", " << _prefix << "_event.invokeid);" << std::endl; + if (_analyzer->usesEventField("delay")) + stream << " printf(\" delay: %d\\n\", " << _prefix << "_event.delay);" << std::endl; + } + stream << std::endl; +#endif stream << " /* terminate if we are stopped */" << std::endl; stream << " if" << std::endl; stream << " :: " << _prefix << "done -> goto " << _prefix << "terminate;" << std::endl; @@ -2396,13 +2348,13 @@ void ChartToPromela::writeFSM(std::ostream& stream) { } #endif - stream << " /* autoforward to respective invokers */" << std::endl; for (std::map, ChartToPromela*>::iterator invIter = _machines.begin(); invIter != _machines.end(); invIter++) { if (invIter->second == this) { continue; } //std::cout << invIter->first << std::endl; if (DOMUtils::attributeIsTrue(ATTR_CAST(invIter->first, "autoforward"))) { + stream << " /* autoforward event to " << invIter->second->_invokerid << " invokers */" << std::endl; stream << " if" << std::endl; stream << " :: " << invIter->second->_prefix << "done -> skip;" << std::endl; stream << " :: " << invIter->second->_prefix << "canceled -> skip;" << std::endl; @@ -2442,8 +2394,8 @@ void ChartToPromela::writeFSM(std::ostream& stream) { } stream << " }" << std::endl; stream << _prefix << "cancel: skip;" << std::endl; - writeRemovePendingEventsFromInvoker(stream, this, 1, true); - + if (_analyzer->usesEventField("delay")) + stream << " removePendingEventsForInvoker(" << _analyzer->macroForLiteral(this->_invokerid) << ")" << std::endl; } // stop all event sources @@ -2459,53 +2411,217 @@ void ChartToPromela::writeFSM(std::ostream& stream) { stream << "}" << std::endl; } -void ChartToPromela::writeRemovePendingEventsFromInvoker(std::ostream& stream, ChartToPromela* invoker, int indent, bool atomic) { +void ChartToPromela::writeRescheduleProcess(std::ostream& stream, int indent) { std::string padding; for (int i = 0; i < indent; i++) { padding += " "; } - if (!invoker || !invoker->_parent) - return; + if (_allowEventInterleaving) { + stream << padding << "inline rescheduleProcess(smallestDelay, procId, internalQ, externalQ, tempQ) {" << std::endl; + } else { + stream << padding << "inline rescheduleProcess(smallestDelay, procId, internalQ, externalQ) {" << std::endl; + } + stream << padding << " _event_t tmpEvent;" << std::endl; + + stream << padding << " set_priority(procId, 1);" << std::endl; + stream << padding << " if" << std::endl; + stream << padding << " :: len(internalQ) > 0 -> set_priority(procId, 10);" << std::endl; + stream << padding << " :: else {" << std::endl; + stream << padding << " if" << std::endl; + + stream << padding << " :: len(externalQ) > 0 -> {" << std::endl; + stream << padding << " externalQ?;" << std::endl; + stream << padding << " if" << std::endl; + stream << padding << " :: smallestDelay == tmpEvent.delay -> set_priority(procId, 10);" << std::endl; + stream << padding << " :: else -> skip;" << std::endl; + stream << padding << " fi;" << std::endl; + stream << padding << " }" << std::endl; + + if (_allowEventInterleaving) { + stream << padding << " :: len(tempQ) > 0 -> {" << std::endl; + stream << padding << " tempQ?;" << std::endl; + stream << padding << " if" << std::endl; + stream << padding << " :: smallestDelay == tmpEvent.delay -> set_priority(procId, 10);" << std::endl; + stream << padding << " :: else -> skip;" << std::endl; + stream << padding << " fi;" << std::endl; + stream << padding << " }" << std::endl; + } + + stream << padding << " :: else -> skip;" << std::endl; + stream << padding << " fi;" << std::endl; + stream << padding << " }" << std::endl; + stream << padding << " fi;" << std::endl; + stream << padding << "}" << std::endl; +} + +void ChartToPromela::writeDetermineShortestDelay(std::ostream& stream, int indent) { + std::string padding; + for (int i = 0; i < indent; i++) { + padding += " "; + } + + stream << padding << "inline determineSmallestDelay(smallestDelay, queue) {" << std::endl; + stream << padding << " _event_t tmpEvent;" << std::endl; + stream << padding << " if" << std::endl; + stream << padding << " :: len(queue) > 0 -> {" << std::endl; + stream << padding << " queue?;" << std::endl; + stream << padding << " if" << std::endl; + stream << padding << " :: (tmpEvent.delay < smallestDelay) -> { smallestDelay = tmpEvent.delay; }" << std::endl; + stream << padding << " :: else -> skip;" << std::endl; + stream << padding << " fi;" << std::endl; + stream << padding << " }" << std::endl; + stream << padding << " :: else -> skip;" << std::endl; + stream << padding << " fi;" << std::endl; + stream << padding << "}" << std::endl; +} + +void ChartToPromela::writeAdvanceTime(std::ostream& stream, int indent) { + std::string padding; + for (int i = 0; i < indent; i++) { + padding += " "; + } - if (_analyzer->usesEventField("delay")) { - if (atomic) { - stream << padding << "atomic {" << std::endl; - } else { - stream << padding << "{" << std::endl; - } - stream << padding << " /* remove all this invoker's pending events from all queues */" << std::endl; - stream << padding << " _event_t tmpE;" << std::endl; - std::list others; - others.push_back(invoker->_parent); - for (std::map, ChartToPromela*>::iterator queueIter = invoker->_parent->_machines.begin(); queueIter != invoker->_parent->_machines.end(); queueIter++) { - if (queueIter->second != invoker) - others.push_back(queueIter->second); + stream << padding << "inline advanceTime(increment, queue) {" << std::endl; + stream << padding << " int tmpIndex = 0;" << std::endl; + stream << padding << " _event_t tmpEvent;" << std::endl; + stream << padding << " do" << std::endl; + stream << padding << " :: tmpIndex < len(queue) -> {" << std::endl; + stream << padding << " queue?tmpEvent;" << std::endl; + stream << padding << " if" << std::endl; + stream << padding << " :: tmpEvent.delay >= increment -> tmpEvent.delay = tmpEvent.delay - increment;" << std::endl; + stream << padding << " :: else -> skip;" << std::endl; + stream << padding << " fi" << std::endl; + stream << padding << " queue!tmpEvent;" << std::endl; + stream << padding << " tmpIndex++;" << std::endl; + stream << padding << " }" << std::endl; + stream << padding << " :: else -> break;" << std::endl; + stream << padding << " od" << std::endl; + stream << padding << "}" << std::endl; +} + +void ChartToPromela::writeRemovePendingEventsFromInvoker(std::ostream& stream, int indent) { + std::list queues; + queues.push_back("eQ"); + if (_allowEventInterleaving) + queues.push_back("tmpQ"); + + stream << "inline removePendingEventsForInvoker(invokeIdentifier) {" << std::endl; + for (std::map, ChartToPromela*>::iterator queueIter = _machinesAll->begin(); queueIter != _machinesAll->end(); queueIter++) { + for (std::list::iterator qIter = queues.begin(); qIter != queues.end(); qIter++) { + stream << " removePendingEventsForInvokerOnQueue(invokeIdentifier, " << queueIter->second->_prefix << *qIter << ");" << std::endl; } - - for (std::list::iterator queueIter = others.begin(); queueIter != others.end(); queueIter++) { - stream << padding << " do" << std::endl; - stream << padding << " :: (len(" << (*queueIter)->_prefix << "eQ) > 0) -> { " << (*queueIter)->_prefix << "eQ?tmpE; " << _prefix << "tmpQ!tmpE; }" << std::endl; - stream << padding << " :: else -> break;" << std::endl; - stream << padding << " od" << std::endl; - - stream << padding << " do" << std::endl; - stream << padding << " :: (len(" << _prefix << "tmpQ) > 0) -> {" << std::endl; - stream << padding << " " << _prefix << "tmpQ?tmpE;" << std::endl; - stream << padding << " if" << std::endl; - stream << padding << " :: (tmpE.invokeid != " << _analyzer->macroForLiteral(invoker->_invokerid) << " || tmpE.delay == 0) -> " << (*queueIter)->_prefix << "eQ!tmpE" << std::endl; - stream << padding << " :: else -> skip;" << std::endl; - stream << padding << " fi" << std::endl; - stream << padding << " }" << std::endl; - stream << padding << " :: else -> break;" << std::endl; - stream << padding << " od" << std::endl; + } + stream << "}" << std::endl; + stream << std::endl; + stream << "inline removePendingEventsForInvokerOnQueue(invokeIdentifier, queue) {" << std::endl; + stream << " int tmpIndex = 0;" << std::endl; + stream << " _event_t tmpEvent;" << std::endl; + stream << " do" << std::endl; + stream << " :: tmpIndex < len(queue) -> {" << std::endl; + stream << " queue?tmpEvent;" << std::endl; + stream << " if" << std::endl; + stream << " :: tmpEvent.delay == 0 || tmpEvent.invokeid != invokeIdentifier -> queue!tmpEvent;" << std::endl; + stream << " :: else -> skip;" << std::endl; + stream << " fi" << std::endl; + stream << " tmpIndex++;" << std::endl; + stream << " }" << std::endl; + stream << " :: else -> break;" << std::endl; + stream << " od" << std::endl; + stream << "}" << std::endl; +} + +void ChartToPromela::writeCancelEvents(std::ostream& stream, int indent) { + std::list queues; + queues.push_back("eQ"); + if (_allowEventInterleaving) + queues.push_back("tmpQ"); + + stream << "inline cancelSendId(sendIdentifier, invokerIdentifier) {" << std::endl; + for (std::map, ChartToPromela*>::iterator queueIter = _machinesAll->begin(); queueIter != _machinesAll->end(); queueIter++) { + for (std::list::iterator qIter = queues.begin(); qIter != queues.end(); qIter++) { + stream << " cancelSendIdOnQueue(sendIdentifier, " << queueIter->second->_prefix << *qIter << ", invokerIdentifier);" << std::endl; } - stream << padding << "}" << std::endl; } + stream << "}" << std::endl; + stream << std::endl; + + stream << "inline cancelSendIdOnQueue(sendIdentifier, queue, invokerIdentifier) {" << std::endl; + stream << " int tmpIndex = 0;" << std::endl; + stream << " _event_t tmpEvent;" << std::endl; + stream << " do" << std::endl; + stream << " :: tmpIndex < len(queue) -> {" << std::endl; + stream << " queue?tmpEvent;" << std::endl; + stream << " if" << std::endl; + stream << " :: tmpEvent.invokeid != invokerIdentifier || tmpEvent.sendid != sendIdentifier || tmpEvent.delay == 0 -> queue!tmpEvent;" << std::endl; + stream << " :: else -> skip;" << std::endl; + stream << " fi" << std::endl; + stream << " tmpIndex++;" << std::endl; + stream << " }" << std::endl; + stream << " :: else -> break;" << std::endl; + stream << " od" << std::endl; + stream << "}" << std::endl; } +void ChartToPromela::writeScheduleMachines(std::ostream& stream, int indent) { + std::string padding; + for (int i = 0; i < indent; i++) { + padding += " "; + } + + stream << padding << "inline scheduleMachines() {" << std::endl; + std::list queues; + queues.push_back("eQ"); + + if (_allowEventInterleaving) + queues.push_back("tmpQ"); + + stream << " /* schedule state-machines with regard to their event's delay */" << std::endl; + stream << " skip;" << std::endl; + stream << " d_step {" << std::endl; + + stream << std::endl << "/* determine smallest delay */" << std::endl; + stream << " int smallestDelay = 2147483647;" << std::endl; + + for (std::map, ChartToPromela*>::iterator queueIter = _machinesAll->begin(); queueIter != _machinesAll->end(); queueIter++) { + for (std::list::iterator qIter = queues.begin(); qIter != queues.end(); qIter++) { + stream << " determineSmallestDelay(smallestDelay, " << queueIter->second->_prefix << *qIter << ");" << std::endl; + } + } + // stream << " printf(\"======= Lowest delay is %d\\n\", smallestDelay);" << std::endl; + + stream << std::endl << "/* prioritize processes with lowest delay or internal events */" << std::endl; + + for (std::map, ChartToPromela*>::iterator queueIter = _machinesAll->begin(); queueIter != _machinesAll->end(); queueIter++) { + stream << " rescheduleProcess(smallestDelay, " + << queueIter->second->_prefix << "procid, " + << queueIter->second->_prefix << "iQ, " + << queueIter->second->_prefix << "eQ"; + if (_allowEventInterleaving) { + stream << ", " << queueIter->second->_prefix << "tmpQ);" << std::endl; + } else { + stream << ");" << std::endl; + } + } + + stream << std::endl << "/* advance time by subtracting the smallest delay from all event delays */" << std::endl; + stream << " if" << std::endl; + stream << " :: (smallestDelay > 0) -> {" << std::endl; + for (std::map, ChartToPromela*>::iterator queueIter = _machinesAll->begin(); queueIter != _machinesAll->end(); queueIter++) { + for (std::list::iterator qIter = queues.begin(); qIter != queues.end(); qIter++) { + stream << " advanceTime(smallestDelay, " << queueIter->second->_prefix << *qIter << ");" << std::endl; + } + } + stream << " }" << std::endl; + stream << " :: else -> skip;" << std::endl; + stream << " fi;" << std::endl; + stream << " }" << std::endl; + stream << " set_priority(_pid, 10);" << std::endl << std::endl; + stream << padding << "}" << std::endl; +} + void ChartToPromela::writeEventDispatching(std::ostream& stream) { for (std::map::iterator stateIter = _activeConf.begin(); stateIter != _activeConf.end(); stateIter++) { // if (_globalStates[i] == _startState) @@ -2882,6 +2998,11 @@ void ChartToPromela::initNodes() { { NodeSet invokes = filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true); NodeSet sends = filterChildElements(_nsInfo.xmlNSPrefix + "send", _scxml, true); + NodeSet cancels = filterChildElements(_nsInfo.xmlNSPrefix + "cancel", _scxml, true); + + if (cancels.size() > 0) { + _analyzer->addCode("_event.invokeid", this); + } for (int i = 0; i < sends.size(); i++) { if (HAS_ATTR_CAST(sends[i], "idlocation")) { @@ -2951,6 +3072,12 @@ void ChartToPromela::initNodes() { } } + if (_globalEventSource || _invokers.size() > 0) { + _allowEventInterleaving = true; + } else { + _allowEventInterleaving = false; + } + // add platform variables as string literals _analyzer->addLiteral(_prefix + "_sessionid"); _analyzer->addLiteral(_prefix + "_name"); @@ -3128,7 +3255,7 @@ void ChartToPromela::writeProgram(std::ostream& stream) { stream << std::endl; initNodes(); - + for (std::map, ChartToPromela*>::iterator nestedIter = _machines.begin(); nestedIter != _machines.end(); nestedIter++) { if (nestedIter->second->_start == NULL) { nestedIter->second->interpret(); @@ -3153,12 +3280,42 @@ void ChartToPromela::writeProgram(std::ostream& stream) { writeStrings(stream); stream << std::endl; writeDeclarations(stream); - + stream << std::endl; + for (std::map, ChartToPromela*>::iterator nestedIter = _machines.begin(); nestedIter != _machines.end(); nestedIter++) { nestedIter->second->writeDeclarations(stream); stream << std::endl; } + stream << std::endl << "/* Global inline functions */" << std::endl; + + + if (_analyzer->usesEventField("delay") && _machines.size() > 0) { + writeDetermineShortestDelay(stream); + stream << std::endl; + writeAdvanceTime(stream); + stream << std::endl; + writeRescheduleProcess(stream); + stream << std::endl; + writeScheduleMachines(stream); + stream << std::endl; + } + + { + NodeSet cancels = filterChildElements(_nsInfo.xmlNSPrefix + "cancel", _scxml, true); + if (cancels.size() > 0) { + writeCancelEvents(stream); + stream << std::endl; + } + } + { + NodeSet invokes = filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true); + if (invokes.size() > 0 && _analyzer->usesEventField("delay")) { + writeRemovePendingEventsFromInvoker(stream); + stream << std::endl; + } + + } stream << std::endl; writeEventSources(stream); stream << std::endl; @@ -3171,7 +3328,7 @@ void ChartToPromela::writeProgram(std::ostream& stream) { nestedIter->second->writeFSM(stream); stream << std::endl; } - + // write ltl expression for success std::stringstream acceptingStates; std::string seperator; diff --git a/src/uscxml/transform/ChartToPromela.h b/src/uscxml/transform/ChartToPromela.h index 2ee0b1a..cfe5a78 100644 --- a/src/uscxml/transform/ChartToPromela.h +++ b/src/uscxml/transform/ChartToPromela.h @@ -312,10 +312,16 @@ protected: void writeDispatchingBlock(std::ostream& stream, std::list, int indent = 0); void writeStartInvoker(std::ostream& stream, const Arabica::DOM::Node& node, ChartToPromela* invoker, int indent = 0); - void writeRemovePendingEventsFromInvoker(std::ostream& stream, ChartToPromela* invoker, int indent = 0, bool atomic = true); - void writeCancelWithIdOrExpr(std::ostream& stream, const Arabica::DOM::Element& cancel, ChartToPromela* invoker, int indent = 0); + //void writeRemovePendingEventsFromInvoker(std::ostream& stream, ChartToPromela* invoker, int indent = 0, bool atomic = true); - Arabica::XPath::NodeSet getTransientContent(const Arabica::DOM::Element& state, const std::string& source = ""); + void writeDetermineShortestDelay(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); + void writeRemovePendingEventsFromInvoker(std::ostream& stream, int indent = 0); + + std::list getTransientContent(GlobalTransition* transition); //Arabica::DOM::Node getUltimateTarget(const Arabica::DOM::Element& transition); static std::string declForRange(const std::string& identifier, long minValue, long maxValue, bool nativeOnly = false); @@ -334,7 +340,8 @@ protected: std::list _varInitializers; // pending initializations for arrays PromelaCodeAnalyzer* _analyzer; - + bool _allowEventInterleaving; + uint32_t _externalQueueLength; uint32_t _internalQueueLength; diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index dd86ac9..3ea960c 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -78,6 +78,30 @@ if (NOT BUILD_MINIMAL) target_link_libraries(test-w3c uscxml uscxml_transform) set_target_properties(test-w3c PROPERTIES FOLDER "Tests") + # copy resources + file(GLOB_RECURSE W3C_RESOURCES + w3c/*.txt + w3c/*sub*.scxml + ) + + foreach(W3C_RESOURCE ${W3C_RESOURCES} ) + # we abuse this as head and tail + get_filename_component(W3C_RESOURCE_PATH ${W3C_RESOURCE} PATH) + get_filename_component(W3C_TEST_TYPE ${W3C_RESOURCE_PATH} NAME) + + if (BUILD_TESTS_W3C_ECMA AND W3C_TEST_TYPE STREQUAL "ecma") + file(COPY ${W3C_RESOURCE} DESTINATION ${CMAKE_CURRENT_BINARY_DIR}/ecma) + elseif (BUILD_TESTS_W3C_XPATH AND W3C_TEST_TYPE STREQUAL "xpath") + file(COPY ${W3C_RESOURCE} DESTINATION ${CMAKE_CURRENT_BINARY_DIR}/xpath) + elseif (BUILD_TESTS_W3C_LUA AND W3C_TEST_TYPE STREQUAL "lua") + file(COPY ${W3C_RESOURCE} DESTINATION ${CMAKE_CURRENT_BINARY_DIR}/lua) + elseif (BUILD_TESTS_W3C_PROMELA AND W3C_TEST_TYPE STREQUAL "promela") + file(COPY ${W3C_RESOURCE} DESTINATION ${CMAKE_CURRENT_BINARY_DIR}/lua) + endif() + + endforeach() + + # prepare tests file(GLOB_RECURSE W3C_TESTS w3c/*.scxml ) @@ -102,6 +126,31 @@ if (NOT BUILD_MINIMAL) if (BUILD_TESTS_FSM_ECMA AND TEST_NAME MATCHES "^ecma\\/.*") add_test("fsm/${TEST_NAME}" ${CMAKE_RUNTIME_OUTPUT_DIRECTORY}/test-w3c -f ${W3C_TEST}) set_property(TEST "fsm/${TEST_NAME}" PROPERTY LABELS "fsm/${TEST_NAME}") + + add_test(NAME "minimized/${TEST_NAME}" + COMMAND ${CMAKE_COMMAND} + -DOUTDIR:FILEPATH=${CMAKE_CURRENT_BINARY_DIR}/ecma + -DTESTFILE:FILEPATH=${W3C_TEST} + -DUSCXML_TRANSFORM_BIN:FILEPATH=${CMAKE_RUNTIME_OUTPUT_DIRECTORY}/uscxml-transform + -DUSCXML_W3C_TEST_BIN:FILEPATH=${CMAKE_RUNTIME_OUTPUT_DIRECTORY}/test-w3c + -P ${CMAKE_CURRENT_SOURCE_DIR}/w3c/run_minimized_test.cmake) + set_property(TEST "minimized/${TEST_NAME}" PROPERTY LABELS "minimized/${TEST_NAME}") + + set_tests_properties(${TEST_NAME} PROPERTIES DEPENDS uscxml-transform) + set_tests_properties(${TEST_NAME} PROPERTIES DEPENDS test-w3c) + + add_test(NAME "fsm/minimized/${TEST_NAME}" + COMMAND ${CMAKE_COMMAND} + -DOUTDIR:FILEPATH=${CMAKE_CURRENT_BINARY_DIR}/ecma + -DTESTFILE:FILEPATH=${W3C_TEST} + -DUSCXML_TRANSFORM_BIN:FILEPATH=${CMAKE_RUNTIME_OUTPUT_DIRECTORY}/uscxml-transform + -DUSCXML_W3C_TEST_BIN:FILEPATH=${CMAKE_RUNTIME_OUTPUT_DIRECTORY}/test-w3c + -P ${CMAKE_CURRENT_SOURCE_DIR}/w3c/run_minimized_flat_test.cmake) + set_property(TEST "fsm/minimized/${TEST_NAME}" PROPERTY LABELS "fsm/minimized/${TEST_NAME}") + + set_tests_properties(${TEST_NAME} PROPERTIES DEPENDS uscxml-transform) + set_tests_properties(${TEST_NAME} PROPERTIES DEPENDS test-w3c) + endif() if (BUILD_TESTS_W3C_XPATH AND TEST_NAME MATCHES "^xpath\\/.*") @@ -131,7 +180,7 @@ if (NOT BUILD_MINIMAL) add_test(NAME "spin/${TEST_NAME}" COMMAND ${CMAKE_COMMAND} - -DOUTDIR:FILEPATH=${CMAKE_CURRENT_BINARY_DIR} + -DOUTDIR:FILEPATH=${CMAKE_CURRENT_BINARY_DIR}/promela -DTESTFILE:FILEPATH=${W3C_TEST} -DUSCXML_TRANSFORM_BIN:FILEPATH=${CMAKE_RUNTIME_OUTPUT_DIRECTORY}/uscxml-transform -DSPIN_BIN:FILEPATH=${SPIN} diff --git a/test/ctest/CTestCustom.ctest.in b/test/ctest/CTestCustom.ctest.in index c4fc9c9..3af297e 100644 --- a/test/ctest/CTestCustom.ctest.in +++ b/test/ctest/CTestCustom.ctest.in @@ -28,6 +28,15 @@ set(CTEST_CUSTOM_TESTS_IGNORE "fsm/ecma/test415.scxml" # manual test # "fsm/ecma/test513.txt" # manual test + ### Ignore for flattened, minimized ECMAScript datamodel + "fsm/minimized/ecma/test178.scxml" # manual test + "fsm/minimized/ecma/test230.scxml" # manual test + "fsm/minimized/ecma/test250.scxml" # manual test + "fsm/minimized/ecma/test301.scxml" # manual test + "fsm/minimized/ecma/test307.scxml" # manual test + "fsm/minimized/ecma/test415.scxml" # manual test + # "fsm/ecma/test513.txt" # manual test + ### Just ignore the XPath datamodel tests that hang, most of the rest fails as well "xpath/test388.scxml" # hangs "xpath/test580.scxml" # hangs diff --git a/test/src/test-w3c.cpp b/test/src/test-w3c.cpp index e2efa59..c7f136d 100644 --- a/test/src/test-w3c.cpp +++ b/test/src/test-w3c.cpp @@ -24,74 +24,16 @@ static std::string documentURI; int retCode = EXIT_FAILURE; -class W3CStatusMonitor : public uscxml::InterpreterMonitor { +class W3CStatusMonitor : public uscxml::StateTransitionMonitor { - void beforeTakingTransition(uscxml::Interpreter interpreter, const Arabica::DOM::Element& transition, bool moreComing) { - std::cout << "Transition: " << uscxml::DOMUtils::xPathForNode(transition) << std::endl; +void beforeCompletion(uscxml::Interpreter interpreter) { + if (interpreter.getConfiguration().size() == 1 && interpreter.isInState("pass")) { + std::cout << "TEST SUCCEEDED" << std::endl; + retCode = EXIT_SUCCESS; + return; } - - void onStableConfiguration(uscxml::Interpreter interpreter) { - std::cout << "Config: {"; - printNodeSet(interpreter.getConfiguration()); - std::cout << "}" << std::endl; - } - - void beforeProcessingEvent(uscxml::Interpreter interpreter, const uscxml::Event& event) { - std::cout << "Event: " << event.name << std::endl; - } - - void beforeExitingState(uscxml::Interpreter interpreter, const Arabica::DOM::Element& state, bool moreComing) { - exitingStates.push_back(state); - if (!moreComing) { - std::cout << "Exiting: {"; - printNodeSet(exitingStates); - std::cout << "}" << std::endl; - exitingStates = Arabica::XPath::NodeSet(); - } - } - - void beforeEnteringState(uscxml::Interpreter interpreter, const Arabica::DOM::Element& state, bool moreComing) { - enteringStates.push_back(state); - if (!moreComing) { - std::cout << "Entering: {"; - printNodeSet(enteringStates); - std::cout << "}" << std::endl; - enteringStates = Arabica::XPath::NodeSet(); - } - - } - - void printNodeSet(const Arabica::XPath::NodeSet& config) { - std::string seperator; - for (int i = 0; i < config.size(); i++) { - std::cout << seperator << ATTR_CAST(config[i], "id"); - seperator = ", "; - } - } - - void beforeCompletion(uscxml::Interpreter interpreter) { - Arabica::XPath::NodeSet config = interpreter.getConfiguration(); - if (config.size() == 1) { - if (withFlattening) { - std::cout << ATTR_CAST(config[0], "id") << std::endl; - if (boost::starts_with(ATTR_CAST(config[0], "id"), "active:{pass")) { - std::cout << "TEST SUCCEEDED" << std::endl; - retCode = EXIT_SUCCESS; - return; - } - } else { - if (boost::iequals(ATTR_CAST(config[0], "id"), "pass")) { - std::cout << "TEST SUCCEEDED" << std::endl; - retCode = EXIT_SUCCESS; - return; - } - } - } - std::cout << "TEST FAILED" << std::endl; - } - - Arabica::XPath::NodeSet exitingStates; - Arabica::XPath::NodeSet enteringStates; + std::cout << "TEST FAILED" << std::endl; +} }; int main(int argc, char** argv) { @@ -143,7 +85,7 @@ int main(int argc, char** argv) { } else { interpreter = Interpreter::fromURL(documentURI); } - + if (delayFactor != 1) { Arabica::DOM::Document document = interpreter.getDocument(); Arabica::DOM::Element root = document.getDocumentElement(); diff --git a/test/w3c/analyze_tests.pl b/test/w3c/analyze_tests.pl index 2525008..111db5a 100755 --- a/test/w3c/analyze_tests.pl +++ b/test/w3c/analyze_tests.pl @@ -42,7 +42,7 @@ $/ = '-' x 58 . "\n"; while ($block = ) { chomp($block); - + # Test Preambel ======== if ($block =~ / @@ -83,6 +83,37 @@ while ($block = ) { # next; - no next as this is part of the actual test output we need to scan below } + # Minimization ======== + # print $block; + + if ($block =~ + / + Number\sof\selements\sbefore\sreduction:\s(\d+) + /x ) { + $test->{$currTest}->{'min'}->{'before'} = $1; + if ($block =~ + / + Number\sof\selements\safter\sreduction:\s(\d+) + /x ) { + $test->{$currTest}->{'min'}->{'after'} = $1; + } + } + + # Flattening ======== + + if ($block =~ + / + Number\sof\selements\sbefore\sflattening:\s(\d+) + /x ) { + $test->{$currTest}->{'flat'}->{'before'} = $1; + if ($block =~ + / + Number\sof\selements\safter\sflattening:\s(\d+) + /x ) { + $test->{$currTest}->{'flat'}->{'after'} = $1; + } + } + # Promela Test ======== if ($block =~ / diff --git a/test/w3c/run_minimized_flat_test.cmake b/test/w3c/run_minimized_flat_test.cmake new file mode 100644 index 0000000..81f9114 --- /dev/null +++ b/test/w3c/run_minimized_flat_test.cmake @@ -0,0 +1,21 @@ +# minimize SCXML document and run + +get_filename_component(TEST_FILE_NAME ${TESTFILE} NAME) + +set(ENV{USCXML_MINIMIZE_WAIT_FOR_COMPLETION} "TRUE") +set(ENV{USCXML_MINIMIZE_RETAIN_AS_COMMENTS} "TRUE") + +execute_process(COMMAND ${USCXML_TRANSFORM_BIN} -tflat -i ${TESTFILE} -o ${OUTDIR}/${TEST_FILE_NAME}.flat.scxml RESULT_VARIABLE CMD_RESULT) +if(CMD_RESULT) + message(FATAL_ERROR "Error running ${USCXML_TRANSFORM_BIN}") +endif() + +execute_process(COMMAND ${USCXML_TRANSFORM_BIN} -tmin -i ${OUTDIR}/${TEST_FILE_NAME}.flat.scxml -o ${OUTDIR}/${TEST_FILE_NAME}.flat.min.scxml RESULT_VARIABLE CMD_RESULT) +if(CMD_RESULT) + message(FATAL_ERROR "Error running ${USCXML_TRANSFORM_BIN}") +endif() + +execute_process(COMMAND ${USCXML_W3C_TEST_BIN} ${OUTDIR}/${TEST_FILE_NAME}.flat.min.scxml RESULT_VARIABLE CMD_RESULT) +if(CMD_RESULT) + message(FATAL_ERROR "Error running ${USCXML_W3C_TEST_BIN}") +endif() diff --git a/test/w3c/run_minimized_test.cmake b/test/w3c/run_minimized_test.cmake new file mode 100644 index 0000000..481c0e9 --- /dev/null +++ b/test/w3c/run_minimized_test.cmake @@ -0,0 +1,16 @@ +# minimize SCXML document and run + +get_filename_component(TEST_FILE_NAME ${TESTFILE} NAME) + +set(ENV{USCXML_MINIMIZE_WAIT_FOR_COMPLETION} "TRUE") +set(ENV{USCXML_MINIMIZE_RETAIN_AS_COMMENTS} "TRUE") + +execute_process(COMMAND ${USCXML_TRANSFORM_BIN} -tmin -i ${TESTFILE} -o ${OUTDIR}/${TEST_FILE_NAME}.min.scxml RESULT_VARIABLE CMD_RESULT) +if(CMD_RESULT) + message(FATAL_ERROR "Error running ${USCXML_TRANSFORM_BIN}") +endif() + +execute_process(COMMAND ${USCXML_W3C_TEST_BIN} ${OUTDIR}/${TEST_FILE_NAME}.min.scxml RESULT_VARIABLE CMD_RESULT) +if(CMD_RESULT) + message(FATAL_ERROR "Error running ${USCXML_W3C_TEST_BIN}") +endif() diff --git a/test/w3c/run_promela_test.cmake b/test/w3c/run_promela_test.cmake index 179cd68..e19148f 100644 --- a/test/w3c/run_promela_test.cmake +++ b/test/w3c/run_promela_test.cmake @@ -1,23 +1,27 @@ # convert given file to promela and run spin get_filename_component(TEST_FILE_NAME ${TESTFILE} NAME) +execute_process(COMMAND ${CMAKE_COMMAND} -E make_directory ${OUTDIR}) execute_process(COMMAND ${USCXML_TRANSFORM_BIN} -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() -execute_process(COMMAND ${SPIN_BIN} -a ${OUTDIR}/${TEST_FILE_NAME}.pml RESULT_VARIABLE CMD_RESULT) +execute_process(COMMAND ${SPIN_BIN} -a ${OUTDIR}/${TEST_FILE_NAME}.pml WORKING_DIRECTORY ${OUTDIR} RESULT_VARIABLE CMD_RESULT) if(CMD_RESULT) - message(FATAL_ERROR "Error running ${SPIN_BIN}: ${CMD_RESULT}") + message(FATAL_ERROR "Error running spin ${SPIN_BIN}: ${CMD_RESULT}") endif() -execute_process(COMMAND ${GCC_BIN} -DMEMLIM=1024 -DVECTORSZ=2048 -O2 -DXUSAFE -w -o ${OUTDIR}/pan ${OUTDIR}/pan.c RESULT_VARIABLE CMD_RESULT) +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) if(CMD_RESULT) - message(FATAL_ERROR "Error running ${GCC_BIN}: ${CMD_RESULT}") + message(FATAL_ERROR "Error running gcc ${GCC_BIN}: ${CMD_RESULT}") endif() -execute_process(COMMAND ${OUTDIR}/pan -m10000 -a RESULT_VARIABLE CMD_RESULT) +execute_process(COMMAND ${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 "${TEST_OUT}") +# file(WRITE ${OUTDIR}/${TEST_FILE_NAME}.pml.out ${TEST_OUT}) \ No newline at end of file -- cgit v0.12