Started with promela datamodel

18 files changed, 5751 insertions, 14 deletions

diff --git a/src/uscxml/plugins/datamodel/CMakeLists.txt b/src/uscxml/plugins/datamodel/CMakeLists.txt
index 3e2aaae..4e5ef00 100644
--- a/src/uscxml/plugins/datamodel/CMakeLists.txt
+++ b/src/uscxml/plugins/datamodel/CMakeLists.txt
@@ -137,6 +137,31 @@ if (SWI_FOUND AND BUILD_DM_PROLOG)
 	endif()
 endif()
 
+
+# Promela datamodel
+
+if (BUILD_DM_PROMELA)
+	set(USCXML_DATAMODELS "promela ${USCXML_DATAMODELS}")
+	
+	file(GLOB_RECURSE PROMELA_DATAMODEL
+		promela/*.cpp
+		promela/*.c
+		promela/*.h
+	)
+	if (BUILD_AS_PLUGINS)
+		source_group("" FILES PROMELA_DATAMODEL)
+		add_library(
+			datamodel_promela SHARED 
+			${PROMELA_DATAMODEL}
+			"../Plugins.cpp")
+		target_link_libraries(datamodel_promela uscxml)
+		set_target_properties(datamodel_promela PROPERTIES FOLDER "Plugin DataModel")
+	else()
+		list (APPEND USCXML_FILES ${PROMELA_DATAMODEL})
+	endif()
+endif()
+
+
 set(USCXML_INCLUDE_DIRS ${USCXML_INCLUDE_DIRS} PARENT_SCOPE)
 set(USCXML_FILES ${USCXML_FILES} PARENT_SCOPE)
 set(USCXML_DATAMODELS ${USCXML_DATAMODELS} PARENT_SCOPE)
diff --git a/src/uscxml/plugins/datamodel/ecmascript/JavaScriptCore/JSCDataModel.cpp b/src/uscxml/plugins/datamodel/ecmascript/JavaScriptCore/JSCDataModel.cpp
index ad2952a..dece4f2 100644
--- a/src/uscxml/plugins/datamodel/ecmascript/JavaScriptCore/JSCDataModel.cpp
+++ b/src/uscxml/plugins/datamodel/ecmascript/JavaScriptCore/JSCDataModel.cpp
@@ -628,6 +628,27 @@ void JSCDataModel::init(const std::string& location, const Data& data) {
 	}
 }
 
+std::string JSCDataModel::andExpressions(std::list<std::string> expressions) {
+
+	if (expressions.size() == 0)
+		return "";
+	
+	if (expressions.size() == 1)
+		return *(expressions.begin());
+	
+	std::ostringstream exprSS;
+	exprSS << "(";
+	std::string conjunction = "";
+	for (std::list<std::string>::const_iterator exprIter = expressions.begin();
+			 exprIter != expressions.end();
+			 exprIter++) {
+		exprSS << conjunction << "(" << *exprIter << ")";
+		conjunction = " && ";
+	}
+	exprSS << ")";
+	return exprSS.str();
+}
+
 void JSCDataModel::handleException(JSValueRef exception) {
 	JSStringRef exceptionStringRef = JSValueToStringCopy(_ctx, exception, NULL);
 	size_t maxSize = JSStringGetMaximumUTF8CStringSize(exceptionStringRef);
@@ -685,7 +706,7 @@ JSValueRef JSCDataModel::jsIn(JSContextRef ctx, JSObjectRef function, JSObjectRe
 			std::string stateName(buffer);
 			free(buffer);
 
-			if (Interpreter::isMember(INSTANCE->_interpreter->getState(stateName), INSTANCE->_interpreter->getConfiguration())) {
+			if (INSTANCE->_interpreter->isInState(stateName)) {
 				continue;
 			}
 		}
diff --git a/src/uscxml/plugins/datamodel/ecmascript/JavaScriptCore/JSCDataModel.h b/src/uscxml/plugins/datamodel/ecmascript/JavaScriptCore/JSCDataModel.h
index c79c29e..7443439 100644
--- a/src/uscxml/plugins/datamodel/ecmascript/JavaScriptCore/JSCDataModel.h
+++ b/src/uscxml/plugins/datamodel/ecmascript/JavaScriptCore/JSCDataModel.h
@@ -79,6 +79,8 @@ public:
 	                  const std::string& content);
 	virtual void init(const std::string& location, const Data& data);
 
+	virtual std::string andExpressions(std::list<std::string>);
+
 protected:
 	Arabica::DOM::JSCDOM* _dom;
 
diff --git a/src/uscxml/plugins/datamodel/ecmascript/v8/V8DataModel.cpp b/src/uscxml/plugins/datamodel/ecmascript/v8/V8DataModel.cpp
index e7c0c72..1341d09 100644
--- a/src/uscxml/plugins/datamodel/ecmascript/v8/V8DataModel.cpp
+++ b/src/uscxml/plugins/datamodel/ecmascript/v8/V8DataModel.cpp
@@ -438,7 +438,7 @@ v8::Handle<v8::Value> V8DataModel::jsIn(const v8::Arguments& args) {
 	for (unsigned int i = 0; i < args.Length(); i++) {
 		if (args[i]->IsString()) {
 			std::string stateName(*v8::String::AsciiValue(args[i]->ToString()));
-			if (Interpreter::isMember(INSTANCE->_interpreter->getState(stateName), INSTANCE->_interpreter->getConfiguration())) {
+			if (INSTANCE->_interpreter->isInState(stateName)) {
 				continue;
 			}
 		}
@@ -658,6 +658,25 @@ void V8DataModel::init(const std::string& location,
 	}
 }
 
+std::string V8DataModel::andExpressions(std::list<std::string> expressions) {
+	if (expressions.size() == 0)
+		return "";
+	
+	if (expressions.size() == 1)
+		return *(expressions.begin());
+
+	std::ostringstream exprSS;
+	exprSS << "(";
+	std::string conjunction = "";
+	for (std::list<std::string>::const_iterator exprIter = expressions.begin();
+			 exprIter != expressions.end();
+			 exprIter++) {
+		exprSS << conjunction << "(" << *exprIter << ")";
+		conjunction = " && ";
+	}
+	exprSS << ")";
+	return exprSS.str();
+}
 
 v8::Handle<v8::Value> V8DataModel::evalAsValue(const std::string& expr, bool dontThrow) {
 	v8::TryCatch tryCatch;
diff --git a/src/uscxml/plugins/datamodel/ecmascript/v8/V8DataModel.h b/src/uscxml/plugins/datamodel/ecmascript/v8/V8DataModel.h
index 0a64a2e..a0a1b09 100644
--- a/src/uscxml/plugins/datamodel/ecmascript/v8/V8DataModel.h
+++ b/src/uscxml/plugins/datamodel/ecmascript/v8/V8DataModel.h
@@ -80,6 +80,8 @@ public:
 	virtual void init(const std::string& location,
 	                  const Data& data);
 
+	virtual std::string andExpressions(std::list<std::string>);
+
 	virtual Data getStringAsData(const std::string& content);
 	virtual Data getValueAsData(const v8::Handle<v8::Value>& value,
 	                            std::set<v8::Value*>& alreadySeen);
diff --git a/src/uscxml/plugins/datamodel/null/NULLDataModel.cpp b/src/uscxml/plugins/datamodel/null/NULLDataModel.cpp
index 1938b0c..9594d5e 100644
--- a/src/uscxml/plugins/datamodel/null/NULLDataModel.cpp
+++ b/src/uscxml/plugins/datamodel/null/NULLDataModel.cpp
@@ -131,7 +131,7 @@ bool NULLDataModel::evalAsBool(const Arabica::DOM::Node<std::string>& node, cons
 			stateName = stateExprs[i];
 		}
 
-		if (Interpreter::isMember(_interpreter->getState(stateName), _interpreter->getConfiguration())) {
+		if (_interpreter->isInState(stateName)) {
 			continue;
 		}
 		return false;
diff --git a/src/uscxml/plugins/datamodel/prolog/swi/SWIDataModel.cpp b/src/uscxml/plugins/datamodel/prolog/swi/SWIDataModel.cpp
index 5e66c68..133925e 100644
--- a/src/uscxml/plugins/datamodel/prolog/swi/SWIDataModel.cpp
+++ b/src/uscxml/plugins/datamodel/prolog/swi/SWIDataModel.cpp
@@ -196,11 +196,8 @@ foreign_t SWIDataModel::inPredicate(term_t a0, int arity, void* context) {
 	try {
 		char *s;
 		if ( PL_get_atom_chars(a0, &s) ) {
-			NodeSet<std::string> config = _dmPtr->_interpreter->getConfiguration();
-			for (int i = 0; i < config.size(); i++) {
-				if (HAS_ATTR(config[i], "id") && strcmp(ATTR(config[i], "id").c_str(), s) == 0) {
-					return TRUE;
-				}
+			if (_dmPtr->_interpreter->isInState(s)) {
+        return true;
 			}
 		}
 		return FALSE;
diff --git a/src/uscxml/plugins/datamodel/promela/PromelaDataModel.cpp b/src/uscxml/plugins/datamodel/promela/PromelaDataModel.cpp
new file mode 100644
index 0000000..f75677e
--- /dev/null
+++ b/src/uscxml/plugins/datamodel/promela/PromelaDataModel.cpp
@@ -0,0 +1,332 @@
+/**
+ *  @file
+ *  @author     2012-2014 Stefan Radomski (stefan.radomski@cs.tu-darmstadt.de)
+ *  @copyright  Simplified BSD
+ *
+ *  @cond
+ *  This program is free software: you can redistribute it and/or modify
+ *  it under the terms of the FreeBSD license as published by the FreeBSD
+ *  project.
+ *
+ *  This program is distributed in the hope that it will be useful,
+ *  but WITHOUT ANY WARRANTY; without even the implied warranty of
+ *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
+ *
+ *  You should have received a copy of the FreeBSD license along with this
+ *  program. If not, see <http://www.opensource.org/licenses/bsd-license>.
+ *  @endcond
+ */
+
+#include <boost/algorithm/string.hpp>
+
+#include "uscxml/Common.h"
+#include "uscxml/config.h"
+#include "PromelaDataModel.h"
+#include "uscxml/DOMUtils.h"
+#include "uscxml/Message.h"
+#include <glog/logging.h>
+#include <cctype>
+
+// #include "PromelaAssignParser.h"
+//#include "PromelaExprParser.h"
+// #include "PromelaStmntParser.h"
+#include "PromelaParser.h"
+
+#ifdef BUILD_AS_PLUGINS
+#include <Pluma/Connector.hpp>
+#endif
+
+namespace uscxml {
+
+using namespace Arabica::XPath;
+using namespace Arabica::DOM;
+
+#ifdef BUILD_AS_PLUGINS
+PLUMA_CONNECTOR
+bool pluginConnect(pluma::Host& host) {
+	host.add( new PromelaDataModelProvider() );
+	return true;
+}
+#endif
+
+PromelaDataModel::PromelaDataModel() {
+}
+
+PromelaDataModel::~PromelaDataModel() {
+}
+
+boost::shared_ptr<DataModelImpl> PromelaDataModel::create(InterpreterImpl* interpreter) {
+	boost::shared_ptr<PromelaDataModel> dm = boost::shared_ptr<PromelaDataModel>(new PromelaDataModel());
+	dm->_interpreter = interpreter;
+	return dm;
+}
+
+void PromelaDataModel::registerIOProcessor(const std::string& name, const IOProcessor& ioprocessor) {
+//	std::cout << "PromelaDataModel::registerIOProcessor" << std::endl;
+}
+
+void PromelaDataModel::setSessionId(const std::string& sessionId) {
+//	std::cout << "PromelaDataModel::setSessionId" << std::endl;
+	_sessionId = sessionId;
+}
+
+void PromelaDataModel::setName(const std::string& name) {
+//	std::cout << "PromelaDataModel::setName" << std::endl;
+	_name = name;
+}
+
+void PromelaDataModel::pushContext() {
+//	std::cout << "PromelaDataModel::pushContext" << std::endl;
+}
+
+void PromelaDataModel::popContext() {
+//	std::cout << "PromelaDataModel::popContext" << std::endl;
+}
+
+void PromelaDataModel::initialize() {
+//	std::cout << "PromelaDataModel::initialize" << std::endl;
+}
+
+void PromelaDataModel::setEvent(const Event& event) {
+	_event = event;
+}
+
+Data PromelaDataModel::getStringAsData(const std::string& content) {
+	return expressionToAST(content);
+}
+
+
+bool PromelaDataModel::validate(const std::string& location, const std::string& schema) {
+//	std::cout << "PromelaDataModel::validate" << std::endl;
+	return true;
+}
+
+uint32_t PromelaDataModel::getLength(const std::string& expr) {
+	return 0;
+}
+
+void PromelaDataModel::setForeach(const std::string& item,
+                              const std::string& array,
+                              const std::string& index,
+                              uint32_t iteration) {
+}
+
+void PromelaDataModel::eval(const Element<std::string>& scriptElem, const std::string& expr) {
+	expressionToAST(expr);
+}
+
+bool PromelaDataModel::evalAsBool(const std::string& expr) {
+	return evalAsBool(Arabica::DOM::Node<std::string>(), expr);
+}
+
+bool PromelaDataModel::evalAsBool(const Arabica::DOM::Node<std::string>& node, const std::string& expr) {
+	PromelaParser ast(expr);
+//	std::cout << Data::toJSON(ast) << std::endl;
+	return false;
+	//	return evalAST(expressionToAST(expr));
+}
+
+Data PromelaDataModel::expressionToAST(const std::string& expr) {
+	// see: http://en.wikipedia.org/wiki/Shunting-yard_algorithm (not used, prefix notation for now)
+	Data ast;
+
+	std::string tok_value;
+	std::list<Token> tokens;
+	size_t start = 0;
+
+	for (int i = 0; i < expr.size();) {
+		if (expr[i] == '(' || expr[i] == ')' || expr[i] == '!' || iswspace(expr[i]) || expr[i] == ',' || i + 1 == expr.size()) {
+#if 0
+			std::cout << ":" << expr << std::endl << ":";
+			for (int c = 0; c < expr.size(); c++) {
+				if (c == start) {
+					std::cout << "s";
+				} else if(c == i) {
+					std::cout << "^";
+				} else {
+					std::cout << " ";
+				}
+			}
+			std::cout << std::endl;;
+#endif
+			
+			Token token;
+			if (i > 0 && start < i - 1) {
+				token.start = start;
+				token.end = i;
+
+				if (i + 1 == expr.size() && !(expr[i] == '(' || expr[i] == ')' || expr[i] == '!'))
+					token.end++;
+//				std::cout << expr.substr(token.start, token.end - token.start) << std::endl;
+
+				tokens.push_back(token);
+			}
+			if (expr[i] == '(' || expr[i] == ')' || expr[i] == '!') {
+				token.start = i;
+				token.end = i + 1;
+//				std::cout << expr.substr(token.start, token.end - token.start) << std::endl;
+
+				tokens.push_back(token);
+				i++;
+			}
+			if (expr[i] == ',') {
+				i++;
+			}
+			if (i + 1 == expr.size())
+				break;
+			
+			if (iswspace(expr[i])) {
+				while(iswspace(expr[++i])); // skip remaining whitespaces
+			}
+			start = i;
+		} else {
+			i++;
+		}
+	}
+	
+	std::list<Data*> dataStack;
+	std::list<Token> tokenStack;
+	dataStack.push_back(&ast);
+
+	for (std::list<Token>::iterator tokIter = tokens.begin();
+			 tokIter != tokens.end();
+			 tokIter++) {
+		std::string token = expr.substr(tokIter->start, tokIter->end - tokIter->start);
+//		std::cout << token << std::endl;
+
+		if (false) {
+		} else if (token == "(") {
+			dataStack.back()->type = Data::INTERPRETED;
+		} else if (token == ")") {
+			dataStack.pop_back();
+		} else if (token == "and") {
+			dataStack.back()->array.push_back(Data("", Data::VERBATIM));
+			dataStack.push_back(&(dataStack.back()->array.back().compound["and"]));
+			dataStack.back()->type = Data::VERBATIM;
+			continue;
+		} else if (token == "or") {
+			dataStack.back()->array.push_back(Data("", Data::VERBATIM));
+			dataStack.push_back(&(dataStack.back()->array.back().compound["or"]));
+			dataStack.back()->type = Data::VERBATIM;
+			continue;
+		} else if (token == "!" || token == "not") {
+			dataStack.back()->array.push_back(Data("", Data::VERBATIM));
+			dataStack.push_back(&(dataStack.back()->array.back().compound["not"]));
+			dataStack.back()->type = Data::VERBATIM;
+			continue;
+		} else {
+			// treat everything else as a variable
+			dataStack.back()->array.push_back(Data(token, Data::VERBATIM));
+		}
+
+		// pop back if not bracketed
+		while (dataStack.back()->type == Data::VERBATIM) {
+			dataStack.pop_back();
+		}
+
+	}
+	
+//	std::cout << Data::toJSON(ast) << std::endl << std::endl;
+	
+	return ast;
+}
+
+bool PromelaDataModel::evalAST(const Data ast) {
+	
+#if 0
+	std::cout << "===========" << std::endl;
+	std::cout << Data::toJSON(ast) << std::endl;
+	std::cout << "===========" << std::endl;
+#endif
+	
+	// atomic term
+	if (ast.atom.size() > 0) {
+		// is it the event name? TODO: Use some prefix here!
+		if (InterpreterImpl::nameMatch(ast.atom, _event.name))
+			return true;
+
+		if (_variables.find(ast.atom) != _variables.end()) {
+			return _variables[ast.atom];
+		}
+		return false;
+	}
+
+	const std::list<Data>* arrayPtr = &(ast.array);
+
+	// no operator is implied 'and'
+	std::string op = "and";
+	if (ast.compound.size() > 0) {
+		op = ast.compound.begin()->first;
+		arrayPtr = &(ast.compound.at(op).array);
+	}
+	
+	for (std::list<Data>::const_iterator termIter = arrayPtr->begin();
+			 termIter != arrayPtr->end();
+			 termIter++) {
+		bool result = evalAST(*termIter);
+		if (false) {
+		} else if (op == "and" && !result) {
+			return false;
+		} else if (op == "or" && result) {
+			return true;
+		} else if (op == "not" && result) {
+			return false;
+		}
+	}
+	return true;
+}
+	
+std::string PromelaDataModel::evalAsString(const std::string& expr) {
+	return "";
+}
+
+void PromelaDataModel::assign(const Element<std::string>& assignElem,
+                          const Node<std::string>& node,
+                          const std::string& content) {
+	Data ast = expressionToAST(content);
+	assign(true, ast);
+}
+
+void PromelaDataModel::assign(bool truth, Data ast) {
+	for (std::list<Data>::iterator arrIter = ast.array.begin();
+			 arrIter != ast.array.end();
+			 arrIter++) {
+		if (false) {
+		} else if (arrIter->atom.size() > 0) {
+			// simple atom to true
+			_variables[arrIter->atom] = truth;
+		} else if (arrIter->hasKey("not")) {
+			// for convenience, we support bracketed "nots"
+			assign(false, arrIter->compound["not"]);
+		} else {
+			Event exceptionEvent;
+			exceptionEvent.data.compound["ast"] = ast;
+			exceptionEvent.data.compound["exception"] = Data("Assignments can only contain atoms and negations", Data::VERBATIM);
+			exceptionEvent.name = "error.execution";
+			exceptionEvent.eventType = Event::PLATFORM;
+			throw exceptionEvent;
+		}
+	}
+}
+	
+void PromelaDataModel::assign(const std::string& location, const Data& data) {
+	// used for e.g. to assign command line parameters
+	std::cout << "Ignoring " << location << " = " << Data::toJSON(data) << std::endl;
+}
+
+void PromelaDataModel::init(const Element<std::string>& dataElem,
+                        const Node<std::string>& node,
+                        const std::string& content) {
+	// from <datamodel>
+	assign(dataElem, node, content);
+}
+void PromelaDataModel::init(const std::string& location, const Data& data) {
+	assign(location, data);
+}
+
+bool PromelaDataModel::isDeclared(const std::string& expr) {
+	return _variables.find(expr) != _variables.end();
+}
+
+
+}
diff --git a/src/uscxml/plugins/datamodel/promela/PromelaDataModel.h b/src/uscxml/plugins/datamodel/promela/PromelaDataModel.h
new file mode 100644
index 0000000..d332db1
--- /dev/null
+++ b/src/uscxml/plugins/datamodel/promela/PromelaDataModel.h
@@ -0,0 +1,109 @@
+/**
+ *  @file
+ *  @author     2012-2014 Stefan Radomski (stefan.radomski@cs.tu-darmstadt.de)
+ *  @copyright  Simplified BSD
+ *
+ *  @cond
+ *  This program is free software: you can redistribute it and/or modify
+ *  it under the terms of the FreeBSD license as published by the FreeBSD
+ *  project.
+ *
+ *  This program is distributed in the hope that it will be useful,
+ *  but WITHOUT ANY WARRANTY; without even the implied warranty of
+ *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
+ *
+ *  You should have received a copy of the FreeBSD license along with this
+ *  program. If not, see <http://www.opensource.org/licenses/bsd-license>.
+ *  @endcond
+ */
+
+#ifndef PROMELADATAMODEL_H_4VG0TDMU
+#define PROMELADATAMODEL_H_4VG0TDMU
+
+#include "uscxml/Interpreter.h"
+#include <list>
+
+#ifdef BUILD_AS_PLUGINS
+#include "uscxml/plugins/Plugins.h"
+#endif
+
+namespace uscxml {
+
+class PromelaDataModel : public DataModelImpl {
+public:
+	PromelaDataModel();
+	virtual ~PromelaDataModel();
+	virtual boost::shared_ptr<DataModelImpl> create(InterpreterImpl* interpreter);
+
+	virtual std::set<std::string> getNames() {
+		std::set<std::string> names;
+		names.insert("promela");
+		return names;
+	}
+
+	virtual void initialize();
+	virtual void setSessionId(const std::string& sessionId);
+	virtual void setName(const std::string& name);
+	virtual void setEvent(const Event& event);
+
+	virtual void registerIOProcessor(const std::string& name, const IOProcessor& ioprocessor);
+
+	virtual bool validate(const std::string& location, const std::string& schema);
+
+	virtual uint32_t getLength(const std::string& expr);
+	virtual void setForeach(const std::string& item,
+	                        const std::string& array,
+	                        const std::string& index,
+	                        uint32_t iteration);
+
+	virtual void pushContext();
+	virtual void popContext();
+
+	virtual void assign(const Arabica::DOM::Element<std::string>& assignElem,
+	                    const Arabica::DOM::Node<std::string>& node,
+	                    const std::string& content);
+	virtual void assign(const std::string& location, const Data& data);
+
+	virtual void init(const Arabica::DOM::Element<std::string>& dataElem,
+	                  const Arabica::DOM::Node<std::string>& node,
+	                  const std::string& content);
+	virtual void init(const std::string& location, const Data& data);
+
+	virtual void eval(const Arabica::DOM::Element<std::string>& scriptElem,
+	                  const std::string& expr);
+
+	virtual bool isDeclared(const std::string& expr);
+
+	virtual Data getStringAsData(const std::string& content);
+	
+	virtual std::string evalAsString(const std::string& expr);
+	virtual bool evalAsBool(const Arabica::DOM::Node<std::string>& node, const std::string& expr);
+	virtual bool evalAsBool(const std::string& expr);
+
+protected:
+
+	struct Token {
+		size_t start;
+		size_t end;
+	};
+
+	Data expressionToAST(const std::string& expr);
+	bool evalAST(const Data ast);
+
+	void assign(bool truth, Data ast);
+
+	Event _event;
+	std::string _name;
+	std::string _sessionId;
+
+	std::map<std::string, bool> _variables;
+
+};
+
+#ifdef BUILD_AS_PLUGINS
+PLUMA_INHERIT_PROVIDER(PromelaDataModel, DataModelImpl);
+#endif
+
+}
+
+#endif /* end of include guard: PROMELADATAMODEL_H_4VG0TDMU */
diff --git a/src/uscxml/plugins/datamodel/promela/PromelaParser.cpp b/src/uscxml/plugins/datamodel/promela/PromelaParser.cpp
new file mode 100644
index 0000000..5bfc2a7
--- /dev/null
+++ b/src/uscxml/plugins/datamodel/promela/PromelaParser.cpp
@@ -0,0 +1,59 @@
+#include "PromelaParser.h"
+#include "parser/promela.tab.hpp"
+
+struct yy_buffer_state; \
+typedef yy_buffer_state *YY_BUFFER_STATE; \
+extern YY_BUFFER_STATE promela__scan_buffer(char *, size_t, void*); \
+extern int promela_lex (PROMELA_STYPE* yylval_param, void* yyscanner); \
+int promela_lex_init (void**); \
+int promela_lex_destroy (void*); \
+
+void promela_error (uscxml::PromelaParser* ctx, void* yyscanner, const char* err) {
+	std::cout << err << std::endl;
+}
+
+namespace uscxml {
+
+PromelaParser::PromelaParser(const std::string& expr) {
+	input_length = expr.length() + 5;  // plus some zero terminators
+	input = (char*) calloc(1, input_length);
+	memcpy(input, expr.c_str(), expr.length());
+
+	promela_lex_init(&scanner);
+	//	promela_assign_set_extra(ast, &scanner);
+	promela__scan_buffer(input, input_length, scanner);
+	promela_parse(this, scanner);
+}
+PromelaParser::~PromelaParser() {
+	free(input);
+	promela_lex_destroy(scanner);
+}
+
+std::string PromelaParser::typeToDesc(int type) {
+	switch(type) {
+		case PLUS: return "PLUS";
+		case MINUS: return "MINUS";
+		case TIMES: return "TIMES";
+		case DIVIDE: return "DIVIDE";
+		case MODULO: return "MODULO";
+		case BITAND: return "BITAND";
+		case BITXOR: return "BITXOR";
+		case BITOR: return "BITOR";
+		case GT: return "GT";
+		case LT: return "LT";
+		case GE: return "GE";
+		case LE: return "LE";
+		case EQ: return "EQ";
+		case NE: return "NE";
+		case AND: return "AND";
+		case OR: return "OR";
+		case LSHIFT: return "LSHIFT";
+		case RSHIFT: return "RSHIFT";
+		case NEG: return "NEG";
+		case ASGN: return "ASGN";
+		default:
+			return std::string("UNK(") + toStr(type) + ")";
+	}
+}
+
+}
\ No newline at end of file
diff --git a/src/uscxml/plugins/datamodel/promela/PromelaParser.h b/src/uscxml/plugins/datamodel/promela/PromelaParser.h
new file mode 100644
index 0000000..c45bcc2
--- /dev/null
+++ b/src/uscxml/plugins/datamodel/promela/PromelaParser.h
@@ -0,0 +1,102 @@
+// bison -v -d promela-expr.ypp && flex promela-expr.l
+// bison promela-expr.ypp && flex promela-expr.l
+
+#ifndef PROMELA_H_9AB78YB1
+#define PROMELA_H_9AB78YB1
+
+#include <stdlib.h>
+#include "uscxml/Message.h"
+
+#define GRAMMAR_COMMON(name, uc_name) \
+struct yy_buffer_state; \
+typedef yy_buffer_state *YY_BUFFER_STATE; \
+extern YY_BUFFER_STATE promela_##name##__scan_buffer(char *, size_t, void*); \
+extern int promela_##name##_lex (PROMELA_##uc_name##_STYPE* yylval_param, void* yyscanner); \
+int promela_##name##_lex_init (void**); \
+int promela_##name##_lex_destroy (void*); \
+
+namespace uscxml {
+
+struct PromelaParserNode {
+	PromelaParserNode() : type(0) {}
+	int type;
+	std::string value;
+	std::list<PromelaParserNode*> operands;
+};
+
+class PromelaParser {
+public:
+	enum Type {
+		PROMELA_EXPR,
+		PROMELA_DECL,
+		PROMELA_STMNT
+	};
+	
+	PromelaParser(const std::string& expr);
+	virtual ~PromelaParser();
+	
+	virtual PromelaParserNode* uniOp(int type, PromelaParserNode* oper) {
+		PromelaParserNode* newNode = new PromelaParserNode();
+		newNode->type = type;
+		newNode->operands.push_back(oper);
+		return newNode;
+	}
+
+	virtual PromelaParserNode* binOp(int type, PromelaParserNode* left, PromelaParserNode* right) {
+		PromelaParserNode* newNode = new PromelaParserNode();
+		newNode->type = type;
+		newNode->operands.push_back(left);
+		newNode->operands.push_back(right);
+		return newNode;
+	}
+
+	virtual PromelaParserNode* value(const char* value) {
+		PromelaParserNode* newNode = new PromelaParserNode();
+		newNode->value = value;
+		return newNode;
+	}
+
+	void dump() {
+		switch (type) {
+		case PROMELA_EXPR:
+			std::cout << "Promela Expression" << std::endl;
+			break;
+		case PROMELA_DECL:
+			std::cout << "Promela Declarations" << std::endl;
+			break;
+		case PROMELA_STMNT:
+			std::cout << "Promela Statement" << std::endl;
+			break;
+		}
+		dump(ast);
+	}
+	
+	void dump(PromelaParserNode* node, int indent = 0) {
+		std::string padding;
+		for (int i = 0; i < indent; i++) {
+			padding += "  ";
+		}
+		std::cout << padding << typeToDesc(node->type) << ": " << node->value << std::endl;
+		for (std::list<PromelaParserNode*>::iterator iter = node->operands.begin();
+				 iter != node->operands.end(); iter++) {
+			dump(*iter, indent + 1);
+		}
+	}
+
+	virtual std::string typeToDesc(int type);
+
+	PromelaParserNode* ast;
+	Type type;
+
+protected:
+		
+	void* scanner;
+	char* input;
+	size_t input_length;
+};
+
+}
+
+void promela_error (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
new file mode 100644
index 0000000..4332c6b
--- /dev/null
+++ b/src/uscxml/plugins/datamodel/promela/parser/promela.l
@@ -0,0 +1,80 @@
+/* see: http://www.phpcompiler.org/articles/reentrantparser.html */
+/* see: http://spinroot.com/spin/Man/operators.html */
+
+
+%option reentrant
+%option bison-bridge
+%option prefix="promela_"
+%option outfile="promela.lex.yy.cpp"
+%option noyywrap
+%option debug 
+%option never-interactive nounistd
+
+%{
+  
+#include "../PromelaParser.h"
+#include "promela.tab.hpp"
+#define YYSTYPE PROMELA_STYPE
+
+%}
+
+DIGIT    [0-9]
+ID       [_a-zA-Z][_a-zA-Z0-9]*
+
+%%
+
+bit|bool|byte|int|mtype|short|unsigned {
+  //printf("TYPE: %s\n", yytext);
+  yylval->value = strdup(yytext);
+  return TYPE;
+}
+
+len                        { return LEN; }
+false|skip|true            { yylval->value = strdup(yytext); return CONST; }
+
+"!"                        { return NEG; }
+"~"                        { return COMPL; }
+
+"*"                        { return TIMES; }
+"/"                        { return DIVIDE; }
+"%"                        { return MODULO; }
+
+"+"                        { return PLUS; }
+"-"                        { return MINUS; }
+
+"<<"                       { return LSHIFT; }
+">>"                       { return RSHIFT; }
+
+"<="                       { return LE; }
+">="                       { return GE; }
+"<"                        { return LT; }
+">"                        { return GT; }
+
+"!="                       { return NE; }
+"=="                       { return EQ; }
+
+"&"                        { return BITAND; }
+"^"                        { return BITXOR; }
+"|"                        { return BITOR; }
+
+
+"&&"                       { return AND; }
+"||"                       { return OR; }
+
+"."                        { return DOT; }
+
+"("                        { return LBRACKET; }
+")"                        { return RBRACKET; }
+
+"="                        { return ASGN; }
+
+{DIGIT}+                   { yylval->value = strdup(yytext); return CONST; }
+{ID}                       { yylval->value = strdup(yytext); return NAME; }
+
+\'(\\.|[^'])*\'            { }
+
+"{"[^}\n]*"}"     /* eat up one-line comments */
+
+[ \t\n]+          /* eat up whitespace */
+
+.                          { /*printf( "Unrecognized character: %s\n", yytext ); */ }
diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.lex.yy.cpp b/src/uscxml/plugins/datamodel/promela/parser/promela.lex.yy.cpp
new file mode 100644
index 0000000..122a408
--- /dev/null
+++ b/src/uscxml/plugins/datamodel/promela/parser/promela.lex.yy.cpp
@@ -0,0 +1,2488 @@
+#line 2 "promela.lex.yy.cpp"
+
+#line 4 "promela.lex.yy.cpp"
+
+#define  YY_INT_ALIGNED short int
+
+/* A lexical scanner generated by flex */
+
+/* %not-for-header */
+
+/* %if-c-only */
+/* %if-not-reentrant */
+/* %endif */
+/* %endif */
+/* %ok-for-header */
+
+#define FLEX_SCANNER
+#define YY_FLEX_MAJOR_VERSION 2
+#define YY_FLEX_MINOR_VERSION 5
+#define YY_FLEX_SUBMINOR_VERSION 35
+#if YY_FLEX_SUBMINOR_VERSION > 0
+#define FLEX_BETA
+#endif
+
+/* %if-c++-only */
+/* %endif */
+
+/* %if-c-only */
+    
+/* %endif */
+
+/* %if-c-only */
+
+/* %endif */
+
+/* First, we deal with  platform-specific or compiler-specific issues. */
+
+/* begin standard C headers. */
+/* %if-c-only */
+#include <stdio.h>
+#include <string.h>
+#include <errno.h>
+#include <stdlib.h>
+/* %endif */
+
+/* %if-tables-serialization */
+/* %endif */
+/* end standard C headers. */
+
+/* %if-c-or-c++ */
+/* flex integer type definitions */
+
+#ifndef FLEXINT_H
+#define FLEXINT_H
+
+/* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */
+
+#if defined (__STDC_VERSION__) && __STDC_VERSION__ >= 199901L
+
+/* C99 says to define __STDC_LIMIT_MACROS before including stdint.h,
+ * if you want the limit (max/min) macros for int types. 
+ */
+#ifndef __STDC_LIMIT_MACROS
+#define __STDC_LIMIT_MACROS 1
+#endif
+
+#include <inttypes.h>
+typedef int8_t flex_int8_t;
+typedef uint8_t flex_uint8_t;
+typedef int16_t flex_int16_t;
+typedef uint16_t flex_uint16_t;
+typedef int32_t flex_int32_t;
+typedef uint32_t flex_uint32_t;
+typedef uint64_t flex_uint64_t;
+#else
+typedef signed char flex_int8_t;
+typedef short int flex_int16_t;
+typedef int flex_int32_t;
+typedef unsigned char flex_uint8_t; 
+typedef unsigned short int flex_uint16_t;
+typedef unsigned int flex_uint32_t;
+#endif /* ! C99 */
+
+/* Limits of integral types. */
+#ifndef INT8_MIN
+#define INT8_MIN               (-128)
+#endif
+#ifndef INT16_MIN
+#define INT16_MIN              (-32767-1)
+#endif
+#ifndef INT32_MIN
+#define INT32_MIN              (-2147483647-1)
+#endif
+#ifndef INT8_MAX
+#define INT8_MAX               (127)
+#endif
+#ifndef INT16_MAX
+#define INT16_MAX              (32767)
+#endif
+#ifndef INT32_MAX
+#define INT32_MAX              (2147483647)
+#endif
+#ifndef UINT8_MAX
+#define UINT8_MAX              (255U)
+#endif
+#ifndef UINT16_MAX
+#define UINT16_MAX             (65535U)
+#endif
+#ifndef UINT32_MAX
+#define UINT32_MAX             (4294967295U)
+#endif
+
+#endif /* ! FLEXINT_H */
+
+/* %endif */
+
+/* %if-c++-only */
+/* %endif */
+
+#ifdef __cplusplus
+
+/* The "const" storage-class-modifier is valid. */
+#define YY_USE_CONST
+
+#else	/* ! __cplusplus */
+
+/* C99 requires __STDC__ to be defined as 1. */
+#if defined (__STDC__)
+
+#define YY_USE_CONST
+
+#endif	/* defined (__STDC__) */
+#endif	/* ! __cplusplus */
+
+#ifdef YY_USE_CONST
+#define yyconst const
+#else
+#define yyconst
+#endif
+
+/* %not-for-header */
+
+/* Returned upon end-of-file. */
+#define YY_NULL 0
+/* %ok-for-header */
+
+/* %not-for-header */
+
+/* Promotes a possibly negative, possibly signed char to an unsigned
+ * integer for use as an array index.  If the signed char is negative,
+ * we want to instead treat it as an 8-bit unsigned char, hence the
+ * double cast.
+ */
+#define YY_SC_TO_UI(c) ((unsigned int) (unsigned char) c)
+/* %ok-for-header */
+
+/* %if-reentrant */
+
+/* An opaque pointer. */
+#ifndef YY_TYPEDEF_YY_SCANNER_T
+#define YY_TYPEDEF_YY_SCANNER_T
+typedef void* yyscan_t;
+#endif
+
+/* For convenience, these vars (plus the bison vars far below)
+   are macros in the reentrant scanner. */
+#define yyin yyg->yyin_r
+#define yyout yyg->yyout_r
+#define yyextra yyg->yyextra_r
+#define yyleng yyg->yyleng_r
+#define yytext yyg->yytext_r
+#define yylineno (YY_CURRENT_BUFFER_LVALUE->yy_bs_lineno)
+#define yycolumn (YY_CURRENT_BUFFER_LVALUE->yy_bs_column)
+#define yy_flex_debug yyg->yy_flex_debug_r
+
+/* %endif */
+
+/* %if-not-reentrant */
+/* %endif */
+
+/* Enter a start condition.  This macro really ought to take a parameter,
+ * but we do it the disgusting crufty way forced on us by the ()-less
+ * definition of BEGIN.
+ */
+#define BEGIN yyg->yy_start = 1 + 2 *
+
+/* Translate the current start state into a value that can be later handed
+ * to BEGIN to return to the state.  The YYSTATE alias is for lex
+ * compatibility.
+ */
+#define YY_START ((yyg->yy_start - 1) / 2)
+#define YYSTATE YY_START
+
+/* Action number for EOF rule of a given start state. */
+#define YY_STATE_EOF(state) (YY_END_OF_BUFFER + state + 1)
+
+/* Special action meaning "start processing a new file". */
+#define YY_NEW_FILE promela_restart(yyin ,yyscanner )
+
+#define YY_END_OF_BUFFER_CHAR 0
+
+/* Size of default input buffer. */
+#ifndef YY_BUF_SIZE
+#define YY_BUF_SIZE 16384
+#endif
+
+/* The state buf must be large enough to hold one state per character in the main buffer.
+ */
+#define YY_STATE_BUF_SIZE   ((YY_BUF_SIZE + 2) * sizeof(yy_state_type))
+
+#ifndef YY_TYPEDEF_YY_BUFFER_STATE
+#define YY_TYPEDEF_YY_BUFFER_STATE
+typedef struct yy_buffer_state *YY_BUFFER_STATE;
+#endif
+
+#ifndef YY_TYPEDEF_YY_SIZE_T
+#define YY_TYPEDEF_YY_SIZE_T
+typedef size_t yy_size_t;
+#endif
+
+/* %if-not-reentrant */
+/* %endif */
+
+/* %if-c-only */
+/* %if-not-reentrant */
+/* %endif */
+/* %endif */
+
+#define EOB_ACT_CONTINUE_SCAN 0
+#define EOB_ACT_END_OF_FILE 1
+#define EOB_ACT_LAST_MATCH 2
+
+    #define YY_LESS_LINENO(n)
+    
+/* Return all but the first "n" matched characters back to the input stream. */
+#define yyless(n) \
+	do \
+		{ \
+		/* Undo effects of setting up yytext. */ \
+        int yyless_macro_arg = (n); \
+        YY_LESS_LINENO(yyless_macro_arg);\
+		*yy_cp = yyg->yy_hold_char; \
+		YY_RESTORE_YY_MORE_OFFSET \
+		yyg->yy_c_buf_p = yy_cp = yy_bp + yyless_macro_arg - YY_MORE_ADJ; \
+		YY_DO_BEFORE_ACTION; /* set up yytext again */ \
+		} \
+	while ( 0 )
+
+#define unput(c) yyunput( c, yyg->yytext_ptr , yyscanner )
+
+#ifndef YY_STRUCT_YY_BUFFER_STATE
+#define YY_STRUCT_YY_BUFFER_STATE
+struct yy_buffer_state
+	{
+/* %if-c-only */
+	FILE *yy_input_file;
+/* %endif */
+
+/* %if-c++-only */
+/* %endif */
+
+	char *yy_ch_buf;		/* input buffer */
+	char *yy_buf_pos;		/* current position in input buffer */
+
+	/* Size of input buffer in bytes, not including room for EOB
+	 * characters.
+	 */
+	yy_size_t yy_buf_size;
+
+	/* Number of characters read into yy_ch_buf, not including EOB
+	 * characters.
+	 */
+	yy_size_t yy_n_chars;
+
+	/* Whether we "own" the buffer - i.e., we know we created it,
+	 * and can realloc() it to grow it, and should free() it to
+	 * delete it.
+	 */
+	int yy_is_our_buffer;
+
+	/* Whether this is an "interactive" input source; if so, and
+	 * if we're using stdio for input, then we want to use getc()
+	 * instead of fread(), to make sure we stop fetching input after
+	 * each newline.
+	 */
+	int yy_is_interactive;
+
+	/* Whether we're considered to be at the beginning of a line.
+	 * If so, '^' rules will be active on the next match, otherwise
+	 * not.
+	 */
+	int yy_at_bol;
+
+    int yy_bs_lineno; /**< The line count. */
+    int yy_bs_column; /**< The column count. */
+    
+	/* Whether to try to fill the input buffer when we reach the
+	 * end of it.
+	 */
+	int yy_fill_buffer;
+
+	int yy_buffer_status;
+
+#define YY_BUFFER_NEW 0
+#define YY_BUFFER_NORMAL 1
+	/* When an EOF's been seen but there's still some text to process
+	 * then we mark the buffer as YY_EOF_PENDING, to indicate that we
+	 * shouldn't try reading from the input source any more.  We might
+	 * still have a bunch of tokens to match, though, because of
+	 * possible backing-up.
+	 *
+	 * When we actually see the EOF, we change the status to "new"
+	 * (via promela_restart()), so that the user can continue scanning by
+	 * just pointing yyin at a new input file.
+	 */
+#define YY_BUFFER_EOF_PENDING 2
+
+	};
+#endif /* !YY_STRUCT_YY_BUFFER_STATE */
+
+/* %if-c-only Standard (non-C++) definition */
+/* %not-for-header */
+
+/* %if-not-reentrant */
+/* %endif */
+/* %ok-for-header */
+
+/* %endif */
+
+/* We provide macros for accessing buffer states in case in the
+ * future we want to put the buffer states in a more general
+ * "scanner state".
+ *
+ * Returns the top of the stack, or NULL.
+ */
+#define YY_CURRENT_BUFFER ( yyg->yy_buffer_stack \
+                          ? yyg->yy_buffer_stack[yyg->yy_buffer_stack_top] \
+                          : NULL)
+
+/* Same as previous macro, but useful when we know that the buffer stack is not
+ * NULL or when we need an lvalue. For internal use only.
+ */
+#define YY_CURRENT_BUFFER_LVALUE yyg->yy_buffer_stack[yyg->yy_buffer_stack_top]
+
+/* %if-c-only Standard (non-C++) definition */
+
+/* %if-not-reentrant */
+/* %not-for-header */
+
+/* %ok-for-header */
+
+/* %endif */
+
+void promela_restart (FILE *input_file ,yyscan_t yyscanner );
+void promela__switch_to_buffer (YY_BUFFER_STATE new_buffer ,yyscan_t yyscanner );
+YY_BUFFER_STATE promela__create_buffer (FILE *file,int size ,yyscan_t yyscanner );
+void promela__delete_buffer (YY_BUFFER_STATE b ,yyscan_t yyscanner );
+void promela__flush_buffer (YY_BUFFER_STATE b ,yyscan_t yyscanner );
+void promela_push_buffer_state (YY_BUFFER_STATE new_buffer ,yyscan_t yyscanner );
+void promela_pop_buffer_state (yyscan_t yyscanner );
+
+static void promela_ensure_buffer_stack (yyscan_t yyscanner );
+static void promela__load_buffer_state (yyscan_t yyscanner );
+static void promela__init_buffer (YY_BUFFER_STATE b,FILE *file ,yyscan_t yyscanner );
+
+#define YY_FLUSH_BUFFER promela__flush_buffer(YY_CURRENT_BUFFER ,yyscanner)
+
+YY_BUFFER_STATE promela__scan_buffer (char *base,yy_size_t size ,yyscan_t yyscanner );
+YY_BUFFER_STATE promela__scan_string (yyconst char *yy_str ,yyscan_t yyscanner );
+YY_BUFFER_STATE promela__scan_bytes (yyconst char *bytes,yy_size_t len ,yyscan_t yyscanner );
+
+/* %endif */
+
+void *promela_alloc (yy_size_t ,yyscan_t yyscanner );
+void *promela_realloc (void *,yy_size_t ,yyscan_t yyscanner );
+void promela_free (void * ,yyscan_t yyscanner );
+
+#define yy_new_buffer promela__create_buffer
+
+#define yy_set_interactive(is_interactive) \
+	{ \
+	if ( ! YY_CURRENT_BUFFER ){ \
+        promela_ensure_buffer_stack (yyscanner); \
+		YY_CURRENT_BUFFER_LVALUE =    \
+            promela__create_buffer(yyin,YY_BUF_SIZE ,yyscanner); \
+	} \
+	YY_CURRENT_BUFFER_LVALUE->yy_is_interactive = is_interactive; \
+	}
+
+#define yy_set_bol(at_bol) \
+	{ \
+	if ( ! YY_CURRENT_BUFFER ){\
+        promela_ensure_buffer_stack (yyscanner); \
+		YY_CURRENT_BUFFER_LVALUE =    \
+            promela__create_buffer(yyin,YY_BUF_SIZE ,yyscanner); \
+	} \
+	YY_CURRENT_BUFFER_LVALUE->yy_at_bol = at_bol; \
+	}
+
+#define YY_AT_BOL() (YY_CURRENT_BUFFER_LVALUE->yy_at_bol)
+
+/* %% [1.0] yytext/yyin/yyout/yy_state_type/yylineno etc. def's & init go here */
+
+#define promela_wrap(n) 1
+#define YY_SKIP_YYWRAP
+
+#define FLEX_DEBUG
+
+typedef unsigned char YY_CHAR;
+
+typedef int yy_state_type;
+
+#define yytext_ptr yytext_r
+
+/* %if-c-only Standard (non-C++) definition */
+
+static yy_state_type yy_get_previous_state (yyscan_t yyscanner );
+static yy_state_type yy_try_NUL_trans (yy_state_type current_state  ,yyscan_t yyscanner);
+static int yy_get_next_buffer (yyscan_t yyscanner );
+static void yy_fatal_error (yyconst char msg[] ,yyscan_t yyscanner );
+
+/* %endif */
+
+/* Done after the current pattern has been matched and before the
+ * corresponding action - sets up yytext.
+ */
+#define YY_DO_BEFORE_ACTION \
+	yyg->yytext_ptr = yy_bp; \
+/* %% [2.0] code to fiddle yytext and yyleng for yymore() goes here \ */\
+	yyleng = (yy_size_t) (yy_cp - yy_bp); \
+	yyg->yy_hold_char = *yy_cp; \
+	*yy_cp = '\0'; \
+/* %% [3.0] code to copy yytext_ptr to yytext[] goes here, if %array \ */\
+	yyg->yy_c_buf_p = yy_cp;
+
+/* %% [4.0] data tables for the DFA and the user's section 1 definitions go here */
+#define YY_NUM_RULES 34
+#define YY_END_OF_BUFFER 35
+/* This struct is not used in this scanner,
+   but its presence is necessary. */
+struct yy_trans_info
+	{
+	flex_int32_t yy_verify;
+	flex_int32_t yy_nxt;
+	};
+static yyconst flex_int16_t yy_accept[84] =
+    {   0,
+        0,    0,   35,   33,   32,   32,    4,    8,   19,   33,
+       25,   26,    6,    9,   10,   24,    7,   28,   15,   27,
+       16,   29,   20,   29,   29,   29,   29,   29,   29,   29,
+       29,   33,   21,    5,   32,   17,   22,    0,   30,    0,
+       28,   11,   13,   18,   14,   12,   29,   29,   29,   29,
+       29,   29,   29,   29,   29,   29,   29,   29,    0,   31,
+       23,    0,   30,    0,    1,   29,   29,   29,    2,   29,
+       29,   29,   29,   29,   29,   29,   29,    3,   29,   29,
+       29,   29,    0
+    } ;
+
+static yyconst flex_int32_t yy_ec[256] =
+    {   0,
+        1,    1,    1,    1,    1,    1,    1,    1,    2,    3,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    2,    4,    1,    1,    1,    5,    6,    7,    8,
+        9,   10,   11,    1,   12,   13,   14,   15,   15,   15,
+       15,   15,   15,   15,   15,   15,   15,    1,    1,   16,
+       17,   18,    1,    1,   19,   19,   19,   19,   19,   19,
+       19,   19,   19,   19,   19,   19,   19,   19,   19,   19,
+       19,   19,   19,   19,   19,   19,   19,   19,   19,   19,
+        1,   20,    1,   21,   19,    1,   22,   23,   19,   24,
+
+       25,   26,   27,   28,   29,   19,   30,   31,   32,   33,
+       34,   35,   19,   36,   37,   38,   39,   19,   19,   19,
+       40,   19,   41,   42,   43,   44,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1
+    } ;
+
+static yyconst flex_int32_t yy_meta[45] =
+    {   0,
+        1,    1,    2,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    3,    1,    1,    1,    3,    1,
+        1,    3,    3,    3,    3,    3,    3,    3,    3,    3,
+        3,    3,    3,    3,    3,    3,    3,    3,    3,    3,
+        1,    1,    1,    1
+    } ;
+
+static yyconst flex_int16_t yy_base[88] =
+    {   0,
+        0,    0,  123,  124,   43,   45,  105,  124,  115,   42,
+      124,  124,  124,  124,  124,  124,  124,  105,   34,  102,
+       35,    0,  124,   25,   96,   84,   91,   77,   27,   78,
+       80,   69,   69,  124,   58,  124,  124,   49,  124,   60,
+       95,  124,  124,  124,  124,  124,    0,   71,   74,   69,
+       75,   67,   71,   63,   68,   72,   61,   62,   55,  124,
+      124,   51,   57,   63,    0,   66,   71,   58,    0,   59,
+       57,   53,   57,   52,   54,   53,   38,    0,   48,   41,
+       48,   48,  124,   83,   65,   86,   89
+    } ;
+
+static yyconst flex_int16_t yy_def[88] =
+    {   0,
+       83,    1,   83,   83,   83,   83,   83,   83,   83,   84,
+       83,   83,   83,   83,   83,   83,   83,   83,   83,   83,
+       83,   85,   83,   85,   85,   85,   85,   85,   85,   85,
+       85,   86,   83,   83,   83,   83,   83,   84,   83,   87,
+       83,   83,   83,   83,   83,   83,   85,   85,   85,   85,
+       85,   85,   85,   85,   85,   85,   85,   85,   86,   83,
+       83,   84,   84,   87,   85,   85,   85,   85,   85,   85,
+       85,   85,   85,   85,   85,   85,   85,   85,   85,   85,
+       85,   85,    0,   83,   83,   83,   83
+    } ;
+
+static yyconst flex_int16_t yy_nxt[169] =
+    {   0,
+        4,    5,    6,    7,    8,    9,   10,   11,   12,   13,
+       14,   15,   16,   17,   18,   19,   20,   21,   22,    4,
+       23,   22,   24,   22,   22,   25,   22,   22,   26,   22,
+       27,   28,   22,   22,   22,   22,   29,   30,   31,   22,
+       32,   33,    4,   34,   35,   35,   35,   35,   39,   42,
+       43,   45,   46,   48,   55,   39,   56,   39,   49,   35,
+       35,   40,   38,   39,   50,   38,   63,   47,   40,   63,
+       40,   65,   82,   81,   80,   65,   40,   65,   78,   64,
+       79,   78,   64,   38,   38,   38,   59,   78,   59,   62,
+       62,   62,   77,   76,   75,   65,   65,   60,   74,   73,
+
+       72,   71,   70,   69,   65,   68,   67,   66,   65,   41,
+       61,   60,   58,   57,   54,   53,   52,   51,   44,   41,
+       37,   36,   83,    3,   83,   83,   83,   83,   83,   83,
+       83,   83,   83,   83,   83,   83,   83,   83,   83,   83,
+       83,   83,   83,   83,   83,   83,   83,   83,   83,   83,
+       83,   83,   83,   83,   83,   83,   83,   83,   83,   83,
+       83,   83,   83,   83,   83,   83,   83,   83
+    } ;
+
+static yyconst flex_int16_t yy_chk[169] =
+    {   0,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    5,    5,    6,    6,   10,   19,
+       19,   21,   21,   24,   29,   38,   29,   62,   24,   35,
+       35,   10,   40,   63,   24,   64,   40,   85,   38,   64,
+       62,   82,   81,   80,   79,   77,   63,   76,   75,   40,
+       74,   73,   64,   84,   84,   84,   86,   72,   86,   87,
+       87,   87,   71,   70,   68,   67,   66,   59,   58,   57,
+
+       56,   55,   54,   53,   52,   51,   50,   49,   48,   41,
+       33,   32,   31,   30,   28,   27,   26,   25,   20,   18,
+        9,    7,    3,   83,   83,   83,   83,   83,   83,   83,
+       83,   83,   83,   83,   83,   83,   83,   83,   83,   83,
+       83,   83,   83,   83,   83,   83,   83,   83,   83,   83,
+       83,   83,   83,   83,   83,   83,   83,   83,   83,   83,
+       83,   83,   83,   83,   83,   83,   83,   83
+    } ;
+
+static yyconst flex_int16_t yy_rule_linenum[34] =
+    {   0,
+       26,   32,   33,   35,   36,   38,   39,   40,   42,   43,
+       45,   46,   48,   49,   50,   51,   53,   54,   56,   57,
+       58,   61,   62,   64,   66,   67,   69,   71,   72,   74,
+       76,   78,   80
+    } ;
+
+/* The intent behind this definition is that it'll catch
+ * any uses of REJECT which flex missed.
+ */
+#define REJECT reject_used_but_not_detected
+#define yymore() yymore_used_but_not_detected
+#define YY_MORE_ADJ 0
+#define YY_RESTORE_YY_MORE_OFFSET
+#line 1 "promela.l"
+/* 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"
+  
+#include "../PromelaParser.h"
+#include "promela.tab.hpp"
+#define YYSTYPE PROMELA_STYPE
+
+#line 596 "promela.lex.yy.cpp"
+
+#define INITIAL 0
+
+#ifndef YY_NO_UNISTD_H
+/* Special case for "unistd.h", since it is non-ANSI. We include it way
+ * down here because we want the user's section 1 to have been scanned first.
+ * The user has a chance to override it with an option.
+ */
+/* %if-c-only */
+#include <unistd.h>
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+#endif
+
+#ifndef YY_EXTRA_TYPE
+#define YY_EXTRA_TYPE void *
+#endif
+
+/* %if-c-only Reentrant structure and macros (non-C++). */
+/* %if-reentrant */
+
+/* Holds the entire state of the reentrant scanner. */
+struct yyguts_t
+    {
+
+    /* User-defined. Not touched by flex. */
+    YY_EXTRA_TYPE yyextra_r;
+
+    /* The rest are the same as the globals declared in the non-reentrant scanner. */
+    FILE *yyin_r, *yyout_r;
+    size_t yy_buffer_stack_top; /**< index of top of stack. */
+    size_t yy_buffer_stack_max; /**< capacity of stack. */
+    YY_BUFFER_STATE * yy_buffer_stack; /**< Stack as an array. */
+    char yy_hold_char;
+    yy_size_t yy_n_chars;
+    yy_size_t yyleng_r;
+    char *yy_c_buf_p;
+    int yy_init;
+    int yy_start;
+    int yy_did_buffer_switch_on_eof;
+    int yy_start_stack_ptr;
+    int yy_start_stack_depth;
+    int *yy_start_stack;
+    yy_state_type yy_last_accepting_state;
+    char* yy_last_accepting_cpos;
+
+    int yylineno_r;
+    int yy_flex_debug_r;
+
+    char *yytext_r;
+    int yy_more_flag;
+    int yy_more_len;
+
+    YYSTYPE * yylval_r;
+
+    }; /* end struct yyguts_t */
+
+/* %if-c-only */
+
+static int yy_init_globals (yyscan_t yyscanner );
+
+/* %endif */
+
+/* %if-reentrant */
+
+    /* This must go here because YYSTYPE and YYLTYPE are included
+     * from bison output in section 1.*/
+    #    define yylval yyg->yylval_r
+    
+int promela_lex_init (yyscan_t* scanner);
+
+int promela_lex_init_extra (YY_EXTRA_TYPE user_defined,yyscan_t* scanner);
+
+/* %endif */
+
+/* %endif End reentrant structures and macros. */
+
+/* Accessor methods to globals.
+   These are made visible to non-reentrant scanners for convenience. */
+
+int promela_lex_destroy (yyscan_t yyscanner );
+
+int promela_get_debug (yyscan_t yyscanner );
+
+void promela_set_debug (int debug_flag ,yyscan_t yyscanner );
+
+YY_EXTRA_TYPE promela_get_extra (yyscan_t yyscanner );
+
+void promela_set_extra (YY_EXTRA_TYPE user_defined ,yyscan_t yyscanner );
+
+FILE *promela_get_in (yyscan_t yyscanner );
+
+void promela_set_in  (FILE * in_str ,yyscan_t yyscanner );
+
+FILE *promela_get_out (yyscan_t yyscanner );
+
+void promela_set_out  (FILE * out_str ,yyscan_t yyscanner );
+
+yy_size_t promela_get_leng (yyscan_t yyscanner );
+
+char *promela_get_text (yyscan_t yyscanner );
+
+int promela_get_lineno (yyscan_t yyscanner );
+
+void promela_set_lineno (int line_number ,yyscan_t yyscanner );
+
+/* %if-bison-bridge */
+
+YYSTYPE * promela_get_lval (yyscan_t yyscanner );
+
+void promela_set_lval (YYSTYPE * yylval_param ,yyscan_t yyscanner );
+
+/* %endif */
+
+/* Macros after this point can all be overridden by user definitions in
+ * section 1.
+ */
+
+#ifndef YY_SKIP_YYWRAP
+#ifdef __cplusplus
+extern "C" int promela_wrap (yyscan_t yyscanner );
+#else
+extern int promela_wrap (yyscan_t yyscanner );
+#endif
+#endif
+
+/* %not-for-header */
+
+    static void yyunput (int c,char *buf_ptr  ,yyscan_t yyscanner);
+    
+/* %ok-for-header */
+
+/* %endif */
+
+#ifndef yytext_ptr
+static void yy_flex_strncpy (char *,yyconst char *,int ,yyscan_t yyscanner);
+#endif
+
+#ifdef YY_NEED_STRLEN
+static int yy_flex_strlen (yyconst char * ,yyscan_t yyscanner);
+#endif
+
+#ifndef YY_NO_INPUT
+/* %if-c-only Standard (non-C++) definition */
+/* %not-for-header */
+
+#ifdef __cplusplus
+static int yyinput (yyscan_t yyscanner );
+#else
+static int input (yyscan_t yyscanner );
+#endif
+/* %ok-for-header */
+
+/* %endif */
+#endif
+
+/* %if-c-only */
+
+/* %endif */
+
+/* Amount of stuff to slurp up with each read. */
+#ifndef YY_READ_BUF_SIZE
+#define YY_READ_BUF_SIZE 8192
+#endif
+
+/* Copy whatever the last rule matched to the standard output. */
+#ifndef ECHO
+/* %if-c-only Standard (non-C++) definition */
+/* This used to be an fputs(), but since the string might contain NUL's,
+ * we now use fwrite().
+ */
+#define ECHO fwrite( yytext, yyleng, 1, yyout )
+/* %endif */
+/* %if-c++-only C++ definition */
+/* %endif */
+#endif
+
+/* Gets input and stuffs it into "buf".  number of characters read, or YY_NULL,
+ * is returned in "result".
+ */
+#ifndef YY_INPUT
+#define YY_INPUT(buf,result,max_size) \
+/* %% [5.0] fread()/read() definition of YY_INPUT goes here unless we're doing C++ \ */\
+	if ( YY_CURRENT_BUFFER_LVALUE->yy_is_interactive ) \
+		{ \
+		int c = '*'; \
+		yy_size_t n; \
+		for ( n = 0; n < max_size && \
+			     (c = getc( yyin )) != EOF && c != '\n'; ++n ) \
+			buf[n] = (char) c; \
+		if ( c == '\n' ) \
+			buf[n++] = (char) c; \
+		if ( c == EOF && ferror( yyin ) ) \
+			YY_FATAL_ERROR( "input in flex scanner failed" ); \
+		result = n; \
+		} \
+	else \
+		{ \
+		errno=0; \
+		while ( (result = fread(buf, 1, max_size, yyin))==0 && ferror(yyin)) \
+			{ \
+			if( errno != EINTR) \
+				{ \
+				YY_FATAL_ERROR( "input in flex scanner failed" ); \
+				break; \
+				} \
+			errno=0; \
+			clearerr(yyin); \
+			} \
+		}\
+\
+/* %if-c++-only C++ definition \ */\
+/* %endif */
+
+#endif
+
+/* No semi-colon after return; correct usage is to write "yyterminate();" -
+ * we don't want an extra ';' after the "return" because that will cause
+ * some compilers to complain about unreachable statements.
+ */
+#ifndef yyterminate
+#define yyterminate() return YY_NULL
+#endif
+
+/* Number of entries by which start-condition stack grows. */
+#ifndef YY_START_STACK_INCR
+#define YY_START_STACK_INCR 25
+#endif
+
+/* Report a fatal error. */
+#ifndef YY_FATAL_ERROR
+/* %if-c-only */
+#define YY_FATAL_ERROR(msg) yy_fatal_error( msg , yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+#endif
+
+/* %if-tables-serialization structures and prototypes */
+/* %not-for-header */
+
+/* %ok-for-header */
+
+/* %not-for-header */
+
+/* %tables-yydmap generated elements */
+/* %endif */
+/* end tables serialization structures and prototypes */
+
+/* %ok-for-header */
+
+/* Default declaration of generated scanner - a define so the user can
+ * easily add parameters.
+ */
+#ifndef YY_DECL
+#define YY_DECL_IS_OURS 1
+/* %if-c-only Standard (non-C++) definition */
+
+extern int promela_lex \
+               (YYSTYPE * yylval_param ,yyscan_t yyscanner);
+
+#define YY_DECL int promela_lex \
+               (YYSTYPE * yylval_param , yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only C++ definition */
+/* %endif */
+#endif /* !YY_DECL */
+
+/* Code executed at the beginning of each rule, after yytext and yyleng
+ * have been set up.
+ */
+#ifndef YY_USER_ACTION
+#define YY_USER_ACTION
+#endif
+
+/* Code executed at the end of each rule. */
+#ifndef YY_BREAK
+#define YY_BREAK break;
+#endif
+
+/* %% [6.0] YY_RULE_SETUP definition goes here */
+#define YY_RULE_SETUP \
+	YY_USER_ACTION
+
+/* %not-for-header */
+
+/** The main scanner function which does all the work.
+ */
+YY_DECL
+{
+	register yy_state_type yy_current_state;
+	register char *yy_cp, *yy_bp;
+	register int yy_act;
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+
+/* %% [7.0] user's declarations go here */
+#line 24 "promela.l"
+
+
+#line 897 "promela.lex.yy.cpp"
+
+    yylval = yylval_param;
+
+	if ( !yyg->yy_init )
+		{
+		yyg->yy_init = 1;
+
+#ifdef YY_USER_INIT
+		YY_USER_INIT;
+#endif
+
+		if ( ! yyg->yy_start )
+			yyg->yy_start = 1;	/* first start state */
+
+		if ( ! yyin )
+/* %if-c-only */
+			yyin = stdin;
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+
+		if ( ! yyout )
+/* %if-c-only */
+			yyout = stdout;
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+
+		if ( ! YY_CURRENT_BUFFER ) {
+			promela_ensure_buffer_stack (yyscanner);
+			YY_CURRENT_BUFFER_LVALUE =
+				promela__create_buffer(yyin,YY_BUF_SIZE ,yyscanner);
+		}
+
+		promela__load_buffer_state(yyscanner );
+		}
+
+	while ( 1 )		/* loops until end-of-file is reached */
+		{
+/* %% [8.0] yymore()-related code goes here */
+		yy_cp = yyg->yy_c_buf_p;
+
+		/* Support of yytext. */
+		*yy_cp = yyg->yy_hold_char;
+
+		/* yy_bp points to the position in yy_ch_buf of the start of
+		 * the current run.
+		 */
+		yy_bp = yy_cp;
+
+/* %% [9.0] code to set up and find next match goes here */
+		yy_current_state = yyg->yy_start;
+yy_match:
+		do
+			{
+			register YY_CHAR yy_c = yy_ec[YY_SC_TO_UI(*yy_cp)];
+			if ( yy_accept[yy_current_state] )
+				{
+				yyg->yy_last_accepting_state = yy_current_state;
+				yyg->yy_last_accepting_cpos = yy_cp;
+				}
+			while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
+				{
+				yy_current_state = (int) yy_def[yy_current_state];
+				if ( yy_current_state >= 84 )
+					yy_c = yy_meta[(unsigned int) yy_c];
+				}
+			yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
+			++yy_cp;
+			}
+		while ( yy_current_state != 83 );
+		yy_cp = yyg->yy_last_accepting_cpos;
+		yy_current_state = yyg->yy_last_accepting_state;
+
+yy_find_action:
+/* %% [10.0] code to find the action number goes here */
+		yy_act = yy_accept[yy_current_state];
+
+		YY_DO_BEFORE_ACTION;
+
+/* %% [11.0] code for yylineno update goes here */
+
+do_action:	/* This label is used only to access EOF actions. */
+
+/* %% [12.0] debug code goes here */
+		if ( yy_flex_debug )
+			{
+			if ( yy_act == 0 )
+				fprintf( stderr, "--scanner backing up\n" );
+			else if ( yy_act < 34 )
+				fprintf( stderr, "--accepting rule at line %ld (\"%s\")\n",
+				         (long)yy_rule_linenum[yy_act], yytext );
+			else if ( yy_act == 34 )
+				fprintf( stderr, "--accepting default rule (\"%s\")\n",
+				         yytext );
+			else if ( yy_act == 35 )
+				fprintf( stderr, "--(end of buffer or a NUL)\n" );
+			else
+				fprintf( stderr, "--EOF (start condition %d)\n", YY_START );
+			}
+
+		switch ( yy_act )
+	{ /* beginning of action switch */
+/* %% [13.0] actions go here */
+			case 0: /* must back up */
+			/* undo the effects of YY_DO_BEFORE_ACTION */
+			*yy_cp = yyg->yy_hold_char;
+			yy_cp = yyg->yy_last_accepting_cpos;
+			yy_current_state = yyg->yy_last_accepting_state;
+			goto yy_find_action;
+
+case 1:
+YY_RULE_SETUP
+#line 26 "promela.l"
+{
+  //printf("TYPE: %s\n", yytext);
+  yylval->value = strdup(yytext);
+  return TYPE;
+}
+	YY_BREAK
+case 2:
+YY_RULE_SETUP
+#line 32 "promela.l"
+{ return LEN; }
+	YY_BREAK
+case 3:
+YY_RULE_SETUP
+#line 33 "promela.l"
+{ yylval->value = strdup(yytext); return CONST; }
+	YY_BREAK
+case 4:
+YY_RULE_SETUP
+#line 35 "promela.l"
+{ return NEG; }
+	YY_BREAK
+case 5:
+YY_RULE_SETUP
+#line 36 "promela.l"
+{ return COMPL; }
+	YY_BREAK
+case 6:
+YY_RULE_SETUP
+#line 38 "promela.l"
+{ return TIMES; }
+	YY_BREAK
+case 7:
+YY_RULE_SETUP
+#line 39 "promela.l"
+{ return DIVIDE; }
+	YY_BREAK
+case 8:
+YY_RULE_SETUP
+#line 40 "promela.l"
+{ return MODULO; }
+	YY_BREAK
+case 9:
+YY_RULE_SETUP
+#line 42 "promela.l"
+{ return PLUS; }
+	YY_BREAK
+case 10:
+YY_RULE_SETUP
+#line 43 "promela.l"
+{ return MINUS; }
+	YY_BREAK
+case 11:
+YY_RULE_SETUP
+#line 45 "promela.l"
+{ return LSHIFT; }
+	YY_BREAK
+case 12:
+YY_RULE_SETUP
+#line 46 "promela.l"
+{ return RSHIFT; }
+	YY_BREAK
+case 13:
+YY_RULE_SETUP
+#line 48 "promela.l"
+{ return LE; }
+	YY_BREAK
+case 14:
+YY_RULE_SETUP
+#line 49 "promela.l"
+{ return GE; }
+	YY_BREAK
+case 15:
+YY_RULE_SETUP
+#line 50 "promela.l"
+{ return LT; }
+	YY_BREAK
+case 16:
+YY_RULE_SETUP
+#line 51 "promela.l"
+{ return GT; }
+	YY_BREAK
+case 17:
+YY_RULE_SETUP
+#line 53 "promela.l"
+{ return NE; }
+	YY_BREAK
+case 18:
+YY_RULE_SETUP
+#line 54 "promela.l"
+{ return EQ; }
+	YY_BREAK
+case 19:
+YY_RULE_SETUP
+#line 56 "promela.l"
+{ return BITAND; }
+	YY_BREAK
+case 20:
+YY_RULE_SETUP
+#line 57 "promela.l"
+{ return BITXOR; }
+	YY_BREAK
+case 21:
+YY_RULE_SETUP
+#line 58 "promela.l"
+{ return BITOR; }
+	YY_BREAK
+case 22:
+YY_RULE_SETUP
+#line 61 "promela.l"
+{ return AND; }
+	YY_BREAK
+case 23:
+YY_RULE_SETUP
+#line 62 "promela.l"
+{ return OR; }
+	YY_BREAK
+case 24:
+YY_RULE_SETUP
+#line 64 "promela.l"
+{ return DOT; }
+	YY_BREAK
+case 25:
+YY_RULE_SETUP
+#line 66 "promela.l"
+{ return LBRACKET; }
+	YY_BREAK
+case 26:
+YY_RULE_SETUP
+#line 67 "promela.l"
+{ return RBRACKET; }
+	YY_BREAK
+case 27:
+YY_RULE_SETUP
+#line 69 "promela.l"
+{ return ASGN; }
+	YY_BREAK
+case 28:
+YY_RULE_SETUP
+#line 71 "promela.l"
+{ yylval->value = strdup(yytext); return CONST; }
+	YY_BREAK
+case 29:
+YY_RULE_SETUP
+#line 72 "promela.l"
+{ yylval->value = strdup(yytext); return NAME; }
+	YY_BREAK
+case 30:
+/* rule 30 can match eol */
+YY_RULE_SETUP
+#line 74 "promela.l"
+{ }
+	YY_BREAK
+case 31:
+YY_RULE_SETUP
+#line 76 "promela.l"
+/* eat up one-line comments */
+	YY_BREAK
+case 32:
+/* rule 32 can match eol */
+YY_RULE_SETUP
+#line 78 "promela.l"
+/* eat up whitespace */
+	YY_BREAK
+case 33:
+YY_RULE_SETUP
+#line 80 "promela.l"
+{ /*printf( "Unrecognized character: %s\n", yytext ); */ }
+	YY_BREAK
+case 34:
+YY_RULE_SETUP
+#line 81 "promela.l"
+ECHO;
+	YY_BREAK
+#line 1185 "promela.lex.yy.cpp"
+case YY_STATE_EOF(INITIAL):
+	yyterminate();
+
+	case YY_END_OF_BUFFER:
+		{
+		/* Amount of text matched not including the EOB char. */
+		int yy_amount_of_matched_text = (int) (yy_cp - yyg->yytext_ptr) - 1;
+
+		/* Undo the effects of YY_DO_BEFORE_ACTION. */
+		*yy_cp = yyg->yy_hold_char;
+		YY_RESTORE_YY_MORE_OFFSET
+
+		if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_NEW )
+			{
+			/* We're scanning a new file or input source.  It's
+			 * possible that this happened because the user
+			 * just pointed yyin at a new source and called
+			 * promela_lex().  If so, then we have to assure
+			 * consistency between YY_CURRENT_BUFFER and our
+			 * globals.  Here is the right place to do so, because
+			 * this is the first action (other than possibly a
+			 * back-up) that will match for the new input source.
+			 */
+			yyg->yy_n_chars = YY_CURRENT_BUFFER_LVALUE->yy_n_chars;
+			YY_CURRENT_BUFFER_LVALUE->yy_input_file = yyin;
+			YY_CURRENT_BUFFER_LVALUE->yy_buffer_status = YY_BUFFER_NORMAL;
+			}
+
+		/* Note that here we test for yy_c_buf_p "<=" to the position
+		 * of the first EOB in the buffer, since yy_c_buf_p will
+		 * already have been incremented past the NUL character
+		 * (since all states make transitions on EOB to the
+		 * end-of-buffer state).  Contrast this with the test
+		 * in input().
+		 */
+		if ( yyg->yy_c_buf_p <= &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[yyg->yy_n_chars] )
+			{ /* This was really a NUL. */
+			yy_state_type yy_next_state;
+
+			yyg->yy_c_buf_p = yyg->yytext_ptr + yy_amount_of_matched_text;
+
+			yy_current_state = yy_get_previous_state( yyscanner );
+
+			/* Okay, we're now positioned to make the NUL
+			 * transition.  We couldn't have
+			 * yy_get_previous_state() go ahead and do it
+			 * for us because it doesn't know how to deal
+			 * with the possibility of jamming (and we don't
+			 * want to build jamming into it because then it
+			 * will run more slowly).
+			 */
+
+			yy_next_state = yy_try_NUL_trans( yy_current_state , yyscanner);
+
+			yy_bp = yyg->yytext_ptr + YY_MORE_ADJ;
+
+			if ( yy_next_state )
+				{
+				/* Consume the NUL. */
+				yy_cp = ++yyg->yy_c_buf_p;
+				yy_current_state = yy_next_state;
+				goto yy_match;
+				}
+
+			else
+				{
+/* %% [14.0] code to do back-up for compressed tables and set up yy_cp goes here */
+				yy_cp = yyg->yy_last_accepting_cpos;
+				yy_current_state = yyg->yy_last_accepting_state;
+				goto yy_find_action;
+				}
+			}
+
+		else switch ( yy_get_next_buffer( yyscanner ) )
+			{
+			case EOB_ACT_END_OF_FILE:
+				{
+				yyg->yy_did_buffer_switch_on_eof = 0;
+
+				if ( promela_wrap(yyscanner ) )
+					{
+					/* Note: because we've taken care in
+					 * yy_get_next_buffer() to have set up
+					 * yytext, we can now set up
+					 * yy_c_buf_p so that if some total
+					 * hoser (like flex itself) wants to
+					 * call the scanner after we return the
+					 * YY_NULL, it'll still work - another
+					 * YY_NULL will get returned.
+					 */
+					yyg->yy_c_buf_p = yyg->yytext_ptr + YY_MORE_ADJ;
+
+					yy_act = YY_STATE_EOF(YY_START);
+					goto do_action;
+					}
+
+				else
+					{
+					if ( ! yyg->yy_did_buffer_switch_on_eof )
+						YY_NEW_FILE;
+					}
+				break;
+				}
+
+			case EOB_ACT_CONTINUE_SCAN:
+				yyg->yy_c_buf_p =
+					yyg->yytext_ptr + yy_amount_of_matched_text;
+
+				yy_current_state = yy_get_previous_state( yyscanner );
+
+				yy_cp = yyg->yy_c_buf_p;
+				yy_bp = yyg->yytext_ptr + YY_MORE_ADJ;
+				goto yy_match;
+
+			case EOB_ACT_LAST_MATCH:
+				yyg->yy_c_buf_p =
+				&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[yyg->yy_n_chars];
+
+				yy_current_state = yy_get_previous_state( yyscanner );
+
+				yy_cp = yyg->yy_c_buf_p;
+				yy_bp = yyg->yytext_ptr + YY_MORE_ADJ;
+				goto yy_find_action;
+			}
+		break;
+		}
+
+	default:
+		YY_FATAL_ERROR(
+			"fatal flex scanner internal error--no action found" );
+	} /* end of action switch */
+		} /* end of scanning one token */
+} /* end of promela_lex */
+/* %ok-for-header */
+
+/* %if-c++-only */
+/* %not-for-header */
+
+/* %ok-for-header */
+
+/* %endif */
+
+/* yy_get_next_buffer - try to read in a new buffer
+ *
+ * Returns a code representing an action:
+ *	EOB_ACT_LAST_MATCH -
+ *	EOB_ACT_CONTINUE_SCAN - continue scanning from current position
+ *	EOB_ACT_END_OF_FILE - end of file
+ */
+/* %if-c-only */
+static int yy_get_next_buffer (yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+	register char *dest = YY_CURRENT_BUFFER_LVALUE->yy_ch_buf;
+	register char *source = yyg->yytext_ptr;
+	register int number_to_move, i;
+	int ret_val;
+
+	if ( yyg->yy_c_buf_p > &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[yyg->yy_n_chars + 1] )
+		YY_FATAL_ERROR(
+		"fatal flex scanner internal error--end of buffer missed" );
+
+	if ( YY_CURRENT_BUFFER_LVALUE->yy_fill_buffer == 0 )
+		{ /* Don't try to fill the buffer, so this is an EOF. */
+		if ( yyg->yy_c_buf_p - yyg->yytext_ptr - YY_MORE_ADJ == 1 )
+			{
+			/* We matched a single character, the EOB, so
+			 * treat this as a final EOF.
+			 */
+			return EOB_ACT_END_OF_FILE;
+			}
+
+		else
+			{
+			/* We matched some text prior to the EOB, first
+			 * process it.
+			 */
+			return EOB_ACT_LAST_MATCH;
+			}
+		}
+
+	/* Try to read more data. */
+
+	/* First move last chars to start of buffer. */
+	number_to_move = (int) (yyg->yy_c_buf_p - yyg->yytext_ptr) - 1;
+
+	for ( i = 0; i < number_to_move; ++i )
+		*(dest++) = *(source++);
+
+	if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_EOF_PENDING )
+		/* don't do the read, it's not guaranteed to return an EOF,
+		 * just force an EOF
+		 */
+		YY_CURRENT_BUFFER_LVALUE->yy_n_chars = yyg->yy_n_chars = 0;
+
+	else
+		{
+			yy_size_t num_to_read =
+			YY_CURRENT_BUFFER_LVALUE->yy_buf_size - number_to_move - 1;
+
+		while ( num_to_read <= 0 )
+			{ /* Not enough room in the buffer - grow it. */
+
+			/* just a shorter name for the current buffer */
+			YY_BUFFER_STATE b = YY_CURRENT_BUFFER;
+
+			int yy_c_buf_p_offset =
+				(int) (yyg->yy_c_buf_p - b->yy_ch_buf);
+
+			if ( b->yy_is_our_buffer )
+				{
+				yy_size_t new_size = b->yy_buf_size * 2;
+
+				if ( new_size <= 0 )
+					b->yy_buf_size += b->yy_buf_size / 8;
+				else
+					b->yy_buf_size *= 2;
+
+				b->yy_ch_buf = (char *)
+					/* Include room in for 2 EOB chars. */
+					promela_realloc((void *) b->yy_ch_buf,b->yy_buf_size + 2 ,yyscanner );
+				}
+			else
+				/* Can't grow it, we don't own it. */
+				b->yy_ch_buf = 0;
+
+			if ( ! b->yy_ch_buf )
+				YY_FATAL_ERROR(
+				"fatal error - scanner input buffer overflow" );
+
+			yyg->yy_c_buf_p = &b->yy_ch_buf[yy_c_buf_p_offset];
+
+			num_to_read = YY_CURRENT_BUFFER_LVALUE->yy_buf_size -
+						number_to_move - 1;
+
+			}
+
+		if ( num_to_read > YY_READ_BUF_SIZE )
+			num_to_read = YY_READ_BUF_SIZE;
+
+		/* Read in more data. */
+		YY_INPUT( (&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move]),
+			yyg->yy_n_chars, num_to_read );
+
+		YY_CURRENT_BUFFER_LVALUE->yy_n_chars = yyg->yy_n_chars;
+		}
+
+	if ( yyg->yy_n_chars == 0 )
+		{
+		if ( number_to_move == YY_MORE_ADJ )
+			{
+			ret_val = EOB_ACT_END_OF_FILE;
+			promela_restart(yyin  ,yyscanner);
+			}
+
+		else
+			{
+			ret_val = EOB_ACT_LAST_MATCH;
+			YY_CURRENT_BUFFER_LVALUE->yy_buffer_status =
+				YY_BUFFER_EOF_PENDING;
+			}
+		}
+
+	else
+		ret_val = EOB_ACT_CONTINUE_SCAN;
+
+	if ((yy_size_t) (yyg->yy_n_chars + number_to_move) > YY_CURRENT_BUFFER_LVALUE->yy_buf_size) {
+		/* Extend the array by 50%, plus the number we really need. */
+		yy_size_t new_size = yyg->yy_n_chars + number_to_move + (yyg->yy_n_chars >> 1);
+		YY_CURRENT_BUFFER_LVALUE->yy_ch_buf = (char *) promela_realloc((void *) YY_CURRENT_BUFFER_LVALUE->yy_ch_buf,new_size ,yyscanner );
+		if ( ! YY_CURRENT_BUFFER_LVALUE->yy_ch_buf )
+			YY_FATAL_ERROR( "out of dynamic memory in yy_get_next_buffer()" );
+	}
+
+	yyg->yy_n_chars += number_to_move;
+	YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[yyg->yy_n_chars] = YY_END_OF_BUFFER_CHAR;
+	YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[yyg->yy_n_chars + 1] = YY_END_OF_BUFFER_CHAR;
+
+	yyg->yytext_ptr = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[0];
+
+	return ret_val;
+}
+
+/* yy_get_previous_state - get the state just before the EOB char was reached */
+
+/* %if-c-only */
+/* %not-for-header */
+
+    static yy_state_type yy_get_previous_state (yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+	register yy_state_type yy_current_state;
+	register char *yy_cp;
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+
+/* %% [15.0] code to get the start state into yy_current_state goes here */
+	yy_current_state = yyg->yy_start;
+
+	for ( yy_cp = yyg->yytext_ptr + YY_MORE_ADJ; yy_cp < yyg->yy_c_buf_p; ++yy_cp )
+		{
+/* %% [16.0] code to find the next state goes here */
+		register YY_CHAR yy_c = (*yy_cp ? yy_ec[YY_SC_TO_UI(*yy_cp)] : 1);
+		if ( yy_accept[yy_current_state] )
+			{
+			yyg->yy_last_accepting_state = yy_current_state;
+			yyg->yy_last_accepting_cpos = yy_cp;
+			}
+		while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
+			{
+			yy_current_state = (int) yy_def[yy_current_state];
+			if ( yy_current_state >= 84 )
+				yy_c = yy_meta[(unsigned int) yy_c];
+			}
+		yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
+		}
+
+	return yy_current_state;
+}
+
+/* yy_try_NUL_trans - try to make a transition on the NUL character
+ *
+ * synopsis
+ *	next_state = yy_try_NUL_trans( current_state );
+ */
+/* %if-c-only */
+    static yy_state_type yy_try_NUL_trans  (yy_state_type yy_current_state , yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+	register int yy_is_jam;
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; /* This var may be unused depending upon options. */
+/* %% [17.0] code to find the next state, and perhaps do backing up, goes here */
+	register char *yy_cp = yyg->yy_c_buf_p;
+
+	register YY_CHAR yy_c = 1;
+	if ( yy_accept[yy_current_state] )
+		{
+		yyg->yy_last_accepting_state = yy_current_state;
+		yyg->yy_last_accepting_cpos = yy_cp;
+		}
+	while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
+		{
+		yy_current_state = (int) yy_def[yy_current_state];
+		if ( yy_current_state >= 84 )
+			yy_c = yy_meta[(unsigned int) yy_c];
+		}
+	yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
+	yy_is_jam = (yy_current_state == 83);
+
+	return yy_is_jam ? 0 : yy_current_state;
+}
+
+/* %if-c-only */
+
+    static void yyunput (int c, register char * yy_bp , yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+	register char *yy_cp;
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+
+    yy_cp = yyg->yy_c_buf_p;
+
+	/* undo effects of setting up yytext */
+	*yy_cp = yyg->yy_hold_char;
+
+	if ( yy_cp < YY_CURRENT_BUFFER_LVALUE->yy_ch_buf + 2 )
+		{ /* need to shift things up to make room */
+		/* +2 for EOB chars. */
+		register yy_size_t number_to_move = yyg->yy_n_chars + 2;
+		register char *dest = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[
+					YY_CURRENT_BUFFER_LVALUE->yy_buf_size + 2];
+		register char *source =
+				&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move];
+
+		while ( source > YY_CURRENT_BUFFER_LVALUE->yy_ch_buf )
+			*--dest = *--source;
+
+		yy_cp += (int) (dest - source);
+		yy_bp += (int) (dest - source);
+		YY_CURRENT_BUFFER_LVALUE->yy_n_chars =
+			yyg->yy_n_chars = YY_CURRENT_BUFFER_LVALUE->yy_buf_size;
+
+		if ( yy_cp < YY_CURRENT_BUFFER_LVALUE->yy_ch_buf + 2 )
+			YY_FATAL_ERROR( "flex scanner push-back overflow" );
+		}
+
+	*--yy_cp = (char) c;
+
+/* %% [18.0] update yylineno here */
+
+	yyg->yytext_ptr = yy_bp;
+	yyg->yy_hold_char = *yy_cp;
+	yyg->yy_c_buf_p = yy_cp;
+}
+/* %if-c-only */
+
+/* %endif */
+
+/* %if-c-only */
+#ifndef YY_NO_INPUT
+#ifdef __cplusplus
+    static int yyinput (yyscan_t yyscanner)
+#else
+    static int input  (yyscan_t yyscanner)
+#endif
+
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+	int c;
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+
+	*yyg->yy_c_buf_p = yyg->yy_hold_char;
+
+	if ( *yyg->yy_c_buf_p == YY_END_OF_BUFFER_CHAR )
+		{
+		/* yy_c_buf_p now points to the character we want to return.
+		 * If this occurs *before* the EOB characters, then it's a
+		 * valid NUL; if not, then we've hit the end of the buffer.
+		 */
+		if ( yyg->yy_c_buf_p < &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[yyg->yy_n_chars] )
+			/* This was really a NUL. */
+			*yyg->yy_c_buf_p = '\0';
+
+		else
+			{ /* need more input */
+			yy_size_t offset = yyg->yy_c_buf_p - yyg->yytext_ptr;
+			++yyg->yy_c_buf_p;
+
+			switch ( yy_get_next_buffer( yyscanner ) )
+				{
+				case EOB_ACT_LAST_MATCH:
+					/* This happens because yy_g_n_b()
+					 * sees that we've accumulated a
+					 * token and flags that we need to
+					 * try matching the token before
+					 * proceeding.  But for input(),
+					 * there's no matching to consider.
+					 * So convert the EOB_ACT_LAST_MATCH
+					 * to EOB_ACT_END_OF_FILE.
+					 */
+
+					/* Reset buffer status. */
+					promela_restart(yyin ,yyscanner);
+
+					/*FALLTHROUGH*/
+
+				case EOB_ACT_END_OF_FILE:
+					{
+					if ( promela_wrap(yyscanner ) )
+						return 0;
+
+					if ( ! yyg->yy_did_buffer_switch_on_eof )
+						YY_NEW_FILE;
+#ifdef __cplusplus
+					return yyinput(yyscanner);
+#else
+					return input(yyscanner);
+#endif
+					}
+
+				case EOB_ACT_CONTINUE_SCAN:
+					yyg->yy_c_buf_p = yyg->yytext_ptr + offset;
+					break;
+				}
+			}
+		}
+
+	c = *(unsigned char *) yyg->yy_c_buf_p;	/* cast for 8-bit char's */
+	*yyg->yy_c_buf_p = '\0';	/* preserve yytext */
+	yyg->yy_hold_char = *++yyg->yy_c_buf_p;
+
+/* %% [19.0] update BOL and yylineno */
+
+	return c;
+}
+/* %if-c-only */
+#endif	/* ifndef YY_NO_INPUT */
+/* %endif */
+
+/** Immediately switch to a different input stream.
+ * @param input_file A readable stream.
+ * @param yyscanner The scanner object.
+ * @note This function does not reset the start condition to @c INITIAL .
+ */
+/* %if-c-only */
+    void promela_restart  (FILE * input_file , yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+
+	if ( ! YY_CURRENT_BUFFER ){
+        promela_ensure_buffer_stack (yyscanner);
+		YY_CURRENT_BUFFER_LVALUE =
+            promela__create_buffer(yyin,YY_BUF_SIZE ,yyscanner);
+	}
+
+	promela__init_buffer(YY_CURRENT_BUFFER,input_file ,yyscanner);
+	promela__load_buffer_state(yyscanner );
+}
+
+/** Switch to a different input buffer.
+ * @param new_buffer The new input buffer.
+ * @param yyscanner The scanner object.
+ */
+/* %if-c-only */
+    void promela__switch_to_buffer  (YY_BUFFER_STATE  new_buffer , yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+
+	/* TODO. We should be able to replace this entire function body
+	 * with
+	 *		promela_pop_buffer_state();
+	 *		promela_push_buffer_state(new_buffer);
+     */
+	promela_ensure_buffer_stack (yyscanner);
+	if ( YY_CURRENT_BUFFER == new_buffer )
+		return;
+
+	if ( YY_CURRENT_BUFFER )
+		{
+		/* Flush out information for old buffer. */
+		*yyg->yy_c_buf_p = yyg->yy_hold_char;
+		YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = yyg->yy_c_buf_p;
+		YY_CURRENT_BUFFER_LVALUE->yy_n_chars = yyg->yy_n_chars;
+		}
+
+	YY_CURRENT_BUFFER_LVALUE = new_buffer;
+	promela__load_buffer_state(yyscanner );
+
+	/* We don't actually know whether we did this switch during
+	 * EOF (promela_wrap()) processing, but the only time this flag
+	 * is looked at is after promela_wrap() is called, so it's safe
+	 * to go ahead and always set it.
+	 */
+	yyg->yy_did_buffer_switch_on_eof = 1;
+}
+
+/* %if-c-only */
+static void promela__load_buffer_state  (yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+	yyg->yy_n_chars = YY_CURRENT_BUFFER_LVALUE->yy_n_chars;
+	yyg->yytext_ptr = yyg->yy_c_buf_p = YY_CURRENT_BUFFER_LVALUE->yy_buf_pos;
+	yyin = YY_CURRENT_BUFFER_LVALUE->yy_input_file;
+	yyg->yy_hold_char = *yyg->yy_c_buf_p;
+}
+
+/** Allocate and initialize an input buffer state.
+ * @param file A readable stream.
+ * @param size The character buffer size in bytes. When in doubt, use @c YY_BUF_SIZE.
+ * @param yyscanner The scanner object.
+ * @return the allocated buffer state.
+ */
+/* %if-c-only */
+    YY_BUFFER_STATE promela__create_buffer  (FILE * file, int  size , yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+	YY_BUFFER_STATE b;
+    
+	b = (YY_BUFFER_STATE) promela_alloc(sizeof( struct yy_buffer_state ) ,yyscanner );
+	if ( ! b )
+		YY_FATAL_ERROR( "out of dynamic memory in promela__create_buffer()" );
+
+	b->yy_buf_size = size;
+
+	/* yy_ch_buf has to be 2 characters longer than the size given because
+	 * we need to put in 2 end-of-buffer characters.
+	 */
+	b->yy_ch_buf = (char *) promela_alloc(b->yy_buf_size + 2 ,yyscanner );
+	if ( ! b->yy_ch_buf )
+		YY_FATAL_ERROR( "out of dynamic memory in promela__create_buffer()" );
+
+	b->yy_is_our_buffer = 1;
+
+	promela__init_buffer(b,file ,yyscanner);
+
+	return b;
+}
+
+/** Destroy the buffer.
+ * @param b a buffer created with promela__create_buffer()
+ * @param yyscanner The scanner object.
+ */
+/* %if-c-only */
+    void promela__delete_buffer (YY_BUFFER_STATE  b , yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+
+	if ( ! b )
+		return;
+
+	if ( b == YY_CURRENT_BUFFER ) /* Not sure if we should pop here. */
+		YY_CURRENT_BUFFER_LVALUE = (YY_BUFFER_STATE) 0;
+
+	if ( b->yy_is_our_buffer )
+		promela_free((void *) b->yy_ch_buf ,yyscanner );
+
+	promela_free((void *) b ,yyscanner );
+}
+
+/* %if-c-only */
+
+/* %endif */
+
+/* %if-c++-only */
+/* %endif */
+
+/* Initializes or reinitializes a buffer.
+ * This function is sometimes called more than once on the same buffer,
+ * such as during a promela_restart() or at EOF.
+ */
+/* %if-c-only */
+    static void promela__init_buffer  (YY_BUFFER_STATE  b, FILE * file , yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+
+{
+	int oerrno = errno;
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+
+	promela__flush_buffer(b ,yyscanner);
+
+	b->yy_input_file = file;
+	b->yy_fill_buffer = 1;
+
+    /* If b is the current buffer, then promela__init_buffer was _probably_
+     * called from promela_restart() or through yy_get_next_buffer.
+     * In that case, we don't want to reset the lineno or column.
+     */
+    if (b != YY_CURRENT_BUFFER){
+        b->yy_bs_lineno = 1;
+        b->yy_bs_column = 0;
+    }
+
+/* %if-c-only */
+
+        b->yy_is_interactive = 0;
+    
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+	errno = oerrno;
+}
+
+/** Discard all buffered characters. On the next scan, YY_INPUT will be called.
+ * @param b the buffer state to be flushed, usually @c YY_CURRENT_BUFFER.
+ * @param yyscanner The scanner object.
+ */
+/* %if-c-only */
+    void promela__flush_buffer (YY_BUFFER_STATE  b , yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+	if ( ! b )
+		return;
+
+	b->yy_n_chars = 0;
+
+	/* We always need two end-of-buffer characters.  The first causes
+	 * a transition to the end-of-buffer state.  The second causes
+	 * a jam in that state.
+	 */
+	b->yy_ch_buf[0] = YY_END_OF_BUFFER_CHAR;
+	b->yy_ch_buf[1] = YY_END_OF_BUFFER_CHAR;
+
+	b->yy_buf_pos = &b->yy_ch_buf[0];
+
+	b->yy_at_bol = 1;
+	b->yy_buffer_status = YY_BUFFER_NEW;
+
+	if ( b == YY_CURRENT_BUFFER )
+		promela__load_buffer_state(yyscanner );
+}
+
+/* %if-c-or-c++ */
+/** Pushes the new state onto the stack. The new state becomes
+ *  the current state. This function will allocate the stack
+ *  if necessary.
+ *  @param new_buffer The new state.
+ *  @param yyscanner The scanner object.
+ */
+/* %if-c-only */
+void promela_push_buffer_state (YY_BUFFER_STATE new_buffer , yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+	if (new_buffer == NULL)
+		return;
+
+	promela_ensure_buffer_stack(yyscanner);
+
+	/* This block is copied from promela__switch_to_buffer. */
+	if ( YY_CURRENT_BUFFER )
+		{
+		/* Flush out information for old buffer. */
+		*yyg->yy_c_buf_p = yyg->yy_hold_char;
+		YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = yyg->yy_c_buf_p;
+		YY_CURRENT_BUFFER_LVALUE->yy_n_chars = yyg->yy_n_chars;
+		}
+
+	/* Only push if top exists. Otherwise, replace top. */
+	if (YY_CURRENT_BUFFER)
+		yyg->yy_buffer_stack_top++;
+	YY_CURRENT_BUFFER_LVALUE = new_buffer;
+
+	/* copied from promela__switch_to_buffer. */
+	promela__load_buffer_state(yyscanner );
+	yyg->yy_did_buffer_switch_on_eof = 1;
+}
+/* %endif */
+
+/* %if-c-or-c++ */
+/** Removes and deletes the top of the stack, if present.
+ *  The next element becomes the new top.
+ *  @param yyscanner The scanner object.
+ */
+/* %if-c-only */
+void promela_pop_buffer_state (yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+	if (!YY_CURRENT_BUFFER)
+		return;
+
+	promela__delete_buffer(YY_CURRENT_BUFFER ,yyscanner);
+	YY_CURRENT_BUFFER_LVALUE = NULL;
+	if (yyg->yy_buffer_stack_top > 0)
+		--yyg->yy_buffer_stack_top;
+
+	if (YY_CURRENT_BUFFER) {
+		promela__load_buffer_state(yyscanner );
+		yyg->yy_did_buffer_switch_on_eof = 1;
+	}
+}
+/* %endif */
+
+/* %if-c-or-c++ */
+/* Allocates the stack if it does not exist.
+ *  Guarantees space for at least one push.
+ */
+/* %if-c-only */
+static void promela_ensure_buffer_stack (yyscan_t yyscanner)
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+{
+	yy_size_t num_to_alloc;
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+
+	if (!yyg->yy_buffer_stack) {
+
+		/* First allocation is just for 2 elements, since we don't know if this
+		 * scanner will even need a stack. We use 2 instead of 1 to avoid an
+		 * immediate realloc on the next call.
+         */
+		num_to_alloc = 1;
+		yyg->yy_buffer_stack = (struct yy_buffer_state**)promela_alloc
+								(num_to_alloc * sizeof(struct yy_buffer_state*)
+								, yyscanner);
+		if ( ! yyg->yy_buffer_stack )
+			YY_FATAL_ERROR( "out of dynamic memory in promela_ensure_buffer_stack()" );
+								  
+		memset(yyg->yy_buffer_stack, 0, num_to_alloc * sizeof(struct yy_buffer_state*));
+				
+		yyg->yy_buffer_stack_max = num_to_alloc;
+		yyg->yy_buffer_stack_top = 0;
+		return;
+	}
+
+	if (yyg->yy_buffer_stack_top >= (yyg->yy_buffer_stack_max) - 1){
+
+		/* Increase the buffer to prepare for a possible push. */
+		int grow_size = 8 /* arbitrary grow size */;
+
+		num_to_alloc = yyg->yy_buffer_stack_max + grow_size;
+		yyg->yy_buffer_stack = (struct yy_buffer_state**)promela_realloc
+								(yyg->yy_buffer_stack,
+								num_to_alloc * sizeof(struct yy_buffer_state*)
+								, yyscanner);
+		if ( ! yyg->yy_buffer_stack )
+			YY_FATAL_ERROR( "out of dynamic memory in promela_ensure_buffer_stack()" );
+
+		/* zero only the new slots.*/
+		memset(yyg->yy_buffer_stack + yyg->yy_buffer_stack_max, 0, grow_size * sizeof(struct yy_buffer_state*));
+		yyg->yy_buffer_stack_max = num_to_alloc;
+	}
+}
+/* %endif */
+
+/* %if-c-only */
+/** Setup the input buffer state to scan directly from a user-specified character buffer.
+ * @param base the character buffer
+ * @param size the size in bytes of the character buffer
+ * @param yyscanner The scanner object.
+ * @return the newly allocated buffer state object. 
+ */
+YY_BUFFER_STATE promela__scan_buffer  (char * base, yy_size_t  size , yyscan_t yyscanner)
+{
+	YY_BUFFER_STATE b;
+    
+	if ( size < 2 ||
+	     base[size-2] != YY_END_OF_BUFFER_CHAR ||
+	     base[size-1] != YY_END_OF_BUFFER_CHAR )
+		/* They forgot to leave room for the EOB's. */
+		return 0;
+
+	b = (YY_BUFFER_STATE) promela_alloc(sizeof( struct yy_buffer_state ) ,yyscanner );
+	if ( ! b )
+		YY_FATAL_ERROR( "out of dynamic memory in promela__scan_buffer()" );
+
+	b->yy_buf_size = size - 2;	/* "- 2" to take care of EOB's */
+	b->yy_buf_pos = b->yy_ch_buf = base;
+	b->yy_is_our_buffer = 0;
+	b->yy_input_file = 0;
+	b->yy_n_chars = b->yy_buf_size;
+	b->yy_is_interactive = 0;
+	b->yy_at_bol = 1;
+	b->yy_fill_buffer = 0;
+	b->yy_buffer_status = YY_BUFFER_NEW;
+
+	promela__switch_to_buffer(b ,yyscanner );
+
+	return b;
+}
+/* %endif */
+
+/* %if-c-only */
+/** Setup the input buffer state to scan a string. The next call to promela_lex() will
+ * scan from a @e copy of @a str.
+ * @param yystr a NUL-terminated string to scan
+ * @param yyscanner The scanner object.
+ * @return the newly allocated buffer state object.
+ * @note If you want to scan bytes that may contain NUL values, then use
+ *       promela__scan_bytes() instead.
+ */
+YY_BUFFER_STATE promela__scan_string (yyconst char * yystr , yyscan_t yyscanner)
+{
+    
+	return promela__scan_bytes(yystr,strlen(yystr) ,yyscanner);
+}
+/* %endif */
+
+/* %if-c-only */
+/** Setup the input buffer state to scan the given bytes. The next call to promela_lex() will
+ * scan from a @e copy of @a bytes.
+ * @param bytes the byte buffer to scan
+ * @param len the number of bytes in the buffer pointed to by @a bytes.
+ * @param yyscanner The scanner object.
+ * @return the newly allocated buffer state object.
+ */
+YY_BUFFER_STATE promela__scan_bytes  (yyconst char * yybytes, yy_size_t  _yybytes_len , yyscan_t yyscanner)
+{
+	YY_BUFFER_STATE b;
+	char *buf;
+	yy_size_t n, i;
+    
+	/* Get memory for full buffer, including space for trailing EOB's. */
+	n = _yybytes_len + 2;
+	buf = (char *) promela_alloc(n ,yyscanner );
+	if ( ! buf )
+		YY_FATAL_ERROR( "out of dynamic memory in promela__scan_bytes()" );
+
+	for ( i = 0; i < _yybytes_len; ++i )
+		buf[i] = yybytes[i];
+
+	buf[_yybytes_len] = buf[_yybytes_len+1] = YY_END_OF_BUFFER_CHAR;
+
+	b = promela__scan_buffer(buf,n ,yyscanner);
+	if ( ! b )
+		YY_FATAL_ERROR( "bad buffer in promela__scan_bytes()" );
+
+	/* It's okay to grow etc. this buffer, and we should throw it
+	 * away when we're done.
+	 */
+	b->yy_is_our_buffer = 1;
+
+	return b;
+}
+/* %endif */
+
+#ifndef YY_EXIT_FAILURE
+#define YY_EXIT_FAILURE 2
+#endif
+
+/* %if-c-only */
+static void yy_fatal_error (yyconst char* msg , yyscan_t yyscanner)
+{
+    	(void) fprintf( stderr, "%s\n", msg );
+	exit( YY_EXIT_FAILURE );
+}
+/* %endif */
+/* %if-c++-only */
+/* %endif */
+
+/* Redefine yyless() so it works in section 3 code. */
+
+#undef yyless
+#define yyless(n) \
+	do \
+		{ \
+		/* Undo effects of setting up yytext. */ \
+        int yyless_macro_arg = (n); \
+        YY_LESS_LINENO(yyless_macro_arg);\
+		yytext[yyleng] = yyg->yy_hold_char; \
+		yyg->yy_c_buf_p = yytext + yyless_macro_arg; \
+		yyg->yy_hold_char = *yyg->yy_c_buf_p; \
+		*yyg->yy_c_buf_p = '\0'; \
+		yyleng = yyless_macro_arg; \
+		} \
+	while ( 0 )
+
+/* Accessor  methods (get/set functions) to struct members. */
+
+/* %if-c-only */
+/* %if-reentrant */
+
+/** Get the user-defined data for this scanner.
+ * @param yyscanner The scanner object.
+ */
+YY_EXTRA_TYPE promela_get_extra  (yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    return yyextra;
+}
+
+/* %endif */
+
+/** Get the current line number.
+ * @param yyscanner The scanner object.
+ */
+int promela_get_lineno  (yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    
+        if (! YY_CURRENT_BUFFER)
+            return 0;
+    
+    return yylineno;
+}
+
+/** Get the current column number.
+ * @param yyscanner The scanner object.
+ */
+int promela_get_column  (yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    
+        if (! YY_CURRENT_BUFFER)
+            return 0;
+    
+    return yycolumn;
+}
+
+/** Get the input stream.
+ * @param yyscanner The scanner object.
+ */
+FILE *promela_get_in  (yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    return yyin;
+}
+
+/** Get the output stream.
+ * @param yyscanner The scanner object.
+ */
+FILE *promela_get_out  (yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    return yyout;
+}
+
+/** Get the length of the current token.
+ * @param yyscanner The scanner object.
+ */
+yy_size_t promela_get_leng  (yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    return yyleng;
+}
+
+/** Get the current token.
+ * @param yyscanner The scanner object.
+ */
+
+char *promela_get_text  (yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    return yytext;
+}
+
+/* %if-reentrant */
+
+/** Set the user-defined data. This data is never touched by the scanner.
+ * @param user_defined The data to be associated with this scanner.
+ * @param yyscanner The scanner object.
+ */
+void promela_set_extra (YY_EXTRA_TYPE  user_defined , yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    yyextra = user_defined ;
+}
+
+/* %endif */
+
+/** Set the current line number.
+ * @param line_number
+ * @param yyscanner The scanner object.
+ */
+void promela_set_lineno (int  line_number , yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+
+        /* lineno is only valid if an input buffer exists. */
+        if (! YY_CURRENT_BUFFER )
+           yy_fatal_error( "promela_set_lineno called with no buffer" , yyscanner); 
+    
+    yylineno = line_number;
+}
+
+/** Set the current column.
+ * @param line_number
+ * @param yyscanner The scanner object.
+ */
+void promela_set_column (int  column_no , yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+
+        /* column is only valid if an input buffer exists. */
+        if (! YY_CURRENT_BUFFER )
+           yy_fatal_error( "promela_set_column called with no buffer" , yyscanner); 
+    
+    yycolumn = column_no;
+}
+
+/** Set the input stream. This does not discard the current
+ * input buffer.
+ * @param in_str A readable stream.
+ * @param yyscanner The scanner object.
+ * @see promela__switch_to_buffer
+ */
+void promela_set_in (FILE *  in_str , yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    yyin = in_str ;
+}
+
+void promela_set_out (FILE *  out_str , yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    yyout = out_str ;
+}
+
+int promela_get_debug  (yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    return yy_flex_debug;
+}
+
+void promela_set_debug (int  bdebug , yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    yy_flex_debug = bdebug ;
+}
+
+/* %endif */
+
+/* %if-reentrant */
+/* Accessor methods for yylval and yylloc */
+
+/* %if-bison-bridge */
+
+YYSTYPE * promela_get_lval  (yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    return yylval;
+}
+
+void promela_set_lval (YYSTYPE *  yylval_param , yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    yylval = yylval_param;
+}
+
+/* %endif */
+
+/* User-visible API */
+
+/* promela_lex_init is special because it creates the scanner itself, so it is
+ * the ONLY reentrant function that doesn't take the scanner as the last argument.
+ * That's why we explicitly handle the declaration, instead of using our macros.
+ */
+
+int promela_lex_init(yyscan_t* ptr_yy_globals)
+
+{
+    if (ptr_yy_globals == NULL){
+        errno = EINVAL;
+        return 1;
+    }
+
+    *ptr_yy_globals = (yyscan_t) promela_alloc ( sizeof( struct yyguts_t ), NULL );
+
+    if (*ptr_yy_globals == NULL){
+        errno = ENOMEM;
+        return 1;
+    }
+
+    /* By setting to 0xAA, we expose bugs in yy_init_globals. Leave at 0x00 for releases. */
+    memset(*ptr_yy_globals,0x00,sizeof(struct yyguts_t));
+
+    return yy_init_globals ( *ptr_yy_globals );
+}
+
+/* promela_lex_init_extra has the same functionality as promela_lex_init, but follows the
+ * convention of taking the scanner as the last argument. Note however, that
+ * this is a *pointer* to a scanner, as it will be allocated by this call (and
+ * is the reason, too, why this function also must handle its own declaration).
+ * The user defined value in the first argument will be available to promela_alloc in
+ * the yyextra field.
+ */
+
+int promela_lex_init_extra(YY_EXTRA_TYPE yy_user_defined,yyscan_t* ptr_yy_globals )
+
+{
+    struct yyguts_t dummy_yyguts;
+
+    promela_set_extra (yy_user_defined, &dummy_yyguts);
+
+    if (ptr_yy_globals == NULL){
+        errno = EINVAL;
+        return 1;
+    }
+	
+    *ptr_yy_globals = (yyscan_t) promela_alloc ( sizeof( struct yyguts_t ), &dummy_yyguts );
+	
+    if (*ptr_yy_globals == NULL){
+        errno = ENOMEM;
+        return 1;
+    }
+    
+    /* By setting to 0xAA, we expose bugs in
+    yy_init_globals. Leave at 0x00 for releases. */
+    memset(*ptr_yy_globals,0x00,sizeof(struct yyguts_t));
+    
+    promela_set_extra (yy_user_defined, *ptr_yy_globals);
+    
+    return yy_init_globals ( *ptr_yy_globals );
+}
+
+/* %endif if-c-only */
+
+/* %if-c-only */
+static int yy_init_globals (yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+    /* Initialization is the same as for the non-reentrant scanner.
+     * This function is called from promela_lex_destroy(), so don't allocate here.
+     */
+
+    yyg->yy_buffer_stack = 0;
+    yyg->yy_buffer_stack_top = 0;
+    yyg->yy_buffer_stack_max = 0;
+    yyg->yy_c_buf_p = (char *) 0;
+    yyg->yy_init = 0;
+    yyg->yy_start = 0;
+
+    yyg->yy_start_stack_ptr = 0;
+    yyg->yy_start_stack_depth = 0;
+    yyg->yy_start_stack =  NULL;
+
+/* Defined in main.c */
+#ifdef YY_STDINIT
+    yyin = stdin;
+    yyout = stdout;
+#else
+    yyin = (FILE *) 0;
+    yyout = (FILE *) 0;
+#endif
+
+    /* For future reference: Set errno on error, since we are called by
+     * promela_lex_init()
+     */
+    return 0;
+}
+/* %endif */
+
+/* %if-c-only SNIP! this currently causes conflicts with the c++ scanner */
+/* promela_lex_destroy is for both reentrant and non-reentrant scanners. */
+int promela_lex_destroy  (yyscan_t yyscanner)
+{
+    struct yyguts_t * yyg = (struct yyguts_t*)yyscanner;
+
+    /* Pop the buffer stack, destroying each element. */
+	while(YY_CURRENT_BUFFER){
+		promela__delete_buffer(YY_CURRENT_BUFFER ,yyscanner );
+		YY_CURRENT_BUFFER_LVALUE = NULL;
+		promela_pop_buffer_state(yyscanner);
+	}
+
+	/* Destroy the stack itself. */
+	promela_free(yyg->yy_buffer_stack ,yyscanner);
+	yyg->yy_buffer_stack = NULL;
+
+    /* Destroy the start condition stack. */
+        promela_free(yyg->yy_start_stack ,yyscanner );
+        yyg->yy_start_stack = NULL;
+
+    /* Reset the globals. This is important in a non-reentrant scanner so the next time
+     * promela_lex() is called, initialization will occur. */
+    yy_init_globals( yyscanner);
+
+/* %if-reentrant */
+    /* Destroy the main struct (reentrant only). */
+    promela_free ( yyscanner , yyscanner );
+    yyscanner = NULL;
+/* %endif */
+    return 0;
+}
+/* %endif */
+
+/*
+ * Internal utility routines.
+ */
+
+#ifndef yytext_ptr
+static void yy_flex_strncpy (char* s1, yyconst char * s2, int n , yyscan_t yyscanner)
+{
+	register int i;
+	for ( i = 0; i < n; ++i )
+		s1[i] = s2[i];
+}
+#endif
+
+#ifdef YY_NEED_STRLEN
+static int yy_flex_strlen (yyconst char * s , yyscan_t yyscanner)
+{
+	register int n;
+	for ( n = 0; s[n]; ++n )
+		;
+
+	return n;
+}
+#endif
+
+void *promela_alloc (yy_size_t  size , yyscan_t yyscanner)
+{
+	return (void *) malloc( size );
+}
+
+void *promela_realloc  (void * ptr, yy_size_t  size , yyscan_t yyscanner)
+{
+	/* The cast to (char *) in the following accommodates both
+	 * implementations that use char* generic pointers, and those
+	 * that use void* generic pointers.  It works with the latter
+	 * because both ANSI C and C++ allow castless assignment from
+	 * any pointer type to void*, and deal with argument conversions
+	 * as though doing an assignment.
+	 */
+	return (void *) realloc( (char *) ptr, size );
+}
+
+void promela_free (void * ptr , yyscan_t yyscanner)
+{
+	free( (char *) ptr );	/* see promela_realloc() for (char *) cast */
+}
+
+/* %if-tables-serialization definitions */
+/* %define-yytables   The name for this specific scanner's tables. */
+#define YYTABLES_NAME "yytables"
+/* %endif */
+
+/* %ok-for-header */
+
+#line 81 "promela.l"
diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.tab.cpp b/src/uscxml/plugins/datamodel/promela/parser/promela.tab.cpp
new file mode 100644
index 0000000..5762dd4
--- /dev/null
+++ b/src/uscxml/plugins/datamodel/promela/parser/promela.tab.cpp
@@ -0,0 +1,2176 @@
+/* A Bison parser, made by GNU Bison 2.7.12-4996.  */
+
+/* Bison implementation for Yacc-like parsers in C
+   
+      Copyright (C) 1984, 1989-1990, 2000-2013 Free Software Foundation, Inc.
+   
+   This program is free software: you can redistribute it and/or modify
+   it under the terms of the GNU General Public License as published by
+   the Free Software Foundation, either version 3 of the License, or
+   (at your option) any later version.
+   
+   This program is distributed in the hope that it will be useful,
+   but WITHOUT ANY WARRANTY; without even the implied warranty of
+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+   GNU General Public License for more details.
+   
+   You should have received a copy of the GNU General Public License
+   along with this program.  If not, see <http://www.gnu.org/licenses/>.  */
+
+/* As a special exception, you may create a larger work that contains
+   part or all of the Bison parser skeleton and distribute that work
+   under terms of your choice, so long as that work isn't itself a
+   parser generator using the skeleton or a modified version thereof
+   as a parser skeleton.  Alternatively, if you modify or redistribute
+   the parser skeleton itself, you may (at your option) remove this
+   special exception, which will cause the skeleton and the resulting
+   Bison output files to be licensed under the GNU General Public
+   License without this special exception.
+   
+   This special exception was added by the Free Software Foundation in
+   version 2.2 of Bison.  */
+
+/* C LALR(1) parser skeleton written by Richard Stallman, by
+   simplifying the original so-called "semantic" parser.  */
+
+/* All symbols defined below should begin with yy or YY, to avoid
+   infringing on user name space.  This should be done even for local
+   variables, as they might otherwise be expanded by user macros.
+   There are some unavoidable exceptions within include files to
+   define necessary library symbols; they are noted "INFRINGES ON
+   USER NAME SPACE" below.  */
+
+/* Identify Bison output.  */
+#define YYBISON 1
+
+/* Bison version.  */
+#define YYBISON_VERSION "2.7.12-4996"
+
+/* Skeleton name.  */
+#define YYSKELETON_NAME "yacc.c"
+
+/* Pure parsers.  */
+#define YYPURE 1
+
+/* Push parsers.  */
+#define YYPUSH 0
+
+/* Pull parsers.  */
+#define YYPULL 1
+
+/* Substitute the type names.  */
+#define YYSTYPE         PROMELA_STYPE
+/* Substitute the variable and function names.  */
+#define yyparse         promela_parse
+#define yylex           promela_lex
+#define yyerror         promela_error
+#define yylval          promela_lval
+#define yychar          promela_char
+#define yydebug         promela_debug
+#define yynerrs         promela_nerrs
+
+/* Copy the first part of user declarations.  */
+/* Line 371 of yacc.c  */
+#line 14 "promela.ypp"
+
+#include "../PromelaParser.h"
+#include "promela.tab.hpp"
+#include <sys/types.h>
+#include <stdarg.h>
+
+#define YYMAXDEPTH	20000	// default is 10000
+#define YYDEBUG		1
+#define YYERROR_VERBOSE 1
+
+extern int promela_lex (PROMELA_STYPE* yylval_param, void* yyscanner);
+
+using namespace uscxml;
+
+/* Line 371 of yacc.c  */
+#line 91 "promela.tab.cpp"
+
+# ifndef YY_NULL
+#  if defined __cplusplus && 201103L <= __cplusplus
+#   define YY_NULL nullptr
+#  else
+#   define YY_NULL 0
+#  endif
+# endif
+
+/* Enabling verbose error messages.  */
+#ifdef YYERROR_VERBOSE
+# undef YYERROR_VERBOSE
+# define YYERROR_VERBOSE 1
+#else
+# define YYERROR_VERBOSE 1
+#endif
+
+/* In a future release of Bison, this section will be replaced
+   by #include "promela.tab.hpp".  */
+#ifndef YY_PROMELA_PROMELA_TAB_HPP_INCLUDED
+# define YY_PROMELA_PROMELA_TAB_HPP_INCLUDED
+/* Enabling traces.  */
+#ifndef PROMELA_DEBUG
+# if defined YYDEBUG
+#  if YYDEBUG
+#   define PROMELA_DEBUG 1
+#  else
+#   define PROMELA_DEBUG 0
+#  endif
+# else /* ! defined YYDEBUG */
+#  define PROMELA_DEBUG 0
+# endif /* ! defined YYDEBUG */
+#endif  /* ! defined PROMELA_DEBUG */
+#if PROMELA_DEBUG
+extern int promela_debug;
+#endif
+
+/* Tokens.  */
+#ifndef PROMELA_TOKENTYPE
+# define PROMELA_TOKENTYPE
+   /* Put the tokens into the symbol table, so that GDB and other debuggers
+      know about them.  */
+   enum promela_tokentype {
+     LBRACKET = 258,
+     RBRACKET = 259,
+     LEN = 260,
+     TYPEDEF = 261,
+     MTYPE = 262,
+     INLINE = 263,
+     RETURN = 264,
+     LABEL = 265,
+     OF = 266,
+     GOTO = 267,
+     BREAK = 268,
+     ELSE = 269,
+     SEMI = 270,
+     ARROW = 271,
+     IF = 272,
+     FI = 273,
+     DO = 274,
+     OD = 275,
+     FOR = 276,
+     SELECT = 277,
+     IN = 278,
+     SEP = 279,
+     DOTDOT = 280,
+     HIDDEN = 281,
+     SHOW = 282,
+     ISLOCAL = 283,
+     CONST = 284,
+     TYPE = 285,
+     XU = 286,
+     NAME = 287,
+     UNAME = 288,
+     PNAME = 289,
+     INAME = 290,
+     STRING = 291,
+     CLAIM = 292,
+     TRACE = 293,
+     INIT = 294,
+     LTL = 295,
+     ASGN = 296,
+     AND = 297,
+     OR = 298,
+     BITAND = 299,
+     BITXOR = 300,
+     BITOR = 301,
+     NE = 302,
+     EQ = 303,
+     LE = 304,
+     GE = 305,
+     LT = 306,
+     GT = 307,
+     RSHIFT = 308,
+     LSHIFT = 309,
+     MINUS = 310,
+     PLUS = 311,
+     MODULO = 312,
+     DIVIDE = 313,
+     TIMES = 314,
+     COMPL = 315,
+     NEG = 316,
+     DOT = 317
+   };
+#endif
+
+
+#if ! defined PROMELA_STYPE && ! defined PROMELA_STYPE_IS_DECLARED
+typedef union PROMELA_STYPE
+{
+/* Line 387 of yacc.c  */
+#line 37 "promela.ypp"
+
+  uscxml::PromelaParserNode* node;
+	char* value;
+
+
+/* Line 387 of yacc.c  */
+#line 210 "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
+
+
+#ifdef YYPARSE_PARAM
+#if defined __STDC__ || defined __cplusplus
+int promela_parse (void *YYPARSE_PARAM);
+#else
+int promela_parse ();
+#endif
+#else /* ! YYPARSE_PARAM */
+#if defined __STDC__ || defined __cplusplus
+int promela_parse (uscxml::PromelaParser* ctx, void * scanner);
+#else
+int promela_parse ();
+#endif
+#endif /* ! YYPARSE_PARAM */
+
+#endif /* !YY_PROMELA_PROMELA_TAB_HPP_INCLUDED  */
+
+/* Copy the second part of user declarations.  */
+
+/* Line 390 of yacc.c  */
+#line 237 "promela.tab.cpp"
+
+#ifdef short
+# undef short
+#endif
+
+#ifdef YYTYPE_UINT8
+typedef YYTYPE_UINT8 yytype_uint8;
+#else
+typedef unsigned char yytype_uint8;
+#endif
+
+#ifdef YYTYPE_INT8
+typedef YYTYPE_INT8 yytype_int8;
+#elif (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+typedef signed char yytype_int8;
+#else
+typedef short int yytype_int8;
+#endif
+
+#ifdef YYTYPE_UINT16
+typedef YYTYPE_UINT16 yytype_uint16;
+#else
+typedef unsigned short int yytype_uint16;
+#endif
+
+#ifdef YYTYPE_INT16
+typedef YYTYPE_INT16 yytype_int16;
+#else
+typedef short int yytype_int16;
+#endif
+
+#ifndef YYSIZE_T
+# ifdef __SIZE_TYPE__
+#  define YYSIZE_T __SIZE_TYPE__
+# elif defined size_t
+#  define YYSIZE_T size_t
+# elif ! defined YYSIZE_T && (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+#  include <stddef.h> /* INFRINGES ON USER NAME SPACE */
+#  define YYSIZE_T size_t
+# else
+#  define YYSIZE_T unsigned int
+# endif
+#endif
+
+#define YYSIZE_MAXIMUM ((YYSIZE_T) -1)
+
+#ifndef YY_
+# if defined YYENABLE_NLS && YYENABLE_NLS
+#  if ENABLE_NLS
+#   include <libintl.h> /* INFRINGES ON USER NAME SPACE */
+#   define YY_(Msgid) dgettext ("bison-runtime", Msgid)
+#  endif
+# endif
+# ifndef YY_
+#  define YY_(Msgid) Msgid
+# endif
+#endif
+
+#ifndef __attribute__
+/* This feature is available in gcc versions 2.5 and later.  */
+# if (! defined __GNUC__ || __GNUC__ < 2 \
+      || (__GNUC__ == 2 && __GNUC_MINOR__ < 5))
+#  define __attribute__(Spec) /* empty */
+# endif
+#endif
+
+/* Suppress unused-variable warnings by "using" E.  */
+#if ! defined lint || defined __GNUC__
+# define YYUSE(E) ((void) (E))
+#else
+# define YYUSE(E) /* empty */
+#endif
+
+
+/* Identity function, used to suppress warnings about constant conditions.  */
+#ifndef lint
+# define YYID(N) (N)
+#else
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+static int
+YYID (int yyi)
+#else
+static int
+YYID (yyi)
+    int yyi;
+#endif
+{
+  return yyi;
+}
+#endif
+
+#if ! defined yyoverflow || YYERROR_VERBOSE
+
+/* The parser invokes alloca or malloc; define the necessary symbols.  */
+
+# ifdef YYSTACK_USE_ALLOCA
+#  if YYSTACK_USE_ALLOCA
+#   ifdef __GNUC__
+#    define YYSTACK_ALLOC __builtin_alloca
+#   elif defined __BUILTIN_VA_ARG_INCR
+#    include <alloca.h> /* INFRINGES ON USER NAME SPACE */
+#   elif defined _AIX
+#    define YYSTACK_ALLOC __alloca
+#   elif defined _MSC_VER
+#    include <malloc.h> /* INFRINGES ON USER NAME SPACE */
+#    define alloca _alloca
+#   else
+#    define YYSTACK_ALLOC alloca
+#    if ! defined _ALLOCA_H && ! defined EXIT_SUCCESS && (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+#     include <stdlib.h> /* INFRINGES ON USER NAME SPACE */
+      /* Use EXIT_SUCCESS as a witness for stdlib.h.  */
+#     ifndef EXIT_SUCCESS
+#      define EXIT_SUCCESS 0
+#     endif
+#    endif
+#   endif
+#  endif
+# endif
+
+# ifdef YYSTACK_ALLOC
+   /* Pacify GCC's `empty if-body' warning.  */
+#  define YYSTACK_FREE(Ptr) do { /* empty */; } while (YYID (0))
+#  ifndef YYSTACK_ALLOC_MAXIMUM
+    /* The OS might guarantee only one guard page at the bottom of the stack,
+       and a page size can be as small as 4096 bytes.  So we cannot safely
+       invoke alloca (N) if N exceeds 4096.  Use a slightly smaller number
+       to allow for a few compiler-allocated temporary stack slots.  */
+#   define YYSTACK_ALLOC_MAXIMUM 4032 /* reasonable circa 2006 */
+#  endif
+# else
+#  define YYSTACK_ALLOC YYMALLOC
+#  define YYSTACK_FREE YYFREE
+#  ifndef YYSTACK_ALLOC_MAXIMUM
+#   define YYSTACK_ALLOC_MAXIMUM YYSIZE_MAXIMUM
+#  endif
+#  if (defined __cplusplus && ! defined EXIT_SUCCESS \
+       && ! ((defined YYMALLOC || defined malloc) \
+	     && (defined YYFREE || defined free)))
+#   include <stdlib.h> /* INFRINGES ON USER NAME SPACE */
+#   ifndef EXIT_SUCCESS
+#    define EXIT_SUCCESS 0
+#   endif
+#  endif
+#  ifndef YYMALLOC
+#   define YYMALLOC malloc
+#   if ! defined malloc && ! defined EXIT_SUCCESS && (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+void *malloc (YYSIZE_T); /* INFRINGES ON USER NAME SPACE */
+#   endif
+#  endif
+#  ifndef YYFREE
+#   define YYFREE free
+#   if ! defined free && ! defined EXIT_SUCCESS && (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+void free (void *); /* INFRINGES ON USER NAME SPACE */
+#   endif
+#  endif
+# endif
+#endif /* ! defined yyoverflow || YYERROR_VERBOSE */
+
+
+#if (! defined yyoverflow \
+     && (! defined __cplusplus \
+	 || (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;
+};
+
+/* The size of the maximum gap between one aligned stack and the next.  */
+# define YYSTACK_GAP_MAXIMUM (sizeof (union yyalloc) - 1)
+
+/* 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)
+
+# define YYCOPY_NEEDED 1
+
+/* Relocate STACK from its old location to the new one.  The
+   local variables YYSIZE and YYSTACKSIZE give the old and new number of
+   elements in the stack, and YYPTR gives the new location of the
+   stack.  Advance YYPTR to a properly aligned location for the next
+   stack.  */
+# define YYSTACK_RELOCATE(Stack_alloc, Stack)				\
+    do									\
+      {									\
+	YYSIZE_T yynewbytes;						\
+	YYCOPY (&yyptr->Stack_alloc, Stack, yysize);			\
+	Stack = &yyptr->Stack_alloc;					\
+	yynewbytes = yystacksize * sizeof (*Stack) + YYSTACK_GAP_MAXIMUM; \
+	yyptr += yynewbytes / sizeof (*yyptr);				\
+      }									\
+    while (YYID (0))
+
+#endif
+
+#if defined YYCOPY_NEEDED && YYCOPY_NEEDED
+/* Copy COUNT objects from SRC to DST.  The source and destination do
+   not overlap.  */
+# ifndef YYCOPY
+#  if defined __GNUC__ && 1 < __GNUC__
+#   define YYCOPY(Dst, Src, Count) \
+      __builtin_memcpy (Dst, Src, (Count) * sizeof (*(Src)))
+#  else
+#   define YYCOPY(Dst, Src, Count)              \
+      do                                        \
+        {                                       \
+          YYSIZE_T yyi;                         \
+          for (yyi = 0; yyi < (Count); yyi++)   \
+            (Dst)[yyi] = (Src)[yyi];            \
+        }                                       \
+      while (YYID (0))
+#  endif
+# endif
+#endif /* !YYCOPY_NEEDED */
+
+/* YYFINAL -- State number of the termination state.  */
+#define YYFINAL  23
+/* YYLAST -- Last index in YYTABLE.  */
+#define YYLAST   205
+
+/* YYNTOKENS -- Number of terminals.  */
+#define YYNTOKENS  77
+/* YYNNTS -- Number of nonterminals.  */
+#define YYNNTS  16
+/* YYNRULES -- Number of rules.  */
+#define YYNRULES  61
+/* YYNRULES -- Number of states.  */
+#define YYNSTATES  110
+
+/* YYTRANSLATE(YYLEX) -- Bison symbol number corresponding to YYLEX.  */
+#define YYUNDEFTOK  2
+#define YYMAXUTOK   317
+
+#define YYTRANSLATE(YYX)						\
+  ((unsigned int) (YYX) <= YYMAXUTOK ? yytranslate[YYX] : YYUNDEFTOK)
+
+/* YYTRANSLATE[YYLEX] -- Bison symbol number corresponding to YYLEX.  */
+static const yytype_uint8 yytranslate[] =
+{
+       0,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,    76,     2,     2,
+      66,    67,    74,    73,    70,    72,    65,    75,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,    71,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,    63,     2,    64,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,    68,     2,    69,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     1,     2,     3,     4,
+       5,     6,     7,     8,     9,    10,    11,    12,    13,    14,
+      15,    16,    17,    18,    19,    20,    21,    22,    23,    24,
+      25,    26,    27,    28,    29,    30,    31,    32,    33,    34,
+      35,    36,    37,    38,    39,    40,    41,    42,    43,    44,
+      45,    46,    47,    48,    49,    50,    51,    52,    53,    54,
+      55,    56,    57,    58,    59,    60,    61,    62
+};
+
+#if PROMELA_DEBUG
+/* YYPRHS[YYN] -- Index of the first RHS symbol of rule number YYN in
+   YYRHS.  */
+static const yytype_uint8 yyprhs[] =
+{
+       0,     0,     3,     5,     7,     9,    11,    16,    17,    21,
+      22,    25,    29,    33,    37,    41,    45,    49,    53,    57,
+      61,    65,    69,    73,    77,    81,    85,    89,    93,    97,
+     101,   104,   107,   112,   114,   116,   117,   119,   121,   123,
+     127,   131,   138,   140,   144,   146,   150,   152,   156,   158,
+     162,   167,   169,   172,   176,   180,   184,   188,   192,   196,
+     198,   201
+};
+
+/* YYRHS -- A `-1'-separated list of the rules' RHS.  */
+static const yytype_int8 yyrhs[] =
+{
+      78,     0,    -1,    87,    -1,    84,    -1,    81,    -1,    32,
+      -1,    32,    63,    84,    64,    -1,    -1,    80,    82,    83,
+      -1,    -1,    65,    81,    -1,     3,    84,     4,    -1,    84,
+      56,    84,    -1,    84,    55,    84,    -1,    84,    59,    84,
+      -1,    84,    58,    84,    -1,    84,    57,    84,    -1,    84,
+      44,    84,    -1,    84,    45,    84,    -1,    84,    46,    84,
+      -1,    84,    52,    84,    -1,    84,    51,    84,    -1,    84,
+      50,    84,    -1,    84,    49,    84,    -1,    84,    48,    84,
+      -1,    84,    47,    84,    -1,    84,    42,    84,    -1,    84,
+      43,    84,    -1,    84,    54,    84,    -1,    84,    53,    84,
+      -1,    61,    84,    -1,    55,    84,    -1,     5,    66,    79,
+      67,    -1,    79,    -1,    29,    -1,    -1,    26,    -1,    27,
+      -1,    28,    -1,    85,    30,    88,    -1,    85,    33,    88,
+      -1,    85,    30,    41,    68,    92,    69,    -1,    86,    -1,
+      86,    15,    87,    -1,    89,    -1,    89,    70,    88,    -1,
+      90,    -1,    90,    41,    84,    -1,    32,    -1,    32,    71,
+      29,    -1,    32,    63,    91,    64,    -1,    29,    -1,    72,
+      91,    -1,    66,    91,    67,    -1,    91,    73,    91,    -1,
+      91,    72,    91,    -1,    91,    74,    91,    -1,    91,    75,
+      91,    -1,    91,    76,    91,    -1,    32,    -1,    92,    32,
+      -1,    92,    70,    -1
+};
+
+/* YYRLINE[YYN] -- source line where rule number YYN was defined.  */
+static const yytype_uint8 yyrline[] =
+{
+       0,    75,    75,    79,    84,    87,    88,    91,    91,    95,
+      96,    99,   100,   101,   102,   103,   104,   105,   106,   107,
+     108,   109,   110,   111,   112,   113,   114,   115,   116,   117,
+     118,   119,   121,   122,   123,   127,   128,   129,   130,   133,
+     134,   135,   138,   139,   143,   144,   147,   148,   151,   152,
+     153,   156,   157,   158,   159,   160,   161,   162,   163,   166,
+     167,   168
+};
+#endif
+
+#if PROMELA_DEBUG || YYERROR_VERBOSE || 1
+/* YYTNAME[SYMBOL-NUM] -- String name of the symbol SYMBOL-NUM.
+   First, the terminals, then, starting at YYNTOKENS, nonterminals.  */
+static const char *const yytname[] =
+{
+  "$end", "error", "$undefined", "LBRACKET", "RBRACKET", "LEN", "TYPEDEF",
+  "MTYPE", "INLINE", "RETURN", "LABEL", "OF", "GOTO", "BREAK", "ELSE",
+  "SEMI", "ARROW", "IF", "FI", "DO", "OD", "FOR", "SELECT", "IN", "SEP",
+  "DOTDOT", "HIDDEN", "SHOW", "ISLOCAL", "CONST", "TYPE", "XU", "NAME",
+  "UNAME", "PNAME", "INAME", "STRING", "CLAIM", "TRACE", "INIT", "LTL",
+  "ASGN", "AND", "OR", "BITAND", "BITXOR", "BITOR", "NE", "EQ", "LE", "GE",
+  "LT", "GT", "RSHIFT", "LSHIFT", "MINUS", "PLUS", "MODULO", "DIVIDE",
+  "TIMES", "COMPL", "NEG", "DOT", "'['", "']'", "'.'", "'('", "')'", "'{'",
+  "'}'", "','", "':'", "'-'", "'+'", "'*'", "'/'", "'%'", "$accept",
+  "program", "varref", "pfld", "cmpnd", "$@1", "sfld", "expr", "vis",
+  "one_decl", "decl_lst", "var_list", "ivar", "vardcl", "const_expr",
+  "nlst", YY_NULL
+};
+#endif
+
+# ifdef YYPRINT
+/* YYTOKNUM[YYLEX-NUM] -- Internal token number corresponding to
+   token YYLEX-NUM.  */
+static const yytype_uint16 yytoknum[] =
+{
+       0,   256,   257,   258,   259,   260,   261,   262,   263,   264,
+     265,   266,   267,   268,   269,   270,   271,   272,   273,   274,
+     275,   276,   277,   278,   279,   280,   281,   282,   283,   284,
+     285,   286,   287,   288,   289,   290,   291,   292,   293,   294,
+     295,   296,   297,   298,   299,   300,   301,   302,   303,   304,
+     305,   306,   307,   308,   309,   310,   311,   312,   313,   314,
+     315,   316,   317,    91,    93,    46,    40,    41,   123,   125,
+      44,    58,    45,    43,    42,    47,    37
+};
+# endif
+
+/* YYR1[YYN] -- Symbol number of symbol that rule YYN derives.  */
+static const yytype_uint8 yyr1[] =
+{
+       0,    77,    78,    78,    79,    80,    80,    82,    81,    83,
+      83,    84,    84,    84,    84,    84,    84,    84,    84,    84,
+      84,    84,    84,    84,    84,    84,    84,    84,    84,    84,
+      84,    84,    84,    84,    84,    85,    85,    85,    85,    86,
+      86,    86,    87,    87,    88,    88,    89,    89,    90,    90,
+      90,    91,    91,    91,    91,    91,    91,    91,    91,    92,
+      92,    92
+};
+
+/* YYR2[YYN] -- Number of symbols composing right hand side of rule YYN.  */
+static const yytype_uint8 yyr2[] =
+{
+       0,     2,     1,     1,     1,     1,     4,     0,     3,     0,
+       2,     3,     3,     3,     3,     3,     3,     3,     3,     3,
+       3,     3,     3,     3,     3,     3,     3,     3,     3,     3,
+       2,     2,     4,     1,     1,     0,     1,     1,     1,     3,
+       3,     6,     1,     3,     1,     3,     1,     3,     1,     3,
+       4,     1,     2,     3,     3,     3,     3,     3,     3,     1,
+       2,     2
+};
+
+/* YYDEFACT[STATE-NAME] -- Default reduction number in state STATE-NUM.
+   Performed when YYTABLE doesn't specify something else to do.  Zero
+   means the default is an error.  */
+static const yytype_uint8 yydefact[] =
+{
+      35,     0,     0,    36,    37,    38,    34,     5,     0,     0,
+       0,    33,     7,     4,     3,     0,    42,     2,     0,     0,
+       0,    31,    30,     1,     9,     0,     0,     0,     0,     0,
+       0,     0,     0,     0,     0,     0,     0,     0,     0,     0,
+       0,     0,     0,     0,     0,    35,    11,     0,     0,     0,
+       8,    26,    27,    17,    18,    19,    25,    24,    23,    22,
+      21,    20,    29,    28,    13,    12,    16,    15,    14,    48,
+       0,    39,    44,    46,    40,    43,    32,     6,    10,     0,
+       0,     0,     0,     0,    51,     0,     0,     0,    49,    59,
+       0,    45,    47,     0,    52,    50,     0,     0,     0,     0,
+       0,    60,    41,    61,    53,    55,    54,    56,    57,    58
+};
+
+/* YYDEFGOTO[NTERM-NUM].  */
+static const yytype_int8 yydefgoto[] =
+{
+      -1,    10,    11,    12,    13,    24,    50,    14,    15,    16,
+      17,    71,    72,    73,    87,    90
+};
+
+/* YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
+   STATE-NUM.  */
+#define YYPACT_NINF -83
+static const yytype_int16 yypact[] =
+{
+      17,    18,   -64,   -83,   -83,   -83,   -83,   -57,    18,    18,
+      11,   -83,   -83,   -83,    67,   -21,    56,   -83,     9,    45,
+      18,    44,   -83,   -83,    15,    18,    18,    18,    18,    18,
+      18,    18,    18,    18,    18,    18,    18,    18,    18,    18,
+      18,    18,    18,   -31,    49,    48,   -83,   114,    41,    45,
+     -83,    83,    83,    96,    96,    96,   120,   120,   104,   104,
+     104,   104,   136,   136,    44,    44,   -83,   -83,   -83,   119,
+      36,   -83,   131,   142,   -83,   -83,   -83,   -83,   -83,   -24,
+     155,   170,    49,    18,   -83,   -24,   -24,    92,   -83,   -83,
+      37,   -83,    67,   113,   124,   -83,   -24,   -24,   -24,   -24,
+     -24,   -83,   -83,   -83,   -83,   124,   124,   124,   124,   124
+};
+
+/* YYPGOTO[NTERM-NUM].  */
+static const yytype_int16 yypgoto[] =
+{
+     -83,   -83,   184,   -83,   156,   -83,   -83,    -1,   -83,   -83,
+     159,    26,   -83,   -83,   -82,   -83
+};
+
+/* YYTABLE[YYPACT[STATE-NUM]].  What to do in state STATE-NUM.  If
+   positive, shift that token.  If negative, reduce the rule which
+   number is the opposite.  If YYTABLE_NINF, syntax error.  */
+#define YYTABLE_NINF -1
+static const yytype_uint8 yytable[] =
+{
+      18,    69,    19,    93,    94,    84,    20,    21,    22,    43,
+      70,    23,    44,    46,   105,   106,   107,   108,   109,    48,
+       1,     1,     2,     2,    51,    52,    53,    54,    55,    56,
+      57,    58,    59,    60,    61,    62,    63,    64,    65,    66,
+      67,    68,    85,     3,     4,     5,     6,     6,    86,     7,
+       7,    25,    26,    27,    28,    29,    30,    31,    32,    33,
+      34,    35,    36,    37,    38,    39,    40,    41,    42,   101,
+      74,    45,     8,     8,     3,     4,     5,     7,     9,     9,
+      49,    69,    92,    25,    26,    27,    28,    29,    30,    31,
+      32,    33,    34,    35,    36,    37,    38,    39,    40,    41,
+      42,    40,    41,    42,    81,    77,   102,   103,    91,    25,
+      26,    27,    28,    29,    30,    31,    32,    33,    34,    35,
+      36,    37,    38,    39,    40,    41,    42,    27,    28,    29,
+      30,    31,    32,    33,    34,    35,    36,    37,    38,    39,
+      40,    41,    42,    30,    31,    32,    33,    34,    35,    36,
+      37,    38,    39,    40,    41,    42,    95,    36,    37,    38,
+      39,    40,    41,    42,    96,    97,    98,    99,   100,    32,
+      33,    34,    35,    36,    37,    38,    39,    40,    41,    42,
+     104,    76,    79,    83,    88,    96,    97,    98,    99,   100,
+      80,    38,    39,    40,    41,    42,    96,    97,    98,    99,
+     100,    82,    89,    47,    75,    78
+};
+
+#define yypact_value_is_default(Yystate) \
+  (!!((Yystate) == (-83)))
+
+#define yytable_value_is_error(Yytable_value) \
+  YYID (0)
+
+static const yytype_uint8 yycheck[] =
+{
+       1,    32,    66,    85,    86,    29,    63,     8,     9,    30,
+      41,     0,    33,     4,    96,    97,    98,    99,   100,    20,
+       3,     3,     5,     5,    25,    26,    27,    28,    29,    30,
+      31,    32,    33,    34,    35,    36,    37,    38,    39,    40,
+      41,    42,    66,    26,    27,    28,    29,    29,    72,    32,
+      32,    42,    43,    44,    45,    46,    47,    48,    49,    50,
+      51,    52,    53,    54,    55,    56,    57,    58,    59,    32,
+      44,    15,    55,    55,    26,    27,    28,    32,    61,    61,
+      65,    32,    83,    42,    43,    44,    45,    46,    47,    48,
+      49,    50,    51,    52,    53,    54,    55,    56,    57,    58,
+      59,    57,    58,    59,    68,    64,    69,    70,    82,    42,
+      43,    44,    45,    46,    47,    48,    49,    50,    51,    52,
+      53,    54,    55,    56,    57,    58,    59,    44,    45,    46,
+      47,    48,    49,    50,    51,    52,    53,    54,    55,    56,
+      57,    58,    59,    47,    48,    49,    50,    51,    52,    53,
+      54,    55,    56,    57,    58,    59,    64,    53,    54,    55,
+      56,    57,    58,    59,    72,    73,    74,    75,    76,    49,
+      50,    51,    52,    53,    54,    55,    56,    57,    58,    59,
+      67,    67,    63,    41,    29,    72,    73,    74,    75,    76,
+      71,    55,    56,    57,    58,    59,    72,    73,    74,    75,
+      76,    70,    32,    19,    45,    49
+};
+
+/* YYSTOS[STATE-NUM] -- The (internal number of the) accessing
+   symbol of state STATE-NUM.  */
+static const yytype_uint8 yystos[] =
+{
+       0,     3,     5,    26,    27,    28,    29,    32,    55,    61,
+      78,    79,    80,    81,    84,    85,    86,    87,    84,    66,
+      63,    84,    84,     0,    82,    42,    43,    44,    45,    46,
+      47,    48,    49,    50,    51,    52,    53,    54,    55,    56,
+      57,    58,    59,    30,    33,    15,     4,    79,    84,    65,
+      83,    84,    84,    84,    84,    84,    84,    84,    84,    84,
+      84,    84,    84,    84,    84,    84,    84,    84,    84,    32,
+      41,    88,    89,    90,    88,    87,    67,    64,    81,    63,
+      71,    68,    70,    41,    29,    66,    72,    91,    29,    32,
+      92,    88,    84,    91,    91,    64,    72,    73,    74,    75,
+      76,    32,    69,    70,    67,    91,    91,    91,    91,    91
+};
+
+#define yyerrok		(yyerrstatus = 0)
+#define yyclearin	(yychar = YYEMPTY)
+#define YYEMPTY		(-2)
+#define YYEOF		0
+
+#define YYACCEPT	goto yyacceptlab
+#define YYABORT		goto yyabortlab
+#define YYERROR		goto yyerrorlab
+
+
+/* Like YYERROR except do call yyerror.  This remains here temporarily
+   to ease the transition to the new meaning of YYERROR, for GCC.
+   Once GCC version 2 has supplanted version 1, this can go.  However,
+   YYFAIL appears to be in use.  Nevertheless, it is formally deprecated
+   in Bison 2.4.2's NEWS entry, where a plan to phase it out is
+   discussed.  */
+
+#define YYFAIL		goto yyerrlab
+#if defined YYFAIL
+  /* This is here to suppress warnings from the GCC cpp's
+     -Wunused-macros.  Normally we don't worry about that warning, but
+     some users do, and we want to make it easy for users to remove
+     YYFAIL uses, which will produce warnings from Bison 2.5.  */
+#endif
+
+#define YYRECOVERING()  (!!yyerrstatus)
+
+#define YYBACKUP(Token, Value)                                  \
+do                                                              \
+  if (yychar == YYEMPTY)                                        \
+    {                                                           \
+      yychar = (Token);                                         \
+      yylval = (Value);                                         \
+      YYPOPSTACK (yylen);                                       \
+      yystate = *yyssp;                                         \
+      goto yybackup;                                            \
+    }                                                           \
+  else                                                          \
+    {                                                           \
+      yyerror (ctx, scanner, YY_("syntax error: cannot back up")); \
+      YYERROR;							\
+    }								\
+while (YYID (0))
+
+/* Error token number */
+#define YYTERROR	1
+#define YYERRCODE	256
+
+
+/* This macro is provided for backward compatibility. */
+#ifndef YY_LOCATION_PRINT
+# define YY_LOCATION_PRINT(File, Loc) ((void) 0)
+#endif
+
+
+/* YYLEX -- calling `yylex' with the right arguments.  */
+#ifdef YYLEX_PARAM
+# define YYLEX yylex (&yylval, YYLEX_PARAM)
+#else
+# define YYLEX yylex (&yylval, scanner)
+#endif
+
+/* Enable debugging if requested.  */
+#if PROMELA_DEBUG
+
+# ifndef YYFPRINTF
+#  include <stdio.h> /* INFRINGES ON USER NAME SPACE */
+#  define YYFPRINTF fprintf
+# endif
+
+# define YYDPRINTF(Args)			\
+do {						\
+  if (yydebug)					\
+    YYFPRINTF Args;				\
+} while (YYID (0))
+
+# define YY_SYMBOL_PRINT(Title, Type, Value, Location)			  \
+do {									  \
+  if (yydebug)								  \
+    {									  \
+      YYFPRINTF (stderr, "%s ", Title);					  \
+      yy_symbol_print (stderr,						  \
+		  Type, Value, ctx, scanner); \
+      YYFPRINTF (stderr, "\n");						  \
+    }									  \
+} while (YYID (0))
+
+
+/*--------------------------------.
+| Print this symbol on YYOUTPUT.  |
+`--------------------------------*/
+
+/*ARGSUSED*/
+#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)
+#else
+static void
+yy_symbol_value_print (yyoutput, yytype, yyvaluep, ctx, scanner)
+    FILE *yyoutput;
+    int yytype;
+    YYSTYPE const * const yyvaluep;
+    uscxml::PromelaParser* ctx;
+    void * scanner;
+#endif
+{
+  FILE *yyo = yyoutput;
+  YYUSE (yyo);
+  if (!yyvaluep)
+    return;
+  YYUSE (ctx);
+  YYUSE (scanner);
+# ifdef YYPRINT
+  if (yytype < YYNTOKENS)
+    YYPRINT (yyoutput, yytoknum[yytype], *yyvaluep);
+# else
+  YYUSE (yyoutput);
+# endif
+  YYUSE (yytype);
+}
+
+
+/*--------------------------------.
+| Print this symbol on YYOUTPUT.  |
+`--------------------------------*/
+
+#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)
+#else
+static void
+yy_symbol_print (yyoutput, yytype, yyvaluep, ctx, scanner)
+    FILE *yyoutput;
+    int yytype;
+    YYSTYPE const * const yyvaluep;
+    uscxml::PromelaParser* ctx;
+    void * scanner;
+#endif
+{
+  if (yytype < YYNTOKENS)
+    YYFPRINTF (yyoutput, "token %s (", yytname[yytype]);
+  else
+    YYFPRINTF (yyoutput, "nterm %s (", yytname[yytype]);
+
+  yy_symbol_value_print (yyoutput, yytype, yyvaluep, ctx, scanner);
+  YYFPRINTF (yyoutput, ")");
+}
+
+/*------------------------------------------------------------------.
+| yy_stack_print -- Print the state stack from its BOTTOM up to its |
+| TOP (included).                                                   |
+`------------------------------------------------------------------*/
+
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+static void
+yy_stack_print (yytype_int16 *yybottom, yytype_int16 *yytop)
+#else
+static void
+yy_stack_print (yybottom, yytop)
+    yytype_int16 *yybottom;
+    yytype_int16 *yytop;
+#endif
+{
+  YYFPRINTF (stderr, "Stack now");
+  for (; yybottom <= yytop; yybottom++)
+    {
+      int yybot = *yybottom;
+      YYFPRINTF (stderr, " %d", yybot);
+    }
+  YYFPRINTF (stderr, "\n");
+}
+
+# define YY_STACK_PRINT(Bottom, Top)				\
+do {								\
+  if (yydebug)							\
+    yy_stack_print ((Bottom), (Top));				\
+} while (YYID (0))
+
+
+/*------------------------------------------------.
+| Report that the YYRULE is going to be reduced.  |
+`------------------------------------------------*/
+
+#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)
+#else
+static void
+yy_reduce_print (yyvsp, yyrule, ctx, scanner)
+    YYSTYPE *yyvsp;
+    int yyrule;
+    uscxml::PromelaParser* ctx;
+    void * scanner;
+#endif
+{
+  int yynrhs = yyr2[yyrule];
+  int yyi;
+  unsigned long int yylno = yyrline[yyrule];
+  YYFPRINTF (stderr, "Reducing stack by rule %d (line %lu):\n",
+	     yyrule - 1, yylno);
+  /* The symbols being reduced.  */
+  for (yyi = 0; yyi < yynrhs; yyi++)
+    {
+      YYFPRINTF (stderr, "   $%d = ", yyi + 1);
+      yy_symbol_print (stderr, yyrhs[yyprhs[yyrule] + yyi],
+		       &(yyvsp[(yyi + 1) - (yynrhs)])
+		       		       , ctx, scanner);
+      YYFPRINTF (stderr, "\n");
+    }
+}
+
+# define YY_REDUCE_PRINT(Rule)		\
+do {					\
+  if (yydebug)				\
+    yy_reduce_print (yyvsp, Rule, ctx, scanner); \
+} while (YYID (0))
+
+/* Nonzero means print parse trace.  It is left uninitialized so that
+   multiple parsers can coexist.  */
+int yydebug;
+#else /* !PROMELA_DEBUG */
+# define YYDPRINTF(Args)
+# define YY_SYMBOL_PRINT(Title, Type, Value, Location)
+# define YY_STACK_PRINT(Bottom, Top)
+# define YY_REDUCE_PRINT(Rule)
+#endif /* !PROMELA_DEBUG */
+
+
+/* YYINITDEPTH -- initial size of the parser's stacks.  */
+#ifndef	YYINITDEPTH
+# define YYINITDEPTH 200
+#endif
+
+/* YYMAXDEPTH -- maximum size the stacks can grow to (effective only
+   if the built-in stack extension method is used).
+
+   Do not make this value too large; the results are undefined if
+   YYSTACK_ALLOC_MAXIMUM < YYSTACK_BYTES (YYMAXDEPTH)
+   evaluated with infinite-precision integer arithmetic.  */
+
+#ifndef YYMAXDEPTH
+# define YYMAXDEPTH 10000
+#endif
+
+
+#if YYERROR_VERBOSE
+
+# ifndef yystrlen
+#  if defined __GLIBC__ && defined _STRING_H
+#   define yystrlen strlen
+#  else
+/* Return the length of YYSTR.  */
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+static YYSIZE_T
+yystrlen (const char *yystr)
+#else
+static YYSIZE_T
+yystrlen (yystr)
+    const char *yystr;
+#endif
+{
+  YYSIZE_T yylen;
+  for (yylen = 0; yystr[yylen]; yylen++)
+    continue;
+  return yylen;
+}
+#  endif
+# endif
+
+# ifndef yystpcpy
+#  if defined __GLIBC__ && defined _STRING_H && defined _GNU_SOURCE
+#   define yystpcpy stpcpy
+#  else
+/* Copy YYSRC to YYDEST, returning the address of the terminating '\0' in
+   YYDEST.  */
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+static char *
+yystpcpy (char *yydest, const char *yysrc)
+#else
+static char *
+yystpcpy (yydest, yysrc)
+    char *yydest;
+    const char *yysrc;
+#endif
+{
+  char *yyd = yydest;
+  const char *yys = yysrc;
+
+  while ((*yyd++ = *yys++) != '\0')
+    continue;
+
+  return yyd - 1;
+}
+#  endif
+# endif
+
+# ifndef yytnamerr
+/* Copy to YYRES the contents of YYSTR after stripping away unnecessary
+   quotes and backslashes, so that it's suitable for yyerror.  The
+   heuristic is that double-quoting is unnecessary unless the string
+   contains an apostrophe, a comma, or backslash (other than
+   backslash-backslash).  YYSTR is taken from yytname.  If YYRES is
+   null, do not copy; instead, return the length of what the result
+   would have been.  */
+static YYSIZE_T
+yytnamerr (char *yyres, const char *yystr)
+{
+  if (*yystr == '"')
+    {
+      YYSIZE_T yyn = 0;
+      char const *yyp = yystr;
+
+      for (;;)
+	switch (*++yyp)
+	  {
+	  case '\'':
+	  case ',':
+	    goto do_not_strip_quotes;
+
+	  case '\\':
+	    if (*++yyp != '\\')
+	      goto do_not_strip_quotes;
+	    /* Fall through.  */
+	  default:
+	    if (yyres)
+	      yyres[yyn] = *yyp;
+	    yyn++;
+	    break;
+
+	  case '"':
+	    if (yyres)
+	      yyres[yyn] = '\0';
+	    return yyn;
+	  }
+    do_not_strip_quotes: ;
+    }
+
+  if (! yyres)
+    return yystrlen (yystr);
+
+  return yystpcpy (yyres, yystr) - yyres;
+}
+# endif
+
+/* Copy into *YYMSG, which is of size *YYMSG_ALLOC, an error message
+   about the unexpected token YYTOKEN for the state stack whose top is
+   YYSSP.
+
+   Return 0 if *YYMSG was successfully written.  Return 1 if *YYMSG is
+   not large enough to hold the message.  In that case, also set
+   *YYMSG_ALLOC to the required number of bytes.  Return 2 if the
+   required number of bytes is too large to store.  */
+static int
+yysyntax_error (YYSIZE_T *yymsg_alloc, char **yymsg,
+                yytype_int16 *yyssp, int yytoken)
+{
+  YYSIZE_T yysize0 = yytnamerr (YY_NULL, yytname[yytoken]);
+  YYSIZE_T yysize = yysize0;
+  enum { YYERROR_VERBOSE_ARGS_MAXIMUM = 5 };
+  /* Internationalized format string. */
+  const char *yyformat = YY_NULL;
+  /* Arguments of yyformat. */
+  char const *yyarg[YYERROR_VERBOSE_ARGS_MAXIMUM];
+  /* Number of reported tokens (one for the "unexpected", one per
+     "expected"). */
+  int yycount = 0;
+
+  /* There are many possibilities here to consider:
+     - Assume YYFAIL is not used.  It's too flawed to consider.  See
+       <http://lists.gnu.org/archive/html/bison-patches/2009-12/msg00024.html>
+       for details.  YYERROR is fine as it does not invoke this
+       function.
+     - If this state is a consistent state with a default action, then
+       the only way this function was invoked is if the default action
+       is an error action.  In that case, don't check for expected
+       tokens because there are none.
+     - The only way there can be no lookahead present (in yychar) is if
+       this state is a consistent state with a default action.  Thus,
+       detecting the absence of a lookahead is sufficient to determine
+       that there is no unexpected or expected token to report.  In that
+       case, just report a simple "syntax error".
+     - Don't assume there isn't a lookahead just because this state is a
+       consistent state with a default action.  There might have been a
+       previous inconsistent state, consistent state with a non-default
+       action, or user semantic action that manipulated yychar.
+     - Of course, the expected token list depends on states to have
+       correct lookahead information, and it depends on the parser not
+       to perform extra reductions after fetching a lookahead from the
+       scanner and before detecting a syntax error.  Thus, state merging
+       (from LALR or IELR) and default reductions corrupt the expected
+       token list.  However, the list is correct for canonical LR with
+       one exception: it will still contain any token that will not be
+       accepted due to an error action in a later state.
+  */
+  if (yytoken != YYEMPTY)
+    {
+      int yyn = yypact[*yyssp];
+      yyarg[yycount++] = yytname[yytoken];
+      if (!yypact_value_is_default (yyn))
+        {
+          /* Start YYX at -YYN if negative to avoid negative indexes in
+             YYCHECK.  In other words, skip the first -YYN actions for
+             this state because they are default actions.  */
+          int yyxbegin = yyn < 0 ? -yyn : 0;
+          /* Stay within bounds of both yycheck and yytname.  */
+          int yychecklim = YYLAST - yyn + 1;
+          int yyxend = yychecklim < YYNTOKENS ? yychecklim : YYNTOKENS;
+          int yyx;
+
+          for (yyx = yyxbegin; yyx < yyxend; ++yyx)
+            if (yycheck[yyx + yyn] == yyx && yyx != YYTERROR
+                && !yytable_value_is_error (yytable[yyx + yyn]))
+              {
+                if (yycount == YYERROR_VERBOSE_ARGS_MAXIMUM)
+                  {
+                    yycount = 1;
+                    yysize = yysize0;
+                    break;
+                  }
+                yyarg[yycount++] = yytname[yyx];
+                {
+                  YYSIZE_T yysize1 = yysize + yytnamerr (YY_NULL, yytname[yyx]);
+                  if (! (yysize <= yysize1
+                         && yysize1 <= YYSTACK_ALLOC_MAXIMUM))
+                    return 2;
+                  yysize = yysize1;
+                }
+              }
+        }
+    }
+
+  switch (yycount)
+    {
+# define YYCASE_(N, S)                      \
+      case N:                               \
+        yyformat = S;                       \
+      break
+      YYCASE_(0, YY_("syntax error"));
+      YYCASE_(1, YY_("syntax error, unexpected %s"));
+      YYCASE_(2, YY_("syntax error, unexpected %s, expecting %s"));
+      YYCASE_(3, YY_("syntax error, unexpected %s, expecting %s or %s"));
+      YYCASE_(4, YY_("syntax error, unexpected %s, expecting %s or %s or %s"));
+      YYCASE_(5, YY_("syntax error, unexpected %s, expecting %s or %s or %s or %s"));
+# undef YYCASE_
+    }
+
+  {
+    YYSIZE_T yysize1 = yysize + yystrlen (yyformat);
+    if (! (yysize <= yysize1 && yysize1 <= YYSTACK_ALLOC_MAXIMUM))
+      return 2;
+    yysize = yysize1;
+  }
+
+  if (*yymsg_alloc < yysize)
+    {
+      *yymsg_alloc = 2 * yysize;
+      if (! (yysize <= *yymsg_alloc
+             && *yymsg_alloc <= YYSTACK_ALLOC_MAXIMUM))
+        *yymsg_alloc = YYSTACK_ALLOC_MAXIMUM;
+      return 1;
+    }
+
+  /* Avoid sprintf, as that infringes on the user's name space.
+     Don't have undefined behavior even if the translation
+     produced a string with the wrong number of "%s"s.  */
+  {
+    char *yyp = *yymsg;
+    int yyi = 0;
+    while ((*yyp = *yyformat) != '\0')
+      if (*yyp == '%' && yyformat[1] == 's' && yyi < yycount)
+        {
+          yyp += yytnamerr (yyp, yyarg[yyi++]);
+          yyformat += 2;
+        }
+      else
+        {
+          yyp++;
+          yyformat++;
+        }
+  }
+  return 0;
+}
+#endif /* YYERROR_VERBOSE */
+
+/*-----------------------------------------------.
+| Release the memory associated to this symbol.  |
+`-----------------------------------------------*/
+
+/*ARGSUSED*/
+#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)
+#else
+static void
+yydestruct (yymsg, yytype, yyvaluep, ctx, scanner)
+    const char *yymsg;
+    int yytype;
+    YYSTYPE *yyvaluep;
+    uscxml::PromelaParser* ctx;
+    void * scanner;
+#endif
+{
+  YYUSE (yyvaluep);
+  YYUSE (ctx);
+  YYUSE (scanner);
+
+  if (!yymsg)
+    yymsg = "Deleting";
+  YY_SYMBOL_PRINT (yymsg, yytype, yyvaluep, yylocationp);
+
+  YYUSE (yytype);
+}
+
+
+
+
+/*----------.
+| yyparse.  |
+`----------*/
+
+#ifdef YYPARSE_PARAM
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+int
+yyparse (void *YYPARSE_PARAM)
+#else
+int
+yyparse (YYPARSE_PARAM)
+    void *YYPARSE_PARAM;
+#endif
+#else /* ! YYPARSE_PARAM */
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+int
+yyparse (uscxml::PromelaParser* ctx, void * scanner)
+#else
+int
+yyparse (ctx, scanner)
+    uscxml::PromelaParser* ctx;
+    void * scanner;
+#endif
+#endif
+{
+/* The lookahead symbol.  */
+int yychar;
+
+
+#if defined __GNUC__ && 407 <= __GNUC__ * 100 + __GNUC_MINOR__
+/* Suppress an incorrect diagnostic about yylval being uninitialized.  */
+# define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
+    _Pragma ("GCC diagnostic push") \
+    _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")\
+    _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
+# define YY_IGNORE_MAYBE_UNINITIALIZED_END \
+    _Pragma ("GCC diagnostic pop")
+#else
+/* Default value used for initialization, for pacifying older GCCs
+   or non-GCC compilers.  */
+static YYSTYPE yyval_default;
+# define YY_INITIAL_VALUE(Value) = Value
+#endif
+#ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
+# define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
+# define YY_IGNORE_MAYBE_UNINITIALIZED_END
+#endif
+#ifndef YY_INITIAL_VALUE
+# define YY_INITIAL_VALUE(Value) /* Nothing. */
+#endif
+
+/* The semantic value of the lookahead symbol.  */
+YYSTYPE yylval YY_INITIAL_VALUE(yyval_default);
+
+    /* Number of syntax errors so far.  */
+    int yynerrs;
+
+    int yystate;
+    /* Number of tokens to shift before error messages enabled.  */
+    int yyerrstatus;
+
+    /* The stacks and their tools:
+       `yyss': related to states.
+       `yyvs': related to semantic values.
+
+       Refer to the stacks through separate pointers, to allow yyoverflow
+       to reallocate them elsewhere.  */
+
+    /* The state stack.  */
+    yytype_int16 yyssa[YYINITDEPTH];
+    yytype_int16 *yyss;
+    yytype_int16 *yyssp;
+
+    /* The semantic value stack.  */
+    YYSTYPE yyvsa[YYINITDEPTH];
+    YYSTYPE *yyvs;
+    YYSTYPE *yyvsp;
+
+    YYSIZE_T yystacksize;
+
+  int yyn;
+  int yyresult;
+  /* Lookahead token as an internal (translated) token number.  */
+  int yytoken = 0;
+  /* The variables used to return semantic value and location from the
+     action routines.  */
+  YYSTYPE yyval;
+
+#if YYERROR_VERBOSE
+  /* Buffer for error messages, and its allocated size.  */
+  char yymsgbuf[128];
+  char *yymsg = yymsgbuf;
+  YYSIZE_T yymsg_alloc = sizeof yymsgbuf;
+#endif
+
+#define YYPOPSTACK(N)   (yyvsp -= (N), yyssp -= (N))
+
+  /* The number of symbols on the RHS of the reduced rule.
+     Keep to zero when no symbol should be popped.  */
+  int yylen = 0;
+
+  yyssp = yyss = yyssa;
+  yyvsp = yyvs = yyvsa;
+  yystacksize = YYINITDEPTH;
+
+  YYDPRINTF ((stderr, "Starting parse\n"));
+
+  yystate = 0;
+  yyerrstatus = 0;
+  yynerrs = 0;
+  yychar = YYEMPTY; /* Cause a token to be read.  */
+  goto yysetstate;
+
+/*------------------------------------------------------------.
+| yynewstate -- Push a new state, which is found in yystate.  |
+`------------------------------------------------------------*/
+ yynewstate:
+  /* In all cases, when you get here, the value and location stacks
+     have just been pushed.  So pushing a state here evens the stacks.  */
+  yyssp++;
+
+ yysetstate:
+  *yyssp = yystate;
+
+  if (yyss + yystacksize - 1 <= yyssp)
+    {
+      /* Get the current used size of the three stacks, in elements.  */
+      YYSIZE_T yysize = yyssp - yyss + 1;
+
+#ifdef yyoverflow
+      {
+	/* Give user a chance to reallocate the stack.  Use copies of
+	   these so that the &'s don't force the real ones into
+	   memory.  */
+	YYSTYPE *yyvs1 = yyvs;
+	yytype_int16 *yyss1 = yyss;
+
+	/* Each stack pointer address is followed by the size of the
+	   data in use in that stack, in bytes.  This used to be a
+	   conditional around just the two extra args, but that might
+	   be undefined if yyoverflow is a macro.  */
+	yyoverflow (YY_("memory exhausted"),
+		    &yyss1, yysize * sizeof (*yyssp),
+		    &yyvs1, yysize * sizeof (*yyvsp),
+		    &yystacksize);
+
+	yyss = yyss1;
+	yyvs = yyvs1;
+      }
+#else /* no yyoverflow */
+# ifndef YYSTACK_RELOCATE
+      goto yyexhaustedlab;
+# else
+      /* Extend the stack our own way.  */
+      if (YYMAXDEPTH <= yystacksize)
+	goto yyexhaustedlab;
+      yystacksize *= 2;
+      if (YYMAXDEPTH < yystacksize)
+	yystacksize = YYMAXDEPTH;
+
+      {
+	yytype_int16 *yyss1 = yyss;
+	union yyalloc *yyptr =
+	  (union yyalloc *) YYSTACK_ALLOC (YYSTACK_BYTES (yystacksize));
+	if (! yyptr)
+	  goto yyexhaustedlab;
+	YYSTACK_RELOCATE (yyss_alloc, yyss);
+	YYSTACK_RELOCATE (yyvs_alloc, yyvs);
+#  undef YYSTACK_RELOCATE
+	if (yyss1 != yyssa)
+	  YYSTACK_FREE (yyss1);
+      }
+# endif
+#endif /* no yyoverflow */
+
+      yyssp = yyss + yysize - 1;
+      yyvsp = yyvs + yysize - 1;
+
+      YYDPRINTF ((stderr, "Stack size increased to %lu\n",
+		  (unsigned long int) yystacksize));
+
+      if (yyss + yystacksize - 1 <= yyssp)
+	YYABORT;
+    }
+
+  YYDPRINTF ((stderr, "Entering state %d\n", yystate));
+
+  if (yystate == YYFINAL)
+    YYACCEPT;
+
+  goto yybackup;
+
+/*-----------.
+| yybackup.  |
+`-----------*/
+yybackup:
+
+  /* Do appropriate processing given the current state.  Read a
+     lookahead token if we need one and don't already have one.  */
+
+  /* First try to decide what to do without reference to lookahead token.  */
+  yyn = yypact[yystate];
+  if (yypact_value_is_default (yyn))
+    goto yydefault;
+
+  /* Not known => get a lookahead token if don't already have one.  */
+
+  /* YYCHAR is either YYEMPTY or YYEOF or a valid lookahead symbol.  */
+  if (yychar == YYEMPTY)
+    {
+      YYDPRINTF ((stderr, "Reading a token: "));
+      yychar = YYLEX;
+    }
+
+  if (yychar <= YYEOF)
+    {
+      yychar = yytoken = YYEOF;
+      YYDPRINTF ((stderr, "Now at end of input.\n"));
+    }
+  else
+    {
+      yytoken = YYTRANSLATE (yychar);
+      YY_SYMBOL_PRINT ("Next token is", yytoken, &yylval, &yylloc);
+    }
+
+  /* If the proper action on seeing token YYTOKEN is to reduce or to
+     detect an error, take that action.  */
+  yyn += yytoken;
+  if (yyn < 0 || YYLAST < yyn || yycheck[yyn] != yytoken)
+    goto yydefault;
+  yyn = yytable[yyn];
+  if (yyn <= 0)
+    {
+      if (yytable_value_is_error (yyn))
+        goto yyerrlab;
+      yyn = -yyn;
+      goto yyreduce;
+    }
+
+  /* Count tokens shifted since error; after three, turn off error
+     status.  */
+  if (yyerrstatus)
+    yyerrstatus--;
+
+  /* Shift the lookahead token.  */
+  YY_SYMBOL_PRINT ("Shifting", yytoken, &yylval, &yylloc);
+
+  /* Discard the shifted token.  */
+  yychar = YYEMPTY;
+
+  yystate = yyn;
+  YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
+  *++yyvsp = yylval;
+  YY_IGNORE_MAYBE_UNINITIALIZED_END
+
+  goto yynewstate;
+
+
+/*-----------------------------------------------------------.
+| yydefault -- do the default action for the current state.  |
+`-----------------------------------------------------------*/
+yydefault:
+  yyn = yydefact[yystate];
+  if (yyn == 0)
+    goto yyerrlab;
+  goto yyreduce;
+
+
+/*-----------------------------.
+| yyreduce -- Do a reduction.  |
+`-----------------------------*/
+yyreduce:
+  /* yyn is the number of a rule to reduce with.  */
+  yylen = yyr2[yyn];
+
+  /* If YYLEN is nonzero, implement the default value of the action:
+     `$$ = $1'.
+
+     Otherwise, the following line sets YYVAL to garbage.
+     This behavior is undocumented and Bison
+     users should not rely upon it.  Assigning to YYVAL
+     unconditionally makes the parser a bit smaller, and it avoids a
+     GCC warning that YYVAL may be used uninitialized.  */
+  yyval = yyvsp[1-yylen];
+
+
+  YY_REDUCE_PRINT (yyn);
+  switch (yyn)
+    {
+        case 2:
+/* Line 1787 of yacc.c  */
+#line 75 "promela.ypp"
+    { 
+    ctx->ast = (yyvsp[(1) - (1)].node); 
+    ctx->type = PromelaParser::PROMELA_DECL; 
+  }
+    break;
+
+  case 3:
+/* Line 1787 of yacc.c  */
+#line 79 "promela.ypp"
+    { 
+    ctx->ast = (yyvsp[(1) - (1)].node); 
+    ctx->type = PromelaParser::PROMELA_EXPR;
+  }
+    break;
+
+  case 4:
+/* Line 1787 of yacc.c  */
+#line 84 "promela.ypp"
+    {}
+    break;
+
+  case 5:
+/* Line 1787 of yacc.c  */
+#line 87 "promela.ypp"
+    { (yyval.node) = ctx->value(yylval.value); }
+    break;
+
+  case 6:
+/* Line 1787 of yacc.c  */
+#line 88 "promela.ypp"
+    {}
+    break;
+
+  case 7:
+/* Line 1787 of yacc.c  */
+#line 91 "promela.ypp"
+    {}
+    break;
+
+  case 8:
+/* Line 1787 of yacc.c  */
+#line 92 "promela.ypp"
+    {}
+    break;
+
+  case 9:
+/* Line 1787 of yacc.c  */
+#line 95 "promela.ypp"
+    {}
+    break;
+
+  case 10:
+/* Line 1787 of yacc.c  */
+#line 96 "promela.ypp"
+    {}
+    break;
+
+  case 11:
+/* Line 1787 of yacc.c  */
+#line 99 "promela.ypp"
+    { (yyval.node) = (yyvsp[(2) - (3)].node); }
+    break;
+
+  case 12:
+/* Line 1787 of yacc.c  */
+#line 100 "promela.ypp"
+    { (yyval.node) = ctx->binOp(PLUS, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 13:
+/* Line 1787 of yacc.c  */
+#line 101 "promela.ypp"
+    { (yyval.node) = ctx->binOp(MINUS, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 14:
+/* Line 1787 of yacc.c  */
+#line 102 "promela.ypp"
+    { (yyval.node) = ctx->binOp(TIMES, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 15:
+/* Line 1787 of yacc.c  */
+#line 103 "promela.ypp"
+    { (yyval.node) = ctx->binOp(DIVIDE, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 16:
+/* Line 1787 of yacc.c  */
+#line 104 "promela.ypp"
+    { (yyval.node) = ctx->binOp(MODULO, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 17:
+/* Line 1787 of yacc.c  */
+#line 105 "promela.ypp"
+    { (yyval.node) = ctx->binOp(BITAND, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 18:
+/* Line 1787 of yacc.c  */
+#line 106 "promela.ypp"
+    { (yyval.node) = ctx->binOp(BITXOR, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 19:
+/* Line 1787 of yacc.c  */
+#line 107 "promela.ypp"
+    { (yyval.node) = ctx->binOp(BITOR, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 20:
+/* Line 1787 of yacc.c  */
+#line 108 "promela.ypp"
+    { (yyval.node) = ctx->binOp(GT, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 21:
+/* Line 1787 of yacc.c  */
+#line 109 "promela.ypp"
+    { (yyval.node) = ctx->binOp(LT, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 22:
+/* Line 1787 of yacc.c  */
+#line 110 "promela.ypp"
+    { (yyval.node) = ctx->binOp(GE, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 23:
+/* Line 1787 of yacc.c  */
+#line 111 "promela.ypp"
+    { (yyval.node) = ctx->binOp(LE, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 24:
+/* Line 1787 of yacc.c  */
+#line 112 "promela.ypp"
+    { (yyval.node) = ctx->binOp(EQ, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 25:
+/* Line 1787 of yacc.c  */
+#line 113 "promela.ypp"
+    { (yyval.node) = ctx->binOp(NE, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 26:
+/* Line 1787 of yacc.c  */
+#line 114 "promela.ypp"
+    { (yyval.node) = ctx->binOp(AND, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 27:
+/* Line 1787 of yacc.c  */
+#line 115 "promela.ypp"
+    { (yyval.node) = ctx->binOp(OR, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 28:
+/* Line 1787 of yacc.c  */
+#line 116 "promela.ypp"
+    { (yyval.node) = ctx->binOp(LSHIFT, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 29:
+/* Line 1787 of yacc.c  */
+#line 117 "promela.ypp"
+    { (yyval.node) = ctx->binOp(RSHIFT, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 30:
+/* Line 1787 of yacc.c  */
+#line 118 "promela.ypp"
+    { (yyval.node) = ctx->uniOp(NEG, (yyvsp[(2) - (2)].node)); }
+    break;
+
+  case 31:
+/* Line 1787 of yacc.c  */
+#line 119 "promela.ypp"
+    { (yyval.node) = ctx->uniOp(MINUS, (yyvsp[(2) - (2)].node)); }
+    break;
+
+  case 32:
+/* Line 1787 of yacc.c  */
+#line 121 "promela.ypp"
+    { (yyval.node) = ctx->uniOp(LEN, (yyvsp[(3) - (4)].node));  }
+    break;
+
+  case 33:
+/* Line 1787 of yacc.c  */
+#line 122 "promela.ypp"
+    {  }
+    break;
+
+  case 34:
+/* Line 1787 of yacc.c  */
+#line 123 "promela.ypp"
+    { (yyval.node) = ctx->value(yylval.value); }
+    break;
+
+  case 35:
+/* Line 1787 of yacc.c  */
+#line 127 "promela.ypp"
+    { }
+    break;
+
+  case 36:
+/* Line 1787 of yacc.c  */
+#line 128 "promela.ypp"
+    {  }
+    break;
+
+  case 37:
+/* Line 1787 of yacc.c  */
+#line 129 "promela.ypp"
+    {  }
+    break;
+
+  case 38:
+/* Line 1787 of yacc.c  */
+#line 130 "promela.ypp"
+    {  }
+    break;
+
+  case 39:
+/* Line 1787 of yacc.c  */
+#line 133 "promela.ypp"
+    { (yyval.node) = ctx->uniOp(ASGN, (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 40:
+/* Line 1787 of yacc.c  */
+#line 134 "promela.ypp"
+    { }
+    break;
+
+  case 41:
+/* Line 1787 of yacc.c  */
+#line 135 "promela.ypp"
+    { }
+    break;
+
+  case 42:
+/* Line 1787 of yacc.c  */
+#line 138 "promela.ypp"
+    { }
+    break;
+
+  case 43:
+/* Line 1787 of yacc.c  */
+#line 140 "promela.ypp"
+    {  }
+    break;
+
+  case 44:
+/* Line 1787 of yacc.c  */
+#line 143 "promela.ypp"
+    { (yyval.node) = ctx->uniOp(ASGN, (yyvsp[(1) - (1)].node)); }
+    break;
+
+  case 45:
+/* Line 1787 of yacc.c  */
+#line 144 "promela.ypp"
+    { (yyval.node) = ctx->binOp(ASGN, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 46:
+/* Line 1787 of yacc.c  */
+#line 147 "promela.ypp"
+    { (yyval.node) = ctx->uniOp(ASGN, (yyvsp[(1) - (1)].node)); }
+    break;
+
+  case 47:
+/* Line 1787 of yacc.c  */
+#line 148 "promela.ypp"
+    { (yyval.node) = ctx->binOp(ASGN, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); }
+    break;
+
+  case 48:
+/* Line 1787 of yacc.c  */
+#line 151 "promela.ypp"
+    { (yyval.node) = ctx->value(yylval.value); }
+    break;
+
+  case 49:
+/* Line 1787 of yacc.c  */
+#line 152 "promela.ypp"
+    { }
+    break;
+
+  case 50:
+/* Line 1787 of yacc.c  */
+#line 153 "promela.ypp"
+    { }
+    break;
+
+  case 51:
+/* Line 1787 of yacc.c  */
+#line 156 "promela.ypp"
+    { }
+    break;
+
+  case 52:
+/* Line 1787 of yacc.c  */
+#line 157 "promela.ypp"
+    {  }
+    break;
+
+  case 53:
+/* Line 1787 of yacc.c  */
+#line 158 "promela.ypp"
+    {  }
+    break;
+
+  case 54:
+/* Line 1787 of yacc.c  */
+#line 159 "promela.ypp"
+    {  }
+    break;
+
+  case 55:
+/* Line 1787 of yacc.c  */
+#line 160 "promela.ypp"
+    {  }
+    break;
+
+  case 56:
+/* Line 1787 of yacc.c  */
+#line 161 "promela.ypp"
+    {  }
+    break;
+
+  case 57:
+/* Line 1787 of yacc.c  */
+#line 162 "promela.ypp"
+    {  }
+    break;
+
+  case 58:
+/* Line 1787 of yacc.c  */
+#line 163 "promela.ypp"
+    {  }
+    break;
+
+  case 59:
+/* Line 1787 of yacc.c  */
+#line 166 "promela.ypp"
+    {  }
+    break;
+
+  case 60:
+/* Line 1787 of yacc.c  */
+#line 167 "promela.ypp"
+    {  }
+    break;
+
+  case 61:
+/* Line 1787 of yacc.c  */
+#line 168 "promela.ypp"
+    {  }
+    break;
+
+
+/* Line 1787 of yacc.c  */
+#line 1943 "promela.tab.cpp"
+      default: break;
+    }
+  /* User semantic actions sometimes alter yychar, and that requires
+     that yytoken be updated with the new translation.  We take the
+     approach of translating immediately before every use of yytoken.
+     One alternative is translating here after every semantic action,
+     but that translation would be missed if the semantic action invokes
+     YYABORT, YYACCEPT, or YYERROR immediately after altering yychar or
+     if it invokes YYBACKUP.  In the case of YYABORT or YYACCEPT, an
+     incorrect destructor might then be invoked immediately.  In the
+     case of YYERROR or YYBACKUP, subsequent parser actions might lead
+     to an incorrect destructor call or verbose syntax error message
+     before the lookahead is translated.  */
+  YY_SYMBOL_PRINT ("-> $$ =", yyr1[yyn], &yyval, &yyloc);
+
+  YYPOPSTACK (yylen);
+  yylen = 0;
+  YY_STACK_PRINT (yyss, yyssp);
+
+  *++yyvsp = yyval;
+
+  /* Now `shift' the result of the reduction.  Determine what state
+     that goes to, based on the state we popped back to and the rule
+     number reduced by.  */
+
+  yyn = yyr1[yyn];
+
+  yystate = yypgoto[yyn - YYNTOKENS] + *yyssp;
+  if (0 <= yystate && yystate <= YYLAST && yycheck[yystate] == *yyssp)
+    yystate = yytable[yystate];
+  else
+    yystate = yydefgoto[yyn - YYNTOKENS];
+
+  goto yynewstate;
+
+
+/*------------------------------------.
+| yyerrlab -- here on detecting error |
+`------------------------------------*/
+yyerrlab:
+  /* Make sure we have latest lookahead translation.  See comments at
+     user semantic actions for why this is necessary.  */
+  yytoken = yychar == YYEMPTY ? YYEMPTY : YYTRANSLATE (yychar);
+
+  /* If not already recovering from an error, report this error.  */
+  if (!yyerrstatus)
+    {
+      ++yynerrs;
+#if ! YYERROR_VERBOSE
+      yyerror (ctx, scanner, YY_("syntax error"));
+#else
+# define YYSYNTAX_ERROR yysyntax_error (&yymsg_alloc, &yymsg, \
+                                        yyssp, yytoken)
+      {
+        char const *yymsgp = YY_("syntax error");
+        int yysyntax_error_status;
+        yysyntax_error_status = YYSYNTAX_ERROR;
+        if (yysyntax_error_status == 0)
+          yymsgp = yymsg;
+        else if (yysyntax_error_status == 1)
+          {
+            if (yymsg != yymsgbuf)
+              YYSTACK_FREE (yymsg);
+            yymsg = (char *) YYSTACK_ALLOC (yymsg_alloc);
+            if (!yymsg)
+              {
+                yymsg = yymsgbuf;
+                yymsg_alloc = sizeof yymsgbuf;
+                yysyntax_error_status = 2;
+              }
+            else
+              {
+                yysyntax_error_status = YYSYNTAX_ERROR;
+                yymsgp = yymsg;
+              }
+          }
+        yyerror (ctx, scanner, yymsgp);
+        if (yysyntax_error_status == 2)
+          goto yyexhaustedlab;
+      }
+# undef YYSYNTAX_ERROR
+#endif
+    }
+
+
+
+  if (yyerrstatus == 3)
+    {
+      /* If just tried and failed to reuse lookahead token after an
+	 error, discard it.  */
+
+      if (yychar <= YYEOF)
+	{
+	  /* Return failure if at end of input.  */
+	  if (yychar == YYEOF)
+	    YYABORT;
+	}
+      else
+	{
+	  yydestruct ("Error: discarding",
+		      yytoken, &yylval, ctx, scanner);
+	  yychar = YYEMPTY;
+	}
+    }
+
+  /* Else will try to reuse lookahead token after shifting the error
+     token.  */
+  goto yyerrlab1;
+
+
+/*---------------------------------------------------.
+| yyerrorlab -- error raised explicitly by YYERROR.  |
+`---------------------------------------------------*/
+yyerrorlab:
+
+  /* Pacify compilers like GCC when the user code never invokes
+     YYERROR and the label yyerrorlab therefore never appears in user
+     code.  */
+  if (/*CONSTCOND*/ 0)
+     goto yyerrorlab;
+
+  /* Do not reclaim the symbols of the rule which action triggered
+     this YYERROR.  */
+  YYPOPSTACK (yylen);
+  yylen = 0;
+  YY_STACK_PRINT (yyss, yyssp);
+  yystate = *yyssp;
+  goto yyerrlab1;
+
+
+/*-------------------------------------------------------------.
+| yyerrlab1 -- common code for both syntax error and YYERROR.  |
+`-------------------------------------------------------------*/
+yyerrlab1:
+  yyerrstatus = 3;	/* Each real token shifted decrements this.  */
+
+  for (;;)
+    {
+      yyn = yypact[yystate];
+      if (!yypact_value_is_default (yyn))
+	{
+	  yyn += YYTERROR;
+	  if (0 <= yyn && yyn <= YYLAST && yycheck[yyn] == YYTERROR)
+	    {
+	      yyn = yytable[yyn];
+	      if (0 < yyn)
+		break;
+	    }
+	}
+
+      /* Pop the current state because it cannot handle the error token.  */
+      if (yyssp == yyss)
+	YYABORT;
+
+
+      yydestruct ("Error: popping",
+		  yystos[yystate], yyvsp, ctx, scanner);
+      YYPOPSTACK (1);
+      yystate = *yyssp;
+      YY_STACK_PRINT (yyss, yyssp);
+    }
+
+  YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
+  *++yyvsp = yylval;
+  YY_IGNORE_MAYBE_UNINITIALIZED_END
+
+
+  /* Shift the error token.  */
+  YY_SYMBOL_PRINT ("Shifting", yystos[yyn], yyvsp, yylsp);
+
+  yystate = yyn;
+  goto yynewstate;
+
+
+/*-------------------------------------.
+| yyacceptlab -- YYACCEPT comes here.  |
+`-------------------------------------*/
+yyacceptlab:
+  yyresult = 0;
+  goto yyreturn;
+
+/*-----------------------------------.
+| yyabortlab -- YYABORT comes here.  |
+`-----------------------------------*/
+yyabortlab:
+  yyresult = 1;
+  goto yyreturn;
+
+#if !defined yyoverflow || YYERROR_VERBOSE
+/*-------------------------------------------------.
+| yyexhaustedlab -- memory exhaustion comes here.  |
+`-------------------------------------------------*/
+yyexhaustedlab:
+  yyerror (ctx, scanner, YY_("memory exhausted"));
+  yyresult = 2;
+  /* Fall through.  */
+#endif
+
+yyreturn:
+  if (yychar != YYEMPTY)
+    {
+      /* Make sure we have latest lookahead translation.  See comments at
+         user semantic actions for why this is necessary.  */
+      yytoken = YYTRANSLATE (yychar);
+      yydestruct ("Cleanup: discarding lookahead",
+                  yytoken, &yylval, ctx, scanner);
+    }
+  /* Do not reclaim the symbols of the rule which action triggered
+     this YYABORT or YYACCEPT.  */
+  YYPOPSTACK (yylen);
+  YY_STACK_PRINT (yyss, yyssp);
+  while (yyssp != yyss)
+    {
+      yydestruct ("Cleanup: popping",
+		  yystos[*yyssp], yyvsp, ctx, scanner);
+      YYPOPSTACK (1);
+    }
+#ifndef yyoverflow
+  if (yyss != yyssa)
+    YYSTACK_FREE (yyss);
+#endif
+#if YYERROR_VERBOSE
+  if (yymsg != yymsgbuf)
+    YYSTACK_FREE (yymsg);
+#endif
+  /* Make sure YYID is used.  */
+  return YYID (yyresult);
+}
+
+
+/* Line 2050 of yacc.c  */
+#line 171 "promela.ypp"
+
+
diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.tab.hpp b/src/uscxml/plugins/datamodel/promela/parser/promela.tab.hpp
new file mode 100644
index 0000000..66c0e03
--- /dev/null
+++ b/src/uscxml/plugins/datamodel/promela/parser/promela.tab.hpp
@@ -0,0 +1,154 @@
+/* A Bison parser, made by GNU Bison 2.7.12-4996.  */
+
+/* Bison interface for Yacc-like parsers in C
+   
+      Copyright (C) 1984, 1989-1990, 2000-2013 Free Software Foundation, Inc.
+   
+   This program is free software: you can redistribute it and/or modify
+   it under the terms of the GNU General Public License as published by
+   the Free Software Foundation, either version 3 of the License, or
+   (at your option) any later version.
+   
+   This program is distributed in the hope that it will be useful,
+   but WITHOUT ANY WARRANTY; without even the implied warranty of
+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+   GNU General Public License for more details.
+   
+   You should have received a copy of the GNU General Public License
+   along with this program.  If not, see <http://www.gnu.org/licenses/>.  */
+
+/* As a special exception, you may create a larger work that contains
+   part or all of the Bison parser skeleton and distribute that work
+   under terms of your choice, so long as that work isn't itself a
+   parser generator using the skeleton or a modified version thereof
+   as a parser skeleton.  Alternatively, if you modify or redistribute
+   the parser skeleton itself, you may (at your option) remove this
+   special exception, which will cause the skeleton and the resulting
+   Bison output files to be licensed under the GNU General Public
+   License without this special exception.
+   
+   This special exception was added by the Free Software Foundation in
+   version 2.2 of Bison.  */
+
+#ifndef YY_PROMELA_PROMELA_TAB_HPP_INCLUDED
+# define YY_PROMELA_PROMELA_TAB_HPP_INCLUDED
+/* Enabling traces.  */
+#ifndef PROMELA_DEBUG
+# if defined YYDEBUG
+#  if YYDEBUG
+#   define PROMELA_DEBUG 1
+#  else
+#   define PROMELA_DEBUG 0
+#  endif
+# else /* ! defined YYDEBUG */
+#  define PROMELA_DEBUG 0
+# endif /* ! defined YYDEBUG */
+#endif  /* ! defined PROMELA_DEBUG */
+#if PROMELA_DEBUG
+extern int promela_debug;
+#endif
+
+/* Tokens.  */
+#ifndef PROMELA_TOKENTYPE
+# define PROMELA_TOKENTYPE
+   /* Put the tokens into the symbol table, so that GDB and other debuggers
+      know about them.  */
+   enum promela_tokentype {
+     LBRACKET = 258,
+     RBRACKET = 259,
+     LEN = 260,
+     TYPEDEF = 261,
+     MTYPE = 262,
+     INLINE = 263,
+     RETURN = 264,
+     LABEL = 265,
+     OF = 266,
+     GOTO = 267,
+     BREAK = 268,
+     ELSE = 269,
+     SEMI = 270,
+     ARROW = 271,
+     IF = 272,
+     FI = 273,
+     DO = 274,
+     OD = 275,
+     FOR = 276,
+     SELECT = 277,
+     IN = 278,
+     SEP = 279,
+     DOTDOT = 280,
+     HIDDEN = 281,
+     SHOW = 282,
+     ISLOCAL = 283,
+     CONST = 284,
+     TYPE = 285,
+     XU = 286,
+     NAME = 287,
+     UNAME = 288,
+     PNAME = 289,
+     INAME = 290,
+     STRING = 291,
+     CLAIM = 292,
+     TRACE = 293,
+     INIT = 294,
+     LTL = 295,
+     ASGN = 296,
+     AND = 297,
+     OR = 298,
+     BITAND = 299,
+     BITXOR = 300,
+     BITOR = 301,
+     NE = 302,
+     EQ = 303,
+     LE = 304,
+     GE = 305,
+     LT = 306,
+     GT = 307,
+     RSHIFT = 308,
+     LSHIFT = 309,
+     MINUS = 310,
+     PLUS = 311,
+     MODULO = 312,
+     DIVIDE = 313,
+     TIMES = 314,
+     COMPL = 315,
+     NEG = 316,
+     DOT = 317
+   };
+#endif
+
+
+#if ! defined PROMELA_STYPE && ! defined PROMELA_STYPE_IS_DECLARED
+typedef union PROMELA_STYPE
+{
+/* Line 2053 of yacc.c  */
+#line 37 "promela.ypp"
+
+  uscxml::PromelaParserNode* node;
+	char* value;
+
+
+/* Line 2053 of yacc.c  */
+#line 133 "promela.tab.hpp"
+} PROMELA_STYPE;
+# define PROMELA_STYPE_IS_TRIVIAL 1
+# define promela_stype PROMELA_STYPE /* obsolescent; will be withdrawn */
+# define PROMELA_STYPE_IS_DECLARED 1
+#endif
+
+
+#ifdef YYPARSE_PARAM
+#if defined __STDC__ || defined __cplusplus
+int promela_parse (void *YYPARSE_PARAM);
+#else
+int promela_parse ();
+#endif
+#else /* ! YYPARSE_PARAM */
+#if defined __STDC__ || defined __cplusplus
+int promela_parse (uscxml::PromelaParser* ctx, void * scanner);
+#else
+int promela_parse ();
+#endif
+#endif /* ! YYPARSE_PARAM */
+
+#endif /* !YY_PROMELA_PROMELA_TAB_HPP_INCLUDED  */
diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.ypp b/src/uscxml/plugins/datamodel/promela/parser/promela.ypp
new file mode 100644
index 0000000..8b4426b
--- /dev/null
+++ b/src/uscxml/plugins/datamodel/promela/parser/promela.ypp
@@ -0,0 +1,172 @@
+/** Subset extracted from spin.y by Stefan Radomski 2014                  */
+
+/***** spin: spin.y *****/
+
+/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     */
+/* All Rights Reserved.  This software is for educational purposes only.  */
+/* No guarantee whatsoever is expressed or implied by the distribution of */
+/* this code.  Permission is given to distribute this code provided that  */
+/* this introductory message is not removed and no monies are exchanged.  */
+/* Software written by Gerard J. Holzmann.  For tool documentation see:   */
+/*             http://spinroot.com/                                       */
+/* Send all bug-reports and/or questions to: bugs@spinroot.com            */
+
+%{
+#include "../PromelaParser.h"
+#include "promela.tab.hpp"
+#include <sys/types.h>
+#include <stdarg.h>
+
+#define YYMAXDEPTH	20000	// default is 10000
+#define YYDEBUG		1
+#define YYERROR_VERBOSE 1
+
+extern int promela_lex (PROMELA_STYPE* yylval_param, void* yyscanner);
+
+using namespace uscxml;
+%}
+
+%pure-parser
+%file-prefix "promela"
+%parse-param { uscxml::PromelaParser* ctx }
+%lex-param {void * scanner}
+%parse-param {void * scanner}
+%define api.prefix promela_
+%defines
+
+%union {
+  uscxml::PromelaParserNode* node;
+	char* value;
+}
+
+%error-verbose
+
+
+%type <node> expr pfld varref decl_lst vardcl ivar var_list one_decl
+
+%token  LBRACKET RBRACKET
+%token  <value> LEN
+%token  TYPEDEF MTYPE INLINE RETURN LABEL OF
+%token  GOTO BREAK ELSE SEMI ARROW
+%token  IF FI DO OD FOR SELECT IN SEP DOTDOT
+%token  HIDDEN SHOW ISLOCAL
+%token  <value> CONST TYPE XU			/* val */
+%token  <value> NAME UNAME PNAME INAME		/* sym */
+%token  STRING CLAIM TRACE INIT	LTL	/* sym */
+
+%right	ASGN
+%left OR AND
+%left	BITOR BITXOR BITAND
+%left	EQ NE
+%left	GT LT GE LE
+%left	LSHIFT RSHIFT
+%left	PLUS MINUS 
+%left TIMES DIVIDE MODULO
+%left COMPL
+%right NEG
+%left	DOT
+
+%%
+
+
+/** PROMELA Grammar Rules **/
+
+program	: 
+  decl_lst { 
+    ctx->ast = $1; 
+    ctx->type = PromelaParser::PROMELA_DECL; 
+  }
+  | expr { 
+    ctx->ast = $1; 
+    ctx->type = PromelaParser::PROMELA_EXPR;
+  }
+
+varref	: cmpnd			{}
+	;
+
+pfld	: NAME			{ $$ = ctx->value(yylval.value); }
+	| NAME '[' expr ']' {}
+	;
+
+cmpnd	: pfld			{}
+				sfld			{}
+	;
+
+sfld	: /* empty */		{}
+	| '.' cmpnd %prec DOT	{}
+	;
+
+expr    : LBRACKET expr RBRACKET		{ $$ = $2; }
+	| expr PLUS expr		{ $$ = ctx->binOp(PLUS, $1, $3); }
+	| expr MINUS expr		{ $$ = ctx->binOp(MINUS, $1, $3); }
+	| expr TIMES expr		{ $$ = ctx->binOp(TIMES, $1, $3); }
+	| expr DIVIDE expr		{ $$ = ctx->binOp(DIVIDE, $1, $3); }
+	| expr MODULO expr		{ $$ = ctx->binOp(MODULO, $1, $3); }
+	| expr BITAND expr		{ $$ = ctx->binOp(BITAND, $1, $3); }
+	| expr BITXOR expr		{ $$ = ctx->binOp(BITXOR, $1, $3); }
+	| expr BITOR expr		{ $$ = ctx->binOp(BITOR, $1, $3); }
+	| expr GT expr		{ $$ = ctx->binOp(GT, $1, $3); }
+	| expr LT expr		{ $$ = ctx->binOp(LT, $1, $3); }
+	| expr GE expr		{ $$ = ctx->binOp(GE, $1, $3); }
+	| expr LE expr		{ $$ = ctx->binOp(LE, $1, $3); }
+	| expr EQ expr		{ $$ = ctx->binOp(EQ, $1, $3); }
+	| expr NE expr		{ $$ = ctx->binOp(NE, $1, $3); }
+	| expr AND expr		{ $$ = ctx->binOp(AND, $1, $3); }
+	| expr OR  expr		{ $$ = ctx->binOp(OR, $1, $3); }
+	| expr LSHIFT expr	{ $$ = ctx->binOp(LSHIFT, $1, $3); }
+	| expr RSHIFT expr	{ $$ = ctx->binOp(RSHIFT, $1, $3); }
+	| NEG expr		      { $$ = ctx->uniOp(NEG, $2); }
+	| MINUS expr %prec MINUS	{ $$ = ctx->uniOp(MINUS, $2); }
+
+	| LEN '(' varref ')'	{ $$ = ctx->uniOp(LEN, $3);  }
+	| varref		{  }
+	| CONST 		{ $$ = ctx->value(yylval.value); }
+	;
+
+
+vis	: /* empty */		{ }
+	| HIDDEN		{  }
+	| SHOW			{  }
+	| ISLOCAL		{  }
+	;
+
+one_decl: vis TYPE var_list	{ $$ = ctx->uniOp(ASGN, $3); }
+	| vis UNAME var_list	{ }
+	| vis TYPE ASGN '{' nlst '}' { }
+	;
+
+decl_lst: one_decl       	{ }
+	| one_decl SEMI
+	  decl_lst		{  }
+	;
+
+var_list: ivar           	{ $$ = ctx->uniOp(ASGN, $1); }
+	| ivar ',' var_list	{ $$ = ctx->binOp(ASGN, $1, $3); }
+	;
+
+ivar    : vardcl           	{ $$ = ctx->uniOp(ASGN, $1); }
+	| vardcl ASGN expr   	{ $$ = ctx->binOp(ASGN, $1, $3); }
+	;
+
+vardcl  : NAME  		{ $$ = ctx->value(yylval.value); }
+	| NAME ':' CONST	{ }
+	| NAME '[' const_expr ']'	{ }
+	;
+
+const_expr:	CONST			{ }
+	| '-' const_expr %prec MINUS	{  }
+	| '(' const_expr ')'		{  }
+	| const_expr '+' const_expr	{  }
+	| const_expr '-' const_expr	{  }
+	| const_expr '*' const_expr	{  }
+	| const_expr '/' const_expr	{  }
+	| const_expr '%' const_expr	{  }
+	;
+
+nlst	: NAME			{  }
+	| nlst NAME 		{  }
+	| nlst ','		{  }
+	;
+
+%%
+
diff --git a/src/uscxml/plugins/datamodel/xpath/XPathDataModel.cpp b/src/uscxml/plugins/datamodel/xpath/XPathDataModel.cpp
index cdbec28..27bf170 100644
--- a/src/uscxml/plugins/datamodel/xpath/XPathDataModel.cpp
+++ b/src/uscxml/plugins/datamodel/xpath/XPathDataModel.cpp
@@ -856,10 +856,11 @@ bool XPathFunctionIn::doEvaluate(const Node<std::string>& context,
 	for (int i = 0; i < argCount(); i++) {
 		XPathValue<std::string> stateName = arg(i, context, executionContext);
 		if (stateName.type() == STRING) {
-			if (!Interpreter::isMember(_interpreter->getState(stateName.asString()), _interpreter->getConfiguration())) {
-				return false;
+			if (_interpreter->isInState(stateName.asString())) {
+				continue;
 			}
 		}
+    return false;
 	}
 	return true;
 }
diff --git a/src/uscxml/plugins/invoker/scxml/USCXMLInvoker.cpp b/src/uscxml/plugins/invoker/scxml/USCXMLInvoker.cpp
index 05ea460..f1d9ad1 100644
--- a/src/uscxml/plugins/invoker/scxml/USCXMLInvoker.cpp
+++ b/src/uscxml/plugins/invoker/scxml/USCXMLInvoker.cpp
@@ -71,7 +71,8 @@ void USCXMLInvoker::invoke(const InvokeRequest& req) {
 		// we need to import the parent - to support xpath test150
 		Arabica::DOM::Node<std::string> newNode = dom.importNode(req.dom, true);
 		dom.appendChild(newNode);
-		_invokedInterpreter = Interpreter::fromDOM(dom);
+		// TODO: where do we get the namespace from?
+		_invokedInterpreter = Interpreter::fromDOM(dom, std::map<std::string, std::string>());
 	} else if (req.content.size() > 0) {
 		_invokedInterpreter = Interpreter::fromXML(req.content);
 	} else {
@@ -79,9 +80,6 @@ void USCXMLInvoker::invoke(const InvokeRequest& req) {
 	}
 	if (_invokedInterpreter) {
 		DataModel dataModel(_invokedInterpreter.getImpl()->getDataModel());
-		if (dataModel) {
-
-		}
 		_invokedInterpreter.getImpl()->setParentQueue(&_parentQueue);
 		// transfer namespace prefixes
 		_invokedInterpreter.getImpl()->_nsURL = _parentInterpreter->_nsURL;