summaryrefslogtreecommitdiffstats
path: root/src/uscxml
diff options
context:
space:
mode:
authorStefan Radomski <radomski@tk.informatik.tu-darmstadt.de>2014-12-01 11:02:40 (GMT)
committerStefan Radomski <radomski@tk.informatik.tu-darmstadt.de>2014-12-01 11:02:40 (GMT)
commitaf6609592298c5e047e37e5ae2b47e6a8edbb677 (patch)
treee6e7da1cd34dccf3fb4f389e684b7c899b12987a /src/uscxml
parentd2e90c02e5ad19a5857e7c7fb87f248182fdb32d (diff)
downloaduscxml-af6609592298c5e047e37e5ae2b47e6a8edbb677.zip
uscxml-af6609592298c5e047e37e5ae2b47e6a8edbb677.tar.gz
uscxml-af6609592298c5e047e37e5ae2b47e6a8edbb677.tar.bz2
Nested invokers and delayed events for PROMELA model checking
Diffstat (limited to 'src/uscxml')
-rw-r--r--src/uscxml/Interpreter.cpp10
-rw-r--r--src/uscxml/URL.cpp19
-rw-r--r--src/uscxml/URL.h5
-rw-r--r--src/uscxml/plugins/datamodel/promela/PromelaParser.cpp30
-rw-r--r--src/uscxml/plugins/datamodel/promela/PromelaParser.h20
-rw-r--r--src/uscxml/plugins/datamodel/promela/parser/promela.l17
-rw-r--r--src/uscxml/plugins/datamodel/promela/parser/promela.lex.yy.cpp199
-rw-r--r--src/uscxml/plugins/datamodel/promela/parser/promela.tab.cpp422
-rw-r--r--src/uscxml/plugins/datamodel/promela/parser/promela.tab.hpp15
-rw-r--r--src/uscxml/plugins/datamodel/promela/parser/promela.ypp37
-rw-r--r--src/uscxml/transform/ChartToFSM.cpp34
-rw-r--r--src/uscxml/transform/ChartToFSM.h2
-rw-r--r--src/uscxml/transform/ChartToPromela.cpp1019
-rw-r--r--src/uscxml/transform/ChartToPromela.h50
14 files changed, 1438 insertions, 441 deletions
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<std::string>& element) {
sendReq.delayMs = strTo<uint32_t>(delayAttr.value);
} else if (iequals(delayAttr.unit, "s")) {
sendReq.delayMs = strTo<double>(delayAttr.value) * 1000;
+ } else if (delayAttr.unit.length() == 0) { // unit less delay is interpreted as milliseconds
+ sendReq.delayMs = strTo<uint32_t>(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<std::string> InterpreterImpl::filterChildElements(const std::string& tag
return filteredChildElems;
}
+
NodeSet<std::string> InterpreterImpl::filterChildType(const Node_base::Type type, const NodeSet<std::string>& nodeSet, bool recurse) {
NodeSet<std::string> 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<CURL*, URL> _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<PromelaParserNode*>::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<PromelaParserNode*>::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<PromelaParserNode*> 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<std::string> ChartToFSM::refsToTransitions(const std::se
}
return transitions;
}
-
-#if 0
-void ChartToFSM::labelTransitions() {
- // put a unique id on each transition
- Arabica::XPath::NodeSet<std::string> states = getAllStates();
- states.push_back(_scxml);
- for (int i = 0; i < states.size(); i++) {
- Arabica::DOM::Element<std::string> stateElem = Arabica::DOM::Element<std::string>(states[i]);
- std::string stateId = ATTR(stateElem, "id");
- NodeSet<std::string> transitions = filterChildElements(_nsInfo.xmlNSPrefix + "transition", stateElem);
- // some transitions are in the inital elements
- NodeSet<std::string> initials = filterChildElements(_nsInfo.xmlNSPrefix + "initial", stateElem);
- transitions.push_back(filterChildElements(_nsInfo.xmlNSPrefix + "transition", initials));
- for (int j = 0; j < transitions.size(); j++) {
- Element<std::string> transition = Element<std::string>(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<std::string>& activeState
const std::string& xmlNSPrefix,
ChartToFSM* flattener) {
interpreter = flattener;
-
+ activeIndex = -1;
+
// take references
for (int i = 0; i < activeStates_.size(); i++) {
activeStatesRefs.insert(strTo<int>(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<std::string, std::string>::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<std::string, std::string>::const_iterator litIter = _strMacroNames.begin(); litIter != _strMacroNames.end(); litIter++) {
+// boost::replace_all(replaced, "'" + litIter->first + "'", litIter->second);
+// }
+// boost::replace_all(replaced, "_event", prefix + "_event");
+ // replace all variables from analyzer
+
+ std::string processed = code;
+ std::stringstream processedStr;
+ std::list<std::pair<size_t, size_t> > posList;
+ std::list<std::pair<size_t, size_t> >::iterator posIter;
+ size_t lastPos;
+
+ // prepend all identifiers with our prefix
+ {
+ PromelaParser parsed(processed);
+// parsed.dump();
+ posList = getTokenPositions(code, PML_NAME, parsed.ast);
+ posList.sort();
+ posIter = posList.begin();
+ lastPos = 0;
+
+ while (posIter != posList.end()) {
+ processedStr << code.substr(lastPos, posIter->first - lastPos) << prefix;
+ lastPos = posIter->first;
+ posIter++;
+ }
+ processedStr << processed.substr(lastPos, processed.size() - lastPos);
+
+ processed = processedStr.str();
+ processedStr.clear();
+ processedStr.str("");
}
- 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<size_t> posList = getTokenPositions(expr, PML_NAME, parsed.ast);
+// posList.sort();
+//
+// std::stringstream prefixed;
+// std::list<size_t>::iterator posIter = posList.begin();
+// size_t lastPos = 0;
+// while (posIter != posList.end()) {
+// prefixed << expr.substr(lastPos, *posIter - lastPos) << prefix;
+// lastPos = *posIter;
+// posIter++;
+// }
+//
+// prefixed << expr.substr(lastPos, expr.size() - lastPos);
+// return prefixed.str();
+//}
+
+std::list<std::pair<size_t, size_t> > PromelaCodeAnalyzer::getTokenPositions(const std::string& expr, int type, PromelaParserNode* ast) {
+ std::list<std::pair<size_t, size_t> > posList;
+ if (ast->type == type && ast->loc != NULL) {
+// ast->dump();
+ if (type == PML_NAME && ast->parent &&
+ ((ast->parent->type == PML_CMPND && ast->parent->operands.front() != ast) ||
+ (ast->parent->parent && ast->parent->type == PML_VAR_ARRAY && ast->parent->parent->type == PML_CMPND))) {
+ // field in a compound
+ } else {
+ if (ast->loc->firstLine == 0) {
+ posList.push_back(std::make_pair(ast->loc->firstCol, ast->loc->lastCol));
+ } else {
+ int line = ast->loc->firstLine;
+ size_t lastPos = 0;
+ while(line > 0) {
+ lastPos = expr.find_first_of('\n', lastPos + 1);
+ line--;
+ }
+ posList.push_back(std::make_pair(lastPos + ast->loc->firstCol, lastPos + ast->loc->lastCol));
+ }
+ }
+ }
+ for (std::list<PromelaParserNode*>::iterator opIter = ast->operands.begin(); opIter != ast->operands.end(); opIter++) {
+ std::list<std::pair<size_t, size_t> > tmp = getTokenPositions(expr, type, *opIter);
+ posList.merge(tmp);
+ }
+ return posList;
+}
+
std::set<std::string> PromelaCodeAnalyzer::getEventsWithPrefix(const std::string& prefix) {
std::set<std::string> eventNames;
std::list<TrieNode*> trieNodes = _eventTrie.getWordsWithPrefix(prefix);
@@ -559,14 +667,23 @@ std::set<std::string> PromelaCodeAnalyzer::getEventsWithPrefix(const std::string
return eventNames;
}
+ChartToPromela::~ChartToPromela() {
+ if (_analyzer != NULL)
+ delete(_analyzer);
+ for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator nestedIter = _machines.begin(); nestedIter != _machines.end(); nestedIter++) {
+ nestedIter->second->_analyzer = NULL;
+ delete (nestedIter->second);
+ }
+}
+
void ChartToPromela::writeEvents(std::ostream& stream) {
- std::map<std::string, int> events = _analyzer.getEvents();
+ std::map<std::string, int> events = _analyzer->getEvents();
std::map<std::string, int>::iterator eventIter = events.begin();
stream << "/* event name identifiers */" << std::endl;
while(eventIter != events.end()) {
if (eventIter->first.length() > 0) {
- stream << "#define " << _analyzer.macroForLiteral(eventIter->first) << " " << _analyzer.indexForLiteral(eventIter->first);
+ stream << "#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<std::string, GlobalState*>::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<std::string, int> origStates = _analyzer.getOrigStates();
+ std::map<std::string, int> origStates = _analyzer->getOrigStates();
for (std::map<std::string, int>::iterator origIter = origStates.begin(); origIter != origStates.end(); origIter++) {
- stream << "#define " << _analyzer.macroForLiteral(origIter->first) << " " << origIter->second;
+ stream << "#define " << _analyzer->macroForLiteral(origIter->first) << " " << origIter->second;
stream << " /* from \"" << origIter->first << "\" */" << std::endl;
}
-// std::map<std::string, int> states = _analyzer.getStates();
+// std::map<std::string, int> states = _analyzer->getStates();
// size_t stateIndex = 0;
// for (std::map<std::string, int>::iterator stateIter = states.begin(); stateIter != states.end(); stateIter++) {
// stream << "_x"
-// std::list<std::string> origStates = _analyzer.getOrigState(stateIter->first);
+// std::list<std::string> origStates = _analyzer->getOrigState(stateIter->first);
// size_t origIndex = 0;
// for (std::list<std::string>::iterator origIter = origStates.begin(); origIter != origStates.end(); origIter++) {
//
@@ -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<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator tIter = currDef.types.begin(); tIter != currDef.types.end(); tIter++) {
+ if (currDef.name.compare("_event_t") == 0 && (tIter->first.compare("name") == 0 ||
+ tIter->first.compare("seqNr") == 0 ||
+ tIter->first.compare("invokeid") == 0 ||
+ tIter->first.compare("delay") == 0)) { // special treatment for _event
+ continue;
+ }
if (currDef.name.compare("_x_t") == 0 && tIter->first.compare("states") == 0) {
- stream << " bool states[" << _analyzer.getOrigStates().size() << "];" << std::endl;
+ 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<std::string, PromelaCodeAnalyzer::PromelaTypedef>::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::set<GlobalTransitio
while(histItemIter != relevanthistIter->second.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<std::string> namelist = tokenize(ATTR_CAST(action.invoke, "namelist"));
+ for (std::list<std::string>::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<std::string> 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<std::string>::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<std::string>::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<std::string>::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<std::string> nodeElem = Arabica::DOM::Element<std::string>(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<std::string> child = node.getFirstChild();
while(child) {
@@ -1352,7 +1561,7 @@ void ChartToPromela::writeExecutableContent(std::ostream& stream, const Arabica:
} else if(TAGNAME(nodeElem) == "script") {
NodeSet<std::string> 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<std::string> 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<std::string> 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<std::string> 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<std::string> paramElem = Element<std::string>(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<std::string> nameListIds = tokenizeIdRefs(sendNameList);
std::list<std::string>::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<std::string> contentElem = Element<std::string>(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<std::string>& 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<ChartToPromela*> others;
+ others.push_back(topMachine);
+ for (std::map<Arabica::DOM::Node<std::string>, 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<ChartToPromela*>::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<ChartToPromela*>::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<std::string>& node, bool recurse) {
PromelaInlines allPromInls;
Arabica::XPath::NodeSet<std::string> 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<std::string> 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<std::string> literals = _analyzer.getLiterals();
- std::map<std::string, int> events = _analyzer.getEvents();
- std::map<std::string, int> origStates = _analyzer.getOrigStates();
+ std::set<std::string> literals = _analyzer->getLiterals();
+ std::map<std::string, int> events = _analyzer->getEvents();
+ std::map<std::string, int> origStates = _analyzer->getOrigStates();
for (std::set<std::string>::const_iterator litIter = literals.begin(); litIter != literals.end(); litIter++) {
- if (events.find(*litIter) == events.end() && (origStates.find(*litIter) == origStates.end() || !_analyzer.usesInPredicate()))
- stream << "#define " << _analyzer.macroForLiteral(*litIter) << " " << _analyzer.indexForLiteral(*litIter) << " /* " << *litIter << " */" << std::endl;
+ 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<std::string> 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<std::string> 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<std::string, PromelaCodeAnalyzer::PromelaTypedef>::iterator typeIter = allTypes.types.begin();
while(typeIter != allTypes.types.end()) {
+ if (typeIter->second.occurrences.find(this) == typeIter->second.occurrences.end()) {
+ typeIter++;
+ continue;
+ }
+
if (processedIdentifiers.find(typeIter->first) != processedIdentifiers.end()) {
typeIter++;
continue;
@@ -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<std::string>& 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<std::string> namelist = tokenize(ATTR_CAST(node, "namelist"));
+ for (std::list<std::string>::iterator nlIter = namelist.begin(); nlIter != namelist.end(); nlIter++) {
+ if (invoker->_dataModelVars.find(*nlIter) != invoker->_dataModelVars.end()) {
+ stream << padding << invoker->_prefix << *nlIter << " = " << _prefix << *nlIter << std::endl;
+ }
+ }
+ }
+
+ // set from params
+ NodeSet<std::string> invokeParams = 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<std::string> 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<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator machIter = _machines.begin(); machIter != _machines.end(); machIter++) {
+ stream << " :: invokerId == " << _analyzer->macroForLiteral(machIter->second->_invokerid) << " -> {" << std::endl;
+ writeStartInvoker(stream, machIter->first, machIter->second, 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<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator queueIter = _machinesAll->begin(); queueIter != _machinesAll->end(); queueIter++) {
+ std::list<std::string> queues;
+ queues.push_back("eQ");
+ queues.push_back("tmpQ");
+ for (std::list<std::string>::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 << "?<tmpE>;" << 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<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator invIter = _machines.begin(); invIter != _machines.end(); invIter++) {
+ NodeSet<std::string> finalizes = filterChildElements(_nsInfo.xmlNSPrefix + "finalize", invIter->first, false);
+ if (finalizes.size() > 0) {
+ finalizeFound = true;
+ break;
+ }
+ }
+ if (finalizeFound) {
+ stream << " /* <finalize> event */" << std::endl;
+ stream << " if" << std::endl;
+ for (std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator invIter = _machines.begin(); invIter != _machines.end(); invIter++) {
+ NodeSet<std::string> finalizes = 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<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator invIter = _machines.begin(); invIter != _machines.end(); invIter++) {
+ if (invIter->second == this) {
+ continue;
+ }
+ //std::cout << invIter->first << std::endl;
+ if (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<ChartToPromela*> others;
+ others.push_back(invoker->_parent);
+ for (std::map<Arabica::DOM::Node<std::string>, 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<ChartToPromela*>::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<std::string, GlobalState*>::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::list<Globa
if (transitions.size() == 0) {
stream << "/* no transition applicable */" << std::endl;
- stream << padding << "spontaneous = false;" << std::endl;
- stream << padding << "goto macroStep;" << std::endl;
+ stream << padding << _prefix << "spontaneous = false;" << std::endl;
+ stream << padding << "goto " << _prefix << "macroStep;" << std::endl;
return;
}
@@ -1972,10 +2525,10 @@ void ChartToPromela::writeDispatchingBlock(std::ostream& stream, std::list<Globa
}
if (currTrans->isEventless) {
- stream << "spontaneous";
+ stream << _prefix << "spontaneous";
} else {
std::string eventDescs = currTrans->eventDesc;
-
+
std::list<std::string> eventNames = tokenizeIdRefs(eventDescs);
std::set<std::string> eventPrefixes;
std::list<std::string>::iterator eventNameIter = eventNames.begin();
@@ -1986,34 +2539,44 @@ void ChartToPromela::writeDispatchingBlock(std::ostream& stream, std::list<Globa
if (boost::ends_with(eventDesc, "."))
eventDesc = eventDesc.substr(0, eventDesc.size() - 1);
if (eventDesc.length() > 0) {
- std::set<std::string> tmp = _analyzer.getEventsWithPrefix(*eventNameIter);
+ std::set<std::string> 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<std::string>::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::list<Globa
PRETTY_PRINT_LIST(stream, flatActiveSource.getActive());
stream << " */" << std::endl;
- stream << padding << " goto t" << currTrans->index << ";" << 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::list<Globa
PRETTY_PRINT_LIST(stream, flatActiveDest.getActive());
stream << " */" << std::endl;
- stream << padding << " s = s" << newState->index << ";" << 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<std::string>::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<Arabica::DOM::Node<std::string>, ChartToPromela*>();
+ (*_machinesAll)[_scxml] = this;
+ }
+
+ if (_machinesAllPerId == NULL)
+ _machinesAllPerId = new std::map<std::string, Arabica::DOM::Node<std::string> >();
+
+ if (_parentTopMost == NULL)
+ _parentTopMost = this;
_internalQueueLength = getMinInternalQueueLength(MSG_QUEUE_LENGTH);
_externalQueueLength = getMinExternalQueueLength(MSG_QUEUE_LENGTH);
@@ -2081,10 +2658,86 @@ void ChartToPromela::initNodes() {
if (InterpreterImpl::isInEmbeddedDocument(states[i]))
continue;
Element<std::string> 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<std::string> 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<std::string> invokeElem(invokes[i]);
+ invokeElem.setAttribute("id", "INV_" + UUID::getUUID().substr(0,5));
+ } else if (HAS_ATTR_CAST(invokes[i], "id") && UUID::isUUID(ATTR_CAST(invokes[i], "id"))) {
+ // shorten UUIDs
+ Element<std::string> invokeElem(invokes[i]);
+ invokeElem.setAttribute("id", "INV_" + ATTR_CAST(invokes[i], "id").substr(0,5));
+ }
}
+
+ }
+
+ // are there nestes SCXML invokers?
+ {
+ NodeSet<std::string> invokes = 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<std::string>(invokes[i]).setAttribute("name", ATTR_CAST(invokes[i], "id"));
+
+ _prefix = "MAIN_";
+ Interpreter nested;
+ if (HAS_ATTR_CAST(invokes[i], "src")) {
+ URL absUrl(ATTR_CAST(invokes[i], "src"));
+ absUrl.toAbsolute(_baseURI);
+ nested = Interpreter::fromURI(absUrl);
+
+ } else {
+ NodeSet<std::string> nestedContent = InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "content", invokes[i]);
+ assert(nestedContent.size() == 1);
+ NodeSet<std::string> nestedRoot = InterpreterImpl::filterChildElements(_nsInfo.xmlNSPrefix + "scxml", nestedContent[0]);
+ assert(nestedRoot.size() == 1);
+
+ DOMImplementation<std::string> domFactory = Arabica::SimpleDOM::DOMImplementation<std::string>::getDOMImplementation();
+ Document<std::string> nestedDoc = domFactory.createDocument(_scxml.getOwnerDocument().getNamespaceURI(), "", 0);
+ Node<std::string> importRoot = nestedDoc.importNode(nestedRoot[0], true);
+ nestedDoc.appendChild(importRoot);
+
+ nested = Interpreter::fromDOM(nestedDoc, _nsInfo);
+ }
+
+// 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<std::string> invokes = filterChildElements(_nsInfo.xmlNSPrefix + "invoke", _scxml, true);
NodeSet<std::string> 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<std::string> 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<std::string> content = filterChildElements(_nsInfo.xmlNSPrefix + "content", withContent[i], true);
+ for (int j = 0; j < content.size(); j++) {
+ Element<std::string> contentElem(content[j]);
+ std::string content = spaceNormalize(contentElem.getFirstChild().getNodeValue());
+ if (!isNumeric(content.c_str(), 10))
+ _analyzer->addLiteral(content);
+ }
+ }
+ }
// external event names from comments and event sources
NodeSet<std::string> promelaEventSourceComments;
NodeSet<std::string> invokers = _xpath.evaluate("//" + _nsInfo.xpathPrefix + "invoke", _scxml).asNodeSet();
@@ -2158,22 +2829,22 @@ void ChartToPromela::initNodes() {
for ( std::list<PromelaInline>::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<std::string> invoker = Element<std::string>(promelaEventSourceComments[i].getParentNode());
+ Element<std::string> invoker = Element<std::string>(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<std::string> contents = filterChildElements(_nsInfo.xmlNSPrefix + "content", _scxml, true);
@@ -2193,7 +2864,7 @@ void ChartToPromela::initNodes() {
Element<std::string> contentElem = Element<std::string>(contents[i]);
if (contentElem.hasChildNodes() && contentElem.getFirstChild().getNodeType() == Node_base::TEXT_NODE && contentElem.getChildNodes().getLength() == 1) {
std::string content = contentElem.getFirstChild().getNodeValue();
- _analyzer.addLiteral(spaceNormalize(content));
+ _analyzer->addLiteral(spaceNormalize(content));
}
}
@@ -2264,7 +2935,7 @@ void ChartToPromela::initNodes() {
}
}
for (std::set<std::string>::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<std::string> names = tokenizeIdRefs(namelist);
for (std::list<std::string>::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<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator nestedIter = _machines.begin(); nestedIter != _machines.end(); nestedIter++) {
+ if (nestedIter->second->_start == NULL) {
+ nestedIter->second->interpret();
+ }
+ nestedIter->second->initNodes();
+ }
+
writeEvents(stream);
stream << std::endl;
writeStates(stream);
stream << std::endl;
- 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<Arabica::DOM::Node<std::string>, 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<Arabica::DOM::Node<std::string>, ChartToPromela*>::iterator nestedIter = _machines.begin(); nestedIter != _machines.end(); nestedIter++) {
+ nestedIter->second->writeFSM(stream);
+ stream << std::endl;
+ }
+
// write ltl expression for success
std::stringstream acceptingStates;
std::string seperator;
@@ -2357,7 +3046,7 @@ void ChartToPromela::writeProgram(std::ostream& stream) {
for (std::map<std::string, GlobalState*>::iterator stateIter = _activeConf.begin(); stateIter != _activeConf.end(); stateIter++) {
FlatStateIdentifier flatId(stateIter->first);
if (std::find(flatId.getActive().begin(), flatId.getActive().end(), "pass") != flatId.getActive().end()) {
- acceptingStates << seperator << "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<std::string> container;
std::list<std::list<std::string> > sequences;
@@ -132,7 +135,8 @@ public:
size_t minValue;
size_t maxValue;
std::map<std::string, PromelaTypedef> types;
-
+ std::set<ChartToPromela*> 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<std::pair<size_t, size_t> > getTokenPositions(const std::string& expr, int type, PromelaParserNode* ast);
PromelaTypedef& getTypes() {
return _typeDefs;
@@ -205,9 +220,8 @@ protected:
std::map<std::string, int> _states;
std::map<std::string, int> _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<std::string>& condChain, int indent = 0);
void writeDispatchingBlock(std::ostream& stream, std::list<GlobalTransition*>, int indent = 0);
+ void writeStartInvoker(std::ostream& stream, const Arabica::DOM::Node<std::string>& 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<std::string>& cancel, ChartToPromela* invoker, int indent = 0);
+
Arabica::XPath::NodeSet<std::string> getTransientContent(const Arabica::DOM::Element<std::string>& state, const std::string& source = "");
//Arabica::DOM::Node<std::string> getUltimateTarget(const Arabica::DOM::Element<std::string>& transition);
@@ -314,7 +332,7 @@ protected:
std::list<std::string> _varInitializers; // pending initializations for arrays
- PromelaCodeAnalyzer _analyzer;
+ PromelaCodeAnalyzer* _analyzer;
uint32_t _externalQueueLength;
uint32_t _internalQueueLength;
@@ -323,7 +341,19 @@ protected:
PromelaEventSource _globalEventSource;
std::map<std::string, std::map<std::string, size_t> > _historyMembers; // ids of all history states
-
+ std::set<std::string> _dataModelVars;
+
+ Arabica::DOM::Node<std::string> _finalize;
+ std::map<Arabica::DOM::Node<std::string>, ChartToPromela*> _machines;
+ std::map<Arabica::DOM::Node<std::string>, ChartToPromela*>* _machinesAll;
+ ChartToPromela* _parent; // our invoking interpreter
+ ChartToPromela* _parentTopMost;
+
+ std::map<std::string, Arabica::DOM::Node<std::string> > _machinesPerId;
+ std::map<std::string, Arabica::DOM::Node<std::string> >* _machinesAllPerId;
+ std::string _prefix; // our prefix in case of nested SCXML documents
+ std::string _invokerid;
+
friend class PromelaEventSource;
};
generated by cgit v0.12 at 2024-08-25 23:17:02 (GMT)