diff options
author | Stefan Radomski <radomski@tk.informatik.tu-darmstadt.de> | 2014-04-24 08:36:14 (GMT) |
---|---|---|
committer | Stefan Radomski <radomski@tk.informatik.tu-darmstadt.de> | 2014-04-24 08:36:14 (GMT) |
commit | 6b53548ae32336db822d6e6af0e14413c82c74dd (patch) | |
tree | 8f2ecf59b1713a9c3ff8720a01ac53c5fca7aa8e /src | |
parent | b54d9c61b6c29c973168f33f683a49051f0ed3cc (diff) | |
download | uscxml-6b53548ae32336db822d6e6af0e14413c82c74dd.zip uscxml-6b53548ae32336db822d6e6af0e14413c82c74dd.tar.gz uscxml-6b53548ae32336db822d6e6af0e14413c82c74dd.tar.bz2 |
Support for custom event sources with promela
Diffstat (limited to 'src')
-rw-r--r-- | src/uscxml/transform/FSMToPromela.cpp | 397 | ||||
-rw-r--r-- | src/uscxml/transform/FSMToPromela.h | 80 |
2 files changed, 334 insertions, 143 deletions
diff --git a/src/uscxml/transform/FSMToPromela.cpp b/src/uscxml/transform/FSMToPromela.cpp index 9ae3155..d72dccb 100644 --- a/src/uscxml/transform/FSMToPromela.cpp +++ b/src/uscxml/transform/FSMToPromela.cpp @@ -42,6 +42,148 @@ void FSMToPromela::writeProgram(std::ostream& stream, FSMToPromela::FSMToPromela() : _eventTrie(".") { } +void PromelaEventSource::writeStartEventSources(std::ostream& stream, int indent) { + std::string padding; + for (int i = 0; i < indent; i++) { + padding += " "; + } + + std::list<PromelaInline>::iterator sourceIter = eventSources.inlines.begin(); + int i = 0; + while(sourceIter != eventSources.inlines.end()) { + if (sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM && sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE) { + sourceIter++; + continue; + } + std::string sourceName = name + "_"+ toStr(i); + stream << padding << "run " << sourceName << "EventSource();" << std::endl; + + i++; + sourceIter++; + } + +} + +void PromelaEventSource::writeStopEventSources(std::ostream& stream, int indent) { + std::string padding; + for (int i = 0; i < indent; i++) { + padding += " "; + } + + std::list<PromelaInline>::iterator sourceIter = eventSources.inlines.begin(); + int i = 0; + while(sourceIter != eventSources.inlines.end()) { + if (sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM && sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE) { + sourceIter++; + continue; + } + std::string sourceName = name + "_"+ toStr(i); + stream << padding << sourceName << "EventSourceDone = 1;" << std::endl; + + i++; + sourceIter++; + } + +} + +void PromelaEventSource::writeDeclarations(std::ostream& stream, int indent) { + std::string padding; + for (int i = 0; i < indent; i++) { + padding += " "; + } + + std::list<PromelaInline>::iterator sourceIter = eventSources.inlines.begin(); + int i = 0; + while(sourceIter != eventSources.inlines.end()) { + if (sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM && sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE) { + sourceIter++; + continue; + } + std::string sourceName = name + "_"+ toStr(i); + stream << "bool " << sourceName << "EventSourceDone = 0;" << std::endl; + + i++; + sourceIter++; + } +} + +void PromelaEventSource::writeEventSource(std::ostream& stream) { + + std::list<PromelaInline>::iterator sourceIter = eventSources.inlines.begin(); + int i = 0; + while(sourceIter != eventSources.inlines.end()) { + if (sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM && sourceIter->type != PromelaInline::PROMELA_EVENT_SOURCE) { + sourceIter++; + continue; + } + + std::string sourceName = name + "_"+ toStr(i); + + stream << "proctype " << sourceName << "EventSource() {" << std::endl; + stream << " " << sourceName << "EventSourceDone = 0;" << std::endl; + stream << " " << sourceName << "NewEvent:" << std::endl; + stream << " " << "if" << std::endl; + stream << " " << ":: " << sourceName << "EventSourceDone -> skip;" << std::endl; + stream << " " << ":: else { " << std::endl; + + if (sourceIter->type == PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM) { + std::string content = sourceIter->content; + + boost::replace_all(content, "#REDO#", sourceName + "NewEvent"); + boost::replace_all(content, "#DONE#", sourceName + "Done"); + + std::list<TrieNode*> eventNames = trie->getChildsWithWords(trie->getNodeWithPrefix("")); + std::list<TrieNode*>::iterator eventNameIter = eventNames.begin(); + while(eventNameIter != eventNames.end()) { + boost::replace_all(content, "#" + (*eventNameIter)->value + "#", "e" + toStr((*eventNameIter)->identifier)); + eventNameIter++; + } + + stream << FSMToPromela::beautifyIndentation(content, 2) << std::endl; + + } else { + stream << " " << " if" << std::endl; +// stream << " " << " :: 1 -> " << "goto " << sourceName << "NewEvent;" << std::endl; + + std::list<std::list<std::string> >::const_iterator seqIter = sourceIter->sequences.begin(); + while(seqIter != sourceIter->sequences.end()) { + stream << " " << ":: "; + std::list<std::string>::const_iterator evIter = seqIter->begin(); + while(evIter != seqIter->end()) { + TrieNode* node = trie->getNodeWithPrefix(*evIter); + stream << "eQ!" << node->identifier << "; "; + evIter++; + } + stream << "goto " << sourceName << "NewEvent;" << std::endl; + seqIter++; + } + + stream << " " << " fi;" << std::endl; + } + + stream << " " << "}" << std::endl; + stream << " " << "fi;" << std::endl; + stream << sourceName << "Done:" << " skip;" << std::endl; + stream << "}" << std::endl; + + i++; + sourceIter++; + } +} + +PromelaEventSource::PromelaEventSource() { + type = PROMELA_EVENT_SOURCE_INVALID; + trie = NULL; +} + +PromelaEventSource::PromelaEventSource(const PromelaInlines& sources, const Arabica::DOM::Node<std::string>& parent) { + type = PROMELA_EVENT_SOURCE_INVALID; + trie = NULL; + + eventSources = sources; + container = parent; +} + void FSMToPromela::writeEvents(std::ostream& stream) { std::list<TrieNode*> eventNames = _eventTrie.getWordsWithPrefix(""); std::list<TrieNode*>::iterator eventIter = eventNames.begin(); @@ -156,11 +298,11 @@ void FSMToPromela::writeExecutableContent(std::ostream& stream, const Arabica::D // check for special promela labels PromelaInlines promInls = getInlinePromela(getTransientContent(_states[ATTR(node, "target")]), true); - if (promInls.hasAcceptLabel) + if (promInls.acceptLabels > 0) stream << padding << "acceptLabelT" << _transitions[node] << ":" << std::endl; - if (promInls.hasEndLabel) + if (promInls.endLabels > 0) stream << padding << "endLabelT" << _transitions[node] << ":" << std::endl; - if (promInls.hasProgressLabel) + if (promInls.progressLabels > 0) stream << padding << "progressLabelT" << _transitions[node] << ":" << std::endl; stream << padding << "atomic {" << std::endl; @@ -221,8 +363,14 @@ void FSMToPromela::writeExecutableContent(std::ostream& stream, const Arabica::D } else if(TAGNAME(node) == "raise") { TrieNode* trieNode = _eventTrie.getNodeWithPrefix(ATTR(node, "event")); stream << padding << "iQ!e" << trieNode->identifier << ";" << std::endl; + } else if(TAGNAME(node) == "send") { + if (!HAS_ATTR(node, "target")) { + // this is for our external queue + TrieNode* trieNode = _eventTrie.getNodeWithPrefix(ATTR(node, "event")); + stream << padding << "tmpQ!e" << trieNode->identifier << ";" << std::endl; + } } else if(TAGNAME(node) == "invoke") { - stream << padding << "run " << ATTR(node, "invokeid") << "EventSource();" << std::endl; + _invokers[ATTR(node, "invokeid")].writeStartEventSources(stream, indent); } else if(TAGNAME(node) == "uninvoke") { stream << padding << ATTR(node, "invokeid") << "EventSourceDone" << "= 1;" << std::endl; } else { @@ -233,68 +381,96 @@ void FSMToPromela::writeExecutableContent(std::ostream& stream, const Arabica::D } -PromelaInlines FSMToPromela::getInlinePromela(const Arabica::XPath::NodeSet<std::string>& elements, bool recurse) { +PromelaInlines FSMToPromela::getInlinePromela(const std::string& content) { PromelaInlines prom; - if (elements.size() == 0) - return prom; - - Arabica::XPath::NodeSet<std::string> comments = filterChildType(Node_base::COMMENT_NODE, elements, recurse); - for (int i = 0; i < comments.size(); i++) { - std::stringstream ssLine(comments[i].getNodeValue()); - std::string line; + std::stringstream ssLine(content); + std::string line; - bool isInPromelaCode = false; - PromelaInline promInl; + bool isInPromelaCode = false; + bool isInPromelaEventSource = false; + PromelaInline promInl; - while(std::getline(ssLine, line)) { - std::string trimLine = boost::trim_copy(line); - if (line.length() == 0) - continue; - if (false) { - } else if (boost::starts_with(trimLine, "promela-progress")) { - prom.hasProgressLabel = true; - if (isInPromelaCode) { - prom.inlines.push_back(promInl); - isInPromelaCode = false; - } - promInl.type = PromelaInline::PROMELA_PROGRESS_LABEL; - promInl.content = line; - prom.inlines.push_back(promInl); - } else if (boost::starts_with(trimLine, "promela-accept")) { - prom.hasAcceptLabel = true; - if (isInPromelaCode) { - prom.inlines.push_back(promInl); - isInPromelaCode = false; - } - promInl.type = PromelaInline::PROMELA_ACCEPT_LABEL; - promInl.content = line; - prom.inlines.push_back(promInl); - } else if (boost::starts_with(trimLine, "promela-end")) { - prom.hasEndLabel = true; - if (isInPromelaCode) { - prom.inlines.push_back(promInl); - isInPromelaCode = false; - } - promInl.type = PromelaInline::PROMELA_END_LABEL; - promInl.content = line; + while(std::getline(ssLine, line)) { + std::string trimLine = boost::trim_copy(line); + if (trimLine.length() == 0) + continue; + if (boost::starts_with(trimLine, "#promela")) { + if (isInPromelaCode || isInPromelaEventSource) { prom.inlines.push_back(promInl); - } else if (boost::starts_with(trimLine, "promela-inline")) { - prom.hasCode = true; - isInPromelaCode = true; - promInl.type = PromelaInline::PROMELA_CODE; - } else if (isInPromelaCode) { - promInl.content += line; + isInPromelaCode = false; + isInPromelaEventSource = false; } + promInl = PromelaInline(); } - // inline code ends with comment - if (isInPromelaCode) { + + if (false) { + } else if (boost::starts_with(trimLine, "#promela-progress")) { + prom.progressLabels++; + promInl.type = PromelaInline::PROMELA_PROGRESS_LABEL; + promInl.content = line; + prom.inlines.push_back(promInl); + } else if (boost::starts_with(trimLine, "#promela-accept")) { + prom.acceptLabels++; + promInl.type = PromelaInline::PROMELA_ACCEPT_LABEL; + promInl.content = line; prom.inlines.push_back(promInl); + } else if (boost::starts_with(trimLine, "#promela-end")) { + prom.endLabels++; + promInl.type = PromelaInline::PROMELA_END_LABEL; + promInl.content = line; + prom.inlines.push_back(promInl); + } else if (boost::starts_with(trimLine, "#promela-inline")) { + prom.codes++; + isInPromelaCode = true; + promInl.type = PromelaInline::PROMELA_CODE; + } else if (boost::starts_with(trimLine, "#promela-event-source-custom")) { + prom.customEventSources++; + isInPromelaCode = true; + promInl.type = PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM; + } else if (boost::starts_with(trimLine, "#promela-event-source")) { + prom.eventSources++; + isInPromelaEventSource = true; + promInl.type = PromelaInline::PROMELA_EVENT_SOURCE; + } else if (isInPromelaCode) { + promInl.content += line; + promInl.content += "\n"; + } else if (isInPromelaEventSource) { + std::list<std::string> seq; + std::stringstream ssToken(trimLine); + std::string token; + while(std::getline(ssToken, token, ' ')) { + if (token.length() == 0) + continue; + seq.push_back(token); + } + promInl.sequences.push_back(seq); } } + // inline code ends with comment + if (isInPromelaCode || isInPromelaEventSource) { + prom.inlines.push_back(promInl); + } + return prom; } +PromelaInlines FSMToPromela::getInlinePromela(const Arabica::DOM::Node<std::string>& node) { + if (node.getNodeType() != Node_base::COMMENT_NODE) + return getInlinePromela(std::string()); + return getInlinePromela(node.getNodeValue()); +} + +PromelaInlines FSMToPromela::getInlinePromela(const Arabica::XPath::NodeSet<std::string>& elements, bool recurse) { + PromelaInlines allPromInls; + + Arabica::XPath::NodeSet<std::string> comments = filterChildType(Node_base::COMMENT_NODE, elements, recurse); + for (int i = 0; i < comments.size(); i++) { + allPromInls.merge(getInlinePromela(comments[i])); + } + return allPromInls; +} + void FSMToPromela::writeIfBlock(std::ostream& stream, const Arabica::XPath::NodeSet<std::string>& condChain, int indent) { if (condChain.size() == 0) return; @@ -410,63 +586,41 @@ void FSMToPromela::writeDeclarations(std::ostream& stream) { stream << "// global variables" << std::endl; stream << "int e; /* current event */" << std::endl; stream << "int s; /* current state */" << std::endl; - stream << "chan iQ = [100] of {int} /* internal queue */" << std::endl; - stream << "chan eQ = [100] of {int} /* external queue */" << std::endl; + stream << "chan iQ = [100] of {int} /* internal queue */" << std::endl; + stream << "chan eQ = [100] of {int} /* external queue */" << std::endl; + stream << "chan tmpQ = [100] of {int} /* temporary queue for external events in transitions */" << std::endl; + stream << "int tmpQItem;" << std::endl; stream << std::endl; stream << "// event sources" << std::endl; - if (_globalEventSource) - stream << "bool globalEventSourceDone;" << std::endl; + + if (_globalEventSource) { + _globalEventSource.writeDeclarations(stream); + } std::map<std::string, PromelaEventSource>::iterator invIter = _invokers.begin(); while(invIter != _invokers.end()) { - stream << "bool " << invIter->first << "EventSourceDone;" << std::endl; - stream << std::endl; + invIter->second.writeDeclarations(stream); invIter++; } } void FSMToPromela::writeEventSources(std::ostream& stream) { - if (_globalEventSource) - writeEventSource(stream, "global", _globalEventSource); + std::list<PromelaInline>::iterator inlineIter; + + if (_globalEventSource) { + _globalEventSource.writeEventSource(stream); + } std::map<std::string, PromelaEventSource>::iterator invIter = _invokers.begin(); while(invIter != _invokers.end()) { - writeEventSource(stream, invIter->first, invIter->second); + invIter->second.writeEventSource(stream); invIter++; } } -void FSMToPromela::writeEventSource(std::ostream& stream, const std::string& name, const PromelaEventSource& source) { - stream << "proctype " << name << "EventSource() {" << std::endl; - stream << " " << name << "EventSourceDone = 0;" << std::endl; - stream << " " << name << "NewEvent:" << std::endl; - stream << " " << "if" << std::endl; - stream << " " << ":: " << name << "EventSourceDone -> skip;" << std::endl; - stream << " " << ":: else { " << std::endl; - stream << " " << " if" << std::endl; - stream << " " << " :: 1 -> " << "goto " << name << "NewEvent;" << std::endl; - - std::list<std::list<std::string> >::const_iterator seqIter = source.sequences.begin(); - while(seqIter != source.sequences.end()) { - stream << " " << ":: "; - std::list<std::string>::const_iterator evIter = seqIter->begin(); - while(evIter != seqIter->end()) { - TrieNode* node = _eventTrie.getNodeWithPrefix(*evIter); - stream << "eQ!" << node->identifier << "; "; - evIter++; - } - stream << "goto " << name << "NewEvent;" << std::endl; - seqIter++; - } - stream << " " << " fi" << std::endl; - stream << " " << "}" << std::endl; - stream << " " << "fi" << std::endl; - stream << "}" << std::endl; -} - void FSMToPromela::writeFSM(std::ostream& stream) { NodeSet<std::string> transitions; @@ -488,7 +642,14 @@ void FSMToPromela::writeFSM(std::ostream& stream) { } stream << std::endl; - stream << "nextStep: /* pop an event */" << std::endl; + stream << "nextStep:" << std::endl; + stream << " // push send events to external queue" << std::endl; + stream << " if" << std::endl; + stream << " :: len(tmpQ) != 0 -> { tmpQ?e; eQ!e }" << std::endl; + stream << " :: else -> skip;" << std::endl; + stream << " fi;" << std::endl << std::endl; + + stream << " /* pop an event */" << std::endl; stream << " if" << std::endl; stream << " :: len(iQ) != 0 -> iQ ? e /* from internal queue */" << std::endl; stream << " :: else -> eQ ? e /* from external queue */" << std::endl; @@ -504,15 +665,14 @@ void FSMToPromela::writeFSM(std::ostream& stream) { // stop all event sources if (_globalEventSource) - stream << " globalEventSourceDone = 1;" << std::endl; + _globalEventSource.writeStopEventSources(stream, 1); std::map<std::string, PromelaEventSource>::iterator invIter = _invokers.begin(); while(invIter != _invokers.end()) { - stream << " " << invIter->first << "EventSourceDone = 1;" << std::endl; + invIter->second.writeStopEventSources(stream, 1); invIter++; } - stream << "}" << std::endl; } @@ -584,7 +744,7 @@ void FSMToPromela::writeMain(std::ostream& stream) { stream << std::endl; stream << "init {" << std::endl; if (_globalEventSource) - stream << " run globalEventSource();" << std::endl; + _globalEventSource.writeStartEventSources(stream, 1); stream << " run step();" << std::endl; stream << "}" << std::endl; @@ -626,47 +786,28 @@ void FSMToPromela::initNodes() { // external event names from comments NodeSet<std::string> promelaEventSourceComments; NodeSet<std::string> invokers = _xpath.evaluate("//" + _nsInfo.xpathPrefix + "invoke", _scxml).asNodeSet(); - promelaEventSourceComments.push_back(filterChildType(Node_base::COMMENT_NODE, invokers, true)); // comments in invoke elements + promelaEventSourceComments.push_back(filterChildType(Node_base::COMMENT_NODE, invokers, false)); // comments in invoke elements promelaEventSourceComments.push_back(filterChildType(Node_base::COMMENT_NODE, _scxml, false)); // comments in scxml element for (int i = 0; i < promelaEventSourceComments.size(); i++) { - std::string comment = promelaEventSourceComments[i].getNodeValue(); - boost::trim(comment); - if (!boost::starts_with(comment, "promela-event-source:")) - continue; - PromelaEventSource* eventSource = NULL; - if (false) { - } else if (TAGNAME(promelaEventSourceComments[i].getParentNode()) == "scxml") { - eventSource = &_globalEventSource; + PromelaInlines promInls = getInlinePromela(promelaEventSourceComments[i]); + PromelaEventSource promES(promInls, promelaEventSourceComments[i].getParentNode()); + + if (TAGNAME(promelaEventSourceComments[i].getParentNode()) == "scxml") { + promES.type = PromelaEventSource::PROMELA_EVENT_SOURCE_GLOBAL; + promES.trie = &_eventTrie; + promES.name = "global"; + _globalEventSource = promES; } else if (TAGNAME(promelaEventSourceComments[i].getParentNode()) == "invoke") { if (!HAS_ATTR(promelaEventSourceComments[i].getParentNode(), "invokeid")) { Element<std::string> invoker = Element<std::string>(promelaEventSourceComments[i].getParentNode()); invoker.setAttribute("invokeid", "invoker" + toStr(_invokers.size())); } std::string invokeId = ATTR(promelaEventSourceComments[i].getParentNode(), "invokeid"); - eventSource = &_invokers[invokeId]; - } else { - assert(false); - } - if (!eventSource) - continue; - std::stringstream ssLine(comment); - std::string line; - std::getline(ssLine, line); // consume first line - while(std::getline(ssLine, line)) { - if (line.length() == 0) - continue; - std::list<std::string> currSeq; - - std::stringstream ssToken(line); - std::string token; - while(std::getline(ssToken, token, ' ')) { - if (token.length() == 0) - continue; - currSeq.push_back(token); - _eventTrie.addWord(token); - } - eventSource->sequences.push_back(currSeq); + promES.type = PromelaEventSource::PROMELA_EVENT_SOURCE_INVOKER; + promES.trie = &_eventTrie; + promES.name = invokeId; + _invokers[invokeId] = promES; } } @@ -678,7 +819,7 @@ void FSMToPromela::initNodes() { } } -void PromelaEventSource::dump() { +void PromelaInline::dump() { std::list<std::list<std::string> >::iterator outerIter = sequences.begin(); while(outerIter != sequences.end()) { std::list<std::string>::iterator innerIter = outerIter->begin(); diff --git a/src/uscxml/transform/FSMToPromela.h b/src/uscxml/transform/FSMToPromela.h index 37c2b67..7872997 100644 --- a/src/uscxml/transform/FSMToPromela.h +++ b/src/uscxml/transform/FSMToPromela.h @@ -20,6 +20,7 @@ #ifndef FSMTOPROMELA_H_RP48RFDJ #define FSMTOPROMELA_H_RP48RFDJ +#include "uscxml/interpreter/InterpreterDraft6.h" #include "uscxml/DOMUtils.h" #include "uscxml/util/Trie.h" @@ -32,42 +33,92 @@ namespace uscxml { class PromelaInline { public: + PromelaInline() : type(PROMELA_NIL) {} + + operator bool() { + return (type != PROMELA_NIL); + } + + void dump(); + enum PromelaInlineType { + PROMELA_NIL, PROMELA_CODE, PROMELA_EVENT_SOURCE, + PROMELA_EVENT_SOURCE_CUSTOM, PROMELA_PROGRESS_LABEL, PROMELA_ACCEPT_LABEL, PROMELA_END_LABEL }; std::string content; + std::list<std::list<std::string> > sequences; + PromelaInlineType type; }; class PromelaInlines { public: - PromelaInlines() : hasProgressLabel(false), hasAcceptLabel(false), hasEndLabel(false), hasEventSource(false), hasCode(false) {} + PromelaInlines() : progressLabels(0), acceptLabels(0), endLabels(0), eventSources(0), customEventSources(0), codes(0) {} + + void merge(const PromelaInlines& other) { + inlines.insert(inlines.end(), other.inlines.begin(), other.inlines.end()); + progressLabels += other.progressLabels; + acceptLabels += other.acceptLabels; + endLabels += other.endLabels; + eventSources += other.eventSources; + customEventSources += other.customEventSources; + codes += other.codes; + } + + operator bool() { + return inlines.size() > 0; + } std::list<PromelaInline> inlines; - bool hasProgressLabel; - bool hasAcceptLabel; - bool hasEndLabel; - bool hasEventSource; - bool hasCode; + int progressLabels; + int acceptLabels; + int endLabels; + int eventSources; + int customEventSources; + int codes; }; -struct PromelaEventSource { - std::list<std::list<std::string> > sequences; - void dump(); +class PromelaEventSource { +public: + + enum PromelaEventSourceType { + PROMELA_EVENT_SOURCE_INVALID, + PROMELA_EVENT_SOURCE_INVOKER, + PROMELA_EVENT_SOURCE_GLOBAL, + }; + + PromelaEventSource(); + PromelaEventSource(const PromelaInlines& sources, const Arabica::DOM::Node<std::string>& parent); + + void writeStartEventSources(std::ostream& stream, int indent = 0); + void writeStopEventSources(std::ostream& stream, int indent = 0); + void writeDeclarations(std::ostream& stream, int indent = 0); + void writeEventSource(std::ostream& stream); + operator bool() { - return sequences.size() > 0; + return type != PROMELA_EVENT_SOURCE_INVALID; } + + std::string name; + PromelaInlines eventSources; + Arabica::DOM::Node<std::string> container; + PromelaEventSourceType type; + Trie* trie; }; class FSMToPromela : public InterpreterDraft6 { public: static void writeProgram(std::ostream& stream, const Interpreter& interpreter); + + static std::string beautifyIndentation(const std::string& code, int indent = 0); + protected: FSMToPromela(); void writeProgram(std::ostream& stream); @@ -78,22 +129,21 @@ protected: void writeStates(std::ostream& stream); void writeDeclarations(std::ostream& stream); void writeEventSources(std::ostream& stream); - void writeEventSource(std::ostream& stream, const std::string& name, const PromelaEventSource& source); void writeExecutableContent(std::ostream& stream, const Arabica::DOM::Node<std::string>& node, int indent = 0); void writeInlineComment(std::ostream& stream, const Arabica::DOM::Node<std::string>& node); void writeFSM(std::ostream& stream); void writeEventDispatching(std::ostream& stream); void writeMain(std::ostream& stream); - void writeIfBlock(std::ostream& stream, const Arabica::XPath::NodeSet<std::string>& condChain, int indent = 0); void writeDispatchingBlock(std::ostream& stream, const Arabica::XPath::NodeSet<std::string>& transChain, int indent = 0); - std::string beautifyIndentation(const std::string& code, int indent = 0); - Arabica::XPath::NodeSet<std::string> getTransientContent(const Arabica::DOM::Node<std::string>& state); Arabica::DOM::Node<std::string> getUltimateTarget(const Arabica::DOM::Node<std::string>& transition); - PromelaInlines getInlinePromela(const Arabica::XPath::NodeSet<std::string>& elements, bool recurse = false); + + static PromelaInlines getInlinePromela(const std::string&); + static PromelaInlines getInlinePromela(const Arabica::XPath::NodeSet<std::string>& elements, bool recurse = false); + static PromelaInlines getInlinePromela(const Arabica::DOM::Node<std::string>& elements); Trie _eventTrie; Arabica::XPath::NodeSet<std::string> _globalStates; |