diff options
Diffstat (limited to 'src/uscxml/plugins')
20 files changed, 7204 insertions, 164 deletions
diff --git a/src/uscxml/plugins/DataModelImpl.h b/src/uscxml/plugins/DataModelImpl.h index a151141..e21be9a 100644 --- a/src/uscxml/plugins/DataModelImpl.h +++ b/src/uscxml/plugins/DataModelImpl.h @@ -43,7 +43,7 @@ class DataModelImpl; */ class USCXML_API DataModelCallbacks { public: - virtual ~DataModelCallbacks() {} ///< silence virtual destructor warning from swig + virtual ~DataModelCallbacks() {} ///< silence virtual destructor warning from swig virtual const std::string& getName() = 0; virtual const std::string& getSessionId() = 0; virtual const std::map<std::string, IOProcessor>& getIOProcessors() = 0; @@ -57,6 +57,7 @@ public: DataModelExtension() : dm(NULL) {} virtual ~DataModelExtension() {} virtual std::string provides() = 0; + virtual Data invoke(const std::string& member, const Data& params) = 0; virtual Data getValueOf(const std::string& member) = 0; virtual void setValueOf(const std::string& member, const Data& data) = 0; DataModelImpl* dm; @@ -117,7 +118,7 @@ public: * @param expr Anything that possibly evaluates to an enumerable object. * @return The number of items in the enumerable object. */ - virtual uint32_t getLength(const std::string& expr) = 0; + virtual uint32_t getLength(const std::string& expr) = 0; /** * Set a given item to the object at a given index for one iteration. diff --git a/src/uscxml/plugins/Factory.cpp b/src/uscxml/plugins/Factory.cpp index 4dabab6..a60fe4c 100644 --- a/src/uscxml/plugins/Factory.cpp +++ b/src/uscxml/plugins/Factory.cpp @@ -56,6 +56,10 @@ # include "uscxml/plugins/datamodel/c89/C89DataModel.h" #endif +#ifdef WITH_DM_PROMELA +# include "uscxml/plugins/datamodel/promela/PromelaDataModel.h" +#endif + #ifdef WITH_INV_SCXML # include "uscxml/plugins/invoker/scxml/USCXMLInvoker.h" @@ -89,66 +93,73 @@ std::string Factory::getDefaultPluginPath() { void Factory::registerPlugins() { #ifdef WITH_IOPROC_SCXML - { - SCXMLIOProcessor* ioProcessor = new SCXMLIOProcessor(); - registerIOProcessor(ioProcessor); - } + { + SCXMLIOProcessor* ioProcessor = new SCXMLIOProcessor(); + registerIOProcessor(ioProcessor); + } #endif #ifdef WITH_IOPROC_BASICHTTP - { - BasicHTTPIOProcessor* ioProcessor = new BasicHTTPIOProcessor(); - registerIOProcessor(ioProcessor); - } + { + BasicHTTPIOProcessor* ioProcessor = new BasicHTTPIOProcessor(); + registerIOProcessor(ioProcessor); + } #endif - + #ifdef WITH_DM_ECMA_V8 - { - V8DataModel* dataModel = new V8DataModel(); - registerDataModel(dataModel); - } + { + V8DataModel* dataModel = new V8DataModel(); + registerDataModel(dataModel); + } #endif #ifdef WITH_DM_ECMA_JSC - { - JSCDataModel* dataModel = new JSCDataModel(); - registerDataModel(dataModel); - } + { + JSCDataModel* dataModel = new JSCDataModel(); + registerDataModel(dataModel); + } #endif - + #ifdef WITH_DM_LUA - { - LuaDataModel* dataModel = new LuaDataModel(); - registerDataModel(dataModel); - } + { + LuaDataModel* dataModel = new LuaDataModel(); + registerDataModel(dataModel); + } #endif #ifdef WITH_DM_C89 - { - C89DataModel* dataModel = new C89DataModel(); - registerDataModel(dataModel); - } + { + C89DataModel* dataModel = new C89DataModel(); + registerDataModel(dataModel); + } #endif - { - NULLDataModel* dataModel = new NULLDataModel(); - registerDataModel(dataModel); - } +#ifdef WITH_DM_PROMELA + { + PromelaDataModel* dataModel = new PromelaDataModel(); + registerDataModel(dataModel); + } +#endif + + { + NULLDataModel* dataModel = new NULLDataModel(); + registerDataModel(dataModel); + } + - #ifdef WITH_INV_SCXML - { - USCXMLInvoker* invoker = new USCXMLInvoker(); - registerInvoker(invoker); - } + { + USCXMLInvoker* invoker = new USCXMLInvoker(); + registerInvoker(invoker); + } #endif - + #ifdef WITH_INV_DIRMON - { - DirMonInvoker* inv = new DirMonInvoker(); - registerInvoker(inv); - } + { + DirMonInvoker* inv = new DirMonInvoker(); + registerInvoker(inv); + } #endif } diff --git a/src/uscxml/plugins/datamodel/CMakeLists.txt b/src/uscxml/plugins/datamodel/CMakeLists.txt index fd08ee0..6409a7a 100644 --- a/src/uscxml/plugins/datamodel/CMakeLists.txt +++ b/src/uscxml/plugins/datamodel/CMakeLists.txt @@ -58,6 +58,17 @@ if (WITH_DM_C89) list (APPEND USCXML_FILES ${C89_DATAMODEL}) endif() +if (WITH_DM_PROMELA) + set(USCXML_DATAMODELS "promela ${USCXML_DATAMODELS}") + # Lua ecmascript datamodel + file(GLOB_RECURSE PROMELA_DATAMODEL + promela/*.cpp + promela/*.c + promela/*.h + ) + list (APPEND USCXML_FILES ${PROMELA_DATAMODEL}) +endif() + if (NOT SWIG_FOUND) message(STATUS "No swig binary found, not generating DOM classes") elseif(SWIG_VERSION VERSION_LESS 3.0.8) diff --git a/src/uscxml/plugins/datamodel/c89/C89DataModel.cpp b/src/uscxml/plugins/datamodel/c89/C89DataModel.cpp index 804b71a..24b9bb1 100644 --- a/src/uscxml/plugins/datamodel/c89/C89DataModel.cpp +++ b/src/uscxml/plugins/datamodel/c89/C89DataModel.cpp @@ -34,13 +34,13 @@ C89DataModel::C89DataModel() { std::shared_ptr<DataModelImpl> C89DataModel::create(DataModelCallbacks* callbacks) { std::shared_ptr<C89DataModel> dm(new C89DataModel()); - PicocInitialise(&dm->_pc, PICOC_STACK_SIZE); - PicocIncludeAllSystemHeaders(&dm->_pc); - return dm; + PicocInitialise(&dm->_pc, PICOC_STACK_SIZE); + PicocIncludeAllSystemHeaders(&dm->_pc); + return dm; } C89DataModel::~C89DataModel() { - PicocCleanup(&_pc); + PicocCleanup(&_pc); } void C89DataModel::addExtension(DataModelExtension* ext) { @@ -60,7 +60,7 @@ bool C89DataModel::isValidSyntax(const std::string& expr) { } uint32_t C89DataModel::getLength(const std::string& expr) { - return 0; + return 0; } void C89DataModel::setForeach(const std::string& item, diff --git a/src/uscxml/plugins/datamodel/c89/C89DataModel.h b/src/uscxml/plugins/datamodel/c89/C89DataModel.h index 30116e1..4e9eef0 100644 --- a/src/uscxml/plugins/datamodel/c89/C89DataModel.h +++ b/src/uscxml/plugins/datamodel/c89/C89DataModel.h @@ -59,7 +59,7 @@ public: virtual std::list<std::string> getNames() { std::list<std::string> names; names.push_back("c89"); - names.push_back("ansi-c"); + names.push_back("ansi-c"); return names; } @@ -86,7 +86,7 @@ public: virtual std::string andExpressions(std::list<std::string>); protected: - Picoc _pc; + Picoc _pc; }; #ifdef BUILD_AS_PLUGINS diff --git a/src/uscxml/plugins/datamodel/ecmascript/JavaScriptCore/JSCDataModel.cpp b/src/uscxml/plugins/datamodel/ecmascript/JavaScriptCore/JSCDataModel.cpp index 05d37d4..bdb8939 100644 --- a/src/uscxml/plugins/datamodel/ecmascript/JavaScriptCore/JSCDataModel.cpp +++ b/src/uscxml/plugins/datamodel/ecmascript/JavaScriptCore/JSCDataModel.cpp @@ -401,23 +401,23 @@ Data JSCDataModel::evalAsData(const std::string& content) { Data JSCDataModel::getAsData(const std::string& content) { // parse as JSON test 578 - Data d = Data::fromJSON(content); - if (!d.empty()) - return d; - - std::string trimmed = boost::trim_copy(content); - if (trimmed.length() > 0) { - if (isNumeric(trimmed.c_str(), 10)) { - d = Data(trimmed, Data::INTERPRETED); - } else if (trimmed.length() >= 2 && - ((trimmed[0] == '"' && trimmed[trimmed.length() - 1] == '"') || - (trimmed[0] == '\'' && trimmed[trimmed.length() - 1] == '\''))) { - d = Data(trimmed.substr(1, trimmed.length() - 2), Data::VERBATIM); - } else { - d = Data(trimmed, Data::INTERPRETED); - } - } - return d; + Data d = Data::fromJSON(content); + if (!d.empty()) + return d; + + std::string trimmed = boost::trim_copy(content); + if (trimmed.length() > 0) { + if (isNumeric(trimmed.c_str(), 10)) { + d = Data(trimmed, Data::INTERPRETED); + } else if (trimmed.length() >= 2 && + ((trimmed[0] == '"' && trimmed[trimmed.length() - 1] == '"') || + (trimmed[0] == '\'' && trimmed[trimmed.length() - 1] == '\''))) { + d = Data(trimmed.substr(1, trimmed.length() - 2), Data::VERBATIM); + } else { + d = Data(trimmed, Data::INTERPRETED); + } + } + return d; } JSValueRef JSCDataModel::getDataAsValue(const Data& data) { diff --git a/src/uscxml/plugins/datamodel/ecmascript/v8/V8DataModel.cpp b/src/uscxml/plugins/datamodel/ecmascript/v8/V8DataModel.cpp index db65ebf..0205674 100644 --- a/src/uscxml/plugins/datamodel/ecmascript/v8/V8DataModel.cpp +++ b/src/uscxml/plugins/datamodel/ecmascript/v8/V8DataModel.cpp @@ -423,23 +423,23 @@ void V8DataModel::setEvent(const Event& event) { } Data V8DataModel::getAsData(const std::string& content) { - Data d = Data::fromJSON(content); - if (!d.empty()) - return d; - - std::string trimmed = boost::trim_copy(content); - if (trimmed.length() > 0) { - if (isNumeric(trimmed.c_str(), 10)) { - d = Data(trimmed, Data::INTERPRETED); - } else if (trimmed.length() >= 2 && - ((trimmed[0] == '"' && trimmed[trimmed.length() - 1] == '"') || - (trimmed[0] == '\'' && trimmed[trimmed.length() - 1] == '\''))) { - d = Data(trimmed.substr(1, trimmed.length() - 2), Data::VERBATIM); - } else { - d = Data(trimmed, Data::INTERPRETED); - } - } - return d; + Data d = Data::fromJSON(content); + if (!d.empty()) + return d; + + std::string trimmed = boost::trim_copy(content); + if (trimmed.length() > 0) { + if (isNumeric(trimmed.c_str(), 10)) { + d = Data(trimmed, Data::INTERPRETED); + } else if (trimmed.length() >= 2 && + ((trimmed[0] == '"' && trimmed[trimmed.length() - 1] == '"') || + (trimmed[0] == '\'' && trimmed[trimmed.length() - 1] == '\''))) { + d = Data(trimmed.substr(1, trimmed.length() - 2), Data::VERBATIM); + } else { + d = Data(trimmed, Data::INTERPRETED); + } + } + return d; } Data V8DataModel::evalAsData(const std::string& content) { diff --git a/src/uscxml/plugins/datamodel/lua/LuaDataModel.cpp b/src/uscxml/plugins/datamodel/lua/LuaDataModel.cpp index ca8cc60..4b7ed67 100644 --- a/src/uscxml/plugins/datamodel/lua/LuaDataModel.cpp +++ b/src/uscxml/plugins/datamodel/lua/LuaDataModel.cpp @@ -79,12 +79,12 @@ static Data getLuaAsData(lua_State* _luaState, const luabridge::LuaRef& lua) { bool isArray = false; bool isMap = false; for (luabridge::Iterator iter (lua); !iter.isNil(); ++iter) { - luabridge::LuaRef luaKey = iter.key(); + luabridge::LuaRef luaKey = iter.key(); luabridge::LuaRef luaVal = *iter; if (luaKey.isString()) { - assert(!isArray); + assert(!isArray); isMap = true; - // luaKey.tostring() is not working?! see issue84 + // luaKey.tostring() is not working?! see issue84 data.compound[luaKey.cast<std::string>()] = getLuaAsData(_luaState, luaVal); } else { assert(!isMap); @@ -335,23 +335,23 @@ Data LuaDataModel::evalAsData(const std::string& content) { data = getLuaAsData(_luaState, luabridge::LuaRef::fromStack(_luaState, -1)); } lua_pop(_luaState, retVals); - return data; + return data; } catch (ErrorEvent e) { - } - - try { + } + + try { // evaluate again without the return() - int retVals = luaEval(_luaState, trimmedExpr); - + int retVals = luaEval(_luaState, trimmedExpr); + if (retVals == 1) { data = getLuaAsData(_luaState, luabridge::LuaRef::fromStack(_luaState, -1)); - } - lua_pop(_luaState, retVals); - return data; + } + lua_pop(_luaState, retVals); + return data; - } catch (ErrorEvent e) { - throw e; // we will assume syntax error and throw - } + } catch (ErrorEvent e) { + throw e; // we will assume syntax error and throw + } return data; } @@ -470,59 +470,59 @@ void LuaDataModel::assign(const std::string& location, const Data& data) { int retVals = luaEval(_luaState, location + " = " + location); lua_pop(_luaState, retVals); - std::list<std::pair<std::string, bool> > idPath; - size_t start = 0; - for (size_t i = 0; i < location.size(); i++) { - if (location[i] == '.' || location[i] == '[') { - idPath.push_back(std::make_pair(location.substr(start, i - start), false)); - start = i + 1; - } else if (location[i] == ']') { - idPath.push_back(std::make_pair(location.substr(start, i - start), true)); - start = i + 1; - } - } - if (start < location.size()) - idPath.push_back(std::make_pair(location.substr(start, location.size() - start), false)); - - if (idPath.size() == 0) - return; - - luabridge::LuaRef lua = getDataAsLua(_luaState, data); - - if (idPath.size() == 1) { - // trivial case where we reference a simple toplevel identifier - luabridge::setGlobal(_luaState, lua, location.c_str()); - - } else { - auto globalId = idPath.front(); - idPath.pop_front(); - - auto field = idPath.back(); - idPath.pop_back(); - - luabridge::LuaRef topValue = luabridge::getGlobal(_luaState, globalId.first.c_str()); - luabridge::LuaRef value = topValue; - - for (auto ident : idPath) { - if (!value.isTable()) - value = luabridge::newTable(_luaState); - - if (ident.second) { - luabridge::LuaRef tmp = value[strTo<long>(ident.first)]; - } else { - luabridge::LuaRef tmp = value[ident]; - value = tmp; - } - } - if (field.second) { - value[strTo<long>(field.first)] = lua; - } else { - value[field.first] = lua; - } - - } - - + std::list<std::pair<std::string, bool> > idPath; + size_t start = 0; + for (size_t i = 0; i < location.size(); i++) { + if (location[i] == '.' || location[i] == '[') { + idPath.push_back(std::make_pair(location.substr(start, i - start), false)); + start = i + 1; + } else if (location[i] == ']') { + idPath.push_back(std::make_pair(location.substr(start, i - start), true)); + start = i + 1; + } + } + if (start < location.size()) + idPath.push_back(std::make_pair(location.substr(start, location.size() - start), false)); + + if (idPath.size() == 0) + return; + + luabridge::LuaRef lua = getDataAsLua(_luaState, data); + + if (idPath.size() == 1) { + // trivial case where we reference a simple toplevel identifier + luabridge::setGlobal(_luaState, lua, location.c_str()); + + } else { + auto globalId = idPath.front(); + idPath.pop_front(); + + auto field = idPath.back(); + idPath.pop_back(); + + luabridge::LuaRef topValue = luabridge::getGlobal(_luaState, globalId.first.c_str()); + luabridge::LuaRef value = topValue; + + for (auto ident : idPath) { + if (!value.isTable()) + value = luabridge::newTable(_luaState); + + if (ident.second) { + luabridge::LuaRef tmp = value[strTo<long>(ident.first)]; + } else { + luabridge::LuaRef tmp = value[ident]; + value = tmp; + } + } + if (field.second) { + value[strTo<long>(field.first)] = lua; + } else { + value[field.first] = lua; + } + + } + + // std::cout << Data::toJSON(evalAsData(location)) << std::endl; } } diff --git a/src/uscxml/plugins/datamodel/promela/PromelaDataModel.cpp b/src/uscxml/plugins/datamodel/promela/PromelaDataModel.cpp new file mode 100644 index 0000000..458e372 --- /dev/null +++ b/src/uscxml/plugins/datamodel/promela/PromelaDataModel.cpp @@ -0,0 +1,728 @@ +/** + * @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 "uscxml/util/String.h" +#include "PromelaDataModel.h" +#include "uscxml/util/DOM.h" + +#include <cctype> + +#include "PromelaParser.h" +#include "parser/promela.tab.hpp" +#include <easylogging++.h> + +#ifdef BUILD_AS_PLUGINS +#include <Pluma/Connector.hpp> +#endif + +#define INVALID_ASSIGNMENT(name) \ +name.compare("_sessionid") == 0 || \ +name.compare("_name") == 0 || \ +name.compare("_ioprocessors") == 0 || \ +name.compare("_event") == 0 + +namespace uscxml { + +#ifdef BUILD_AS_PLUGINS +PLUMA_CONNECTOR +bool pluginConnect(pluma::Host& host) { + host.add( new PromelaDataModelProvider() ); + return true; +} +#endif + +PromelaDataModel::PromelaDataModel() { +} + +PromelaDataModel::~PromelaDataModel() { +} + +std::shared_ptr<DataModelImpl> PromelaDataModel::create(DataModelCallbacks* callbacks) { + std::shared_ptr<PromelaDataModel> dm(new PromelaDataModel()); + + dm->_callbacks = callbacks; + + // session id + Data sessionId; + sessionId.compound["type"] = Data("string", Data::VERBATIM); + sessionId.compound["value"] = Data(callbacks->getSessionId(), Data::VERBATIM); + dm->_variables["_sessionid"] = sessionId; + + // name + Data name; + name.compound["type"] = Data("string", Data::VERBATIM); + name.compound["value"] = Data(callbacks->getName(), Data::VERBATIM); + dm->_variables["_name"] = name; + + // ioprocessors + Data ioProcs; + ioProcs.compound["type"] = Data("compound", Data::VERBATIM); + + std::map<std::string, IOProcessor> ioProcessors = callbacks->getIOProcessors(); + for (std::map<std::string, IOProcessor>::iterator iter = ioProcessors.begin(); iter != ioProcessors.end(); iter++) { + ioProcs.compound["value"].compound[iter->first] = iter->second.getDataModelVariables(); + } + dm->_variables["_ioprocessors"] = ioProcs; + + dm->_lastMType = 0; + return dm; +} + + +void PromelaDataModel::setEvent(const Event& event) { + Data variable; + variable.compound["type"] = Data("compound", Data::VERBATIM); + variable.compound["value"].compound["name"] = Data(event.name, Data::VERBATIM); + variable.compound["value"].compound["origin"] = Data(event.origin, Data::VERBATIM); + variable.compound["value"].compound["origintype"] = Data(event.origintype, Data::VERBATIM); + variable.compound["value"].compound["invokeid"] = Data(event.invokeid, Data::VERBATIM); + if (event.hideSendId) { + variable.compound["value"].compound["sendid"] = Data("", Data::VERBATIM); + } else { + variable.compound["value"].compound["sendid"] = Data(event.sendid, Data::VERBATIM); + } + switch (event.eventType) { + case Event::PLATFORM: + variable.compound["value"].compound["type"] = Data("platform", Data::VERBATIM); + break; + case Event::INTERNAL: + variable.compound["value"].compound["type"] = Data("internal", Data::VERBATIM); + break; + case Event::EXTERNAL: + variable.compound["value"].compound["type"] = Data("external", Data::VERBATIM); + break; + default: + variable.compound["value"].compound["type"] = Data("invalid", Data::VERBATIM); + break; + } + + if (false) { +#if 0 + else if (event.dom) { + // no support + } else if (event.content.length() > 0) { + // _event.data is a string or JSON + Data json = Data::fromJSON(event.content); + if (!json.empty()) { + variable.compound["value"].compound["data"] = json; + } else { + if (isNumeric(event.content.c_str(), 10)) { + variable.compound["value"].compound["data"] = Data(event.content, Data::INTERPRETED); + } else { + variable.compound["value"].compound["data"] = Data(spaceNormalize(event.content), Data::VERBATIM); + } + } +#endif + } else { + // _event.data is KVP + if (!event.data.empty()) { + variable.compound["value"].compound["data"] = event.data; + } else { + // test 343 / test 488 + variable.compound["value"].compound["data"]; + } + + for (Event::params_t::const_iterator start = event.params.begin(), end = event.params.end(); + start != end; start = event.params.upper_bound(start->first)) { + // only set first param key + if (isNumeric(start->second.atom.c_str(), 10)) { + variable.compound["value"].compound["data"].compound[start->first] = strTo<int>(start->second.atom); + } else { + variable.compound["value"].compound["data"].compound[start->first] = start->second; + } + } + + for (Event::namelist_t::const_iterator iter = event.namelist.begin(); iter != event.namelist.end(); iter++) { + if (isNumeric(iter->second.atom.c_str(), 10)) { + variable.compound["value"].compound["data"].compound[iter->first] = strTo<int>(iter->second.atom); + } else { + variable.compound["value"].compound["data"].compound[iter->first] = iter->second; + } + } + } + + // iterate all data elements and adapt type for int if atom is integer + adaptType(variable.compound["value"].compound["data"]); + + _variables["_event"] = variable; + } + + void PromelaDataModel::adaptType(Data& data) { + if (data.atom.length() > 0 && isInteger(data.atom.c_str(), 10)) { + data.type = Data::INTERPRETED; + return; + } + + if (data.array.size() > 0) { + for (std::list<Data>::iterator iter = data.array.begin(); iter != data.array.end(); iter++) { + adaptType(*iter); + } + return; + } + + if (data.compound.size() > 0) { + for (std::map<std::string, Data>::iterator iter = data.compound.begin(); iter != data.compound.end(); iter++) { + adaptType(iter->second); + } + return; + } + + } + + bool PromelaDataModel::isValidSyntax(const std::string& expr) { + try { + PromelaParser parser(expr); + } catch (Event e) { + LOG(ERROR) << e << std::endl; + return false; + } + return true; + } + + uint32_t PromelaDataModel::getLength(const std::string& expr) { + if (!isDeclared(expr)) { + ERROR_EXECUTION_THROW("Variable '" + expr + "' was not declared"); + } + + if (!_variables[expr].hasKey("size")) { + ERROR_EXECUTION_THROW("Variable '" + expr + "' is no array"); + } + + return strTo<int>(_variables[expr]["size"].atom); + } + + void PromelaDataModel::setForeach(const std::string& item, + const std::string& array, + const std::string& index, + uint32_t iteration) { + // assign array element to item + std::stringstream ss; + ss << array << "[" << iteration << "]"; + + PromelaParser itemParser(item, 1, PromelaParser::PROMELA_EXPR); + if (itemParser.ast->type != PML_NAME) + ERROR_EXECUTION_THROW("Expression '" + item + "' is no valid item"); + + PromelaParser arrayParser(ss.str(), 1, PromelaParser::PROMELA_EXPR); + + setVariable(itemParser.ast, getVariable(arrayParser.ast)); + + if (index.length() > 0) { + PromelaParser indexParser(index, 1, PromelaParser::PROMELA_EXPR); + setVariable(indexParser.ast, iteration); + } + + } + + bool PromelaDataModel::evalAsBool(const std::string& expr) { + PromelaParser parser(expr, 1, PromelaParser::PROMELA_EXPR); +// parser.dump(); + Data tmp = evaluateExpr(parser.ast); + + if (tmp.atom.compare("false") == 0) + return false; + if (tmp.atom.compare("0") == 0) + return false; + return true; + } + + Data PromelaDataModel::evalAsData(const std::string& expr) { + PromelaParser parser(expr); + return evaluateExpr(parser.ast); + } + + Data PromelaDataModel::getAsData(const std::string& content) { + return evalAsData(content); + } + + void PromelaDataModel::evaluateDecl(const std::string& expr) { + PromelaParser parser(expr, 1, PromelaParser::PROMELA_DECL); + evaluateDecl(parser.ast); + } + + Data PromelaDataModel::evaluateExpr(const std::string& expr) { + PromelaParser parser(expr, 1, PromelaParser::PROMELA_EXPR); + return evaluateExpr(parser.ast); + } + + void PromelaDataModel::evaluateStmnt(const std::string& expr) { + PromelaParser parser(expr, 1, PromelaParser::PROMELA_STMNT); + evaluateStmnt(parser.ast); + } + + void PromelaDataModel::evaluateDecl(void* ast) { + PromelaParserNode* node = (PromelaParserNode*)ast; +// node->dump(); + if (false) { + } else if (node->type == PML_DECL) { + std::list<PromelaParserNode*>::iterator opIter = node->operands.begin(); + PromelaParserNode* vis = *opIter++; + PromelaParserNode* type = *opIter++; + PromelaParserNode* varlist = *opIter++; + + for (std::list<PromelaParserNode*>::iterator nameIter = varlist->operands.begin(); + nameIter != varlist->operands.end(); + nameIter++) { + Data variable; + variable.compound["vis"] = Data(vis->value, Data::VERBATIM); + variable.compound["type"] = Data(type->value, Data::VERBATIM); + + if (false) { + } else if ((*nameIter)->type == PML_NAME) { + // plain variables without initial assignment + + if (type->value == "mtype") { + variable.compound["value"] = Data(_lastMType++, Data::INTERPRETED); + } else { + variable.compound["value"] = Data(0, Data::INTERPRETED); + } + _variables.compound[(*nameIter)->value] = variable; + + } else if ((*nameIter)->type == PML_ASGN) { + // initially assigned variables + + std::list<PromelaParserNode*>::iterator opIterAsgn = (*nameIter)->operands.begin(); + PromelaParserNode* name = *opIterAsgn++; + PromelaParserNode* expr = *opIterAsgn++; + + try { + variable.compound["value"] = evaluateExpr(expr); + } catch(uscxml::Event e) { + // test277, declare and throw + _variables.compound[name->value] = variable; + throw e; + } + + assert(opIterAsgn == (*nameIter)->operands.end()); + _variables.compound[name->value] = variable; + } else if ((*nameIter)->type == PML_VAR_ARRAY) { + // variable arrays + + std::list<PromelaParserNode*>::iterator opIterAsgn = (*nameIter)->operands.begin(); + PromelaParserNode* name = *opIterAsgn++; + int size = dataToInt(evaluateExpr(*opIterAsgn++)); + + variable.compound["size"] = size; + for (size_t i = 0; i < size; i++) { + variable.compound["value"].array.push_back(Data(0, Data::INTERPRETED)); + } + + assert(opIterAsgn == (*nameIter)->operands.end()); + _variables.compound[name->value] = variable; + + } else { + ERROR_EXECUTION_THROW("Declaring variables via " + PromelaParserNode::typeToDesc((*nameIter)->type) + " not implemented"); + } + } + assert(opIter == node->operands.end()); + } else if (node->type == PML_DECLLIST) { + for (std::list<PromelaParserNode*>::iterator declIter = node->operands.begin(); + declIter != node->operands.end(); + declIter++) { + evaluateDecl(*declIter); + } + } else { + node->dump(); + ERROR_EXECUTION_THROW("Declaring variables via " + PromelaParserNode::typeToDesc(node->type) + " not implemented"); + } + } + + int PromelaDataModel::dataToInt(const Data& data) { + if (data.type != Data::INTERPRETED) + ERROR_EXECUTION_THROW("Operand is not integer"); + int value = strTo<int>(data.atom); + if (data.atom.compare(toStr(value)) != 0) + ERROR_EXECUTION_THROW("Operand is not integer"); + return value; + } + + bool PromelaDataModel::dataToBool(const Data& data) { + if (data.atom.size() == 0) // empty string or undefined + return false; + + if (data.type == Data::VERBATIM) { + // non-empty string is true + return true; + } else { + if (data.atom.compare("true") == 0) { + // boolean true is true + return true; + } else if (data.atom.compare("false") == 0) { + return false; + } else if (dataToInt(data) != 0) { + return true; // non zero values are true + } + } + return false; + } + + Data PromelaDataModel::evaluateExpr(void* ast) { + PromelaParserNode* node = (PromelaParserNode*)ast; + std::list<PromelaParserNode*>::iterator opIter = node->operands.begin(); + switch (node->type) { + case PML_CONST: + if (iequals(node->value, "false")) + return Data(false); + if (iequals(node->value, "true")) + return Data(true); + return strTo<int>(node->value); + case PML_NAME: + case PML_VAR_ARRAY: + case PML_CMPND: + return getVariable(node); + case PML_STRING: { + std::string stripped = node->value.substr(1, node->value.size() - 2); + return Data(stripped, Data::VERBATIM); +// return Data(node->value, Data::INTERPRETED); + } + case PML_PLUS: + return dataToInt(evaluateExpr(*opIter++)) + dataToInt(evaluateExpr(*opIter++)); + case PML_MINUS: + return dataToInt(evaluateExpr(*opIter++)) - dataToInt(evaluateExpr(*opIter++)); + case PML_DIVIDE: + return dataToInt(evaluateExpr(*opIter++)) / dataToInt(evaluateExpr(*opIter++)); + case PML_MODULO: + return dataToInt(evaluateExpr(*opIter++)) % dataToInt(evaluateExpr(*opIter++)); + case PML_EQ: { + PromelaParserNode* lhs = *opIter++; + PromelaParserNode* rhs = *opIter++; + + Data left = evaluateExpr(lhs); + Data right = evaluateExpr(rhs); + + if (left == right) // overloaded operator== + return Data(true); + + // literal strings or strings in variables + if ((lhs->type == PML_STRING || rhs->type == PML_STRING) + || (left.type == Data::VERBATIM && right.type == Data::VERBATIM)) { + return (left.atom.compare(right.atom) == 0 ? Data(true) : Data(false)); + } + return dataToInt(left) == dataToInt(right); + } + case PML_NEG: + return !dataToBool(evaluateExpr(*opIter++)); + case PML_LT: + return dataToInt(evaluateExpr(*opIter++)) < dataToInt(evaluateExpr(*opIter++)); + case PML_LE: + return dataToInt(evaluateExpr(*opIter++)) <= dataToInt(evaluateExpr(*opIter++)); + case PML_GT: + return dataToInt(evaluateExpr(*opIter++)) > dataToInt(evaluateExpr(*opIter++)); + case PML_GE: + return dataToInt(evaluateExpr(*opIter++)) >= dataToInt(evaluateExpr(*opIter++)); + case PML_TIMES: + return dataToInt(evaluateExpr(*opIter++)) * dataToInt(evaluateExpr(*opIter++)); + case PML_LSHIFT: + return dataToInt(evaluateExpr(*opIter++)) << dataToInt(evaluateExpr(*opIter++)); + case PML_RSHIFT: + return dataToInt(evaluateExpr(*opIter++)) >> dataToInt(evaluateExpr(*opIter++)); + case PML_AND: + case PML_OR: { + PromelaParserNode* lhs = *opIter++; + PromelaParserNode* rhs = *opIter++; + +// std::cout << "-----" << std::endl; +// lhs->dump(); +// rhs->dump(); + + Data left = evaluateExpr(lhs); + Data right = evaluateExpr(rhs); + + bool truthLeft = dataToBool(left); + bool truthRight = dataToBool(right); + + if (node->type == PML_AND) { + return truthLeft && truthRight; + } else { + return truthLeft || truthRight; + } + } + default: + ERROR_EXECUTION_THROW("Support for " + PromelaParserNode::typeToDesc(node->type) + " expressions not implemented"); + } + return 0; + } + + void PromelaDataModel::evaluateStmnt(void* ast) { + PromelaParserNode* node = (PromelaParserNode*)ast; + std::list<PromelaParserNode*>::iterator opIter = node->operands.begin(); + switch (node->type) { + case PML_ASGN: { + PromelaParserNode* name = *opIter++; + PromelaParserNode* expr = *opIter++; + setVariable(name, evaluateExpr(expr)); + break; + } + case PML_STMNT: { + while(opIter != node->operands.end()) { + evaluateStmnt(*opIter++); + } + break; + } + case PML_INCR: { + PromelaParserNode* name = *opIter++; + setVariable(name, strTo<long>(getVariable(name)) + 1); + break; + } + case PML_DECR: { + PromelaParserNode* name = *opIter++; + setVariable(name, strTo<long>(getVariable(name)) - 1); + break; + } + default: + node->dump(); + ERROR_EXECUTION_THROW("No support for " + PromelaParserNode::typeToDesc(node->type) + " statement implemented"); + } + } + + + void PromelaDataModel::setVariable(void* ast, const Data& value) { + PromelaParserNode* node = (PromelaParserNode*)ast; + + if (INVALID_ASSIGNMENT(node->value)) { + ERROR_EXECUTION_THROW("Cannot assign to " + node->value); + } + +// if (_variables.compound.find(name->value) == _variables.compound.end()) { +// // declare implicitly / convenience +// evaluateDecl(ast); +// } + + switch (node->type) { + case PML_VAR_ARRAY: { + std::list<PromelaParserNode*>::iterator opIter = node->operands.begin(); + + PromelaParserNode* name = *opIter++; + PromelaParserNode* expr = *opIter++; + + // is the location an array? + if (!_variables[name->value].hasKey("size")) { + ERROR_EXECUTION_THROW("Variable " + name->value + " is no array"); + } + + // is the array large enough? + int index = dataToInt(evaluateExpr(expr)); + if (strTo<int>(_variables[name->value]["size"].atom) <= index) { + ERROR_EXECUTION_THROW("Index " + toStr(index) + " in array " + name->value + "[" + _variables[name->value]["size"].atom + "] is out of bounds"); + } + + _variables.compound[name->value].compound["value"][index] = value; + + break; + } + case PML_NAME: { + // location is an array, but no array was passed + if (_variables[node->value].hasKey("size")) { + if (value.compound.size() > 0 || value.atom.size() > 0) + ERROR_EXECUTION_THROW("Variable " + node->value + " is an array"); + + if (strTo<size_t>(_variables[node->value].compound["size"].atom) < value.array.size()) + ERROR_EXECUTION_THROW("Array assigned to " + node->value + " is too large"); + } + + _variables.compound[node->value].compound["value"] = value; + break; + } + case PML_CMPND: { + std::list<PromelaParserNode*>::iterator opIter = node->operands.begin(); + PromelaParserNode* name = *opIter++; + + // location is no array + if (_variables[name->value].hasKey("size")) { + ERROR_EXECUTION_THROW("Variable " + name->value + " is an array"); + } + +// std::cout << Data::toJSON(_variables) << std::endl;; + + Data* var = &_variables[name->value].compound["value"]; + var->compound["type"] = Data("compound", Data::VERBATIM); + var->compound["vis"] = Data("", Data::VERBATIM); + + while(opIter != node->operands.end()) { + name = *opIter; + opIter++; + var = &(var->compound[name->value]); + } + *var = value; + + break; + } + default: + node->dump(); + ERROR_EXECUTION_THROW("No support for " + PromelaParserNode::typeToDesc(node->type) + " variables implemented"); + break; + } + +// std::cout << Data::toJSON(_variables) << std::endl; + } + + Data PromelaDataModel::getVariable(void* ast) { + PromelaParserNode* node = (PromelaParserNode*)ast; +// node->dump(); + + std::list<PromelaParserNode*>::iterator opIter = node->operands.begin(); + switch(node->type) { + case PML_NAME: + if (_variables.compound.find(node->value) == _variables.compound.end()) { + ERROR_EXECUTION_THROW("No variable " + node->value + " was declared"); + } +// if (_variables[node->value].compound.find("size") != _variables[node->value].compound.end()) { +// ERROR_EXECUTION_THROW("Type error: Variable " + node->value + " is an array"); +// } + return _variables[node->value]["value"]; + case PML_VAR_ARRAY: { + PromelaParserNode* name = *opIter++; + PromelaParserNode* expr = *opIter++; + int index = dataToInt(evaluateExpr(expr)); + + if (_variables.compound.find(name->value) == _variables.compound.end()) { + ERROR_EXECUTION_THROW("No variable " + name->value + " was declared"); + } + + if (!_variables[name->value].hasKey("size")) { + ERROR_EXECUTION_THROW("Variable " + name->value + " is no array"); + } + + if (strTo<int>(_variables[name->value]["size"].atom) <= index) { + ERROR_EXECUTION_THROW("Index " + toStr(index) + " in array " + name->value + "[" + _variables[name->value]["size"].atom + "] is out of bounds"); + } + return _variables.compound[name->value].compound["value"][index]; + } + case PML_CMPND: { +// node->dump(); +// std::cout << Data::toJSON(_variables["_event"]); + std::stringstream idPath; + PromelaParserNode* name = *opIter++; + + // special case for _x variables + if (name->value.compare("_x") == 0) { + PromelaParserNode* what = *opIter++; + + if (what->type == PML_VAR_ARRAY) { + if (what->operands.size() == 2) { + std::string arrName = what->operands.front()->value; + std::string index = what->operands.back()->value; + + if (what->operands.back()->type == PML_STRING) { + index = index.substr(1, index.size() - 2); // remove quotes + } + + if (arrName.compare("states") == 0) { + return Data(_callbacks->isInState(index)); + } + } + } + ERROR_EXECUTION_THROW("No variable " + name->value + " was declared"); + } + + if (_variables.compound.find(name->value) == _variables.compound.end()) { + ERROR_EXECUTION_THROW("No variable " + name->value + " was declared"); + } + + Data currData = _variables.compound[name->value]["value"]; + idPath << name->value; + while(opIter != node->operands.end()) { + std::string key = (*opIter)->value; + idPath << "." << key; + if (currData.compound.find(key) == currData.compound.end()) { + ERROR_EXECUTION_THROW("No variable " + idPath.str() + " was declared"); + } + Data tmp = currData.compound[key]; + currData = tmp; + + opIter++; + } + return currData; + } + default: + ERROR_EXECUTION_THROW("Retrieving value of " + PromelaParserNode::typeToDesc(node->type) + " variable not implemented"); + } + return 0; + } + + std::string PromelaDataModel::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 PromelaDataModel::assign(const std::string& location, const Data& data) { + // used for e.g. to assign command line parameters and idlocation + PromelaParser parser(location); + setVariable(parser.ast, data); + } + + void PromelaDataModel::init(const std::string& location, const Data& data) { + assign(location, data); + } + + bool PromelaDataModel::isDeclared(const std::string& expr) { + PromelaParser parser(expr); +// parser.dump(); + if (parser.ast->type == PML_VAR_ARRAY) + return _variables.compound.find(parser.ast->operands.front()->value) != _variables.compound.end(); + + if (parser.ast->type == PML_CMPND) { + // JSON declaration + std::list<PromelaParserNode*>::iterator opIter = parser.ast->operands.begin(); + Data* var = &_variables; + + while(opIter != parser.ast->operands.end()) { + std::string name = (*opIter)->value; + opIter++; + if (var->compound.find(name) != var->compound.end()) { + var = &(var->compound.at(name)); + } else if (var->compound.find("value") != var->compound.end() && var->compound.at("value").compound.find(name) != var->compound.at("value").compound.end()) { + var = &(var->compound.at("value").compound.at(name)); + } else { + return false; + } + } + return true; + + } + + return _variables.compound.find(expr) != _variables.compound.end(); + } + + void PromelaDataModel::addExtension(DataModelExtension* ext) { + ERROR_EXECUTION_THROW("Extensions unimplemented in promela datamodel"); + } + + +} diff --git a/src/uscxml/plugins/datamodel/promela/PromelaDataModel.h b/src/uscxml/plugins/datamodel/promela/PromelaDataModel.h new file mode 100644 index 0000000..2c1f58d --- /dev/null +++ b/src/uscxml/plugins/datamodel/promela/PromelaDataModel.h @@ -0,0 +1,102 @@ +/** + * @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/plugins/DataModelImpl.h" +#include <list> + +#ifdef BUILD_AS_PLUGINS +#include "uscxml/plugins/Plugins.h" +#endif + +namespace uscxml { + +class PromelaDataModel : public DataModelImpl { +public: + PromelaDataModel(); + virtual ~PromelaDataModel(); + virtual std::shared_ptr<DataModelImpl> create(DataModelCallbacks* callbacks); + + virtual std::list<std::string> getNames() { + std::list<std::string> names; + names.push_back("promela"); + return names; + } + + virtual void addExtension(DataModelExtension* ext); + + virtual bool isValidSyntax(const std::string& expr); + + virtual void setEvent(const Event& event); + + // foreach + 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 bool evalAsBool(const std::string& expr); + virtual Data evalAsData(const std::string& expr); + virtual Data getAsData(const std::string& content); + + virtual bool isDeclared(const std::string& expr); + + virtual void assign(const std::string& location, const Data& data); + virtual void init(const std::string& location, const Data& data); + + virtual std::string andExpressions(std::list<std::string>); + +protected: + + int dataToInt(const Data& data); + bool dataToBool(const Data& data); + + void evaluateDecl(void* ast); + Data evaluateExpr(void* ast); + void evaluateStmnt(void* ast); + + void evaluateDecl(const std::string& expr); + Data evaluateExpr(const std::string& expr); + void evaluateStmnt(const std::string& expr); + + void setVariable(void* ast, const Data& value); + Data getVariable(void* ast); + + void adaptType(Data& data); + + int _lastMType; + + Event _event; + std::string _name; + std::string _sessionId; + + Data _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..3467598 --- /dev/null +++ b/src/uscxml/plugins/datamodel/promela/PromelaParser.cpp @@ -0,0 +1,298 @@ +/** + * @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 "PromelaParser.h" +#include "parser/promela.tab.hpp" +#include "uscxml/messages/Event.h" + +#include <iostream> + +struct yy_buffer_state; +typedef yy_buffer_state *YY_BUFFER_STATE; +extern YY_BUFFER_STATE promela__scan_buffer(char *, size_t, void*); +void promela__delete_buffer(YY_BUFFER_STATE, void*); +YY_BUFFER_STATE promela__scan_string (const char * yystr , void*); + + +extern int promela_lex (PROMELA_STYPE* yylval_param, PROMELA_LTYPE* yylloc_param, void* yyscanner); +int promela_lex_init (void**); +int promela_lex_destroy (void*); + +void promela_error (void* yylloc_param, uscxml::PromelaParser* ctx, void* yyscanner, const char* err) { + PROMELA_LTYPE* yylloc = (PROMELA_LTYPE*)yylloc_param; + // mark as pending exception as we cannot throw from constructor and have the destructor called + ERROR_EXECUTION(excEvent, err); + excEvent.data.compound["line"] = uscxml::Data(yylloc->first_line, uscxml::Data::VERBATIM); + excEvent.data.compound["col"] = uscxml::Data(yylloc->first_column, uscxml::Data::VERBATIM); + + std::stringstream ssUnderline; + for (size_t i = 0; i < yylloc->first_column; i++) + ssUnderline << " "; + ssUnderline << "^"; + excEvent.data.compound["sourcemark"] = uscxml::Data(ssUnderline.str(), uscxml::Data::VERBATIM); + + ctx->pendingException = excEvent; +} + +namespace uscxml { + +PromelaParser::PromelaParser(const std::string& expr) { + init(expr); +} + +PromelaParser::PromelaParser(const std::string& expr, int nrArgs, ...) { + init(expr); + + if (nrArgs == 0) + return; + + std::stringstream errSS; + std::string seperator; + errSS << "Promela syntax type mismatch: Expected {"; + + va_list ap; + va_start(ap, nrArgs); + for(int i = 1; i <= nrArgs; i++) { + int expectedType = va_arg(ap, int); + if (type == expectedType) + return; + errSS << seperator << typeToDesc(expectedType); + seperator = ", "; + } + errSS << "} but got " << typeToDesc(type); + ERROR_EXECUTION_THROW(errSS.str()); +} + +void PromelaParser::init(const std::string& expr) { + ast = NULL; + parseInCompound = 0; + input_length = expr.length() + 2; // 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); + buffer = promela__scan_string(input, scanner); + // buffer = promela__scan_buffer(input, input_length, scanner); + promela_parse(this, scanner); + if (pendingException.name.size() > 0) { + // parsing failed in promela_error + destroy(); + pendingException.data.compound["sourceline"] = Data(expr, Data::VERBATIM); + throw pendingException; + } +} + +void PromelaParser::destroy() { + if (ast) + delete(ast); + free(input); + promela__delete_buffer((YY_BUFFER_STATE)buffer, scanner); + promela_lex_destroy(scanner); +} + +PromelaParser::~PromelaParser() { + destroy(); +} + +std::string PromelaParser::typeToDesc(int type) { + switch (type) { + case PROMELA_EXPR: + return "expression"; + case PROMELA_DECL: + return "declarations"; + case PROMELA_STMNT: + return "statements"; + default: + break; + } + return ""; +} + +PromelaParserNode::~PromelaParserNode() { + while(operands.size() > 0) { + delete operands.front(); + operands.pop_front(); + } + if (loc) + free(loc); +} + +PromelaParserNode* PromelaParser::node(int type, int nrArgs, ...) { + PromelaParserNode* newNode = new PromelaParserNode(); + + newNode->type = type; + va_list ap; + va_start(ap, nrArgs); + for(int i = 1; i <= nrArgs; i++) { + newNode->operands.push_back(va_arg(ap, PromelaParserNode*)); + newNode->operands.back()->parent = newNode; + } + return newNode; +} + +PromelaParserNode* PromelaParser::value(int type, void* location, const char* value) { + PromelaParserNode* newNode = new PromelaParserNode(); + + if (location) { + PROMELA_LTYPE* location_param = (PROMELA_LTYPE*)location; + newNode->loc = (PromelaParserNode::Location*)malloc(sizeof(PromelaParserNode::Location)); + newNode->loc->firstCol = location_param->first_column; + newNode->loc->firstLine = location_param->first_line; + newNode->loc->lastCol = location_param->last_column; + newNode->loc->lastLine = location_param->last_line; + } + + newNode->value = value; + newNode->type = type; + return newNode; +} + + +void PromelaParser::dump() { + switch (type) { + case PROMELA_EXPR: + 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; + } + ast->dump(); +} + + +void PromelaParserNode::merge(PromelaParserNode* node) { + for (std::list<PromelaParserNode*>::iterator iter = node->operands.begin(); + iter != node->operands.end(); iter++) { + operands.push_back(*iter); + (*iter)->parent = this; + } + node->operands.clear(); +} + +void PromelaParserNode::push(PromelaParserNode* node) { + node->parent = this; + operands.push_back(node); +} + +void PromelaParserNode::dump(int indent) { + std::string padding; + for (size_t i = 0; i < indent; i++) { + padding += " "; + } + std::cout << padding << typeToDesc(type) << ": " << value; + if (loc != NULL) { + std::cout << " (" << loc->firstLine << ":" << loc->firstCol << ")-(" << loc->lastLine << ":" << loc->lastCol << ")"; + } + std::cout << std::endl; + for (std::list<PromelaParserNode*>::iterator iter = operands.begin(); + iter != operands.end(); iter++) { + (*iter)->dump(indent + 1); + } +} + +std::string PromelaParserNode::typeToDesc(int type) { + switch(type) { + case PML_PLUS: + return "PLUS"; + case PML_MINUS: + return "MINUS"; + case PML_TIMES: + return "TIMES"; + case PML_DIVIDE: + return "DIVIDE"; + case PML_MODULO: + return "MODULO"; + case PML_BITAND: + return "BITAND"; + case PML_BITXOR: + return "BITXOR"; + case PML_BITOR: + return "BITOR"; + case PML_GT: + return "GT"; + case PML_LT: + return "LT"; + case PML_GE: + return "GE"; + case PML_LE: + return "LE"; + case PML_EQ: + return "EQ"; + case PML_NE: + return "NE"; + case PML_AND: + return "AND"; + case PML_OR: + return "OR"; + case PML_LSHIFT: + return "LSHIFT"; + case PML_RSHIFT: + return "RSHIFT"; + case PML_NEG: + return "NEG"; + case PML_ASGN: + return "ASGN"; + case PML_INCR: + return "INCR"; + case PML_DECR: + return "DECR"; + case PML_VAR_ARRAY: + return "VAR_ARRAY"; + case PML_DECL: + return "DECL"; + case PML_STMNT: + return "STMNT"; + case PML_TYPE: + return "TYPE"; + case PML_NAME: + return "NAME"; + case PML_CONST: + return "CONST"; + case PML_PRINT: + return "PRINT"; + case PML_SHOW: + return "SHOW"; + case PML_EXPR: + return "EXPR"; + case PML_VARLIST: + return "VARLIST"; + case PML_DECLLIST: + return "DECLLIST"; + case PML_NAMELIST: + return "NAMELIST"; + case PML_STRING: + return "STRING"; + case PML_TYPEDEF: + return "TYPEDEF"; + case PML_CMPND: + return "CMPND"; + case PML_ASSERT: + return "ASSERT"; + + 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..51a2111 --- /dev/null +++ b/src/uscxml/plugins/datamodel/promela/PromelaParser.h @@ -0,0 +1,106 @@ +/** + * @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 + */ + +// bison -v promela.ypp && flex promela.l + +#ifndef PROMELA_H_9AB78YB1 +#define PROMELA_H_9AB78YB1 + +#include <stdlib.h> +//#include <stdarg.h> +#include <cstdarg> +#include <string> +#include <list> + +#include "uscxml/messages/Event.h" + +namespace uscxml { + +class PromelaParser; + +class PromelaParserNode { +public: + struct Location { + int firstLine; + int firstCol; + int lastLine; + int lastCol; + }; + + PromelaParserNode() : type(0), parent(NULL), loc(NULL) {} + virtual ~PromelaParserNode(); + + void merge(PromelaParserNode* node); + void push(PromelaParserNode* node); + void dump(int indent = 0); + + static std::string typeToDesc(int type); + + int type; + std::string value; + std::list<PromelaParserNode*> operands; + PromelaParserNode* parent; + Location* loc; +}; + +class PromelaParser { +public: + enum Type { + PROMELA_EXPR, + PROMELA_DECL, + PROMELA_STMNT + }; + + static std::string typeToDesc(int type); + + PromelaParser() : ast(NULL) {} + PromelaParser(const std::string& expr); + PromelaParser(const std::string& expr, int nrArgs, ...); + virtual ~PromelaParser(); + + virtual PromelaParserNode* node(int type, int nrArgs, ...); + virtual PromelaParserNode* value(int type, void* location, const char* value); + void dump(); + + int parseInCompound; + + PromelaParserNode* ast; + Type type; + + Event pendingException; + operator bool() const { + return ast != NULL; + } + +protected: + + void init(const std::string& expr); + void destroy(); + + void* buffer; + void* scanner; + char* input; + size_t input_length; +}; + +} + +void promela_error (void* yylloc_param, uscxml::PromelaParser* ctx, void* yyscanner, const char* err); + +#endif /* end of include guard: PROMELA_H_9AB78YB1 */ diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.l b/src/uscxml/plugins/datamodel/promela/parser/promela.l new file mode 100644 index 0000000..1edc625 --- /dev/null +++ b/src/uscxml/plugins/datamodel/promela/parser/promela.l @@ -0,0 +1,117 @@ +/* see: http://www.phpcompiler.org/articles/reentrantparser.html */ +/* see: http://spinroot.com/spin/Man/operators.html */ + + +%option yylineno +%option reentrant +%option bison-bridge +%option prefix="promela_" +%option outfile="promela.lex.yy.cpp" +%option noyywrap +%option debug +%option never-interactive nounistd +%option bison-locations + +%{ + +#include "../PromelaParser.h" +#include "promela.tab.hpp" +#define YYSTYPE PROMELA_STYPE +#define YYLTYPE PROMELA_LTYPE +#define YY_USER_INIT \ + yycolumn = yylloc->first_line = yylloc->first_column = 0; \ + yylineno = yylloc->last_line = yylloc->last_column = 0; \ + +//int yycolumn = 1; + +#define YY_USER_ACTION \ +{ \ + yylloc->first_line = yylineno; \ + yylloc->first_column = yycolumn; \ + yylloc->last_column = yycolumn + yyleng; \ + yylloc->last_line = yylineno; \ + yycolumn = yycolumn + yyleng; \ +} + +%} + +DIGIT [0-9] +ID [_a-zA-Z][_a-zA-Z0-9]* +L [a-zA-Z_] + +%% + +\/\*([^*]|\*[^/])*\*+\/ /* multiline comments */ + +bit|bool|byte|int|mtype|short|unsigned|string|auto { + yylval->value = strdup(yytext); + return PML_TYPE; +} + +len { return PML_LEN; } +false|skip|true { yylval->value = strdup(yytext); return PML_CONST; } +printf { return PML_PRINT; } +typedef { return PML_TYPEDEF; } +assert { return PML_ASSERT; } + +"!" { return PML_NEG; } +"~" { return PML_COMPL; } +"++" { return PML_INCR; } +"--" { return PML_DECR; } + +"*" { return PML_TIMES; } +"/" { return PML_DIVIDE; } +"%" { return PML_MODULO; } + +"+" { return PML_PLUS; } +"-" { return PML_MINUS; } + +"<<" { return PML_LSHIFT; } +">>" { return PML_RSHIFT; } + +"<=" { return PML_LE; } +">=" { return PML_GE; } +"<" { return PML_LT; } +">" { return PML_GT; } + +"!=" { return PML_NE; } +"==" { return PML_EQ; } + +"&" { return PML_BITAND; } +"^" { return PML_BITXOR; } +"|" { return PML_BITOR; } + + +"&&" { return PML_AND; } +"||" { return PML_OR; } + +"." { return PML_DOT; } +"," { return PML_COMMA; } +";" { return PML_SEMI; } + +"(" { return '('; } +")" { return ')'; } + +"[" { return '['; } +"]" { return ']'; } + +"{" { return '{'; } +"}" { return '}'; } + +"=" { return PML_ASGN; } + +L?\"(\\.|[^\\"])*\" { yylval->value = strdup(yytext); return(PML_STRING); } + + +L?'(\\.|[^\'])*\' { + /* Non PROMELA extension for single quoted string literals */ + yylval->value = strdup(yytext); return(PML_STRING); +} + +{DIGIT}+ { yylval->value = strdup(yytext); return PML_CONST; } +{ID} { yylval->value = strdup(yytext); return PML_NAME; } + +[ \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..3a99921 --- /dev/null +++ b/src/uscxml/plugins/datamodel/promela/parser/promela.lex.yy.cpp @@ -0,0 +1,2598 @@ +#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 + +/* Note: We specifically omit the test for yy_rule_can_match_eol because it requires + * access to the local variable yy_act. Since yyless() is a macro, it would break + * existing scanners that call yyless() from OUTSIDE promela_lex. + * One obvious solution it to make yy_act a global. I tried that, and saw + * a 5% performance hit in a non-yylineno scanner, because yy_act is + * normally declared as a register variable-- so it is not worth it. + */ +#define YY_LESS_LINENO(n) \ + do { \ + yy_size_t yyl;\ + for ( yyl = n; yyl < yyleng; ++yyl )\ + if ( yytext[yyl] == '\n' )\ + --yylineno;\ + }while(0) + +/* Return all but the first "n" matched characters back to the input stream. */ +#define yyless(n) \ + 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 46 +#define YY_END_OF_BUFFER 47 +/* 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[126] = { + 0, + 0, 0, 47, 45, 44, 44, 8, 45, 14, 25, + 45, 33, 34, 12, 15, 31, 16, 30, 13, 42, + 32, 21, 39, 22, 43, 43, 35, 36, 26, 43, + 43, 43, 43, 43, 43, 43, 43, 43, 43, 37, + 27, 38, 9, 44, 23, 0, 40, 0, 28, 0, + 41, 0, 10, 11, 0, 42, 17, 19, 24, 20, + 18, 43, 0, 0, 43, 43, 43, 43, 43, 43, + 43, 43, 43, 43, 43, 43, 43, 43, 43, 43, + 29, 0, 41, 0, 0, 0, 43, 43, 2, 43, + 43, 43, 3, 43, 43, 43, 43, 43, 43, 43, + + 43, 0, 1, 43, 43, 43, 43, 43, 4, 43, + 43, 43, 1, 43, 43, 43, 43, 43, 7, 5, + 43, 43, 6, 43, 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, 5, 1, 1, 6, 7, 8, 9, + 10, 11, 12, 13, 14, 15, 16, 17, 17, 17, + 17, 17, 17, 17, 17, 17, 17, 1, 18, 19, + 20, 21, 1, 1, 22, 22, 22, 22, 22, 22, + 22, 22, 22, 22, 22, 23, 22, 22, 22, 22, + 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, + 24, 25, 26, 27, 22, 1, 28, 29, 22, 30, + + 31, 32, 33, 34, 35, 22, 36, 37, 38, 39, + 40, 41, 22, 42, 43, 44, 45, 22, 22, 22, + 46, 22, 47, 48, 49, 50, 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[51] = { + 0, + 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, + 1, 1, 1, 1, 1, 1, 2, 1, 1, 1, + 1, 2, 2, 1, 1, 1, 1, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 1, 1, 1, 1 +} ; + +static yyconst flex_int16_t yy_base[131] = { + 0, + 0, 0, 172, 173, 49, 51, 151, 50, 173, 163, + 48, 173, 173, 173, 157, 173, 154, 173, 156, 149, + 173, 38, 145, 39, 0, 56, 173, 173, 173, 20, + 31, 136, 124, 131, 117, 118, 34, 30, 120, 173, + 110, 173, 173, 77, 173, 57, 173, 154, 173, 59, + 173, 66, 173, 173, 145, 138, 173, 173, 173, 173, + 173, 0, 76, 75, 111, 109, 108, 111, 106, 112, + 104, 108, 100, 110, 104, 108, 100, 96, 99, 96, + 173, 77, 78, 84, 127, 77, 106, 96, 0, 98, + 103, 90, 0, 91, 92, 88, 88, 93, 96, 95, + + 90, 78, 173, 82, 92, 91, 77, 76, 0, 80, + 88, 75, 96, 62, 73, 71, 68, 59, 0, 0, + 65, 65, 0, 65, 173, 109, 111, 88, 113, 115 +} ; + +static yyconst flex_int16_t yy_def[131] = { + 0, + 125, 1, 125, 125, 125, 125, 125, 126, 125, 125, + 127, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 128, 128, 125, 125, 125, 128, + 128, 128, 128, 128, 128, 128, 128, 128, 128, 125, + 125, 125, 125, 125, 125, 126, 125, 126, 125, 127, + 125, 129, 125, 125, 130, 125, 125, 125, 125, 125, + 125, 128, 126, 127, 128, 128, 128, 128, 128, 128, + 128, 128, 128, 128, 128, 128, 128, 128, 128, 128, + 125, 127, 127, 129, 130, 130, 128, 128, 128, 128, + 128, 128, 128, 128, 128, 128, 128, 128, 128, 128, + + 128, 130, 125, 128, 128, 128, 128, 128, 128, 128, + 128, 128, 130, 128, 128, 128, 128, 128, 128, 128, + 128, 128, 128, 128, 0, 125, 125, 125, 125, 125 +} ; + +static yyconst flex_int16_t yy_nxt[224] = { + 0, + 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, + 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, + 24, 25, 26, 27, 4, 28, 29, 30, 31, 25, + 25, 32, 25, 25, 33, 25, 34, 35, 25, 25, + 36, 25, 37, 38, 39, 25, 40, 41, 42, 43, + 44, 44, 44, 44, 47, 51, 57, 58, 60, 61, + 63, 47, 65, 64, 66, 67, 51, 75, 50, 76, + 68, 78, 52, 83, 48, 79, 69, 77, 44, 44, + 47, 48, 51, 52, 51, 51, 50, 102, 86, 62, + 84, 83, 103, 113, 89, 124, 123, 122, 121, 52, + + 48, 52, 52, 89, 120, 119, 86, 118, 84, 46, + 46, 50, 50, 82, 82, 85, 85, 117, 116, 89, + 115, 89, 109, 114, 112, 111, 109, 110, 109, 108, + 107, 106, 105, 89, 89, 89, 104, 86, 101, 100, + 99, 98, 97, 96, 95, 94, 93, 89, 92, 91, + 90, 89, 88, 87, 56, 86, 125, 81, 80, 74, + 73, 72, 71, 70, 59, 56, 55, 54, 53, 49, + 45, 125, 3, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125 +} ; + +static yyconst flex_int16_t yy_chk[224] = { + 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, 1, 1, 1, 1, 1, 1, + 5, 5, 6, 6, 8, 11, 22, 22, 24, 24, + 26, 46, 30, 26, 30, 31, 50, 37, 52, 37, + 31, 38, 11, 52, 8, 38, 31, 37, 44, 44, + 63, 46, 64, 50, 82, 83, 84, 86, 102, 128, + 52, 84, 86, 102, 124, 122, 121, 118, 117, 64, + + 63, 82, 83, 116, 115, 114, 113, 112, 84, 126, + 126, 127, 127, 129, 129, 130, 130, 111, 110, 108, + 107, 106, 105, 104, 101, 100, 99, 98, 97, 96, + 95, 94, 92, 91, 90, 88, 87, 85, 80, 79, + 78, 77, 76, 75, 74, 73, 72, 71, 70, 69, + 68, 67, 66, 65, 56, 55, 48, 41, 39, 36, + 35, 34, 33, 32, 23, 20, 19, 17, 15, 10, + 7, 3, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125, 125, 125, 125, 125, 125, 125, 125, + 125, 125, 125 +} ; + +/* Table of booleans, true if rule could match eol. */ +static yyconst flex_int32_t yy_rule_can_match_eol[47] = { + 0, + 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 1, 1, 0, 0, 1, 0, 0, +}; + +static yyconst flex_int16_t yy_rule_linenum[46] = { + 0, + 44, 46, 51, 52, 53, 54, 55, 57, 58, 59, + 60, 62, 63, 64, 66, 67, 69, 70, 72, 73, + 74, 75, 77, 78, 80, 81, 82, 85, 86, 88, + 89, 90, 92, 93, 95, 96, 98, 99, 101, 103, + 106, 111, 112, 114, 117 +} ; + +/* The intent behind this definition is that it'll catch + * 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 16 "promela.l" + +#include "../PromelaParser.h" +#include "promela.tab.hpp" +#define YYSTYPE PROMELA_STYPE +#define YYLTYPE PROMELA_LTYPE +#define YY_USER_INIT \ + yycolumn = yylloc->first_line = yylloc->first_column = 0; \ + yylineno = yylloc->last_line = yylloc->last_column = 0; \ + +//int yycolumn = 1; + +#define YY_USER_ACTION \ +{ \ + yylloc->first_line = yylineno; \ + yylloc->first_column = yycolumn; \ + yylloc->last_column = yycolumn + yyleng; \ + yylloc->last_line = yylineno; \ + yycolumn = yycolumn + yyleng; \ +} + +#line 661 "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; + + YYLTYPE * yylloc_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 + +# define yylloc yyg->yylloc_r + +int promela_lex_init (yyscan_t* scanner); + +int promela_lex_init_extra (YY_EXTRA_TYPE user_defined,yyscan_t* scanner); + +/* %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 ); + +YYLTYPE *promela_get_lloc (yyscan_t yyscanner ); + +void promela_set_lloc (YYLTYPE * yylloc_param ,yyscan_t yyscanner ); + +/* %endif */ + +/* Macros after this point can all be overridden by user definitions in + * 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,YYLTYPE * yylloc_param ,yyscan_t yyscanner); + +#define YY_DECL int promela_lex \ + (YYSTYPE * yylval_param, YYLTYPE * yylloc_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 42 "promela.l" + + +#line 970 "promela.lex.yy.cpp" + + yylval = yylval_param; + + yylloc = yylloc_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 >= 126 ) + 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 != 125 ); + 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 */ + + if ( yy_act != YY_END_OF_BUFFER && yy_rule_can_match_eol[yy_act] ) { + yy_size_t yyl; + for ( yyl = 0; yyl < yyleng; ++yyl ) + if ( yytext[yyl] == '\n' ) + + do { + yylineno++; + yycolumn=0; + } while(0) + ; + } + +do_action: /* This label is used only to access EOF actions. */ + + /* %% [12.0] debug code goes here */ + if ( yy_flex_debug ) { + if ( yy_act == 0 ) + fprintf( stderr, "--scanner backing up\n" ); + else if ( yy_act < 46 ) + fprintf( stderr, "--accepting rule at line %ld (\"%s\")\n", + (long)yy_rule_linenum[yy_act], yytext ); + else if ( yy_act == 46 ) + fprintf( stderr, "--accepting default rule (\"%s\")\n", + yytext ); + else if ( yy_act == 47 ) + 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: + /* rule 1 can match eol */ + YY_RULE_SETUP +#line 44 "promela.l" + /* multiline comments */ + YY_BREAK + case 2: + YY_RULE_SETUP +#line 46 "promela.l" + { + yylval->value = strdup(yytext); + return PML_TYPE; + } + YY_BREAK + case 3: + YY_RULE_SETUP +#line 51 "promela.l" + { return PML_LEN; } + YY_BREAK + case 4: + YY_RULE_SETUP +#line 52 "promela.l" + { yylval->value = strdup(yytext); return PML_CONST; } + YY_BREAK + case 5: + YY_RULE_SETUP +#line 53 "promela.l" + { return PML_PRINT; } + YY_BREAK + case 6: + YY_RULE_SETUP +#line 54 "promela.l" + { return PML_TYPEDEF; } + YY_BREAK + case 7: + YY_RULE_SETUP +#line 55 "promela.l" + { return PML_ASSERT; } + YY_BREAK + case 8: + YY_RULE_SETUP +#line 57 "promela.l" + { return PML_NEG; } + YY_BREAK + case 9: + YY_RULE_SETUP +#line 58 "promela.l" + { return PML_COMPL; } + YY_BREAK + case 10: + YY_RULE_SETUP +#line 59 "promela.l" + { return PML_INCR; } + YY_BREAK + case 11: + YY_RULE_SETUP +#line 60 "promela.l" + { return PML_DECR; } + YY_BREAK + case 12: + YY_RULE_SETUP +#line 62 "promela.l" + { return PML_TIMES; } + YY_BREAK + case 13: + YY_RULE_SETUP +#line 63 "promela.l" + { return PML_DIVIDE; } + YY_BREAK + case 14: + YY_RULE_SETUP +#line 64 "promela.l" + { return PML_MODULO; } + YY_BREAK + case 15: + YY_RULE_SETUP +#line 66 "promela.l" + { return PML_PLUS; } + YY_BREAK + case 16: + YY_RULE_SETUP +#line 67 "promela.l" + { return PML_MINUS; } + YY_BREAK + case 17: + YY_RULE_SETUP +#line 69 "promela.l" + { return PML_LSHIFT; } + YY_BREAK + case 18: + YY_RULE_SETUP +#line 70 "promela.l" + { return PML_RSHIFT; } + YY_BREAK + case 19: + YY_RULE_SETUP +#line 72 "promela.l" + { return PML_LE; } + YY_BREAK + case 20: + YY_RULE_SETUP +#line 73 "promela.l" + { return PML_GE; } + YY_BREAK + case 21: + YY_RULE_SETUP +#line 74 "promela.l" + { return PML_LT; } + YY_BREAK + case 22: + YY_RULE_SETUP +#line 75 "promela.l" + { return PML_GT; } + YY_BREAK + case 23: + YY_RULE_SETUP +#line 77 "promela.l" + { return PML_NE; } + YY_BREAK + case 24: + YY_RULE_SETUP +#line 78 "promela.l" + { return PML_EQ; } + YY_BREAK + case 25: + YY_RULE_SETUP +#line 80 "promela.l" + { return PML_BITAND; } + YY_BREAK + case 26: + YY_RULE_SETUP +#line 81 "promela.l" + { return PML_BITXOR; } + YY_BREAK + case 27: + YY_RULE_SETUP +#line 82 "promela.l" + { return PML_BITOR; } + YY_BREAK + case 28: + YY_RULE_SETUP +#line 85 "promela.l" + { return PML_AND; } + YY_BREAK + case 29: + YY_RULE_SETUP +#line 86 "promela.l" + { return PML_OR; } + YY_BREAK + case 30: + YY_RULE_SETUP +#line 88 "promela.l" + { return PML_DOT; } + YY_BREAK + case 31: + YY_RULE_SETUP +#line 89 "promela.l" + { return PML_COMMA; } + YY_BREAK + case 32: + YY_RULE_SETUP +#line 90 "promela.l" + { return PML_SEMI; } + YY_BREAK + case 33: + YY_RULE_SETUP +#line 92 "promela.l" + { return '('; } + YY_BREAK + case 34: + YY_RULE_SETUP +#line 93 "promela.l" + { return ')'; } + YY_BREAK + case 35: + YY_RULE_SETUP +#line 95 "promela.l" + { return '['; } + YY_BREAK + case 36: + YY_RULE_SETUP +#line 96 "promela.l" + { return ']'; } + YY_BREAK + case 37: + YY_RULE_SETUP +#line 98 "promela.l" + { return '{'; } + YY_BREAK + case 38: + YY_RULE_SETUP +#line 99 "promela.l" + { return '}'; } + YY_BREAK + case 39: + YY_RULE_SETUP +#line 101 "promela.l" + { return PML_ASGN; } + YY_BREAK + case 40: + /* rule 40 can match eol */ + YY_RULE_SETUP +#line 103 "promela.l" + { yylval->value = strdup(yytext); return(PML_STRING); } + YY_BREAK + case 41: + /* rule 41 can match eol */ + YY_RULE_SETUP +#line 106 "promela.l" + { + /* Non PROMELA extension for single quoted string literals */ + yylval->value = strdup(yytext); + return(PML_STRING); + } + YY_BREAK + case 42: + YY_RULE_SETUP +#line 111 "promela.l" + { yylval->value = strdup(yytext); return PML_CONST; } + YY_BREAK + case 43: + YY_RULE_SETUP +#line 112 "promela.l" + { yylval->value = strdup(yytext); return PML_NAME; } + YY_BREAK + case 44: + /* rule 44 can match eol */ + YY_RULE_SETUP +#line 114 "promela.l" + /* eat up whitespace */ + YY_BREAK + case 45: + YY_RULE_SETUP +#line 117 "promela.l" + { /*printf( "Unrecognized character: %s\n", yytext ); */ } + YY_BREAK + case 46: + YY_RULE_SETUP +#line 118 "promela.l" + ECHO; + YY_BREAK +#line 1336 "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 >= 126 ) + 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 >= 126 ) + 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 == 125); + + 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 */ + + if ( c == '\n' ) { + --yylineno; + } + + 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 */ + if ( c == '\n' ) + + do { + yylineno++; + yycolumn=0; + } while(0) + ; + + 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; +} + +YYLTYPE *promela_get_lloc (yyscan_t yyscanner) { + struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; + return yylloc; +} + +void promela_set_lloc (YYLTYPE * yylloc_param , yyscan_t yyscanner) { + struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; + yylloc = yylloc_param; +} + +/* %endif */ + +/* User-visible API */ + +/* 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 118 "promela.l" diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.tab.cpp b/src/uscxml/plugins/datamodel/promela/parser/promela.tab.cpp new file mode 100644 index 0000000..098c890 --- /dev/null +++ b/src/uscxml/plugins/datamodel/promela/parser/promela.tab.cpp @@ -0,0 +1,2634 @@ +/* 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 +#define YYLTYPE PROMELA_LTYPE +/* 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 +#define yylloc promela_lloc + +/* 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, PROMELA_LTYPE* yylloc_param, void* yyscanner); + +using namespace uscxml; + +/* Line 371 of yacc.c */ +#line 93 "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 1 +# 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 { + PML_VAR_ARRAY = 258, + PML_VARLIST = 259, + PML_DECL = 260, + PML_DECLLIST = 261, + PML_STMNT = 262, + PML_COLON = 263, + PML_EXPR = 264, + PML_NAMELIST = 265, + PML_ASSERT = 266, + PML_PRINT = 267, + PML_PRINTM = 268, + PML_LEN = 269, + PML_STRING = 270, + PML_TYPEDEF = 271, + PML_MTYPE = 272, + PML_INLINE = 273, + PML_RETURN = 274, + PML_LABEL = 275, + PML_OF = 276, + PML_GOTO = 277, + PML_BREAK = 278, + PML_ELSE = 279, + PML_SEMI = 280, + PML_ARROW = 281, + PML_IF = 282, + PML_FI = 283, + PML_DO = 284, + PML_OD = 285, + PML_FOR = 286, + PML_SELECT = 287, + PML_IN = 288, + PML_SEP = 289, + PML_DOTDOT = 290, + PML_HIDDEN = 291, + PML_SHOW = 292, + PML_ISLOCAL = 293, + PML_CONST = 294, + PML_TYPE = 295, + PML_XU = 296, + PML_NAME = 297, + PML_UNAME = 298, + PML_PNAME = 299, + PML_INAME = 300, + PML_CLAIM = 301, + PML_TRACE = 302, + PML_INIT = 303, + PML_LTL = 304, + PML_COMMA = 305, + PML_ASGN = 306, + PML_AND = 307, + PML_OR = 308, + PML_BITAND = 309, + PML_BITXOR = 310, + PML_BITOR = 311, + PML_NE = 312, + PML_EQ = 313, + PML_LE = 314, + PML_GE = 315, + PML_LT = 316, + PML_GT = 317, + PML_RSHIFT = 318, + PML_LSHIFT = 319, + PML_MINUS = 320, + PML_PLUS = 321, + PML_MODULO = 322, + PML_DIVIDE = 323, + PML_TIMES = 324, + PML_DECR = 325, + PML_INCR = 326, + PML_COMPL = 327, + PML_NEG = 328, + PML_CMPND = 329, + PML_DOT = 330 +}; +#endif + + +#if ! defined PROMELA_STYPE && ! defined PROMELA_STYPE_IS_DECLARED +typedef union PROMELA_STYPE { + /* Line 387 of yacc.c */ +#line 39 "promela.ypp" + + uscxml::PromelaParserNode* node; + char* value; + + + /* Line 387 of yacc.c */ +#line 225 "promela.tab.cpp" +} PROMELA_STYPE; +# define PROMELA_STYPE_IS_TRIVIAL 1 +# define promela_stype PROMELA_STYPE /* obsolescent; will be withdrawn */ +# define PROMELA_STYPE_IS_DECLARED 1 +#endif + +#if ! defined PROMELA_LTYPE && ! defined PROMELA_LTYPE_IS_DECLARED +typedef struct PROMELA_LTYPE { + int first_line; + int first_column; + int last_line; + int last_column; +} PROMELA_LTYPE; +# define promela_ltype PROMELA_LTYPE /* obsolescent; will be withdrawn */ +# define PROMELA_LTYPE_IS_DECLARED 1 +# define PROMELA_LTYPE_IS_TRIVIAL 1 +#endif + + +#ifdef YYPARSE_PARAM +#if defined __STDC__ || defined __cplusplus +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 265 "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_LTYPE_IS_TRIVIAL && PROMELA_LTYPE_IS_TRIVIAL \ + && defined PROMELA_STYPE_IS_TRIVIAL && PROMELA_STYPE_IS_TRIVIAL))) + +/* A type that is properly aligned for any stack member. */ +union yyalloc { + yytype_int16 yyss_alloc; + YYSTYPE yyvs_alloc; + YYLTYPE yyls_alloc; +}; + +/* The size of the maximum gap between one aligned stack and the next. */ +# 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) + sizeof (YYLTYPE)) \ + + 2 * 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 32 +/* YYLAST -- Last index in YYTABLE. */ +#define YYLAST 285 + +/* YYNTOKENS -- Number of terminals. */ +#define YYNTOKENS 82 +/* YYNNTS -- Number of nonterminals. */ +#define YYNNTS 21 +/* YYNRULES -- Number of rules. */ +#define YYNRULES 81 +/* YYNRULES -- Number of states. */ +#define YYNSTATES 143 + +/* YYTRANSLATE(YYLEX) -- Bison symbol number corresponding to YYLEX. */ +#define YYUNDEFTOK 2 +#define YYMAXUTOK 330 + +#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, 2, 2, 2, + 11, 12, 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, 13, 2, 14, 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, 15, 2, 16, 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, 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, 63, 64, 65, 66, 67, 68, 69, 70, + 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, + 81 +}; + +#if PROMELA_DEBUG +/* YYPRHS[YYN] -- Index of the first RHS symbol of rule number YYN in + YYRHS. */ +static const yytype_uint16 yyprhs[] = { + 0, 0, 3, 5, 7, 9, 11, 13, 18, 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, 118, 119, 121, 123, + 125, 129, 133, 140, 143, 149, 151, 154, 158, 160, + 164, 166, 170, 172, 176, 181, 183, 186, 190, 194, + 198, 202, 206, 210, 212, 215, 218, 220, 223, 227, + 229, 233, 236, 239, 245, 250, 255, 258, 260, 261, + 264, 266 +}; + +/* YYRHS -- A `-1'-separated list of the rules' RHS. */ +static const yytype_int8 yyrhs[] = { + 83, 0, -1, 92, -1, 88, -1, 98, -1, 86, + -1, 48, -1, 48, 13, 88, 14, -1, 85, 87, + -1, -1, 81, 86, -1, 11, 88, 12, -1, 88, + 72, 88, -1, 88, 71, 88, -1, 88, 75, 88, + -1, 88, 74, 88, -1, 88, 73, 88, -1, 88, + 60, 88, -1, 88, 61, 88, -1, 88, 62, 88, + -1, 88, 68, 88, -1, 88, 67, 88, -1, 88, + 66, 88, -1, 88, 65, 88, -1, 88, 64, 88, + -1, 88, 63, 88, -1, 88, 58, 88, -1, 88, + 59, 88, -1, 88, 70, 88, -1, 88, 69, 88, + -1, 79, 88, -1, 71, 88, -1, 20, 11, 84, + 12, -1, 84, -1, 45, -1, 21, -1, -1, 42, + -1, 43, -1, 44, -1, 89, 46, 93, -1, 89, + 49, 93, -1, 89, 46, 57, 15, 97, 16, -1, + 89, 91, -1, 22, 48, 15, 92, 16, -1, 90, + -1, 90, 31, -1, 90, 31, 92, -1, 94, -1, + 94, 56, 93, -1, 95, -1, 95, 57, 88, -1, + 48, -1, 48, 8, 45, -1, 48, 13, 96, 14, + -1, 45, -1, 71, 96, -1, 11, 96, 12, -1, + 96, 72, 96, -1, 96, 71, 96, -1, 96, 75, + 96, -1, 96, 74, 96, -1, 96, 73, 96, -1, + 48, -1, 97, 48, -1, 97, 56, -1, 99, -1, + 99, 31, -1, 99, 31, 98, -1, 100, -1, 84, + 57, 88, -1, 84, 77, -1, 84, 76, -1, 18, + 11, 21, 101, 12, -1, 18, 11, 84, 12, -1, + 18, 11, 45, 12, -1, 17, 88, -1, 88, -1, + -1, 56, 102, -1, 88, -1, 88, 56, 102, -1 +}; + +/* YYRLINE[YYN] -- source line where rule number YYN was defined. */ +static const yytype_uint8 yyrline[] = { + 0, 85, 85, 89, 93, 99, 102, 103, 106, 121, + 122, 132, 133, 134, 135, 136, 137, 138, 139, 140, + 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, + 151, 152, 154, 155, 156, 157, 163, 164, 165, 166, + 169, 170, 171, 172, 175, 178, 179, 180, 190, 191, + 194, 195, 198, 199, 200, 203, 204, 205, 206, 207, + 208, 209, 210, 213, 214, 223, 226, 227, 228, 231, + 234, 235, 236, 237, 238, 239, 240, 241, 244, 245, + 248, 249 +}; +#endif + +#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", "PML_VAR_ARRAY", "PML_VARLIST", + "PML_DECL", "PML_DECLLIST", "PML_STMNT", "PML_COLON", "PML_EXPR", + "PML_NAMELIST", "'('", "')'", "'['", "']'", "'{'", "'}'", "PML_ASSERT", + "PML_PRINT", "PML_PRINTM", "PML_LEN", "PML_STRING", "PML_TYPEDEF", + "PML_MTYPE", "PML_INLINE", "PML_RETURN", "PML_LABEL", "PML_OF", + "PML_GOTO", "PML_BREAK", "PML_ELSE", "PML_SEMI", "PML_ARROW", "PML_IF", + "PML_FI", "PML_DO", "PML_OD", "PML_FOR", "PML_SELECT", "PML_IN", + "PML_SEP", "PML_DOTDOT", "PML_HIDDEN", "PML_SHOW", "PML_ISLOCAL", + "PML_CONST", "PML_TYPE", "PML_XU", "PML_NAME", "PML_UNAME", "PML_PNAME", + "PML_INAME", "PML_CLAIM", "PML_TRACE", "PML_INIT", "PML_LTL", + "PML_COMMA", "PML_ASGN", "PML_AND", "PML_OR", "PML_BITAND", "PML_BITXOR", + "PML_BITOR", "PML_NE", "PML_EQ", "PML_LE", "PML_GE", "PML_LT", "PML_GT", + "PML_RSHIFT", "PML_LSHIFT", "PML_MINUS", "PML_PLUS", "PML_MODULO", + "PML_DIVIDE", "PML_TIMES", "PML_DECR", "PML_INCR", "PML_COMPL", + "PML_NEG", "PML_CMPND", "PML_DOT", "$accept", "program", "varref", + "pfld", "cmpnd", "sfld", "expr", "vis", "one_decl", "utype", "decl_lst", + "var_list", "ivar", "vardcl", "const_expr", "nlst", "stmnt_lst", "stmnt", + "Stmnt", "prargs", "arg", 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, 40, 41, 91, 93, 123, 125, 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, 318, + 319, 320, 321, 322, 323, 324, 325, 326, 327, 328, + 329, 330 +}; +# endif + +/* YYR1[YYN] -- Symbol number of symbol that rule YYN derives. */ +static const yytype_uint8 yyr1[] = { + 0, 82, 83, 83, 83, 84, 85, 85, 86, 87, + 87, 88, 88, 88, 88, 88, 88, 88, 88, 88, + 88, 88, 88, 88, 88, 88, 88, 88, 88, 88, + 88, 88, 88, 88, 88, 88, 89, 89, 89, 89, + 90, 90, 90, 90, 91, 92, 92, 92, 93, 93, + 94, 94, 95, 95, 95, 96, 96, 96, 96, 96, + 96, 96, 96, 97, 97, 97, 98, 98, 98, 99, + 100, 100, 100, 100, 100, 100, 100, 100, 101, 101, + 102, 102 +}; + +/* YYR2[YYN] -- Number of symbols composing right hand side of rule YYN. */ +static const yytype_uint8 yyr2[] = { + 0, 2, 1, 1, 1, 1, 1, 4, 2, 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, 1, 0, 1, 1, 1, + 3, 3, 6, 2, 5, 1, 2, 3, 1, 3, + 1, 3, 1, 3, 4, 1, 2, 3, 3, 3, + 3, 3, 3, 1, 2, 2, 1, 2, 3, 1, + 3, 2, 2, 5, 4, 4, 2, 1, 0, 2, + 1, 3 +}; + +/* 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[] = { + 36, 0, 0, 0, 0, 35, 37, 38, 39, 34, + 6, 0, 0, 0, 33, 9, 5, 3, 0, 45, + 2, 4, 66, 69, 33, 0, 76, 0, 0, 0, + 31, 30, 1, 0, 72, 71, 0, 8, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 43, + 36, 67, 11, 78, 0, 0, 0, 0, 70, 10, + 26, 27, 17, 18, 19, 25, 24, 23, 22, 21, + 20, 29, 28, 13, 12, 16, 15, 14, 0, 52, + 0, 40, 48, 50, 41, 47, 77, 68, 0, 0, + 75, 74, 32, 7, 36, 0, 0, 0, 0, 0, + 80, 79, 73, 0, 53, 0, 55, 0, 0, 63, + 0, 49, 51, 0, 44, 0, 56, 54, 0, 0, + 0, 0, 0, 42, 64, 65, 81, 57, 59, 58, + 62, 61, 60 +}; + +/* YYDEFGOTO[NTERM-NUM]. */ +static const yytype_int8 yydefgoto[] = { + -1, 13, 24, 15, 16, 37, 110, 18, 19, 59, + 20, 91, 92, 93, 118, 120, 21, 22, 23, 99, + 111 +}; + +/* YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing + STATE-NUM. */ +#define YYPACT_NINF -112 +static const yytype_int16 yypact[] = { + 14, 53, 53, 3, 13, -112, -112, -112, -112, -112, + 15, 53, 53, 26, 34, -51, -112, 138, 81, 5, + -112, -112, 58, -112, -112, 75, 160, 169, 42, 53, + -66, -112, -112, 53, -112, -112, 42, -112, 53, 53, + 53, 53, 53, 53, 53, 53, 53, 53, 53, 53, + 53, 53, 53, 53, 53, 53, 44, -35, 51, -112, + 72, 49, -112, 46, 88, 96, 100, 93, 160, -112, + 176, 176, 189, 189, 189, 200, 200, 207, 207, 207, + 207, 120, 120, -66, -66, -112, -112, -112, 98, -3, + 102, -112, 63, 74, -112, -112, 160, -112, 53, 113, + -112, -112, -112, -112, 62, 126, -8, 167, 51, 53, + 114, -112, -112, 267, -112, -8, -112, -8, 9, -112, + 70, -112, 160, 53, -112, 4, 48, -112, -8, -8, + -8, -8, -8, -112, -112, -112, -112, -112, 48, 48, + -112, -112, -112 +}; + +/* YYPGOTO[NTERM-NUM]. */ +static const yytype_int16 yypgoto[] = { + -112, -112, 68, -112, 180, -112, 0, -112, -112, -112, + -33, -43, -112, -112, -111, -112, 223, -112, -112, -112, + 162 +}; + +/* 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 -78 +static const yytype_int16 yytable[] = { + 17, 25, 26, 115, 125, 105, 126, 53, 54, 55, + 106, 30, 31, 89, 27, 94, 137, 138, 139, 140, + 141, 142, 90, 127, 28, 1, 32, 95, 29, 67, + 36, 2, 3, 68, 4, 5, 60, 116, 70, 71, + 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, + 82, 83, 84, 85, 86, 87, 6, 7, 8, 9, + 1, 96, 10, 117, 1, 121, 2, 3, 14, 4, + 5, 113, -46, 4, 5, 128, 129, 130, 131, 132, + 128, 129, 130, 131, 132, 11, 133, 62, -46, 61, + 10, 33, 88, 12, 9, 65, 66, 10, 9, 89, + 100, 10, 98, 56, 6, 7, 8, 103, 101, 122, + 34, 35, 102, 104, 6, 7, 8, 107, 134, 108, + 11, 130, 131, 132, 11, 112, 135, 57, 12, 14, + 58, 109, 12, 38, 39, 40, 41, 42, 43, 44, + 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, + 55, 38, 39, 40, 41, 42, 43, 44, 45, 46, + 47, 48, 49, 50, 51, 52, 53, 54, 55, -77, + 123, 114, 38, 39, 40, 41, 42, 43, 44, 45, + 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, + 63, 51, 52, 53, 54, 55, 38, 39, 40, 41, + 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, + 52, 53, 54, 55, 64, 119, 69, 10, 38, 39, + 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, + 50, 51, 52, 53, 54, 55, 40, 41, 42, 43, + 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, + 54, 55, 43, 44, 45, 46, 47, 48, 49, 50, + 51, 52, 53, 54, 55, 45, 46, 47, 48, 49, + 50, 51, 52, 53, 54, 55, 49, 50, 51, 52, + 53, 54, 55, 124, 97, 136 +}; + +#define yypact_value_is_default(Yystate) \ + (!!((Yystate) == (-112))) + +#define yytable_value_is_error(Yytable_value) \ + YYID (0) + +static const yytype_uint8 yycheck[] = { + 0, 1, 2, 11, 115, 8, 117, 73, 74, 75, + 13, 11, 12, 48, 11, 58, 12, 128, 129, 130, + 131, 132, 57, 14, 11, 11, 0, 60, 13, 29, + 81, 17, 18, 33, 20, 21, 31, 45, 38, 39, + 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, + 50, 51, 52, 53, 54, 55, 42, 43, 44, 45, + 11, 61, 48, 71, 11, 108, 17, 18, 0, 20, + 21, 104, 0, 20, 21, 71, 72, 73, 74, 75, + 71, 72, 73, 74, 75, 71, 16, 12, 16, 31, + 48, 57, 48, 79, 45, 27, 28, 48, 45, 48, + 12, 48, 56, 22, 42, 43, 44, 14, 12, 109, + 76, 77, 12, 15, 42, 43, 44, 15, 48, 56, + 71, 73, 74, 75, 71, 12, 56, 46, 79, 61, + 49, 57, 79, 58, 59, 60, 61, 62, 63, 64, + 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, + 75, 58, 59, 60, 61, 62, 63, 64, 65, 66, + 67, 68, 69, 70, 71, 72, 73, 74, 75, 31, + 56, 45, 58, 59, 60, 61, 62, 63, 64, 65, + 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, + 21, 71, 72, 73, 74, 75, 58, 59, 60, 61, + 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, + 72, 73, 74, 75, 45, 48, 36, 48, 58, 59, + 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, + 70, 71, 72, 73, 74, 75, 60, 61, 62, 63, + 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, + 74, 75, 63, 64, 65, 66, 67, 68, 69, 70, + 71, 72, 73, 74, 75, 65, 66, 67, 68, 69, + 70, 71, 72, 73, 74, 75, 69, 70, 71, 72, + 73, 74, 75, 16, 61, 123 +}; + +/* YYSTOS[STATE-NUM] -- The (internal number of the) accessing + symbol of state STATE-NUM. */ +static const yytype_uint8 yystos[] = { + 0, 11, 17, 18, 20, 21, 42, 43, 44, 45, + 48, 71, 79, 83, 84, 85, 86, 88, 89, 90, + 92, 98, 99, 100, 84, 88, 88, 11, 11, 13, + 88, 88, 0, 57, 76, 77, 81, 87, 58, 59, + 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, + 70, 71, 72, 73, 74, 75, 22, 46, 49, 91, + 31, 31, 12, 21, 45, 84, 84, 88, 88, 86, + 88, 88, 88, 88, 88, 88, 88, 88, 88, 88, + 88, 88, 88, 88, 88, 88, 88, 88, 48, 48, + 57, 93, 94, 95, 93, 92, 88, 98, 56, 101, + 12, 12, 12, 14, 15, 8, 13, 15, 56, 57, + 88, 102, 12, 92, 45, 11, 45, 71, 96, 48, + 97, 93, 88, 56, 16, 96, 96, 14, 71, 72, + 73, 74, 75, 16, 48, 56, 102, 12, 96, 96, + 96, 96, 96 +}; + +#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 (&yylloc, ctx, scanner, YY_("syntax error: cannot back up")); \ + YYERROR; \ + } \ +while (YYID (0)) + +/* Error token number */ +#define YYTERROR 1 +#define YYERRCODE 256 + + +/* YYLLOC_DEFAULT -- Set CURRENT to span from RHS[1] to RHS[N]. + If N is 0, then set CURRENT to the empty location which ends + the previous symbol: RHS[0] (always defined). */ + +#ifndef YYLLOC_DEFAULT +# define YYLLOC_DEFAULT(Current, Rhs, N) \ + do \ + if (YYID (N)) \ + { \ + (Current).first_line = YYRHSLOC (Rhs, 1).first_line; \ + (Current).first_column = YYRHSLOC (Rhs, 1).first_column; \ + (Current).last_line = YYRHSLOC (Rhs, N).last_line; \ + (Current).last_column = YYRHSLOC (Rhs, N).last_column; \ + } \ + else \ + { \ + (Current).first_line = (Current).last_line = \ + YYRHSLOC (Rhs, 0).last_line; \ + (Current).first_column = (Current).last_column = \ + YYRHSLOC (Rhs, 0).last_column; \ + } \ + while (YYID (0)) +#endif + +#define YYRHSLOC(Rhs, K) ((Rhs)[K]) + + +/* YY_LOCATION_PRINT -- Print the location on the stream. + This macro was not mandated originally: define only if we know + we won't break user code: when these are the locations we know. */ + +#ifndef YY_LOCATION_PRINT +# if defined PROMELA_LTYPE_IS_TRIVIAL && PROMELA_LTYPE_IS_TRIVIAL + +/* Print *YYLOCP on YYO. Private, do not rely on its existence. */ + +__attribute__((__unused__)) +#if (defined __STDC__ || defined __C99__FUNC__ \ + || defined __cplusplus || defined _MSC_VER) +static unsigned +yy_location_print_ (FILE *yyo, YYLTYPE const * const yylocp) +#else +static unsigned +yy_location_print_ (yyo, yylocp) +FILE *yyo; +YYLTYPE const * const yylocp; +#endif +{ + unsigned res = 0; + int end_col = 0 != yylocp->last_column ? yylocp->last_column - 1 : 0; + if (0 <= yylocp->first_line) { + res += fprintf (yyo, "%d", yylocp->first_line); + if (0 <= yylocp->first_column) + res += fprintf (yyo, ".%d", yylocp->first_column); + } + if (0 <= yylocp->last_line) { + if (yylocp->first_line < yylocp->last_line) { + res += fprintf (yyo, "-%d", yylocp->last_line); + if (0 <= end_col) + res += fprintf (yyo, ".%d", end_col); + } else if (0 <= end_col && yylocp->first_column < end_col) + res += fprintf (yyo, "-%d", end_col); + } + return res; +} + +# define YY_LOCATION_PRINT(File, Loc) \ + yy_location_print_ (File, &(Loc)) + +# else +# define YY_LOCATION_PRINT(File, Loc) ((void) 0) +# endif +#endif + + +/* YYLEX -- calling `yylex' with the right arguments. */ +#ifdef YYLEX_PARAM +# define YYLEX yylex (&yylval, &yylloc, YYLEX_PARAM) +#else +# define YYLEX yylex (&yylval, &yylloc, 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, Location, 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, YYLTYPE const * const yylocationp, uscxml::PromelaParser* ctx, void * scanner) +#else +static void +yy_symbol_value_print (yyoutput, yytype, yyvaluep, yylocationp, ctx, scanner) +FILE *yyoutput; +int yytype; +YYSTYPE const * const yyvaluep; +YYLTYPE const * const yylocationp; +uscxml::PromelaParser* ctx; +void * scanner; +#endif +{ + FILE *yyo = yyoutput; + YYUSE (yyo); + if (!yyvaluep) + return; + YYUSE (yylocationp); + 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, YYLTYPE const * const yylocationp, uscxml::PromelaParser* ctx, void * scanner) +#else +static void +yy_symbol_print (yyoutput, yytype, yyvaluep, yylocationp, ctx, scanner) +FILE *yyoutput; +int yytype; +YYSTYPE const * const yyvaluep; +YYLTYPE const * const yylocationp; +uscxml::PromelaParser* ctx; +void * scanner; +#endif +{ + if (yytype < YYNTOKENS) + YYFPRINTF (yyoutput, "token %s (", yytname[yytype]); + else + YYFPRINTF (yyoutput, "nterm %s (", yytname[yytype]); + + YY_LOCATION_PRINT (yyoutput, *yylocationp); + YYFPRINTF (yyoutput, ": "); + yy_symbol_value_print (yyoutput, yytype, yyvaluep, yylocationp, 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, YYLTYPE *yylsp, int yyrule, uscxml::PromelaParser* ctx, void * scanner) +#else +static void +yy_reduce_print (yyvsp, yylsp, yyrule, ctx, scanner) +YYSTYPE *yyvsp; +YYLTYPE *yylsp; +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)]) + , &(yylsp[(yyi + 1) - (yynrhs)]) , ctx, scanner); + YYFPRINTF (stderr, "\n"); + } +} + +# define YY_REDUCE_PRINT(Rule) \ +do { \ + if (yydebug) \ + yy_reduce_print (yyvsp, yylsp, 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, YYLTYPE *yylocationp, uscxml::PromelaParser* ctx, void * scanner) +#else +static void +yydestruct (yymsg, yytype, yyvaluep, yylocationp, ctx, scanner) +const char *yymsg; +int yytype; +YYSTYPE *yyvaluep; +YYLTYPE *yylocationp; +uscxml::PromelaParser* ctx; +void * scanner; +#endif +{ + YYUSE (yyvaluep); + YYUSE (yylocationp); + YYUSE (ctx); + YYUSE (scanner); + + 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 + static YYLTYPE yyloc_default +# if defined PROMELA_LTYPE_IS_TRIVIAL && PROMELA_LTYPE_IS_TRIVIAL + = { 1, 1, 1, 1 } +# endif + ; +#ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN +# define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN +# define YY_IGNORE_MAYBE_UNINITIALIZED_END +#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); + + /* Location data for the lookahead symbol. */ + YYLTYPE yylloc = yyloc_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. + `yyls': related to locations. + + 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; + + /* The location stack. */ + YYLTYPE yylsa[YYINITDEPTH]; + YYLTYPE *yyls; + YYLTYPE *yylsp; + + /* The locations where the error started and ended. */ + YYLTYPE yyerror_range[3]; + + YYSIZE_T yystacksize; + + int yyn; + 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; + YYLTYPE yyloc; + +#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), yylsp -= (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; + yylsp = yyls = yylsa; + yystacksize = YYINITDEPTH; + + YYDPRINTF ((stderr, "Starting parse\n")); + + yystate = 0; + yyerrstatus = 0; + yynerrs = 0; + yychar = YYEMPTY; /* Cause a token to be read. */ + yylsp[0] = yylloc; + 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; + YYLTYPE *yyls1 = yyls; + + /* Each stack pointer address is followed by the size of the + data in use in that stack, in bytes. This used to be a + 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), + &yyls1, yysize * sizeof (*yylsp), + &yystacksize); + + yyls = yyls1; + 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); + YYSTACK_RELOCATE (yyls_alloc, yyls); +# undef YYSTACK_RELOCATE + if (yyss1 != yyssa) + YYSTACK_FREE (yyss1); + } +# endif +#endif /* no yyoverflow */ + + yyssp = yyss + yysize - 1; + yyvsp = yyvs + yysize - 1; + yylsp = yyls + 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 + *++yylsp = yylloc; + 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]; + + /* Default location. */ + YYLLOC_DEFAULT (yyloc, (yylsp - yylen), yylen); + YY_REDUCE_PRINT (yyn); + switch (yyn) { + case 2: + /* Line 1787 of yacc.c */ +#line 85 "promela.ypp" + { + ctx->ast = (yyvsp[(1) - (1)].node); + ctx->type = PromelaParser::PROMELA_DECL; + } + break; + + case 3: + /* Line 1787 of yacc.c */ +#line 89 "promela.ypp" + { + ctx->ast = (yyvsp[(1) - (1)].node); + ctx->type = PromelaParser::PROMELA_EXPR; + } + break; + + case 4: + /* Line 1787 of yacc.c */ +#line 93 "promela.ypp" + { + ctx->ast = (yyvsp[(1) - (1)].node); + ctx->type = PromelaParser::PROMELA_STMNT; + } + break; + + case 5: + /* Line 1787 of yacc.c */ +#line 99 "promela.ypp" + { + (yyval.node) = (yyvsp[(1) - (1)].node); + } + break; + + case 6: + /* Line 1787 of yacc.c */ +#line 102 "promela.ypp" + { + (yyval.node) = ctx->value(PML_NAME, (void*)&((yylsp[(1) - (1)])), (yyvsp[(1) - (1)].value)); + free((yyvsp[(1) - (1)].value)); + } + break; + + case 7: + /* Line 1787 of yacc.c */ +#line 103 "promela.ypp" + { + (yyval.node) = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, (void*)&((yylsp[(1) - (4)])), (yyvsp[(1) - (4)].value)), (yyvsp[(3) - (4)].node)); + free((yyvsp[(1) - (4)].value)); + } + break; + + case 8: + /* Line 1787 of yacc.c */ +#line 107 "promela.ypp" + { + if ((yyvsp[(2) - (2)].node) != NULL) { + if ((yyvsp[(2) - (2)].node)->type == PML_CMPND) { + (yyval.node) = ctx->node(PML_CMPND, 1, (yyvsp[(1) - (2)].node)); + (yyval.node)->merge((yyvsp[(2) - (2)].node)); + delete (yyvsp[(2) - (2)].node); + } else { + (yyval.node) = ctx->node(PML_CMPND, 2, (yyvsp[(1) - (2)].node), (yyvsp[(2) - (2)].node)); + } + } else { + (yyval.node) = (yyvsp[(1) - (2)].node); + } + } + break; + + case 9: + /* Line 1787 of yacc.c */ +#line 121 "promela.ypp" + { + (yyval.node) = NULL; + } + break; + + case 10: + /* Line 1787 of yacc.c */ +#line 122 "promela.ypp" + { + (yyval.node) = (yyvsp[(2) - (2)].node); + } + break; + + case 11: + /* Line 1787 of yacc.c */ +#line 132 "promela.ypp" + { + (yyval.node) = (yyvsp[(2) - (3)].node); + } + break; + + case 12: + /* Line 1787 of yacc.c */ +#line 133 "promela.ypp" + { + (yyval.node) = ctx->node(PML_PLUS, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 13: + /* Line 1787 of yacc.c */ +#line 134 "promela.ypp" + { + (yyval.node) = ctx->node(PML_MINUS, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 14: + /* Line 1787 of yacc.c */ +#line 135 "promela.ypp" + { + (yyval.node) = ctx->node(PML_TIMES, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 15: + /* Line 1787 of yacc.c */ +#line 136 "promela.ypp" + { + (yyval.node) = ctx->node(PML_DIVIDE, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 16: + /* Line 1787 of yacc.c */ +#line 137 "promela.ypp" + { + (yyval.node) = ctx->node(PML_MODULO, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 17: + /* Line 1787 of yacc.c */ +#line 138 "promela.ypp" + { + (yyval.node) = ctx->node(PML_BITAND, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 18: + /* Line 1787 of yacc.c */ +#line 139 "promela.ypp" + { + (yyval.node) = ctx->node(PML_BITXOR, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 19: + /* Line 1787 of yacc.c */ +#line 140 "promela.ypp" + { + (yyval.node) = ctx->node(PML_BITOR, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 20: + /* Line 1787 of yacc.c */ +#line 141 "promela.ypp" + { + (yyval.node) = ctx->node(PML_GT, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 21: + /* Line 1787 of yacc.c */ +#line 142 "promela.ypp" + { + (yyval.node) = ctx->node(PML_LT, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 22: + /* Line 1787 of yacc.c */ +#line 143 "promela.ypp" + { + (yyval.node) = ctx->node(PML_GE, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 23: + /* Line 1787 of yacc.c */ +#line 144 "promela.ypp" + { + (yyval.node) = ctx->node(PML_LE, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 24: + /* Line 1787 of yacc.c */ +#line 145 "promela.ypp" + { + (yyval.node) = ctx->node(PML_EQ, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 25: + /* Line 1787 of yacc.c */ +#line 146 "promela.ypp" + { + (yyval.node) = ctx->node(PML_NE, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 26: + /* Line 1787 of yacc.c */ +#line 147 "promela.ypp" + { + (yyval.node) = ctx->node(PML_AND, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 27: + /* Line 1787 of yacc.c */ +#line 148 "promela.ypp" + { + (yyval.node) = ctx->node(PML_OR, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 28: + /* Line 1787 of yacc.c */ +#line 149 "promela.ypp" + { + (yyval.node) = ctx->node(PML_LSHIFT, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 29: + /* Line 1787 of yacc.c */ +#line 150 "promela.ypp" + { + (yyval.node) = ctx->node(PML_RSHIFT, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 30: + /* Line 1787 of yacc.c */ +#line 151 "promela.ypp" + { + (yyval.node) = ctx->node(PML_NEG, 1, (yyvsp[(2) - (2)].node)); + } + break; + + case 31: + /* Line 1787 of yacc.c */ +#line 152 "promela.ypp" + { + (yyval.node) = ctx->node(PML_MINUS, 1, (yyvsp[(2) - (2)].node)); + } + break; + + case 32: + /* Line 1787 of yacc.c */ +#line 154 "promela.ypp" + { + (yyval.node) = ctx->node(PML_LEN, 1, (yyvsp[(3) - (4)].node)); + } + break; + + case 33: + /* Line 1787 of yacc.c */ +#line 155 "promela.ypp" + { + (yyval.node) = (yyvsp[(1) - (1)].node); + } + break; + + case 34: + /* Line 1787 of yacc.c */ +#line 156 "promela.ypp" + { + (yyval.node) = ctx->value(PML_CONST, (void*)&((yylsp[(1) - (1)])), (yyvsp[(1) - (1)].value)); + free((yyvsp[(1) - (1)].value)); + } + break; + + case 35: + /* Line 1787 of yacc.c */ +#line 157 "promela.ypp" + { + /* Non standard promela for string literals */ + (yyval.node) = ctx->value(PML_STRING, (void*)&((yylsp[(1) - (1)])), (yyvsp[(1) - (1)].value)); + free((yyvsp[(1) - (1)].value)); + } + break; + + case 36: + /* Line 1787 of yacc.c */ +#line 163 "promela.ypp" + { + (yyval.node) = ctx->node(PML_SHOW, 0); + } + break; + + case 37: + /* Line 1787 of yacc.c */ +#line 164 "promela.ypp" + { + (yyval.node) = ctx->node(PML_HIDDEN, 0); + } + break; + + case 38: + /* Line 1787 of yacc.c */ +#line 165 "promela.ypp" + { + (yyval.node) = ctx->node(PML_SHOW, 0); + } + break; + + case 39: + /* Line 1787 of yacc.c */ +#line 166 "promela.ypp" + { + (yyval.node) = ctx->node(PML_ISLOCAL, 0); + } + break; + + case 40: + /* Line 1787 of yacc.c */ +#line 169 "promela.ypp" + { + (yyval.node) = ctx->node(PML_DECL, 3, (yyvsp[(1) - (3)].node), ctx->value(PML_TYPE, (void*)&((yylsp[(2) - (3)])), (yyvsp[(2) - (3)].value)), (yyvsp[(3) - (3)].node)); + free((yyvsp[(2) - (3)].value)); + } + break; + + case 41: + /* Line 1787 of yacc.c */ +#line 170 "promela.ypp" + { + (yyval.node) = ctx->node(PML_UNAME, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 42: + /* Line 1787 of yacc.c */ +#line 171 "promela.ypp" + { + (yyval.node) = ctx->node(PML_DECL, 3, (yyvsp[(1) - (6)].node), ctx->value(PML_TYPE, (void*)&((yylsp[(2) - (6)])), (yyvsp[(2) - (6)].value)), (yyvsp[(5) - (6)].node)); + free((yyvsp[(2) - (6)].value)); + } + break; + + case 43: + /* Line 1787 of yacc.c */ +#line 172 "promela.ypp" + { + (yyval.node) = (yyvsp[(2) - (2)].node); + } + break; + + case 44: + /* Line 1787 of yacc.c */ +#line 175 "promela.ypp" + { + (yyval.node) = ctx->node(PML_TYPEDEF, 2, ctx->value(PML_NAME, (void*)&((yylsp[(2) - (5)])), (yyvsp[(2) - (5)].value)), (yyvsp[(4) - (5)].node)); + } + break; + + case 45: + /* Line 1787 of yacc.c */ +#line 178 "promela.ypp" + { + (yyval.node) = (yyvsp[(1) - (1)].node); + } + break; + + case 46: + /* Line 1787 of yacc.c */ +#line 179 "promela.ypp" + { + (yyval.node) = (yyvsp[(1) - (2)].node); + } + break; + + case 47: + /* Line 1787 of yacc.c */ +#line 180 "promela.ypp" + { + (yyval.node) = ctx->node(PML_DECLLIST, 1, (yyvsp[(1) - (3)].node)); + if((yyvsp[(3) - (3)].node)->type == PML_DECLLIST) { + (yyval.node)->merge((yyvsp[(3) - (3)].node)); + delete (yyvsp[(3) - (3)].node); + } else { + (yyval.node)->push((yyvsp[(3) - (3)].node)); + } + } + break; + + case 48: + /* Line 1787 of yacc.c */ +#line 190 "promela.ypp" + { + (yyval.node) = ctx->node(PML_VARLIST, 1, (yyvsp[(1) - (1)].node)); + } + break; + + case 49: + /* Line 1787 of yacc.c */ +#line 191 "promela.ypp" + { + (yyval.node) = ctx->node(PML_VARLIST, 1, (yyvsp[(1) - (3)].node)); + (yyval.node)->merge((yyvsp[(3) - (3)].node)); + delete (yyvsp[(3) - (3)].node); + } + break; + + case 50: + /* Line 1787 of yacc.c */ +#line 194 "promela.ypp" + { + (yyval.node) = (yyvsp[(1) - (1)].node); + } + break; + + case 51: + /* Line 1787 of yacc.c */ +#line 195 "promela.ypp" + { + (yyval.node) = ctx->node(PML_ASGN, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 52: + /* Line 1787 of yacc.c */ +#line 198 "promela.ypp" + { + (yyval.node) = ctx->value(PML_NAME, (void*)&((yylsp[(1) - (1)])), (yyvsp[(1) - (1)].value)); + free((yyvsp[(1) - (1)].value)); + } + break; + + case 53: + /* Line 1787 of yacc.c */ +#line 199 "promela.ypp" + { + (yyval.node) = ctx->node(PML_COLON, 2, ctx->value(PML_NAME, (void*)&((yylsp[(1) - (3)])), (yyvsp[(1) - (3)].value)), ctx->value(PML_CONST, (void*)&((yylsp[(3) - (3)])), (yyvsp[(3) - (3)].value))); + free((yyvsp[(1) - (3)].value)); + free((yyvsp[(3) - (3)].value)); + } + break; + + case 54: + /* Line 1787 of yacc.c */ +#line 200 "promela.ypp" + { + (yyval.node) = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, (void*)&((yylsp[(1) - (4)])), (yyvsp[(1) - (4)].value)), (yyvsp[(3) - (4)].node)); + free((yyvsp[(1) - (4)].value)); + } + break; + + case 55: + /* Line 1787 of yacc.c */ +#line 203 "promela.ypp" + { + (yyval.node) = ctx->value(PML_CONST, (void*)&((yylsp[(1) - (1)])), (yyvsp[(1) - (1)].value)); + free((yyvsp[(1) - (1)].value)); + } + break; + + case 56: + /* Line 1787 of yacc.c */ +#line 204 "promela.ypp" + { + (yyval.node) = ctx->node(PML_MINUS, 1, (yyvsp[(2) - (2)].node)); + } + break; + + case 57: + /* Line 1787 of yacc.c */ +#line 205 "promela.ypp" + { + (yyval.node) = (yyvsp[(2) - (3)].node); + } + break; + + case 58: + /* Line 1787 of yacc.c */ +#line 206 "promela.ypp" + { + (yyval.node) = ctx->node(PML_PLUS, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 59: + /* Line 1787 of yacc.c */ +#line 207 "promela.ypp" + { + (yyval.node) = ctx->node(PML_MINUS, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 60: + /* Line 1787 of yacc.c */ +#line 208 "promela.ypp" + { + (yyval.node) = ctx->node(PML_TIMES, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 61: + /* Line 1787 of yacc.c */ +#line 209 "promela.ypp" + { + (yyval.node) = ctx->node(PML_DIVIDE, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 62: + /* Line 1787 of yacc.c */ +#line 210 "promela.ypp" + { + (yyval.node) = ctx->node(PML_MODULO, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 63: + /* Line 1787 of yacc.c */ +#line 213 "promela.ypp" + { + (yyval.node) = ctx->value(PML_NAME, (void*)&((yylsp[(1) - (1)])), (yyvsp[(1) - (1)].value)); + free((yyvsp[(1) - (1)].value)); + } + break; + + case 64: + /* Line 1787 of yacc.c */ +#line 214 "promela.ypp" + { + if ((yyvsp[(1) - (2)].node)->type == PML_NAME) { + (yyval.node) = ctx->node(PML_NAMELIST, 1, (yyvsp[(1) - (2)].node)); + (yyval.node)->push(ctx->value(PML_NAME, (void*)&((yylsp[(2) - (2)])), (yyvsp[(2) - (2)].value))); + } else { + (yyvsp[(1) - (2)].node)->push(ctx->value(PML_NAME, (void*)&((yylsp[(2) - (2)])), (yyvsp[(2) - (2)].value))); + } + free((yyvsp[(2) - (2)].value)); + } + break; + + case 65: + /* Line 1787 of yacc.c */ +#line 223 "promela.ypp" + { + (yyval.node) = (yyvsp[(1) - (2)].node); + } + break; + + case 66: + /* Line 1787 of yacc.c */ +#line 226 "promela.ypp" + { + (yyval.node) = (yyvsp[(1) - (1)].node); + } + break; + + case 67: + /* Line 1787 of yacc.c */ +#line 227 "promela.ypp" + { + (yyval.node) = (yyvsp[(1) - (2)].node); + } + break; + + case 68: + /* Line 1787 of yacc.c */ +#line 228 "promela.ypp" + { + (yyval.node) = ctx->node(PML_STMNT, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 69: + /* Line 1787 of yacc.c */ +#line 231 "promela.ypp" + { + (yyval.node) = (yyvsp[(1) - (1)].node); + } + break; + + case 70: + /* Line 1787 of yacc.c */ +#line 234 "promela.ypp" + { + (yyval.node) = ctx->node(PML_ASGN, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + case 71: + /* Line 1787 of yacc.c */ +#line 235 "promela.ypp" + { + (yyval.node) = ctx->node(PML_INCR, 1, (yyvsp[(1) - (2)].node)); + } + break; + + case 72: + /* Line 1787 of yacc.c */ +#line 236 "promela.ypp" + { + (yyval.node) = ctx->node(PML_DECR, 1, (yyvsp[(1) - (2)].node)); + } + break; + + case 73: + /* Line 1787 of yacc.c */ +#line 237 "promela.ypp" + { + (yyval.node) = ctx->node(PML_PRINT, 2, ctx->value(PML_STRING, (void*)&((yylsp[(3) - (5)])), (yyvsp[(3) - (5)].value)), (yyvsp[(4) - (5)].node)); + free((yyvsp[(3) - (5)].value)); + } + break; + + case 74: + /* Line 1787 of yacc.c */ +#line 238 "promela.ypp" + { + (yyval.node) = ctx->node(PML_PRINT, 1, (yyvsp[(3) - (4)].node)); + } + break; + + case 75: + /* Line 1787 of yacc.c */ +#line 239 "promela.ypp" + { + (yyval.node) = ctx->node(PML_PRINT, 1, ctx->value(PML_CONST, (void*)&((yylsp[(3) - (4)])), (yyvsp[(3) - (4)].value))); + free((yyvsp[(3) - (4)].value)); + } + break; + + case 76: + /* Line 1787 of yacc.c */ +#line 240 "promela.ypp" + { + (yyval.node) = ctx->node(PML_ASSERT, 1, (yyvsp[(2) - (2)].node)); + } + break; + + case 77: + /* Line 1787 of yacc.c */ +#line 241 "promela.ypp" + { + (yyval.node) = (yyvsp[(1) - (1)].node); + } + break; + + case 78: + /* Line 1787 of yacc.c */ +#line 244 "promela.ypp" + { + (yyval.node) = ctx->value(0, NULL, ""); + } + break; + + case 79: + /* Line 1787 of yacc.c */ +#line 245 "promela.ypp" + { + (yyval.node) = (yyvsp[(2) - (2)].node); + } + break; + + case 80: + /* Line 1787 of yacc.c */ +#line 248 "promela.ypp" + { + (yyval.node) = (yyvsp[(1) - (1)].node); + } + break; + + case 81: + /* Line 1787 of yacc.c */ +#line 249 "promela.ypp" + { + (yyval.node) = ctx->node(0, 2, (yyvsp[(1) - (3)].node), (yyvsp[(3) - (3)].node)); + } + break; + + + /* Line 1787 of yacc.c */ +#line 2285 "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; + *++yylsp = yyloc; + + /* Now `shift' the result of the reduction. Determine what state + that goes to, based on the state we popped back to and the rule + 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 (&yylloc, 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 (&yylloc, ctx, scanner, yymsgp); + if (yysyntax_error_status == 2) + goto yyexhaustedlab; + } +# undef YYSYNTAX_ERROR +#endif + } + + yyerror_range[1] = yylloc; + + 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, &yylloc, 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; + + yyerror_range[1] = yylsp[1-yylen]; + /* 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; + + yyerror_range[1] = *yylsp; + yydestruct ("Error: popping", + yystos[yystate], yyvsp, yylsp, ctx, scanner); + YYPOPSTACK (1); + yystate = *yyssp; + YY_STACK_PRINT (yyss, yyssp); + } + + YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN + *++yyvsp = yylval; + YY_IGNORE_MAYBE_UNINITIALIZED_END + + yyerror_range[2] = yylloc; + /* Using YYLLOC is tempting, but would change the location of + the lookahead. YYLOC is available though. */ + YYLLOC_DEFAULT (yyloc, yyerror_range, 2); + *++yylsp = yyloc; + + /* Shift the error token. */ + YY_SYMBOL_PRINT ("Shifting", yystos[yyn], yyvsp, yylsp); + + 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 (&yylloc, 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, &yylloc, 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, yylsp, 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 253 "promela.ypp" + + diff --git a/src/uscxml/plugins/datamodel/promela/parser/promela.tab.hpp b/src/uscxml/plugins/datamodel/promela/parser/promela.tab.hpp new file mode 100644 index 0000000..a48031a --- /dev/null +++ b/src/uscxml/plugins/datamodel/promela/parser/promela.tab.hpp @@ -0,0 +1,180 @@ +/* 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 1 +# 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 { + PML_VAR_ARRAY = 258, + PML_VARLIST = 259, + PML_DECL = 260, + PML_DECLLIST = 261, + PML_STMNT = 262, + PML_COLON = 263, + PML_EXPR = 264, + PML_NAMELIST = 265, + PML_ASSERT = 266, + PML_PRINT = 267, + PML_PRINTM = 268, + PML_LEN = 269, + PML_STRING = 270, + PML_TYPEDEF = 271, + PML_MTYPE = 272, + PML_INLINE = 273, + PML_RETURN = 274, + PML_LABEL = 275, + PML_OF = 276, + PML_GOTO = 277, + PML_BREAK = 278, + PML_ELSE = 279, + PML_SEMI = 280, + PML_ARROW = 281, + PML_IF = 282, + PML_FI = 283, + PML_DO = 284, + PML_OD = 285, + PML_FOR = 286, + PML_SELECT = 287, + PML_IN = 288, + PML_SEP = 289, + PML_DOTDOT = 290, + PML_HIDDEN = 291, + PML_SHOW = 292, + PML_ISLOCAL = 293, + PML_CONST = 294, + PML_TYPE = 295, + PML_XU = 296, + PML_NAME = 297, + PML_UNAME = 298, + PML_PNAME = 299, + PML_INAME = 300, + PML_CLAIM = 301, + PML_TRACE = 302, + PML_INIT = 303, + PML_LTL = 304, + PML_COMMA = 305, + PML_ASGN = 306, + PML_AND = 307, + PML_OR = 308, + PML_BITAND = 309, + PML_BITXOR = 310, + PML_BITOR = 311, + PML_NE = 312, + PML_EQ = 313, + PML_LE = 314, + PML_GE = 315, + PML_LT = 316, + PML_GT = 317, + PML_RSHIFT = 318, + PML_LSHIFT = 319, + PML_MINUS = 320, + PML_PLUS = 321, + PML_MODULO = 322, + PML_DIVIDE = 323, + PML_TIMES = 324, + PML_DECR = 325, + PML_INCR = 326, + PML_COMPL = 327, + PML_NEG = 328, + PML_CMPND = 329, + PML_DOT = 330 + }; +#endif + + +#if ! defined PROMELA_STYPE && ! defined PROMELA_STYPE_IS_DECLARED +typedef union PROMELA_STYPE +{ +/* Line 2053 of yacc.c */ +#line 39 "promela.ypp" + + uscxml::PromelaParserNode* node; + char* value; + + +/* Line 2053 of yacc.c */ +#line 146 "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 + +#if ! defined PROMELA_LTYPE && ! defined PROMELA_LTYPE_IS_DECLARED +typedef struct PROMELA_LTYPE +{ + int first_line; + int first_column; + int last_line; + int last_column; +} PROMELA_LTYPE; +# define promela_ltype PROMELA_LTYPE /* obsolescent; will be withdrawn */ +# define PROMELA_LTYPE_IS_DECLARED 1 +# define PROMELA_LTYPE_IS_TRIVIAL 1 +#endif + + +#ifdef YYPARSE_PARAM +#if defined __STDC__ || defined __cplusplus +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..d76b24a --- /dev/null +++ b/src/uscxml/plugins/datamodel/promela/parser/promela.ypp @@ -0,0 +1,254 @@ +/** 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, PROMELA_LTYPE* yylloc_param, void* yyscanner); + +using namespace uscxml; +%} + +%pure-parser +%debug +%locations +%file-prefix "promela" +%parse-param { uscxml::PromelaParser* ctx } +%lex-param {void * scanner} +%parse-param {void * scanner} +%define api.prefix promela_ +%defines + +%union { + uscxml::PromelaParserNode* node; + char* value; +} + +%error-verbose + +/* %type <node> expr_lst */ +%type <node> expr pfld sfld varref decl_lst stmnt_lst vardcl ivar var_list one_decl prargs utype cmpnd +%type <node> stmnt Stmnt const_expr nlst vis arg + +%token PML_VAR_ARRAY PML_VARLIST PML_DECL PML_DECLLIST PML_STMNT PML_COLON PML_EXPR PML_NAMELIST + +%token '(' ')' +%token '[' ']' +%token '{' '}' +%token PML_ASSERT PML_PRINT PML_PRINTM +%token <value> PML_LEN PML_STRING +%token PML_TYPEDEF PML_MTYPE PML_INLINE PML_RETURN PML_LABEL PML_OF +%token PML_GOTO PML_BREAK PML_ELSE PML_SEMI PML_ARROW +%token PML_IF PML_FI PML_DO PML_OD PML_FOR PML_SELECT PML_IN PML_SEP PML_DOTDOT +%token PML_HIDDEN PML_SHOW PML_ISLOCAL +%token <value> PML_CONST PML_TYPE PML_XU /* val */ +%token <value> PML_NAME PML_UNAME PML_PNAME PML_INAME /* sym */ +%token PML_CLAIM PML_TRACE PML_INIT PML_LTL /* sym */ +%token PML_COMMA + +%right PML_ASGN +%left PML_OR PML_AND +%left PML_BITOR PML_BITXOR PML_BITAND +%left PML_EQ PML_NE +%left PML_GT PML_LT PML_GE PML_LE +%left PML_LSHIFT PML_RSHIFT +%left PML_PLUS PML_MINUS +%left PML_TIMES PML_DIVIDE PML_MODULO +%left PML_INCR PML_DECR +%left PML_COMPL +%right PML_NEG +%left PML_DOT PML_CMPND + +%% + + +/** PROMELA Grammar Rules **/ + +program : + decl_lst { + ctx->ast = $1; + ctx->type = PromelaParser::PROMELA_DECL; + } + | expr { + ctx->ast = $1; + ctx->type = PromelaParser::PROMELA_EXPR; + } + | stmnt_lst { + ctx->ast = $1; + ctx->type = PromelaParser::PROMELA_STMNT; + } + ; + +varref : cmpnd { $$ = $1; } + ; + +pfld : PML_NAME { $$ = ctx->value(PML_NAME, (void*)&(@1), $1); free($1); } + | PML_NAME '[' expr ']' { $$ = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, (void*)&(@1), $1), $3); free($1); } + ; + +cmpnd : pfld + sfld { + if ($2 != NULL) { + if ($2->type == PML_CMPND) { + $$ = ctx->node(PML_CMPND, 1, $1); + $$->merge($2); delete $2; + } else { + $$ = ctx->node(PML_CMPND, 2, $1, $2); + } + } else { + $$ = $1; + } + } + ; + +sfld : /* empty */ { $$ = NULL; } + | PML_DOT cmpnd %prec PML_DOT { $$ = $2; } + ; + +/* +expr_lst: expr { $$ = ctx->node(PML_EXPR, 1, $1); } + | expr PML_SEMI { $$ = ctx->node(PML_EXPR, 1, $1); } + | expr PML_SEMI expr_lst { $$ = ctx->node(PML_EXPR, 2, $1, $3); } + ; +*/ + +expr : '(' expr ')' { $$ = $2; } + | expr PML_PLUS expr { $$ = ctx->node(PML_PLUS, 2, $1, $3); } + | expr PML_MINUS expr { $$ = ctx->node(PML_MINUS, 2, $1, $3); } + | expr PML_TIMES expr { $$ = ctx->node(PML_TIMES, 2, $1, $3); } + | expr PML_DIVIDE expr { $$ = ctx->node(PML_DIVIDE, 2, $1, $3); } + | expr PML_MODULO expr { $$ = ctx->node(PML_MODULO, 2, $1, $3); } + | expr PML_BITAND expr { $$ = ctx->node(PML_BITAND, 2, $1, $3); } + | expr PML_BITXOR expr { $$ = ctx->node(PML_BITXOR, 2, $1, $3); } + | expr PML_BITOR expr { $$ = ctx->node(PML_BITOR, 2, $1, $3); } + | expr PML_GT expr { $$ = ctx->node(PML_GT, 2, $1, $3); } + | expr PML_LT expr { $$ = ctx->node(PML_LT, 2, $1, $3); } + | expr PML_GE expr { $$ = ctx->node(PML_GE, 2, $1, $3); } + | expr PML_LE expr { $$ = ctx->node(PML_LE, 2, $1, $3); } + | expr PML_EQ expr { $$ = ctx->node(PML_EQ, 2, $1, $3); } + | expr PML_NE expr { $$ = ctx->node(PML_NE, 2, $1, $3); } + | expr PML_AND expr { $$ = ctx->node(PML_AND, 2, $1, $3); } + | expr PML_OR expr { $$ = ctx->node(PML_OR, 2, $1, $3); } + | expr PML_LSHIFT expr { $$ = ctx->node(PML_LSHIFT, 2, $1, $3); } + | expr PML_RSHIFT expr { $$ = ctx->node(PML_RSHIFT, 2, $1, $3); } + | PML_NEG expr { $$ = ctx->node(PML_NEG, 1, $2); } + | PML_MINUS expr %prec PML_MINUS { $$ = ctx->node(PML_MINUS, 1, $2); } + + | PML_LEN '(' varref ')' { $$ = ctx->node(PML_LEN, 1, $3); } + | varref { $$ = $1; } + | PML_CONST { $$ = ctx->value(PML_CONST, (void*)&(@1), $1); free($1); } + | PML_STRING { + /* Non standard promela for string literals */ + $$ = ctx->value(PML_STRING, (void*)&(@1), $1); free($1); } + ; + + +vis : /* empty */ { $$ = ctx->node(PML_SHOW, 0); } + | PML_HIDDEN { $$ = ctx->node(PML_HIDDEN, 0); } + | PML_SHOW { $$ = ctx->node(PML_SHOW, 0); } + | PML_ISLOCAL { $$ = ctx->node(PML_ISLOCAL, 0); } + ; + +one_decl: vis PML_TYPE var_list { $$ = ctx->node(PML_DECL, 3, $1, ctx->value(PML_TYPE, (void*)&(@2), $2), $3); free($2); } + | vis PML_UNAME var_list { $$ = ctx->node(PML_UNAME, 2, $1, $3); } + | vis PML_TYPE PML_ASGN '{' nlst '}' { $$ = ctx->node(PML_DECL, 3, $1, ctx->value(PML_TYPE, (void*)&(@2), $2), $5); free($2); } + | vis utype { $$ = $2; } + ; + +utype : PML_TYPEDEF PML_NAME '{' decl_lst '}' { $$ = ctx->node(PML_TYPEDEF, 2, ctx->value(PML_NAME, (void*)&(@2), $2), $4); } + ; + +decl_lst: one_decl { $$ = $1; } + | one_decl PML_SEMI { $$ = $1; } + | one_decl PML_SEMI decl_lst { + $$ = ctx->node(PML_DECLLIST, 1, $1); + if($3->type == PML_DECLLIST) { + $$->merge($3); delete $3; + } else { + $$->push($3); + } + } + ; + +var_list: ivar { $$ = ctx->node(PML_VARLIST, 1, $1); } + | ivar PML_COMMA var_list { $$ = ctx->node(PML_VARLIST, 1, $1); $$->merge($3); delete $3; } + ; + +ivar : vardcl { $$ = $1; } + | vardcl PML_ASGN expr { $$ = ctx->node(PML_ASGN, 2, $1, $3); } + ; + +vardcl : PML_NAME { $$ = ctx->value(PML_NAME, (void*)&(@1), $1); free($1); } + | PML_NAME PML_COLON PML_CONST { $$ = ctx->node(PML_COLON, 2, ctx->value(PML_NAME, (void*)&(@1), $1), ctx->value(PML_CONST, (void*)&(@3), $3)); free($1); free($3); } + | PML_NAME '[' const_expr ']' { $$ = ctx->node(PML_VAR_ARRAY, 2, ctx->value(PML_NAME, (void*)&(@1), $1), $3); free($1); } + ; + +const_expr: PML_CONST { $$ = ctx->value(PML_CONST, (void*)&(@1), $1); free($1); } + | PML_MINUS const_expr %prec PML_MINUS { $$ = ctx->node(PML_MINUS, 1, $2); } + | '(' const_expr ')' { $$ = $2; } + | const_expr PML_PLUS const_expr { $$ = ctx->node(PML_PLUS, 2, $1, $3); } + | const_expr PML_MINUS const_expr { $$ = ctx->node(PML_MINUS, 2, $1, $3); } + | const_expr PML_TIMES const_expr { $$ = ctx->node(PML_TIMES, 2, $1, $3); } + | const_expr PML_DIVIDE const_expr { $$ = ctx->node(PML_DIVIDE, 2, $1, $3); } + | const_expr PML_MODULO const_expr { $$ = ctx->node(PML_MODULO, 2, $1, $3); } + ; + +nlst : PML_NAME { $$ = ctx->value(PML_NAME, (void*)&(@1), $1); free($1); } + | nlst PML_NAME { + if ($1->type == PML_NAME) { + $$ = ctx->node(PML_NAMELIST, 1, $1); + $$->push(ctx->value(PML_NAME, (void*)&(@2), $2)); + } else { + $1->push(ctx->value(PML_NAME, (void*)&(@2), $2)); + } + free($2); + } + | nlst PML_COMMA { $$ = $1; } + ; + +stmnt_lst: stmnt { $$ = $1; } + | stmnt PML_SEMI { $$ = $1; } + | stmnt PML_SEMI stmnt_lst { $$ = ctx->node(PML_STMNT, 2, $1, $3); } + ; + +stmnt : Stmnt { $$ = $1; } + ; + +Stmnt : varref PML_ASGN expr { $$ = ctx->node(PML_ASGN, 2, $1, $3); } + | varref PML_INCR { $$ = ctx->node(PML_INCR, 1, $1); } + | varref PML_DECR { $$ = ctx->node(PML_DECR, 1, $1); } + | PML_PRINT '(' PML_STRING prargs ')' { $$ = ctx->node(PML_PRINT, 2, ctx->value(PML_STRING, (void*)&(@3), $3), $4); free($3); } + | PML_PRINT '(' varref ')' { $$ = ctx->node(PML_PRINT, 1, $3); } + | PML_PRINT '(' PML_CONST ')' { $$ = ctx->node(PML_PRINT, 1, ctx->value(PML_CONST, (void*)&(@3), $3)); free($3); } + | PML_ASSERT expr { $$ = ctx->node(PML_ASSERT, 1, $2); } + | expr { $$ = $1; } + ; + +prargs : /* empty */ { $$ = ctx->value(0, NULL, ""); } + | PML_COMMA arg { $$ = $2; } + ; + +arg : expr { $$ = $1; } + | expr PML_COMMA arg { $$ = ctx->node(0, 2, $1, $3); } + ; + + +%% + diff --git a/src/uscxml/plugins/invoker/dirmon/DirMonInvoker.cpp b/src/uscxml/plugins/invoker/dirmon/DirMonInvoker.cpp index f3b429f..08a0be8 100644 --- a/src/uscxml/plugins/invoker/dirmon/DirMonInvoker.cpp +++ b/src/uscxml/plugins/invoker/dirmon/DirMonInvoker.cpp @@ -134,8 +134,8 @@ void DirMonInvoker::invoke(const std::string& source, const Event& req) { std::multimap<std::string, Data>::const_iterator dirIter = req.params.find("dir"); while(dirIter != req.params.upper_bound("dir")) { // this is simplified - Data might be more elaborate than a simple string atom - URL url = URL::resolve(dirIter->second.atom, _interpreter->getBaseURL()); - + URL url = URL::resolve(dirIter->second.atom, _interpreter->getBaseURL()); + if (!url.isAbsolute()) { LOG(ERROR) << "Given directory '" << dirIter->second << "' cannot be transformed to absolute path"; } else { @@ -153,13 +153,13 @@ void DirMonInvoker::invoke(const std::string& source, const Event& req) { } void DirMonInvoker::uninvoke() { - _isRunning = false; - if (_thread) { - _thread->join(); - delete _thread; - } + _isRunning = false; + if (_thread) { + _thread->join(); + delete _thread; + } } - + void DirMonInvoker::run(void* instance) { while(((DirMonInvoker*)instance)->_isRunning) { { diff --git a/src/uscxml/plugins/invoker/dirmon/DirMonInvoker.h b/src/uscxml/plugins/invoker/dirmon/DirMonInvoker.h index be510d9..6e13864 100644 --- a/src/uscxml/plugins/invoker/dirmon/DirMonInvoker.h +++ b/src/uscxml/plugins/invoker/dirmon/DirMonInvoker.h @@ -107,9 +107,9 @@ public: } virtual Data getDataModelVariables(); - virtual void eventFromSCXML(const Event& event); - virtual void invoke(const std::string& source, const Event& invokeEvent); - virtual void uninvoke(); + virtual void eventFromSCXML(const Event& event); + virtual void invoke(const std::string& source, const Event& invokeEvent); + virtual void uninvoke(); virtual void handleChanges(DirectoryWatch::Action action, const std::string dir, const std::string file, struct stat fileStat); diff --git a/src/uscxml/plugins/ioprocessor/basichttp/BasicHTTPIOProcessor.cpp b/src/uscxml/plugins/ioprocessor/basichttp/BasicHTTPIOProcessor.cpp index 317b94c..564977d 100644 --- a/src/uscxml/plugins/ioprocessor/basichttp/BasicHTTPIOProcessor.cpp +++ b/src/uscxml/plugins/ioprocessor/basichttp/BasicHTTPIOProcessor.cpp @@ -200,8 +200,8 @@ void BasicHTTPIOProcessor::eventFromSCXML(const std::string& target, const Event kvps << kvpSeperator << eventNameCStr << "=" << eventValueCStr; kvpSeperator = "&"; targetURL.addOutHeader("_scxmleventname", eventValueCStr); - free(eventNameCStr); - free(eventValueCStr); + free(eventNameCStr); + free(eventValueCStr); } // event namelist |