diff options
Diffstat (limited to 'src/uscxml/transform/ChartToPromela.cpp')
-rw-r--r-- | src/uscxml/transform/ChartToPromela.cpp | 3578 |
1 files changed, 0 insertions, 3578 deletions
diff --git a/src/uscxml/transform/ChartToPromela.cpp b/src/uscxml/transform/ChartToPromela.cpp deleted file mode 100644 index a9afea6..0000000 --- a/src/uscxml/transform/ChartToPromela.cpp +++ /dev/null @@ -1,3578 +0,0 @@ -/** - * @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 <http://www.opensource.org/licenses/bsd-license>. - * @endcond - */ - -#define NEW_DELAY_RESHUFFLE 1 - -#include "uscxml/transform/ChartToFSM.h" -#include "uscxml/transform/ChartToPromela.h" -#include "uscxml/transform/FlatStateIdentifier.h" -#include "uscxml/plugins/datamodel/promela/PromelaParser.h" -#include "uscxml/plugins/datamodel/promela/parser/promela.tab.hpp" - -#include <DOM/io/Stream.hpp> -#include <DOM/SAX2DOM/SAX2DOM.hpp> -#include <iostream> -#include "uscxml/UUID.h" -#include <math.h> -#include <boost/algorithm/string.hpp> -#include <glog/logging.h> - -#define MSG_QUEUE_LENGTH 5 -#define MAX_MACRO_CHARS 64 -#define MIN_COMMENT_PADDING 60 -#define MAX(X,Y) ((X) > (Y) ? (X) : (Y)) - -#define ADAPT_SRC(code) _analyzer->adaptCode(code, _prefix) - -#define BIT_WIDTH(number) (number > 1 ? (int)ceil(log((double)number) / log((double)2.0)) : 1) -#define LENGTH_FOR_NUMBER(input, output) \ -{ \ - int number = input; \ - int output = 0; \ - do { \ - number /= 10; \ - output++; \ - } while (number != 0); \ -} - -#define INDENT_MIN(stream, start, cols) \ -for (size_t indentIndex = start; indentIndex < cols; indentIndex++) \ - stream << " "; - -#define DIFF_MAPS(base, compare, result) \ -{ \ - histIter_t baseIter = base.begin(); \ - while(baseIter != base.end()) { \ - if (compare.find(baseIter->first) == compare.end()) { \ - result[baseIter->first] = baseIter->second; \ - } else { \ - histMemberIter_t baseMemberIter = baseIter->second.begin(); \ - while(baseMemberIter != baseIter->second.end()) { \ - if (compare.at(baseIter->first).find(*baseMemberIter) == compare.at(baseIter->first).end()) { \ - result[baseIter->first].insert(*baseMemberIter); \ - } \ - baseMemberIter++; \ - } \ - } \ - baseIter++; \ - } \ -} - -#define INTERSECT_MAPS(base, compare, result) \ -{ \ - histIter_t baseIter = base.begin(); \ - while(baseIter != base.end()) { \ - if (compare.find(baseIter->first) != compare.end()) { \ - histMemberIter_t baseMemberIter = baseIter->second.begin(); \ - while(baseMemberIter != baseIter->second.end()) { \ - if (compare.at(baseIter->first).find(*baseMemberIter) != compare.at(baseIter->first).end()) { \ - result[baseIter->first].insert(*baseMemberIter); \ - } \ - baseMemberIter++; \ - } \ - } \ - baseIter++; \ - } \ -} - -#define PRETTY_PRINT_LIST(stream, var) \ -{ \ - std::list<std::string>::const_iterator listIter = var.begin(); \ - std::string sep;\ - while(listIter != var.end()) { \ - stream << sep << *listIter; \ - sep = ", "; \ - listIter++; \ - } \ -} - -#define TRANSITION_TRACE(transList, value) \ -if (_traceTransitions) { \ -for (std::set<int>::iterator transRefIter = transList->transitionRefs.begin(); \ - transRefIter != transList->transitionRefs.end(); \ - transRefIter++) { \ - stream << padding << _prefix << "transitions[" << *transRefIter << "] = "#value"; " << std::endl; \ - } \ -} \ - - -#define DUMP_STATS(disregardTime) \ -uint64_t now = tthread::chrono::system_clock::now(); \ -if (now - _lastTimeStamp > 1000 || disregardTime) { \ - std::cerr << "## State : " << _perfStatesTotal << " [" << _perfStatesProcessed << "/sec]" << std::endl; \ - std::cerr << "## Transition: " << _perfTransTotal << " [" << _perfHistoryProcessed << "/sec]" << std::endl; \ - std::cerr << "## History : " << _perfHistoryTotal << " [" << _perfHistoryProcessed << "/sec]" << std::endl; \ - std::cerr << "toPML: "; \ - std::cerr << _perfStatesTotal << ", " << _perfStatesProcessed << ", "; \ - std::cerr << _perfTransTotal << ", " << _perfTransProcessed << ", "; \ - std::cerr << _perfHistoryTotal << ", " << _perfHistoryProcessed; \ - std::cerr << std::endl << std::endl; \ - _perfTransProcessed = 0; \ - _perfHistoryProcessed = 0; \ - _perfStatesProcessed = 0; \ - if (!disregardTime)\ - _lastTimeStamp = now; \ -} - -namespace uscxml { - -using namespace Arabica::DOM; -using namespace Arabica::XPath; - -Transformer ChartToPromela::transform(const Interpreter& other) { - return boost::shared_ptr<TransformerImpl>(new ChartToPromela(other)); -} - -void ChartToPromela::writeTo(std::ostream& stream) { - writeProgram(stream); -} - - -void PromelaCodeAnalyzer::addCode(const std::string& code, ChartToPromela* interpreter) { - PromelaParser parser(code); -// parser.dump(); - - // find all strings - std::list<PromelaParserNode*> astNodes; - astNodes.push_back(parser.ast); - - while(astNodes.size() > 0) { - PromelaParserNode* node = astNodes.front(); - astNodes.pop_front(); - -// node->dump(); - - bool hasValue = false; - int assignedValue = 0; - - - switch (node->type) { - case PML_STRING: { - std::string unquoted = node->value; - if (boost::starts_with(unquoted, "'")) { - unquoted = unquoted.substr(1, unquoted.size() - 2); - } - addLiteral(unquoted); - break; - } - case PML_ASGN: - if (node->operands.back()->type == PML_CONST) { - hasValue = true; - if (isInteger(node->operands.back()->value.c_str(), 10)) { - assignedValue = strTo<int>(node->operands.back()->value); - } - } - if (node->operands.back()->type == PML_STRING) { - // remember strings for later - astNodes.push_back(node->operands.back()); - } - if (node->operands.front()->type == PML_CMPND) { - node = node->operands.front(); - } else { - break; - } -// if (node->operands.front()->type != PML_NAME) -// break; // this will skip array assignments - case PML_CMPND: { - std::string nameOfType; - std::list<PromelaParserNode*>::iterator opIter = node->operands.begin(); - if ((*opIter)->type != PML_NAME) { - node->dump(); - return; - assert(false); - } - - PromelaTypedef* td = &_typeDefs; - std::string seperator; - - while(opIter != node->operands.end()) { - switch ((*opIter)->type) { - case PML_NAME: - td = &td->types[(*opIter)->value]; - td->occurrences.insert(interpreter); - - nameOfType += seperator + (*opIter)->value; - if (nameOfType.compare("_x") == 0) - _usesPlatformVars = true; - seperator = "_"; - td->name = nameOfType + "_t"; - break; - case PML_VAR_ARRAY: { - PromelaParserNode* name = (*opIter)->operands.front(); - PromelaParserNode* subscript = *(++(*opIter)->operands.begin()); - td = &td->types[name->value]; - td->occurrences.insert(interpreter); - - nameOfType += seperator + name->value; - td->name = nameOfType + "_t"; - - if (isInteger(subscript->value.c_str(), 10)) { - td->arraySize = strTo<int>(subscript->value); - } - break; - } - default: - if ((*opIter)->type == PML_CONST) { - // break fall through from ASGN - break; - } -// node->dump(); -// assert(false); - break; - } - - if (nameOfType.compare("_x_states") == 0) { - _usesInPredicate = true; - } - if (nameOfType.compare("_event_type") == 0) { - addLiteral("internal"); - addLiteral("external"); - addLiteral("platform"); - } - if (nameOfType.compare("_event_origintype") == 0) { - addLiteral("http://www.w3.org/TR/scxml/#SCXMLEventProcessor"); - } - opIter++; - } - - if (hasValue) { - if (td->maxValue < assignedValue) - td->maxValue = assignedValue; - if (td->minValue > assignedValue) - td->minValue = assignedValue; - } - - continue; // skip processing nested AST nodes - } - case PML_NAME: { - _typeDefs.types[node->value].occurrences.insert(interpreter); - _typeDefs.types[node->value].minValue = 0; - _typeDefs.types[node->value].maxValue = 0; - // test325 - if (node->value.compare("_ioprocessors") == 0) { - addCode("_ioprocessors.scxml.location", interpreter); - } - - break; - } - - default: -// node->dump(); - break; -// assert(false); - } - - astNodes.insert(astNodes.end(), node->operands.begin(), node->operands.end()); - - } -} - -void PromelaCodeAnalyzer::addEvent(const std::string& eventName) { - if (_events.find(eventName) != _events.end()) - return; - - addLiteral(eventName, _lastEventIndex); - assert(_strIndex.find(eventName) != _strIndex.end()); - - _eventTrie.addWord(eventName); - _events[eventName] = _strIndex[eventName]; - _lastEventIndex++; -} - -void PromelaCodeAnalyzer::addOrigState(const std::string& stateName) { - if (_origStateIndex.find(stateName) == _origStateIndex.end()) { - _origStateIndex[stateName] = _lastStateIndex++; - createMacroName(stateName); - } -} - -void PromelaCodeAnalyzer::addState(const std::string& stateName) { - if (_states.find(stateName) != _states.end()) - return; - - createMacroName(stateName); -} - -void PromelaCodeAnalyzer::addLiteral(const std::string& literal, int forceIndex) { - if (boost::starts_with(literal, "'")) - throw std::runtime_error("Literal " + literal + " passed with quotes"); - - if (_strLiterals.find(literal) != _strLiterals.end()) - return; - - _strLiterals.insert(literal); - createMacroName(literal); - enumerateLiteral(literal, forceIndex); -} - -int PromelaCodeAnalyzer::enumerateLiteral(const std::string& literal, int forceIndex) { - if (forceIndex >= 0) { - _strIndex[literal] = forceIndex; - return forceIndex; - } - - if (_strIndex.find(literal) != _strIndex.end()) - return _strIndex[literal]; - - _strIndex[literal] = _lastStrIndex++; - return _lastStrIndex + 1; -} - -std::string PromelaCodeAnalyzer::createMacroName(const std::string& literal) { - if (_strMacroNames.find(literal) != _strMacroNames.end()) - return _strMacroNames[literal]; - - // find a suitable macro name for the strings - std::string macroName = literal; //literal.substr(1, literal.size() - 2); - - // cannot start with digit - if (isInteger(macroName.substr(0,1).c_str(), 10)) - macroName = "_" + macroName; - - macroName = macroName.substr(0, MAX_MACRO_CHARS); - boost::to_upper(macroName); - - std::string illegalChars = "#\\/:?\"<>| \n\t()[]{}',.-"; - std::string tmp; - std::string::iterator it = macroName.begin(); - while (it < macroName.end()) { - bool found = illegalChars.find(*it) != std::string::npos; - if(found) { - tmp += '_'; - it++; - while(it < macroName.end() && illegalChars.find(*it) != std::string::npos) { - it++; - } - } else { - tmp += *it++; - } - } - macroName = tmp; - if(macroName.length() < 1) - macroName = "_EMPTY_STRING"; - if(macroName.length() < 2 && macroName[0] == '_') - macroName = "_WEIRD_CHARS"; - - unsigned int index = 2; - while (_macroNameSet.find(macroName) != _macroNameSet.end()) { - std::string suffix = toStr(index); - if (macroName.size() > suffix.size()) { - macroName = macroName.substr(0, macroName.size() - suffix.size()) + suffix; - } else { - macroName = suffix; - } - index++; - } - - _macroNameSet.insert(macroName); - _strMacroNames[literal] = macroName; - return macroName; -} - -std::string PromelaCodeAnalyzer::getTypeReset(const std::string& var, const PromelaTypedef& type, const std::string padding) { - std::stringstream assignment; - - std::map<std::string, PromelaTypedef>::const_iterator typeIter = type.types.begin(); - while(typeIter != type.types.end()) { - const PromelaTypedef& innerType = typeIter->second; - if (innerType.arraySize > 0) { - for (size_t i = 0; i < innerType.arraySize; i++) { - assignment << padding << var << "." << typeIter->first << "[" << i << "] = 0;" << std::endl; - } - } else if (innerType.types.size() > 0) { - assignment << getTypeReset(var + "." + typeIter->first, typeIter->second, padding); - } else { - assignment << padding << var << "." << typeIter->first << " = 0;" << std::endl; - } - typeIter++; - } - return assignment.str(); - -} - -std::string PromelaCodeAnalyzer::getTypeAssignment(const std::string& varTo, const std::string& varFrom, const PromelaTypedef& type, const std::string padding) { - std::stringstream assignment; - - std::map<std::string, PromelaTypedef>::const_iterator typeIter = type.types.begin(); - while(typeIter != type.types.end()) { - const PromelaTypedef& innerType = typeIter->second; - if (innerType.arraySize > 0) { - for (size_t i = 0; i < innerType.arraySize; i++) { - assignment << padding << varTo << "." << typeIter->first << "[" << i << "] = " << varFrom << "." << typeIter->first << "[" << i << "];" << std::endl; - } - } else if (innerType.types.size() > 0) { - assignment << getTypeAssignment(varTo + "." + typeIter->first, varFrom + "." + typeIter->first, typeIter->second, padding); - } else { - assignment << padding << varTo << "." << typeIter->first << " = " << varFrom << "." << typeIter->first << ";" << std::endl; - } - typeIter++; - } - return assignment.str(); -} - -std::string PromelaCodeAnalyzer::macroForLiteral(const std::string& literal) { - if (boost::starts_with(literal, "'")) - throw std::runtime_error("Literal " + literal + " passed with quotes"); - - if (_strMacroNames.find(literal) == _strMacroNames.end()) - throw std::runtime_error("No macro for literal '" + literal + "' known"); - return _strMacroNames[literal]; -} - -int PromelaCodeAnalyzer::indexForLiteral(const std::string& literal) { - if (boost::starts_with(literal, "'")) - throw std::runtime_error("Literal " + literal + " passed with quotes"); - - if (_strIndex.find(literal) == _strIndex.end()) - throw std::runtime_error("No index for literal " + literal + " known"); - return _strIndex[literal]; -} - -std::string PromelaCodeAnalyzer::adaptCode(const std::string& code, const std::string& prefix) { -// for (std::map<std::string, std::string>::const_iterator litIter = _strMacroNames.begin(); litIter != _strMacroNames.end(); litIter++) { -// boost::replace_all(replaced, "'" + litIter->first + "'", litIter->second); -// } -// boost::replace_all(replaced, "_event", prefix + "_event"); - // replace all variables from analyzer - - std::string processed = code; - std::stringstream processedStr; - std::list<std::pair<size_t, size_t> > posList; - std::list<std::pair<size_t, size_t> >::iterator posIter; - size_t lastPos; - - // prepend all identifiers with our prefix - { - PromelaParser parsed(processed); -// parsed.dump(); - posList = getTokenPositions(code, PML_NAME, parsed.ast); - posList.sort(); - posIter = posList.begin(); - lastPos = 0; - - while (posIter != posList.end()) { - processedStr << code.substr(lastPos, posIter->first - lastPos) << prefix; - lastPos = posIter->first; - posIter++; - } - processedStr << processed.substr(lastPos, processed.size() - lastPos); - - processed = processedStr.str(); - processedStr.clear(); - processedStr.str(""); - } - - // replace string literals - { - PromelaParser parsed(processed); - posList = getTokenPositions(code, PML_STRING, parsed.ast); - posList.sort(); - posIter = posList.begin(); - lastPos = 0; - - while (posIter != posList.end()) { - processedStr << processed.substr(lastPos, posIter->first - lastPos); -// std::cout << processed.substr(posIter->first + 1, posIter->second - posIter->first - 2) << std::endl; - assert(_strMacroNames.find(processed.substr(posIter->first + 1, posIter->second - posIter->first - 2)) != _strMacroNames.end()); - processedStr << _strMacroNames[processed.substr(posIter->first + 1, posIter->second - posIter->first - 2)]; - lastPos = posIter->second; - posIter++; - } - processedStr << processed.substr(lastPos, processed.size() - lastPos); - - processed = processedStr.str(); - processedStr.clear(); - processedStr.str(""); - } - - return processed; -} - -//std::string PromelaCodeAnalyzer::prefixIdentifiers(const std::string& expr, const std::string& prefix) { -// PromelaParser parsed(expr); -// std::list<size_t> posList = getTokenPositions(expr, PML_NAME, parsed.ast); -// posList.sort(); -// -// std::stringstream prefixed; -// std::list<size_t>::iterator posIter = posList.begin(); -// size_t lastPos = 0; -// while (posIter != posList.end()) { -// prefixed << expr.substr(lastPos, *posIter - lastPos) << prefix; -// lastPos = *posIter; -// posIter++; -// } -// -// prefixed << expr.substr(lastPos, expr.size() - lastPos); -// return prefixed.str(); -//} - -std::list<std::pair<size_t, size_t> > PromelaCodeAnalyzer::getTokenPositions(const std::string& expr, int type, PromelaParserNode* ast) { - std::list<std::pair<size_t, size_t> > posList; - if (ast->type == type && ast->loc != NULL) { -// ast->dump(); - if (type == PML_NAME && ast->parent && - ((ast->parent->type == PML_CMPND && ast->parent->operands.front() != ast) || - (ast->parent->parent && ast->parent->type == PML_VAR_ARRAY && ast->parent->parent->type == PML_CMPND))) { - // field in a compound - } else { - if (ast->loc->firstLine == 0) { - posList.push_back(std::make_pair(ast->loc->firstCol, ast->loc->lastCol)); - } else { - int line = ast->loc->firstLine; - size_t lastPos = 0; - while(line > 0) { - lastPos = expr.find_first_of('\n', lastPos + 1); - line--; - } - posList.push_back(std::make_pair(lastPos + ast->loc->firstCol, lastPos + ast->loc->lastCol)); - } - } - } - for (std::list<PromelaParserNode*>::iterator opIter = ast->operands.begin(); opIter != ast->operands.end(); opIter++) { - std::list<std::pair<size_t, size_t> > tmp = getTokenPositions(expr, type, *opIter); - posList.insert(posList.end(), tmp.begin(), tmp.end()); - } - return posList; -} - -std::set<std::string> PromelaCodeAnalyzer::getEventsWithPrefix(const std::string& prefix) { - std::set<std::string> eventNames; - std::list<TrieNode*> trieNodes = _eventTrie.getWordsWithPrefix(prefix); - - std::list<TrieNode*>::iterator trieIter = trieNodes.begin(); - while(trieIter != trieNodes.end()) { - eventNames.insert((*trieIter)->value); - trieIter++; - } - - return eventNames; -} - -ChartToPromela::~ChartToPromela() { - if (_analyzer != NULL) - delete(_analyzer); - for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator nestedIter = _machines.begin(); nestedIter != _machines.end(); nestedIter++) { - nestedIter->second->_analyzer = NULL; - delete (nestedIter->second); - } -} - - -void ChartToPromela::writeEvents(std::ostream& stream) { - std::map<std::string, int> events = _analyzer->getEvents(); - std::map<std::string, int>::iterator eventIter = events.begin(); - stream << "/* event name identifiers */" << std::endl; - while(eventIter != events.end()) { - if (eventIter->first.length() > 0) { - stream << "#define " << _analyzer->macroForLiteral(eventIter->first) << " " << _analyzer->indexForLiteral(eventIter->first); - stream << " /* from \"" << eventIter->first << "\" */" << std::endl; - } - eventIter++; - } -} - -void ChartToPromela::writeStates(std::ostream& stream) { - stream << "/* state name identifiers */" << std::endl; - - std::map<std::string, GlobalState*>::iterator stateIter = _activeConf.begin(); - while(stateIter != _activeConf.end()) { - stream << "#define " << "s" << stateIter->second->activeIndex << " " << stateIter->second->activeIndex; - stream << " /* from \"" << stateIter->first << "\" */" << std::endl; - stateIter++; - } - -// for (size_t i = 0; i < _globalConf.size(); i++) { -// stream << "#define " << "s" << i << " " << i; -// stream << " /* from \"" << ATTR_CAST(_globalStates[i], "id") << "\" */" << std::endl; -// } -} - -void ChartToPromela::writeStateMap(std::ostream& stream) { - stream << "/* original state names */" << std::endl; - std::map<std::string, int> origStates = _analyzer->getOrigStates(); - for (std::map<std::string, int>::iterator origIter = origStates.begin(); origIter != origStates.end(); origIter++) { - stream << "#define " << _analyzer->macroForLiteral(origIter->first) << " " << origIter->second; - stream << " /* from \"" << origIter->first << "\" */" << std::endl; - } - -// std::map<std::string, int> states = _analyzer->getStates(); -// size_t stateIndex = 0; -// for (std::map<std::string, int>::iterator stateIter = states.begin(); stateIter != states.end(); stateIter++) { -// stream << "_x" -// std::list<std::string> origStates = _analyzer->getOrigState(stateIter->first); -// size_t origIndex = 0; -// for (std::list<std::string>::iterator origIter = origStates.begin(); origIter != origStates.end(); origIter++) { -// -// } -// } -} - -void ChartToPromela::writeHistoryArrays(std::ostream& stream) { - std::map<std::string, std::map<std::string, size_t> >::iterator histNameIter = _historyMembers.begin(); - while(histNameIter != _historyMembers.end()) { - stream << "/* history assignments for " << histNameIter->first << std::endl; - std::map<std::string, size_t>::iterator histMemberIter = histNameIter->second.begin(); - while(histMemberIter != histNameIter->second.end()) { - stream << " " << histMemberIter->second << ": " << histMemberIter->first << std::endl;; - histMemberIter++; - } - 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 << "/* type definitions */" << std::endl; - PromelaCodeAnalyzer::PromelaTypedef typeDefs = _analyzer->getTypes(); - if (typeDefs.types.size() == 0) - return; - - std::list<PromelaCodeAnalyzer::PromelaTypedef> individualDefs; - std::list<PromelaCodeAnalyzer::PromelaTypedef> currDefs; - currDefs.push_back(typeDefs); - - while(currDefs.size() > 0) { - if (std::find(individualDefs.begin(), individualDefs.end(), currDefs.front()) == individualDefs.end()) { - individualDefs.push_back(currDefs.front()); - for (std::map<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator typeIter = currDefs.front().types.begin(); typeIter != currDefs.front().types.end(); typeIter++) { - currDefs.push_back(typeIter->second); - } - } - currDefs.pop_front(); - } - individualDefs.pop_front(); - - for (std::list<PromelaCodeAnalyzer::PromelaTypedef>::reverse_iterator rIter = individualDefs.rbegin(); rIter != individualDefs.rend(); rIter++) { - PromelaCodeAnalyzer::PromelaTypedef currDef = *rIter; - - if (currDef.types.size() == 0 || currDef.name.size() == 0) - continue; - - stream << "typedef " << currDef.name << " {" << std::endl; - if (currDef.name.compare("_event_t") ==0) { - if (_analyzer->usesEventField("delay")) { - // make sure delay is the first member for sorted enqueuing to work - stream << " int delay;" << std::endl; -#if NEW_DELAY_RESHUFFLE -#else - stream << " int seqNr;" << std::endl; -#endif - } - stream << " int name;" << std::endl; - if (_analyzer->usesEventField("invokeid")) { - stream << " int invokeid;" << std::endl; - } - } - for (std::map<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator tIter = currDef.types.begin(); tIter != currDef.types.end(); tIter++) { - if (currDef.name.compare("_event_t") == 0 && (tIter->first.compare("name") == 0 || - tIter->first.compare("seqNr") == 0 || - tIter->first.compare("invokeid") == 0 || - tIter->first.compare("delay") == 0)) { // special treatment for _event - continue; - } - if (currDef.name.compare("_x_t") == 0 && tIter->first.compare("states") == 0) { - stream << " bool states[" << _analyzer->getOrigStates().size() << "];" << std::endl; - continue; - } - if (tIter->second.types.size() == 0) { - stream << " " << declForRange(tIter->first, tIter->second.minValue, tIter->second.maxValue, true) << ";" << std::endl; // not further nested -// stream << " int " << tIter->first << ";" << std::endl; // not further nested - } else { - stream << " " << tIter->second.name << " " << tIter->first << ";" << std::endl; - } - } - stream << "};" << std::endl << std::endl; - } - -// stream << "/* typedef instances */" << std::endl; -// PromelaCodeAnalyzer::PromelaTypedef allTypes = _analyzer->getTypes(); -// std::map<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator typeIter = allTypes.types.begin(); -// while(typeIter != allTypes.types.end()) { -// if (typeIter->second.types.size() > 0) { -// // an actual typedef -// stream << "hidden " << typeIter->second.name << " " << typeIter->first << ";" << std::endl; -// } else { -// stream << "hidden " << declForRange(typeIter->first, typeIter->second.minValue, typeIter->second.maxValue) << ";" << std::endl; -// } -// typeIter++; -// } - -} - -std::string ChartToPromela::declForRange(const std::string& identifier, long minValue, long maxValue, bool nativeOnly) { -// return "int " + identifier; // just for testing - - // we know nothing about this type - if (minValue == 0 && maxValue == 0) - return "int " + identifier; - - if (minValue < 0) { - // only short or int for negatives - if (minValue < -32769 || maxValue > 32767) - return "int " + identifier; - return "short " + identifier; - } - - // type is definitely positive - if (nativeOnly) { - if (maxValue > 32767) - return "int " + identifier; - if (maxValue > 255) - return "short " + identifier; - if (maxValue > 1) - return "byte " + identifier; - return "bool " + identifier; - } else { - return "unsigned " + identifier + " : " + toStr(BIT_WIDTH(maxValue)); - } -} - - -void ChartToPromela::writeInlineComment(std::ostream& stream, const Arabica::DOM::Node<std::string>& node) { - if (node.getNodeType() != Node_base::COMMENT_NODE) - return; - - std::string comment = node.getNodeValue(); - boost::trim(comment); - if (!boost::starts_with(comment, "#promela-inline")) - return; - - std::stringstream ssLine(comment); - std::string line; - std::getline(ssLine, line); // consume first line - while(std::getline(ssLine, line)) { - if (line.length() == 0) - continue; - stream << line; - } -} - -std::string ChartToPromela::conditionForHistoryTransition(const GlobalTransition* transition) { - FlatStateIdentifier flatSource(transition->source); - FlatStateIdentifier flatTarget(transition->destination); - std::string condition; - - return condition; -} - -std::string ChartToPromela::conditionalizeForHist(GlobalTransition* transition, int indent) { - std::set<GlobalTransition*> transitions; - transitions.insert(transition); - return conditionalizeForHist(transitions); -} - -std::string ChartToPromela::conditionalizeForHist(const std::set<GlobalTransition*>& transitions, int indent) { - std::stringstream condition; - std::string memberSep; - - std::set<std::map<std::string, std::list<std::string> > > histSeen; - - for (std::set<GlobalTransition*>::const_iterator transIter = transitions.begin(); transIter != transitions.end(); transIter++) { - if ((*transIter)->histTargets.size() == 0) // there are no history transitions in here! - continue; - - std::map<std::string, std::list<std::string> > relevantHist; - std::map<std::string, std::list<std::string> > currentHist; - FlatStateIdentifier flatSource((*transIter)->source); - currentHist = flatSource.getHistory(); - - std::set<std::string>::iterator histTargetIter = (*transIter)->histTargets.begin(); - while(histTargetIter != (*transIter)->histTargets.end()) { - if (currentHist.find(*histTargetIter) != currentHist.end()) { - relevantHist[*histTargetIter] = currentHist[*histTargetIter]; - } - histTargetIter++; - } - if (relevantHist.size() == 0) - continue; - - if (histSeen.find(relevantHist) != histSeen.end()) - continue; - histSeen.insert(relevantHist); - - std::string itemSep; - std::map<std::string, std::list<std::string> >::iterator relevanthistIter = relevantHist.begin(); - - if (relevantHist.size() > 0) - condition << memberSep; - - while(relevanthistIter != relevantHist.end()) { - std::list<std::string>::iterator histItemIter = relevanthistIter->second.begin(); - while(histItemIter != relevanthistIter->second.end()) { - assert(_historyMembers.find(relevanthistIter->first) != _historyMembers.end()); - assert(_historyMembers[relevanthistIter->first].find(*histItemIter) != _historyMembers[relevanthistIter->first].end()); - condition << itemSep << _prefix << "_hist_" << boost::to_lower_copy(_analyzer->macroForLiteral(relevanthistIter->first)) << "[" << _historyMembers[relevanthistIter->first][*histItemIter] << "]"; - itemSep = " && "; - histItemIter++; - } - relevanthistIter++; - } - - if (relevantHist.size() > 0) - memberSep = " || "; - - } - if (condition.str().size() > 0) { - return "(" + condition.str() + ")"; - } else { - assert(false); - } - return "true"; -} - -//std::list<GlobalTransition::Action> ChartToPromela::getTransientContent(GlobalTransition* transition) { -// std::list<GlobalTransition::Action> content; -// GlobalTransition* currTrans = transition; -// for (;;) { -// if (!HAS_ATTR(currState, "transient") || !DOMUtils::attributeIsTrue(ATTR(currState, "transient"))) -// break; -// content.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "invoke", currState)); -// content.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "onentry", currState)); -// content.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "onexit", currState)); -// NodeSet<std::string> transitions = DOMUtils::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 (size_t i = 0; i < indent; i++) { - padding += " "; - } - std::list<GlobalTransition*>::const_iterator histIter; - - if (envVarIsTrue("USCXML_ANNOTATE_NOCOMMENT")) { - stream << std::endl << _prefix << "t" << transition->index << ": /* ######################## */ " << std::endl; - - } else { - - stream << std::endl << _prefix << "t" << transition->index << ": /* ######################## " << std::endl; - FlatStateIdentifier flatActiveSource(transition->source); - stream << " from state: "; - PRETTY_PRINT_LIST(stream, flatActiveSource.getActive()); - stream << std::endl; - // stream << " with history: " << flatActiveSource.getFlatHistory() << std::endl; - stream << " ----- on event: " << (transition->eventDesc.size() > 0 ? transition->eventDesc : "SPONTANEOUS") << " --" << std::endl; - stream << " to state: "; - std::set<FlatStateIdentifier> destinations; - destinations.insert(FlatStateIdentifier(transition->destination)); - histIter = transition->historyTrans.begin(); - while(histIter != transition->historyTrans.end()) { - destinations.insert(FlatStateIdentifier((*histIter)->destination)); - histIter++; - } - std::string seperator = ""; - for (std::set<FlatStateIdentifier>::iterator destIter = destinations.begin(); destIter != destinations.end(); destIter++) { - stream << seperator; - PRETTY_PRINT_LIST(stream, destIter->getActive()); - stream << " with " << (destIter->getFlatHistory().size() > 0 ? destIter->getFlatHistory() : "no history"); - seperator = "\n "; - } - stream << std::endl; - - stream << "############################### */" << std::endl; - } - stream << std::endl; - stream << padding << "skip;" << std::endl; - stream << padding << "d_step {" << std::endl; - if (_writeTransitionPrintfs) - stream << padding << " printf(\"Taking Transition " << _prefix << "t" << transition->index << "\\n\");" << std::endl; - - padding += " "; - indent++; - - // iterators of history transitions executable content - std::map<GlobalTransition*, std::pair<GlobalTransition::Action::iter_t, GlobalTransition::Action::iter_t> > actionIters; - std::map<GlobalTransition*, std::set<GlobalTransition::Action> > actionsInTransition; - - typedef std::map<GlobalTransition*, std::pair<GlobalTransition::Action::iter_t, GlobalTransition::Action::iter_t> > actionIters_t; - - histIter = transition->historyTrans.begin(); - while(histIter != transition->historyTrans.end()) { - actionIters.insert(std::make_pair((*histIter), std::make_pair((*histIter)->actions.begin(), (*histIter)->actions.end()))); - // add history transitions actions to the set - for (std::list<GlobalTransition::Action>::iterator actionIter = (*histIter)->actions.begin(); actionIter != (*histIter)->actions.end(); actionIter++) { - actionsInTransition[*histIter].insert(*actionIter); - } -// std::copy((*histIter)->actions.begin(), (*histIter)->actions.end(), std::inserter(actionsInTransition[*histIter], actionsInTransition[*histIter].begin())); - histIter++; - } -// std::cout << "###" << std::endl; - for (std::list<GlobalTransition::Action>::iterator actionIter = transition->actions.begin(); actionIter != transition->actions.end(); actionIter++) { - actionsInTransition[transition].insert(*actionIter); - } -// std::copy(transition->actions.begin(), transition->actions.end(), std::inserter(actionsInTransition[transition], actionsInTransition[transition].begin())); - - -// GlobalTransition::Action action; - std::set<GlobalTransition*> allBut; - std::list<ExecContentSeqItem> ecSeq; - - for (std::list<GlobalTransition::Action>::const_iterator actionIter = transition->actions.begin(); actionIter != transition->actions.end(); actionIter++) { - // for every executable content in base transition - const GlobalTransition::Action& baseAction = *actionIter; - allBut.clear(); - - for (actionIters_t::iterator histActionIter = actionIters.begin(); histActionIter != actionIters.end(); histActionIter++) { - // iterate every history transition - GlobalTransition* histTrans = histActionIter->first; - if (histActionIter->second.first == histActionIter->second.second) // TODO: is this correct? - continue; - GlobalTransition::Action& histAction = *(histActionIter->second.first); - - // is the current action identical or a generated raise for done.state.ID? -// std::cerr << baseAction << std::endl; -// std::cerr << histAction << std::endl; - if (baseAction != histAction && !baseAction.raiseDone) { -// std::cout << baseAction << std::endl; -// std::cout << histAction << std::endl; - - // executable content differs - will given executable content appear later in history? - if (actionsInTransition[histTrans].find(baseAction) != actionsInTransition[histTrans].end()) { - // yes -> write all exec content exclusive to this history transition until base executable content - while(baseAction != *(histActionIter->second.first)) { - histAction = *(histActionIter->second.first); - ecSeq.push_back(ExecContentSeqItem(ExecContentSeqItem::EXEC_CONTENT_ONLY_FOR, histTrans, histAction)); - actionsInTransition[histTrans].erase(histAction); - histActionIter->second.first++; - } - } else { - // no -> exclude this history transition - allBut.insert(histTrans); - } - } else { - // that's great, they are equal, just increase iterator - histActionIter->second.first++; - } - } - - if (allBut.empty()) { - // everyone has the current actionIter one behind the base action - ecSeq.push_back(ExecContentSeqItem(ExecContentSeqItem::EXEC_CONTENT_EVERY, NULL, baseAction)); - } else { - // everyone but some have this content - ecSeq.push_back(ExecContentSeqItem(ExecContentSeqItem::EXEC_CONTENT_ALL_BUT, allBut, baseAction)); - } - } - - // see what remains in history transitions and add as exclusive - for (actionIters_t::iterator histActionIter = actionIters.begin(); histActionIter != actionIters.end(); histActionIter++) { - GlobalTransition* histTrans = histActionIter->first; - - while(histActionIter->second.first != histActionIter->second.second) { - GlobalTransition::Action& histAction = *(histActionIter->second.first); - ecSeq.push_back(ExecContentSeqItem(ExecContentSeqItem::EXEC_CONTENT_ONLY_FOR, histTrans, histAction)); - histActionIter->second.first++; - } - } - - bool isConditionalized = false; - bool wroteHistoryAssignments = false; - - for (std::list<ExecContentSeqItem>::const_iterator ecIter = ecSeq.begin(); ecIter != ecSeq.end(); ecIter++) { - const GlobalTransition::Action& action = ecIter->action; - - if (action.exited) { - // first onexit handler writes history assignments - if (!wroteHistoryAssignments) { - writeHistoryAssignments(stream, transition, indent); - wroteHistoryAssignments = true; - } - } - - if (!_analyzer->usesInPredicate() && (action.entered || action.exited)) { - continue; - } - - if (!isConditionalized && ecIter->type == ExecContentSeqItem::EXEC_CONTENT_ONLY_FOR) { -// assert(!wroteHistoryAssignments); // we need to move assignments after dispatching? - stream << padding << "if" << std::endl; - stream << padding << ":: " << conditionalizeForHist(ecIter->transitions) << " -> {" << std::endl; - padding += " "; - indent++; - isConditionalized = true; - } else if (!isConditionalized && ecIter->type == ExecContentSeqItem::EXEC_CONTENT_ALL_BUT) { -// assert(!wroteHistoryAssignments); // we need to move assignments after dispatching? - stream << padding << "if" << std::endl; - stream << padding << ":: " << conditionalizeForHist(ecIter->transitions) << " -> skip;" << std::endl; - stream << padding << ":: else -> {" << std::endl; - padding += " "; - indent++; - isConditionalized = true; - } - -#if 0 - switch (ecIter->type) { - case ExecContentSeqItem::EXEC_CONTENT_ALL_BUT: - std::cout << "ALL_BUT" << std::endl; - break; - case ExecContentSeqItem::EXEC_CONTENT_EVERY: - std::cout << "EVERY" << std::endl; - break; - case ExecContentSeqItem::EXEC_CONTENT_ONLY_FOR: - std::cout << "ONLY_FOR" << std::endl; - break; - - default: - break; - } -#endif - - if (action.exited) { - // we left a state - stream << padding << _prefix << "_x.states[" << _analyzer->macroForLiteral(ATTR(action.exited, "id")) << "] = false; " << std::endl; -// continue; - } - - if (action.entered) { - // we entered a state - stream << padding << _prefix << "_x.states[" << _analyzer->macroForLiteral(ATTR(action.entered, "id")) << "] = true; " << std::endl; -// continue; - } - - if (action.transition) { - // this is executable content from a transition - stream << "/* 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 << "/* 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 << "/* executable content for entering state " << ATTR_CAST(action.onEntry.getParentNode(), "id") << " */" << std::endl; - writeExecutableContent(stream, action.onEntry, indent); -// continue; - } - - if (action.raiseDone) { - // executable content from an onentry element - if (action.raiseDone.getParentNode()) // this should not be necessary? - stream << "/* raising done event for " << ATTR_CAST(action.raiseDone.getParentNode(), "id") << " */" << std::endl; - writeExecutableContent(stream, action.raiseDone, indent); - // continue; - } - - if (action.invoke) { - // an invoke element - - if (_machines.find(action.invoke) != _machines.end()) { - stream << padding << _prefix << "start!" << _analyzer->macroForLiteral(_machines[action.invoke]->_invokerid) << ";" << std::endl; - } else { - if (HAS_ATTR_CAST(action.invoke, "id")) { - stream << padding << _prefix << ATTR_CAST(action.invoke, "id") << "Running = true;" << std::endl; - } - } - - } - - if (action.uninvoke) { - if (_machines.find(action.uninvoke) != _machines.end()) { - stream << padding << "do" << std::endl; - stream << padding << ":: " << _prefix << "start??" << _analyzer->macroForLiteral(_machines[action.uninvoke]->_invokerid) << " -> skip" << std::endl; - stream << padding << ":: else -> break;" << std::endl; - stream << padding << "od" << std::endl; - - stream << padding << _machines[action.uninvoke]->_prefix << "canceled = true;" << std::endl; - if (_analyzer->usesEventField("delay")) { - stream << padding << "removePendingEventsForInvoker(" << _analyzer->macroForLiteral(_machines[action.uninvoke]->_invokerid) << ");" << std::endl; - } - } else { - if (HAS_ATTR_CAST(action.uninvoke, "id")) { - stream << padding << _prefix << ATTR_CAST(action.uninvoke, "id") << "Running = false;" << std::endl; - } - } - } - - if (isConditionalized) { - // peek into next content and see if same conditions apply -> keep conditionalization - bool sameCondition = false; - std::list<ExecContentSeqItem>::const_iterator nextIter = ecIter; - nextIter++; - if (nextIter != ecSeq.end() && ecIter->type == nextIter->type && ecIter->transitions == nextIter->transitions) { - sameCondition = true; - } - - if (!sameCondition) { - padding = padding.substr(2); - indent--; - - if (ecIter->type == ExecContentSeqItem::EXEC_CONTENT_ALL_BUT) { - stream << padding << "}" << std::endl; - stream << padding << "fi" << std::endl << std::endl; - } else if(ecIter->type == ExecContentSeqItem::EXEC_CONTENT_ONLY_FOR) { - stream << padding << "}" << std::endl; - stream << padding << ":: else -> skip;" << std::endl; - stream << padding << "fi;" << std::endl << std::endl; - } - isConditionalized = false; - } - } - } - - if (!wroteHistoryAssignments) { - writeHistoryAssignments(stream, transition, indent); - wroteHistoryAssignments = true; - } - - // write new state assignment and goto dispatching - GlobalState* origNewState = NULL; - - // sort history transitions by new active state - std::map<GlobalState*, std::set<GlobalTransition*> > histTargets; - histIter = transition->historyTrans.begin(); - while(histIter != transition->historyTrans.end()) { - origNewState = _activeConf[(*histIter)->activeDestination]; - assert(origNewState != NULL); - histTargets[origNewState].insert(*histIter); - histIter++; - } - - origNewState = _activeConf[transition->activeDestination]; - bool hasHistoryTarget = false; - - for (std::map<GlobalState*, std::set<GlobalTransition*> >::const_iterator histTargetIter = histTargets.begin(); histTargetIter != histTargets.end(); histTargetIter++) { - GlobalState* histNewState = histTargetIter->first; - if (histNewState == origNewState) - continue; - stream << padding << "if" << std::endl; - - if (!envVarIsTrue("USCXML_ANNOTATE_NOCOMMENT")) { - stream << "/* to state "; - FlatStateIdentifier flatActiveDest(histNewState->activeId); - PRETTY_PRINT_LIST(stream, flatActiveDest.getActive()); - stream << " via history */" << std::endl; - } - - stream << padding << ":: " << conditionalizeForHist(histTargetIter->second) << " -> " << _prefix << "s = s" << histNewState->activeIndex << ";" << std::endl; -// writeTransitionClosure(stream, *histTargetIter->second.begin(), histNewState, indent + 1); // is this correct for everyone in set? - - - hasHistoryTarget = true; - } - - origNewState = _activeConf[transition->activeDestination]; - FlatStateIdentifier flatActiveDest(transition->activeDestination); - assert(origNewState != NULL); - - if (!envVarIsTrue("USCXML_ANNOTATE_NOCOMMENT")) { - stream << "/* to state "; - PRETTY_PRINT_LIST(stream, flatActiveDest.getActive()); - stream << " */" << std::endl; - } - if (hasHistoryTarget) { - stream << padding << ":: else -> "; - padding += " "; - indent++; - } - - stream << padding << _prefix << "s = s" << origNewState->activeIndex << ";" << std::endl; - - - if (hasHistoryTarget) { - padding = padding.substr(2); - indent--; -// stream << padding << "}" << std::endl; - stream << padding << "fi;" << std::endl; - } - - TRANSITION_TRACE(transition, false); - - padding = padding.substr(2); - stream << padding << "}" << std::endl; - - // moved up here for goto from d_step - writeTransitionClosure(stream, transition, origNewState, indent-1); - - _perfTransProcessed++; - _perfTransTotal++; - - DUMP_STATS(false); - -} - -void ChartToPromela::writeHistoryAssignments(std::ostream& stream, GlobalTransition* transition, int indent) { - std::string padding; - for (size_t i = 0; i < indent; i++) { - padding += " "; - } - - if (transition->historyTrans.size() == 0) - return; - - // GlobalState to *changed* history configuration - std::list<HistoryTransitionClass> histClasses; - - std::set<GlobalTransition*> allTrans; - allTrans.insert(transition); - allTrans.insert(transition->historyTrans.begin(), transition->historyTrans.end()); - - // iterate all transitions - std::set<GlobalTransition*>::iterator transIter = allTrans.begin(); - while(transIter != allTrans.end()) { - histClasses.push_back(HistoryTransitionClass(*transIter)); - transIter++; - } - - // nothing to do here - if (histClasses.size() == 0) - return; - -// std::cout << histClasses.size() << " / "; - - // now sort into equivalence classes - std::list<HistoryTransitionClass>::iterator outerHistClassIter = histClasses.begin(); - std::list<HistoryTransitionClass>::iterator innerHistClassIter = histClasses.begin(); - while(outerHistClassIter != histClasses.end()) { - HistoryTransitionClass& outerClass = *outerHistClassIter; - - // iterate inner iter for every outer iter and see if we can merge - innerHistClassIter = outerHistClassIter; - innerHistClassIter++; - - while(innerHistClassIter != histClasses.end()) { - // can we merge the inner class into the outer one? - HistoryTransitionClass& innerClass = *innerHistClassIter; - - if (outerClass.matches(innerClass)) { - outerClass.merge(innerClass); - histClasses.erase(innerHistClassIter++); - } else { - innerHistClassIter++; - } - } - - _perfHistoryProcessed++; - _perfHistoryTotal++; - - outerHistClassIter++; - } -// std::cout << histClasses.size() << std::endl; - - bool preambelWritten = false; - std::list<HistoryTransitionClass>::iterator histClassIter = histClasses.begin(); - std::list<HistoryTransitionClass>::iterator defaultHistClassIter = histClasses.end(); - size_t nrMembers = 0; - while(histClassIter != histClasses.end() || defaultHistClassIter != histClasses.end()) { - - // remember iterator position with default transition - if (histClassIter == histClasses.end() && defaultHistClassIter != histClasses.end()) { - histClassIter = defaultHistClassIter; - } else if (histClassIter->members.find(transition) != histClassIter->members.end()) { - defaultHistClassIter = histClassIter; - histClassIter++; - continue; - } - - nrMembers += histClassIter->members.size(); - - if (!preambelWritten && histClasses.size() > 1) { - stream << padding << "if" << std::endl; - preambelWritten = true; - } - - if (histClasses.size() > 1) { - stream << padding << "::" << conditionalizeForHist(histClassIter->members) << " {" << std::endl; - } - - { - std::map<std::string, std::set<std::string> >::iterator forgetIter = histClassIter->toForget.begin(); - while(forgetIter != histClassIter->toForget.end()) { - std::set<std::string>::iterator forgetMemberIter = forgetIter->second.begin(); - while(forgetMemberIter != forgetIter->second.end()) { - stream << padding << _prefix << "_hist_" << boost::to_lower_copy(_analyzer->macroForLiteral(forgetIter->first)); - stream << "[" << _historyMembers[forgetIter->first][*forgetMemberIter] << "] = 0;"; - stream << " \t/* " << *forgetMemberIter << " */" << std::endl; - forgetMemberIter++; - } - forgetIter++; - } - } - - { - std::map<std::string, std::set<std::string> >::iterator rememberIter = histClassIter->toRemember.begin(); - while(rememberIter != histClassIter->toRemember.end()) { - std::set<std::string>::iterator rememberMemberIter = rememberIter->second.begin(); - while(rememberMemberIter != rememberIter->second.end()) { - stream << padding << _prefix << "_hist_" << boost::to_lower_copy(_analyzer->macroForLiteral(rememberIter->first)); - stream << "[" << _historyMembers[rememberIter->first][*rememberMemberIter] << "] = 1;"; - stream << " \t/* " << *rememberMemberIter << " */" << std::endl; - rememberMemberIter++; - } - rememberIter++; - } - } - - if (histClasses.size() > 1) { - stream << padding << "}" << std::endl; - } - - if (histClassIter == defaultHistClassIter) { - break; - } - - histClassIter++; - } - assert(nrMembers == allTrans.size()); - -} - -HistoryTransitionClass::HistoryTransitionClass(GlobalTransition* transition) { - members.insert(transition); - init(transition->source, transition->destination); -} - -HistoryTransitionClass::HistoryTransitionClass(const std::string& from, const std::string& to) { - init(from, to); -} - -void HistoryTransitionClass::init(const std::string& from, const std::string& to) { - if (from == to) - return; - - FlatStateIdentifier flatSource(from); - FlatStateIdentifier flatTarget(to); - - std::map<std::string, std::set<std::string> > activeBefore = flatSource.getHistorySets(); - std::map<std::string, std::set<std::string> > activeAfter = flatTarget.getHistorySets(); - - std::map<std::string, std::set<std::string> >::const_iterator targetHistIter = activeAfter.begin(); - while(targetHistIter != activeAfter.end()) { - // for every history state in target, see if it existed in source - if (activeBefore.find(targetHistIter->first) == activeBefore.end()) { - // this target history did not exist source -> every item is changed - std::set<std::string>::const_iterator histMemberIter = activeAfter.at(targetHistIter->first).begin(); - while(histMemberIter != activeAfter.at(targetHistIter->first).end()) { - toRemember[targetHistIter->first].insert(*histMemberIter); - histMemberIter++; - } - } else { - // this target *did* already exist, but was it equally assigned? - std::set<std::string>::const_iterator sourceHistMemberIter = activeBefore.at(targetHistIter->first).begin(); - while(sourceHistMemberIter != activeBefore.at(targetHistIter->first).end()) { - // iterate every item in source and try to find it in target - if (targetHistIter->second.find(*sourceHistMemberIter) == targetHistIter->second.end()) { - // no, source is no longer in target - toForget[targetHistIter->first].insert(*sourceHistMemberIter); - } else { - toKeep[targetHistIter->first].insert(*sourceHistMemberIter); - } - sourceHistMemberIter++; - } - - std::set<std::string>::const_iterator targetHistMemberIter = activeAfter.at(targetHistIter->first).begin(); - while(targetHistMemberIter != activeAfter.at(targetHistIter->first).end()) { - // iterate member of target history and see if it is new - if (activeBefore.at(targetHistIter->first).find(*targetHistMemberIter) == activeBefore.at(targetHistIter->first).end()) { - // not found -> new assignment - toRemember[targetHistIter->first].insert(*targetHistMemberIter); - } - targetHistMemberIter++; - } - } - targetHistIter++; - } -} - -bool HistoryTransitionClass::matches(const HistoryTransitionClass& other) { - - /* does the given transition match this one?: - 1. everything remembered has to be remembered as well or already enabled - 2. everything forgot has to be forgotten as well or already disabled - and vice versa - */ - - std::map<std::string, std::set<std::string> > tmp; - - typedef std::map<std::string, std::set<std::string> >::const_iterator histIter_t; - typedef std::set<std::string>::const_iterator histMemberIter_t; - - // we will remember these - will the other try to forget them? - INTERSECT_MAPS(toRemember, other.toForget, tmp); - if (tmp.size() > 0) - return false; - - // we will keep these - will the other try to forget them? - INTERSECT_MAPS(toKeep, other.toForget, tmp); - if (tmp.size() > 0) - return false; - - // we will forget these - will the other try to keep or even remember? - INTERSECT_MAPS(toForget, other.toKeep, tmp); - if (tmp.size() > 0) - return false; - INTERSECT_MAPS(toForget, other.toRemember, tmp); - if (tmp.size() > 0) - return false; - - return true; -} - -void HistoryTransitionClass::merge(const HistoryTransitionClass& other) { - members.insert(other.members.begin(), other.members.end()); - - std::map<std::string, std::set<std::string> >::const_iterator histIter; - - histIter = other.toRemember.begin(); - while(histIter != other.toRemember.end()) { - toRemember[histIter->first].insert(histIter->second.begin(), histIter->second.end()); - histIter++; - } - - histIter = other.toForget.begin(); - while(histIter != other.toForget.end()) { - toForget[histIter->first].insert(histIter->second.begin(), histIter->second.end()); - histIter++; - } - - histIter = other.toKeep.begin(); - while(histIter != other.toKeep.end()) { - toKeep[histIter->first].insert(histIter->second.begin(), histIter->second.end()); - histIter++; - } - -} - -void ChartToPromela::writeTransitionClosure(std::ostream& stream, GlobalTransition* transition, GlobalState* state, int indent) { - std::string padding; - for (size_t i = 0; i < indent; i++) { - padding += " "; - } - -// if (_traceTransitions) { -// for (std::set<int>::iterator transRefIter = transition->transitionRefs.begin(); transRefIter != transition->transitionRefs.end(); transRefIter++) { -// stream << padding << _prefix << "transitions[" << *transRefIter << "] = false; " << std::endl; -// } -// } - - if (state->isFinal) { - stream << padding << "goto " << _prefix << "terminate;" << std::endl; - } else { - if (!transition->isEventless) { - stream << padding << _prefix << "spontaneous = true;" << std::endl; - } - stream << padding << "goto " << _prefix << "microStep;" << std::endl; - } -} - -void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica::DOM::Node<std::string>& node, int indent) { - if (!node) - return; - - std::string padding; - for (size_t i = 0; i < indent; i++) { - padding += " "; - } - - if (node.getNodeType() == Node_base::TEXT_NODE) { - if (boost::trim_copy(node.getNodeValue()).length() > 0) - stream << beautifyIndentation(ADAPT_SRC(node.getNodeValue()), indent) << std::endl; - } - - if (node.getNodeType() != Node_base::ELEMENT_NODE) - return; // skip anything not an element - - Arabica::DOM::Element<std::string> nodeElem = Arabica::DOM::Element<std::string>(node); - - if (false) { - } else if(TAGNAME(nodeElem) == "onentry" || TAGNAME(nodeElem) == "onexit" || TAGNAME(nodeElem) == "transition" || TAGNAME(nodeElem) == "finalize") { - // descent into childs and write their contents - Arabica::DOM::Node<std::string> child = node.getFirstChild(); - while(child) { - writeExecutableContent(stream, child, indent); - child = child.getNextSibling(); - } - } else if(TAGNAME(nodeElem) == "script") { - NodeSet<std::string> scriptText = DOMUtils::filterChildType(Node_base::TEXT_NODE, node, true); - for (size_t i = 0; i < scriptText.size(); i++) { - stream << ADAPT_SRC(beautifyIndentation(scriptText[i].getNodeValue(), indent)) << std::endl; - } - - } else if(TAGNAME(nodeElem) == "log") { - std::string label = (HAS_ATTR(nodeElem, "label") ? ATTR(nodeElem, "label") : ""); - std::string expr = (HAS_ATTR(nodeElem, "expr") ? ADAPT_SRC(ATTR(nodeElem, "expr")) : ""); - std::string trimmedExpr = boost::trim_copy(expr); - bool isStringLiteral = (boost::starts_with(trimmedExpr, "\"") || boost::starts_with(trimmedExpr, "'")); - - std::string formatString; - std::string varString; - std::string seperator; - - if (label.size() > 0) { - if (expr.size() > 0) { - formatString += label + ": "; - } else { - formatString += label; - } - } - - if (isStringLiteral) { - formatString += expr; - } else if (expr.size() > 0) { - formatString += "%d"; - varString += seperator + expr; - } - - if (varString.length() > 0) { - stream << padding << "printf(\"" + formatString + "\", " + varString + ");" << std::endl; - } else { - stream << padding << "printf(\"" + formatString + "\");" << std::endl; - } - - } else if(TAGNAME(nodeElem) == "foreach") { - stream << padding << "for (" << _prefix << (HAS_ATTR(nodeElem, "index") ? ATTR(nodeElem, "index") : "_index") << " in " << _prefix << ATTR(nodeElem, "array") << ") {" << std::endl; - if (HAS_ATTR(nodeElem, "item")) { - stream << padding << " " << _prefix << ATTR(nodeElem, "item") << " = " << _prefix << ATTR(nodeElem, "array") << "[" << _prefix << (HAS_ATTR(nodeElem, "index") ? ATTR(nodeElem, "index") : "_index") << "];" << std::endl; - } - Arabica::DOM::Node<std::string> child = node.getFirstChild(); - while(child) { - writeExecutableContent(stream, child, indent + 1); - child = child.getNextSibling(); - } -// if (HAS_ATTR(nodeElem, "index")) -// stream << padding << " " << _prefix << ATTR(nodeElem, "index") << "++;" << std::endl; - stream << padding << "}" << std::endl; - - } else if(TAGNAME(nodeElem) == "if") { - NodeSet<std::string> condChain; - condChain.push_back(node); - condChain.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "elseif", node)); - condChain.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "else", node)); - - writeIfBlock(stream, condChain, indent); - - } else if(TAGNAME(nodeElem) == "assign") { - NodeSet<std::string> assignTexts = DOMUtils::filterChildType(Node_base::TEXT_NODE, nodeElem, true); - assert(assignTexts.size() > 0); - stream << beautifyIndentation(ADAPT_SRC(boost::trim_copy(assignTexts[0].getNodeValue())), indent) << std::endl; - - } else if(TAGNAME(nodeElem) == "send" || TAGNAME(nodeElem) == "raise") { - std::string targetQueue; - std::string insertOp = "!"; - if (TAGNAME(nodeElem) == "raise") { - targetQueue = _prefix + "iQ"; - } else if (!HAS_ATTR(nodeElem, "target")) { - 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) { - targetQueue = _parent->_prefix + "eQ"; - } else if (boost::starts_with(ATTR(nodeElem, "target"), "#_") && _machinesPerId.find(ATTR(nodeElem, "target").substr(2)) != _machinesPerId.end()) { - targetQueue = _machines[_machinesPerId[ATTR(nodeElem, "target").substr(2)]]->_prefix + "eQ"; - } - if (targetQueue.length() > 0) { - // this is for our external queue - std::string event; - - if (HAS_ATTR(nodeElem, "event")) { - event = _analyzer->macroForLiteral(ATTR(nodeElem, "event")); - } else if (HAS_ATTR(nodeElem, "eventexpr")) { - event = ADAPT_SRC(ATTR(nodeElem, "eventexpr")); - } - if (_analyzer->usesComplexEventStruct()) { - stream << padding << "{" << std::endl; - std::string typeReset = _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), padding + " "); - std::stringstream typeAssignSS; - typeAssignSS << padding << " tmpE.name = " << event << ";" << std::endl; - - if (HAS_ATTR(nodeElem, "idlocation")) { - typeAssignSS << padding << " /* idlocation */" << std::endl; - typeAssignSS << padding << " _lastSendId = _lastSendId + 1;" << std::endl; - typeAssignSS << padding << " " << _prefix << ATTR(nodeElem, "idlocation") << " = _lastSendId;" << std::endl; - typeAssignSS << padding << " tmpE.sendid = _lastSendId;" << std::endl; - typeAssignSS << padding << " if" << std::endl; - typeAssignSS << padding << " :: _lastSendId == 2147483647 -> _lastSendId = 0;" << std::endl; - typeAssignSS << padding << " :: else -> skip;" << std::endl; - typeAssignSS << padding << " fi;" << std::endl; - } else if (HAS_ATTR(nodeElem, "id")) { - typeAssignSS << padding << " tmpE.sendid = " << _analyzer->macroForLiteral(ATTR(nodeElem, "id")) << ";" << std::endl; - } - - if (_invokerid.length() > 0) { // do not send invokeid if we send / raise to ourself - typeAssignSS << padding << " tmpE.invokeid = " << _analyzer->macroForLiteral(_invokerid) << ";" << std::endl; - } - - if (_analyzer->usesEventField("origintype") && !boost::ends_with(targetQueue, "iQ")) { - typeAssignSS << padding << " tmpE.origintype = " << _analyzer->macroForLiteral("http://www.w3.org/TR/scxml/#SCXMLEventProcessor") << ";" << std::endl; - } - - if (_analyzer->usesEventField("delay")) { -#if NEW_DELAY_RESHUFFLE -#else - insertOp += "!"; - typeAssignSS << padding << " _lastSeqId = _lastSeqId + 1;" << std::endl; -#endif - if (HAS_ATTR_CAST(nodeElem, "delay")) { - typeAssignSS << padding << " tmpE.delay = " << ATTR_CAST(nodeElem, "delay") << ";" << std::endl; - } else if (HAS_ATTR_CAST(nodeElem, "delayexpr")) { - typeAssignSS << padding << " tmpE.delay = " << ADAPT_SRC(ATTR_CAST(nodeElem, "delayexpr")) << ";" << std::endl; - } else { - typeAssignSS << padding << " tmpE.delay = 0;" << std::endl; - } -#if NEW_DELAY_RESHUFFLE -#else - typeAssignSS << padding << " tmpE.seqNr = _lastSeqId;" << std::endl; -#endif - } - - if (_analyzer->usesEventField("type")) { - std::string eventType = (targetQueue.compare("iQ!") == 0 ? _analyzer->macroForLiteral("internal") : _analyzer->macroForLiteral("external")); - typeAssignSS << padding << " tmpE.type = " << eventType << ";" << std::endl; - } - - NodeSet<std::string> sendParams = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "param", nodeElem); - NodeSet<std::string> sendContents = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "content", nodeElem); - std::string sendNameList = ATTR(nodeElem, "namelist"); - if (sendParams.size() > 0) { - for (size_t i = 0; i < sendParams.size(); i++) { - Element<std::string> paramElem = Element<std::string>(sendParams[i]); - typeAssignSS << padding << " tmpE.data." << ATTR(paramElem, "name") << " = " << ADAPT_SRC(ATTR(paramElem, "expr")) << ";" << std::endl; - } - } - if (sendNameList.size() > 0) { - std::list<std::string> nameListIds = tokenize(sendNameList); - std::list<std::string>::iterator nameIter = nameListIds.begin(); - while(nameIter != nameListIds.end()) { - typeAssignSS << padding << " tmpE.data." << *nameIter << " = " << ADAPT_SRC(*nameIter) << ";" << std::endl; - nameIter++; - } - } - - if (sendParams.size() == 0 && sendNameList.size() == 0 && sendContents.size() > 0) { - Element<std::string> contentElem = Element<std::string>(sendContents[0]); - if (contentElem.hasChildNodes() && contentElem.getFirstChild().getNodeType() == Node_base::TEXT_NODE) { - std::string content = spaceNormalize(contentElem.getFirstChild().getNodeValue()); - if (!isNumeric(content.c_str(), 10)) { - typeAssignSS << padding << " tmpE.data = " << _analyzer->macroForLiteral(content) << ";" << std::endl; - } else { - typeAssignSS << padding << " tmpE.data = " << content << ";" << std::endl; - } - } else if (HAS_ATTR(contentElem, "expr")) { - typeAssignSS << padding << " tmpE.data = " << ADAPT_SRC(ATTR(contentElem, "expr")) << ";" << std::endl; - } - } - - // remove all fields from typeReset that are indeed set by typeAssign -// for (std::string assigned; std::getline(typeAssignSS, assigned); ) { -// assigned = assigned.substr(0, assigned.find('=')); -// assigned = assigned.substr(assigned.find('.')); -// std::istringstream typeResetSS (typeReset); -// for (std::string reset; std::getline(typeResetSS, reset); ) { -// if (!boost::find_first(reset, assigned)) { -// stream << reset << std::endl; -// } -// } -// } -// stream << typeAssignSS.str(); - - std::istringstream typeResetSS (typeReset); - for (std::string reset; std::getline(typeResetSS, reset); ) { - std::string resetField = reset.substr(0, reset.find('=')); - resetField = resetField.substr(resetField.find('.')); - for (std::string assigned; std::getline(typeAssignSS, assigned); ) { - if (boost::find_first(resetField, assigned)) { - break; - } - } - stream << reset << std::endl; - } - stream << typeAssignSS.str(); - - - stream << padding << " " << targetQueue << insertOp <<"tmpE;" << std::endl; - -#if NEW_DELAY_RESHUFFLE - if (_analyzer->usesEventField("delay") && !boost::ends_with(targetQueue, "iQ")) { - stream << padding << " insertWithDelay(" << targetQueue << ");" << std::endl; - } -#endif - - stream << padding << "}" << std::endl; - } else { - stream << padding << targetQueue << insertOp << event << ";" << std::endl; - } - } - } else if(TAGNAME(nodeElem) == "cancel") { - 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); - } -} - -PromelaInlines::~PromelaInlines() { - return; -} - -std::list<PromelaInline*> PromelaInlines::getRelatedTo(const Arabica::DOM::Node<std::string>& node, PromelaInline::PromelaInlineType type) { - std::list<PromelaInline*> related; - - std::map<Arabica::DOM::Node<std::string>, std::list<PromelaInline*> >::iterator inlIter = inlines.begin(); - while (inlIter != inlines.end()) { - std::list<PromelaInline*>::iterator pmlIter = inlIter->second.begin(); - while (pmlIter != inlIter->second.end()) { - if ((type != PromelaInline::PROMELA_NIL || (*pmlIter)->type == type) && (*pmlIter)->relatesTo(node)) { - related.push_back(*pmlIter); - } - pmlIter++; - } - inlIter++; - } - return related; - - return related; -} - -std::list<PromelaInline*> PromelaInlines::getAllOfType(uint32_t type) { - std::list<PromelaInline*> related; - - std::map<Arabica::DOM::Node<std::string>, std::list<PromelaInline*> >::iterator inlIter = inlines.begin(); - while (inlIter != inlines.end()) { - std::list<PromelaInline*>::iterator pmlIter = inlIter->second.begin(); - while (pmlIter != inlIter->second.end()) { - if ((*pmlIter)->type & type) { - related.push_back(*pmlIter); - } - pmlIter++; - } - inlIter++; - } - return related; -} - -PromelaInline::PromelaInline(const Arabica::DOM::Node<std::string>& node) : prevSibling(NULL), nextSibling(NULL), type(PROMELA_NIL) { - if (node.getNodeType() != Node_base::COMMENT_NODE && node.getNodeType() != Node_base::TEXT_NODE) - return; // nothing to do - - std::stringstream ssLine(node.getNodeValue()); - std::string line; - - while(std::getline(ssLine, line)) { - // skip to first promela line - boost::trim(line); - if (boost::starts_with(line, "promela")) - break; - } - - if (!boost::starts_with(line, "promela")) - return; - - if (false) { - } else if (boost::starts_with(line, "promela-code")) { - type = PROMELA_CODE; - } else if (boost::starts_with(line, "promela-ltl")) { - type = PROMELA_LTL; - } else if (boost::starts_with(line, "promela-event-all")) { - type = PROMELA_EVENT_ALL_BUT; - } else if (boost::starts_with(line, "promela-event")) { - type = PROMELA_EVENT_ONLY; - } else if (boost::starts_with(line, "promela-progress")) { - type = PROMELA_PROGRESS_LABEL; - } else if (boost::starts_with(line, "promela-accept")) { - type = PROMELA_ACCEPT_LABEL; - } else if (boost::starts_with(line, "promela-end")) { - type = PROMELA_END_LABEL; - } - - std::stringstream contentSS; - size_t endType = line.find_first_of(": \n"); - - std::string seperator; - if (endType != std::string::npos && endType + 1 < line.size()) { - contentSS << line.substr(endType + 1, line.size() - endType + 1); - seperator = "\n"; - } - - while(std::getline(ssLine, line)) { - boost::trim(line); - if (boost::starts_with(line, "promela")) { - std::cerr << "Split multiple #promela pragmas into multiple comments!" << std::endl; - break; - } - contentSS << seperator << line; - seperator = "\n"; - } - content = contentSS.str(); -} - - -PromelaInlines::PromelaInlines(const Arabica::DOM::Node<std::string>& node) { - NodeSet<std::string> levelNodes; - levelNodes.push_back(node); - - size_t level = 0; - while(levelNodes.size() > 0) { - PromelaInline* predecessor = NULL; - - // iterate all nodes at given level - for (size_t i = 0; i < levelNodes.size(); i++) { - - // get all comments - NodeSet<std::string> comments = DOMUtils::filterChildType(Node_base::COMMENT_NODE, levelNodes[i]); - for (size_t j = 0; j < comments.size(); j++) { - PromelaInline* tmp = new PromelaInline(comments[j]); - if (tmp->type == PromelaInline::PROMELA_NIL) { - delete tmp; - continue; - } - - if (predecessor != NULL) { - tmp->prevSibling = predecessor; - predecessor->nextSibling = tmp; - } - tmp->level = level; - tmp->container = Element<std::string>(levelNodes[i]); - predecessor = tmp; - inlines[levelNodes[i]].push_back(tmp); - allInlines.push_back(tmp); - } - } - - levelNodes = DOMUtils::filterChildType(Node_base::ELEMENT_NODE, levelNodes); - level++; - } -} - -void PromelaInline::dump() { -#if 0 - switch(type) { - case PROMELA_NIL: - std::cerr << "PROMELA_NIL" << std::endl; - break; - case PROMELA_CODE: - std::cerr << "PROMELA_CODE" << std::endl; - break; - case PROMELA_EVENT_SOURCE_ALL: - std::cerr << "PROMELA_EVENT_SOURCE" << std::endl; - break; - case PROMELA_INVOKER: - std::cerr << "PROMELA_INVOKER" << std::endl; - break; - case PROMELA_PROGRESS_LABEL: - std::cerr << "PROMELA_PROGRESS_LABEL" << std::endl; - break; - case PROMELA_ACCEPT_LABEL: - std::cerr << "PROMELA_ACCEPT_LABEL" << std::endl; - break; - case PROMELA_END_LABEL: - std::cerr << "PROMELA_END_LABEL" << std::endl; - break; - } -#endif -} - - -void ChartToPromela::writeIfBlock(std::ostream& stream, const Arabica::XPath::NodeSet<std::string>& condChain, int indent) { - if (condChain.size() == 0) - return; - - std::string padding; - for (size_t i = 0; i < indent; i++) { - padding += " "; - } - - bool noNext = condChain.size() == 1; - bool nextIsElse = false; - if (condChain.size() > 1) { - if (TAGNAME_CAST(condChain[1]) == "else") { - nextIsElse = true; - } - } - - Element<std::string> ifNode = Element<std::string>(condChain[0]); - - stream << padding << "if" << std::endl; - // we need to nest the elseifs to resolve promela if semantics - stream << padding << ":: (" << ADAPT_SRC(ATTR(ifNode, "cond")) << ") -> {" << std::endl; - - Arabica::DOM::Node<std::string> child; - if (TAGNAME(ifNode) == "if") { - child = ifNode.getFirstChild(); - } else { - child = ifNode.getNextSibling(); - } - while(child) { - if (child.getNodeType() == Node_base::ELEMENT_NODE) { - Arabica::DOM::Element<std::string> childElem = Arabica::DOM::Element<std::string>(child); - if (TAGNAME(childElem) == "elseif" || TAGNAME_CAST(childElem) == "else") - break; - writeExecutableContent(stream, childElem, indent + 1); - } - child = child.getNextSibling(); - } - stream << padding << "}" << std::endl; - stream << padding << ":: else -> "; - - if (nextIsElse) { - child = condChain[1].getNextSibling(); - stream << "{" << std::endl; - while(child) { - if (child.getNodeType() == Node_base::ELEMENT_NODE) { - writeExecutableContent(stream, child, indent + 1); - } - child = child.getNextSibling(); - } - stream << padding << "}" << std::endl; - - } else if (noNext) { - stream << "skip;" << std::endl; - } else { - stream << "{" << std::endl; - - Arabica::XPath::NodeSet<std::string> cdrCondChain; - for (size_t i = 1; i < condChain.size(); i++) { - cdrCondChain.push_back(condChain[i]); - } - writeIfBlock(stream, cdrCondChain, indent + 1); - stream << padding << "}" << std::endl; - } - - stream << padding << "fi;" << std::endl; - -} - - -std::string ChartToPromela::beautifyIndentation(const std::string& code, int indent) { - - std::string padding; - for (size_t i = 0; i < indent; i++) { - padding += " "; - } - - // remove topmost indentation from every line and reindent - std::stringstream beautifiedSS; - - std::string initialIndent; - bool gotIndent = false; - bool isFirstLine = true; - std::stringstream ssLine(code); - std::string line; - - while(std::getline(ssLine, line)) { - size_t firstChar = line.find_first_not_of(" \t\r\n"); - if (firstChar != std::string::npos) { - if (!gotIndent) { - initialIndent = line.substr(0, firstChar); - gotIndent = true; - } - beautifiedSS << (isFirstLine ? "" : "\n") << padding << boost::replace_first_copy(line, initialIndent, ""); - isFirstLine = false; - } - } - - return beautifiedSS.str(); -} - -void ChartToPromela::writeStrings(std::ostream& stream) { - stream << "/* string literals */" << std::endl; - std::set<std::string> literals = _analyzer->getLiterals(); - std::map<std::string, int> events = _analyzer->getEvents(); - std::map<std::string, int> origStates = _analyzer->getOrigStates(); - - for (std::set<std::string>::const_iterator litIter = literals.begin(); litIter != literals.end(); litIter++) { - if (events.find(*litIter) == events.end() && (origStates.find(*litIter) == origStates.end() || !_analyzer->usesInPredicate())) - stream << "#define " << _analyzer->macroForLiteral(*litIter) << " " << _analyzer->indexForLiteral(*litIter) << " /* " << *litIter << " */" << std::endl; - } -} - -void ChartToPromela::writeDeclarations(std::ostream& stream) { - - 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; - - if (_analyzer->usesComplexEventStruct()) { - // event is defined with the typedefs - stream << "_event_t " << _prefix << "_event; /* 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 {_event_t} /* internal queue */" << std::endl; - stream << "chan " << _prefix << "eQ = [" << _externalQueueLength + tolerance << "] of {_event_t} /* external queue */" << 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; - 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) { - stream << "chan " << _prefix << "start = [" << _machines.size() << "] of {int} /* nested machines to start at next macrostep */" << std::endl; - } - - if (_hasIndexLessLoops) - stream << "hidden int " << _prefix << "_index; /* helper for indexless foreach loops */" << std::endl; - - stream << "hidden int " << _prefix << "procid; /* the process id running this machine */" << std::endl; - stream << "bool " << _prefix << "spontaneous; /* whether to take spontaneous transitions */" << std::endl; - stream << "bool " << _prefix << "done; /* is the state machine stopped? */" << std::endl; - stream << "bool " << _prefix << "canceled; /* is the state machine canceled? */" << std::endl; - - if (_traceTransitions) - stream << "bool " << _prefix << "transitions[" << indexedTransitions.size() << "]; /* transitions in the optimal transition set */" << std::endl; - - if (_analyzer->getTypes().types.find("_ioprocessors") != _analyzer->getTypes().types.end()) { - stream << "hidden _ioprocessors_t " << _prefix << "_ioprocessors;" << std::endl; - _varInitializers.push_front("_ioprocessors.scxml.location = " + (_invokerid.size() > 0 ? _analyzer->macroForLiteral(_invokerid) : "1") + ";"); - } - - 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 */" << std::endl; - } - - if (_analyzer->usesEventField("delay")) { -#if NEW_DELAY_RESHUFFLE -#else - stream << "hidden int _lastSeqId = 0; /* sequential counter for delayed events */" << std::endl; -#endif - } - } -// if (_analyzer->usesPlatformVars()) { -// stream << "_x_t _x;" << std::endl; -// } - - if (_analyzer->usesInPredicate()) { - stream << "_x_t " << _prefix << "_x;" << std::endl; - } - - std::list<PromelaInline*> pmls = pmlInlines.getAllOfType(PromelaInline::PROMELA_EVENT_ALL_BUT | PromelaInline::PROMELA_EVENT_ONLY); - for (std::list<PromelaInline*>::iterator pmlIter = pmls.begin(); pmlIter != pmls.end(); pmlIter++) { - if ((*pmlIter)->container && LOCALNAME((*pmlIter)->container) == "invoke") { - stream << "bool " << _prefix << ATTR_CAST((*pmlIter)->container, "id") << "Running;" << std::endl; - } - } - - stream << std::endl << std::endl; - - // get all data elements - NodeSet<std::string> datas = _xpath.evaluate("//" + _nsInfo.xpathPrefix + "data", _scxml).asNodeSet(); - - // write their text content - stream << "/* data model variables" << (_prefix.size() > 0 ? " for " + _prefix : "") << " */" << std::endl; - std::set<std::string> processedIdentifiers; - - // automatic types - PromelaCodeAnalyzer::PromelaTypedef allTypes = _analyzer->getTypes(); - - for (size_t i = 0; i < datas.size(); i++) { - - Node<std::string> data = datas[i]; - if (isInEmbeddedDocument(data)) - continue; - - std::string identifier = (HAS_ATTR_CAST(data, "id") ? ATTR_CAST(data, "id") : ""); - std::string type = boost::trim_copy(HAS_ATTR_CAST(data, "type") ? ATTR_CAST(data, "type") : ""); - - _dataModelVars.insert(identifier); - if (processedIdentifiers.find(identifier) != processedIdentifiers.end()) - continue; - - processedIdentifiers.insert(identifier); - - if (boost::starts_with(type, "string")) { - type = "int" + type.substr(6, type.length() - 6); - } - - if (type.length() == 0 || type == "auto") { - if (allTypes.types.find(identifier) != allTypes.types.end()) { - type = allTypes.types[identifier].name; - } else { - LOG(ERROR) << "Automatic or no type for '" << identifier << "' but no type resolved"; - continue; - } - } - - std::string arrSize; - size_t bracketPos = type.find("["); - if (bracketPos != std::string::npos) { - arrSize = type.substr(bracketPos, type.length() - bracketPos); - type = type.substr(0, bracketPos); - } - std::string decl = type + " " + _prefix + identifier + arrSize; - stream << decl << ";" << std::endl; - - } - - - // implicit and dynamic types - std::map<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator typeIter = allTypes.types.begin(); - while(typeIter != allTypes.types.end()) { - if (typeIter->second.occurrences.find(this) == typeIter->second.occurrences.end()) { - typeIter++; - continue; - } - - if (processedIdentifiers.find(typeIter->first) != processedIdentifiers.end()) { - typeIter++; - continue; - } - - if (typeIter->first == "_event" || - typeIter->first == "_x" || - typeIter->first == "_ioprocessors" || - typeIter->first == "_SESSIONID" || - typeIter->first == "_NAME") { - typeIter++; - continue; - } - - processedIdentifiers.insert(typeIter->first); - - if (typeIter->second.types.size() == 0) { - stream << "hidden " << declForRange(_prefix + typeIter->first, typeIter->second.minValue, typeIter->second.maxValue) << ";" << std::endl; - } else { - stream << "hidden " << _prefix << typeIter->second.name << " " << typeIter->first << ";" << std::endl; - } - typeIter++; - } - - stream << std::endl; - -} - -void ChartToPromela::writeEventSources(std::ostream& stream) { -} - -void ChartToPromela::writeStartInvoker(std::ostream& stream, const Arabica::DOM::Node<std::string>& node, ChartToPromela* invoker, int indent) { - std::string padding; - for (size_t i = 0; i < indent; i++) { - padding += " "; - } - - // set from namelist - if (HAS_ATTR_CAST(node, "namelist")) { - std::list<std::string> namelist = tokenize(ATTR_CAST(node, "namelist")); - for (std::list<std::string>::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; - } - } - } - - // set from params - NodeSet<std::string> invokeParams = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "param", node); - for (size_t i = 0; i < invokeParams.size(); i++) { - std::string identifier = ATTR_CAST(invokeParams[i], "name"); - std::string expression = ATTR_CAST(invokeParams[i], "expr"); - if (invoker->_dataModelVars.find(identifier) != invoker->_dataModelVars.end()) { - stream << padding << invoker->_prefix << identifier << " = " << ADAPT_SRC(expression) << ";" << std::endl; - } - } - - stream << padding << "run " << invoker->_prefix << "run() priority 20;" << std::endl; - if (HAS_ATTR_CAST(node, "idlocation")) { - stream << padding << ADAPT_SRC(ATTR_CAST(node, "idlocation")) << " = " << _analyzer->macroForLiteral(invoker->_invokerid) << ";" << std::endl; - } - -} - -void ChartToPromela::writeFSM(std::ostream& stream) { - NodeSet<std::string> transitions; - - stream << "proctype " << (_prefix.size() == 0 ? "machine_" : _prefix) << "run() {" << std::endl; - stream << " d_step {" << std::endl; - stream << " " << _prefix << "done = false;" << std::endl; - stream << " " << _prefix << "canceled = false;" << std::endl; - stream << " " << _prefix << "spontaneous = true;" << std::endl; - stream << " " << _prefix << "procid = _pid;" << std::endl; - stream << " }" << std::endl; - // write initial transition -// transitions = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "transition", _startState); -// assert(transitions.size() == 1); - - NodeSet<std::string> scripts = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "script", _scxml, false); - if (scripts.size() > 0) { - stream << std::endl << "/* global scripts */" << std::endl; - for (size_t i = 0; i < scripts.size(); i++) { - writeExecutableContent(stream, scripts[i], 1); - } - stream << 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); - stream << std::endl; - - // every other transition - for (std::map<std::string, GlobalState*>::iterator stateIter = _activeConf.begin(); stateIter != _activeConf.end(); stateIter++) { - for (std::list<GlobalTransition*>::iterator transIter = stateIter->second->sortedOutgoing.begin(); transIter != stateIter->second->sortedOutgoing.end(); transIter++) { - // don't write invalid transition - if (!(*transIter)->isValid) { - LOG(ERROR) << "Sorted outgoing transitions contains invalid transitions - did you instruct ChartToFSM to keep those?"; - abort(); - } - - // don't write initial transition - if (_start->sortedOutgoing.front() == *transIter) - continue; - // don't write trivial or history transitions - if ((*transIter)->historyBase == NULL) // TODO! -// if ((*transIter)->hasExecutableContent && (*transIter)->historyBase == NULL) - writeTransition(stream, *transIter, 1); - } - _perfStatesProcessed++; - _perfStatesTotal++; - - DUMP_STATS(false); - } - DUMP_STATS(true); - - stream << std::endl; - stream << _prefix << "macroStep: skip;" << std::endl; - if (_allowEventInterleaving) { - stream << " /* push send events to external queue - this needs to be interleavable! */" << std::endl; - stream << " do" << std::endl; - if (_analyzer->usesEventField("delay")) { -#if NEW_DELAY_RESHUFFLE - stream << " :: len(" << _prefix << "tmpQ) != 0 -> { " << _prefix << "tmpQ?" << _prefix << "_event; " << _prefix << "eQ!" << _prefix << "_event; insertWithDelay(" << _prefix << "eQ); }" << std::endl; -#else - stream << " :: len(" << _prefix << "tmpQ) != 0 -> { " << _prefix << "tmpQ?" << _prefix << "_event; " << _prefix << "eQ!!" << _prefix << "_event }" << std::endl; -#endif - } else { - stream << " :: len(" << _prefix << "tmpQ) != 0 -> { " << _prefix << "tmpQ?" << _prefix << "_event; " << _prefix << "eQ!" << _prefix << "_event }" << std::endl; - } - stream << " :: else -> break;" << std::endl; - 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; - for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator machIter = _machines.begin(); machIter != _machines.end(); machIter++) { - 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 << 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; - } - - std::list<PromelaInline*> eventSources = pmlInlines.getAllOfType(PromelaInline::PROMELA_EVENT_ALL_BUT | - PromelaInline::PROMELA_EVENT_ONLY); - - stream << " atomic {" << std::endl; - stream << "/* pop an event */" << std::endl; - stream << " if" << std::endl; - stream << " :: len(" << _prefix << "iQ) != 0 -> " << _prefix << "iQ ? " << _prefix << "_event /* from internal queue */" << std::endl; - if (eventSources.size() > 0) { - stream << " :: len(" << _prefix << "eQ) != 0 -> " << _prefix << "eQ ? " << _prefix << "_event /* from external queue */" << std::endl; - stream << " :: else -> {" << std::endl; - stream << " /* external queue is empty -> automatically enqueue external event */" << std::endl; - stream << " if" << std::endl; - - for (std::list<PromelaInline*>::iterator esIter = eventSources.begin(); esIter != eventSources.end(); esIter++) { - PromelaEventSource es(**esIter); - - std::string condition = "true"; - - if (LOCALNAME(es.container) == "invoke") { - if (HAS_ATTR_CAST(es.container, "id")) { - condition = _prefix + ATTR_CAST(es.container, "id") + "Running"; - } else { - LOG(ERROR) << "Invoker has no id"; - } - } else if (HAS_ATTR(es.container, "id")) { - condition = _prefix + "_x.states[" + _analyzer->macroForLiteral(ATTR(es.container, "id")) + "]"; - } - stream << " :: " << condition << " -> {" << std::endl; - - if (es.type == PromelaInline::PROMELA_EVENT_ALL_BUT) { - std::string excludeEventDescs; - for (std::list<Data>::iterator evIter = es.events.array.begin(); evIter != es.events.array.end(); evIter++) { - excludeEventDescs += " " + evIter->atom; - } - - NodeSet<std::string> transitions = DOMUtils::filterChildElements("transition", es.container, true); - std::set<std::string> eventNames; - for (size_t i = 0; i < transitions.size(); i++) { - if (!HAS_ATTR_CAST(transitions[i], "event")) - continue; - if (HAS_ATTR_CAST(transitions[i], "cond") && ATTR_CAST(transitions[i], "cond").find("_event.") != std::string::npos) - continue; - std::list<std::string> events = tokenize(ATTR_CAST(transitions[i], "event")); - for (std::list<std::string>::iterator evIter = events.begin(); evIter != events.end(); evIter++) { - std::string eventName = *evIter; - if (boost::ends_with(eventName, "*")) - eventName = eventName.substr(0, eventName.size() - 1); - if (boost::ends_with(eventName, ".")) - eventName = eventName.substr(0, eventName.size() - 1); - - // is this event excluded? - if (!nameMatch(excludeEventDescs, eventName)) { - eventNames.insert(eventName); - } - } - } - - if (eventNames.size() > 0) { - stream << " if " << std::endl; - for (std::set<std::string>::iterator evIter = eventNames.begin(); evIter != eventNames.end(); evIter++) { - stream << " :: true -> { " << _prefix << "_event" << (_analyzer->usesComplexEventStruct() ? ".name" : "")<< " = " << _analyzer->macroForLiteral(*evIter) << " }" << std::endl; - } - stream << " fi " << std::endl; - } - - } else if (es.type == PromelaInline::PROMELA_EVENT_ONLY) { - if (es.events.array.size() > 0) { - stream << " if " << std::endl; - for (std::list<Data>::iterator evIter = es.events.array.begin(); evIter != es.events.array.end(); evIter++) { - stream << " :: true -> { " << std::endl; - stream << dataToAssignments(" _event", *evIter); - stream << " } " << std::endl; - } - stream << " fi " << std::endl; - } else { - stream << dataToAssignments(" _event", es.events); - } - } else { - assert(false); - } - stream << " }" << std::endl; - } - - stream << " fi" << std::endl; - stream << " }" << std::endl; - } else { - stream << " :: else -> " << _prefix << "eQ ? " << _prefix << "_event /* from external queue */" << std::endl; - } - stream << " fi;" << std::endl << std::endl; - - - stream << "/* terminate if we are stopped */" << std::endl; - stream << " if" << std::endl; - stream << " :: " << _prefix << "done -> goto " << _prefix << "terminate;" << std::endl; - if (_parent != NULL) { - stream << " :: " << _prefix << "canceled -> goto " << _prefix << "cancel;" << std::endl; - } - stream << " :: else -> skip;" << std::endl; - stream << " fi;" << std::endl << std::endl; - - { - bool finalizeFound = false; - for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator invIter = _machines.begin(); invIter != _machines.end(); invIter++) { - NodeSet<std::string> finalizes = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "finalize", invIter->first, false); - if (finalizes.size() > 0) { - finalizeFound = true; - break; - } - } - if (finalizeFound) { - stream << "/* <finalize> event */" << std::endl; - stream << " if" << std::endl; - for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator invIter = _machines.begin(); invIter != _machines.end(); invIter++) { - NodeSet<std::string> finalizes = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "finalize", invIter->first, false); - if (finalizes.size() > 0) { - stream << " :: " << _prefix << "_event.invokeid == " << _analyzer->macroForLiteral(invIter->second->_invokerid) << " -> {" << std::endl; - writeExecutableContent(stream, finalizes[0], 3); - stream << " } " << std::endl; - } - } - stream << " :: else -> skip;" << std::endl; - stream << " fi;" << std::endl << std::endl; - } - } - - for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator invIter = _machines.begin(); invIter != _machines.end(); invIter++) { - if (invIter->second == this) { - continue; - } - //std::cout << invIter->first << std::endl; - if (stringIsTrue(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; -#if NEW_DELAY_RESHUFFLE - stream << " :: else -> { " << invIter->second->_prefix << "eQ!" << _prefix << "_event" << "; insertWithDelay(" << invIter->second->_prefix << "eQ" << "); }" << std::endl; -#else - stream << " :: else -> { " << invIter->second->_prefix << "eQ!!" << _prefix << "_event" << " }" << std::endl; -#endif - stream << " fi;" << std::endl << std::endl; - - } - } - stream << std::endl; - - stream << _prefix << "microStep:" << std::endl; - stream << "/* event dispatching per state */" << std::endl; - stream << " if" << std::endl; - - writeEventDispatching(stream); - - stream << "/* this is an error as we dispatched all valid states */" << std::endl; - stream << " :: else -> assert(false);" << std::endl; - stream << " fi;" << std::endl; - stream << std::endl; - stream << _prefix << "terminate: skip;" << std::endl; - - if (_parent != NULL) { - stream << " {" << std::endl; - stream << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), " "); - stream << " tmpE.name = " << _analyzer->macroForLiteral("done.invoke." + _invokerid) << ";" << std::endl; - if (_invokerid.length() > 0) { - stream << " tmpE.invokeid = " << _analyzer->macroForLiteral(_invokerid) << ";" << std::endl; - } - if (_analyzer->usesEventField("delay")) { -#if NEW_DELAY_RESHUFFLE - stream << " " << _parent->_prefix << "eQ!tmpE;" << std::endl; - stream << " insertWithDelay(" << _parent->_prefix << "eQ);" << std::endl; - -#else - stream << " _lastSeqId = _lastSeqId + 1;" << std::endl; - stream << " tmpE.seqNr = _lastSeqId;" << std::endl; - stream << " " << _parent->_prefix << "eQ!!tmpE;" << std::endl; -#endif - } else { - stream << " " << _parent->_prefix << "eQ!tmpE;" << std::endl; - } - stream << " }" << std::endl; - stream << _prefix << "cancel: skip;" << std::endl; - if (_analyzer->usesEventField("delay")) - stream << " removePendingEventsForInvoker(" << _analyzer->macroForLiteral(this->_invokerid) << ")" << std::endl; - } - - stream << " }" << std::endl; - stream << "}" << std::endl; -} - -void ChartToPromela::writeRescheduleProcess(std::ostream& stream, int indent) { - std::string padding; - for (size_t i = 0; i < indent; i++) { - padding += " "; - } - - 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 << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), " "); - - 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?<tmpE>;" << std::endl; - stream << padding << " if" << std::endl; - stream << padding << " :: smallestDelay == tmpE.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?<tmpE>;" << std::endl; - stream << padding << " if" << std::endl; - stream << padding << " :: smallestDelay == tmpE.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 (size_t i = 0; i < indent; i++) { - padding += " "; - } - - stream << padding << "inline determineSmallestDelay(smallestDelay, queue) {" << std::endl; -// stream << padding << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), " "); - stream << padding << " if" << std::endl; - stream << padding << " :: len(queue) > 0 -> {" << std::endl; - stream << padding << " queue?<tmpE>;" << std::endl; - stream << padding << " if" << std::endl; - stream << padding << " :: (tmpE.delay < smallestDelay) -> { smallestDelay = tmpE.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::writeInsertWithDelay(std::ostream& stream, int indent) { - std::string padding; - for (size_t i = 0; i < indent; i++) { - padding += " "; - } - - uint32_t maxExternalQueueLength = 1; - std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator machineIter = _machinesAll->begin(); - while(machineIter != _machinesAll->end()) { - maxExternalQueueLength = MAX(maxExternalQueueLength, machineIter->second->_externalQueueLength); - machineIter++; - } - - maxExternalQueueLength += 6; - - if (maxExternalQueueLength <= 1) { - stream << padding << "/* noop for external queues with length <= 1 */" << std::endl; - stream << padding << "inline insertWithDelay(queue) {}" << std::endl; - } - - stream << padding << "hidden _event_t _iwdQ[" << maxExternalQueueLength - 1 << "];" << std::endl; - stream << padding << "hidden int _iwdQLength = 0;" << std::endl; - stream << padding << "hidden int _iwdIdx1 = 0;" << std::endl; - stream << padding << "hidden int _iwdIdx2 = 0;" << std::endl; - stream << padding << "hidden _event_t _iwdTmpE;" << std::endl; - stream << padding << "hidden _event_t _iwdLastE;" << std::endl; - stream << padding << "bool _iwdInserted = false;" << std::endl; - stream << padding << "" << std::endl; - stream << padding << "/* last event in given queue is potentially at wrong position */" << std::endl; - stream << padding << "inline insertWithDelay(queue) {" << std::endl; - stream << padding << " d_step {" << std::endl; - stream << padding << "" << std::endl; - stream << padding << " /* only process for non-trivial queues */" << std::endl; - stream << padding << " if" << std::endl; - stream << padding << " :: len(queue) > 1 -> {" << std::endl; - stream << padding << "" << std::endl; - stream << padding << " /* move all events but last over and remember the last one */" << std::endl; - stream << padding << " _iwdIdx1 = 0;" << std::endl; - stream << padding << " _iwdQLength = len(queue) - 1;" << std::endl; - stream << padding << "" << std::endl; - stream << padding << " do" << std::endl; - stream << padding << " :: _iwdIdx1 < _iwdQLength -> {" << std::endl; - stream << padding << " queue?_iwdTmpE;" << std::endl; - stream << padding << " _iwdQ[_iwdIdx1].name = _iwdTmpE.name;" << std::endl; - - stream << _analyzer->getTypeAssignment("_iwdQ[_iwdIdx1]", "_iwdTmpE", _analyzer->getType("_event"), padding + " "); - - stream << padding << " _iwdIdx1++;" << std::endl; - stream << padding << " }" << std::endl; - stream << padding << " :: else -> break;" << std::endl; - stream << padding << " od" << std::endl; - stream << padding << "" << std::endl; - stream << padding << " queue?_iwdLastE;" << std::endl; - stream << padding << "" << std::endl; - stream << padding << " /* _iwdQ now contains all but last item in _iwdLastE */" << std::endl; - stream << padding << " assert(len(queue) == 0);" << std::endl; - stream << padding << "" << std::endl; - stream << padding << " /* reinsert into queue and place _iwdLastE correctly */" << std::endl; - stream << padding << " _iwdInserted = false;" << std::endl; - stream << padding << " _iwdIdx2 = 0;" << std::endl; - stream << padding << "" << std::endl; - stream << padding << " do" << std::endl; - stream << padding << " :: _iwdIdx2 < _iwdIdx1 -> {" << std::endl; - stream << padding << " _iwdTmpE.name = _iwdQ[_iwdIdx2].name;" << std::endl; - - stream << _analyzer->getTypeAssignment("_iwdTmpE", "_iwdQ[_iwdIdx2]", _analyzer->getType("_event"), padding + " "); - - stream << padding << "" << std::endl; - stream << padding << " if" << std::endl; - stream << padding << " :: _iwdTmpE.delay > _iwdLastE.delay -> {" << std::endl; - stream << padding << " queue!_iwdLastE;" << std::endl; - stream << padding << " _iwdInserted = true;" << std::endl; - stream << padding << " }" << std::endl; - stream << padding << " :: else -> skip" << std::endl; - stream << padding << " fi;" << std::endl; - stream << padding << "" << std::endl; - stream << padding << " queue!_iwdTmpE;" << std::endl; - stream << padding << " _iwdIdx2++;" << std::endl; - stream << padding << " }" << std::endl; - stream << padding << " :: else -> break;" << std::endl; - stream << padding << " od" << std::endl; - stream << padding << "" << std::endl; - stream << padding << " if" << std::endl; - stream << padding << " :: !_iwdInserted -> queue!_iwdLastE;" << std::endl; - stream << padding << " :: else -> skip;" << std::endl; - stream << padding << " fi;" << std::endl; - stream << padding << "" << std::endl; - stream << padding << " }" << std::endl; - stream << padding << " :: else -> skip;" << std::endl; - stream << padding << " fi;" << std::endl; - stream << padding << " }" << std::endl; - stream << padding << "}" << std::endl; -} - -void ChartToPromela::writeAdvanceTime(std::ostream& stream, int indent) { - std::string padding; - for (size_t i = 0; i < indent; i++) { - padding += " "; - } - - stream << padding << "inline advanceTime(increment, queue) {" << std::endl; - stream << padding << " tmpIndex = 0;" << std::endl; - stream << padding << " do" << std::endl; - stream << padding << " :: tmpIndex < len(queue) -> {" << std::endl; - stream << padding << " queue?tmpE;" << std::endl; - stream << padding << " if" << std::endl; - stream << padding << " :: tmpE.delay >= increment -> tmpE.delay = tmpE.delay - increment;" << std::endl; - stream << padding << " :: else -> skip;" << std::endl; - stream << padding << " fi" << std::endl; - stream << padding << " queue!tmpE;" << 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<std::string> queues; - queues.push_back("eQ"); - if (_allowEventInterleaving) - queues.push_back("tmpQ"); - - stream << "inline removePendingEventsForInvoker(invokeIdentifier) {" << std::endl; - for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator queueIter = _machinesAll->begin(); queueIter != _machinesAll->end(); queueIter++) { - for (std::list<std::string>::iterator qIter = queues.begin(); qIter != queues.end(); qIter++) { - stream << " removePendingEventsForInvokerOnQueue(invokeIdentifier, " << queueIter->second->_prefix << *qIter << ");" << std::endl; - } - } - stream << "}" << std::endl; - stream << std::endl; - - stream << "inline removePendingEventsForInvokerOnQueue(invokeIdentifier, queue) {" << std::endl; - stream << " tmpIndex = 0;" << std::endl; -// stream << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), " "); - stream << " do" << std::endl; - stream << " :: tmpIndex < len(queue) -> {" << std::endl; - stream << " queue?tmpE;" << std::endl; - stream << " if" << std::endl; - stream << " :: tmpE.delay == 0 || tmpE.invokeid != invokeIdentifier -> queue!tmpE;" << 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<std::string> queues; - queues.push_back("eQ"); - if (_allowEventInterleaving) - queues.push_back("tmpQ"); - - stream << "inline cancelSendId(sendIdentifier, invokerIdentifier) {" << std::endl; - for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator queueIter = _machinesAll->begin(); queueIter != _machinesAll->end(); queueIter++) { - for (std::list<std::string>::iterator qIter = queues.begin(); qIter != queues.end(); qIter++) { - stream << " cancelSendIdOnQueue(sendIdentifier, " << queueIter->second->_prefix << *qIter << ", invokerIdentifier);" << std::endl; - } - } - stream << "}" << std::endl; - stream << std::endl; - - - stream << "inline cancelSendIdOnQueue(sendIdentifier, queue, invokerIdentifier) {" << std::endl; - stream << " tmpIndex = 0;" << std::endl; -// stream << _analyzer->getTypeReset("tmpE", _analyzer->getType("_event"), " "); - stream << " do" << std::endl; - stream << " :: tmpIndex < len(queue) -> {" << std::endl; - stream << " queue?tmpE;" << std::endl; - stream << " if" << std::endl; - stream << " :: tmpE.invokeid != invokerIdentifier || tmpE.sendid != sendIdentifier || tmpE.delay == 0 -> queue!tmpE;" << 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 (size_t i = 0; i < indent; i++) { - padding += " "; - } - - stream << padding << "inline scheduleMachines() {" << std::endl; - std::list<std::string> 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<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator queueIter = _machinesAll->begin(); queueIter != _machinesAll->end(); queueIter++) { - for (std::list<std::string>::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<Arabica::DOM::Node<std::string>, 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<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator queueIter = _machinesAll->begin(); queueIter != _machinesAll->end(); queueIter++) { - for (std::list<std::string>::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<std::string, GlobalState*>::iterator stateIter = _activeConf.begin(); stateIter != _activeConf.end(); stateIter++) { - - const std::string& stateId = stateIter->first; - const GlobalState* state = stateIter->second; - - stream << std::endl << "/* ### current state "; - FlatStateIdentifier flatActiveSource(stateId); - PRETTY_PRINT_LIST(stream, flatActiveSource.getActive()); - stream << " ######################## */" << std::endl; - - stream << " :: (" << _prefix << "s == s" << state->activeIndex << ") -> {" << std::endl; - - writeDispatchingBlock(stream, state->sortedOutgoing, 3); - stream << " }" << std::endl; - } -} - -void ChartToPromela::writeDispatchingBlock(std::ostream& stream, std::list<GlobalTransition*> transitions, int indent) { - std::string padding; - for (size_t i = 0; i < indent; i++) { - padding += " "; - } - - if (transitions.size() == 0) { - stream << "/* no transition applicable */" << std::endl; - stream << padding << _prefix << "spontaneous = false;" << std::endl; - stream << padding << "goto " << _prefix << "macroStep;" << std::endl; - return; - } - - - GlobalTransition* currTrans = transitions.front(); - transitions.pop_front(); - - stream << padding << "if" << std::endl; - - if (currTrans->condition.size() > 0) { - stream << padding << ":: (("; - } else { - stream << padding << ":: ("; - } - - if (currTrans->isEventless) { - stream << _prefix << "spontaneous"; - } else { - std::string eventDescs = currTrans->eventDesc; - - std::list<std::string> eventNames = tokenize(eventDescs); - std::set<std::string> eventPrefixes; - std::list<std::string>::iterator eventNameIter = eventNames.begin(); - while(eventNameIter != eventNames.end()) { - std::string eventDesc = *eventNameIter; - if (boost::ends_with(eventDesc, "*")) - eventDesc = eventDesc.substr(0, eventDesc.size() - 1); - if (boost::ends_with(eventDesc, ".")) - eventDesc = eventDesc.substr(0, eventDesc.size() - 1); - if (eventDesc.length() > 0) { - std::set<std::string> tmp = _analyzer->getEventsWithPrefix(*eventNameIter); - eventPrefixes.insert(tmp.begin(), tmp.end()); - } - eventNameIter++; - } - - if (eventPrefixes.size() > 0) { - stream << "!" << _prefix << "spontaneous"; - } else { - stream << "!" << _prefix << "spontaneous"; - } - - if (eventPrefixes.size() > 0) - stream << " &&"; - - if (eventPrefixes.size() > 1) - stream << " ("; - - std::string seperator; - std::set<std::string>::iterator eventIter = eventPrefixes.begin(); - while(eventIter != eventPrefixes.end()) { - if (_analyzer->usesComplexEventStruct()) { - stream << seperator << " " << _prefix << "_event.name == " << _analyzer->macroForLiteral(*eventIter); - } else { - stream << seperator << " " << _prefix << "_event == " << _analyzer->macroForLiteral(*eventIter); - } - seperator = " || "; - eventIter++; - } - - if (eventPrefixes.size() > 1) - stream << ")"; - - } - - stream << ")"; - if (currTrans->condition.size() > 0) { - stream << " && (" + ADAPT_SRC(currTrans->condition) + "))"; - } - if (currTrans->hasExecutableContent || currTrans->historyTrans.size() > 0) { - stream << " -> { " << std::endl; - if (!envVarIsTrue("USCXML_ANNOTATE_NOCOMMENT")) { - stream << "/* transition to "; - FlatStateIdentifier flatActiveSource(currTrans->activeDestination); - PRETTY_PRINT_LIST(stream, flatActiveSource.getActive()); - stream << " */" << std::endl; - } - - if (_traceTransitions) { - for (std::set<int>::iterator transRefIter = currTrans->transitionRefs.begin(); transRefIter != currTrans->transitionRefs.end(); transRefIter++) { - stream << padding << " " << _prefix << "transitions[" << *transRefIter << "] = true; " << std::endl; - } - } - - stream << padding << " goto " << _prefix << "t" << currTrans->index << ";" << std::endl; - stream << padding << "}" << std::endl; - - } else { - - stream << " -> {" << std::endl; - GlobalState* newState = _activeConf[currTrans->activeDestination]; - assert(newState != NULL); - - if (!envVarIsTrue("USCXML_ANNOTATE_NOCOMMENT")) { - stream << "/* new state "; - FlatStateIdentifier flatActiveDest(currTrans->activeDestination); - PRETTY_PRINT_LIST(stream, flatActiveDest.getActive()); - stream << " */" << std::endl; - } - stream << padding << " " << _prefix << "s = s" << newState->activeIndex << ";" << std::endl; - - TRANSITION_TRACE(currTrans, false); - writeTransitionClosure(stream, currTrans, newState, indent + 1); - stream << padding << "}" << std::endl; - } - - stream << padding << ":: else -> {" << std::endl; - - writeDispatchingBlock(stream, transitions, indent + 1); - - stream << padding << "}" << std::endl; - stream << padding << "fi;" << std::endl; -} - -void ChartToPromela::writeMain(std::ostream& stream) { - stream << std::endl; - stream << "init {" << std::endl; - if (_varInitializers.size() > 0) { - stream << "/* initialize data model variables */" << std::endl; - std::list<std::string>::iterator initIter = _varInitializers.begin(); - while(initIter != _varInitializers.end()) { - stream << ADAPT_SRC(beautifyIndentation(*initIter, 1)) << std::endl; - initIter++; - } - stream << std::endl; - } - - stream << " run " << (_prefix.size() == 0 ? "machine_" : _prefix) << "run() priority 10;" << std::endl; - stream << "}" << std::endl; - -} - - -void ChartToPromela::initNodes() { - // some things we share with our invokers - if (_analyzer == NULL) - _analyzer = new PromelaCodeAnalyzer(); - - if (_machinesAll == NULL) { - _machinesAll = new std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>(); - (*_machinesAll)[_scxml] = this; - } - - if (_machinesAllPerId == NULL) - _machinesAllPerId = new std::map<std::string, Arabica::DOM::Node<std::string> >(); - - if (_parentTopMost == NULL) - _parentTopMost = this; - - _internalQueueLength = getMinInternalQueueLength(MSG_QUEUE_LENGTH); - _externalQueueLength = getMinExternalQueueLength(MSG_QUEUE_LENGTH); - - // get all states - NodeSet<std::string> states = getAllStates(); - for (size_t i = 0; i < states.size(); i++) { - if (InterpreterImpl::isInEmbeddedDocument(states[i])) - continue; - Element<std::string> stateElem(states[i]); - _analyzer->addOrigState(ATTR(stateElem, "id")); - if (isCompound(stateElem) || isParallel(stateElem)) { - _analyzer->addEvent("done.state." + ATTR(stateElem, "id")); - } - } - - { - // shorten UUID ids at invokers for readability - NodeSet<std::string> invokes = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true); - invokes.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "uninvoke", _scxml, true)); - - // make sure all invokers have an id! - for (size_t i = 0; i < invokes.size(); i++) { - if (!HAS_ATTR_CAST(invokes[i], "id")) { - Element<std::string> invokeElem(invokes[i]); - invokeElem.setAttribute("id", "INV_" + UUID::getUUID().substr(0,5)); - } else if (HAS_ATTR_CAST(invokes[i], "id") && UUID::isUUID(ATTR_CAST(invokes[i], "id"))) { - // shorten UUIDs - Element<std::string> invokeElem(invokes[i]); - invokeElem.setAttribute("id", "INV_" + ATTR_CAST(invokes[i], "id").substr(0,5)); - } - } - - } - - // are there nestes SCXML invokers? - { - NodeSet<std::string> invokes = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true); - for (size_t i = 0; i < invokes.size(); i++) { - if (!HAS_ATTR_CAST(invokes[i], "type") || - ATTR_CAST(invokes[i], "type") == "scxml" || - ATTR_CAST(invokes[i], "type") == "http://www.w3.org/TR/scxml/#SCXMLEventProcessor" || - ATTR_CAST(invokes[i], "type") == "http://www.w3.org/TR/scxml/") { - assert(HAS_ATTR_CAST(invokes[i], "id")); - Element<std::string>(invokes[i]).setAttribute("name", ATTR_CAST(invokes[i], "id")); - - _prefix = "MAIN_"; - Interpreter nested; - if (HAS_ATTR_CAST(invokes[i], "src")) { - URL absUrl(ATTR_CAST(invokes[i], "src")); - absUrl.toAbsolute(_baseURL[_scxml]); - nested = Interpreter::fromURL(absUrl); - - } else { - NodeSet<std::string> nestedContent = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "content", invokes[i]); - assert(nestedContent.size() == 1); - NodeSet<std::string> nestedRoot = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "scxml", nestedContent[0]); - assert(nestedRoot.size() == 1); - - DOMImplementation<std::string> domFactory = Arabica::SimpleDOM::DOMImplementation<std::string>::getDOMImplementation(); - Document<std::string> nestedDoc = domFactory.createDocument(_scxml.getOwnerDocument().getNamespaceURI(), "", 0); - Node<std::string> importRoot = nestedDoc.importNode(nestedRoot[0], true); - nestedDoc.appendChild(importRoot); - - nested = Interpreter::fromDOM(nestedDoc, _nsInfo, _sourceURL); - } - -// std::cout << invokes[i] << std::endl; - - // we found machines but have no prefix - if (_prefix.length() == 0) - _prefix = "MAIN_"; - - _machines[invokes[i]] = new ChartToPromela(nested); - _machines[invokes[i]]->_analyzer = _analyzer; - _machines[invokes[i]]->_parent = this; - _machines[invokes[i]]->_parentTopMost = _parentTopMost; - _machines[invokes[i]]->_machinesAll = _machinesAll; - (*_machinesAll)[invokes[i]] = _machines[invokes[i]]; - - _machines[invokes[i]]->_invokerid = ATTR_CAST(invokes[i], "id"); - _machines[invokes[i]]->_prefix = ATTR_CAST(invokes[i], "id") + "_"; - - _analyzer->addLiteral(_machines[invokes[i]]->_invokerid); - _analyzer->addEvent("done.invoke." + _machines[invokes[i]]->_invokerid); - - _machinesPerId[ATTR_CAST(invokes[i], "id")] = invokes[i]; - (*_machinesAllPerId)[ATTR_CAST(invokes[i], "id")] = invokes[i]; - } - } - } - - if (_machines.size() > 0) { - _analyzer->addCode("_event.invokeid", this); - } - - // gather all potential members per history - std::map<std::string, Arabica::DOM::Element<std::string> >::iterator histIter = _historyTargets.begin(); - while(histIter != _historyTargets.end()) { - NodeSet<std::string> histStatesMembers; - bool isDeep = (HAS_ATTR_CAST(histIter->second, "type") && ATTR_CAST(histIter->second, "type") == "deep"); - histStatesMembers.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "state", histIter->second.getParentNode(), isDeep)); - histStatesMembers.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "parallel", histIter->second.getParentNode(), isDeep)); - histStatesMembers.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "final", histIter->second.getParentNode(), isDeep)); - - for (size_t i = 0; i < histStatesMembers.size(); i++) { - _historyMembers[histIter->first].insert(std::make_pair(ATTR_CAST(histStatesMembers[i], "id"), i)); - } - histIter++; - } - - // initialize event trie with all events that might occur - NodeSet<std::string> internalEventNames; - internalEventNames.push_back(_xpath.evaluate("//" + _nsInfo.xpathPrefix + "transition", _scxml).asNodeSet()); - internalEventNames.push_back(_xpath.evaluate("//" + _nsInfo.xpathPrefix + "raise", _scxml).asNodeSet()); - internalEventNames.push_back(_xpath.evaluate("//" + _nsInfo.xpathPrefix + "send", _scxml).asNodeSet()); - - for (size_t i = 0; i < internalEventNames.size(); i++) { - if (HAS_ATTR_CAST(internalEventNames[i], "event")) { - std::string eventNames = ATTR_CAST(internalEventNames[i], "event"); - std::list<std::string> events = tokenize(eventNames); - for (std::list<std::string>::iterator eventIter = events.begin(); - eventIter != events.end(); eventIter++) { - std::string eventName = *eventIter; - if (boost::ends_with(eventName, "*")) - eventName = eventName.substr(0, eventName.size() - 1); - if (boost::ends_with(eventName, ".")) - eventName = eventName.substr(0, eventName.size() - 1); - if (eventName.size() > 0) - _analyzer->addEvent(eventName); - } - } - } - -// _analyzer->addCode("bumpDownArrow = 1; _event.foo = 3; forgetSelectedServer = 1;", this); -// exit(0); - - // transform data / assign json into PROMELA statements - { - NodeSet<std::string> asgn; - asgn.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "data", _scxml, true)); - asgn.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "assign", _scxml, true)); - - for (size_t i = 0; i < asgn.size(); i++) { - if (isInEmbeddedDocument(asgn[i])) - continue; - - Element<std::string> asgnElem(asgn[i]); - - std::string key; - if (HAS_ATTR(asgnElem, "id")) { - key = ATTR(asgnElem, "id"); - } else if (HAS_ATTR(asgnElem, "location")) { - key = ATTR(asgnElem, "location"); - } - - if (key.length() == 0) - continue; - - std::string value; - if (HAS_ATTR(asgnElem, "expr")) { - value = ATTR(asgnElem, "expr"); - } else if (HAS_ATTR(asgnElem, "src")) { - URL absUrl(ATTR_CAST(asgnElem, "src")); - absUrl.toAbsolute(_baseURL[_scxml]); - value = absUrl.getInContent(); - } else { - NodeSet<std::string> textChilds = DOMUtils::filterChildType(Node_base::TEXT_NODE, asgnElem); - if (textChilds.size() > 0) { - for (size_t j = 0; j < textChilds.size(); j++) { - value += textChilds[j].getNodeValue(); - } - } - } - - boost::trim(value); - if (value.size() == 0) - continue; - - // remove all children, we will replae by suitable promela statements - while(asgnElem.hasChildNodes()) - asgnElem.removeChild(asgnElem.getFirstChild()); - - std::string newValue; - Data json = Data::fromJSON(value); - if (!json.empty()) { - newValue = dataToAssignments(key, json); - } else { - newValue = key + " = " + value + ";"; - } - newValue = sanitizeCode(newValue); - _analyzer->addCode(newValue, this); - - if (asgnElem.getLocalName() == "data") - _varInitializers.push_back(newValue); - Text<std::string> newText = _document.createTextNode(newValue); - asgnElem.insertBefore(newText, Node<std::string>()); - } - } - - // do we need sendid / invokeid? - { - NodeSet<std::string> invokes = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true); - NodeSet<std::string> sends = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "send", _scxml, true); - NodeSet<std::string> cancels = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "cancel", _scxml, true); - - if (cancels.size() > 0) { - _analyzer->addCode("_event.invokeid", this); - } - - for (size_t i = 0; i < sends.size(); i++) { - if (HAS_ATTR_CAST(sends[i], "idlocation")) { - _analyzer->addCode("_event.sendid", this); - } - if (HAS_ATTR_CAST(sends[i], "id")) { - _analyzer->addLiteral(ATTR_CAST(sends[i], "id")); - _analyzer->addCode("_event.sendid", this); - } - } - - // do we need delays? - for (size_t i = 0; i < sends.size(); i++) { - if (HAS_ATTR_CAST(sends[i], "delay") || HAS_ATTR_CAST(sends[i], "delayexpr")) { - _analyzer->addCode("_event.delay", this); -#if NEW_DELAY_RESHUFFLE -#else - _analyzer->addCode("_event.seqNr", this); -#endif - } - } - } - - { - // string literals for raise / send content - NodeSet<std::string> withContent; - withContent.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "send", _scxml, true)); - withContent.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "raise", _scxml, true)); - - for (size_t i = 0; i < withContent.size(); i++) { - NodeSet<std::string> content = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "content", withContent[i], true); - for (size_t j = 0; j < content.size(); j++) { - Element<std::string> contentElem(content[j]); - std::string content = spaceNormalize(contentElem.getFirstChild().getNodeValue()); - if (!isNumeric(content.c_str(), 10)) - _analyzer->addLiteral(content); - } - } - } - - { - // gather all inline promela comments - pmlInlines = PromelaInlines(_scxml); - if (pmlInlines.getAllOfType(PromelaInline::PROMELA_EVENT_ONLY).size() > 0) - _analyzer->addCode("_x.states", this); - - // register events and string literals - for (std::list<PromelaInline*>::iterator inlIter = pmlInlines.allInlines.begin(); inlIter != pmlInlines.allInlines.end(); inlIter++) { - if ((*inlIter)->type != (PromelaInline::PROMELA_EVENT_ONLY)) - continue; - - Data json = Data::fromJSON((*inlIter)->content); - if (!json.empty()) { - std::list<std::string> eventNames = PromelaInlines::getEventNames(json); - for (std::list<std::string>::iterator evIter = eventNames.begin(); evIter != eventNames.end(); evIter++) { - _analyzer->addEvent(*evIter); - } - - std::list<std::string> stringLiterals = PromelaInlines::getStringLiterals(json); - for (std::list<std::string>::iterator strIter = stringLiterals.begin(); strIter != stringLiterals.end(); strIter++) { - _analyzer->addLiteral(*strIter); - } - - if (json.array.size() > 0) { - for (size_t i = 0; i < json.array.size(); i++) { - std::string expr = dataToAssignments("_event", json.item(i)); - _analyzer->addCode(expr, this); - } - } else { - std::string expr = dataToAssignments("_event", json); - _analyzer->addCode(expr, this); - - } - - } - } - } - - // add platform variables as string literals - _analyzer->addLiteral(_prefix + "_sessionid"); - _analyzer->addLiteral(_prefix + "_name"); - - if (HAS_ATTR(_scxml, "name")) { - _analyzer->addLiteral(ATTR(_scxml, "name"), _analyzer->indexForLiteral(_prefix + "_sessionid")); - } - - NodeSet<std::string> contents = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "content", _scxml, true); - for (size_t i = 0; i < contents.size(); i++) { - Element<std::string> contentElem = Element<std::string>(contents[i]); - if (contentElem.hasChildNodes() && contentElem.getFirstChild().getNodeType() == Node_base::TEXT_NODE && contentElem.getChildNodes().getLength() == 1) { - std::string content = contentElem.getFirstChild().getNodeValue(); - _analyzer->addLiteral(spaceNormalize(content)); - } - } - - - // extract and analyze source code - std::set<std::string> allCode; - std::set<std::string> allStrings; - { - NodeSet<std::string> withCond; - withCond.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "transition", _scxml, true)); - withCond.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "if", _scxml, true)); - withCond.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "elseif", _scxml, true)); - for (size_t i = 0; i < withCond.size(); i++) { - Element<std::string> elem = Element<std::string>(withCond[i]); - if (HAS_ATTR(elem, "cond")) { - std::string code = ATTR(elem, "cond"); - code = sanitizeCode(code); - elem.setAttribute("cond", code); - allCode.insert(code); - } - } - } - { - NodeSet<std::string> withExpr; - withExpr.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "log", _scxml, true)); - withExpr.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "data", _scxml, true)); - withExpr.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "assign", _scxml, true)); - withExpr.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "content", _scxml, true)); - withExpr.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "param", _scxml, true)); - for (size_t i = 0; i < withExpr.size(); i++) { - Element<std::string> elem = Element<std::string>(withExpr[i]); - if (HAS_ATTR(elem, "expr")) { - std::string code = ATTR(elem, "expr"); - code = sanitizeCode(code); - elem.setAttribute("expr", code); - allCode.insert(code); - } - } - } - { - NodeSet<std::string> withLocation; - withLocation.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "assign", _scxml, true)); - for (size_t i = 0; i < withLocation.size(); i++) { - Element<std::string> elem = Element<std::string>(withLocation[i]); - if (HAS_ATTR(elem, "location")) { - std::string code = ATTR(elem, "location"); - code = sanitizeCode(code); - elem.setAttribute("location", code); - allCode.insert(code); - } - } - } - { - NodeSet<std::string> withText; - withText.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "script", _scxml, true)); -// withText.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "data", _scxml, true)); - for (size_t i = 0; i < withText.size(); i++) { - NodeSet<std::string> texts = DOMUtils::filterChildType(Node_base::TEXT_NODE, withText[i], true); - for (size_t j = 0; j < texts.size(); j++) { - if (texts[j].getNodeValue().size() > 0) { - Text<std::string> elem = Text<std::string>(texts[j]); - std::string code = elem.getNodeValue(); - code = sanitizeCode(code); - elem.setNodeValue(code); - allCode.insert(code); - } - } - } - } - { - NodeSet<std::string> foreachs = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "foreach", _scxml, true); - for (size_t i = 0; i < foreachs.size(); i++) { - if (HAS_ATTR_CAST(foreachs[i], "index")) { - allCode.insert(ATTR_CAST(foreachs[i], "index")); - } else { - _hasIndexLessLoops = true; - } - if (HAS_ATTR_CAST(foreachs[i], "item")) { - allCode.insert(ATTR_CAST(foreachs[i], "item")); - } - } - } - for (std::set<std::string>::const_iterator codeIter = allCode.begin(); codeIter != allCode.end(); codeIter++) { - _analyzer->addCode(*codeIter, this); - } - - // add all namelist entries to the _event structure - { - NodeSet<std::string> withNamelist; - withNamelist.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "send", _scxml, true)); - withNamelist.push_back(DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true)); - for (size_t i = 0; i < withNamelist.size(); i++) { - if (HAS_ATTR_CAST(withNamelist[i], "namelist")) { - std::string namelist = ATTR_CAST(withNamelist[i], "namelist"); - std::list<std::string> names = tokenize(namelist); - for (std::list<std::string>::iterator nameIter = names.begin(); nameIter != names.end(); nameIter++) { - _analyzer->addCode("_event.data." + *nameIter + " = 0;", this); // introduce for _event_t typedef - } - } - } - } -} - -std::list<std::string> PromelaInlines::getStringLiterals(const Data& data) { - std::list<std::string> literals; - if (data.atom.size() > 0 && data.type == Data::VERBATIM) { - literals.push_back(data.atom); - } - if (data.array.size() > 0) { - for (std::list<Data>::const_iterator arrIter = data.array.begin(); arrIter != data.array.end(); arrIter++) { - std::list<std::string> nested = getStringLiterals(*arrIter); - literals.insert(literals.end(), nested.begin(), nested.end()); - } - } - if (data.compound.size() > 0) { - for (std::map<std::string, Data>::const_iterator compIter = data.compound.begin(); compIter != data.compound.end(); compIter++) { - std::list<std::string> nested = getStringLiterals(compIter->second); - literals.insert(literals.end(), nested.begin(), nested.end()); - } - } - return literals; -} - -std::list<std::string> PromelaInlines::getEventNames(const Data& data) { - std::list<std::string> eventNames; - if (data.compound.size() > 0 && data.hasKey("name")) { - eventNames.push_back(data.at("name")); - } - if (data.array.size() > 0) { - for (std::list<Data>::const_iterator arrIter = data.array.begin(); arrIter != data.array.end(); arrIter++) { - std::list<std::string> nested = getEventNames(*arrIter); - eventNames.insert(eventNames.end(), nested.begin(), nested.end()); - } - } - if (data.compound.size() > 0) { - for (std::map<std::string, Data>::const_iterator compIter = data.compound.begin(); compIter != data.compound.end(); compIter++) { - std::list<std::string> nested = getEventNames(compIter->second); - eventNames.insert(eventNames.end(), nested.begin(), nested.end()); - } - } - - return eventNames; -} - -std::string ChartToPromela::dataToAssignments(const std::string& prefix, const Data& data) { - std::stringstream retVal; - if (data.atom.size() > 0) { - if (data.type == Data::VERBATIM) { - retVal << prefix << " = " << _analyzer->macroForLiteral(data.atom) << ";" << std::endl; - } else { - retVal << prefix << " = " << data.atom << ";" << std::endl; - } - } else if (data.compound.size() > 0) { - for (std::map<std::string, Data>::const_iterator cIter = data.compound.begin(); cIter != data.compound.end(); cIter++) { - retVal << dataToAssignments(prefix + "." + cIter->first, cIter->second); - } - } else if (data.array.size() > 0) { - size_t index = 0; - for(std::list<Data>::const_iterator aIter = data.array.begin(); aIter != data.array.end(); aIter++) { - retVal << dataToAssignments(prefix + "[" + toStr(index) + "]", *aIter); - index++; - } - } - return retVal.str(); -} - -std::string ChartToPromela::sanitizeCode(const std::string& code) { - std::string replaced = code; - boost::replace_all(replaced, "\"", "'"); - boost::replace_all(replaced, "_sessionid", "_SESSIONID"); - boost::replace_all(replaced, "_name", "_NAME"); - return replaced; -} - - -void ChartToPromela::writeProgram(std::ostream& stream) { - - _traceTransitions = envVarIsTrue("USCXML_PROMELA_TRANSITION_TRACE"); - _writeTransitionPrintfs = envVarIsTrue("USCXML_PROMELA_TRANSITION_DEBUG"); - - if (!HAS_ATTR(_scxml, "datamodel") || ATTR(_scxml, "datamodel") != "promela") { - LOG(ERROR) << "Can only convert SCXML documents with \"promela\" datamodel"; - return; - } - - if (_start == NULL) { - interpret(); - } - - if (HAS_ATTR(_scxml, "binding") && ATTR(_scxml, "binding") != "early") { - LOG(ERROR) << "Can only convert for early data bindings"; - return; - } - -// std::cerr << _scxml << std::endl; - - stream << "/* " << _sourceURL.asString() << " */" << std::endl; - stream << std::endl; - - initNodes(); - - for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator nestedIter = _machines.begin(); nestedIter != _machines.end(); nestedIter++) { - if (nestedIter->second->_start == NULL) { - nestedIter->second->interpret(); - } - nestedIter->second->initNodes(); - } - - writeEvents(stream); - stream << std::endl; - writeStates(stream); - stream << std::endl; - writeStrings(stream); - stream << std::endl; - if (_analyzer->usesInPredicate()) { - writeStateMap(stream); - stream << std::endl; - } - if (_historyMembers.size() > 0) { - writeHistoryArrays(stream); - stream << std::endl; - } - writeTypeDefs(stream); - stream << std::endl; - writeDeclarations(stream); - stream << std::endl; - - for (std::map<Arabica::DOM::Node<std::string>, 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->usesComplexEventStruct()) { - stream << "hidden _event_t tmpE;" << std::endl; - } else { - stream << "hidden int tmpE;" << std::endl; - } - stream << "hidden int tmpIndex;" << std::endl; - - -#if NEW_DELAY_RESHUFFLE - if (_analyzer->usesEventField("delay")) { - writeInsertWithDelay(stream); - stream << std::endl; - } -#endif - - if (_analyzer->usesEventField("delay") && _machines.size() > 0) { - writeDetermineShortestDelay(stream); - stream << std::endl; - writeAdvanceTime(stream); - stream << std::endl; - writeRescheduleProcess(stream); - stream << std::endl; - writeScheduleMachines(stream); - stream << std::endl; - } - - { - NodeSet<std::string> cancels = DOMUtils::filterChildElements(_nsInfo.xmlNSPrefix + "cancel", _scxml, true); - if (cancels.size() > 0) { - writeCancelEvents(stream); - stream << std::endl; - } - } - { - NodeSet<std::string> invokes = DOMUtils::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; - writeFSM(stream); - stream << std::endl; - writeMain(stream); - stream << std::endl; - - for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator nestedIter = _machines.begin(); nestedIter != _machines.end(); nestedIter++) { - nestedIter->second->writeFSM(stream); - stream << std::endl; - } - - // write ltl expression for success - std::stringstream acceptingStates; - std::string seperator; - - for (std::map<std::string, GlobalState*>::iterator stateIter = _activeConf.begin(); stateIter != _activeConf.end(); stateIter++) { - FlatStateIdentifier flatId(stateIter->first); - if (std::find(flatId.getActive().begin(), flatId.getActive().end(), "pass") != flatId.getActive().end()) { - acceptingStates << seperator << _prefix << "s == s" << stateIter->second->activeIndex; - seperator = " || "; - } - } - if (acceptingStates.str().size() > 0) { - stream << "ltl { eventually (" << acceptingStates.str() << ") }" << std::endl; - } -} - -}
\ No newline at end of file |