From af6609592298c5e047e37e5ae2b47e6a8edbb677 Mon Sep 17 00:00:00 2001 From: Stefan Radomski Date: Mon, 1 Dec 2014 12:02:40 +0100 Subject: Nested invokers and delayed events for PROMELA model checking --- README.md | 11 + apps/uscxml-browser.cpp | 12 +- embedding/java/.classpath | 3 +- .../datamodel/ecmascript/ECMAScriptDataModel.java | 2 +- .../tests/datamodel/TestPlatformExtensions.java | 2 +- src/uscxml/Interpreter.cpp | 10 +- src/uscxml/URL.cpp | 19 +- src/uscxml/URL.h | 5 + .../plugins/datamodel/promela/PromelaParser.cpp | 30 +- .../plugins/datamodel/promela/PromelaParser.h | 20 +- .../plugins/datamodel/promela/parser/promela.l | 17 + .../datamodel/promela/parser/promela.lex.yy.cpp | 199 ++-- .../datamodel/promela/parser/promela.tab.cpp | 422 +++++--- .../datamodel/promela/parser/promela.tab.hpp | 15 +- .../plugins/datamodel/promela/parser/promela.ypp | 37 +- src/uscxml/transform/ChartToFSM.cpp | 34 +- src/uscxml/transform/ChartToFSM.h | 2 + src/uscxml/transform/ChartToPromela.cpp | 1019 ++++++++++++++++---- src/uscxml/transform/ChartToPromela.h | 50 +- test/ctest/CTestCustom.ctest.in | 70 +- test/src/test-promela-parser.cpp | 16 +- test/uscxml/promela/test-syntax.scxml | 12 +- test/w3c/confPromela.xsl | 45 +- test/w3c/promela/test175.scxml | 6 +- test/w3c/promela/test185.scxml | 2 +- test/w3c/promela/test186.scxml | 2 +- test/w3c/promela/test187.scxml | 4 +- test/w3c/promela/test191.scxml | 2 +- test/w3c/promela/test192.scxml | 4 +- test/w3c/promela/test193.scxml | 2 +- test/w3c/promela/test207.scxml | 6 +- test/w3c/promela/test208.scxml | 4 +- test/w3c/promela/test210.scxml | 4 +- test/w3c/promela/test215.scxml | 2 +- test/w3c/promela/test216.scxml | 2 +- test/w3c/promela/test220.scxml | 2 +- test/w3c/promela/test223.scxml | 2 +- test/w3c/promela/test224.scxml | 2 +- test/w3c/promela/test225.scxml | 2 +- test/w3c/promela/test226.scxml | 2 +- test/w3c/promela/test228.scxml | 2 +- test/w3c/promela/test229.scxml | 4 +- test/w3c/promela/test230.scxml | 4 +- test/w3c/promela/test232.scxml | 2 +- test/w3c/promela/test233.scxml | 2 +- test/w3c/promela/test234.scxml | 4 +- test/w3c/promela/test235.scxml | 2 +- test/w3c/promela/test236.scxml | 2 +- test/w3c/promela/test237.scxml | 6 +- test/w3c/promela/test239.scxml | 2 +- test/w3c/promela/test240.scxml | 4 +- test/w3c/promela/test241.scxml | 2 +- test/w3c/promela/test242.scxml | 97 +- test/w3c/promela/test243.scxml | 2 +- test/w3c/promela/test244.scxml | 2 +- test/w3c/promela/test245.scxml | 2 +- test/w3c/promela/test247.scxml | 2 +- test/w3c/promela/test250.scxml | 2 +- test/w3c/promela/test252.scxml | 4 +- test/w3c/promela/test253.scxml | 2 +- test/w3c/promela/test298.scxml | 2 +- test/w3c/promela/test311.scxml | 2 +- test/w3c/promela/test338.scxml | 2 +- test/w3c/promela/test347.scxml | 80 +- test/w3c/promela/test350.scxml | 2 +- test/w3c/promela/test351.scxml | 4 +- test/w3c/promela/test352.scxml | 2 +- test/w3c/promela/test354.scxml | 4 +- test/w3c/promela/test364.scxml | 2 +- test/w3c/promela/test372.scxml | 2 +- test/w3c/promela/test387.scxml | 2 +- test/w3c/promela/test388.scxml | 2 +- test/w3c/promela/test399.scxml | 2 +- test/w3c/promela/test402.scxml | 2 +- test/w3c/promela/test403a.scxml | 2 +- test/w3c/promela/test403c.scxml | 2 +- test/w3c/promela/test405.scxml | 2 +- test/w3c/promela/test406.scxml | 2 +- test/w3c/promela/test409.scxml | 2 +- test/w3c/promela/test411.scxml | 2 +- test/w3c/promela/test412.scxml | 2 +- test/w3c/promela/test416.scxml | 2 +- test/w3c/promela/test417.scxml | 2 +- test/w3c/promela/test422.scxml | 2 +- test/w3c/promela/test423.scxml | 2 +- test/w3c/promela/test501.scxml | 2 +- test/w3c/promela/test530.scxml | 2 +- test/w3c/promela/test531.scxml | 2 +- test/w3c/promela/test532.scxml | 2 +- test/w3c/promela/test553.scxml | 2 +- test/w3c/promela/test554.scxml | 2 +- test/w3c/promela/test567.scxml | 2 +- test/w3c/promela/test570.scxml | 2 +- test/w3c/promela/test576.scxml | 2 +- test/w3c/promela/test579.scxml | 2 +- test/w3c/promela/test580.scxml | 2 +- test/w3c/run_promela_test.cmake | 2 +- 97 files changed, 1728 insertions(+), 679 deletions(-) diff --git a/README.md b/README.md index ff10818..60f803b 100644 --- a/README.md +++ b/README.md @@ -168,6 +168,7 @@ The uSCXML interpreter can be extended by introducing new 2. Invokers to represent external components that deliver and accept events (e.g. iCal, SceneGraph, DirectoryMonitor) 3. I/O-Processors to provide communication with external systems (e.g. BasicHTTP, SCXML). 4. Elements for Executable Content (e.g. <respond>, <fetch>, <postpone>). +5. Data model extionsions to establish callbacks from the data model into the host language. The basic approach to extend the interpreter is the same in all cases: @@ -180,6 +181,16 @@ The basic approach to extend the interpreter is the same in all cases: Note: Within the language bindings, you will have to inherit the base classes without the Impl suffix. Have a look at the examples in embedding for examples. + #### Ad-hoc Extensions Sometimes, it is more suited to provide an interpreter with an already instantiated extension (e.g. an diff --git a/apps/uscxml-browser.cpp b/apps/uscxml-browser.cpp index a3c7419..359a9a0 100644 --- a/apps/uscxml-browser.cpp +++ b/apps/uscxml-browser.cpp @@ -28,7 +28,17 @@ class VerboseMonitor : public uscxml::InterpreterMonitor { } void beforeProcessingEvent(uscxml::Interpreter interpreter, const uscxml::Event& event) { - std::cout << "Event: " << event.name << std::endl; + switch (event.eventType) { + case uscxml::Event::INTERNAL: + std::cout << "Internal Event: " << event.name << std::endl; + break; + case uscxml::Event::EXTERNAL: + std::cout << "External Event: " << event.name << std::endl; + break; + case uscxml::Event::PLATFORM: + std::cout << "Platform Event: " << event.name << std::endl; + break; + } } void beforeCompletion(uscxml::Interpreter interpreter) { diff --git a/embedding/java/.classpath b/embedding/java/.classpath index fa94b3c..7d0462c 100644 --- a/embedding/java/.classpath +++ b/embedding/java/.classpath @@ -2,8 +2,7 @@ - - + diff --git a/embedding/java/src/org/uscxml/datamodel/ecmascript/ECMAScriptDataModel.java b/embedding/java/src/org/uscxml/datamodel/ecmascript/ECMAScriptDataModel.java index 679581d..ca53df3 100644 --- a/embedding/java/src/org/uscxml/datamodel/ecmascript/ECMAScriptDataModel.java +++ b/embedding/java/src/org/uscxml/datamodel/ecmascript/ECMAScriptDataModel.java @@ -118,7 +118,7 @@ public class ECMAScriptDataModel extends DataModel { invokers.put(key, invokersNatives.get(key).getDataModelVariables()); } newDM.scope - .put("_ioprocessors", newDM.scope, new ECMAData(invokers)); + .put("_invokers", newDM.scope, new ECMAData(invokers)); } // In predicate (not working as static is required) see: diff --git a/embedding/java/src/org/uscxml/tests/datamodel/TestPlatformExtensions.java b/embedding/java/src/org/uscxml/tests/datamodel/TestPlatformExtensions.java index 86ba884..4b2a59e 100644 --- a/embedding/java/src/org/uscxml/tests/datamodel/TestPlatformExtensions.java +++ b/embedding/java/src/org/uscxml/tests/datamodel/TestPlatformExtensions.java @@ -8,7 +8,7 @@ import org.uscxml.InterpreterState; public class TestPlatformExtensions extends DataModelExtension { - /* Currently only with ECMAScript via JavaScriptCore! */ + /* Currently only with ECMAScript datamodels! */ @Override public String provides() { diff --git a/src/uscxml/Interpreter.cpp b/src/uscxml/Interpreter.cpp index dc53906..6aca93c 100644 --- a/src/uscxml/Interpreter.cpp +++ b/src/uscxml/Interpreter.cpp @@ -1682,6 +1682,8 @@ void InterpreterImpl::send(const Arabica::DOM::Element& element) { sendReq.delayMs = strTo(delayAttr.value); } else if (iequals(delayAttr.unit, "s")) { sendReq.delayMs = strTo(delayAttr.value) * 1000; + } else if (delayAttr.unit.length() == 0) { // unit less delay is interpreted as milliseconds + sendReq.delayMs = strTo(delayAttr.value); } else { LOG(ERROR) << "Cannot make sense of delay value " << delay << ": does not end in 's' or 'ms'"; } @@ -1784,7 +1786,7 @@ void InterpreterImpl::delayedSend(void* userdata, std::string eventName) { } catch(Event e) { throw e; } catch (const std::exception &e) { - LOG(ERROR) << "Exception caught while sending event to ioprocessor " << sendReq.type << ":" << e.what(); + LOG(ERROR) << "Exception caught while sending event to ioprocessor " << sendReq.type << ": '" << e.what() << "'"; } catch(...) { LOG(ERROR) << "Exception caught while sending event to ioprocessor " << sendReq.type; } @@ -2790,13 +2792,11 @@ NodeSet InterpreterImpl::filterChildElements(const std::string& tag return filteredChildElems; } + NodeSet InterpreterImpl::filterChildType(const Node_base::Type type, const NodeSet& nodeSet, bool recurse) { NodeSet filteredChildType; for (unsigned int i = 0; i < nodeSet.size(); i++) { - if (nodeSet[i].getNodeType() == type) - filteredChildType.push_back(nodeSet[i]); - if (recurse) - filteredChildType.push_back(filterChildType(type, nodeSet[i], recurse)); + filteredChildType.push_back(filterChildType(type, nodeSet[i], recurse)); } return filteredChildType; } diff --git a/src/uscxml/URL.cpp b/src/uscxml/URL.cpp index b1297d5..38cb780 100644 --- a/src/uscxml/URL.cpp +++ b/src/uscxml/URL.cpp @@ -562,6 +562,7 @@ std::ostream & operator<<(std::ostream & stream, const URL& url) { URLFetcher::URLFetcher() { _isStarted = false; + _envProxy = NULL; _multiHandle = curl_multi_init(); // read proxy information from environment @@ -575,15 +576,16 @@ URLFetcher::URLFetcher() { // CURLOPT_PROXYUSERNAME; // CURLOPT_PROXYUSERPWD; - bool unsupported = false; - CURLcode curlError; - /* see http://curl.haxx.se/libcurl/c/CURLOPT_PROXY.html e.g. 'socks5://bob:marley@localhost:12345' */ - char* envProxy = getenv("USCXML_PROXY"); + _envProxy = getenv("USCXML_PROXY"); +#if 0 + bool unsupported = false; + CURLcode curlError; + // exposed just in case char* envProxyTransferMode = getenv("USCXML_PROXY_TRANSFER_MODE"); char* envProxyAuth = getenv("USCXML_PROXYAUTH"); @@ -645,7 +647,8 @@ URLFetcher::URLFetcher() { if (envProxyUserPwd) (curlError = curl_easy_setopt(_multiHandle, CURLOPT_PROXYUSERPWD, envProxyUserPwd)) == CURLE_OK || LOG(ERROR) << "Cannot set curl proxy user password: " << curl_easy_strerror(curlError); - +#endif + start(); } @@ -693,12 +696,16 @@ void URLFetcher::fetchURL(URL& url) { (curlError = curl_easy_setopt(handle, CURLOPT_SSL_VERIFYPEER, false)) == CURLE_OK || LOG(ERROR) << "Cannot forfeit peer verification: " << curl_easy_strerror(curlError); - (curlError = curl_easy_setopt(handle, CURLOPT_USERAGENT, "uscxml/0.3.3")) == CURLE_OK || + (curlError = curl_easy_setopt(handle, CURLOPT_USERAGENT, "uscxml/" USCXML_VERSION)) == CURLE_OK || LOG(ERROR) << "Cannot set our user agent string: " << curl_easy_strerror(curlError); (curlError = curl_easy_setopt(handle, CURLOPT_FOLLOWLOCATION, true)) == CURLE_OK || LOG(ERROR) << "Cannot enable follow redirects: " << curl_easy_strerror(curlError); + if (instance->_envProxy) + (curlError = curl_easy_setopt(handle, CURLOPT_PROXY, instance->_envProxy)) == CURLE_OK || + LOG(ERROR) << "Cannot set curl proxy: " << curl_easy_strerror(curlError); + if (iequals(url._impl->_requestType, "post")) { (curlError = curl_easy_setopt(handle, CURLOPT_POST, 1)) == CURLE_OK || diff --git a/src/uscxml/URL.h b/src/uscxml/URL.h index 09d5ed0..20a22cc 100644 --- a/src/uscxml/URL.h +++ b/src/uscxml/URL.h @@ -283,6 +283,10 @@ public: return _impl->operator Data(); } + operator std::string() const { + return asString(); + } + protected: void downloadStarted() { return _impl->downloadStarted(); @@ -322,6 +326,7 @@ protected: std::map _handlesToURLs; CURLM* _multiHandle; + char* _envProxy; }; USCXML_API std::ostream& operator<< (std::ostream &stream, const URL& p); diff --git a/src/uscxml/plugins/datamodel/promela/PromelaParser.cpp b/src/uscxml/plugins/datamodel/promela/PromelaParser.cpp index 9fed02c..ada2c48 100644 --- a/src/uscxml/plugins/datamodel/promela/PromelaParser.cpp +++ b/src/uscxml/plugins/datamodel/promela/PromelaParser.cpp @@ -30,11 +30,12 @@ void promela__delete_buffer(YY_BUFFER_STATE, void*); YY_BUFFER_STATE promela__scan_string (const char * yystr , void*); -extern int promela_lex (PROMELA_STYPE* yylval_param, void* yyscanner); +extern int promela_lex (PROMELA_STYPE* yylval_param, PROMELA_LTYPE* yylloc_param, void* yyscanner); int promela_lex_init (void**); int promela_lex_destroy (void*); -void promela_error (uscxml::PromelaParser* ctx, void* yyscanner, const char* err) { +void promela_error (void* yylloc_param, uscxml::PromelaParser* ctx, void* yyscanner, const char* err) { + PROMELA_LTYPE* yylloc = (PROMELA_LTYPE*)yylloc_param; // mark as pending exception as we cannot throw from constructor and have the destructor called ERROR_EXECUTION(excEvent, err); ctx->pendingException = excEvent; @@ -120,26 +121,41 @@ PromelaParserNode::~PromelaParserNode() { delete operands.front(); operands.pop_front(); } + if (loc) + free(loc); } PromelaParserNode* PromelaParser::node(int type, int nrArgs, ...) { PromelaParserNode* newNode = new PromelaParserNode(); + newNode->type = type; va_list ap; va_start(ap, nrArgs); for(int i = 1; i <= nrArgs; i++) { newNode->operands.push_back(va_arg(ap, PromelaParserNode*)); + newNode->operands.back()->parent = newNode; } return newNode; } -PromelaParserNode* PromelaParser::value(int type, const char* value) { +PromelaParserNode* PromelaParser::value(int type, void* location, const char* value) { PromelaParserNode* newNode = new PromelaParserNode(); + + if (location) { + PROMELA_LTYPE* location_param = (PROMELA_LTYPE*)location; + newNode->loc = (PromelaParserNode::Location*)malloc(sizeof(PromelaParserNode::Location)); + newNode->loc->firstCol = location_param->first_column; + newNode->loc->firstLine = location_param->first_line; + newNode->loc->lastCol = location_param->last_column; + newNode->loc->lastLine = location_param->last_line; + } + newNode->value = value; newNode->type = type; return newNode; } + void PromelaParser::dump() { switch (type) { case PROMELA_EXPR: @@ -160,11 +176,13 @@ void PromelaParserNode::merge(PromelaParserNode* node) { for (std::list::iterator iter = node->operands.begin(); iter != node->operands.end(); iter++) { operands.push_back(*iter); + (*iter)->parent = this; } node->operands.clear(); } void PromelaParserNode::push(PromelaParserNode* node) { + node->parent = this; operands.push_back(node); } @@ -173,7 +191,11 @@ void PromelaParserNode::dump(int indent) { for (int i = 0; i < indent; i++) { padding += " "; } - std::cout << padding << typeToDesc(type) << ": " << value << std::endl; + std::cout << padding << typeToDesc(type) << ": " << value; + if (loc != NULL) { + std::cout << " (" << loc->firstLine << ":" << loc->firstCol << ")-(" << loc->lastLine << ":" << loc->lastCol << ")"; + } + std::cout << std::endl; for (std::list::iterator iter = operands.begin(); iter != operands.end(); iter++) { (*iter)->dump(indent + 1); diff --git a/src/uscxml/plugins/datamodel/promela/PromelaParser.h b/src/uscxml/plugins/datamodel/promela/PromelaParser.h index 6cf9a81..303b9be 100644 --- a/src/uscxml/plugins/datamodel/promela/PromelaParser.h +++ b/src/uscxml/plugins/datamodel/promela/PromelaParser.h @@ -32,8 +32,16 @@ namespace uscxml { class PromelaParser; -struct PromelaParserNode { - PromelaParserNode() : type(0) {} +class PromelaParserNode { +public: + struct Location { + int firstLine; + int firstCol; + int lastLine; + int lastCol; + }; + + PromelaParserNode() : type(0), parent(NULL), loc(NULL) {} virtual ~PromelaParserNode(); void merge(PromelaParserNode* node); @@ -45,7 +53,8 @@ struct PromelaParserNode { int type; std::string value; std::list operands; - + PromelaParserNode* parent; + Location* loc; }; class PromelaParser { @@ -58,12 +67,13 @@ public: static std::string typeToDesc(int type); + PromelaParser() : ast(NULL) {} PromelaParser(const std::string& expr); PromelaParser(const std::string& expr, int nrArgs, ...); virtual ~PromelaParser(); virtual PromelaParserNode* node(int type, int nrArgs, ...); - virtual PromelaParserNode* value(int type, const char* value); + virtual PromelaParserNode* value(int type, void* location, const char* value); void dump(); int parseInCompound; @@ -86,6 +96,6 @@ protected: } -void promela_error (uscxml::PromelaParser* ctx, void* yyscanner, const char* err); +void promela_error (void* yylloc_param, uscxml::PromelaParser* ctx, void* yyscanner, const char* err); #endif /* end of include guard: PROMELA_H_9AB78YB1 */ diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.l b/src/uscxml/plugins/datamodel/promela/parser/promela.l index dc4b66c..d247d74 100644 --- a/src/uscxml/plugins/datamodel/promela/parser/promela.l +++ b/src/uscxml/plugins/datamodel/promela/parser/promela.l @@ -2,6 +2,7 @@ /* see: http://spinroot.com/spin/Man/operators.html */ +%option yylineno %option reentrant %option bison-bridge %option prefix="promela_" @@ -9,12 +10,28 @@ %option noyywrap %option debug %option never-interactive nounistd +%option bison-locations %{ #include "../PromelaParser.h" #include "promela.tab.hpp" #define YYSTYPE PROMELA_STYPE +#define YYLTYPE PROMELA_LTYPE +#define YY_USER_INIT \ + yycolumn = yylloc->first_line = yylloc->first_column = 0; \ + yylineno = yylloc->last_line = yylloc->last_column = 0; \ + +//int yycolumn = 1; + +#define YY_USER_ACTION \ +{ \ + yylloc->first_line = yylineno; \ + yylloc->first_column = yycolumn; \ + yylloc->last_column = yycolumn + yyleng; \ + yylloc->last_line = yylineno; \ + yycolumn = yycolumn + yyleng; \ +} %} diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.lex.yy.cpp b/src/uscxml/plugins/datamodel/promela/parser/promela.lex.yy.cpp index c6e4573..842efe6 100644 --- a/src/uscxml/plugins/datamodel/promela/parser/promela.lex.yy.cpp +++ b/src/uscxml/plugins/datamodel/promela/parser/promela.lex.yy.cpp @@ -230,7 +230,20 @@ typedef size_t yy_size_t; #define EOB_ACT_END_OF_FILE 1 #define EOB_ACT_LAST_MATCH 2 - #define YY_LESS_LINENO(n) + /* Note: We specifically omit the test for yy_rule_can_match_eol because it requires + * access to the local variable yy_act. Since yyless() is a macro, it would break + * existing scanners that call yyless() from OUTSIDE promela_lex. + * One obvious solution it to make yy_act a global. I tried that, and saw + * a 5% performance hit in a non-yylineno scanner, because yy_act is + * normally declared as a register variable-- so it is not worth it. + */ + #define YY_LESS_LINENO(n) \ + do { \ + yy_size_t yyl;\ + for ( yyl = n; yyl < yyleng; ++yyl )\ + if ( yytext[yyl] == '\n' )\ + --yylineno;\ + }while(0) /* Return all but the first "n" matched characters back to the input stream. */ #define yyless(n) \ @@ -594,13 +607,20 @@ static yyconst flex_int16_t yy_chk[221] = 123, 123, 123, 123, 123, 123, 123, 123, 123, 123 } ; +/* Table of booleans, true if rule could match eol. */ +static yyconst flex_int32_t yy_rule_can_match_eol[47] = + { 0, +1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 1, 1, 0, 0, 1, 0, 0, }; + static yyconst flex_int16_t yy_rule_linenum[46] = { 0, - 27, 29, 34, 35, 36, 37, 38, 40, 41, 42, - 43, 45, 46, 47, 49, 50, 52, 53, 55, 56, - 57, 58, 60, 61, 63, 64, 65, 68, 69, 71, - 72, 73, 75, 76, 78, 79, 81, 82, 84, 86, - 89, 94, 95, 97, 100 + 44, 46, 51, 52, 53, 54, 55, 57, 58, 59, + 60, 62, 63, 64, 66, 67, 69, 70, 72, 73, + 74, 75, 77, 78, 80, 81, 82, 85, 86, 88, + 89, 90, 92, 93, 95, 96, 98, 99, 101, 103, + 106, 111, 112, 114, 117 } ; /* The intent behind this definition is that it'll catch @@ -614,13 +634,28 @@ static yyconst flex_int16_t yy_rule_linenum[46] = /* see: http://www.phpcompiler.org/articles/reentrantparser.html */ /* see: http://spinroot.com/spin/Man/operators.html */ #define YY_NO_UNISTD_H 1 -#line 14 "promela.l" +#line 16 "promela.l" #include "../PromelaParser.h" #include "promela.tab.hpp" #define YYSTYPE PROMELA_STYPE +#define YYLTYPE PROMELA_LTYPE +#define YY_USER_INIT \ + yycolumn = yylloc->first_line = yylloc->first_column = 0; \ + yylineno = yylloc->last_line = yylloc->last_column = 0; \ + +//int yycolumn = 1; + +#define YY_USER_ACTION \ +{ \ + yylloc->first_line = yylineno; \ + yylloc->first_column = yycolumn; \ + yylloc->last_column = yycolumn + yyleng; \ + yylloc->last_line = yylineno; \ + yycolumn = yycolumn + yyleng; \ +} -#line 624 "promela.lex.yy.cpp" +#line 659 "promela.lex.yy.cpp" #define INITIAL 0 @@ -677,6 +712,8 @@ struct yyguts_t YYSTYPE * yylval_r; + YYLTYPE * yylloc_r; + }; /* end struct yyguts_t */ /* %if-c-only */ @@ -691,6 +728,8 @@ static int yy_init_globals (yyscan_t yyscanner ); * from bison output in section 1.*/ # define yylval yyg->yylval_r + # define yylloc yyg->yylloc_r + int promela_lex_init (yyscan_t* scanner); int promela_lex_init_extra (YY_EXTRA_TYPE user_defined,yyscan_t* scanner); @@ -734,6 +773,10 @@ YYSTYPE * promela_get_lval (yyscan_t yyscanner ); void promela_set_lval (YYSTYPE * yylval_param ,yyscan_t yyscanner ); + YYLTYPE *promela_get_lloc (yyscan_t yyscanner ); + + void promela_set_lloc (YYLTYPE * yylloc_param ,yyscan_t yyscanner ); + /* %endif */ /* Macros after this point can all be overridden by user definitions in @@ -881,10 +924,10 @@ static int input (yyscan_t yyscanner ); /* %if-c-only Standard (non-C++) definition */ extern int promela_lex \ - (YYSTYPE * yylval_param ,yyscan_t yyscanner); + (YYSTYPE * yylval_param,YYLTYPE * yylloc_param ,yyscan_t yyscanner); #define YY_DECL int promela_lex \ - (YYSTYPE * yylval_param , yyscan_t yyscanner) + (YYSTYPE * yylval_param, YYLTYPE * yylloc_param , yyscan_t yyscanner) /* %endif */ /* %if-c++-only C++ definition */ /* %endif */ @@ -918,13 +961,15 @@ YY_DECL struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; /* %% [7.0] user's declarations go here */ -#line 25 "promela.l" +#line 42 "promela.l" -#line 925 "promela.lex.yy.cpp" +#line 968 "promela.lex.yy.cpp" yylval = yylval_param; + yylloc = yylloc_param; + if ( !yyg->yy_init ) { yyg->yy_init = 1; @@ -1004,6 +1049,18 @@ yy_find_action: /* %% [11.0] code for yylineno update goes here */ + if ( yy_act != YY_END_OF_BUFFER && yy_rule_can_match_eol[yy_act] ) + { + yy_size_t yyl; + for ( yyl = 0; yyl < yyleng; ++yyl ) + if ( yytext[yyl] == '\n' ) + + do{ yylineno++; + yycolumn=0; + }while(0) +; + } + do_action: /* This label is used only to access EOF actions. */ /* %% [12.0] debug code goes here */ @@ -1036,12 +1093,12 @@ do_action: /* This label is used only to access EOF actions. */ case 1: /* rule 1 can match eol */ YY_RULE_SETUP -#line 27 "promela.l" +#line 44 "promela.l" /* multiline comments */ YY_BREAK case 2: YY_RULE_SETUP -#line 29 "promela.l" +#line 46 "promela.l" { yylval->value = strdup(yytext); return PML_TYPE; @@ -1049,199 +1106,199 @@ YY_RULE_SETUP YY_BREAK case 3: YY_RULE_SETUP -#line 34 "promela.l" +#line 51 "promela.l" { return PML_LEN; } YY_BREAK case 4: YY_RULE_SETUP -#line 35 "promela.l" +#line 52 "promela.l" { yylval->value = strdup(yytext); return PML_CONST; } YY_BREAK case 5: YY_RULE_SETUP -#line 36 "promela.l" +#line 53 "promela.l" { return PML_PRINT; } YY_BREAK case 6: YY_RULE_SETUP -#line 37 "promela.l" +#line 54 "promela.l" { return PML_TYPEDEF; } YY_BREAK case 7: YY_RULE_SETUP -#line 38 "promela.l" +#line 55 "promela.l" { return PML_ASSERT; } YY_BREAK case 8: YY_RULE_SETUP -#line 40 "promela.l" +#line 57 "promela.l" { return PML_NEG; } YY_BREAK case 9: YY_RULE_SETUP -#line 41 "promela.l" +#line 58 "promela.l" { return PML_COMPL; } YY_BREAK case 10: YY_RULE_SETUP -#line 42 "promela.l" +#line 59 "promela.l" { return PML_INCR; } YY_BREAK case 11: YY_RULE_SETUP -#line 43 "promela.l" +#line 60 "promela.l" { return PML_DECR; } YY_BREAK case 12: YY_RULE_SETUP -#line 45 "promela.l" +#line 62 "promela.l" { return PML_TIMES; } YY_BREAK case 13: YY_RULE_SETUP -#line 46 "promela.l" +#line 63 "promela.l" { return PML_DIVIDE; } YY_BREAK case 14: YY_RULE_SETUP -#line 47 "promela.l" +#line 64 "promela.l" { return PML_MODULO; } YY_BREAK case 15: YY_RULE_SETUP -#line 49 "promela.l" +#line 66 "promela.l" { return PML_PLUS; } YY_BREAK case 16: YY_RULE_SETUP -#line 50 "promela.l" +#line 67 "promela.l" { return PML_MINUS; } YY_BREAK case 17: YY_RULE_SETUP -#line 52 "promela.l" +#line 69 "promela.l" { return PML_LSHIFT; } YY_BREAK case 18: YY_RULE_SETUP -#line 53 "promela.l" +#line 70 "promela.l" { return PML_RSHIFT; } YY_BREAK case 19: YY_RULE_SETUP -#line 55 "promela.l" +#line 72 "promela.l" { return PML_LE; } YY_BREAK case 20: YY_RULE_SETUP -#line 56 "promela.l" +#line 73 "promela.l" { return PML_GE; } YY_BREAK case 21: YY_RULE_SETUP -#line 57 "promela.l" +#line 74 "promela.l" { return PML_LT; } YY_BREAK case 22: YY_RULE_SETUP -#line 58 "promela.l" +#line 75 "promela.l" { return PML_GT; } YY_BREAK case 23: YY_RULE_SETUP -#line 60 "promela.l" +#line 77 "promela.l" { return PML_NE; } YY_BREAK case 24: YY_RULE_SETUP -#line 61 "promela.l" +#line 78 "promela.l" { return PML_EQ; } YY_BREAK case 25: YY_RULE_SETUP -#line 63 "promela.l" +#line 80 "promela.l" { return PML_BITAND; } YY_BREAK case 26: YY_RULE_SETUP -#line 64 "promela.l" +#line 81 "promela.l" { return PML_BITXOR; } YY_BREAK case 27: YY_RULE_SETUP -#line 65 "promela.l" +#line 82 "promela.l" { return PML_BITOR; } YY_BREAK case 28: YY_RULE_SETUP -#line 68 "promela.l" +#line 85 "promela.l" { return PML_AND; } YY_BREAK case 29: YY_RULE_SETUP -#line 69 "promela.l" +#line 86 "promela.l" { return PML_OR; } YY_BREAK case 30: YY_RULE_SETUP -#line 71 "promela.l" +#line 88 "promela.l" { return PML_DOT; } YY_BREAK case 31: YY_RULE_SETUP -#line 72 "promela.l" +#line 89 "promela.l" { return PML_COMMA; } YY_BREAK case 32: YY_RULE_SETUP -#line 73 "promela.l" +#line 90 "promela.l" { return PML_SEMI; } YY_BREAK case 33: YY_RULE_SETUP -#line 75 "promela.l" +#line 92 "promela.l" { return '('; } YY_BREAK case 34: YY_RULE_SETUP -#line 76 "promela.l" +#line 93 "promela.l" { return ')'; } YY_BREAK case 35: YY_RULE_SETUP -#line 78 "promela.l" +#line 95 "promela.l" { return '['; } YY_BREAK case 36: YY_RULE_SETUP -#line 79 "promela.l" +#line 96 "promela.l" { return ']'; } YY_BREAK case 37: YY_RULE_SETUP -#line 81 "promela.l" +#line 98 "promela.l" { return '{'; } YY_BREAK case 38: YY_RULE_SETUP -#line 82 "promela.l" +#line 99 "promela.l" { return '}'; } YY_BREAK case 39: YY_RULE_SETUP -#line 84 "promela.l" +#line 101 "promela.l" { return PML_ASGN; } YY_BREAK case 40: /* rule 40 can match eol */ YY_RULE_SETUP -#line 86 "promela.l" +#line 103 "promela.l" { yylval->value = strdup(yytext); return(PML_STRING); } YY_BREAK case 41: /* rule 41 can match eol */ YY_RULE_SETUP -#line 89 "promela.l" +#line 106 "promela.l" { /* Non PROMELA extension for single quoted string literals */ yylval->value = strdup(yytext); return(PML_STRING); @@ -1249,31 +1306,31 @@ YY_RULE_SETUP YY_BREAK case 42: YY_RULE_SETUP -#line 94 "promela.l" +#line 111 "promela.l" { yylval->value = strdup(yytext); return PML_CONST; } YY_BREAK case 43: YY_RULE_SETUP -#line 95 "promela.l" +#line 112 "promela.l" { yylval->value = strdup(yytext); return PML_NAME; } YY_BREAK case 44: /* rule 44 can match eol */ YY_RULE_SETUP -#line 97 "promela.l" +#line 114 "promela.l" /* eat up whitespace */ YY_BREAK case 45: YY_RULE_SETUP -#line 100 "promela.l" +#line 117 "promela.l" { /*printf( "Unrecognized character: %s\n", yytext ); */ } YY_BREAK case 46: YY_RULE_SETUP -#line 101 "promela.l" +#line 118 "promela.l" ECHO; YY_BREAK -#line 1277 "promela.lex.yy.cpp" +#line 1334 "promela.lex.yy.cpp" case YY_STATE_EOF(INITIAL): yyterminate(); @@ -1672,6 +1729,10 @@ static int yy_get_next_buffer (yyscan_t yyscanner) /* %% [18.0] update yylineno here */ + if ( c == '\n' ){ + --yylineno; + } + yyg->yytext_ptr = yy_bp; yyg->yy_hold_char = *yy_cp; yyg->yy_c_buf_p = yy_cp; @@ -1756,6 +1817,12 @@ static int yy_get_next_buffer (yyscan_t yyscanner) yyg->yy_hold_char = *++yyg->yy_c_buf_p; /* %% [19.0] update BOL and yylineno */ + if ( c == '\n' ) + + do{ yylineno++; + yycolumn=0; + }while(0) +; return c; } @@ -2387,6 +2454,18 @@ void promela_set_lval (YYSTYPE * yylval_param , yyscan_t yyscanner) yylval = yylval_param; } +YYLTYPE *promela_get_lloc (yyscan_t yyscanner) +{ + struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; + return yylloc; +} + +void promela_set_lloc (YYLTYPE * yylloc_param , yyscan_t yyscanner) +{ + struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; + yylloc = yylloc_param; +} + /* %endif */ /* User-visible API */ @@ -2577,4 +2656,4 @@ void promela_free (void * ptr , yyscan_t yyscanner) /* %ok-for-header */ -#line 101 "promela.l" +#line 118 "promela.l" diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.tab.cpp b/src/uscxml/plugins/datamodel/promela/parser/promela.tab.cpp index 3e9e92c..9d957e7 100644 --- a/src/uscxml/plugins/datamodel/promela/parser/promela.tab.cpp +++ b/src/uscxml/plugins/datamodel/promela/parser/promela.tab.cpp @@ -60,6 +60,7 @@ /* Substitute the type names. */ #define YYSTYPE PROMELA_STYPE +#define YYLTYPE PROMELA_LTYPE /* Substitute the variable and function names. */ #define yyparse promela_parse #define yylex promela_lex @@ -68,6 +69,7 @@ #define yychar promela_char #define yydebug promela_debug #define yynerrs promela_nerrs +#define yylloc promela_lloc /* Copy the first part of user declarations. */ /* Line 371 of yacc.c */ @@ -82,12 +84,12 @@ #define YYDEBUG 1 #define YYERROR_VERBOSE 1 -extern int promela_lex (PROMELA_STYPE* yylval_param, void* yyscanner); +extern int promela_lex (PROMELA_STYPE* yylval_param, PROMELA_LTYPE* yylloc_param, void* yyscanner); using namespace uscxml; /* Line 371 of yacc.c */ -#line 91 "promela.tab.cpp" +#line 93 "promela.tab.cpp" # ifndef YY_NULL # if defined __cplusplus && 201103L <= __cplusplus @@ -212,20 +214,33 @@ extern int promela_debug; typedef union PROMELA_STYPE { /* Line 387 of yacc.c */ -#line 38 "promela.ypp" +#line 39 "promela.ypp" uscxml::PromelaParserNode* node; char* value; /* Line 387 of yacc.c */ -#line 223 "promela.tab.cpp" +#line 225 "promela.tab.cpp" } PROMELA_STYPE; # define PROMELA_STYPE_IS_TRIVIAL 1 # define promela_stype PROMELA_STYPE /* obsolescent; will be withdrawn */ # define PROMELA_STYPE_IS_DECLARED 1 #endif +#if ! defined PROMELA_LTYPE && ! defined PROMELA_LTYPE_IS_DECLARED +typedef struct PROMELA_LTYPE +{ + int first_line; + int first_column; + int last_line; + int last_column; +} PROMELA_LTYPE; +# define promela_ltype PROMELA_LTYPE /* obsolescent; will be withdrawn */ +# define PROMELA_LTYPE_IS_DECLARED 1 +# define PROMELA_LTYPE_IS_TRIVIAL 1 +#endif + #ifdef YYPARSE_PARAM #if defined __STDC__ || defined __cplusplus @@ -246,7 +261,7 @@ int promela_parse (); /* Copy the second part of user declarations. */ /* Line 390 of yacc.c */ -#line 250 "promela.tab.cpp" +#line 265 "promela.tab.cpp" #ifdef short # undef short @@ -414,13 +429,15 @@ void free (void *); /* INFRINGES ON USER NAME SPACE */ #if (! defined yyoverflow \ && (! defined __cplusplus \ - || (defined PROMELA_STYPE_IS_TRIVIAL && PROMELA_STYPE_IS_TRIVIAL))) + || (defined PROMELA_LTYPE_IS_TRIVIAL && PROMELA_LTYPE_IS_TRIVIAL \ + && defined PROMELA_STYPE_IS_TRIVIAL && PROMELA_STYPE_IS_TRIVIAL))) /* A type that is properly aligned for any stack member. */ union yyalloc { yytype_int16 yyss_alloc; YYSTYPE yyvs_alloc; + YYLTYPE yyls_alloc; }; /* The size of the maximum gap between one aligned stack and the next. */ @@ -429,8 +446,8 @@ union yyalloc /* The size of an array large to enough to hold all stacks, each with N elements. */ # define YYSTACK_BYTES(N) \ - ((N) * (sizeof (yytype_int16) + sizeof (YYSTYPE)) \ - + YYSTACK_GAP_MAXIMUM) + ((N) * (sizeof (yytype_int16) + sizeof (YYSTYPE) + sizeof (YYLTYPE)) \ + + 2 * YYSTACK_GAP_MAXIMUM) # define YYCOPY_NEEDED 1 @@ -583,15 +600,15 @@ static const yytype_int8 yyrhs[] = /* YYRLINE[YYN] -- source line where rule number YYN was defined. */ static const yytype_uint8 yyrline[] = { - 0, 84, 84, 88, 92, 98, 101, 102, 105, 120, - 121, 131, 132, 133, 134, 135, 136, 137, 138, 139, - 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, - 150, 151, 153, 154, 155, 156, 162, 163, 164, 165, - 168, 169, 170, 171, 174, 177, 178, 179, 189, 190, - 193, 194, 197, 198, 199, 202, 203, 204, 205, 206, - 207, 208, 209, 212, 213, 222, 225, 226, 227, 230, - 233, 234, 235, 236, 237, 238, 239, 240, 243, 244, - 247, 248 + 0, 85, 85, 89, 93, 99, 102, 103, 106, 121, + 122, 132, 133, 134, 135, 136, 137, 138, 139, 140, + 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, + 151, 152, 154, 155, 156, 157, 163, 164, 165, 166, + 169, 170, 171, 172, 175, 178, 179, 180, 190, 191, + 194, 195, 198, 199, 200, 203, 204, 205, 206, 207, + 208, 209, 210, 213, 214, 223, 226, 227, 228, 231, + 234, 235, 236, 237, 238, 239, 240, 241, 244, 245, + 248, 249 }; #endif @@ -862,7 +879,7 @@ do \ } \ else \ { \ - yyerror (ctx, scanner, YY_("syntax error: cannot back up")); \ + yyerror (&yylloc, ctx, scanner, YY_("syntax error: cannot back up")); \ YYERROR; \ } \ while (YYID (0)) @@ -872,17 +889,90 @@ while (YYID (0)) #define YYERRCODE 256 -/* This macro is provided for backward compatibility. */ +/* YYLLOC_DEFAULT -- Set CURRENT to span from RHS[1] to RHS[N]. + If N is 0, then set CURRENT to the empty location which ends + the previous symbol: RHS[0] (always defined). */ + +#ifndef YYLLOC_DEFAULT +# define YYLLOC_DEFAULT(Current, Rhs, N) \ + do \ + if (YYID (N)) \ + { \ + (Current).first_line = YYRHSLOC (Rhs, 1).first_line; \ + (Current).first_column = YYRHSLOC (Rhs, 1).first_column; \ + (Current).last_line = YYRHSLOC (Rhs, N).last_line; \ + (Current).last_column = YYRHSLOC (Rhs, N).last_column; \ + } \ + else \ + { \ + (Current).first_line = (Current).last_line = \ + YYRHSLOC (Rhs, 0).last_line; \ + (Current).first_column = (Current).last_column = \ + YYRHSLOC (Rhs, 0).last_column; \ + } \ + while (YYID (0)) +#endif + +#define YYRHSLOC(Rhs, K) ((Rhs)[K]) + + +/* YY_LOCATION_PRINT -- Print the location on the stream. + This macro was not mandated originally: define only if we know + we won't break user code: when these are the locations we know. */ + #ifndef YY_LOCATION_PRINT -# define YY_LOCATION_PRINT(File, Loc) ((void) 0) +# if defined PROMELA_LTYPE_IS_TRIVIAL && PROMELA_LTYPE_IS_TRIVIAL + +/* Print *YYLOCP on YYO. Private, do not rely on its existence. */ + +__attribute__((__unused__)) +#if (defined __STDC__ || defined __C99__FUNC__ \ + || defined __cplusplus || defined _MSC_VER) +static unsigned +yy_location_print_ (FILE *yyo, YYLTYPE const * const yylocp) +#else +static unsigned +yy_location_print_ (yyo, yylocp) + FILE *yyo; + YYLTYPE const * const yylocp; +#endif +{ + unsigned res = 0; + int end_col = 0 != yylocp->last_column ? yylocp->last_column - 1 : 0; + if (0 <= yylocp->first_line) + { + res += fprintf (yyo, "%d", yylocp->first_line); + if (0 <= yylocp->first_column) + res += fprintf (yyo, ".%d", yylocp->first_column); + } + if (0 <= yylocp->last_line) + { + if (yylocp->first_line < yylocp->last_line) + { + res += fprintf (yyo, "-%d", yylocp->last_line); + if (0 <= end_col) + res += fprintf (yyo, ".%d", end_col); + } + else if (0 <= end_col && yylocp->first_column < end_col) + res += fprintf (yyo, "-%d", end_col); + } + return res; + } + +# define YY_LOCATION_PRINT(File, Loc) \ + yy_location_print_ (File, &(Loc)) + +# else +# define YY_LOCATION_PRINT(File, Loc) ((void) 0) +# endif #endif /* YYLEX -- calling `yylex' with the right arguments. */ #ifdef YYLEX_PARAM -# define YYLEX yylex (&yylval, YYLEX_PARAM) +# define YYLEX yylex (&yylval, &yylloc, YYLEX_PARAM) #else -# define YYLEX yylex (&yylval, scanner) +# define YYLEX yylex (&yylval, &yylloc, scanner) #endif /* Enable debugging if requested. */ @@ -905,7 +995,7 @@ do { \ { \ YYFPRINTF (stderr, "%s ", Title); \ yy_symbol_print (stderr, \ - Type, Value, ctx, scanner); \ + Type, Value, Location, ctx, scanner); \ YYFPRINTF (stderr, "\n"); \ } \ } while (YYID (0)) @@ -919,13 +1009,14 @@ do { \ #if (defined __STDC__ || defined __C99__FUNC__ \ || defined __cplusplus || defined _MSC_VER) static void -yy_symbol_value_print (FILE *yyoutput, int yytype, YYSTYPE const * const yyvaluep, uscxml::PromelaParser* ctx, void * scanner) +yy_symbol_value_print (FILE *yyoutput, int yytype, YYSTYPE const * const yyvaluep, YYLTYPE const * const yylocationp, uscxml::PromelaParser* ctx, void * scanner) #else static void -yy_symbol_value_print (yyoutput, yytype, yyvaluep, ctx, scanner) +yy_symbol_value_print (yyoutput, yytype, yyvaluep, yylocationp, ctx, scanner) FILE *yyoutput; int yytype; YYSTYPE const * const yyvaluep; + YYLTYPE const * const yylocationp; uscxml::PromelaParser* ctx; void * scanner; #endif @@ -934,6 +1025,7 @@ yy_symbol_value_print (yyoutput, yytype, yyvaluep, ctx, scanner) YYUSE (yyo); if (!yyvaluep) return; + YYUSE (yylocationp); YYUSE (ctx); YYUSE (scanner); # ifdef YYPRINT @@ -953,13 +1045,14 @@ yy_symbol_value_print (yyoutput, yytype, yyvaluep, ctx, scanner) #if (defined __STDC__ || defined __C99__FUNC__ \ || defined __cplusplus || defined _MSC_VER) static void -yy_symbol_print (FILE *yyoutput, int yytype, YYSTYPE const * const yyvaluep, uscxml::PromelaParser* ctx, void * scanner) +yy_symbol_print (FILE *yyoutput, int yytype, YYSTYPE const * const yyvaluep, YYLTYPE const * const yylocationp, uscxml::PromelaParser* ctx, void * scanner) #else static void -yy_symbol_print (yyoutput, yytype, yyvaluep, ctx, scanner) +yy_symbol_print (yyoutput, yytype, yyvaluep, yylocationp, ctx, scanner) FILE *yyoutput; int yytype; YYSTYPE const * const yyvaluep; + YYLTYPE const * const yylocationp; uscxml::PromelaParser* ctx; void * scanner; #endif @@ -969,7 +1062,9 @@ yy_symbol_print (yyoutput, yytype, yyvaluep, ctx, scanner) else YYFPRINTF (yyoutput, "nterm %s (", yytname[yytype]); - yy_symbol_value_print (yyoutput, yytype, yyvaluep, ctx, scanner); + YY_LOCATION_PRINT (yyoutput, *yylocationp); + YYFPRINTF (yyoutput, ": "); + yy_symbol_value_print (yyoutput, yytype, yyvaluep, yylocationp, ctx, scanner); YYFPRINTF (yyoutput, ")"); } @@ -1012,11 +1107,12 @@ do { \ #if (defined __STDC__ || defined __C99__FUNC__ \ || defined __cplusplus || defined _MSC_VER) static void -yy_reduce_print (YYSTYPE *yyvsp, int yyrule, uscxml::PromelaParser* ctx, void * scanner) +yy_reduce_print (YYSTYPE *yyvsp, YYLTYPE *yylsp, int yyrule, uscxml::PromelaParser* ctx, void * scanner) #else static void -yy_reduce_print (yyvsp, yyrule, ctx, scanner) +yy_reduce_print (yyvsp, yylsp, yyrule, ctx, scanner) YYSTYPE *yyvsp; + YYLTYPE *yylsp; int yyrule; uscxml::PromelaParser* ctx; void * scanner; @@ -1033,7 +1129,7 @@ yy_reduce_print (yyvsp, yyrule, ctx, scanner) YYFPRINTF (stderr, " $%d = ", yyi + 1); yy_symbol_print (stderr, yyrhs[yyprhs[yyrule] + yyi], &(yyvsp[(yyi + 1) - (yynrhs)]) - , ctx, scanner); + , &(yylsp[(yyi + 1) - (yynrhs)]) , ctx, scanner); YYFPRINTF (stderr, "\n"); } } @@ -1041,7 +1137,7 @@ yy_reduce_print (yyvsp, yyrule, ctx, scanner) # define YY_REDUCE_PRINT(Rule) \ do { \ if (yydebug) \ - yy_reduce_print (yyvsp, Rule, ctx, scanner); \ + yy_reduce_print (yyvsp, yylsp, Rule, ctx, scanner); \ } while (YYID (0)) /* Nonzero means print parse trace. It is left uninitialized so that @@ -1321,18 +1417,20 @@ yysyntax_error (YYSIZE_T *yymsg_alloc, char **yymsg, #if (defined __STDC__ || defined __C99__FUNC__ \ || defined __cplusplus || defined _MSC_VER) static void -yydestruct (const char *yymsg, int yytype, YYSTYPE *yyvaluep, uscxml::PromelaParser* ctx, void * scanner) +yydestruct (const char *yymsg, int yytype, YYSTYPE *yyvaluep, YYLTYPE *yylocationp, uscxml::PromelaParser* ctx, void * scanner) #else static void -yydestruct (yymsg, yytype, yyvaluep, ctx, scanner) +yydestruct (yymsg, yytype, yyvaluep, yylocationp, ctx, scanner) const char *yymsg; int yytype; YYSTYPE *yyvaluep; + YYLTYPE *yylocationp; uscxml::PromelaParser* ctx; void * scanner; #endif { YYUSE (yyvaluep); + YYUSE (yylocationp); YYUSE (ctx); YYUSE (scanner); @@ -1391,6 +1489,11 @@ int yychar; static YYSTYPE yyval_default; # define YY_INITIAL_VALUE(Value) = Value #endif +static YYLTYPE yyloc_default +# if defined PROMELA_LTYPE_IS_TRIVIAL && PROMELA_LTYPE_IS_TRIVIAL + = { 1, 1, 1, 1 } +# endif +; #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN # define YY_IGNORE_MAYBE_UNINITIALIZED_END @@ -1402,6 +1505,10 @@ static YYSTYPE yyval_default; /* The semantic value of the lookahead symbol. */ YYSTYPE yylval YY_INITIAL_VALUE(yyval_default); +/* Location data for the lookahead symbol. */ +YYLTYPE yylloc = yyloc_default; + + /* Number of syntax errors so far. */ int yynerrs; @@ -1412,6 +1519,7 @@ YYSTYPE yylval YY_INITIAL_VALUE(yyval_default); /* The stacks and their tools: `yyss': related to states. `yyvs': related to semantic values. + `yyls': related to locations. Refer to the stacks through separate pointers, to allow yyoverflow to reallocate them elsewhere. */ @@ -1426,6 +1534,14 @@ YYSTYPE yylval YY_INITIAL_VALUE(yyval_default); YYSTYPE *yyvs; YYSTYPE *yyvsp; + /* The location stack. */ + YYLTYPE yylsa[YYINITDEPTH]; + YYLTYPE *yyls; + YYLTYPE *yylsp; + + /* The locations where the error started and ended. */ + YYLTYPE yyerror_range[3]; + YYSIZE_T yystacksize; int yyn; @@ -1435,6 +1551,7 @@ YYSTYPE yylval YY_INITIAL_VALUE(yyval_default); /* The variables used to return semantic value and location from the action routines. */ YYSTYPE yyval; + YYLTYPE yyloc; #if YYERROR_VERBOSE /* Buffer for error messages, and its allocated size. */ @@ -1443,7 +1560,7 @@ YYSTYPE yylval YY_INITIAL_VALUE(yyval_default); YYSIZE_T yymsg_alloc = sizeof yymsgbuf; #endif -#define YYPOPSTACK(N) (yyvsp -= (N), yyssp -= (N)) +#define YYPOPSTACK(N) (yyvsp -= (N), yyssp -= (N), yylsp -= (N)) /* The number of symbols on the RHS of the reduced rule. Keep to zero when no symbol should be popped. */ @@ -1451,6 +1568,7 @@ YYSTYPE yylval YY_INITIAL_VALUE(yyval_default); yyssp = yyss = yyssa; yyvsp = yyvs = yyvsa; + yylsp = yyls = yylsa; yystacksize = YYINITDEPTH; YYDPRINTF ((stderr, "Starting parse\n")); @@ -1459,6 +1577,7 @@ YYSTYPE yylval YY_INITIAL_VALUE(yyval_default); yyerrstatus = 0; yynerrs = 0; yychar = YYEMPTY; /* Cause a token to be read. */ + yylsp[0] = yylloc; goto yysetstate; /*------------------------------------------------------------. @@ -1484,6 +1603,7 @@ YYSTYPE yylval YY_INITIAL_VALUE(yyval_default); memory. */ YYSTYPE *yyvs1 = yyvs; yytype_int16 *yyss1 = yyss; + YYLTYPE *yyls1 = yyls; /* Each stack pointer address is followed by the size of the data in use in that stack, in bytes. This used to be a @@ -1492,8 +1612,10 @@ YYSTYPE yylval YY_INITIAL_VALUE(yyval_default); yyoverflow (YY_("memory exhausted"), &yyss1, yysize * sizeof (*yyssp), &yyvs1, yysize * sizeof (*yyvsp), + &yyls1, yysize * sizeof (*yylsp), &yystacksize); + yyls = yyls1; yyss = yyss1; yyvs = yyvs1; } @@ -1516,6 +1638,7 @@ YYSTYPE yylval YY_INITIAL_VALUE(yyval_default); goto yyexhaustedlab; YYSTACK_RELOCATE (yyss_alloc, yyss); YYSTACK_RELOCATE (yyvs_alloc, yyvs); + YYSTACK_RELOCATE (yyls_alloc, yyls); # undef YYSTACK_RELOCATE if (yyss1 != yyssa) YYSTACK_FREE (yyss1); @@ -1525,6 +1648,7 @@ YYSTYPE yylval YY_INITIAL_VALUE(yyval_default); yyssp = yyss + yysize - 1; yyvsp = yyvs + yysize - 1; + yylsp = yyls + yysize - 1; YYDPRINTF ((stderr, "Stack size increased to %lu\n", (unsigned long int) yystacksize)); @@ -1602,7 +1726,7 @@ yybackup: YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN *++yyvsp = yylval; YY_IGNORE_MAYBE_UNINITIALIZED_END - + *++yylsp = yylloc; goto yynewstate; @@ -1633,13 +1757,14 @@ yyreduce: GCC warning that YYVAL may be used uninitialized. */ yyval = yyvsp[1-yylen]; - + /* Default location. */ + YYLLOC_DEFAULT (yyloc, (yylsp - yylen), yylen); YY_REDUCE_PRINT (yyn); switch (yyn) { case 2: /* Line 1787 of yacc.c */ -#line 84 "promela.ypp" +#line 85 "promela.ypp" { ctx->ast = (yyvsp[(1) - (1)].node); ctx->type = PromelaParser::PROMELA_DECL; @@ -1648,7 +1773,7 @@ yyreduce: case 3: /* Line 1787 of yacc.c */ -#line 88 "promela.ypp" +#line 89 "promela.ypp" { ctx->ast = (yyvsp[(1) - (1)].node); ctx->type = PromelaParser::PROMELA_EXPR; @@ -1657,7 +1782,7 @@ yyreduce: case 4: /* Line 1787 of yacc.c */ -#line 92 "promela.ypp" +#line 93 "promela.ypp" { ctx->ast = (yyvsp[(1) - (1)].node); ctx->type = PromelaParser::PROMELA_STMNT; @@ -1666,25 +1791,25 @@ yyreduce: case 5: /* Line 1787 of yacc.c */ -#line 98 "promela.ypp" +#line 99 "promela.ypp" { (yyval.node) = (yyvsp[(1) - (1)].node); } break; case 6: /* Line 1787 of yacc.c */ -#line 101 "promela.ypp" - { (yyval.node) = ctx->value(PML_NAME, (yyvsp[(1) - (1)].value)); free((yyvsp[(1) - (1)].value)); } +#line 102 "promela.ypp" + { (yyval.node) = ctx->value(PML_NAME, (void*)&((yylsp[(1) - (1)])), (yyvsp[(1) - (1)].value)); free((yyvsp[(1) - (1)].value)); } break; case 7: /* Line 1787 of yacc.c */ -#line 102 "promela.ypp" - { (yyval.node) = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, (yyvsp[(1) - (4)].value)), (yyvsp[(3) - (4)].node)); free((yyvsp[(1) - (4)].value)); } +#line 103 "promela.ypp" + { (yyval.node) = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, (void*)&((yylsp[(1) - (4)])), (yyvsp[(1) - (4)].value)), (yyvsp[(3) - (4)].node)); free((yyvsp[(1) - (4)].value)); } break; case 8: /* Line 1787 of yacc.c */ -#line 106 "promela.ypp" +#line 107 "promela.ypp" { if ((yyvsp[(2) - (2)].node) != NULL) { if ((yyvsp[(2) - (2)].node)->type == PML_CMPND) { @@ -1701,237 +1826,237 @@ yyreduce: case 9: /* Line 1787 of yacc.c */ -#line 120 "promela.ypp" +#line 121 "promela.ypp" { (yyval.node) = NULL; } break; case 10: /* Line 1787 of yacc.c */ -#line 121 "promela.ypp" +#line 122 "promela.ypp" { (yyval.node) = (yyvsp[(2) - (2)].node); } break; case 11: /* Line 1787 of yacc.c */ -#line 131 "promela.ypp" +#line 132 "promela.ypp" { (yyval.node) = (yyvsp[(2) - (3)].node); } break; case 12: /* Line 1787 of yacc.c */ -#line 132 "promela.ypp" +#line 133 "promela.ypp" { (yyval.node) = ctx->node(PML_PLUS, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 13: /* Line 1787 of yacc.c */ -#line 133 "promela.ypp" +#line 134 "promela.ypp" { (yyval.node) = ctx->node(PML_MINUS, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 14: /* Line 1787 of yacc.c */ -#line 134 "promela.ypp" +#line 135 "promela.ypp" { (yyval.node) = ctx->node(PML_TIMES, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 15: /* Line 1787 of yacc.c */ -#line 135 "promela.ypp" +#line 136 "promela.ypp" { (yyval.node) = ctx->node(PML_DIVIDE, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 16: /* Line 1787 of yacc.c */ -#line 136 "promela.ypp" +#line 137 "promela.ypp" { (yyval.node) = ctx->node(PML_MODULO, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 17: /* Line 1787 of yacc.c */ -#line 137 "promela.ypp" +#line 138 "promela.ypp" { (yyval.node) = ctx->node(PML_BITAND, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 18: /* Line 1787 of yacc.c */ -#line 138 "promela.ypp" +#line 139 "promela.ypp" { (yyval.node) = ctx->node(PML_BITXOR, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 19: /* Line 1787 of yacc.c */ -#line 139 "promela.ypp" +#line 140 "promela.ypp" { (yyval.node) = ctx->node(PML_BITOR, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 20: /* Line 1787 of yacc.c */ -#line 140 "promela.ypp" +#line 141 "promela.ypp" { (yyval.node) = ctx->node(PML_GT, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 21: /* Line 1787 of yacc.c */ -#line 141 "promela.ypp" +#line 142 "promela.ypp" { (yyval.node) = ctx->node(PML_LT, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 22: /* Line 1787 of yacc.c */ -#line 142 "promela.ypp" +#line 143 "promela.ypp" { (yyval.node) = ctx->node(PML_GE, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 23: /* Line 1787 of yacc.c */ -#line 143 "promela.ypp" +#line 144 "promela.ypp" { (yyval.node) = ctx->node(PML_LE, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 24: /* Line 1787 of yacc.c */ -#line 144 "promela.ypp" +#line 145 "promela.ypp" { (yyval.node) = ctx->node(PML_EQ, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 25: /* Line 1787 of yacc.c */ -#line 145 "promela.ypp" +#line 146 "promela.ypp" { (yyval.node) = ctx->node(PML_NE, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 26: /* Line 1787 of yacc.c */ -#line 146 "promela.ypp" +#line 147 "promela.ypp" { (yyval.node) = ctx->node(PML_AND, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 27: /* Line 1787 of yacc.c */ -#line 147 "promela.ypp" +#line 148 "promela.ypp" { (yyval.node) = ctx->node(PML_OR, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 28: /* Line 1787 of yacc.c */ -#line 148 "promela.ypp" +#line 149 "promela.ypp" { (yyval.node) = ctx->node(PML_LSHIFT, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 29: /* Line 1787 of yacc.c */ -#line 149 "promela.ypp" +#line 150 "promela.ypp" { (yyval.node) = ctx->node(PML_RSHIFT, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 30: /* Line 1787 of yacc.c */ -#line 150 "promela.ypp" +#line 151 "promela.ypp" { (yyval.node) = ctx->node(PML_NEG, 1, (yyvsp[(2) - (2)].node)); } break; case 31: /* Line 1787 of yacc.c */ -#line 151 "promela.ypp" +#line 152 "promela.ypp" { (yyval.node) = ctx->node(PML_MINUS, 1, (yyvsp[(2) - (2)].node)); } break; case 32: /* Line 1787 of yacc.c */ -#line 153 "promela.ypp" +#line 154 "promela.ypp" { (yyval.node) = ctx->node(PML_LEN, 1, (yyvsp[(3) - (4)].node)); } break; case 33: /* Line 1787 of yacc.c */ -#line 154 "promela.ypp" +#line 155 "promela.ypp" { (yyval.node) = (yyvsp[(1) - (1)].node); } break; case 34: /* Line 1787 of yacc.c */ -#line 155 "promela.ypp" - { (yyval.node) = ctx->value(PML_CONST, (yyvsp[(1) - (1)].value)); free((yyvsp[(1) - (1)].value)); } +#line 156 "promela.ypp" + { (yyval.node) = ctx->value(PML_CONST, (void*)&((yylsp[(1) - (1)])), (yyvsp[(1) - (1)].value)); free((yyvsp[(1) - (1)].value)); } break; case 35: /* Line 1787 of yacc.c */ -#line 156 "promela.ypp" +#line 157 "promela.ypp" { /* Non standard promela for string literals */ - (yyval.node) = ctx->value(PML_STRING, (yyvsp[(1) - (1)].value)); free((yyvsp[(1) - (1)].value)); } + (yyval.node) = ctx->value(PML_STRING, (void*)&((yylsp[(1) - (1)])), (yyvsp[(1) - (1)].value)); free((yyvsp[(1) - (1)].value)); } break; case 36: /* Line 1787 of yacc.c */ -#line 162 "promela.ypp" +#line 163 "promela.ypp" { (yyval.node) = ctx->node(PML_SHOW, 0); } break; case 37: /* Line 1787 of yacc.c */ -#line 163 "promela.ypp" +#line 164 "promela.ypp" { (yyval.node) = ctx->node(PML_HIDDEN, 0); } break; case 38: /* Line 1787 of yacc.c */ -#line 164 "promela.ypp" +#line 165 "promela.ypp" { (yyval.node) = ctx->node(PML_SHOW, 0); } break; case 39: /* Line 1787 of yacc.c */ -#line 165 "promela.ypp" +#line 166 "promela.ypp" { (yyval.node) = ctx->node(PML_ISLOCAL, 0); } break; case 40: /* Line 1787 of yacc.c */ -#line 168 "promela.ypp" - { (yyval.node) = ctx->node(PML_DECL, 3, (yyvsp[(1) - (3)].node), ctx->value(PML_TYPE, (yyvsp[(2) - (3)].value)), (yyvsp[(3) - (3)].node)); free((yyvsp[(2) - (3)].value)); } +#line 169 "promela.ypp" + { (yyval.node) = ctx->node(PML_DECL, 3, (yyvsp[(1) - (3)].node), ctx->value(PML_TYPE, (void*)&((yylsp[(2) - (3)])), (yyvsp[(2) - (3)].value)), (yyvsp[(3) - (3)].node)); free((yyvsp[(2) - (3)].value)); } break; case 41: /* Line 1787 of yacc.c */ -#line 169 "promela.ypp" +#line 170 "promela.ypp" { (yyval.node) = ctx->node(PML_UNAME, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 42: /* Line 1787 of yacc.c */ -#line 170 "promela.ypp" - { (yyval.node) = ctx->node(PML_DECL, 3, (yyvsp[(1) - (6)].node), ctx->value(PML_TYPE, (yyvsp[(2) - (6)].value)), (yyvsp[(5) - (6)].node)); free((yyvsp[(2) - (6)].value)); } +#line 171 "promela.ypp" + { (yyval.node) = ctx->node(PML_DECL, 3, (yyvsp[(1) - (6)].node), ctx->value(PML_TYPE, (void*)&((yylsp[(2) - (6)])), (yyvsp[(2) - (6)].value)), (yyvsp[(5) - (6)].node)); free((yyvsp[(2) - (6)].value)); } break; case 43: /* Line 1787 of yacc.c */ -#line 171 "promela.ypp" +#line 172 "promela.ypp" { (yyval.node) = (yyvsp[(2) - (2)].node); } break; case 44: /* Line 1787 of yacc.c */ -#line 174 "promela.ypp" - { (yyval.node) = ctx->node(PML_TYPEDEF, 2, ctx->value(PML_NAME, (yyvsp[(2) - (5)].value)), (yyvsp[(4) - (5)].node)); } +#line 175 "promela.ypp" + { (yyval.node) = ctx->node(PML_TYPEDEF, 2, ctx->value(PML_NAME, (void*)&((yylsp[(2) - (5)])), (yyvsp[(2) - (5)].value)), (yyvsp[(4) - (5)].node)); } break; case 45: /* Line 1787 of yacc.c */ -#line 177 "promela.ypp" +#line 178 "promela.ypp" { (yyval.node) = (yyvsp[(1) - (1)].node); } break; case 46: /* Line 1787 of yacc.c */ -#line 178 "promela.ypp" +#line 179 "promela.ypp" { (yyval.node) = (yyvsp[(1) - (2)].node); } break; case 47: /* Line 1787 of yacc.c */ -#line 179 "promela.ypp" +#line 180 "promela.ypp" { (yyval.node) = ctx->node(PML_DECLLIST, 1, (yyvsp[(1) - (3)].node)); if((yyvsp[(3) - (3)].node)->type == PML_DECLLIST) { @@ -1944,109 +2069,109 @@ yyreduce: case 48: /* Line 1787 of yacc.c */ -#line 189 "promela.ypp" +#line 190 "promela.ypp" { (yyval.node) = ctx->node(PML_VARLIST, 1, (yyvsp[(1) - (1)].node)); } break; case 49: /* Line 1787 of yacc.c */ -#line 190 "promela.ypp" +#line 191 "promela.ypp" { (yyval.node) = ctx->node(PML_VARLIST, 1, (yyvsp[(1) - (3)].node)); (yyval.node)->merge((yyvsp[(3) - (3)].node)); delete (yyvsp[(3) - (3)].node); } break; case 50: /* Line 1787 of yacc.c */ -#line 193 "promela.ypp" +#line 194 "promela.ypp" { (yyval.node) = (yyvsp[(1) - (1)].node); } break; case 51: /* Line 1787 of yacc.c */ -#line 194 "promela.ypp" +#line 195 "promela.ypp" { (yyval.node) = ctx->node(PML_ASGN, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 52: /* Line 1787 of yacc.c */ -#line 197 "promela.ypp" - { (yyval.node) = ctx->value(PML_NAME, (yyvsp[(1) - (1)].value)); free((yyvsp[(1) - (1)].value)); } +#line 198 "promela.ypp" + { (yyval.node) = ctx->value(PML_NAME, (void*)&((yylsp[(1) - (1)])), (yyvsp[(1) - (1)].value)); free((yyvsp[(1) - (1)].value)); } break; case 53: /* Line 1787 of yacc.c */ -#line 198 "promela.ypp" - { (yyval.node) = ctx->node(PML_COLON, 2, ctx->value(PML_NAME, (yyvsp[(1) - (3)].value)), ctx->value(PML_CONST, (yyvsp[(3) - (3)].value))); free((yyvsp[(1) - (3)].value)); free((yyvsp[(3) - (3)].value)); } +#line 199 "promela.ypp" + { (yyval.node) = ctx->node(PML_COLON, 2, ctx->value(PML_NAME, (void*)&((yylsp[(1) - (3)])), (yyvsp[(1) - (3)].value)), ctx->value(PML_CONST, (void*)&((yylsp[(3) - (3)])), (yyvsp[(3) - (3)].value))); free((yyvsp[(1) - (3)].value)); free((yyvsp[(3) - (3)].value)); } break; case 54: /* Line 1787 of yacc.c */ -#line 199 "promela.ypp" - { (yyval.node) = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, (yyvsp[(1) - (4)].value)), (yyvsp[(3) - (4)].node)); free((yyvsp[(1) - (4)].value)); } +#line 200 "promela.ypp" + { (yyval.node) = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, (void*)&((yylsp[(1) - (4)])), (yyvsp[(1) - (4)].value)), (yyvsp[(3) - (4)].node)); free((yyvsp[(1) - (4)].value)); } break; case 55: /* Line 1787 of yacc.c */ -#line 202 "promela.ypp" - { (yyval.node) = ctx->value(PML_CONST, (yyvsp[(1) - (1)].value)); free((yyvsp[(1) - (1)].value)); } +#line 203 "promela.ypp" + { (yyval.node) = ctx->value(PML_CONST, (void*)&((yylsp[(1) - (1)])), (yyvsp[(1) - (1)].value)); free((yyvsp[(1) - (1)].value)); } break; case 56: /* Line 1787 of yacc.c */ -#line 203 "promela.ypp" +#line 204 "promela.ypp" { (yyval.node) = ctx->node(PML_MINUS, 1, (yyvsp[(2) - (2)].node)); } break; case 57: /* Line 1787 of yacc.c */ -#line 204 "promela.ypp" +#line 205 "promela.ypp" { (yyval.node) = (yyvsp[(2) - (3)].node); } break; case 58: /* Line 1787 of yacc.c */ -#line 205 "promela.ypp" +#line 206 "promela.ypp" { (yyval.node) = ctx->node(PML_PLUS, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 59: /* Line 1787 of yacc.c */ -#line 206 "promela.ypp" +#line 207 "promela.ypp" { (yyval.node) = ctx->node(PML_MINUS, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 60: /* Line 1787 of yacc.c */ -#line 207 "promela.ypp" +#line 208 "promela.ypp" { (yyval.node) = ctx->node(PML_TIMES, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 61: /* Line 1787 of yacc.c */ -#line 208 "promela.ypp" +#line 209 "promela.ypp" { (yyval.node) = ctx->node(PML_DIVIDE, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 62: /* Line 1787 of yacc.c */ -#line 209 "promela.ypp" +#line 210 "promela.ypp" { (yyval.node) = ctx->node(PML_MODULO, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 63: /* Line 1787 of yacc.c */ -#line 212 "promela.ypp" - { (yyval.node) = ctx->value(PML_NAME, (yyvsp[(1) - (1)].value)); free((yyvsp[(1) - (1)].value)); } +#line 213 "promela.ypp" + { (yyval.node) = ctx->value(PML_NAME, (void*)&((yylsp[(1) - (1)])), (yyvsp[(1) - (1)].value)); free((yyvsp[(1) - (1)].value)); } break; case 64: /* Line 1787 of yacc.c */ -#line 213 "promela.ypp" +#line 214 "promela.ypp" { if ((yyvsp[(1) - (2)].node)->type == PML_NAME) { (yyval.node) = ctx->node(PML_NAMELIST, 1, (yyvsp[(1) - (2)].node)); - (yyval.node)->push(ctx->value(PML_NAME, (yyvsp[(2) - (2)].value))); + (yyval.node)->push(ctx->value(PML_NAME, (void*)&((yylsp[(2) - (2)])), (yyvsp[(2) - (2)].value))); } else { - (yyvsp[(1) - (2)].node)->push(ctx->value(PML_NAME, (yyvsp[(2) - (2)].value))); + (yyvsp[(1) - (2)].node)->push(ctx->value(PML_NAME, (void*)&((yylsp[(2) - (2)])), (yyvsp[(2) - (2)].value))); } free((yyvsp[(2) - (2)].value)); } @@ -2054,109 +2179,109 @@ yyreduce: case 65: /* Line 1787 of yacc.c */ -#line 222 "promela.ypp" +#line 223 "promela.ypp" { (yyval.node) = (yyvsp[(1) - (2)].node); } break; case 66: /* Line 1787 of yacc.c */ -#line 225 "promela.ypp" +#line 226 "promela.ypp" { (yyval.node) = (yyvsp[(1) - (1)].node); } break; case 67: /* Line 1787 of yacc.c */ -#line 226 "promela.ypp" +#line 227 "promela.ypp" { (yyval.node) = (yyvsp[(1) - (2)].node); } break; case 68: /* Line 1787 of yacc.c */ -#line 227 "promela.ypp" +#line 228 "promela.ypp" { (yyval.node) = ctx->node(PML_STMNT, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 69: /* Line 1787 of yacc.c */ -#line 230 "promela.ypp" +#line 231 "promela.ypp" { (yyval.node) = (yyvsp[(1) - (1)].node); } break; case 70: /* Line 1787 of yacc.c */ -#line 233 "promela.ypp" +#line 234 "promela.ypp" { (yyval.node) = ctx->node(PML_ASGN, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; case 71: /* Line 1787 of yacc.c */ -#line 234 "promela.ypp" +#line 235 "promela.ypp" { (yyval.node) = ctx->node(PML_INCR, 1, (yyvsp[(1) - (2)].node)); } break; case 72: /* Line 1787 of yacc.c */ -#line 235 "promela.ypp" +#line 236 "promela.ypp" { (yyval.node) = ctx->node(PML_DECR, 1, (yyvsp[(1) - (2)].node)); } break; case 73: /* Line 1787 of yacc.c */ -#line 236 "promela.ypp" - { (yyval.node) = ctx->node(PML_PRINT, 2, ctx->value(PML_STRING, (yyvsp[(3) - (5)].value)), (yyvsp[(4) - (5)].node)); free((yyvsp[(3) - (5)].value)); } +#line 237 "promela.ypp" + { (yyval.node) = ctx->node(PML_PRINT, 2, ctx->value(PML_STRING, (void*)&((yylsp[(3) - (5)])), (yyvsp[(3) - (5)].value)), (yyvsp[(4) - (5)].node)); free((yyvsp[(3) - (5)].value)); } break; case 74: /* Line 1787 of yacc.c */ -#line 237 "promela.ypp" +#line 238 "promela.ypp" { (yyval.node) = ctx->node(PML_PRINT, 1, (yyvsp[(3) - (4)].node)); } break; case 75: /* Line 1787 of yacc.c */ -#line 238 "promela.ypp" - { (yyval.node) = ctx->node(PML_PRINT, 1, ctx->value(PML_CONST, (yyvsp[(3) - (4)].value))); free((yyvsp[(3) - (4)].value)); } +#line 239 "promela.ypp" + { (yyval.node) = ctx->node(PML_PRINT, 1, ctx->value(PML_CONST, (void*)&((yylsp[(3) - (4)])), (yyvsp[(3) - (4)].value))); free((yyvsp[(3) - (4)].value)); } break; case 76: /* Line 1787 of yacc.c */ -#line 239 "promela.ypp" +#line 240 "promela.ypp" { (yyval.node) = ctx->node(PML_ASSERT, 1, (yyvsp[(2) - (2)].node)); } break; case 77: /* Line 1787 of yacc.c */ -#line 240 "promela.ypp" +#line 241 "promela.ypp" { (yyval.node) = (yyvsp[(1) - (1)].node); } break; case 78: /* Line 1787 of yacc.c */ -#line 243 "promela.ypp" - { (yyval.node) = ctx->value(0, ""); } +#line 244 "promela.ypp" + { (yyval.node) = ctx->value(0, NULL, ""); } break; case 79: /* Line 1787 of yacc.c */ -#line 244 "promela.ypp" +#line 245 "promela.ypp" { (yyval.node) = (yyvsp[(2) - (2)].node); } break; case 80: /* Line 1787 of yacc.c */ -#line 247 "promela.ypp" +#line 248 "promela.ypp" { (yyval.node) = (yyvsp[(1) - (1)].node); } break; case 81: /* Line 1787 of yacc.c */ -#line 248 "promela.ypp" +#line 249 "promela.ypp" { (yyval.node) = ctx->node(0, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); } break; /* Line 1787 of yacc.c */ -#line 2160 "promela.tab.cpp" +#line 2285 "promela.tab.cpp" default: break; } /* User semantic actions sometimes alter yychar, and that requires @@ -2177,6 +2302,7 @@ yyreduce: YY_STACK_PRINT (yyss, yyssp); *++yyvsp = yyval; + *++yylsp = yyloc; /* Now `shift' the result of the reduction. Determine what state that goes to, based on the state we popped back to and the rule @@ -2206,7 +2332,7 @@ yyerrlab: { ++yynerrs; #if ! YYERROR_VERBOSE - yyerror (ctx, scanner, YY_("syntax error")); + yyerror (&yylloc, ctx, scanner, YY_("syntax error")); #else # define YYSYNTAX_ERROR yysyntax_error (&yymsg_alloc, &yymsg, \ yyssp, yytoken) @@ -2233,7 +2359,7 @@ yyerrlab: yymsgp = yymsg; } } - yyerror (ctx, scanner, yymsgp); + yyerror (&yylloc, ctx, scanner, yymsgp); if (yysyntax_error_status == 2) goto yyexhaustedlab; } @@ -2241,7 +2367,7 @@ yyerrlab: #endif } - + yyerror_range[1] = yylloc; if (yyerrstatus == 3) { @@ -2257,7 +2383,7 @@ yyerrlab: else { yydestruct ("Error: discarding", - yytoken, &yylval, ctx, scanner); + yytoken, &yylval, &yylloc, ctx, scanner); yychar = YYEMPTY; } } @@ -2278,6 +2404,7 @@ yyerrorlab: if (/*CONSTCOND*/ 0) goto yyerrorlab; + yyerror_range[1] = yylsp[1-yylen]; /* Do not reclaim the symbols of the rule which action triggered this YYERROR. */ YYPOPSTACK (yylen); @@ -2311,9 +2438,9 @@ yyerrlab1: if (yyssp == yyss) YYABORT; - + yyerror_range[1] = *yylsp; yydestruct ("Error: popping", - yystos[yystate], yyvsp, ctx, scanner); + yystos[yystate], yyvsp, yylsp, ctx, scanner); YYPOPSTACK (1); yystate = *yyssp; YY_STACK_PRINT (yyss, yyssp); @@ -2323,6 +2450,11 @@ yyerrlab1: *++yyvsp = yylval; YY_IGNORE_MAYBE_UNINITIALIZED_END + yyerror_range[2] = yylloc; + /* Using YYLLOC is tempting, but would change the location of + the lookahead. YYLOC is available though. */ + YYLLOC_DEFAULT (yyloc, yyerror_range, 2); + *++yylsp = yyloc; /* Shift the error token. */ YY_SYMBOL_PRINT ("Shifting", yystos[yyn], yyvsp, yylsp); @@ -2350,7 +2482,7 @@ yyabortlab: | yyexhaustedlab -- memory exhaustion comes here. | `-------------------------------------------------*/ yyexhaustedlab: - yyerror (ctx, scanner, YY_("memory exhausted")); + yyerror (&yylloc, ctx, scanner, YY_("memory exhausted")); yyresult = 2; /* Fall through. */ #endif @@ -2362,7 +2494,7 @@ yyreturn: user semantic actions for why this is necessary. */ yytoken = YYTRANSLATE (yychar); yydestruct ("Cleanup: discarding lookahead", - yytoken, &yylval, ctx, scanner); + yytoken, &yylval, &yylloc, ctx, scanner); } /* Do not reclaim the symbols of the rule which action triggered this YYABORT or YYACCEPT. */ @@ -2371,7 +2503,7 @@ yyreturn: while (yyssp != yyss) { yydestruct ("Cleanup: popping", - yystos[*yyssp], yyvsp, ctx, scanner); + yystos[*yyssp], yyvsp, yylsp, ctx, scanner); YYPOPSTACK (1); } #ifndef yyoverflow @@ -2388,6 +2520,6 @@ yyreturn: /* Line 2050 of yacc.c */ -#line 252 "promela.ypp" +#line 253 "promela.ypp" diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.tab.hpp b/src/uscxml/plugins/datamodel/promela/parser/promela.tab.hpp index e6eb572..a48031a 100644 --- a/src/uscxml/plugins/datamodel/promela/parser/promela.tab.hpp +++ b/src/uscxml/plugins/datamodel/promela/parser/promela.tab.hpp @@ -135,7 +135,7 @@ extern int promela_debug; typedef union PROMELA_STYPE { /* Line 2053 of yacc.c */ -#line 38 "promela.ypp" +#line 39 "promela.ypp" uscxml::PromelaParserNode* node; char* value; @@ -149,6 +149,19 @@ typedef union PROMELA_STYPE # define PROMELA_STYPE_IS_DECLARED 1 #endif +#if ! defined PROMELA_LTYPE && ! defined PROMELA_LTYPE_IS_DECLARED +typedef struct PROMELA_LTYPE +{ + int first_line; + int first_column; + int last_line; + int last_column; +} PROMELA_LTYPE; +# define promela_ltype PROMELA_LTYPE /* obsolescent; will be withdrawn */ +# define PROMELA_LTYPE_IS_DECLARED 1 +# define PROMELA_LTYPE_IS_TRIVIAL 1 +#endif + #ifdef YYPARSE_PARAM #if defined __STDC__ || defined __cplusplus diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.ypp b/src/uscxml/plugins/datamodel/promela/parser/promela.ypp index 8e87c75..d76b24a 100644 --- a/src/uscxml/plugins/datamodel/promela/parser/promela.ypp +++ b/src/uscxml/plugins/datamodel/promela/parser/promela.ypp @@ -21,13 +21,14 @@ #define YYDEBUG 1 #define YYERROR_VERBOSE 1 -extern int promela_lex (PROMELA_STYPE* yylval_param, void* yyscanner); +extern int promela_lex (PROMELA_STYPE* yylval_param, PROMELA_LTYPE* yylloc_param, void* yyscanner); using namespace uscxml; %} %pure-parser %debug +%locations %file-prefix "promela" %parse-param { uscxml::PromelaParser* ctx } %lex-param {void * scanner} @@ -98,8 +99,8 @@ program : varref : cmpnd { $$ = $1; } ; -pfld : PML_NAME { $$ = ctx->value(PML_NAME, $1); free($1); } - | PML_NAME '[' expr ']' { $$ = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, $1), $3); free($1); } +pfld : PML_NAME { $$ = ctx->value(PML_NAME, (void*)&(@1), $1); free($1); } + | PML_NAME '[' expr ']' { $$ = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, (void*)&(@1), $1), $3); free($1); } ; cmpnd : pfld @@ -152,10 +153,10 @@ expr : '(' expr ')' { $$ = $2; } | PML_LEN '(' varref ')' { $$ = ctx->node(PML_LEN, 1, $3); } | varref { $$ = $1; } - | PML_CONST { $$ = ctx->value(PML_CONST, $1); free($1); } + | PML_CONST { $$ = ctx->value(PML_CONST, (void*)&(@1), $1); free($1); } | PML_STRING { /* Non standard promela for string literals */ - $$ = ctx->value(PML_STRING, $1); free($1); } + $$ = ctx->value(PML_STRING, (void*)&(@1), $1); free($1); } ; @@ -165,13 +166,13 @@ vis : /* empty */ { $$ = ctx->node(PML_SHOW, 0); } | PML_ISLOCAL { $$ = ctx->node(PML_ISLOCAL, 0); } ; -one_decl: vis PML_TYPE var_list { $$ = ctx->node(PML_DECL, 3, $1, ctx->value(PML_TYPE, $2), $3); free($2); } +one_decl: vis PML_TYPE var_list { $$ = ctx->node(PML_DECL, 3, $1, ctx->value(PML_TYPE, (void*)&(@2), $2), $3); free($2); } | vis PML_UNAME var_list { $$ = ctx->node(PML_UNAME, 2, $1, $3); } - | vis PML_TYPE PML_ASGN '{' nlst '}' { $$ = ctx->node(PML_DECL, 3, $1, ctx->value(PML_TYPE, $2), $5); free($2); } + | vis PML_TYPE PML_ASGN '{' nlst '}' { $$ = ctx->node(PML_DECL, 3, $1, ctx->value(PML_TYPE, (void*)&(@2), $2), $5); free($2); } | vis utype { $$ = $2; } ; -utype : PML_TYPEDEF PML_NAME '{' decl_lst '}' { $$ = ctx->node(PML_TYPEDEF, 2, ctx->value(PML_NAME, $2), $4); } +utype : PML_TYPEDEF PML_NAME '{' decl_lst '}' { $$ = ctx->node(PML_TYPEDEF, 2, ctx->value(PML_NAME, (void*)&(@2), $2), $4); } ; decl_lst: one_decl { $$ = $1; } @@ -194,12 +195,12 @@ ivar : vardcl { $$ = $1; } | vardcl PML_ASGN expr { $$ = ctx->node(PML_ASGN, 2, $1, $3); } ; -vardcl : PML_NAME { $$ = ctx->value(PML_NAME, $1); free($1); } - | PML_NAME PML_COLON PML_CONST { $$ = ctx->node(PML_COLON, 2, ctx->value(PML_NAME, $1), ctx->value(PML_CONST, $3)); free($1); free($3); } - | PML_NAME '[' const_expr ']' { $$ = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, $1), $3); free($1); } +vardcl : PML_NAME { $$ = ctx->value(PML_NAME, (void*)&(@1), $1); free($1); } + | PML_NAME PML_COLON PML_CONST { $$ = ctx->node(PML_COLON, 2, ctx->value(PML_NAME, (void*)&(@1), $1), ctx->value(PML_CONST, (void*)&(@3), $3)); free($1); free($3); } + | PML_NAME '[' const_expr ']' { $$ = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, (void*)&(@1), $1), $3); free($1); } ; -const_expr: PML_CONST { $$ = ctx->value(PML_CONST, $1); free($1); } +const_expr: PML_CONST { $$ = ctx->value(PML_CONST, (void*)&(@1), $1); free($1); } | PML_MINUS const_expr %prec PML_MINUS { $$ = ctx->node(PML_MINUS, 1, $2); } | '(' const_expr ')' { $$ = $2; } | const_expr PML_PLUS const_expr { $$ = ctx->node(PML_PLUS, 2, $1, $3); } @@ -209,13 +210,13 @@ const_expr: PML_CONST { $$ = ctx->value(PML_CONST, $1); free($1); } | const_expr PML_MODULO const_expr { $$ = ctx->node(PML_MODULO, 2, $1, $3); } ; -nlst : PML_NAME { $$ = ctx->value(PML_NAME, $1); free($1); } +nlst : PML_NAME { $$ = ctx->value(PML_NAME, (void*)&(@1), $1); free($1); } | nlst PML_NAME { if ($1->type == PML_NAME) { $$ = ctx->node(PML_NAMELIST, 1, $1); - $$->push(ctx->value(PML_NAME, $2)); + $$->push(ctx->value(PML_NAME, (void*)&(@2), $2)); } else { - $1->push(ctx->value(PML_NAME, $2)); + $1->push(ctx->value(PML_NAME, (void*)&(@2), $2)); } free($2); } @@ -233,14 +234,14 @@ stmnt : Stmnt { $$ = $1; } Stmnt : varref PML_ASGN expr { $$ = ctx->node(PML_ASGN, 2, $1, $3); } | varref PML_INCR { $$ = ctx->node(PML_INCR, 1, $1); } | varref PML_DECR { $$ = ctx->node(PML_DECR, 1, $1); } - | PML_PRINT '(' PML_STRING prargs ')' { $$ = ctx->node(PML_PRINT, 2, ctx->value(PML_STRING, $3), $4); free($3); } + | PML_PRINT '(' PML_STRING prargs ')' { $$ = ctx->node(PML_PRINT, 2, ctx->value(PML_STRING, (void*)&(@3), $3), $4); free($3); } | PML_PRINT '(' varref ')' { $$ = ctx->node(PML_PRINT, 1, $3); } - | PML_PRINT '(' PML_CONST ')' { $$ = ctx->node(PML_PRINT, 1, ctx->value(PML_CONST, $3)); free($3); } + | PML_PRINT '(' PML_CONST ')' { $$ = ctx->node(PML_PRINT, 1, ctx->value(PML_CONST, (void*)&(@3), $3)); free($3); } | PML_ASSERT expr { $$ = ctx->node(PML_ASSERT, 1, $2); } | expr { $$ = $1; } ; -prargs : /* empty */ { $$ = ctx->value(0, ""); } +prargs : /* empty */ { $$ = ctx->value(0, NULL, ""); } | PML_COMMA arg { $$ = $2; } ; diff --git a/src/uscxml/transform/ChartToFSM.cpp b/src/uscxml/transform/ChartToFSM.cpp index 8d286a7..d220638 100644 --- a/src/uscxml/transform/ChartToFSM.cpp +++ b/src/uscxml/transform/ChartToFSM.cpp @@ -200,6 +200,7 @@ ChartToFSM::ChartToFSM(const Interpreter& other) { _lastTransientStateId = 0; _lastStateIndex = 0; + _lastActiveIndex = 0; _lastTransIndex = 0; _maxEventSentChain = 0; @@ -880,7 +881,12 @@ void ChartToFSM::explode() { _globalConf[globalState->stateId]->index = _lastStateIndex++; if(_globalConf[globalState->stateId]->isFinal) { - _activeConf[globalState->activeId] = globalState; // remember as active configuration + if (_activeConf.find(globalState->activeId) == _activeConf.end()) { + assert(globalState->activeIndex == -1); + globalState->activeIndex = _lastActiveIndex++; + _activeConf[globalState->activeId] = globalState; // remember as active configuration + exitInterpreter(); + } continue; // done in this branch } @@ -914,6 +920,9 @@ void ChartToFSM::explode() { // unique is not quite like what we need, but it was a start globalState->sortedOutgoing = reapplyUniquePredicates(globalState->sortedOutgoing); + assert(_activeConf.find(globalState->activeId) == _activeConf.end()); + assert(globalState->activeIndex == -1); + globalState->activeIndex = _lastActiveIndex++; _activeConf[globalState->activeId] = globalState; } @@ -1049,26 +1058,6 @@ Arabica::XPath::NodeSet ChartToFSM::refsToTransitions(const std::se } return transitions; } - -#if 0 -void ChartToFSM::labelTransitions() { - // put a unique id on each transition - Arabica::XPath::NodeSet states = getAllStates(); - states.push_back(_scxml); - for (int i = 0; i < states.size(); i++) { - Arabica::DOM::Element stateElem = Arabica::DOM::Element(states[i]); - std::string stateId = ATTR(stateElem, "id"); - NodeSet transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", stateElem); - // some transitions are in the inital elements - NodeSet initials = filterChildElements(_nsInfo.xmlNSPrefix + "initial", stateElem); - transitions.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "transition", initials)); - for (int j = 0; j < transitions.size(); j++) { - Element transition = Element(transitions[j]); - transition.setAttribute("id", stateId + ":"+ toStr(j + 1)); - } - } -} -#endif void ChartToFSM::beforeMicroStep(Interpreter interpreter) { } @@ -1093,7 +1082,8 @@ GlobalState::GlobalState(const Arabica::XPath::NodeSet& activeState const std::string& xmlNSPrefix, ChartToFSM* flattener) { interpreter = flattener; - + activeIndex = -1; + // take references for (int i = 0; i < activeStates_.size(); i++) { activeStatesRefs.insert(strTo(ATTR_CAST(activeStates_[i], "index"))); diff --git a/src/uscxml/transform/ChartToFSM.h b/src/uscxml/transform/ChartToFSM.h index f8dad5a..006e73b 100644 --- a/src/uscxml/transform/ChartToFSM.h +++ b/src/uscxml/transform/ChartToFSM.h @@ -92,6 +92,7 @@ public: std::string stateId; std::string activeId; + long activeIndex; long index; bool isFinal; @@ -253,6 +254,7 @@ protected: size_t _lastTransientStateId; size_t _lastStateIndex; + size_t _lastActiveIndex; size_t _lastTransIndex; bool _skipEventChainCalculations; diff --git a/src/uscxml/transform/ChartToPromela.cpp b/src/uscxml/transform/ChartToPromela.cpp index 9b6674d..092a284 100644 --- a/src/uscxml/transform/ChartToPromela.cpp +++ b/src/uscxml/transform/ChartToPromela.cpp @@ -35,6 +35,8 @@ #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) \ { \ @@ -116,7 +118,7 @@ void PromelaEventSource::writeStart(std::ostream& stream, int indent) { for (int i = 0; i < indent; i++) { padding += " "; } - stream << padding << "run " << name << "EventSource();" << std::endl; + stream << padding << "run " << name << "EventSource() priority 10;" << std::endl; } void PromelaEventSource::writeStop(std::ostream& stream, int indent) { @@ -139,15 +141,16 @@ void PromelaEventSource::writeDeclarations(std::ostream& stream, int indent) { void PromelaEventSource::writeBody(std::ostream& stream) { + stream << "proctype " << name << "EventSource() {" << std::endl; stream << " " << name << "EventSourceDone = 0;" << std::endl; if (analyzer->usesComplexEventStruct()) { - stream << " _event_t tmpEvent;" << std::endl; + stream << " _event_t tmpE;" << std::endl; } stream << " " << name << "NewEvent:" << std::endl; stream << " " << "if" << std::endl; - stream << " " << ":: " << name << "EventSourceDone -> skip;" << std::endl; - stream << " " << ":: " << "len(eQ) <= " << externalQueueLength << " -> skip;" << std::endl; + stream << " " << ":: " << name << "EventSourceDone -> goto " << name << "Done;" << std::endl; + stream << " " << ":: " << "len(eQ) >= " << externalQueueLength - longestSequence << " -> skip;" << std::endl; stream << " " << ":: else { " << std::endl; Trie& trie = analyzer->getTrie(); @@ -183,7 +186,7 @@ void PromelaEventSource::writeBody(std::ostream& stream) { continue; } if (analyzer->usesComplexEventStruct()) { - stream << "tmpEvent.name = " << analyzer->macroForLiteral(node->value) << "; eQ!tmpEvent; "; + stream << "tmpE.name = " << analyzer->macroForLiteral(node->value) << "; eQ!tmpE; "; } else { stream << "eQ!" << analyzer->macroForLiteral(node->value) << "; "; } @@ -272,9 +275,9 @@ PromelaEventSource::PromelaEventSource() { analyzer = NULL; } -PromelaEventSource::PromelaEventSource(const PromelaInline& source, uint32_t eQueueLength) { +PromelaEventSource::PromelaEventSource(const PromelaInline& source, PromelaCodeAnalyzer* analyzer, uint32_t eQueueLength) { type = PROMELA_EVENT_SOURCE_INVALID; - analyzer = NULL; + this->analyzer = analyzer; externalQueueLength = eQueueLength; this->source = source; @@ -296,13 +299,17 @@ PromelaEventSource::PromelaEventSource(const PromelaInline& source, uint32_t eQu if (token.length() == 0) continue; seq.push_back(token); + if (analyzer != NULL) + analyzer->addEvent(token); } sequences.push_back(seq); + if (seq.size() > longestSequence) + longestSequence = seq.size(); } } } -void PromelaCodeAnalyzer::addCode(const std::string& code) { +void PromelaCodeAnalyzer::addCode(const std::string& code, ChartToPromela* interpreter) { PromelaParser parser(code); // find all strings @@ -344,6 +351,7 @@ void PromelaCodeAnalyzer::addCode(const std::string& code) { assert(false); } + _typeDefs.occurrences.insert(interpreter); PromelaTypedef* td = &_typeDefs; std::string seperator; @@ -403,6 +411,7 @@ void PromelaCodeAnalyzer::addCode(const std::string& code) { 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 = 1; break; @@ -538,14 +547,113 @@ int PromelaCodeAnalyzer::indexForLiteral(const std::string& literal) { return _strIndex[literal]; } -std::string PromelaCodeAnalyzer::replaceLiterals(const std::string code) { - std::string replaced = code; - for (std::map::const_iterator litIter = _strMacroNames.begin(); litIter != _strMacroNames.end(); litIter++) { - boost::replace_all(replaced, "'" + litIter->first + "'", litIter->second); +std::string PromelaCodeAnalyzer::adaptCode(const std::string& code, const std::string& prefix) { +// for (std::map::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 > posList; + std::list >::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(""); } - return replaced; + + // 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 posList = getTokenPositions(expr, PML_NAME, parsed.ast); +// posList.sort(); +// +// std::stringstream prefixed; +// std::list::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 > PromelaCodeAnalyzer::getTokenPositions(const std::string& expr, int type, PromelaParserNode* ast) { + std::list > 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::iterator opIter = ast->operands.begin(); opIter != ast->operands.end(); opIter++) { + std::list > tmp = getTokenPositions(expr, type, *opIter); + posList.merge(tmp); + } + return posList; +} + std::set PromelaCodeAnalyzer::getEventsWithPrefix(const std::string& prefix) { std::set eventNames; std::list trieNodes = _eventTrie.getWordsWithPrefix(prefix); @@ -559,14 +667,23 @@ std::set PromelaCodeAnalyzer::getEventsWithPrefix(const std::string return eventNames; } +ChartToPromela::~ChartToPromela() { + if (_analyzer != NULL) + delete(_analyzer); + for (std::map, ChartToPromela*>::iterator nestedIter = _machines.begin(); nestedIter != _machines.end(); nestedIter++) { + nestedIter->second->_analyzer = NULL; + delete (nestedIter->second); + } +} + void ChartToPromela::writeEvents(std::ostream& stream) { - std::map events = _analyzer.getEvents(); + std::map events = _analyzer->getEvents(); std::map::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 << "#define " << _analyzer->macroForLiteral(eventIter->first) << " " << _analyzer->indexForLiteral(eventIter->first); stream << " /* from \"" << eventIter->first << "\" */" << std::endl; } eventIter++; @@ -578,7 +695,7 @@ void ChartToPromela::writeStates(std::ostream& stream) { std::map::iterator stateIter = _activeConf.begin(); while(stateIter != _activeConf.end()) { - stream << "#define " << "s" << stateIter->second->index << " " << stateIter->second->index; + stream << "#define " << "s" << stateIter->second->activeIndex << " " << stateIter->second->activeIndex; stream << " /* from \"" << stateIter->first << "\" */" << std::endl; stateIter++; } @@ -591,17 +708,17 @@ void ChartToPromela::writeStates(std::ostream& stream) { void ChartToPromela::writeStateMap(std::ostream& stream) { stream << "/* macros for original state names */" << std::endl; - std::map origStates = _analyzer.getOrigStates(); + std::map origStates = _analyzer->getOrigStates(); for (std::map::iterator origIter = origStates.begin(); origIter != origStates.end(); origIter++) { - stream << "#define " << _analyzer.macroForLiteral(origIter->first) << " " << origIter->second; + stream << "#define " << _analyzer->macroForLiteral(origIter->first) << " " << origIter->second; stream << " /* from \"" << origIter->first << "\" */" << std::endl; } -// std::map states = _analyzer.getStates(); +// std::map states = _analyzer->getStates(); // size_t stateIndex = 0; // for (std::map::iterator stateIter = states.begin(); stateIter != states.end(); stateIter++) { // stream << "_x" -// std::list origStates = _analyzer.getOrigState(stateIter->first); +// std::list origStates = _analyzer->getOrigState(stateIter->first); // size_t origIndex = 0; // for (std::list::iterator origIter = origStates.begin(); origIter != origStates.end(); origIter++) { // @@ -628,7 +745,7 @@ void ChartToPromela::writeHistoryArrays(std::ostream& stream) { void ChartToPromela::writeTypeDefs(std::ostream& stream) { stream << "/* typedefs */" << std::endl; - PromelaCodeAnalyzer::PromelaTypedef typeDefs = _analyzer.getTypes(); + PromelaCodeAnalyzer::PromelaTypedef typeDefs = _analyzer->getTypes(); if (typeDefs.types.size() == 0) return; @@ -653,12 +770,26 @@ void ChartToPromela::writeTypeDefs(std::ostream& stream) { continue; stream << "typedef " << currDef.name << " {" << std::endl; - if (currDef.name.compare("_event_t") == 0 && currDef.types.find("name") == currDef.types.end()) { // special treatment for _event + 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; + stream << " int seqNr;" << std::endl; + } stream << " int name;" << std::endl; + if (_analyzer->usesEventField("invokeid")) { + stream << " int invokeid;" << std::endl; + } } for (std::map::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; + stream << " bool states[" << _analyzer->getOrigStates().size() << "];" << std::endl; continue; } if (tIter->second.types.size() == 0) { @@ -672,7 +803,7 @@ void ChartToPromela::writeTypeDefs(std::ostream& stream) { } // stream << "/* typedef instances */" << std::endl; -// PromelaCodeAnalyzer::PromelaTypedef allTypes = _analyzer.getTypes(); +// PromelaCodeAnalyzer::PromelaTypedef allTypes = _analyzer->getTypes(); // std::map::iterator typeIter = allTypes.types.begin(); // while(typeIter != allTypes.types.end()) { // if (typeIter->second.types.size() > 0) { @@ -788,7 +919,7 @@ std::string ChartToPromela::conditionalizeForHist(const std::setsecond.end()) { assert(_historyMembers.find(relevanthistIter->first) != _historyMembers.end()); assert(_historyMembers[relevanthistIter->first].find(*histItemIter) != _historyMembers[relevanthistIter->first].end()); - condition << itemSep << "_hist_" << boost::to_lower_copy(_analyzer.macroForLiteral(relevanthistIter->first)) << "[" << _historyMembers[relevanthistIter->first][*histItemIter] << "]"; + condition << itemSep << "_hist_" << boost::to_lower_copy(_analyzer->macroForLiteral(relevanthistIter->first)) << "[" << _historyMembers[relevanthistIter->first][*histItemIter] << "]"; itemSep = " && "; histItemIter++; } @@ -810,7 +941,7 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra padding += " "; } - stream << std::endl << "t" << transition->index << ": /* ######################## " << std::endl; + stream << std::endl << _prefix << "t" << transition->index << ": /* ######################## " << std::endl; stream << " from state: "; FlatStateIdentifier flatActiveSource(transition->source); PRETTY_PRINT_LIST(stream, flatActiveSource.getActive()); @@ -820,6 +951,10 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra stream << std::endl; stream << padding << "atomic {" << std::endl; +// stream << padding << " if" << std::endl; +// stream << padding << " :: " << _prefix << "done -> goto " << _prefix << "terminate;" << std::endl; +// stream << padding << " :: else -> skip;" << std::endl; +// stream << padding << " fi" << std::endl; padding += " "; indent++; @@ -909,12 +1044,12 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra } } - if (!_analyzer.usesInPredicate() && (action.entered || action.exited)) { + if (!_analyzer->usesInPredicate() && (action.entered || action.exited)) { continue; } if (ecIter->type == ExecContentSeqItem::EXEC_CONTENT_ONLY_FOR) { - assert(!wroteHistoryAssignments); // we need to move assignments after dispatching? +// assert(!wroteHistoryAssignments); // we need to move assignments after dispatching? if (condSet != ecIter->transitions) { stream << padding << "if" << std::endl; stream << padding << ":: " << conditionalizeForHist(ecIter->transitions) << " -> {" << std::endl; @@ -924,7 +1059,7 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra condSet = ecIter->transitions; } } else if (ecIter->type == ExecContentSeqItem::EXEC_CONTENT_ALL_BUT) { - assert(!wroteHistoryAssignments); // we need to move assignments after dispatching? +// assert(!wroteHistoryAssignments); // we need to move assignments after dispatching? if (condSet != ecIter->transitions) { stream << padding << "if" << std::endl; stream << padding << ":: " << conditionalizeForHist(ecIter->transitions) << " -> skip;" << std::endl; @@ -941,42 +1076,115 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra if (action.exited) { // we left a state - stream << padding << "_x.states[" << _analyzer.macroForLiteral(ATTR(action.exited, "id")) << "] = false; " << std::endl; - continue; + stream << padding << _prefix << "_x.states[" << _analyzer->macroForLiteral(ATTR(action.exited, "id")) << "] = false; " << std::endl; +// continue; } if (action.entered) { // we entered a state - stream << padding << "_x.states[" << _analyzer.macroForLiteral(ATTR(action.entered, "id")) << "] = true; " << std::endl; - continue; + 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 writeExecutableContent(stream, action.transition, indent); - continue; +// continue; } if (action.onExit) { // executable content from an onexit element writeExecutableContent(stream, action.onExit, indent); - continue; +// continue; } if (action.onEntry) { // executable content from an onentry element writeExecutableContent(stream, action.onEntry, indent); - continue; +// continue; } if (action.invoke) { // an invoke element - continue; + + if (_machines.find(action.invoke) != _machines.end()) { +#if 1 + stream << padding << _prefix << "start!" << _analyzer->macroForLiteral(_machines[action.invoke]->_invokerid) << ";" << std::endl; +#else + + // nested SCXML document + + // set from namelist + if (HAS_ATTR_CAST(action.invoke, "namelist")) { + std::list namelist = tokenize(ATTR_CAST(action.invoke, "namelist")); + for (std::list::iterator nlIter = namelist.begin(); nlIter != namelist.end(); nlIter++) { + if (_machines[action.invoke]->_dataModelVars.find(*nlIter) != _machines[action.invoke]->_dataModelVars.end()) { + stream << padding << _machines[action.invoke]->_prefix << *nlIter << " = " << _prefix << *nlIter << std::endl; + } + } + } + + // set from params + NodeSet invokeParams = filterChildElements(_nsInfo.xmlNSPrefix + "param", action.invoke); + for (int i = 0; i < invokeParams.size(); i++) { + std::string identifier = ATTR_CAST(invokeParams[i], "name"); + std::string expression = ATTR_CAST(invokeParams[i], "expr"); + if (_machines[action.invoke]->_dataModelVars.find(identifier) != _machines[action.invoke]->_dataModelVars.end()) { + stream << padding << _machines[action.invoke]->_prefix << identifier << " = " << ADAPT_SRC(expression) << ";" << std::endl; + } + } + +// stream << padding << " /* assign local variables from invoke request */" << std::endl; +// +// if (_analyzer->usesComplexEventStruct() && _analyzer->usesEventField("data")) { +// for (std::set::iterator dmIter = _dataModelVars.begin(); dmIter != _dataModelVars.end(); dmIter++) { +// if (_analyzer->usesEventDataField(*dmIter)) { +// stream << " if" << std::endl; +// stream << " :: " << _prefix << "_event.data." << *dmIter << " -> " << _prefix << *dmIter << " = " << "_event.data." << *dmIter << ";" << std::endl; +// stream << " :: else -> skip;" << std::endl; +// stream << " fi" << std::endl; +// } +// } +// } +// stream << std::endl; + + stream << padding << "run " << _machines[action.invoke]->_prefix << "run() priority 20;" << std::endl; + if (HAS_ATTR_CAST(action.invoke, "idlocation")) { + stream << padding << ADAPT_SRC(ATTR_CAST(action.invoke, "idlocation")) << " = " << _analyzer->macroForLiteral(_machines[_machinesPerId[ATTR_CAST(action.invoke, "id")]]->_invokerid) << ";" << std::endl; + } +#endif + } else { + if (HAS_ATTR_CAST(action.invoke, "invokeid") && _invokers.find(ATTR_CAST(action.invoke, "invokeid")) != _invokers.end()) + _invokers[ATTR_CAST(action.invoke, "invokeid")].writeStart(stream, indent); + } + } if (action.uninvoke) { + assert(_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; + +// std::cout << action.uninvoke << std::endl; // an invoke element to uninvoke - continue; + if (_machines.find(action.uninvoke) != _machines.end()) { + // nested SCXML document + stream << padding << _machines[action.uninvoke]->_prefix << "canceled = true;" << std::endl; + writeRemovePendingEventsFromInvoker(stream, _machines[action.uninvoke], indent, false); +#if 0 + stream << padding << "do" << std::endl; + stream << padding << ":: len(" << _machines[action.uninvoke]->_prefix << "tmpQ) > 0 -> " << _machines[action.uninvoke]->_prefix << "tmpQ?_;" << std::endl; + stream << padding << ":: len(" << _machines[action.uninvoke]->_prefix << "eQ) > 0 -> " << _machines[action.uninvoke]->_prefix << "eQ?_;" << std::endl; + stream << padding << ":: else -> break;" << std::endl; + stream << padding << "od" << std::endl; +#endif + } else { + if (HAS_ATTR_CAST(action.uninvoke, "invokeid") && _invokers.find(ATTR_CAST(action.invoke, "invokeid")) != _invokers.end()) + stream << padding << ATTR_CAST(action.uninvoke, "invokeid") << "EventSourceDone" << "= 1;" << std::endl; + } +// continue; } if (isConditionalized) { @@ -990,6 +1198,7 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra stream << padding << ":: else -> skip;" << std::endl; stream << padding << "fi;" << std::endl; } + isConditionalized = false; } } @@ -1025,7 +1234,7 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra PRETTY_PRINT_LIST(stream, flatActiveDest.getActive()); stream << "*/" << std::endl; - stream << padding << " s = s" << histNewState->index << ";" << std::endl; + stream << padding << " " << _prefix << "s = s" << histNewState->activeIndex << ";" << std::endl; writeTransitionClosure(stream, *histTargetIter->second.begin(), histNewState, indent + 1); // is this correct for everyone in set? @@ -1048,7 +1257,7 @@ void ChartToPromela::writeTransition(std::ostream& stream, GlobalTransition* tra PRETTY_PRINT_LIST(stream, flatActiveDest.getActive()); stream << " */" << std::endl; - stream << padding << "s = s" << origNewState->index << ";" << std::endl; + stream << padding << _prefix << "s = s" << origNewState->activeIndex << ";" << std::endl; writeTransitionClosure(stream, transition, origNewState, indent); @@ -1146,7 +1355,7 @@ void ChartToPromela::writeHistoryAssignments(std::ostream& stream, GlobalTransit while(forgetIter != histClassIter->toForget.end()) { std::set::iterator forgetMemberIter = forgetIter->second.begin(); while(forgetMemberIter != forgetIter->second.end()) { - stream << padding << "_hist_" << boost::to_lower_copy(_analyzer.macroForLiteral(forgetIter->first)); + stream << padding << "_hist_" << boost::to_lower_copy(_analyzer->macroForLiteral(forgetIter->first)); stream << "[" << _historyMembers[forgetIter->first][*forgetMemberIter] << "] = 0;"; stream << " \t/* " << *forgetMemberIter << " */" << std::endl; forgetMemberIter++; @@ -1160,7 +1369,7 @@ void ChartToPromela::writeHistoryAssignments(std::ostream& stream, GlobalTransit while(rememberIter != histClassIter->toRemember.end()) { std::set::iterator rememberMemberIter = rememberIter->second.begin(); while(rememberMemberIter != rememberIter->second.end()) { - stream << padding << "_hist_" << boost::to_lower_copy(_analyzer.macroForLiteral(rememberIter->first)); + stream << padding << "_hist_" << boost::to_lower_copy(_analyzer->macroForLiteral(rememberIter->first)); stream << "[" << _historyMembers[rememberIter->first][*rememberMemberIter] << "] = 1;"; stream << " \t/* " << *rememberMemberIter << " */" << std::endl; rememberMemberIter++; @@ -1303,12 +1512,12 @@ void ChartToPromela::writeTransitionClosure(std::ostream& stream, GlobalTransiti } if (state->isFinal) { - stream << padding << "goto terminate;" << std::endl; + stream << padding << "goto " << _prefix << "terminate;" << std::endl; } else { if (!transition->isEventless) { - stream << padding << "spontaneous = true;" << std::endl; + stream << padding << _prefix << "spontaneous = true;" << std::endl; } - stream << padding << "goto microStep;" << std::endl; + stream << padding << "goto " << _prefix << "microStep;" << std::endl; } } @@ -1333,7 +1542,7 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: if (node.getNodeType() == Node_base::TEXT_NODE) { if (boost::trim_copy(node.getNodeValue()).length() > 0) - stream << beautifyIndentation(_analyzer.replaceLiterals(node.getNodeValue()), indent) << std::endl; + stream << beautifyIndentation(ADAPT_SRC(node.getNodeValue()), indent) << std::endl; } if (node.getNodeType() != Node_base::ELEMENT_NODE) @@ -1342,7 +1551,7 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: Arabica::DOM::Element nodeElem = Arabica::DOM::Element(node); if (false) { - } else if(TAGNAME(nodeElem) == "onentry" || TAGNAME(nodeElem) == "onexit" || TAGNAME(nodeElem) == "transition") { + } else if(TAGNAME(nodeElem) == "onentry" || TAGNAME(nodeElem) == "onexit" || TAGNAME(nodeElem) == "transition" || TAGNAME(nodeElem) == "finalize") { // descent into childs and write their contents Arabica::DOM::Node child = node.getFirstChild(); while(child) { @@ -1352,7 +1561,7 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: } else if(TAGNAME(nodeElem) == "script") { NodeSet scriptText = filterChildType(Node_base::TEXT_NODE, node, true); for (int i = 0; i < scriptText.size(); i++) { - stream << _analyzer.replaceLiterals(beautifyIndentation(scriptText[i].getNodeValue(), indent)) << std::endl; + stream << ADAPT_SRC(beautifyIndentation(scriptText[i].getNodeValue(), indent)) << std::endl; } } else if(TAGNAME(nodeElem) == "log") { @@ -1383,9 +1592,9 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: } } else if(TAGNAME(nodeElem) == "foreach") { - stream << padding << "for (" << (HAS_ATTR(nodeElem, "index") ? ATTR(nodeElem, "index") : "_index") << " in " << ATTR(nodeElem, "array") << ") {" << std::endl; + 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 << " " << ATTR(nodeElem, "item") << " = " << ATTR(nodeElem, "array") << "[" << (HAS_ATTR(nodeElem, "index") ? ATTR(nodeElem, "index") : "_index") << "];" << std::endl; + stream << padding << " " << _prefix << ATTR(nodeElem, "item") << " = " << _prefix << ATTR(nodeElem, "array") << "[" << _prefix << (HAS_ATTR(nodeElem, "index") ? ATTR(nodeElem, "index") : "_index") << "];" << std::endl; } Arabica::DOM::Node child = node.getFirstChild(); while(child) { @@ -1393,7 +1602,7 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: child = child.getNextSibling(); } if (HAS_ATTR(nodeElem, "index")) - stream << padding << " " << ATTR(nodeElem, "index") << "++;" << std::endl; + stream << padding << " " << _prefix << ATTR(nodeElem, "index") << "++;" << std::endl; stream << padding << "}" << std::endl; } else if(TAGNAME(nodeElem) == "if") { @@ -1406,59 +1615,80 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: } else if(TAGNAME(nodeElem) == "assign") { if (HAS_ATTR(nodeElem, "location")) { - stream << padding << ATTR(nodeElem, "location") << " = "; + stream << padding << _prefix << ATTR(nodeElem, "location") << " = "; } if (HAS_ATTR(nodeElem, "expr")) { - stream << _analyzer.replaceLiterals(ATTR(nodeElem, "expr")) << ";" << std::endl; + stream << ADAPT_SRC(ATTR(nodeElem, "expr")) << ";" << std::endl; } else { NodeSet assignTexts = filterChildType(Node_base::TEXT_NODE, nodeElem, true); if (assignTexts.size() > 0) { - stream << _analyzer.replaceLiterals(boost::trim_copy(assignTexts[0].getNodeValue())) << ";" << std::endl; + stream << ADAPT_SRC(boost::trim_copy(assignTexts[0].getNodeValue())) << ";" << std::endl; } } } else if(TAGNAME(nodeElem) == "send" || TAGNAME(nodeElem) == "raise") { std::string targetQueue; if (TAGNAME(nodeElem) == "raise") { - targetQueue = "iQ!"; + targetQueue = _prefix + "iQ!"; } else if (!HAS_ATTR(nodeElem, "target")) { - targetQueue = "tmpQ!"; + targetQueue = _prefix + "tmpQ!"; } else if (ATTR(nodeElem, "target").compare("#_internal") == 0) { - targetQueue = "iQ!"; + 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")); + event = _analyzer->macroForLiteral(ATTR(nodeElem, "event")); } else if (HAS_ATTR(nodeElem, "eventexpr")) { - event = ATTR(nodeElem, "eventexpr"); + event = ADAPT_SRC(ATTR(nodeElem, "eventexpr")); } - if (_analyzer.usesComplexEventStruct()) { + if (_analyzer->usesComplexEventStruct()) { stream << padding << "{" << std::endl; - stream << padding << " _event_t tmpEvent;" << std::endl; - stream << padding << " tmpEvent.name = " << event << ";" << std::endl; + stream << padding << " _event_t tmpE;" << std::endl; + stream << padding << " tmpE.name = " << event << ";" << std::endl; if (HAS_ATTR(nodeElem, "idlocation")) { stream << padding << " /* idlocation */" << std::endl; stream << padding << " _lastSendId = _lastSendId + 1;" << std::endl; - stream << padding << " " << ATTR(nodeElem, "idlocation") << " = _lastSendId;" << std::endl; - stream << padding << " tmpEvent.sendid = _lastSendId;" << std::endl; + stream << padding << " " << _prefix << ATTR(nodeElem, "idlocation") << " = _lastSendId;" << std::endl; + stream << padding << " tmpE.sendid = _lastSendId;" << std::endl; stream << padding << " if" << std::endl; stream << padding << " :: _lastSendId == 2147483647 -> _lastSendId = 0;" << std::endl; stream << padding << " :: timeout -> skip;" << std::endl; stream << padding << " fi;" << std::endl; } else if (HAS_ATTR(nodeElem, "id")) { - stream << padding << " tmpEvent.sendid = " << _analyzer.macroForLiteral(ATTR(nodeElem, "id")) << ";" << std::endl; + stream << padding << " tmpE.sendid = " << _analyzer->macroForLiteral(ATTR(nodeElem, "id")) << ";" << std::endl; } - if (_analyzer.usesEventField("origintype") && targetQueue.compare("iQ!") != 0) { - stream << padding << " tmpEvent.origintype = " << _analyzer.macroForLiteral("http://www.w3.org/TR/scxml/#SCXMLEventProcessor") << ";" << std::endl; + if (_invokerid.length() > 0 && !boost::starts_with(targetQueue, _prefix)) { // do not send invokeid if we send / raise to ourself + stream << padding << " tmpE.invokeid = " << _analyzer->macroForLiteral(_invokerid) << ";" << std::endl; } - if (_analyzer.usesEventField("type")) { - std::string eventType = (targetQueue.compare("iQ!") == 0 ? _analyzer.macroForLiteral("internal") : _analyzer.macroForLiteral("external")); - stream << padding << " tmpEvent.type = " << eventType << ";" << std::endl; + if (_analyzer->usesEventField("origintype") && !boost::ends_with(targetQueue, "iQ!")) { + stream << padding << " tmpE.origintype = " << _analyzer->macroForLiteral("http://www.w3.org/TR/scxml/#SCXMLEventProcessor") << ";" << std::endl; + } + + if (_analyzer->usesEventField("delay")) { + targetQueue += "!"; + stream << padding << " _lastSeqId = _lastSeqId + 1;" << std::endl; + if (HAS_ATTR_CAST(nodeElem, "delay")) { + stream << padding << " tmpE.delay = " << ATTR_CAST(nodeElem, "delay") << ";" << std::endl; + } else if (HAS_ATTR_CAST(nodeElem, "delayexpr")) { + stream << padding << " tmpE.delay = " << ADAPT_SRC(ATTR_CAST(nodeElem, "delayexpr")) << ";" << std::endl; + } else { + stream << padding << " tmpE.delay = 0;" << std::endl; + } + stream << padding << " tmpE.seqNr = _lastSeqId;" << std::endl; + } + + if (_analyzer->usesEventField("type")) { + std::string eventType = (targetQueue.compare("iQ!") == 0 ? _analyzer->macroForLiteral("internal") : _analyzer->macroForLiteral("external")); + stream << padding << " tmpE.type = " << eventType << ";" << std::endl; } NodeSet sendParams = filterChildElements(_nsInfo.xmlNSPrefix + "param", nodeElem); @@ -1467,14 +1697,14 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: if (sendParams.size() > 0) { for (int i = 0; i < sendParams.size(); i++) { Element paramElem = Element(sendParams[i]); - stream << padding << " tmpEvent.data." << ATTR(paramElem, "name") << " = " << ATTR(paramElem, "expr") << ";" << std::endl; + stream << padding << " tmpE.data." << ATTR(paramElem, "name") << " = " << ADAPT_SRC(ATTR(paramElem, "expr")) << ";" << std::endl; } } if (sendNameList.size() > 0) { std::list nameListIds = tokenizeIdRefs(sendNameList); std::list::iterator nameIter = nameListIds.begin(); while(nameIter != nameListIds.end()) { - stream << padding << " tmpEvent.data." << *nameIter << " = " << *nameIter << ";" << std::endl; + stream << padding << " tmpE.data." << *nameIter << " = " << ADAPT_SRC(*nameIter) << ";" << std::endl; nameIter++; } } @@ -1482,29 +1712,100 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica: if (sendParams.size() == 0 && sendNameList.size() == 0 && sendContents.size() > 0) { Element contentElem = Element(sendContents[0]); if (contentElem.hasChildNodes() && contentElem.getFirstChild().getNodeType() == Node_base::TEXT_NODE) { - stream << padding << " tmpEvent.data = " << spaceNormalize(contentElem.getFirstChild().getNodeValue()) << ";" << std::endl; + std::string content = spaceNormalize(contentElem.getFirstChild().getNodeValue()); + if (!isNumeric(content.c_str(), 10)) { + stream << padding << " tmpE.data = " << _analyzer->macroForLiteral(content) << ";" << std::endl; + } else { + stream << padding << " tmpE.data = " << content << ";" << std::endl; + } } else if (HAS_ATTR(contentElem, "expr")) { - stream << padding << " tmpEvent.data = " << _analyzer.replaceLiterals(ATTR(contentElem, "expr")) << ";" << std::endl; + stream << padding << " tmpE.data = " << ADAPT_SRC(ATTR(contentElem, "expr")) << ";" << std::endl; } } - stream << padding << " " << targetQueue << "tmpEvent;" << std::endl; + stream << padding << " " << targetQueue << "tmpE;" << std::endl; stream << padding << "}" << std::endl; } else { stream << padding << targetQueue << event << ";" << std::endl; } } - } else if(TAGNAME(nodeElem) == "invoke") { - _invokers[ATTR(nodeElem, "invokeid")].writeStart(stream, indent); - } else if(TAGNAME(nodeElem) == "uninvoke") { - stream << padding << ATTR(nodeElem, "invokeid") << "EventSourceDone" << "= 1;" << std::endl; } else if(TAGNAME(nodeElem) == "cancel") { - // noop + writeCancelWithIdOrExpr(stream, nodeElem, this, indent); } else { std::cerr << "'" << TAGNAME(nodeElem) << "'" << std::endl << nodeElem << std::endl; assert(false); } } + +void ChartToPromela::writeCancelWithIdOrExpr(std::ostream& stream, const Arabica::DOM::Element& cancel, ChartToPromela* invoker, int indent) { + std::string padding; + for (int i = 0; i < indent; i++) { + padding += " "; + } + + ChartToPromela* topMachine = (invoker->_parent != NULL ? invoker->_parent : invoker); + + std::list others; + others.push_back(topMachine); + for (std::map, ChartToPromela*>::iterator queueIter = topMachine->_machines.begin(); queueIter != topMachine->_machines.end(); queueIter++) { + others.push_back(queueIter->second); + } + if (HAS_ATTR(cancel, "sendid")) { + stream << padding << "/* cancel event given by sendid */" << std::endl; + stream << padding << "atomic {" << std::endl; + stream << padding << " _event_t tmpE;" << std::endl; + stream << padding << " do" << std::endl; + for (std::list::iterator queueIter = others.begin(); queueIter != others.end(); queueIter++) { + stream << padding << " :: " << (*queueIter)->_prefix << "eQ?\?" << (_analyzer->usesEventField("delay") ? "tmpE.delay, tmpE.seqNr," : "") << " tmpE.name, " << _analyzer->macroForLiteral(ATTR(cancel, "sendid")) << ";" << std::endl; + stream << padding << " :: " << (*queueIter)->_prefix << "tmpQ?\?" << (_analyzer->usesEventField("delay") ? "tmpE.delay, tmpE.seqNr," : "") << " tmpE.name, " << _analyzer->macroForLiteral(ATTR(cancel, "sendid")) << ";" << std::endl; + } + stream << padding << " :: else -> break;" << std::endl; + stream << padding << " od" << std::endl; + stream << padding << "}" << std::endl; + + } else if (HAS_ATTR(cancel, "sendidexpr")) { + stream << padding << "/* cancel event given by sendidexpr */" << std::endl; + stream << padding << "atomic {" << std::endl; + stream << padding << " _event_t tmpE;" << std::endl; + + stream << padding << " do" << std::endl; + stream << padding << " :: (len(" << _prefix << "tmpQ) > 0) -> { " << _prefix << "tmpQ?tmpE; sendIdQ!tmpE; }" << std::endl; + stream << padding << " :: else -> break;" << std::endl; + stream << padding << " od" << std::endl; + + stream << padding << " do" << std::endl; + stream << padding << " :: (len(sendIdQ) > 0) -> {" << std::endl; + stream << padding << " sendIdQ?tmpE;" << std::endl; + stream << padding << " if" << std::endl; + stream << padding << " :: (tmpE.sendid != " << ADAPT_SRC(ATTR(cancel, "sendidexpr")) << ") -> " << _prefix << "tmpQ!tmpE" << std::endl; + stream << padding << " :: else -> skip;" << std::endl; + stream << padding << " fi" << std::endl; + stream << padding << " }" << std::endl; + stream << padding << " :: else -> break;" << std::endl; + stream << padding << " od" << std::endl; + + for (std::list::iterator queueIter = others.begin(); queueIter != others.end(); queueIter++) { + stream << padding << " do" << std::endl; + stream << padding << " :: (len(" << (*queueIter)->_prefix << "eQ) > 0) -> { " << (*queueIter)->_prefix << "eQ?tmpE; sendIdQ!tmpE; }" << std::endl; + stream << padding << " :: else -> break;" << std::endl; + stream << padding << " od" << std::endl; + + stream << padding << " do" << std::endl; + stream << padding << " :: (len(sendIdQ) > 0) -> {" << std::endl; + stream << padding << " sendIdQ?tmpE;" << std::endl; + stream << padding << " if" << std::endl; + stream << padding << " :: (tmpE.sendid != " << ADAPT_SRC(ATTR(cancel, "sendidexpr")) << ") -> " << (*queueIter)->_prefix << "eQ!tmpE" << std::endl; + stream << padding << " :: else -> skip;" << std::endl; + stream << padding << " fi" << std::endl; + stream << padding << " }" << std::endl; + stream << padding << " :: else -> break;" << std::endl; + stream << padding << " od" << std::endl; + } + stream << padding << "}" << std::endl; + } + +} + PromelaInlines PromelaInlines::fromNodeSet(const NodeSet& node, bool recurse) { PromelaInlines allPromInls; Arabica::XPath::NodeSet comments = InterpreterImpl::filterChildType(Node_base::COMMENT_NODE, node, recurse); @@ -1613,7 +1914,7 @@ void ChartToPromela::writeIfBlock(std::ostream& stream, const Arabica::XPath::No stream << padding << "if" << std::endl; // we need to nest the elseifs to resolve promela if semantics - stream << padding << ":: (" << _analyzer.replaceLiterals(ATTR(ifNode, "cond")) << ") -> {" << std::endl; + stream << padding << ":: (" << ADAPT_SRC(ATTR(ifNode, "cond")) << ") -> {" << std::endl; Arabica::DOM::Node child; if (TAGNAME(ifNode) == "if") { @@ -1695,13 +1996,13 @@ std::string ChartToPromela::beautifyIndentation(const std::string& code, int ind void ChartToPromela::writeStrings(std::ostream& stream) { stream << "/* string literals */" << std::endl; - std::set literals = _analyzer.getLiterals(); - std::map events = _analyzer.getEvents(); - std::map origStates = _analyzer.getOrigStates(); + std::set literals = _analyzer->getLiterals(); + std::map events = _analyzer->getEvents(); + std::map origStates = _analyzer->getOrigStates(); for (std::set::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; + if (events.find(*litIter) == events.end() && (origStates.find(*litIter) == origStates.end() || !_analyzer->usesInPredicate())) + stream << "#define " << _analyzer->macroForLiteral(*litIter) << " " << _analyzer->indexForLiteral(*litIter) << " /* " << *litIter << " */" << std::endl; } } @@ -1709,37 +2010,57 @@ void ChartToPromela::writeDeclarations(std::ostream& stream) { stream << "/* global variables */" << std::endl; - if (_analyzer.usesComplexEventStruct()) { + // 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 _event; /* current state */" << std::endl; - stream << "unsigned s : " << BIT_WIDTH(_activeConf.size() + 1) << "; /* current state */" << std::endl; - stream << "chan iQ = [" << MAX(_internalQueueLength, 1) << "] of {_event_t} /* internal queue */" << std::endl; - stream << "chan eQ = [" << _externalQueueLength + 1 << "] of {_event_t} /* external queue */" << std::endl; - stream << "chan tmpQ = [" << MAX(_externalQueueLength, 1) << "] of {_event_t} /* temporary queue for external events in transitions */" << std::endl; - stream << "hidden _event_t tmpQItem;" << std::endl; + 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; + stream << "chan " << _prefix << "tmpQ = [" << MAX(_externalQueueLength + tolerance, 1) << "] of {_event_t} /* temporary queue for external events in transitions */" << std::endl; +// stream << "hidden " << "_event_t " << _prefix << "tmpQItem;" << std::endl; } else { - stream << "unsigned _event : " << BIT_WIDTH(_analyzer.getEvents().size() + 1) << "; /* current event */" << std::endl; - stream << "unsigned s : " << BIT_WIDTH(_activeConf.size() + 1) << "; /* current state */" << std::endl; - stream << "chan iQ = [" << MAX(_internalQueueLength, 1) << "] of {int} /* internal queue */" << std::endl; - stream << "chan eQ = [" << _externalQueueLength + 1 << "] of {int} /* external queue */" << std::endl; - stream << "chan tmpQ = [" << MAX(_externalQueueLength, 1) << "] of {int} /* temporary queue for external events in transitions */" << std::endl; - stream << "hidden unsigned tmpQItem : " << BIT_WIDTH(_analyzer.getEvents().size() + 1) << ";" << std::endl; + stream << "unsigned " << _prefix << "_event : " << BIT_WIDTH(_analyzer->getEvents().size() + 1) << "; /* current event */" << std::endl; + stream << "unsigned " << _prefix << "s : " << BIT_WIDTH(_activeConf.size() + 1) << "; /* current state */" << std::endl; + stream << "chan " << _prefix << "iQ = [" << MAX(_internalQueueLength, 1) << "] of {int} /* internal queue */" << std::endl; + stream << "chan " << _prefix << "eQ = [" << _externalQueueLength + tolerance << "] of {int} /* external queue */" << std::endl; + stream << "chan " << _prefix << "tmpQ = [" << MAX(_externalQueueLength + tolerance, 1) << "] of {int} /* temporary queue for external events in transitions */" << std::endl; +// stream << "hidden unsigned " << _prefix << "tmpQItem : " << BIT_WIDTH(_analyzer->getEvents().size() + 1) << ";" << std::endl; } - stream << "bool spontaneous = true; /* whether to process event-less only n this step */" << std::endl; - stream << "hidden int _index; /* helper for indexless foreach loops */" << std::endl; - - if (_analyzer.getTypes().types.find("_ioprocessors") != _analyzer.getTypes().types.end()) { - stream << "hidden _ioprocessors_t _ioprocessors;" << std::endl; + if (_machines.size() > 0) { + stream << "chan " << _prefix << "start = [" << _machines.size() << "] of {int} /* nested machines to start at next macrostep */" << std::endl; } - if (_analyzer.usesEventField("sendid")) { - stream << "hidden int _lastSendId = 0; /* sequential counter for send ids */"; + stream << "hidden int " << _prefix << "_index; /* helper for indexless foreach loops */" << std::endl; + stream << "hidden int " << _prefix << "_pid; /* 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 (_analyzer->getTypes().types.find("_ioprocessors") != _analyzer->getTypes().types.end()) { + stream << "hidden _ioprocessors_t " << _prefix << "_ioprocessors;" << std::endl; } + + 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 */"; + } -// if (_analyzer.usesPlatformVars()) { + if (_analyzer->usesEventField("delay")) { + stream << "hidden int _lastSeqId = 0; /* sequential counter for delayed events */"; + } + } +// if (_analyzer->usesPlatformVars()) { // stream << "_x_t _x;" << std::endl; // } + if (_analyzer->usesInPredicate()) { + stream << "_x_t " << _prefix << "_x;" << std::endl; + } + stream << std::endl << std::endl; // get all data elements @@ -1747,7 +2068,7 @@ void ChartToPromela::writeDeclarations(std::ostream& stream) { // NodeSet dataText = filterChildType(Node_base::TEXT_NODE, datas, true); // write their text content - stream << "/* datamodel variables */" << std::endl; + stream << "/* datamodel variables for " << _prefix << " */" << std::endl; std::set processedIdentifiers; for (int i = 0; i < datas.size(); i++) { @@ -1759,6 +2080,7 @@ void ChartToPromela::writeDeclarations(std::ostream& stream) { std::string expression = (HAS_ATTR_CAST(data, "expr") ? ATTR_CAST(data, "expr") : ""); 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); @@ -1782,7 +2104,7 @@ void ChartToPromela::writeDeclarations(std::ostream& stream) { arrSize = type.substr(bracketPos, type.length() - bracketPos); type = type.substr(0, bracketPos); } - std::string decl = type + " " + identifier + arrSize; + std::string decl = type + " " + _prefix + identifier + arrSize; if (arrSize.length() > 0) { stream << decl << ";" << std::endl; @@ -1791,10 +2113,10 @@ void ChartToPromela::writeDeclarations(std::ostream& stream) { stream << decl; if (expression.length() > 0) { // id and expr given - stream << " = " << _analyzer.replaceLiterals(boost::trim_copy(expression)) << ";" << std::endl; + stream << " = " << ADAPT_SRC(boost::trim_copy(expression)) << ";" << std::endl; } else if (value.length() > 0) { // id and text content given - stream << " = " << _analyzer.replaceLiterals(value) << ";" << std::endl; + stream << " = " << ADAPT_SRC(value) << ";" << std::endl; } else { // only id given stream << ";" << std::endl; @@ -1806,9 +2128,14 @@ void ChartToPromela::writeDeclarations(std::ostream& stream) { } } - PromelaCodeAnalyzer::PromelaTypedef allTypes = _analyzer.getTypes(); + PromelaCodeAnalyzer::PromelaTypedef allTypes = _analyzer->getTypes(); std::map::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; @@ -1821,9 +2148,9 @@ void ChartToPromela::writeDeclarations(std::ostream& stream) { processedIdentifiers.insert(typeIter->first); if (typeIter->second.types.size() == 0) { - stream << "hidden " << declForRange(typeIter->first, typeIter->second.minValue, typeIter->second.maxValue) << ";" << std::endl; + stream << "hidden " << declForRange(_prefix + typeIter->first, typeIter->second.minValue, typeIter->second.maxValue) << ";" << std::endl; } else { - stream << "hidden " << typeIter->second.name << " " << typeIter->first << ";" << std::endl; + stream << "hidden " << _prefix << typeIter->second.name << " " << typeIter->first << ";" << std::endl; } typeIter++; } @@ -1857,10 +2184,47 @@ void ChartToPromela::writeEventSources(std::ostream& stream) { } } +void ChartToPromela::writeStartInvoker(std::ostream& stream, const Arabica::DOM::Node& node, ChartToPromela* invoker, int indent) { + std::string padding; + for (int i = 0; i < indent; i++) { + padding += " "; + } + + // set from namelist + if (HAS_ATTR_CAST(node, "namelist")) { + std::list namelist = tokenize(ATTR_CAST(node, "namelist")); + for (std::list::iterator nlIter = namelist.begin(); nlIter != namelist.end(); nlIter++) { + if (invoker->_dataModelVars.find(*nlIter) != invoker->_dataModelVars.end()) { + stream << padding << invoker->_prefix << *nlIter << " = " << _prefix << *nlIter << std::endl; + } + } + } + + // set from params + NodeSet invokeParams = filterChildElements(_nsInfo.xmlNSPrefix + "param", node); + for (int 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 transitions; - stream << "proctype step() {" << std::endl; + stream << "proctype " << _prefix << "run() {" << std::endl; + stream << " " << _prefix << "done = false;" << std::endl; + stream << " " << _prefix << "canceled = false;" << std::endl; + stream << " " << _prefix << "spontaneous = true;" << std::endl; + stream << " " << _prefix << "_pid = _pid;" << std::endl; // write initial transition // transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", _startState); // assert(transitions.size() == 1); @@ -1885,19 +2249,140 @@ void ChartToPromela::writeFSM(std::ostream& stream) { } stream << std::endl; - stream << "macroStep:" << std::endl; + stream << _prefix << "macroStep:" << std::endl; stream << " /* push send events to external queue */" << std::endl; + stream << " do" << std::endl; + if (_analyzer->usesEventField("delay")) { + stream << " :: len(" << _prefix << "tmpQ) != 0 -> { " << _prefix << "tmpQ?" << _prefix << "_event; " << _prefix << "eQ!!" << _prefix << "_event }" << std::endl; + } else { + stream << " :: len(" << _prefix << "tmpQ) != 0 -> { " << _prefix << "tmpQ?" << _prefix << "_event; " << _prefix << "eQ!" << _prefix << "_event }" << std::endl; + } + stream << " :: 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, ChartToPromela*>::iterator machIter = _machines.begin(); machIter != _machines.end(); machIter++) { + stream << " :: invokerId == " << _analyzer->macroForLiteral(machIter->second->_invokerid) << " -> {" << std::endl; + writeStartInvoker(stream, machIter->first, machIter->second, 2); + stream << " }" << std::endl; + } + stream << " :: else -> skip; " << std::endl; + stream << " fi " << std::endl; + stream << " } " << std::endl; + stream << " :: else -> break;" << std::endl; + stream << " od" << std::endl; + } + + if (_analyzer->usesEventField("delay")) { + stream << " /* find machine with next event due */" << std::endl; + stream << " if" << std::endl; + stream << " :: len(" << _prefix << "iQ) != 0 -> skip; /* internal queue not empty -> do not reduce our priority */" << std::endl; + stream << " :: " << _prefix << "eQ?\? <0> -> skip; /* at least one event without delay -> do not reduce our priority */" << std::endl; + stream << " :: timeout -> { "<< std::endl; + // stream << " /* determine queue with shortest delay in front */" << std::endl; + stream << " atomic {" << std::endl; + stream << " int nextPid;" << std::endl; + stream << " int lowestDelay = 0;" << std::endl; + stream << " _event_t tmpE;" << std::endl; + + for (std::map, ChartToPromela*>::iterator queueIter = _machinesAll->begin(); queueIter != _machinesAll->end(); queueIter++) { + std::list queues; + queues.push_back("eQ"); + queues.push_back("tmpQ"); + for (std::list::iterator qIter = queues.begin(); qIter != queues.end(); qIter++) { + stream << " if" << std::endl; + stream << " :: len(" << queueIter->second->_prefix << *qIter << ") > 0 -> {" << std::endl; + stream << " " << queueIter->second->_prefix << *qIter << "?;" << std::endl; + stream << " if" << std::endl; + stream << " :: (tmpE.delay < lowestDelay || lowestDelay == 0) -> {" << std::endl; + stream << " lowestDelay = tmpE.delay;" << std::endl; + stream << " nextPid = " << queueIter->second->_prefix << "_pid;" << std::endl; + stream << " }" << std::endl; + stream << " :: else -> skip;" << std::endl; + stream << " fi;" << std::endl; + stream << " }" << std::endl; + stream << " :: else -> skip;;" << std::endl; + stream << " fi;" << std::endl; + } + } + + stream << " set_priority(nextPid, 10);" << std::endl; + stream << " if" << std::endl; + stream << " :: (nextPid != _pid) -> set_priority(_pid, 1);" << std::endl; + stream << " :: else -> skip;" << std::endl; + stream << " fi;" << std::endl; + stream << " }" << std::endl; + stream << " }" << std::endl; + stream << " fi;" << std::endl; + stream << " set_priority(_pid, 10);" << std::endl << std::endl; + } + + stream << " /* pop an event */" << std::endl; stream << " if" << std::endl; - stream << " :: len(tmpQ) != 0 -> { tmpQ?_event; eQ!_event }" << std::endl; - stream << " :: else -> skip;" << std::endl; + stream << " :: len(" << _prefix << "iQ) != 0 -> " << _prefix << "iQ ? " << _prefix << "_event /* from internal queue */" << std::endl; + stream << " :: else -> " << _prefix << "eQ ? " << _prefix << "_event /* from external queue */" << std::endl; stream << " fi;" << std::endl << std::endl; - - stream << " /* pop an event */" << std::endl; + + stream << " /* terminate if we are stopped */" << std::endl; stream << " if" << std::endl; - stream << " :: len(iQ) != 0 -> iQ ? _event /* from internal queue */" << std::endl; - stream << " :: else -> eQ ? _event /* from external queue */" << 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; - stream << "microStep:" << std::endl; + +#if 1 + { + bool finalizeFound = false; + for (std::map, ChartToPromela*>::iterator invIter = _machines.begin(); invIter != _machines.end(); invIter++) { + NodeSet finalizes = filterChildElements(_nsInfo.xmlNSPrefix + "finalize", invIter->first, false); + if (finalizes.size() > 0) { + finalizeFound = true; + break; + } + } + if (finalizeFound) { + stream << " /* event */" << std::endl; + stream << " if" << std::endl; + for (std::map, ChartToPromela*>::iterator invIter = _machines.begin(); invIter != _machines.end(); invIter++) { + NodeSet finalizes = 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], 2); + stream << " } " << std::endl; + } + } + stream << " :: else -> skip;" << std::endl; + stream << " fi;" << std::endl << std::endl; + } + } +#endif + + stream << " /* autoforward to respective invokers */" << std::endl; + for (std::map, ChartToPromela*>::iterator invIter = _machines.begin(); invIter != _machines.end(); invIter++) { + if (invIter->second == this) { + continue; + } + //std::cout << invIter->first << std::endl; + if (DOMUtils::attributeIsTrue(ATTR_CAST(invIter->first, "autoforward"))) { + stream << " if" << std::endl; + stream << " :: " << invIter->second->_prefix << "done -> skip;" << std::endl; + stream << " :: " << invIter->second->_prefix << "canceled -> skip;" << std::endl; + stream << " :: else -> { " << invIter->second->_prefix << "eQ!!" << _prefix << "_event" << " }" << std::endl; + 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; @@ -1906,8 +2391,29 @@ void ChartToPromela::writeFSM(std::ostream& 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 << "terminate: skip;" << std::endl; + stream << std::endl; + stream << _prefix << "terminate: skip;" << std::endl; + + if (_parent != NULL) { + stream << " {" << std::endl; + stream << " _event_t tmpE;" << std::endl; + stream << " tmpE.name = " << _analyzer->macroForLiteral("done.invoke." + _invokerid) << ";" << std::endl; + if (_invokerid.length() > 0) { + stream << " tmpE.invokeid = " << _analyzer->macroForLiteral(_invokerid) << ";" << std::endl; + } + if (_analyzer->usesEventField("delay")) { + stream << " _lastSeqId = _lastSeqId + 1;" << std::endl; + stream << " tmpE.seqNr = _lastSeqId;" << std::endl; + stream << " " << _parent->_prefix << "eQ!!tmpE;" << std::endl; + } else { + stream << " " << _parent->_prefix << "eQ!tmpE;" << std::endl; + } + stream << " }" << std::endl; + stream << _prefix << "cancel: skip;" << std::endl; + writeRemovePendingEventsFromInvoker(stream, this, 1, true); + } + // stop all event sources if (_globalEventSource) _globalEventSource.writeStop(stream, 1); @@ -1921,6 +2427,53 @@ void ChartToPromela::writeFSM(std::ostream& stream) { stream << "}" << std::endl; } +void ChartToPromela::writeRemovePendingEventsFromInvoker(std::ostream& stream, ChartToPromela* invoker, int indent, bool atomic) { + std::string padding; + for (int i = 0; i < indent; i++) { + padding += " "; + } + + if (!invoker || !invoker->_parent) + return; + + if (_analyzer->usesEventField("delay")) { + if (atomic) { + stream << padding << "atomic {" << std::endl; + } else { + stream << padding << "{" << std::endl; + } + stream << padding << " /* remove all this invoker's pending events from all queues */" << std::endl; + stream << padding << " _event_t tmpE;" << std::endl; + std::list others; + others.push_back(invoker->_parent); + for (std::map, ChartToPromela*>::iterator queueIter = invoker->_parent->_machines.begin(); queueIter != invoker->_parent->_machines.end(); queueIter++) { + if (queueIter->second != invoker) + others.push_back(queueIter->second); + } + + for (std::list::iterator queueIter = others.begin(); queueIter != others.end(); queueIter++) { + stream << padding << " do" << std::endl; + stream << padding << " :: (len(" << (*queueIter)->_prefix << "eQ) > 0) -> { " << (*queueIter)->_prefix << "eQ?tmpE; " << _prefix << "tmpQ!tmpE; }" << std::endl; + stream << padding << " :: else -> break;" << std::endl; + stream << padding << " od" << std::endl; + + stream << padding << " do" << std::endl; + stream << padding << " :: (len(" << _prefix << "tmpQ) > 0) -> {" << std::endl; + stream << padding << " " << _prefix << "tmpQ?tmpE;" << std::endl; + stream << padding << " if" << std::endl; + stream << padding << " :: (tmpE.invokeid != " << _analyzer->macroForLiteral(invoker->_invokerid) << " || tmpE.delay == 0) -> " << (*queueIter)->_prefix << "eQ!tmpE" << std::endl; + stream << padding << " :: else -> skip;" << std::endl; + stream << padding << " fi" << std::endl; + stream << padding << " }" << std::endl; + stream << padding << " :: else -> break;" << std::endl; + stream << padding << " od" << std::endl; + + } + stream << padding << "}" << std::endl; + } + +} + void ChartToPromela::writeEventDispatching(std::ostream& stream) { for (std::map::iterator stateIter = _activeConf.begin(); stateIter != _activeConf.end(); stateIter++) { // if (_globalStates[i] == _startState) @@ -1938,7 +2491,7 @@ void ChartToPromela::writeEventDispatching(std::ostream& stream) { PRETTY_PRINT_LIST(stream, flatActiveSource.getActive()); stream << " ######################## */" << std::endl; - stream << " :: (s == s" << state->index << ") -> {" << std::endl; + stream << " :: (" << _prefix << "s == s" << state->activeIndex << ") -> {" << std::endl; writeDispatchingBlock(stream, state->sortedOutgoing, 2); // stream << " goto macroStep;"; @@ -1954,8 +2507,8 @@ void ChartToPromela::writeDispatchingBlock(std::ostream& stream, std::listisEventless) { - stream << "spontaneous"; + stream << _prefix << "spontaneous"; } else { std::string eventDescs = currTrans->eventDesc; - + std::list eventNames = tokenizeIdRefs(eventDescs); std::set eventPrefixes; std::list::iterator eventNameIter = eventNames.begin(); @@ -1986,34 +2539,44 @@ void ChartToPromela::writeDispatchingBlock(std::ostream& stream, std::list 0) { - std::set tmp = _analyzer.getEventsWithPrefix(*eventNameIter); + std::set tmp = _analyzer->getEventsWithPrefix(*eventNameIter); eventPrefixes.insert(tmp.begin(), tmp.end()); } eventNameIter++; } if (eventPrefixes.size() > 0) { - stream << "!spontaneous && "; + stream << "!" << _prefix << "spontaneous"; } else { - stream << "!spontaneous"; + stream << "!" << _prefix << "spontaneous"; } + if (eventPrefixes.size() > 0) + stream << " &&"; + + if (eventPrefixes.size() > 1) + stream << " ("; + std::string seperator; std::set::iterator eventIter = eventPrefixes.begin(); while(eventIter != eventPrefixes.end()) { - if (_analyzer.usesComplexEventStruct()) { - stream << seperator << "_event.name == " << _analyzer.macroForLiteral(*eventIter); + if (_analyzer->usesComplexEventStruct()) { + stream << seperator << " " << _prefix << "_event.name == " << _analyzer->macroForLiteral(*eventIter); } else { - stream << seperator << "_event == " << _analyzer.macroForLiteral(*eventIter); + stream << seperator << " " << _prefix << "_event == " << _analyzer->macroForLiteral(*eventIter); } seperator = " || "; eventIter++; } + + if (eventPrefixes.size() > 1) + stream << ")"; + } stream << ")"; if (currTrans->condition.size() > 0) { - stream << " && " + _analyzer.replaceLiterals(currTrans->condition) + ")"; + stream << " && (" + ADAPT_SRC(currTrans->condition) + "))"; } if (currTrans->hasExecutableContent || currTrans->historyTrans.size() > 0) { stream << " -> { " << std::endl; @@ -2023,7 +2586,7 @@ void ChartToPromela::writeDispatchingBlock(std::ostream& stream, std::listindex << ";" << std::endl; + stream << padding << " goto " << _prefix << "t" << currTrans->index << ";" << std::endl; stream << padding << "}" << std::endl; } else { @@ -2037,7 +2600,7 @@ void ChartToPromela::writeDispatchingBlock(std::ostream& stream, std::listindex << ";" << std::endl; + stream << padding << " " << _prefix << "s = s" << newState->activeIndex << ";" << std::endl; writeTransitionClosure(stream, currTrans, newState, indent + 1); stream << padding << "}" << std::endl; @@ -2057,20 +2620,34 @@ void ChartToPromela::writeMain(std::ostream& stream) { if (_varInitializers.size() > 0) { std::list::iterator initIter = _varInitializers.begin(); while(initIter != _varInitializers.end()) { - stream << beautifyIndentation(*initIter); + stream << ADAPT_SRC(beautifyIndentation(*initIter)); initIter++; } stream << std::endl; } if (_globalEventSource) _globalEventSource.writeStart(stream, 1); - stream << " run step();" << std::endl; + stream << " run " << _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, ChartToPromela*>(); + (*_machinesAll)[_scxml] = this; + } + + if (_machinesAllPerId == NULL) + _machinesAllPerId = new std::map >(); + + if (_parentTopMost == NULL) + _parentTopMost = this; _internalQueueLength = getMinInternalQueueLength(MSG_QUEUE_LENGTH); _externalQueueLength = getMinExternalQueueLength(MSG_QUEUE_LENGTH); @@ -2081,10 +2658,86 @@ void ChartToPromela::initNodes() { if (InterpreterImpl::isInEmbeddedDocument(states[i])) continue; Element stateElem(states[i]); - _analyzer.addOrigState(ATTR(stateElem, "id")); + _analyzer->addOrigState(ATTR(stateElem, "id")); if (isCompound(stateElem) || isParallel(stateElem)) { - _analyzer.addEvent("done.state." + ATTR(stateElem, "id")); + _analyzer->addEvent("done.state." + ATTR(stateElem, "id")); + } + } + + { + // shorten UUID ids at invokers for readability + NodeSet invokes = filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true); + invokes.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "uninvoke", _scxml, true)); + + // make sure all invokers have an id! + for (int i = 0; i < invokes.size(); i++) { + if (!HAS_ATTR_CAST(invokes[i], "id")) { + Element 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 invokeElem(invokes[i]); + invokeElem.setAttribute("id", "INV_" + ATTR_CAST(invokes[i], "id").substr(0,5)); + } } + + } + + // are there nestes SCXML invokers? + { + NodeSet invokes = filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true); + for (int 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(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(_baseURI); + nested = Interpreter::fromURI(absUrl); + + } else { + NodeSet nestedContent = InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "content", invokes[i]); + assert(nestedContent.size() == 1); + NodeSet nestedRoot = InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "scxml", nestedContent[0]); + assert(nestedRoot.size() == 1); + + DOMImplementation domFactory = Arabica::SimpleDOM::DOMImplementation::getDOMImplementation(); + Document nestedDoc = domFactory.createDocument(_scxml.getOwnerDocument().getNamespaceURI(), "", 0); + Node importRoot = nestedDoc.importNode(nestedRoot[0], true); + nestedDoc.appendChild(importRoot); + + nested = Interpreter::fromDOM(nestedDoc, _nsInfo); + } + +// std::cout << invokes[i] << std::endl; + + _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 @@ -2120,7 +2773,7 @@ void ChartToPromela::initNodes() { if (boost::ends_with(eventName, ".")) eventName = eventName.substr(0, eventName.size() - 1); if (eventName.size() > 0) - _analyzer.addEvent(eventName); + _analyzer->addEvent(eventName); } } } @@ -2129,24 +2782,42 @@ void ChartToPromela::initNodes() { { NodeSet invokes = filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true); NodeSet sends = filterChildElements(_nsInfo.xmlNSPrefix + "send", _scxml, true); - - for (int i = 0; i < invokes.size(); i++) { - if (HAS_ATTR_CAST(invokes[i], "idlocation")) { - } - } - + for (int i = 0; i < sends.size(); i++) { if (HAS_ATTR_CAST(sends[i], "idlocation")) { - _analyzer.addCode("_event.sendid"); + _analyzer->addCode("_event.sendid", this); } if (HAS_ATTR_CAST(sends[i], "id")) { - _analyzer.addLiteral(ATTR_CAST(sends[i], "id")); - _analyzer.addCode("_event.sendid"); + _analyzer->addLiteral(ATTR_CAST(sends[i], "id")); + _analyzer->addCode("_event.sendid", this); } } + // do we need delays? + for (int i = 0; i < sends.size(); i++) { + if (HAS_ATTR_CAST(sends[i], "delay") || HAS_ATTR_CAST(sends[i], "delayexpr")) { + _analyzer->addCode("_event.delay", this); + _analyzer->addCode("_event.seqNr", this); + } + } } + { + // string literals for raise / send content + NodeSet withContent; + withContent.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "send", _scxml, true)); + withContent.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "raise", _scxml, true)); + + for (int i = 0; i < withContent.size(); i++) { + NodeSet content = filterChildElements(_nsInfo.xmlNSPrefix + "content", withContent[i], true); + for (int j = 0; j < content.size(); j++) { + Element contentElem(content[j]); + std::string content = spaceNormalize(contentElem.getFirstChild().getNodeValue()); + if (!isNumeric(content.c_str(), 10)) + _analyzer->addLiteral(content); + } + } + } // external event names from comments and event sources NodeSet promelaEventSourceComments; NodeSet invokers = _xpath.evaluate("//" + _nsInfo.xpathPrefix + "invoke", _scxml).asNodeSet(); @@ -2158,22 +2829,22 @@ void ChartToPromela::initNodes() { for ( std::list::iterator promIter = promInls.code.begin(); promIter != promInls.code.end(); promIter++) { if (promIter->type == PromelaInline::PROMELA_EVENT_SOURCE || promIter->type == PromelaInline::PROMELA_EVENT_SOURCE_CUSTOM) { - PromelaEventSource promES(*promIter, _externalQueueLength); + PromelaEventSource promES(*promIter, _analyzer, _externalQueueLength); if (TAGNAME_CAST(promelaEventSourceComments[i].getParentNode()) == "scxml") { promES.type = PromelaEventSource::PROMELA_EVENT_SOURCE_GLOBAL; promES.name = "global"; - promES.analyzer = &_analyzer; _globalEventSource = promES; } else { - if (!HAS_ATTR_CAST(promelaEventSourceComments[i].getParentNode(), "invokeid")) { - Element invoker = Element(promelaEventSourceComments[i].getParentNode()); + Element invoker = Element(promelaEventSourceComments[i].getParentNode()); + if (!HAS_ATTR_CAST(promelaEventSourceComments[i].getParentNode(), "id")) { invoker.setAttribute("invokeid", "invoker" + toStr(_invokers.size())); // if there is no invokeid, enumerate + } else { + invoker.setAttribute("invokeid", ATTR_CAST(promelaEventSourceComments[i].getParentNode(), "id")); } std::string invokeId = ATTR_CAST(promelaEventSourceComments[i].getParentNode(), "invokeid"); promES.type = PromelaEventSource::PROMELA_EVENT_SOURCE_INVOKER; promES.name = invokeId; - promES.analyzer = &_analyzer; _invokers[invokeId] = promES; } } @@ -2181,11 +2852,11 @@ void ChartToPromela::initNodes() { } // add platform variables as string literals - _analyzer.addLiteral("_sessionid"); - _analyzer.addLiteral("_name"); + _analyzer->addLiteral(_prefix + "_sessionid"); + _analyzer->addLiteral(_prefix + "_name"); if (HAS_ATTR(_scxml, "name")) { - _analyzer.addLiteral(ATTR(_scxml, "name"), _analyzer.indexForLiteral("_sessionid")); + _analyzer->addLiteral(ATTR(_scxml, "name"), _analyzer->indexForLiteral(_prefix + "_sessionid")); } NodeSet contents = filterChildElements(_nsInfo.xmlNSPrefix + "content", _scxml, true); @@ -2193,7 +2864,7 @@ void ChartToPromela::initNodes() { Element contentElem = Element(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)); + _analyzer->addLiteral(spaceNormalize(content)); } } @@ -2264,7 +2935,7 @@ void ChartToPromela::initNodes() { } } for (std::set::const_iterator codeIter = allCode.begin(); codeIter != allCode.end(); codeIter++) { - _analyzer.addCode(*codeIter); + _analyzer->addCode(*codeIter, this); } // add all namelist entries to the _event structure @@ -2277,7 +2948,7 @@ void ChartToPromela::initNodes() { std::string namelist = ATTR_CAST(withNamelist[i], "namelist"); std::list names = tokenizeIdRefs(namelist); for (std::list::iterator nameIter = names.begin(); nameIter != names.end(); nameIter++) { - _analyzer.addCode("_event.data." + *nameIter + " = 0;"); // introduce for _event_t typedef + _analyzer->addCode("_event.data." + *nameIter + " = 0;", this); // introduce for _event_t typedef } } } @@ -2325,11 +2996,18 @@ void ChartToPromela::writeProgram(std::ostream& stream) { initNodes(); + for (std::map, 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; - if (_analyzer.usesInPredicate()) { + if (_analyzer->usesInPredicate()) { writeStateMap(stream); stream << std::endl; } @@ -2342,6 +3020,12 @@ void ChartToPromela::writeProgram(std::ostream& stream) { writeStrings(stream); stream << std::endl; writeDeclarations(stream); + + for (std::map, ChartToPromela*>::iterator nestedIter = _machines.begin(); nestedIter != _machines.end(); nestedIter++) { + nestedIter->second->writeDeclarations(stream); + stream << std::endl; + } + stream << std::endl; writeEventSources(stream); stream << std::endl; @@ -2350,6 +3034,11 @@ void ChartToPromela::writeProgram(std::ostream& stream) { writeMain(stream); stream << std::endl; + for (std::map, 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; @@ -2357,7 +3046,7 @@ void ChartToPromela::writeProgram(std::ostream& stream) { for (std::map::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 << "s == s" << stateIter->second->index; + acceptingStates << seperator << _prefix << "s == s" << stateIter->second->activeIndex; seperator = " || "; } } diff --git a/src/uscxml/transform/ChartToPromela.h b/src/uscxml/transform/ChartToPromela.h index fe0660f..e322eaf 100644 --- a/src/uscxml/transform/ChartToPromela.h +++ b/src/uscxml/transform/ChartToPromela.h @@ -34,6 +34,8 @@ namespace uscxml { class PromelaCodeAnalyzer; +class ChartToPromela; +class PromelaParserNode; class USCXML_API PromelaInline { public: @@ -69,7 +71,7 @@ public: }; PromelaEventSource(); - PromelaEventSource(const PromelaInline& source, uint32_t externalQueueLength = 0); + PromelaEventSource(const PromelaInline& source, PromelaCodeAnalyzer* analyzer = NULL, uint32_t externalQueueLength = 0); void writeStart(std::ostream& stream, int indent = 0); void writeStop(std::ostream& stream, int indent = 0); @@ -83,6 +85,7 @@ public: PromelaInline source; std::string name; uint32_t externalQueueLength; + uint32_t longestSequence; Arabica::DOM::Node container; std::list > sequences; @@ -132,7 +135,8 @@ public: size_t minValue; size_t maxValue; std::map types; - + std::set occurrences; + bool operator==(const PromelaTypedef& other) const { return name == other.name; } @@ -142,7 +146,7 @@ public: PromelaCodeAnalyzer() : _eventTrie("."), _lastStrIndex(1), _lastStateIndex(0), _lastEventIndex(1), _usesInPredicate(false), _usesPlatformVars(false) { } - void addCode(const std::string& code); + void addCode(const std::string& code, ChartToPromela* interpreter); void addEvent(const std::string& eventName); void addState(const std::string& stateName); void addOrigState(const std::string& stateName); @@ -157,6 +161,14 @@ public: return false; } + bool usesEventDataField(const std::string& fieldName) { + if (usesComplexEventStruct() && + _typeDefs.types["_event"].types.find("data") != _typeDefs.types["_event"].types.end() && + _typeDefs.types["_event"].types["data"].types.find(fieldName) != _typeDefs.types["_event"].types["data"].types.end()) + return true; + return false; + } + bool usesInPredicate() { return _usesInPredicate; } @@ -188,7 +200,10 @@ public: return _eventTrie; } - std::string replaceLiterals(const std::string code); + std::string adaptCode(const std::string& code, const std::string& prefix); + + static std::string prefixIdentifiers(const std::string& expr, const std::string& prefix); + static std::list > getTokenPositions(const std::string& expr, int type, PromelaParserNode* ast); PromelaTypedef& getTypes() { return _typeDefs; @@ -205,9 +220,8 @@ protected: std::map _states; std::map _events; - + PromelaTypedef _typeDefs; - Trie _eventTrie; private: @@ -260,13 +274,13 @@ public: class USCXML_API ChartToPromela : public TransformerImpl, public ChartToFSM { public: - virtual ~ChartToPromela() {} + virtual ~ChartToPromela(); static Transformer transform(const Interpreter& other); void writeTo(std::ostream& stream); protected: - ChartToPromela(const Interpreter& other) : TransformerImpl(), ChartToFSM(other) {} + ChartToPromela(const Interpreter& other) : TransformerImpl(), ChartToFSM(other), _analyzer(NULL), _machinesAll(NULL), _parent(NULL), _parentTopMost(NULL), _machinesAllPerId(NULL), _prefix("MAIN_") {} void initNodes(); @@ -297,6 +311,10 @@ protected: void writeIfBlock(std::ostream& stream, const Arabica::XPath::NodeSet& condChain, int indent = 0); void writeDispatchingBlock(std::ostream& stream, std::list, int indent = 0); + void writeStartInvoker(std::ostream& stream, const Arabica::DOM::Node& node, ChartToPromela* invoker, int indent = 0); + void writeRemovePendingEventsFromInvoker(std::ostream& stream, ChartToPromela* invoker, int indent = 0, bool atomic = true); + void writeCancelWithIdOrExpr(std::ostream& stream, const Arabica::DOM::Element& cancel, ChartToPromela* invoker, int indent = 0); + Arabica::XPath::NodeSet getTransientContent(const Arabica::DOM::Element& state, const std::string& source = ""); //Arabica::DOM::Node getUltimateTarget(const Arabica::DOM::Element& transition); @@ -314,7 +332,7 @@ protected: std::list _varInitializers; // pending initializations for arrays - PromelaCodeAnalyzer _analyzer; + PromelaCodeAnalyzer* _analyzer; uint32_t _externalQueueLength; uint32_t _internalQueueLength; @@ -323,7 +341,19 @@ protected: PromelaEventSource _globalEventSource; std::map > _historyMembers; // ids of all history states - + std::set _dataModelVars; + + Arabica::DOM::Node _finalize; + std::map, ChartToPromela*> _machines; + std::map, ChartToPromela*>* _machinesAll; + ChartToPromela* _parent; // our invoking interpreter + ChartToPromela* _parentTopMost; + + std::map > _machinesPerId; + std::map >* _machinesAllPerId; + std::string _prefix; // our prefix in case of nested SCXML documents + std::string _invokerid; + friend class PromelaEventSource; }; diff --git a/test/ctest/CTestCustom.ctest.in b/test/ctest/CTestCustom.ctest.in index 609c926..484dcb2 100644 --- a/test/ctest/CTestCustom.ctest.in +++ b/test/ctest/CTestCustom.ctest.in @@ -9,6 +9,8 @@ # these are manual or xpath tests generated by the ecma generator set(CTEST_CUSTOM_TESTS_IGNORE + + ### Ignore for ECMAScript datamodel "ecma/test178.scxml" # Manual - PASSED "ecma/test230.scxml" # Manual - PASSED "ecma/test250.scxml" # Manual - PASSED @@ -17,17 +19,21 @@ set(CTEST_CUSTOM_TESTS_IGNORE "ecma/test415.scxml" # Manual - PASSED # "ecma/test513.txt" # Manual - PASSED + ### Ignore for flattened ECMAScript datamodel "fsm/ecma/test178.scxml" # manual test - # "fsm/ecma/test224.scxml" # automatically generated id has the form stateid.platformid "fsm/ecma/test230.scxml" # manual test "fsm/ecma/test250.scxml" # manual test "fsm/ecma/test301.scxml" # manual test "fsm/ecma/test307.scxml" # manual test "fsm/ecma/test415.scxml" # manual test - + # "fsm/ecma/test513.txt" # manual test + + ### Just ignore the XPath datamodel tests that hang, most of the rest fails as well "xpath/test388.scxml" # hangs "xpath/test580.scxml" # hangs + + ### Ignore for PROMELA datamodel "promela/test178.scxml" # manual test "promela/test190.scxml" # string concatenation "promela/test224.scxml" # string operation startWith @@ -51,24 +57,25 @@ set(CTEST_CUSTOM_TESTS_IGNORE "promela/test530.scxml" # assigns DOM node to variable "promela/test534.scxml" # string operation contains + ### Ignore for PROMELA model checking # fail for syntax "spin/promela/test150.scxml" # test that foreach causes a new variable to be declared "spin/promela/test151.scxml" # test that foreach causes a new variable to be declared "spin/promela/test152.scxml" # test that an illegal array or item value causes error.execution "spin/promela/test156.scxml" # test that an error causes the foreach to stop execution - "spin/promela/test172.scxml" # targetexpr _internal - can we support? + # "spin/promela/test172.scxml" # targetexpr _internal - can we support? "spin/promela/test224.scxml" # string operation startWith "spin/promela/test224.scxml" # string operation startWith - "spin/promela/test277.scxml" # 'return' as a literal - "spin/promela/test280.scxml" # late data binding - "spin/promela/test286.scxml" # assigment to a non-declared var - "spin/promela/test294.scxml" # mixed types for event.data + "spin/promela/test277.scxml" # platform creates unbound variable if we assign an illegal value to it + "spin/promela/test280.scxml" # late data binding / undeclared variable + "spin/promela/test286.scxml" # assignment to a non-declared var causes an error + "spin/promela/test294.scxml" # mixed types for event.data via donedata "spin/promela/test301.scxml" # manual test "spin/promela/test302.scxml" # variable not declared "spin/promela/test304.scxml" # variable not declared "spin/promela/test307.scxml" # manual test "spin/promela/test309.scxml" # 'return' as an invalid boolean expression ought to eval to false - "spin/promela/test311.scxml" # assigment to a non-declared var + "spin/promela/test311.scxml" # assignment to a non-declared var "spin/promela/test312.scxml" # assignment of 'return' "spin/promela/test313.scxml" # assignment of 'return' "spin/promela/test314.scxml" # assignment of 'return' @@ -76,7 +83,7 @@ set(CTEST_CUSTOM_TESTS_IGNORE "spin/promela/test324.scxml" # assignment to _name "spin/promela/test325.scxml" # assignment from _ioprocessor "spin/promela/test326.scxml" # assignment from _ioprocessor - "spin/promela/test329.scxml" # several assignment to constants + "spin/promela/test329.scxml" # test that none of the system variables can be modified "spin/promela/test331.scxml" # assigment to a non-declared var "spin/promela/test344.scxml" # 'return' as a cond "spin/promela/test346.scxml" # assignment to system variables @@ -97,52 +104,17 @@ set(CTEST_CUSTOM_TESTS_IGNORE # fail for semantics "spin/promela/test159.scxml" # error raised causes all subsequent elements to be skipped - "spin/promela/test175.scxml" # delay used "spin/promela/test178.scxml" # manual test with two identical params - failed - "spin/promela/test185.scxml" # delay used - "spin/promela/test191.scxml" # nested SCXML document - "spin/promela/test192.scxml" # delay used and nested SCXML document "spin/promela/test194.scxml" # illegal target for send "spin/promela/test199.scxml" # invalid send type - "spin/promela/test207.scxml" # delay / cancel - "spin/promela/test208.scxml" # delay / cancel - "spin/promela/test210.scxml" # sendidexpr works with cancel - "spin/promela/test215.scxml" # nested SCXML document - "spin/promela/test216.scxml" # assignment from file and nested SCXML document - "spin/promela/test220.scxml" # nested SCXML document - "spin/promela/test223.scxml" # nested SCXML document - "spin/promela/test225.scxml" # nested SCXML document - can't we just copy as nested states with event prefixes? - "spin/promela/test226.scxml" # assignment from file and nested SCXML document - "spin/promela/test228.scxml" # nested SCXML document and invokeid - "spin/promela/test229.scxml" # nested SCXML document with autoforward + "spin/promela/test207.scxml" # delay / cancel / nested SCXML + "spin/promela/test215.scxml" # nested SCXML document with typeexpr at invoke + "spin/promela/test216.scxml" # nested SCXML document with srcexpr at invoke "spin/promela/test230.scxml" # nested SCXML document with manual test - "spin/promela/test232.scxml" # nested SCXML document sends events - "spin/promela/test233.scxml" # nested SCXML document with finalize - "spin/promela/test234.scxml" # nested SCXML document with finalize - "spin/promela/test235.scxml" # nested SCXML document sends done.invoke - "spin/promela/test236.scxml" # nested SCXML document sends done.invoke as last event - "spin/promela/test239.scxml" # nested SCXML document from content and src - "spin/promela/test240.scxml" # nested SCXML document with namelist - "spin/promela/test241.scxml" # nested SCXML document with namelist and param - "spin/promela/test243.scxml" # nested SCXML document with param - "spin/promela/test244.scxml" # nested SCXML document with namelist - "spin/promela/test245.scxml" # nested SCXML document with unbound vars - "spin/promela/test247.scxml" # nested SCXML document with done.invoke - "spin/promela/test253.scxml" # nested SCXML document with bidirectional SCXML ioprocessor - "spin/promela/test276.scxml" # nested SCXML document overriding var defaults "spin/promela/test298.scxml" # non-existent data model location "spin/promela/test332.scxml" # sendid is present in error events "spin/promela/test338.scxml" # test that invokeid is set correctly "spin/promela/test343.scxml" # test that illegal produces error.execution - "spin/promela/test347.scxml" # nested SCXML document with bidirectional SCXML ioprocessor - "spin/promela/test351.scxml" # timeout with delay - "spin/promela/test352.scxml" # timeout with delay - "spin/promela/test342.scxml" # timeout with delay - "spin/promela/test388.scxml" # timeout with delay - "spin/promela/test399.scxml" # timeout with delay - # "spin/promela/test409.scxml" # entering states order - In - # "spin/promela/test411.scxml" # entering states order - In - "spin/promela/test422.scxml" # nested SCXML document "spin/promela/test488.scxml" # illegal expr in produces error.execution "spin/promela/test496.scxml" # tests error.communication with illegal target "spin/promela/test500.scxml" # uses _ioprocessors.scxml.location @@ -153,10 +125,10 @@ set(CTEST_CUSTOM_TESTS_IGNORE "spin/promela/test531.scxml" # uses _ioprocessors.basichttp.location "spin/promela/test532.scxml" # uses _ioprocessors.basichttp.location "spin/promela/test552.scxml" # initialize data from file + "spin/promela/test553.scxml" # error in namelist + "spin/promela/test554.scxml" # evaluation of 's args causes an error "spin/promela/test567.scxml" # uses _ioprocessors.basichttp.location "spin/promela/test577.scxml" # send without target for basichttp - "spin/promela/test579.scxml" # timeout with delay - "spin/promela/test580.scxml" # timeout with delay ) diff --git a/test/src/test-promela-parser.cpp b/test/src/test-promela-parser.cpp index 955d39a..00cc347 100644 --- a/test/src/test-promela-parser.cpp +++ b/test/src/test-promela-parser.cpp @@ -171,10 +171,19 @@ void testInlinePromela() { } } +void checkTokenLocations(const std::string& expr, PromelaParserNode* ast) { + if (ast->loc != NULL) { + assert(expr.substr(ast->loc->firstCol, ast->loc->lastCol - ast->loc->firstCol) == ast->value); + } + for (std::list::iterator opIter = ast->operands.begin(); opIter != ast->operands.end(); opIter++) { + checkTokenLocations(expr, *opIter); + } +} + void testPromelaParser() { promela_debug = 0; - +#if 1 std::list expressions; /* declarations */ expressions.push_back("bool b1"); @@ -202,7 +211,9 @@ void testPromelaParser() { expressions.push_back("_x.states[1]"); expressions.push_back("_x.states[1].foo"); expressions.push_back("_event.data[1].aParam.key1.key2[1].key3.key4"); + expressions.push_back("\n\n\n\n int foo = 3;\n\nint bar = 5;"); + /* expressions */ expressions.push_back("i+1"); expressions.push_back("(x == false || t == Bturn);"); @@ -232,10 +243,13 @@ void testPromelaParser() { std::cout << std::endl << "'" << *exprIter << "':" << std::endl; PromelaParser ast(*exprIter); ast.dump(); + if (!boost::contains(*exprIter, "\n")) + checkTokenLocations(*exprIter, ast.ast); } catch (Event e) { std::cerr << e << std::endl; } } +#endif } diff --git a/test/uscxml/promela/test-syntax.scxml b/test/uscxml/promela/test-syntax.scxml index 619e138..101c97a 100644 --- a/test/uscxml/promela/test-syntax.scxml +++ b/test/uscxml/promela/test-syntax.scxml @@ -44,6 +44,16 @@ + + + + diff --git a/test/w3c/confPromela.xsl b/test/w3c/confPromela.xsl index e9ff4ce..e9094d8 100644 --- a/test/w3c/confPromela.xsl +++ b/test/w3c/confPromela.xsl @@ -53,6 +53,11 @@ + + Var + int + + Var int[3] @@ -99,7 +104,37 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -113,6 +148,14 @@ + + 1000 + + + + 0 + + '' @@ -273,7 +316,7 @@ - 's' + diff --git a/test/w3c/promela/test175.scxml b/test/w3c/promela/test175.scxml index 9cd732f..c44a6ab 100644 --- a/test/w3c/promela/test175.scxml +++ b/test/w3c/promela/test175.scxml @@ -4,13 +4,13 @@ event1 will be raised first. Succeed if event1 occurs before event2, otherwise fail --> - + - + - + diff --git a/test/w3c/promela/test185.scxml b/test/w3c/promela/test185.scxml index 8cb877c..0ef8c2e 100644 --- a/test/w3c/promela/test185.scxml +++ b/test/w3c/promela/test185.scxml @@ -4,7 +4,7 @@ - + diff --git a/test/w3c/promela/test186.scxml b/test/w3c/promela/test186.scxml index d8c30ea..b30f6d0 100644 --- a/test/w3c/promela/test186.scxml +++ b/test/w3c/promela/test186.scxml @@ -9,7 +9,7 @@ in the interval.) If var2 ends up == 1, we pass. Otherwise we fail --> - + diff --git a/test/w3c/promela/test187.scxml b/test/w3c/promela/test187.scxml index 1400694..fe09a12 100644 --- a/test/w3c/promela/test187.scxml +++ b/test/w3c/promela/test187.scxml @@ -6,7 +6,7 @@ parent session, should not receive childToParent. If it does, we fail. Otherwis - + @@ -14,7 +14,7 @@ parent session, should not receive childToParent. If it does, we fail. Otherwis - + diff --git a/test/w3c/promela/test191.scxml b/test/w3c/promela/test191.scxml index 760caf9..6fc9a7f 100644 --- a/test/w3c/promela/test191.scxml +++ b/test/w3c/promela/test191.scxml @@ -5,7 +5,7 @@ pass, otherwise we fail. The timer insures that some event is generated and tha - + diff --git a/test/w3c/promela/test192.scxml b/test/w3c/promela/test192.scxml index 0a50aed..48a019a 100644 --- a/test/w3c/promela/test192.scxml +++ b/test/w3c/promela/test192.scxml @@ -7,7 +7,7 @@ We also set a timeout in this process to make sure the test doesn't hang --> - + @@ -17,7 +17,7 @@ We also set a timeout in this process to make sure the test doesn't hang --> - + diff --git a/test/w3c/promela/test193.scxml b/test/w3c/promela/test193.scxml index aa2f297..2d240e7 100644 --- a/test/w3c/promela/test193.scxml +++ b/test/w3c/promela/test193.scxml @@ -7,7 +7,7 @@ SCXML event i/o processor puts the event on the external queue. --> - + diff --git a/test/w3c/promela/test207.scxml b/test/w3c/promela/test207.scxml index 4adbfca..a780b41 100644 --- a/test/w3c/promela/test207.scxml +++ b/test/w3c/promela/test207.scxml @@ -6,7 +6,7 @@ raised in another session, but the spec doesn't define any way to refer to an ev - + @@ -16,8 +16,8 @@ raised in another session, but the spec doesn't define any way to refer to an ev - - + + diff --git a/test/w3c/promela/test208.scxml b/test/w3c/promela/test208.scxml index 72f57a6..3fce2d2 100644 --- a/test/w3c/promela/test208.scxml +++ b/test/w3c/promela/test208.scxml @@ -4,8 +4,8 @@ we get event1 or an error first, cancel didn't work and we fail. --> - - + + diff --git a/test/w3c/promela/test210.scxml b/test/w3c/promela/test210.scxml index 6b692be..08612be 100644 --- a/test/w3c/promela/test210.scxml +++ b/test/w3c/promela/test210.scxml @@ -7,8 +7,8 @@ delayed event1. Thus we get event2 first and pass. If we get event1 or an erro - - + + diff --git a/test/w3c/promela/test215.scxml b/test/w3c/promela/test215.scxml index 1a0819b..3f139c5 100644 --- a/test/w3c/promela/test215.scxml +++ b/test/w3c/promela/test215.scxml @@ -8,7 +8,7 @@ the runtime value is used, the invocation will succeed --> - + diff --git a/test/w3c/promela/test216.scxml b/test/w3c/promela/test216.scxml index 6a9aaa4..8555040 100644 --- a/test/w3c/promela/test216.scxml +++ b/test/w3c/promela/test216.scxml @@ -8,7 +8,7 @@ the runtime value is used, the invocation will succeed --> - + diff --git a/test/w3c/promela/test220.scxml b/test/w3c/promela/test220.scxml index 25bb26b..e16f838 100644 --- a/test/w3c/promela/test220.scxml +++ b/test/w3c/promela/test220.scxml @@ -3,7 +3,7 @@ - + diff --git a/test/w3c/promela/test223.scxml b/test/w3c/promela/test223.scxml index 5317ac7..99ee320 100644 --- a/test/w3c/promela/test223.scxml +++ b/test/w3c/promela/test223.scxml @@ -6,7 +6,7 @@ - + diff --git a/test/w3c/promela/test224.scxml b/test/w3c/promela/test224.scxml index 3892083..09bbb25 100644 --- a/test/w3c/promela/test224.scxml +++ b/test/w3c/promela/test224.scxml @@ -7,7 +7,7 @@ - + diff --git a/test/w3c/promela/test225.scxml b/test/w3c/promela/test225.scxml index 25aa2f1..b38d1a2 100644 --- a/test/w3c/promela/test225.scxml +++ b/test/w3c/promela/test225.scxml @@ -7,7 +7,7 @@ - + diff --git a/test/w3c/promela/test226.scxml b/test/w3c/promela/test226.scxml index 7ab32d8..9a003c2 100644 --- a/test/w3c/promela/test226.scxml +++ b/test/w3c/promela/test226.scxml @@ -5,7 +5,7 @@ success. otherwise it will hang and the timeout in this doc signifies failure. - + diff --git a/test/w3c/promela/test228.scxml b/test/w3c/promela/test228.scxml index 9771a9e..137418a 100644 --- a/test/w3c/promela/test228.scxml +++ b/test/w3c/promela/test228.scxml @@ -6,7 +6,7 @@ - + diff --git a/test/w3c/promela/test229.scxml b/test/w3c/promela/test229.scxml index 3ba733a..4030b85 100644 --- a/test/w3c/promela/test229.scxml +++ b/test/w3c/promela/test229.scxml @@ -6,7 +6,7 @@ it eventually times out and the done.invoke signals failure --> - + @@ -18,7 +18,7 @@ it eventually times out and the done.invoke signals failure --> - + diff --git a/test/w3c/promela/test230.scxml b/test/w3c/promela/test230.scxml index ee97cef..e8bd447 100644 --- a/test/w3c/promela/test230.scxml +++ b/test/w3c/promela/test230.scxml @@ -6,7 +6,7 @@ must check if they are the same and report his result. --> - + @@ -16,7 +16,7 @@ must check if they are the same and report his result. --> - + diff --git a/test/w3c/promela/test232.scxml b/test/w3c/promela/test232.scxml index 2c8a8aa..c54874e 100644 --- a/test/w3c/promela/test232.scxml +++ b/test/w3c/promela/test232.scxml @@ -3,7 +3,7 @@ - + diff --git a/test/w3c/promela/test233.scxml b/test/w3c/promela/test233.scxml index 3087e1f..195d244 100644 --- a/test/w3c/promela/test233.scxml +++ b/test/w3c/promela/test233.scxml @@ -8,7 +8,7 @@ the transtitions. --> - + diff --git a/test/w3c/promela/test234.scxml b/test/w3c/promela/test234.scxml index ee59cad..2e79a98 100644 --- a/test/w3c/promela/test234.scxml +++ b/test/w3c/promela/test234.scxml @@ -10,7 +10,7 @@ var2 should still be set to 1 --> - + @@ -39,7 +39,7 @@ var2 should still be set to 1 --> - + diff --git a/test/w3c/promela/test235.scxml b/test/w3c/promela/test235.scxml index 95b5827..6c6383b 100644 --- a/test/w3c/promela/test235.scxml +++ b/test/w3c/promela/test235.scxml @@ -4,7 +4,7 @@ and should generate done.invoke.foo --> - + diff --git a/test/w3c/promela/test236.scxml b/test/w3c/promela/test236.scxml index 600b7f4..2a8c76c 100644 --- a/test/w3c/promela/test236.scxml +++ b/test/w3c/promela/test236.scxml @@ -5,7 +5,7 @@ events after the done.invoke. Hence timeout indicates success --> - + diff --git a/test/w3c/promela/test237.scxml b/test/w3c/promela/test237.scxml index d23fc20..b39e7db 100644 --- a/test/w3c/promela/test237.scxml +++ b/test/w3c/promela/test237.scxml @@ -6,7 +6,7 @@ the time timeout2 fires, success --> - + @@ -14,7 +14,7 @@ the time timeout2 fires, success --> - + @@ -26,7 +26,7 @@ the time timeout2 fires, success --> - + diff --git a/test/w3c/promela/test239.scxml b/test/w3c/promela/test239.scxml index dab80b9..dc13d5f 100644 --- a/test/w3c/promela/test239.scxml +++ b/test/w3c/promela/test239.scxml @@ -3,7 +3,7 @@ - + diff --git a/test/w3c/promela/test240.scxml b/test/w3c/promela/test240.scxml index e586d4e..f18b796 100644 --- a/test/w3c/promela/test240.scxml +++ b/test/w3c/promela/test240.scxml @@ -9,7 +9,7 @@ should run correctly. --> - + @@ -46,7 +46,7 @@ should run correctly. --> - + diff --git a/test/w3c/promela/test241.scxml b/test/w3c/promela/test241.scxml index dff2920..f2cebaa 100644 --- a/test/w3c/promela/test241.scxml +++ b/test/w3c/promela/test241.scxml @@ -9,7 +9,7 @@ Var1, but should run correctly. --> - + diff --git a/test/w3c/promela/test242.scxml b/test/w3c/promela/test242.scxml index 01ea8d0..c887bcf 100644 --- a/test/w3c/promela/test242.scxml +++ b/test/w3c/promela/test242.scxml @@ -1,56 +1,53 @@ - - - - - - + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + - + - - + + + + + + + + + + + + + + - + - - + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/test/w3c/promela/test243.scxml b/test/w3c/promela/test243.scxml index c29d49f..886f732 100644 --- a/test/w3c/promela/test243.scxml +++ b/test/w3c/promela/test243.scxml @@ -4,7 +4,7 @@ test240sub1 will return success ifits Var1 is set to 1, failure otherwise. --> - + diff --git a/test/w3c/promela/test244.scxml b/test/w3c/promela/test244.scxml index 84b6ec3..87d1f0e 100644 --- a/test/w3c/promela/test244.scxml +++ b/test/w3c/promela/test244.scxml @@ -9,7 +9,7 @@ but should run correctly. --> - + diff --git a/test/w3c/promela/test245.scxml b/test/w3c/promela/test245.scxml index 5f00a42..5f5db7f 100644 --- a/test/w3c/promela/test245.scxml +++ b/test/w3c/promela/test245.scxml @@ -7,7 +7,7 @@ invoked child's datamodel. It will will return success if its Var2 remains unbo - + diff --git a/test/w3c/promela/test247.scxml b/test/w3c/promela/test247.scxml index 822f97d..383813b 100644 --- a/test/w3c/promela/test247.scxml +++ b/test/w3c/promela/test247.scxml @@ -3,7 +3,7 @@ - + diff --git a/test/w3c/promela/test250.scxml b/test/w3c/promela/test250.scxml index e3f6b7a..0747224 100644 --- a/test/w3c/promela/test250.scxml +++ b/test/w3c/promela/test250.scxml @@ -12,7 +12,7 @@ Tester must examine log output from child process to determine success --> - + diff --git a/test/w3c/promela/test252.scxml b/test/w3c/promela/test252.scxml index f4667ef..3a4a982 100644 --- a/test/w3c/promela/test252.scxml +++ b/test/w3c/promela/test252.scxml @@ -5,7 +5,7 @@ timeout indicates success. --> - + @@ -19,7 +19,7 @@ timeout indicates success. --> - + diff --git a/test/w3c/promela/test253.scxml b/test/w3c/promela/test253.scxml index 467f7ff..d8777ca 100644 --- a/test/w3c/promela/test253.scxml +++ b/test/w3c/promela/test253.scxml @@ -9,7 +9,7 @@ this process uses the scxml processor to send the message to it, otherwise failu - + diff --git a/test/w3c/promela/test298.scxml b/test/w3c/promela/test298.scxml index 0f623b7..692b7da 100644 --- a/test/w3c/promela/test298.scxml +++ b/test/w3c/promela/test298.scxml @@ -6,7 +6,7 @@ - + diff --git a/test/w3c/promela/test311.scxml b/test/w3c/promela/test311.scxml index 7ee4a33..8453a82 100644 --- a/test/w3c/promela/test311.scxml +++ b/test/w3c/promela/test311.scxml @@ -3,7 +3,7 @@ - + diff --git a/test/w3c/promela/test338.scxml b/test/w3c/promela/test338.scxml index e7d97e4..46c702c 100644 --- a/test/w3c/promela/test338.scxml +++ b/test/w3c/promela/test338.scxml @@ -8,7 +8,7 @@ case where the invoke doesn't work correctly --> - + diff --git a/test/w3c/promela/test347.scxml b/test/w3c/promela/test347.scxml index 3b79584..4b70bcf 100644 --- a/test/w3c/promela/test347.scxml +++ b/test/w3c/promela/test347.scxml @@ -1,44 +1,40 @@ - - - - - + + + + + - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/test/w3c/promela/test350.scxml b/test/w3c/promela/test350.scxml index 7ae6fe8..d356f22 100644 --- a/test/w3c/promela/test350.scxml +++ b/test/w3c/promela/test350.scxml @@ -9,7 +9,7 @@ able to send an event to itself using its own session ID as the target --> - + diff --git a/test/w3c/promela/test351.scxml b/test/w3c/promela/test351.scxml index 956e006..5e2a5b0 100644 --- a/test/w3c/promela/test351.scxml +++ b/test/w3c/promela/test351.scxml @@ -7,7 +7,7 @@ - + @@ -22,7 +22,7 @@ - + diff --git a/test/w3c/promela/test352.scxml b/test/w3c/promela/test352.scxml index a964a04..a113c6a 100644 --- a/test/w3c/promela/test352.scxml +++ b/test/w3c/promela/test352.scxml @@ -6,7 +6,7 @@ - + diff --git a/test/w3c/promela/test354.scxml b/test/w3c/promela/test354.scxml index 91932ca..5a5d234 100644 --- a/test/w3c/promela/test354.scxml +++ b/test/w3c/promela/test354.scxml @@ -9,7 +9,7 @@ and that correct values are used --> - + @@ -31,7 +31,7 @@ and that correct values are used --> - + 123 diff --git a/test/w3c/promela/test364.scxml b/test/w3c/promela/test364.scxml index 44ba527..585754d 100644 --- a/test/w3c/promela/test364.scxml +++ b/test/w3c/promela/test364.scxml @@ -5,7 +5,7 @@ If we get to s01111 we succeed, if any other state, failure. --> - + diff --git a/test/w3c/promela/test372.scxml b/test/w3c/promela/test372.scxml index 6062428..481f348 100644 --- a/test/w3c/promela/test372.scxml +++ b/test/w3c/promela/test372.scxml @@ -7,7 +7,7 @@ Var1 should be set to 2 (but not 3) by the time the event is raised --> - + diff --git a/test/w3c/promela/test387.scxml b/test/w3c/promela/test387.scxml index 769d69b..9983f48 100644 --- a/test/w3c/promela/test387.scxml +++ b/test/w3c/promela/test387.scxml @@ -73,7 +73,7 @@ transition to s1's default deep history state. We should end up in s122, generat - + diff --git a/test/w3c/promela/test388.scxml b/test/w3c/promela/test388.scxml index c6ffffc..1f9971b 100644 --- a/test/w3c/promela/test388.scxml +++ b/test/w3c/promela/test388.scxml @@ -14,7 +14,7 @@ state is s011, so we should get entering.s011, otherwise failure.--> - + diff --git a/test/w3c/promela/test399.scxml b/test/w3c/promela/test399.scxml index 5f4548a..574d303 100644 --- a/test/w3c/promela/test399.scxml +++ b/test/w3c/promela/test399.scxml @@ -4,7 +4,7 @@ that the event attribute of transition may contain multiple event designators. - + diff --git a/test/w3c/promela/test402.scxml b/test/w3c/promela/test402.scxml index 3888751..5de6f9f 100644 --- a/test/w3c/promela/test402.scxml +++ b/test/w3c/promela/test402.scxml @@ -5,7 +5,7 @@ are pulled off the internal queue in order, and that prefix matching works on th - + diff --git a/test/w3c/promela/test403a.scxml b/test/w3c/promela/test403a.scxml index 5c8e398..7042e7b 100644 --- a/test/w3c/promela/test403a.scxml +++ b/test/w3c/promela/test403a.scxml @@ -10,7 +10,7 @@ matching transition in the child. --> - + diff --git a/test/w3c/promela/test403c.scxml b/test/w3c/promela/test403c.scxml index 335fc2e..909d675 100644 --- a/test/w3c/promela/test403c.scxml +++ b/test/w3c/promela/test403c.scxml @@ -7,7 +7,7 @@ - + diff --git a/test/w3c/promela/test405.scxml b/test/w3c/promela/test405.scxml index ce89b3a..7b61986 100644 --- a/test/w3c/promela/test405.scxml +++ b/test/w3c/promela/test405.scxml @@ -5,7 +5,7 @@ state machine is entered --> - + diff --git a/test/w3c/promela/test406.scxml b/test/w3c/promela/test406.scxml index 99c4c40..b6928b6 100644 --- a/test/w3c/promela/test406.scxml +++ b/test/w3c/promela/test406.scxml @@ -5,7 +5,7 @@ order when the transition in s01 is taken --> - + diff --git a/test/w3c/promela/test409.scxml b/test/w3c/promela/test409.scxml index 98e3c81..4ae15d7 100644 --- a/test/w3c/promela/test409.scxml +++ b/test/w3c/promela/test409.scxml @@ -5,7 +5,7 @@ be raised. Therefore the timeout should fire to indicate success --> - + diff --git a/test/w3c/promela/test411.scxml b/test/w3c/promela/test411.scxml index aae7e3c..20b119b 100644 --- a/test/w3c/promela/test411.scxml +++ b/test/w3c/promela/test411.scxml @@ -6,7 +6,7 @@ timeout also indicates failure --> - + diff --git a/test/w3c/promela/test412.scxml b/test/w3c/promela/test412.scxml index cc362be..564647b 100644 --- a/test/w3c/promela/test412.scxml +++ b/test/w3c/promela/test412.scxml @@ -4,7 +4,7 @@ and before the onentry handler of the child states. Event1, event2, and event3 - + diff --git a/test/w3c/promela/test416.scxml b/test/w3c/promela/test416.scxml index 763a48a..ee747f4 100644 --- a/test/w3c/promela/test416.scxml +++ b/test/w3c/promela/test416.scxml @@ -3,7 +3,7 @@ - + diff --git a/test/w3c/promela/test417.scxml b/test/w3c/promela/test417.scxml index abe4aa1..ed38eea 100644 --- a/test/w3c/promela/test417.scxml +++ b/test/w3c/promela/test417.scxml @@ -4,7 +4,7 @@ parallel elements children enter final states. --> - + diff --git a/test/w3c/promela/test422.scxml b/test/w3c/promela/test422.scxml index bc99d52..12cbf2f 100644 --- a/test/w3c/promela/test422.scxml +++ b/test/w3c/promela/test422.scxml @@ -12,7 +12,7 @@ in s11. So we should receive invokeS1, invokeS12, but not invokeS12. Furthermor - + diff --git a/test/w3c/promela/test423.scxml b/test/w3c/promela/test423.scxml index 6d87d30..5527d7f 100644 --- a/test/w3c/promela/test423.scxml +++ b/test/w3c/promela/test423.scxml @@ -4,7 +4,7 @@ - + diff --git a/test/w3c/promela/test501.scxml b/test/w3c/promela/test501.scxml index 02ae229..ea7f1ad 100644 --- a/test/w3c/promela/test501.scxml +++ b/test/w3c/promela/test501.scxml @@ -7,7 +7,7 @@ - + diff --git a/test/w3c/promela/test530.scxml b/test/w3c/promela/test530.scxml index c23eb9a..431802c 100644 --- a/test/w3c/promela/test530.scxml +++ b/test/w3c/promela/test530.scxml @@ -13,7 +13,7 @@ is evaluated at the right time, we should get invoke.done, otherwise an error - - + diff --git a/test/w3c/promela/test531.scxml b/test/w3c/promela/test531.scxml index 1e8cd15..d2ea9a6 100644 --- a/test/w3c/promela/test531.scxml +++ b/test/w3c/promela/test531.scxml @@ -4,7 +4,7 @@ of the raised event. --> - + diff --git a/test/w3c/promela/test532.scxml b/test/w3c/promela/test532.scxml index 69ffa54..356342d 100644 --- a/test/w3c/promela/test532.scxml +++ b/test/w3c/promela/test532.scxml @@ -4,7 +4,7 @@ as the name of the resulting event. --> - + some content diff --git a/test/w3c/promela/test553.scxml b/test/w3c/promela/test553.scxml index ad056a8..7f641d4 100644 --- a/test/w3c/promela/test553.scxml +++ b/test/w3c/promela/test553.scxml @@ -5,7 +5,7 @@ of 's args causes an error.. --> - + diff --git a/test/w3c/promela/test554.scxml b/test/w3c/promela/test554.scxml index b93888a..5832090 100644 --- a/test/w3c/promela/test554.scxml +++ b/test/w3c/promela/test554.scxml @@ -5,7 +5,7 @@ before the timer goes off. --> - + diff --git a/test/w3c/promela/test567.scxml b/test/w3c/promela/test567.scxml index 50eb4bd..5d99e88 100644 --- a/test/w3c/promela/test567.scxml +++ b/test/w3c/promela/test567.scxml @@ -7,7 +7,7 @@ _event.data. --> - + diff --git a/test/w3c/promela/test570.scxml b/test/w3c/promela/test570.scxml index 6ec678b..1a14640 100644 --- a/test/w3c/promela/test570.scxml +++ b/test/w3c/promela/test570.scxml @@ -6,7 +6,7 @@ - + diff --git a/test/w3c/promela/test576.scxml b/test/w3c/promela/test576.scxml index 1b40fd7..eeff4be 100644 --- a/test/w3c/promela/test576.scxml +++ b/test/w3c/promela/test576.scxml @@ -7,7 +7,7 @@ test that both are entered. --> - + diff --git a/test/w3c/promela/test579.scxml b/test/w3c/promela/test579.scxml index 20419d8..8ed8ac1 100644 --- a/test/w3c/promela/test579.scxml +++ b/test/w3c/promela/test579.scxml @@ -14,7 +14,7 @@ parent state has been visited and exited, the default history content must not b - + diff --git a/test/w3c/promela/test580.scxml b/test/w3c/promela/test580.scxml index ac1cbb7..34c5ae4 100644 --- a/test/w3c/promela/test580.scxml +++ b/test/w3c/promela/test580.scxml @@ -6,7 +6,7 @@ - + diff --git a/test/w3c/run_promela_test.cmake b/test/w3c/run_promela_test.cmake index 1200442..179cd68 100644 --- a/test/w3c/run_promela_test.cmake +++ b/test/w3c/run_promela_test.cmake @@ -12,7 +12,7 @@ if(CMD_RESULT) message(FATAL_ERROR "Error running ${SPIN_BIN}: ${CMD_RESULT}") endif() -execute_process(COMMAND ${GCC_BIN} -DMEMLIM=1024 -O2 -DXUSAFE -w -o ${OUTDIR}/pan ${OUTDIR}/pan.c RESULT_VARIABLE CMD_RESULT) +execute_process(COMMAND ${GCC_BIN} -DMEMLIM=1024 -DVECTORSZ=2048 -O2 -DXUSAFE -w -o ${OUTDIR}/pan ${OUTDIR}/pan.c RESULT_VARIABLE CMD_RESULT) if(CMD_RESULT) message(FATAL_ERROR "Error running ${GCC_BIN}: ${CMD_RESULT}") endif() -- cgit v0.12