summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorStefan Radomski <radomski@tk.informatik.tu-darmstadt.de>2014-04-24 08:36:14 (GMT)
committerStefan Radomski <radomski@tk.informatik.tu-darmstadt.de>2014-04-24 08:36:14 (GMT)
commit6b53548ae32336db822d6e6af0e14413c82c74dd (patch)
tree8f2ecf59b1713a9c3ff8720a01ac53c5fca7aa8e /src
parentb54d9c61b6c29c973168f33f683a49051f0ed3cc (diff)
downloaduscxml-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.cpp397
-rw-r--r--src/uscxml/transform/FSMToPromela.h80
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;