diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index 24dba6d27..e9f4263d6 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -45,8 +45,8 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { std::shared_ptr stateLabeling = this->getStateLabeling(this->program->getLabels()); std::shared_ptr> stateRewards = nullptr; - if (this->rewardModel.hasStateRewards()) { - stateRewards = this->getStateRewards(this->rewardModel.getStateRewards()); + if (this->rewardModel->hasStateRewards()) { + stateRewards = this->getStateRewards(this->rewardModel->getStateRewards()); } switch (this->program->getModelType()) @@ -90,11 +90,11 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { std::get<1>(*state)[index] = value; } - std::shared_ptr> ExplicitModelAdapter::getStateRewards(std::vector const & rewards) { + std::shared_ptr> ExplicitModelAdapter::getStateRewards(std::vector> const & rewards) { std::shared_ptr> results(new std::vector(this->allStates.size())); for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { for (auto reward: rewards) { - (*results)[index] = reward.getReward(this->allStates[index]); + (*results)[index] = reward->getReward(this->allStates[index]); } } return results; @@ -119,8 +119,8 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { uint_fast64_t numberOfIntegerVariables = 0; uint_fast64_t numberOfBooleanVariables = 0; for (uint_fast64_t i = 0; i < program->getNumberOfModules(); ++i) { - numberOfIntegerVariables += program->getModule(i).getNumberOfIntegerVariables(); - numberOfBooleanVariables += program->getModule(i).getNumberOfBooleanVariables(); + numberOfIntegerVariables += program->getModule(i)->getNumberOfIntegerVariables(); + numberOfBooleanVariables += program->getModule(i)->getNumberOfBooleanVariables(); } this->booleanVariables.resize(numberOfBooleanVariables); @@ -129,16 +129,16 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { uint_fast64_t nextBooleanVariableIndex = 0; uint_fast64_t nextIntegerVariableIndex = 0; for (uint_fast64_t i = 0; i < program->getNumberOfModules(); ++i) { - storm::ir::Module const& module = program->getModule(i); + std::shared_ptr const module = program->getModule(i); - for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { - this->booleanVariables[nextBooleanVariableIndex] = module.getBooleanVariable(j); - this->booleanVariableToIndexMap[module.getBooleanVariable(j).getName()] = nextBooleanVariableIndex; + for (uint_fast64_t j = 0; j < module->getNumberOfBooleanVariables(); ++j) { + this->booleanVariables[nextBooleanVariableIndex] = module->getBooleanVariable(j); + this->booleanVariableToIndexMap[module->getBooleanVariable(j).getName()] = nextBooleanVariableIndex; ++nextBooleanVariableIndex; } - for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { - this->integerVariables[nextIntegerVariableIndex] = module.getIntegerVariable(j); - this->integerVariableToIndexMap[module.getIntegerVariable(j).getName()] = nextIntegerVariableIndex; + for (uint_fast64_t j = 0; j < module->getNumberOfIntegerVariables(); ++j) { + this->integerVariables[nextIntegerVariableIndex] = module->getIntegerVariable(j); + this->integerVariableToIndexMap[module->getIntegerVariable(j).getName()] = nextIntegerVariableIndex; ++nextIntegerVariableIndex; } } @@ -157,28 +157,28 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { * @param action Action label. * @return Active commands. */ - std::unique_ptr>> ExplicitModelAdapter::getActiveCommandsByAction(StateType const * state, std::string& action) { - std::unique_ptr>> res = std::unique_ptr>>(new std::list>()); + std::unique_ptr>>> ExplicitModelAdapter::getActiveCommandsByAction(StateType const * state, std::string& action) { + std::unique_ptr>>> res = std::unique_ptr>>>(new std::list>>()); // Iterate over all modules. for (uint_fast64_t i = 0; i < this->program->getNumberOfModules(); ++i) { - storm::ir::Module const& module = this->program->getModule(i); + std::shared_ptr const module = this->program->getModule(i); - std::shared_ptr> ids = module.getCommandsByAction(action); - std::list commands; + std::shared_ptr> ids = module->getCommandsByAction(action); + std::list> commands; // Look up commands by their id. Add, if guard holds. for (uint_fast64_t id : *ids) { - storm::ir::Command cmd = module.getCommand(id); - if (cmd.getGuard()->getValueAsBool(state)) { - commands.push_back(module.getCommand(id)); + std::shared_ptr cmd = module->getCommand(id); + if (cmd->getGuard()->getValueAsBool(state)) { + commands.push_back(module->getCommand(id)); } } res->push_back(commands); } // Sort the result in the vague hope that having small lists at the beginning will speed up the expanding. // This is how lambdas may look like in C++... - res->sort([](const std::list& a, const std::list& b){ return a.size() < b.size(); }); + res->sort([](const std::list>& a, const std::list>& b){ return a.size() < b.size(); }); return res; } @@ -188,12 +188,12 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { * @params update Update to be applied. * @return Resulting state. */ - StateType* ExplicitModelAdapter::applyUpdate(StateType const * const state, storm::ir::Update const & update) const { + StateType* ExplicitModelAdapter::applyUpdate(StateType const * const state, std::shared_ptr const update) const { StateType* newState = new StateType(*state); - for (auto assignedVariable : update.getBooleanAssignments()) { + for (auto assignedVariable : update->getBooleanAssignments()) { setValue(newState, this->booleanVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsBool(state)); } - for (auto assignedVariable : update.getIntegerAssignments()) { + for (auto assignedVariable : update->getIntegerAssignments()) { setValue(newState, this->integerVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsInt(state)); } return newState; @@ -291,32 +291,32 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { const StateType* state = this->allStates[stateID]; // Iterate over all modules. for (uint_fast64_t i = 0; i < program->getNumberOfModules(); ++i) { - storm::ir::Module const& module = program->getModule(i); + std::shared_ptr const module = program->getModule(i); // Iterate over all commands. - for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) { - storm::ir::Command const& command = module.getCommand(j); + for (uint_fast64_t j = 0; j < module->getNumberOfCommands(); ++j) { + std::shared_ptr const command = module->getCommand(j); // Only consider unlabeled commands. - if (command.getActionName() != "") continue; + if (command->getActionName() != "") continue; // Omit, if command is not active. - if (!command.getGuard()->getValueAsBool(state)) continue; + if (!command->getGuard()->getValueAsBool(state)) continue; // Add a new map and get pointer. res.emplace_back(); std::map* states = &res.back().second; // Iterate over all updates. - for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { + for (uint_fast64_t k = 0; k < command->getNumberOfUpdates(); ++k) { // Obtain new state id. - storm::ir::Update const& update = command.getUpdate(k); + std::shared_ptr const update = command->getUpdate(k); uint_fast64_t newStateId = this->getOrAddStateId(this->applyUpdate(state, update)); // Check, if we already know this state, add up probabilities for every state. auto stateIt = states->find(newStateId); if (stateIt == states->end()) { - (*states)[newStateId] = update.getLikelihoodExpression()->getValueAsDouble(state); + (*states)[newStateId] = update->getLikelihoodExpression()->getValueAsDouble(state); this->numberOfTransitions++; } else { - (*states)[newStateId] += update.getLikelihoodExpression()->getValueAsDouble(state); + (*states)[newStateId] += update->getLikelihoodExpression()->getValueAsDouble(state); } } } @@ -333,21 +333,21 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { // Create a copy of the current state, as we will free intermediate states... for (std::string action : this->program->getActions()) { StateType* state = new StateType(*this->allStates[stateID]); - std::unique_ptr>> cmds = this->getActiveCommandsByAction(state, action); + std::unique_ptr>>> cmds = this->getActiveCommandsByAction(state, action); // Start with current state std::unordered_map resultStates; resultStates[state] = 1.0; - for (std::list module : *cmds) { + for (std::list> module : *cmds) { if (resultStates.size() == 0) break; std::unordered_map newStates; // Iterate over all commands within this module. - for (storm::ir::Command command : module) { + for (std::shared_ptr command : module) { // Iterate over all updates of this command. - for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { - storm::ir::Update const& update = command.getUpdate(k); + for (uint_fast64_t k = 0; k < command->getNumberOfUpdates(); ++k) { + std::shared_ptr const update = command->getUpdate(k); // Iterate over all resultStates. for (auto it : resultStates) { @@ -357,9 +357,9 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { // Take care of calculation of likelihood, combine identical states. auto s = newStates.find(newState); if (s == newStates.end()) { - newStates[newState] = it.second * update.getLikelihoodExpression()->getValueAsDouble(it.first); + newStates[newState] = it.second * update->getLikelihoodExpression()->getValueAsDouble(it.first); } else { - newStates[newState] += it.second * update.getLikelihoodExpression()->getValueAsDouble(it.first); + newStates[newState] += it.second * update->getLikelihoodExpression()->getValueAsDouble(it.first); } } } @@ -413,7 +413,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { std::shared_ptr> result(new storm::storage::SparseMatrix(allStates.size())); result->initialize(numberOfTransitions); - if (this->rewardModel.hasTransitionRewards()) { + if (this->rewardModel->hasTransitionRewards()) { this->transitionRewards = std::shared_ptr>(new storm::storage::SparseMatrix(allStates.size())); this->transitionRewards->initialize(numberOfTransitions); } @@ -427,9 +427,9 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { for (auto choice : transitionMap[state]) { for (auto elem : choice.second) { map[elem.first] += elem.second; - if (this->rewardModel.hasTransitionRewards()) { - for (storm::ir::TransitionReward reward : this->rewardModel.getTransitionRewards()) { - rewardMap[elem.first] += reward.getReward(choice.first, this->allStates[state]); + if (this->rewardModel->hasTransitionRewards()) { + for (auto reward : this->rewardModel->getTransitionRewards()) { + rewardMap[elem.first] += reward->getReward(choice.first, this->allStates[state]); } } } @@ -438,7 +438,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { double factor = 1.0 / transitionMap[state].size(); for (auto it : map) { result->addNextValue(state, it.first, it.second * factor); - if (this->rewardModel.hasTransitionRewards()) { + if (this->rewardModel->hasTransitionRewards()) { this->transitionRewards->addNextValue(state, it.first, rewardMap[it.first] * factor); } } @@ -458,7 +458,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { LOG4CPLUS_DEBUG(logger, "Building nondeterministic transition matrix with " << this->numberOfChoices << " choices and " << this->numberOfTransitions << " transitions now."); std::shared_ptr> result(new storm::storage::SparseMatrix(allStates.size(), this->numberOfChoices)); result->initialize(this->numberOfTransitions); - if (this->rewardModel.hasTransitionRewards()) { + if (this->rewardModel->hasTransitionRewards()) { this->transitionRewards = std::shared_ptr>(new storm::storage::SparseMatrix(allStates.size(), this->numberOfChoices)); this->transitionRewards->initialize(this->numberOfTransitions); } @@ -468,10 +468,10 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { for (auto choice : transitionMap[state]) { for (auto it : choice.second) { result->addNextValue(nextRow, it.first, it.second); - if (this->rewardModel.hasTransitionRewards()) { + if (this->rewardModel->hasTransitionRewards()) { double rewardValue = 0; - for (storm::ir::TransitionReward reward : this->rewardModel.getTransitionRewards()) { - rewardValue = reward.getReward(choice.first, this->allStates[state]); + for (auto reward : this->rewardModel->getTransitionRewards()) { + rewardValue = reward->getReward(choice.first, this->allStates[state]); } this->transitionRewards->addNextValue(nextRow, it.first, rewardValue); } diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 03214d165..962bfa6d8 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -83,7 +83,7 @@ private: * @params update Update to be applied. * @return Resulting state. */ - StateType* applyUpdate(StateType const * const state, storm::ir::Update const & update) const; + StateType* applyUpdate(StateType const * const state, std::shared_ptr const update) const; /*! * Reads and combines variables from all program modules and stores them. @@ -91,7 +91,7 @@ private: */ void initializeVariables(); - std::shared_ptr> getStateRewards(std::vector const & rewards); + std::shared_ptr> getStateRewards(std::vector> const & rewards); std::shared_ptr getStateLabeling(std::map> labels); /*! @@ -107,7 +107,7 @@ private: * @param action Action label. * @return Active commands. */ - std::unique_ptr>> getActiveCommandsByAction(StateType const * state, std::string& action); + std::unique_ptr>>> getActiveCommandsByAction(StateType const * state, std::string& action); /*! * Generates all initial states and adds them to allStates. @@ -173,7 +173,7 @@ private: std::map integerVariableToIndexMap; // Members that are filled during the conversion. - storm::ir::RewardModel rewardModel; + std::shared_ptr rewardModel; std::vector allStates; std::unordered_map stateToIndexMap; uint_fast64_t numberOfTransitions; diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp index b34ab60ed..ea2141bf0 100644 --- a/src/ir/Command.cpp +++ b/src/ir/Command.cpp @@ -8,6 +8,7 @@ #include "Command.h" #include +#include namespace storm { @@ -19,19 +20,22 @@ Command::Command() : actionName(), guardExpression(), updates() { } // Initializes all members according to the given values. -Command::Command(std::string actionName, std::shared_ptr guardExpression, std::vector updates) +Command::Command(std::string actionName, std::shared_ptr guardExpression, std::vector> updates) : actionName(actionName), guardExpression(guardExpression), updates(updates) { // Nothing to do here. } Command::Command(const Command& cmd, const std::map& renaming, const std::map& bools, const std::map& ints) : actionName(cmd.actionName), guardExpression(cmd.guardExpression->clone(renaming, bools, ints)) { + std::cout << "Cloning command" << std::endl; + std::cout << cmd.guardExpression->dump("\t"); + std::cout << this->guardExpression->dump("\t"); if (renaming.count(this->actionName) > 0) { this->actionName = renaming.at(this->actionName); } this->updates.reserve(cmd.updates.size()); - for (Update u : cmd.updates) { - this->updates.emplace_back(u, renaming, bools, ints); + for (std::shared_ptr u : cmd.updates) { + this->updates.emplace_back(new Update(*u, renaming, bools, ints)); } } @@ -51,7 +55,7 @@ uint_fast64_t Command::getNumberOfUpdates() const { } // Return the requested update. -storm::ir::Update const& Command::getUpdate(uint_fast64_t index) const { +std::shared_ptr const& Command::getUpdate(uint_fast64_t index) const { return this->updates[index]; } @@ -60,7 +64,7 @@ std::string Command::toString() const { std::stringstream result; result << "[" << actionName << "] " << guardExpression->toString() << " -> "; for (uint_fast64_t i = 0; i < updates.size(); ++i) { - result << updates[i].toString(); + result << updates[i]->toString(); if (i < updates.size() - 1) { result << " + "; } diff --git a/src/ir/Command.h b/src/ir/Command.h index b4049307c..4e3da7f65 100644 --- a/src/ir/Command.h +++ b/src/ir/Command.h @@ -34,7 +34,7 @@ public: * @param actionName the action name of the command. * @param guardExpression the expression that defines the guard of the command. */ - Command(std::string actionName, std::shared_ptr guardExpression, std::vector updates); + Command(std::string actionName, std::shared_ptr guardExpression, std::vector> updates); Command(const Command& cmd, const std::map& renaming, const std::map& bools, const std::map& ints); /*! @@ -59,7 +59,7 @@ public: * Retrieves a reference to the update with the given index. * @returns a reference to the update with the given index. */ - storm::ir::Update const& getUpdate(uint_fast64_t index) const; + std::shared_ptr const& getUpdate(uint_fast64_t index) const; /*! * Retrieves a string representation of this command. @@ -75,7 +75,7 @@ private: std::shared_ptr guardExpression; // The list of updates of the command. - std::vector updates; + std::vector> updates; }; } // namespace ir diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index 592c92164..c3049a0ea 100644 --- a/src/ir/Module.cpp +++ b/src/ir/Module.cpp @@ -27,29 +27,31 @@ Module::Module(std::string moduleName, std::vector b std::vector integerVariables, std::map booleanVariableToIndexMap, std::map integerVariableToIndexMap, - std::vector commands) + std::vector> commands) : moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), booleanVariablesToIndexMap(booleanVariableToIndexMap), integerVariablesToIndexMap(integerVariableToIndexMap), commands(commands), actions(), actionsToCommandIndexMap() { + std::cout << "Created module " << this << ":" << std::endl << this->toString() << std::endl; this->collectActions(); } -Module::Module(const Module& module, const std::string& moduleName, const std::map& renaming, const VariableAdder& adder) +Module::Module(const Module& module, const std::string& moduleName, const std::map& renaming, std::shared_ptr adder) : moduleName(moduleName) { std::cout << "Renaming module " << module.moduleName << " to " << moduleName << " with " << renaming.size() << " renamings:" << std::endl; for (auto it: renaming) { std::cout << "\t" << it.first << " -> " << it.second << std::endl; } + std::cout << "Current module " << &module << ":" << std::endl << module.toString() << std::endl; this->booleanVariables.reserve(module.booleanVariables.size()); for (BooleanVariable it: module.booleanVariables) { if (renaming.count(it.getName()) > 0) { - this->booleanVariablesToIndexMap[renaming.at(it.getName())] = adder.addBooleanVariable(it.getName(), it.getInitialValue()); + this->booleanVariablesToIndexMap[renaming.at(it.getName())] = adder->addBooleanVariable(renaming.at(it.getName()), it.getInitialValue()); } else std::cerr << "ERROR: " << moduleName << "." << it.getName() << " was not renamed!" << std::endl; } this->integerVariables.reserve(module.integerVariables.size()); for (IntegerVariable it: module.integerVariables) { if (renaming.count(it.getName()) > 0) { - this->integerVariablesToIndexMap[renaming.at(it.getName())] = adder.addIntegerVariable(it.getName(), it.getLowerBound(), it.getUpperBound(), it.getInitialValue()); + this->integerVariablesToIndexMap[renaming.at(it.getName())] = adder->addIntegerVariable(renaming.at(it.getName()), it.getLowerBound(), it.getUpperBound(), it.getInitialValue()); } else std::cerr << "ERROR: " << moduleName << "." << it.getName() << " was not renamed!" << std::endl; } this->booleanVariables.reserve(module.booleanVariables.size()); @@ -66,8 +68,9 @@ Module::Module(const Module& module, const std::string& moduleName, const std::m } this->commands.reserve(module.commands.size()); - for (Command cmd: module.commands) { - this->commands.emplace_back(cmd, renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap); + for (std::shared_ptr cmd: module.commands) { + std::cout << "2: Current command: " << cmd->toString() << std::endl; + this->commands.emplace_back(new Command(*cmd, renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap)); } this->collectActions(); @@ -119,7 +122,7 @@ uint_fast64_t Module::getIntegerVariableIndex(std::string variableName) const { } // Return the requested command. -storm::ir::Command const& Module::getCommand(uint_fast64_t index) const { +std::shared_ptr const Module::getCommand(uint_fast64_t index) const { return this->commands[index]; } @@ -134,7 +137,7 @@ std::string Module::toString() const { result << "\t" << variable.toString() << std::endl; } for (auto command : commands) { - result << "\t" << command.toString() << std::endl; + result << "\t" << command->toString() << std::endl; } result << "endmodule" << std::endl; return result.str(); @@ -157,7 +160,7 @@ std::shared_ptr> const Module::getCommandsByAction(std:: void Module::collectActions() { for (unsigned int id = 0; id < this->commands.size(); id++) { - std::string action = this->commands[id].getActionName(); + std::string action = this->commands[id]->getActionName(); if (action != "") { if (this->actionsToCommandIndexMap.count(action) == 0) { this->actionsToCommandIndexMap[action] = std::shared_ptr>(new std::set()); diff --git a/src/ir/Module.h b/src/ir/Module.h index 8991062ec..2a97a2ab3 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -23,8 +23,8 @@ namespace storm { namespace ir { struct VariableAdder { - virtual uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper, const std::shared_ptr init) const = 0; - virtual uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr init) const = 0; + virtual uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper, const std::shared_ptr init) = 0; + virtual uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr init) = 0; }; /*! @@ -48,7 +48,7 @@ public: std::vector integerVariables, std::map booleanVariableToIndexMap, std::map integerVariableToIndexMap, - std::vector commands); + std::vector> commands); typedef uint_fast64_t (*addIntegerVariablePtr)(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper, const std::shared_ptr init); typedef uint_fast64_t (*addBooleanVariablePtr)(const std::string& name, const std::shared_ptr init); @@ -60,7 +60,7 @@ public: * @param moduleName Name of the new module. * @param renaming Renaming map. */ - Module(const Module& module, const std::string& moduleName, const std::map& renaming, const VariableAdder& adder); + Module(const Module& module, const std::string& moduleName, const std::map& renaming, std::shared_ptr adder); /*! * Retrieves the number of boolean variables in the module. @@ -110,7 +110,7 @@ public: * Retrieves a reference to the command with the given index. * @returns a reference to the command with the given index. */ - storm::ir::Command const& getCommand(uint_fast64_t index) const; + std::shared_ptr const getCommand(uint_fast64_t index) const; /*! * Retrieves a string representation of this variable. @@ -152,7 +152,7 @@ private: std::map integerVariablesToIndexMap; // The commands associated with the module. - std::vector commands; + std::vector> commands; // The set of actions present in this module. std::set actions; diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index 8e5306e71..01a77298f 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -24,11 +24,11 @@ Program::Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions() } // Initializes all members according to the given values. -Program::Program(ModelType modelType, std::map> booleanUndefinedConstantExpressions, std::map> integerUndefinedConstantExpressions, std::map> doubleUndefinedConstantExpressions, std::vector modules, std::map rewards, std::map> labels) +Program::Program(ModelType modelType, std::map> booleanUndefinedConstantExpressions, std::map> integerUndefinedConstantExpressions, std::map> doubleUndefinedConstantExpressions, std::vector> modules, std::map> rewards, std::map> labels) : modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards), labels(labels), actionsToModuleIndexMap() { // Build actionsToModuleIndexMap for (unsigned int id = 0; id < this->modules.size(); id++) { - for (auto action : this->modules[id].getActions()) { + for (auto action : this->modules[id]->getActions()) { if (this->actionsToModuleIndexMap.count(action) == 0) { this->actionsToModuleIndexMap[action] = std::shared_ptr>(new std::set()); } @@ -55,22 +55,22 @@ std::string Program::toString() const { result << std::endl; for (auto element : booleanUndefinedConstantExpressions) { - result << "const bool " << element.first << ";" << std::endl; + result << "const bool " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; } for (auto element : integerUndefinedConstantExpressions) { - result << "const int " << element.first << ";" << std::endl; + result << "const int " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; } for (auto element : doubleUndefinedConstantExpressions) { - result << "const double " << element.first << ";" << std::endl; + result << "const double " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; } result << std::endl; - for (auto mod : modules) { - result << mod.toString() << std::endl; + for (auto module : modules) { + result << module->toString() << std::endl; } for (auto rewardModel : rewards) { - result << rewardModel.second.toString() << std::endl; + result << rewardModel.first << ": " << rewardModel.second->toString() << std::endl; } for (auto label : labels) { @@ -84,7 +84,7 @@ uint_fast64_t Program::getNumberOfModules() const { return this->modules.size(); } -storm::ir::Module const& Program::getModule(uint_fast64_t index) const { +std::shared_ptr const& Program::getModule(uint_fast64_t index) const { return this->modules[index]; } @@ -103,11 +103,11 @@ std::shared_ptr> const Program::getModulesByAction(std:: } } -storm::ir::RewardModel Program::getRewardModel(std::string const & name) const { +std::shared_ptr Program::getRewardModel(std::string const & name) const { auto it = this->rewards.find(name); if (it == this->rewards.end()) { LOG4CPLUS_ERROR(logger, "The given reward model \"" << name << "\" does not exist. We will proceed without rewards."); - return RewardModel(); + return nullptr; } else { return it->second; } diff --git a/src/ir/Program.h b/src/ir/Program.h index b6daecdd7..d51ebeb0e 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -53,7 +53,14 @@ public: * @param rewards The reward models of the program. * @param labels The labels defined for this model. */ - Program(ModelType modelType, std::map> booleanUndefinedConstantExpressions, std::map> integerUndefinedConstantExpressions, std::map> doubleUndefinedConstantExpressions, std::vector modules, std::map rewards, std::map> labels); + Program( + ModelType modelType, + std::map> booleanUndefinedConstantExpressions, + std::map> integerUndefinedConstantExpressions, + std::map> doubleUndefinedConstantExpressions, + std::vector> modules, + std::map> rewards, + std::map> labels); /*! * Retrieves the number of modules in the program. @@ -65,7 +72,7 @@ public: * Retrieves a reference to the module with the given index. * @param index the index of the module to retrieve. */ - storm::ir::Module const& getModule(uint_fast64_t index) const; + std::shared_ptr const& getModule(uint_fast64_t index) const; /*! * Retrieves the model type of the model. @@ -98,7 +105,7 @@ public: * @param name Name of the reward model. * @return Reward model with given name. */ - storm::ir::RewardModel getRewardModel(std::string const & name) const; + std::shared_ptr getRewardModel(std::string const & name) const; /*! * Retrieves all labels. @@ -120,10 +127,10 @@ private: std::map> doubleUndefinedConstantExpressions; // The modules associated with the program. - std::vector modules; + std::vector> modules; // The reward models associated with the program. - std::map rewards; + std::map> rewards; // The labels that are defined for this model. std::map> labels; diff --git a/src/ir/RewardModel.cpp b/src/ir/RewardModel.cpp index d6611e4ec..352c8614c 100644 --- a/src/ir/RewardModel.cpp +++ b/src/ir/RewardModel.cpp @@ -19,7 +19,7 @@ RewardModel::RewardModel() : rewardModelName(), stateRewards(), transitionReward } // Initializes all members according to the given values. -RewardModel::RewardModel(std::string rewardModelName, std::vector stateRewards, std::vector transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) { +RewardModel::RewardModel(std::string rewardModelName, std::vector> stateRewards, std::vector> transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) { // Nothing to do here. } @@ -28,10 +28,10 @@ std::string RewardModel::toString() const { std::stringstream result; result << "rewards \"" << rewardModelName << "\"" << std::endl; for (auto reward : stateRewards) { - result << reward.toString() << std::endl; + result << reward->toString() << std::endl; } for (auto reward : transitionRewards) { - result << reward.toString() << std::endl; + result << reward->toString() << std::endl; } result << "endrewards" << std::endl; return result.str(); @@ -41,7 +41,7 @@ bool RewardModel::hasStateRewards() const { return this->stateRewards.size() > 0; } -std::vector RewardModel::getStateRewards() const { +std::vector> RewardModel::getStateRewards() const { return this->stateRewards; } @@ -49,7 +49,7 @@ bool RewardModel::hasTransitionRewards() const { return this->transitionRewards.size() > 0; } -std::vector RewardModel::getTransitionRewards() const { +std::vector> RewardModel::getTransitionRewards() const { return this->transitionRewards; } diff --git a/src/ir/RewardModel.h b/src/ir/RewardModel.h index cb538f173..29029a4db 100644 --- a/src/ir/RewardModel.h +++ b/src/ir/RewardModel.h @@ -34,7 +34,7 @@ public: * @param stateRewards A vector of state-based reward. * @param transitionRewards A vector of transition-based reward. */ - RewardModel(std::string rewardModelName, std::vector stateRewards, std::vector transitionRewards); + RewardModel(std::string rewardModelName, std::vector> stateRewards, std::vector> transitionRewards); /*! * Retrieves a string representation of this variable. @@ -52,7 +52,7 @@ public: * Retrieve state rewards. * @return State rewards. */ - std::vector getStateRewards() const; + std::vector> getStateRewards() const; /*! * Check, if there are any transition rewards. @@ -64,17 +64,17 @@ public: * Retrieve transition rewards. * @return Transition rewards. */ - std::vector getTransitionRewards() const; + std::vector> getTransitionRewards() const; private: // The name of the reward model. std::string rewardModelName; // The state-based rewards associated with this reward model. - std::vector stateRewards; + std::vector> stateRewards; // The transition-based rewards associated with this reward model. - std::vector transitionRewards; + std::vector> transitionRewards; }; } // namespace ir diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h index 563037266..a8d3377a9 100644 --- a/src/ir/expressions/BaseExpression.h +++ b/src/ir/expressions/BaseExpression.h @@ -86,6 +86,8 @@ public: ReturnType getType() const { return type; } + + virtual std::string dump(std::string prefix) const = 0; private: ReturnType type; diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.h b/src/ir/expressions/BinaryBooleanFunctionExpression.h index dc1dc1147..4882c0d92 100644 --- a/src/ir/expressions/BinaryBooleanFunctionExpression.h +++ b/src/ir/expressions/BinaryBooleanFunctionExpression.h @@ -65,6 +65,18 @@ public: return result.str(); } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "BinaryBooleanFunctionExpression" << std::endl; + result << this->getLeft()->dump(prefix + "\t"); + switch (functionType) { + case AND: result << prefix << "&" << std::endl; break; + case OR: result << prefix << "|" << std::endl; break; + } + result << this->getRight()->dump(prefix + "\t"); + return result.str(); + } private: FunctionType functionType; diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h index 49d2c9494..151c10062 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.h +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.h @@ -86,6 +86,20 @@ public: return result; } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "BinaryNumericalFunctionExpression" << std::endl; + result << this->getLeft()->dump(prefix + "\t"); + switch (functionType) { + case PLUS: result << prefix << "+" << std::endl; break; + case MINUS: result << prefix << "-" << std::endl; break; + case TIMES: result << prefix << "*" << std::endl; break; + case DIVIDE: result << prefix << "/" << std::endl; break; + } + result << this->getRight()->dump(prefix + "\t"); + return result.str(); + } private: FunctionType functionType; }; diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h index 76471c17e..99e4232c2 100644 --- a/src/ir/expressions/BinaryRelationExpression.h +++ b/src/ir/expressions/BinaryRelationExpression.h @@ -22,7 +22,7 @@ public: enum RelationType {EQUAL, NOT_EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL}; BinaryRelationExpression(std::shared_ptr left, std::shared_ptr right, RelationType relationType) : BinaryExpression(bool_, left, right), relationType(relationType) { - + std::cerr << "BinaryRelationExpression: " << left.get() << " " << relationType << " " << right.get() << " ?" << std::endl; } virtual ~BinaryRelationExpression() { @@ -30,8 +30,9 @@ public: } virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { - std::cout << "Cloning " << this->getLeft()->toString() << " ~ " << this->getRight()->toString() << std::endl; - return std::shared_ptr(new BinaryRelationExpression(this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->relationType)); + auto res = std::shared_ptr(new BinaryRelationExpression(this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->relationType)); + std::cout << "Cloning " << this->toString() << " to " << res->toString() << std::endl; + return res; } virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { @@ -71,6 +72,21 @@ public: return result; } + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "BinaryRelationExpression" << std::endl; + result << this->getLeft()->dump(prefix + "\t"); + switch (relationType) { + case EQUAL: result << prefix << "=" << std::endl; break; + case NOT_EQUAL: result << prefix << "!=" << std::endl; break; + case LESS: result << prefix << "<" << std::endl; break; + case LESS_OR_EQUAL: result << prefix << "<=" << std::endl; break; + case GREATER: result << prefix << ">" << std::endl; break; + case GREATER_OR_EQUAL: result << prefix << ">=" << std::endl; break; + } + result << this->getRight()->dump(prefix + "\t"); + return result.str(); + } private: RelationType relationType; diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h index 15dcd9d4b..2a01a600a 100644 --- a/src/ir/expressions/BooleanConstantExpression.h +++ b/src/ir/expressions/BooleanConstantExpression.h @@ -53,6 +53,12 @@ public: } return result; } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "BooleanConstantExpression " << this->toString() << std::endl; + return result.str(); + } bool isDefined() { return defined; diff --git a/src/ir/expressions/BooleanLiteral.h b/src/ir/expressions/BooleanLiteral.h index 696deb787..e2d17fb0f 100644 --- a/src/ir/expressions/BooleanLiteral.h +++ b/src/ir/expressions/BooleanLiteral.h @@ -45,6 +45,12 @@ public: return std::string("false"); } } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "BooleanLiteral " << this->toString() << std::endl; + return result.str(); + } }; } diff --git a/src/ir/expressions/ConstantExpression.h b/src/ir/expressions/ConstantExpression.h index 79c356dba..b1be49e58 100644 --- a/src/ir/expressions/ConstantExpression.h +++ b/src/ir/expressions/ConstantExpression.h @@ -35,6 +35,12 @@ public: virtual std::string toString() const { return constantName; } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "ConstantExpression " << this->toString() << std::endl; + return result.str(); + } }; } diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h index a0c31efbe..dc8cd7920 100644 --- a/src/ir/expressions/DoubleConstantExpression.h +++ b/src/ir/expressions/DoubleConstantExpression.h @@ -50,6 +50,12 @@ public: } return result; } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "DoubleConstantExpression " << this->toString() << std::endl; + return result.str(); + } bool isDefined() { return defined; diff --git a/src/ir/expressions/DoubleLiteral.h b/src/ir/expressions/DoubleLiteral.h index efa0d1bb5..20d43d464 100644 --- a/src/ir/expressions/DoubleLiteral.h +++ b/src/ir/expressions/DoubleLiteral.h @@ -45,6 +45,12 @@ public: virtual std::string toString() const { return boost::lexical_cast(value); } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "DoubleLiteral " << this->toString() << std::endl; + return result.str(); + } }; } diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h index 01d8f2d71..8d916bf7f 100644 --- a/src/ir/expressions/IntegerConstantExpression.h +++ b/src/ir/expressions/IntegerConstantExpression.h @@ -19,7 +19,6 @@ namespace expressions { class IntegerConstantExpression : public ConstantExpression { public: IntegerConstantExpression(std::string constantName) : ConstantExpression(int_, constantName), defined(false), value(0) { - } virtual ~IntegerConstantExpression() { @@ -50,6 +49,11 @@ public: } return result; } + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "IntegerConstantExpression " << this->toString() << std::endl; + return result.str(); + } bool isDefined() { return defined; diff --git a/src/ir/expressions/IntegerLiteral.h b/src/ir/expressions/IntegerLiteral.h index 8911f640a..7ff615ee4 100644 --- a/src/ir/expressions/IntegerLiteral.h +++ b/src/ir/expressions/IntegerLiteral.h @@ -21,7 +21,6 @@ public: int_fast64_t value; IntegerLiteral(int_fast64_t value) : BaseExpression(int_), value(value) { - } virtual ~IntegerLiteral() { @@ -43,6 +42,11 @@ public: virtual std::string toString() const { return boost::lexical_cast(value); } + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "IntegerLiteral " << this->toString() << std::endl; + return result.str(); + } }; } diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.h b/src/ir/expressions/UnaryBooleanFunctionExpression.h index 73b9969a7..03dd1d87c 100644 --- a/src/ir/expressions/UnaryBooleanFunctionExpression.h +++ b/src/ir/expressions/UnaryBooleanFunctionExpression.h @@ -58,6 +58,15 @@ public: return result; } + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "UnaryBooleanFunctionExpression" << std::endl; + switch (functionType) { + case NOT: result << prefix << "!" << std::endl; break; + } + result << this->getChild()->dump(prefix + "\t"); + return result.str(); + } private: FunctionType functionType; diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h index 0556892f2..d0a770494 100644 --- a/src/ir/expressions/UnaryNumericalFunctionExpression.h +++ b/src/ir/expressions/UnaryNumericalFunctionExpression.h @@ -75,6 +75,16 @@ public: return result; } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "UnaryNumericalFunctionExpression" << std::endl; + switch (functionType) { + case MINUS: result << prefix << "-" << std::endl; break; + } + result << this->getChild()->dump(prefix + "\t"); + return result.str(); + } private: FunctionType functionType; diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h index b7160f929..3aa57ee3e 100644 --- a/src/ir/expressions/VariableExpression.h +++ b/src/ir/expressions/VariableExpression.h @@ -26,7 +26,7 @@ public: std::shared_ptr upperBound = std::shared_ptr(nullptr)) : BaseExpression(type), index(index), variableName(variableName), lowerBound(lowerBound), upperBound(upperBound) { - + std::cerr << "VariableExpression " << this->variableName << std::endl; } virtual ~VariableExpression() { @@ -34,9 +34,13 @@ public: } virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { - std::cout << "Cloning VarExpr " << this->variableName << std::endl; + std::cout << this << " Cloning VarExpr " << this->variableName << " (" << renaming.size() << " renamings)" << std::endl; + for (auto it: renaming) { + std::cout << "\t" << it.first << " -> " << it.second << std::endl; + } if (renaming.count(this->variableName) > 0) { std::string newName = renaming.at(this->variableName); + std::cout << "index of " << newName << " are " << bools.at(newName) << " and " << ints.at(newName) << std::endl; if (this->getType() == bool_) { return std::shared_ptr(new VariableExpression(bool_, bools.at(newName), newName, this->lowerBound, this->upperBound)); } else if (this->getType() == int_) { @@ -52,11 +56,28 @@ public: virtual void accept(ExpressionVisitor* visitor) { + std::cout << "Visitor!" << std::endl; visitor->visit(this); } virtual std::string toString() const { - return variableName; + std::stringstream result; + result << variableName << "(" << this->index << ")"; + return result.str(); + } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << this->variableName << " " << index << std::endl; + if (this->lowerBound != nullptr) { + result << prefix << "lower bound" << std::endl; + result << this->lowerBound->dump(prefix + "\t"); + } + if (this->upperBound != nullptr) { + result << prefix << "upper bound" << std::endl; + result << this->upperBound->dump(prefix + "\t"); + } + return result.str(); } virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { @@ -106,6 +127,10 @@ public: return upperBound; } + uint_fast64_t getVariableIndex() const { + return this->index; + } + private: uint_fast64_t index; std::string variableName; diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index e31e31b8a..2714d369e 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -9,25 +9,18 @@ #include "src/utility/OsDetection.h" +#include "src/parser/PrismParser/Includes.h" #include "src/parser/PrismParser/BooleanExpressionGrammar.h" #include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h" #include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h" #include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h" #include "src/parser/PrismParser/IntegerExpressionGrammar.h" +#include "src/parser/PrismParser/IdentifierGrammars.h" #include "src/parser/PrismParser/VariableState.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFileFormatException.h" -// Used for Boost spirit. -#include -#include -#include - -// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. -#include -#include - // Needed for file IO. #include #include @@ -46,37 +39,84 @@ namespace parser { void dump(const std::string& s) { std::cerr << "Dump: " << s << std::endl; } - /*void dump(const std::string& s, ) { - std::cerr << "Dump: " << s << std::endl; - }*/ - std::shared_ptr addIntegerConstant(const std::string& name, const std::shared_ptr value, std::shared_ptr state) { - std::cerr << "addIntegerConstant: " << name << std::endl; - state->integerConstants_.add(name, value); - state->allConstantNames_.add(name, name); + std::shared_ptr PrismParser::PrismGrammar::addIntegerConstant(const std::string& name, const std::shared_ptr value) { + this->state->integerConstants_.add(name, value); + this->state->allConstantNames_.add(name, name); return value; } -PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type(start), state(new storm::parser::prism::VariableState()) { + void PrismParser::PrismGrammar::addLabel(const std::string& name, std::shared_ptr value, std::map>& mapping) { + this->state->labelNames_.add(name, name); + mapping[name] = value; + } + void PrismParser::PrismGrammar::addIntAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping) { + this->state->assignedLocalIntegerVariables_.add(variable, variable); + mapping[variable] = Assignment(variable, value); + } + void PrismParser::PrismGrammar::addBoolAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping) { + this->state->assignedLocalBooleanVariables_.add(variable, variable); + mapping[variable] = Assignment(variable, value); + } + std::shared_ptr PrismParser::PrismGrammar::renameModule(const std::string& name, const std::string& oldname, std::map& mapping) { + this->state->moduleNames_.add(name, name); + std::shared_ptr old = this->state->moduleMap_.at(oldname); + if (old == nullptr) { + std::cerr << "Renaming module failed: module " << oldname << " does not exist!" << std::endl; + return nullptr; + } + std::shared_ptr res = std::shared_ptr(new Module(*old, name, mapping, this->state)); + this->state->moduleMap_.add(name, res); + return res; + } + std::shared_ptr PrismParser::PrismGrammar::createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector> commands) { + this->state->moduleNames_.add(name, name); + std::shared_ptr res = std::shared_ptr(new Module(name, bools, ints, boolids, intids, commands)); + this->state->moduleMap_.add(name, res); + return res; + } - // This rule defines all identifiers that have not been previously used. - identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&storm::parser::prism::VariableState::isIdentifier, *this->state, qi::_1) ]; - identifierName.name("identifier"); - freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&storm::parser::prism::VariableState::isFreeIdentifier, *this->state, qi::_1) ]; - freeIdentifierName.name("unused identifier"); + std::shared_ptr createStateReward(std::shared_ptr guard, std::shared_ptr reward) { + return std::shared_ptr(new StateReward(guard, reward)); + } + std::shared_ptr createTransitionReward(std::string label, std::shared_ptr guard, std::shared_ptr reward) { + return std::shared_ptr(new TransitionReward(label, guard, reward)); + } + void createRewardModel(std::string name, std::vector>& stateRewards, std::vector>& transitionRewards, std::map>& mapping) { + mapping[name] = std::shared_ptr(new RewardModel(name, stateRewards, transitionRewards)); + } + std::shared_ptr createUpdate(std::shared_ptr likelihood, std::map& bools, std::map ints) { + return std::shared_ptr(new Update(likelihood, bools, ints)); + } + std::shared_ptr createCommand(std::string& label, std::shared_ptr guard, std::vector>& updates) { + return std::shared_ptr(new Command(label, guard, updates)); + } + std::shared_ptr createProgram( + Program::ModelType modelType, + std::map> undefBoolConst, + std::map> undefIntConst, + std::map> undefDoubleConst, + std::vector> modules, + std::map> rewards, + std::map> labels) { + return std::shared_ptr(new Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst, modules, rewards, labels)); + } + +PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type(start), state(new storm::parser::prism::VariableState()) { - // This block defines all entities that are needed for parsing labels. - labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> freeIdentifierName >> -qi::lit("\"") >> qi::lit("=") >> prism::BooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_2)), phoenix::bind(this->state->labelNames_.add, qi::_1, qi::_1)]; + labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> prism::FreeIdentifierGrammar::instance(this->state) >> -qi::lit("\"") >> qi::lit("=") >> prism::BooleanExpressionGrammar::instance(this->state) >> qi::lit(";")) + [phoenix::bind(&PrismParser::PrismGrammar::addLabel, this, qi::_1, qi::_2, qi::_r1)]; labelDefinition.name("label declaration"); labelDefinitionList %= *labelDefinition(qi::_r1); labelDefinitionList.name("label declaration list"); // This block defines all entities that are needed for parsing a reward model. - stateRewardDefinition = (prism::BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > prism::ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_2)]; + stateRewardDefinition = (prism::BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > prism::ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[qi::_val = phoenix::bind(&createStateReward, qi::_1, qi::_2)]; stateRewardDefinition.name("state reward definition"); - transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > prism::BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > prism::ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[qi::_val = phoenix::construct(qi::_a, qi::_2, qi::_3)]; + transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > prism::BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > prism::ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[qi::_val = phoenix::bind(&createTransitionReward, qi::_a, qi::_2, qi::_3)]; transitionRewardDefinition.name("transition reward definition"); - rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > freeIdentifierName > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards"))[phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_a, qi::_b)))]; + rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > prism::FreeIdentifierGrammar::instance(this->state) > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards")) + [phoenix::bind(&createRewardModel, qi::_1, qi::_a, qi::_b, qi::_r1)]; rewardDefinition.name("reward definition"); rewardDefinitionList = *rewardDefinition(qi::_r1); rewardDefinitionList.name("reward definition list"); @@ -89,23 +129,25 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type unassignedLocalIntegerVariableName.name("unassigned local integer variable"); // This block defines all entities that are needed for parsing a single command. - assignmentDefinition = (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > prism::IntegerExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(this->state->assignedLocalIntegerVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_2)))] | (qi::lit("(") > unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > prism::BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(this->state->assignedLocalBooleanVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_2)))]; + assignmentDefinition = + (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > prism::IntegerExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismParser::PrismGrammar::addIntAssignment, this, qi::_1, qi::_2, qi::_r2)] | + (qi::lit("(") >> unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > prism::BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismParser::PrismGrammar::addBoolAssignment, this, qi::_1, qi::_2, qi::_r1)]; assignmentDefinition.name("assignment"); assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&"; assignmentDefinitionList.name("assignment list"); - updateDefinition = (prism::ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b)]; + updateDefinition = (prism::ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&createUpdate, qi::_1, qi::_a, qi::_b)]; updateDefinition.name("update"); updateListDefinition = +updateDefinition % "+"; updateListDefinition.name("update list"); commandDefinition = ( qi::lit("[") > -( - (freeIdentifierName[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1] + (prism::FreeIdentifierGrammar::instance(this->state)[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1] ) > qi::lit("]") > prism::BooleanExpressionGrammar::instance(this->state) > qi::lit("->") > updateListDefinition > qi::lit(";") - )[qi::_val = phoenix::construct(qi::_a, qi::_2, qi::_3)]; + )[qi::_val = phoenix::bind(&createCommand, qi::_a, qi::_2, qi::_3)]; commandDefinition.name("command"); // This block defines all entities that are needed for parsing variable definitions. - booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > prism::ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) + booleanVariableDefinition = (prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > prism::ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) [ //qi::_a = phoenix::bind(&VariableState::addBooleanVariable, *this->state.get(), qi::_1), qi::_a = phoenix::bind(&storm::parser::prism::VariableState::addBooleanVariable, *this->state, qi::_1, qi::_b), @@ -117,7 +159,7 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type integerLiteralExpression = qi::int_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; integerLiteralExpression.name("integer literal"); - integerVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("[") > integerLiteralExpression > qi::lit("..") > integerLiteralExpression > qi::lit("]") > -(qi::lit("init") > prism::ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) + integerVariableDefinition = (prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > integerLiteralExpression > qi::lit("..") > integerLiteralExpression > qi::lit("]") > -(qi::lit("init") > prism::ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) [ qi::_a = phoenix::bind(&storm::parser::prism::VariableState::addIntegerVariable, *this->state, qi::_1, qi::_2, qi::_3, qi::_b), phoenix::push_back(qi::_r1, phoenix::construct(qi::_a, qi::_1, qi::_2, qi::_3, qi::_b)), @@ -129,69 +171,53 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type variableDefinition.name("variable declaration"); // This block defines all entities that are needed for parsing a module. - moduleDefinition = (qi::lit("module") >> freeIdentifierName - [phoenix::bind(&prism::VariableState::startModule, *this->state)] + moduleDefinition = (qi::lit("module") >> prism::FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&prism::VariableState::startModule, *this->state)] >> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule")) - [ - phoenix::bind(this->state->moduleNames_.add, qi::_1, qi::_1), - qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2), - phoenix::bind(this->state->moduleMap_.add, qi::_1, qi::_val) - ]; + [phoenix::bind(&PrismParser::PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)]; - Module const * (qi::symbols::*moduleFinder)(const std::string&) const = &qi::symbols::find; moduleDefinition.name("module"); - moduleRenaming = (qi::lit("module") >> freeIdentifierName >> qi::lit("=") + moduleRenaming = (qi::lit("module") >> prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > this->state->moduleNames_ > qi::lit("[") > *( - (identifierName > qi::lit("=") > identifierName >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct>(qi::_1, qi::_2))] + (prism::IdentifierGrammar::instance(this->state) > qi::lit("=") > prism::IdentifierGrammar::instance(this->state) >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct>(qi::_1, qi::_2))] ) > qi::lit("]") > qi::lit("endmodule")) - [ - phoenix::bind(this->state->moduleNames_.add, qi::_1, qi::_1), - qi::_val = phoenix::construct(*phoenix::bind(moduleFinder, this->state->moduleMap_, qi::_2), qi::_1, qi::_a, this->state), - phoenix::bind(this->state->moduleMap_.add, qi::_1, qi::_val) - - ]; + [phoenix::bind(&PrismParser::PrismGrammar::renameModule, this, qi::_1, qi::_2, qi::_a)]; moduleRenaming.name("renamed module"); moduleDefinitionList %= +(moduleDefinition | moduleRenaming); moduleDefinitionList.name("module list"); // This block defines all entities that are needed for parsing constant definitions. - definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") > prism::ConstBooleanExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > prism::ConstBooleanExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; definedBooleanConstantDefinition.name("defined boolean constant declaration"); definedIntegerConstantDefinition = ( - qi::lit("const") >> - qi::lit("int")[phoenix::bind(&dump, "const int")] >> - freeIdentifierName >> - qi::lit("=")[phoenix::bind(&dump, "const int = ")] >> - //constIntExpr.integerLiteralExpression[phoenix::bind(&dump, "const int = ")] >> - prism::ConstIntegerExpressionGrammar::instance(this->state)[phoenix::bind(&dump, "const int = ")] >> - qi::lit(";")[phoenix::bind(&dump, "const int = ;")] - )[ qi::_val = phoenix::bind(&addIntegerConstant, qi::_1, qi::_2, this->state) ]; + qi::lit("const") >> qi::lit("int") >> prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> + prism::ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";") + )[ qi::_val = phoenix::bind(&PrismParser::PrismGrammar::addIntegerConstant, this, qi::_1, qi::_2) ]; definedIntegerConstantDefinition.name("defined integer constant declaration"); - definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") > prism::ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > prism::ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; definedDoubleConstantDefinition.name("defined double constant declaration"); - undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; + undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > prism::FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); - undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; + undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > prism::FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); - undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; + undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > prism::FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; undefinedDoubleConstantDefinition.name("undefined double constant declaration"); - definedConstantDefinition %= (definedBooleanConstantDefinition[phoenix::bind(&dump, "")] | definedIntegerConstantDefinition[phoenix::bind(&dump, "")] | definedDoubleConstantDefinition[phoenix::bind(&dump, "")]); + definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); definedConstantDefinition.name("defined constant declaration"); undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); undefinedConstantDefinition.name("undefined constant declaration"); - constantDefinitionList = *(definedConstantDefinition[phoenix::bind(&dump, "")] | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)[phoenix::bind(&dump, "")]); + constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)); constantDefinitionList.name("constant declaration list"); // This block defines all entities that are needed for parsing a program. modelTypeDefinition = modelType_; modelTypeDefinition.name("model type"); start = ( - modelTypeDefinition[phoenix::bind(&dump, "")] > - constantDefinitionList(qi::_a, qi::_b, qi::_c)[phoenix::bind(&dump, "")] > - moduleDefinitionList[phoenix::bind(&dump, "")] > - rewardDefinitionList(qi::_d)[phoenix::bind(&dump, "")] > - labelDefinitionList(qi::_e)[phoenix::bind(&dump, "")] - )[qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; + modelTypeDefinition > + constantDefinitionList(qi::_a, qi::_b, qi::_c) > + moduleDefinitionList > + rewardDefinitionList(qi::_d) > + labelDefinitionList(qi::_e) + )[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; start.name("probabilistic program declaration"); } @@ -250,12 +276,12 @@ std::shared_ptr PrismParser::parse(std::istream& inputStream try { // Now parse the content using phrase_parse in order to be able to supply a skipping parser. // First run. - qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, *result); + qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); grammar.prepareForSecondRun(); result = std::shared_ptr(new storm::ir::Program()); std::cout << "Now we start the second run..." << std::endl; // Second run. - qi::phrase_parse(positionIteratorBegin2, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, *result); + qi::phrase_parse(positionIteratorBegin2, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); std::cout << "Here is the parsed grammar: " << std::endl << result->toString() << std::endl; } catch(const qi::expectation_failure& e) { // If the parser expected content different than the one provided, display information diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index a32487c78..b08777c65 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -48,7 +48,13 @@ public: * The Boost spirit grammar for the PRISM language. Returns the intermediate representation of * the input that complies with the PRISM syntax. */ - class PrismGrammar : public qi::grammar>, std::map>, std::map>, std::map, std::map>>, Skipper> { + class PrismGrammar : public qi::grammar< + Iterator, + std::shared_ptr(), + qi::locals< + std::map>, + std::map>, + std::map>, std::map>, std::map>>, Skipper> { public: PrismGrammar(); void prepareForSecondRun(); @@ -58,14 +64,18 @@ public: std::shared_ptr state; // The starting point of the grammar. - qi::rule>, std::map>, std::map>, std::map, std::map>>, Skipper> start; + qi::rule< + Iterator, + std::shared_ptr(), + qi::locals>, std::map>, std::map>, std::map>, std::map>>, + Skipper> start; qi::rule modelTypeDefinition; qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; - qi::rule(), Skipper> moduleDefinitionList; + qi::rule>(), Skipper> moduleDefinitionList; // Rules for module definition. - qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; - qi::rule>, Skipper> moduleRenaming; + qi::rule(), qi::locals, std::vector, std::map, std::map>, Skipper> moduleDefinition; + qi::rule(), qi::locals>, Skipper> moduleRenaming; // Rules for variable definitions. qi::rule(), Skipper> integerLiteralExpression; @@ -74,9 +84,9 @@ public: qi::rule&, std::map&), qi::locals>, Skipper> integerVariableDefinition; // Rules for command definitions. - qi::rule, Skipper> commandDefinition; - qi::rule(), Skipper> updateListDefinition; - qi::rule, std::map>, Skipper> updateDefinition; + qi::rule(), qi::locals, Skipper> commandDefinition; + qi::rule>(), Skipper> updateListDefinition; + qi::rule(), qi::locals, std::map>, Skipper> updateDefinition; qi::rule&, std::map&), Skipper> assignmentDefinitionList; qi::rule&, std::map&), Skipper> assignmentDefinition; @@ -86,10 +96,10 @@ public: qi::rule unassignedLocalIntegerVariableName; // Rules for reward definitions. - qi::rule&), Skipper> rewardDefinitionList; - qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; - qi::rule stateRewardDefinition; - qi::rule, Skipper> transitionRewardDefinition; + qi::rule>&), Skipper> rewardDefinitionList; + qi::rule>&), qi::locals>, std::vector>>, Skipper> rewardDefinition; + qi::rule(), Skipper> stateRewardDefinition; + qi::rule(), qi::locals, Skipper> transitionRewardDefinition; // Rules for label definitions. qi::rule>&), Skipper> labelDefinitionList; @@ -106,10 +116,6 @@ public: qi::rule(), Skipper> definedIntegerConstantDefinition; qi::rule(), Skipper> definedDoubleConstantDefinition; - qi::rule freeIdentifierName; - qi::rule identifierName; - - // Rules for variable recognition. qi::rule(), Skipper> booleanVariableCreatorExpression; qi::rule(), qi::locals>, Skipper> integerVariableCreatorExpression; @@ -118,6 +124,13 @@ public: storm::parser::prism::modelTypeStruct modelType_; storm::parser::prism::relationalOperatorStruct relations_; + std::shared_ptr addIntegerConstant(const std::string& name, const std::shared_ptr value); + void addLabel(const std::string& name, std::shared_ptr value, std::map>& mapping); + void addBoolAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); + void addIntAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); + std::shared_ptr renameModule(const std::string& name, const std::string& oldname, std::map& mapping); + std::shared_ptr createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector> commands); + }; private: diff --git a/src/parser/PrismParser/VariableState.h b/src/parser/PrismParser/VariableState.h index 1076d2764..6b2c9a9b3 100644 --- a/src/parser/PrismParser/VariableState.h +++ b/src/parser/PrismParser/VariableState.h @@ -38,14 +38,14 @@ public: // the intermediate representation. struct qi::symbols> integerVariables_, booleanVariables_; struct qi::symbols> integerConstants_, booleanConstants_, doubleConstants_; - struct qi::symbols moduleMap_; + struct qi::symbols> moduleMap_; // A structure representing the identity function over identifier names. struct variableNamesStruct : qi::symbols { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_, localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_; uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr init) { - std::cerr << "adding boolean variable " << name << std::endl; + //std::cerr << "adding boolean variable " << name << std::endl; if (firstRun) { std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextBooleanVariableIndex, name)); this->booleanVariables_.add(name, varExpr); @@ -64,7 +64,7 @@ public: } uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper, const std::shared_ptr init) { - std::cerr << "adding integer variable " << name << std::endl; + //std::cerr << "adding integer variable " << name << std::endl; if (firstRun) { std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextIntegerVariableIndex, name, lower, upper)); this->integerVariables_.add(name, varExpr); @@ -83,7 +83,7 @@ public: } std::shared_ptr getBooleanVariable(const std::string& name) { - std::cerr << "getting boolen variable " << name << std::endl; + //std::cerr << "getting boolen variable " << name << std::endl; std::shared_ptr res = this->booleanVariables_.at(name); if (res != nullptr) { return res; @@ -98,7 +98,7 @@ public: } std::shared_ptr getIntegerVariable(const std::string& name) { - std::cerr << "getting integer variable " << name << std::endl; + //std::cerr << "getting integer variable " << name << std::endl; std::shared_ptr res = this->integerVariables_.at(name); if (res != nullptr) { return res; @@ -113,13 +113,13 @@ public: } void startModule() { - std::cerr << "starting new module" << std::endl; + //std::cerr << "starting new module" << std::endl; this->localBooleanVariables_.clear(); this->localIntegerVariables_.clear(); } bool isFreeIdentifier(std::string& s) const { - std::cerr << "Checking if " << s << " is free" << std::endl; + //std::cerr << "Checking if " << s << " is free" << std::endl; if (this->integerVariableNames_.find(s) != nullptr) return false; if (this->allConstantNames_.find(s) != nullptr) return false; if (this->labelNames_.find(s) != nullptr) return false; @@ -128,7 +128,7 @@ public: return true; } bool isIdentifier(std::string& s) const { - std::cerr << "Checking if " << s << " is identifier" << std::endl; + //std::cerr << "Checking if " << s << " is identifier" << std::endl; if (this->allConstantNames_.find(s) != nullptr) return false; if (this->keywords.find(s) != nullptr) return false; return true;