From d414b93bad7d68ab0b5b02eade551d4696cfc37f Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 13 Jan 2013 22:47:29 +0100 Subject: [PATCH] Added some functionality to IR. Introduced case distinction for boolean/integer assignments in updates. Started writing an IR adapter. --- .../IntermediateRepresentationAdapter.h | 144 ++++++++++++++++++ .../ExpressionEvaluationException.h | 23 +++ src/exceptions/NotImplementedException.h | 23 +++ src/ir/BooleanVariable.cpp | 6 +- src/ir/BooleanVariable.h | 5 +- src/ir/Command.cpp | 15 ++ src/ir/Command.h | 18 +++ src/ir/IntegerVariable.cpp | 10 +- src/ir/IntegerVariable.h | 3 +- src/ir/Module.cpp | 47 +++++- src/ir/Module.h | 54 ++++++- src/ir/Program.cpp | 9 ++ src/ir/Program.h | 12 ++ src/ir/Update.cpp | 67 +++++++- src/ir/Update.h | 51 ++++++- src/ir/Variable.cpp | 12 +- src/ir/Variable.h | 14 +- src/ir/expressions/BaseExpression.h | 73 +++++++-- .../BinaryBooleanFunctionExpression.h | 57 ++++--- .../BinaryNumericalFunctionExpression.h | 51 +++++-- src/ir/expressions/BinaryRelationExpression.h | 30 +++- .../expressions/BooleanConstantExpression.h | 11 +- src/ir/expressions/BooleanLiteral.h | 8 +- src/ir/expressions/ConstantExpression.h | 8 +- src/ir/expressions/DoubleConstantExpression.h | 17 ++- src/ir/expressions/DoubleLiteral.h | 8 +- .../expressions/IntegerConstantExpression.h | 19 ++- src/ir/expressions/IntegerLiteral.h | 10 +- .../UnaryBooleanFunctionExpression.h | 23 ++- .../UnaryNumericalFunctionExpression.h | 40 ++++- src/ir/expressions/VariableExpression.h | 33 +++- src/parser/PrismParser.cpp | 50 +++--- src/storm.cpp | 4 +- test.input | 30 ++-- 34 files changed, 833 insertions(+), 152 deletions(-) create mode 100644 src/adapters/IntermediateRepresentationAdapter.h create mode 100644 src/exceptions/ExpressionEvaluationException.h create mode 100644 src/exceptions/NotImplementedException.h diff --git a/src/adapters/IntermediateRepresentationAdapter.h b/src/adapters/IntermediateRepresentationAdapter.h new file mode 100644 index 000000000..d60325b11 --- /dev/null +++ b/src/adapters/IntermediateRepresentationAdapter.h @@ -0,0 +1,144 @@ +/* + * IntermediateRepresentationAdapter.h + * + * Created on: 13.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_ +#define STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_ + +#include +#include +#include +#include +#include +#include + +typedef std::pair, std::vector> StateType; + +namespace storm { + +namespace adapters { + +class StateHash { +public: + std::size_t operator()(StateType* state) const { + size_t seed = 0; + for (auto it = state->first.begin(); it != state->first.end(); ++it) { + boost::hash_combine(seed, *it); + } + for (auto it = state->second.begin(); it != state->second.end(); ++it) { + boost::hash_combine(seed, *it); + } + return seed; + } +}; + +class IntermediateRepresentationAdapter { +public: + template + static storm::storage::SquareSparseMatrix* toSparseMatrix(storm::ir::Program const& program) { + + 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(); + } + + std::vector booleanVariables; + std::vector integerVariables; + booleanVariables.resize(numberOfBooleanVariables); + integerVariables.resize(numberOfIntegerVariables); + + std::unordered_map booleanVariableToIndexMap; + std::unordered_map integerVariableToIndexMap; + + 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); + + for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { + booleanVariables[nextBooleanVariableIndex] = module.getBooleanVariable(j); + booleanVariableToIndexMap[module.getBooleanVariable(j).getName()] = nextBooleanVariableIndex; + ++nextBooleanVariableIndex; + } + for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { + integerVariables[nextIntegerVariableIndex] = module.getIntegerVariable(j); + integerVariableToIndexMap[module.getIntegerVariable(j).getName()] = nextIntegerVariableIndex; + ++nextIntegerVariableIndex; + } + } + + StateType* initialState = new StateType(std::vector(), std::vector()); + std::get<0>(*initialState).resize(numberOfBooleanVariables); + std::get<1>(*initialState).resize(numberOfIntegerVariables); + + for (uint_fast64_t i = 0; i < numberOfBooleanVariables; ++i) { + bool initialValue = booleanVariables[i].getInitialValue()->getValueAsBool(std::get<0>(*initialState), std::get<1>(*initialState)); + std::get<0>(*initialState)[i] = initialValue; + } + + for (uint_fast64_t i = 0; i < numberOfIntegerVariables; ++i) { + int_fast64_t initialValue = integerVariables[i].getInitialValue()->getValueAsInt(std::get<0>(*initialState), std::get<1>(*initialState)); + std::get<1>(*initialState)[i] = initialValue; + } + + std::cout << "Initial State:" << std::get<0>(*initialState) << " / " << std::get<1>(*initialState) << std::endl; + + uint_fast64_t nextIndex = 1; + std::unordered_map stateToIndexMap; + std::vector allStates; + std::queue stateQueue; + + allStates.push_back(initialState); + stateQueue.push(initialState); + stateToIndexMap[initialState] = 0; + + while (!stateQueue.empty()) { + // Get first state in queue. + StateType* currentState = stateQueue.front(); + stateQueue.pop(); + + // Iterate over all modules. + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + storm::ir::Module 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); + + // Check if this command is enabled in the current state. + if (command.getGuard()->getValueAsBool(std::get<0>(*currentState), std::get<1>(*currentState))) { + for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { + storm::ir::Update const& update = command.getUpdate(k); + + std::map const& booleanAssignmentMap = update.getBooleanAssignments(); + for (auto assignedVariable : booleanAssignmentMap) { + // Check if the variable that is being assigned is a boolean or an integer. + // auto boolIt = + + } + } + } + } + } + } + + // Now free all the elements we allocated. + for (auto element : allStates) { + delete element; + } + return nullptr; + } + +}; + +} + +} + + +#endif /* STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_ */ diff --git a/src/exceptions/ExpressionEvaluationException.h b/src/exceptions/ExpressionEvaluationException.h new file mode 100644 index 000000000..390991c1d --- /dev/null +++ b/src/exceptions/ExpressionEvaluationException.h @@ -0,0 +1,23 @@ +/* + * ExpressionEvaluationException.h + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_ +#define STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" + +namespace storm { + +namespace exceptions { + +STORM_EXCEPTION_DEFINE_NEW(ExpressionEvaluationException) + +} + +} + +#endif /* STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_ */ diff --git a/src/exceptions/NotImplementedException.h b/src/exceptions/NotImplementedException.h new file mode 100644 index 000000000..cf98d4d99 --- /dev/null +++ b/src/exceptions/NotImplementedException.h @@ -0,0 +1,23 @@ +/* + * NotImplementedException.h + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_ +#define STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" + +namespace storm { + +namespace exceptions { + +STORM_EXCEPTION_DEFINE_NEW(NotImplementedException) + +} + +} + +#endif /* STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_ */ diff --git a/src/ir/BooleanVariable.cpp b/src/ir/BooleanVariable.cpp index e524d6753..b867a1aa1 100644 --- a/src/ir/BooleanVariable.cpp +++ b/src/ir/BooleanVariable.cpp @@ -19,16 +19,16 @@ BooleanVariable::BooleanVariable() : Variable() { } // Initializes all members according to the given values. -BooleanVariable::BooleanVariable(std::string variableName, +BooleanVariable::BooleanVariable(uint_fast64_t index, std::string variableName, std::shared_ptr initialValue) - : Variable(variableName, initialValue) { + : Variable(index, variableName, initialValue) { // Nothing to do here. } // Build a string representation of the variable. std::string BooleanVariable::toString() const { std::stringstream result; - result << getVariableName() << ": bool"; + result << this->getName() << ": bool"; if (this->getInitialValue() != nullptr) { result << " init " << this->getInitialValue()->toString(); } diff --git a/src/ir/BooleanVariable.h b/src/ir/BooleanVariable.h index dc832399e..e12506b67 100644 --- a/src/ir/BooleanVariable.h +++ b/src/ir/BooleanVariable.h @@ -8,6 +8,8 @@ #ifndef STORM_IR_BOOLEANVARIABLE_H_ #define STORM_IR_BOOLEANVARIABLE_H_ +#include "expressions/BooleanLiteral.h" + #include "Variable.h" #include @@ -27,10 +29,11 @@ public: /*! * Creates a boolean variable with the given name and the given initial value. + * @param index a unique (among the variables of equal type) index for the variable. * @param variableName the name of the variable. * @param initialValue the expression that defines the initial value of the variable. */ - BooleanVariable(std::string variableName, std::shared_ptr initialValue = std::shared_ptr()); + BooleanVariable(uint_fast64_t index, std::string variableName, std::shared_ptr initialValue = std::shared_ptr(new storm::ir::expressions::BooleanLiteral(false))); /*! * Retrieves a string representation of this variable. diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp index 832fbb302..5cb4c6354 100644 --- a/src/ir/Command.cpp +++ b/src/ir/Command.cpp @@ -24,6 +24,21 @@ Command::Command(std::string commandName, std::shared_ptr const& Command::getGuard() const { + return guardExpression; +} + +// Return the number of updates. +uint_fast64_t Command::getNumberOfUpdates() const { + return this->updates.size(); +} + +// Return the requested update. +storm::ir::Update const& Command::getUpdate(uint_fast64_t index) const { + return this->updates[index]; +} + // Build a string representation of the command. std::string Command::toString() const { std::stringstream result; diff --git a/src/ir/Command.h b/src/ir/Command.h index 186d81058..2ac54b525 100644 --- a/src/ir/Command.h +++ b/src/ir/Command.h @@ -35,6 +35,24 @@ public: */ Command(std::string commandName, std::shared_ptr guardExpression, std::vector updates); + /*! + * Retrieves a reference to the guard of the command. + * @returns a reference to the guard of the command. + */ + std::shared_ptr const& getGuard() const; + + /*! + * Retrieves the number of updates associated with this command. + * @returns the number of updates associated with this command. + */ + uint_fast64_t getNumberOfUpdates() const; + + /*! + * 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; + /*! * Retrieves a string representation of this command. * @returns a string representation of this command. diff --git a/src/ir/IntegerVariable.cpp b/src/ir/IntegerVariable.cpp index 6b6724b1a..8374551a9 100644 --- a/src/ir/IntegerVariable.cpp +++ b/src/ir/IntegerVariable.cpp @@ -9,6 +9,8 @@ #include +#include + namespace storm { namespace ir { @@ -19,14 +21,16 @@ IntegerVariable::IntegerVariable() : lowerBound(), upperBound() { } // Initializes all members according to the given values. -IntegerVariable::IntegerVariable(std::string variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue) : Variable(variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) { - // Nothing to do here. +IntegerVariable::IntegerVariable(uint_fast64_t index, std::string variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue) : Variable(index, variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) { + if (this->getInitialValue() == nullptr) { + this->setInitialValue(lowerBound); + } } // Build a string representation of the variable. std::string IntegerVariable::toString() const { std::stringstream result; - result << this->getVariableName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]"; + result << this->getName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]"; if (this->getInitialValue() != nullptr) { result << " init " + this->getInitialValue()->toString(); } diff --git a/src/ir/IntegerVariable.h b/src/ir/IntegerVariable.h index d687e2a04..86e2dfc1b 100644 --- a/src/ir/IntegerVariable.h +++ b/src/ir/IntegerVariable.h @@ -29,12 +29,13 @@ public: /*! * Creates an integer variable with the given name, lower and upper bounds and the given initial * value. + * @param index A unique (among the variables of equal type) index for the variable. * @param variableName the name of the variable. * @param lowerBound the lower bound of the domain of the variable. * @param upperBound the upper bound of the domain of the variable. * @param initialValue the expression that defines the initial value of the variable. */ - IntegerVariable(std::string variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue = std::shared_ptr()); + IntegerVariable(uint_fast64_t index, std::string variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue = std::shared_ptr(nullptr)); /*! * Retrieves a string representation of this variable. diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index 5f28a8d13..f76a53b88 100644 --- a/src/ir/Module.cpp +++ b/src/ir/Module.cpp @@ -14,25 +14,62 @@ namespace storm { namespace ir { // Initializes all members with their default constructors. -Module::Module() : moduleName(), booleanVariables(), integerVariables(), commands() { +Module::Module() : moduleName(), booleanVariables(), integerVariables(), booleanVariablesToIndexMap(), + integerVariablesToIndexMap(), commands() { // Nothing to do here. } // Initializes all members according to the given values. -Module::Module(std::string moduleName, std::map booleanVariables, std::map integerVariables, std::vector commands) - : moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands) { +Module::Module(std::string moduleName, std::vector booleanVariables, + std::vector integerVariables, + std::map booleanVariableToIndexMap, + std::map integerVariableToIndexMap, + std::vector commands) + : moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), + booleanVariablesToIndexMap(booleanVariableToIndexMap), + integerVariablesToIndexMap(integerVariableToIndexMap), commands(commands) { // Nothing to do here. } +// Return the number of boolean variables. +uint_fast64_t Module::getNumberOfBooleanVariables() const { + return this->booleanVariables.size(); +} + +// Return the requested boolean variable. +storm::ir::BooleanVariable const& Module::getBooleanVariable(uint_fast64_t index) const { + return this->booleanVariables[index]; +} + +// Return the number of integer variables. +uint_fast64_t Module::getNumberOfIntegerVariables() const { + return this->integerVariables.size(); +} + +// Return the requested integer variable. +storm::ir::IntegerVariable const& Module::getIntegerVariable(uint_fast64_t index) const { + return this->integerVariables[index]; +} + +// Return the number of commands. +uint_fast64_t Module::getNumberOfCommands() const { + return this->commands.size(); +} + +// Return the requested command. +storm::ir::Command const& Module::getCommand(uint_fast64_t index) const { + return this->commands[index]; +} + // Build a string representation of the variable. std::string Module::toString() const { std::stringstream result; result << "module " << moduleName << std::endl; for (auto variable : booleanVariables) { - result << "\t" << variable.second.toString() << std::endl; + result << "\t" << variable.toString() << std::endl; } for (auto variable : integerVariables) { - result << "\t" << variable.second.toString() << std::endl; + result << "\t" << variable.toString() << std::endl; } for (auto command : commands) { result << "\t" << command.toString() << std::endl; diff --git a/src/ir/Module.h b/src/ir/Module.h index ad0218730..0ed2ed010 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -37,7 +37,47 @@ public: * @param integerVariables a map of integer variables. * @param commands the vector of commands. */ - Module(std::string moduleName, std::map booleanVariables, std::map integerVariables, std::vector commands); + Module(std::string moduleName, std::vector booleanVariables, + std::vector integerVariables, + std::map booleanVariableToIndexMap, + std::map integerVariableToIndexMap, + std::vector commands); + + /*! + * Retrieves the number of boolean variables in the module. + * @returns the number of boolean variables in the module. + */ + uint_fast64_t getNumberOfBooleanVariables() const; + + /*! + * Retrieves a reference to the boolean variable with the given index. + * @returns a reference to the boolean variable with the given index. + */ + storm::ir::BooleanVariable const& getBooleanVariable(uint_fast64_t index) const; + + /*! + * Retrieves the number of integer variables in the module. + * @returns the number of integer variables in the module. + */ + uint_fast64_t getNumberOfIntegerVariables() const; + + /*! + * Retrieves a reference to the integer variable with the given index. + * @returns a reference to the integer variable with the given index. + */ + storm::ir::IntegerVariable const& getIntegerVariable(uint_fast64_t index) const; + + /*! + * Retrieves the number of commands of this module. + * @returns the number of commands of this module. + */ + uint_fast64_t getNumberOfCommands() const; + + /*! + * 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; /*! * Retrieves a string representation of this variable. @@ -49,11 +89,17 @@ private: // The name of the module. std::string moduleName; - // A map of boolean variable names to their details. - std::map booleanVariables; + // A list of boolean variables. + std::vector booleanVariables; + + // A list of integer variables. + std::vector integerVariables; + + // A map of boolean variable names to their index. + std::map booleanVariablesToIndexMap; // A map of integer variable names to their details. - std::map integerVariables; + std::map integerVariablesToIndexMap; // The commands associated with the module. std::vector commands; diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index 5a250405e..e5dfa9ce3 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -62,6 +62,15 @@ std::string Program::toString() const { return result.str(); } +uint_fast64_t Program::getNumberOfModules() const { + return this->modules.size(); +} + +storm::ir::Module const& Program::getModule(uint_fast64_t index) const { + return this->modules[index]; +} + + } // namespace ir } // namepsace storm diff --git a/src/ir/Program.h b/src/ir/Program.h index 8fcd7c10f..8ea9b5b11 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -54,6 +54,18 @@ public: */ 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. + * @returns the number of modules in the program. + */ + uint_fast64_t getNumberOfModules() const; + + /*! + * 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; + /*! * Retrieves a string representation of this program. * @returns a string representation of this program. diff --git a/src/ir/Update.cpp b/src/ir/Update.cpp index 4e59d46be..668b543da 100644 --- a/src/ir/Update.cpp +++ b/src/ir/Update.cpp @@ -7,6 +7,8 @@ #include "Update.h" +#include "src/exceptions/OutOfRangeException.h" + #include namespace storm { @@ -14,28 +16,81 @@ namespace storm { namespace ir { // Initializes all members with their default constructors. -Update::Update() : likelihoodExpression(), assignments() { +Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignments() { // Nothing to do here. } // Initializes all members according to the given values. -Update::Update(std::shared_ptr likelihoodExpression, std::map assignments) - : likelihoodExpression(likelihoodExpression), assignments(assignments) { +Update::Update(std::shared_ptr likelihoodExpression, std::map booleanAssignments, std::map integerAssignments) + : likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments) { // Nothing to do here. } +// Return the expression for the likelihood of the update. +std::shared_ptr const& Update::getLikelihoodExpression() const { + return likelihoodExpression; +} + +// Return the number of assignments. +uint_fast64_t Update::getNumberOfBooleanAssignments() const { + return booleanAssignments.size(); +} + +uint_fast64_t Update::getNumberOfIntegerAssignments() const { + return integerAssignments.size(); +} + +// Return the boolean variable name to assignment map. +std::map const& Update::getBooleanAssignments() const { + return booleanAssignments; +} + +// Return the integer variable name to assignment map. +std::map const& Update::getIntegerAssignments() const { + return integerAssignments; +} + +// Return the assignment for the boolean variable if it exists and throw an exception otherwise. +storm::ir::Assignment const& Update::getBooleanAssignment(std::string variableName) const { + auto it = booleanAssignments.find(variableName); + if (it == booleanAssignments.end()) { + throw storm::exceptions::OutOfRangeException() << "Cannot find boolean assignment for variable '" + << variableName << "' in update " << this->toString() << "."; + } + + return (*it).second; +} + +// Return the assignment for the boolean variable if it exists and throw an exception otherwise. +storm::ir::Assignment const& Update::getIntegerAssignment(std::string variableName) const { + auto it = integerAssignments.find(variableName); + if (it == integerAssignments.end()) { + throw storm::exceptions::OutOfRangeException() << "Cannot find integer assignment for variable '" + << variableName << "' in update " << this->toString() << "."; + } + + return (*it).second; +} + // Build a string representation of the update. std::string Update::toString() const { std::stringstream result; result << likelihoodExpression->toString() << " : "; uint_fast64_t i = 0; - for (auto assignment : assignments) { + for (auto assignment : booleanAssignments) { result << assignment.second.toString(); ++i; - if (i < assignments.size() - 1) { + if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) { + result << " & "; + } + } + i = 0; + for (auto assignment : integerAssignments) { + result << assignment.second.toString(); + ++i; + if (i < integerAssignments.size() - 1) { result << " & "; } - } return result.str(); } diff --git a/src/ir/Update.h b/src/ir/Update.h index 1aeb1d125..54ddc5cd8 100644 --- a/src/ir/Update.h +++ b/src/ir/Update.h @@ -34,7 +34,49 @@ public: * @param likelihoodExpression an expression specifying the likelihood of this update. * @param assignments a map of variable names to their assignments. */ - Update(std::shared_ptr likelihoodExpression, std::map assignments); + Update(std::shared_ptr likelihoodExpression, std::map booleanAssignments, std::map integerAssignments); + + /*! + * Retrieves the expression for the likelihood of this update. + * @returns the expression for the likelihood of this update. + */ + std::shared_ptr const& getLikelihoodExpression() const; + + /*! + * Retrieves the number of boolean assignments associated with this update. + * @returns the number of boolean assignments associated with this update. + */ + uint_fast64_t getNumberOfBooleanAssignments() const; + + /*! + * Retrieves the number of integer assignments associated with this update. + * @returns the number of integer assignments associated with this update. + */ + uint_fast64_t getNumberOfIntegerAssignments() const; + + /*! + * Retrieves a reference to the map of boolean variable names to their respective assignments. + * @returns a reference to the map of boolean variable names to their respective assignments. + */ + std::map const& getBooleanAssignments() const; + + /*! + * Retrieves a reference to the map of integer variable names to their respective assignments. + * @returns a reference to the map of integer variable names to their respective assignments. + */ + std::map const& getIntegerAssignments() const; + + /*! + * Retrieves a reference to the assignment for the boolean variable with the given name. + * @returns a reference to the assignment for the boolean variable with the given name. + */ + storm::ir::Assignment const& getBooleanAssignment(std::string variableName) const; + + /*! + * Retrieves a reference to the assignment for the integer variable with the given name. + * @returns a reference to the assignment for the integer variable with the given name. + */ + storm::ir::Assignment const& getIntegerAssignment(std::string variableName) const; /*! * Retrieves a string representation of this update. @@ -46,8 +88,11 @@ private: // An expression specifying the likelihood of taking this update. std::shared_ptr likelihoodExpression; - // A mapping of variable names to their assignments in this update. - std::map assignments; + // A mapping of boolean variable names to their assignments in this update. + std::map booleanAssignments; + + // A mapping of integer variable names to their assignments in this update. + std::map integerAssignments; }; } // namespace ir diff --git a/src/ir/Variable.cpp b/src/ir/Variable.cpp index a735fa94d..d051b9ca1 100644 --- a/src/ir/Variable.cpp +++ b/src/ir/Variable.cpp @@ -14,17 +14,17 @@ namespace storm { namespace ir { // Initializes all members with their default constructors. -Variable::Variable() : variableName(), initialValue() { +Variable::Variable() : index(0), variableName(), initialValue() { // Nothing to do here. } // Initializes all members according to the given values. -Variable::Variable(std::string variableName, std::shared_ptr initialValue) : variableName(variableName), initialValue(initialValue) { +Variable::Variable(uint_fast64_t index, std::string variableName, std::shared_ptr initialValue) : index(index), variableName(variableName), initialValue(initialValue) { // Nothing to do here. } // Return the name of the variable. -std::string const& Variable::getVariableName() const { +std::string const& Variable::getName() const { return variableName; } @@ -33,6 +33,12 @@ std::shared_ptr const& Variable::getInit return initialValue; } +// Set the initial value expression to the one provided. +void Variable::setInitialValue(std::shared_ptr const& initialValue) { + this->initialValue = initialValue; +} + + } // namespace ir } // namespace storm diff --git a/src/ir/Variable.h b/src/ir/Variable.h index bbd567073..eed1e538c 100644 --- a/src/ir/Variable.h +++ b/src/ir/Variable.h @@ -28,16 +28,17 @@ public: /*! * Creates an untyped variable with the given name and initial value. + * @param index A unique (among the variables of equal type) index for the variable. * @param variableName the name of the variable. * @param initialValue the expression that defines the initial value of the variable. */ - Variable(std::string variableName, std::shared_ptr initialValue = std::shared_ptr()); + Variable(uint_fast64_t index, std::string variableName, std::shared_ptr initialValue = std::shared_ptr()); /*! * Retrieves the name of the variable. * @returns the name of the variable. */ - std::string const& getVariableName() const; + std::string const& getName() const; /*! * Retrieves the expression defining the initial value of the variable. @@ -45,7 +46,16 @@ public: */ std::shared_ptr const& getInitialValue() const; + /*! + * Sets the initial value to the given expression. + * @param initialValue the new initial value. + */ + void setInitialValue(std::shared_ptr const& initialValue); + private: + // A unique (among the variables of equal type) index for the variable + uint_fast64_t index; + // The name of the variable. std::string variableName; diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h index f2d848fb7..b88953dce 100644 --- a/src/ir/expressions/BaseExpression.h +++ b/src/ir/expressions/BaseExpression.h @@ -2,13 +2,17 @@ * Expression.h * * Created on: 03.01.2013 - * Author: chris + * Author: Christian Dehnert */ -#ifndef EXPRESSION_H_ -#define EXPRESSION_H_ +#ifndef STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ +#define STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ + +#include "src/exceptions/ExpressionEvaluationException.h" +#include "src/exceptions/NotImplementedException.h" #include +#include namespace storm { @@ -19,19 +23,70 @@ namespace expressions { class BaseExpression { public: + enum ReturnType {undefined, bool_, int_, double_}; + + BaseExpression() : type(undefined) { + + } + + BaseExpression(ReturnType type) : type(type) { + + } + virtual ~BaseExpression() { } - virtual std::string toString() const { - return "expr here!"; + virtual int_fast64_t getValueAsInt(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + if (type != int_) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" + << this->getTypeName() << "' as 'int'."; + } + throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '" + << this->getTypeName() << " because evaluation implementation is missing."; + } + + virtual bool getValueAsBool(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + if (type != bool_) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" + << this->getTypeName() << "' as 'bool'."; + } + throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '" + << this->getTypeName() << " because evaluation implementation is missing."; + } + + virtual double getValueAsDouble(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + if (type != bool_) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" + << this->getTypeName() << "' as 'double'."; + } + throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '" + << this->getTypeName() << " because evaluation implementation is missing."; } + + virtual std::string toString() const = 0; + + std::string getTypeName() const { + switch(type) { + case bool_: return std::string("bool"); + case int_: return std::string("int"); + case double_: return std::string("double"); + default: return std::string("undefined"); + } + } + + ReturnType getType() const { + return type; + } + +private: + ReturnType type; }; -} +} // namespace expressions -} +} // namespace ir -} +} // namespace storm -#endif /* EXPRESSION_H_ */ +#endif /* STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ */ diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.h b/src/ir/expressions/BinaryBooleanFunctionExpression.h index bd388dc04..e26bd22f3 100644 --- a/src/ir/expressions/BinaryBooleanFunctionExpression.h +++ b/src/ir/expressions/BinaryBooleanFunctionExpression.h @@ -5,11 +5,13 @@ * Author: chris */ -#ifndef BINARYBOOLEANFUNCTIONEXPRESSION_H_ -#define BINARYBOOLEANFUNCTIONEXPRESSION_H_ +#ifndef STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ +#define STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ #include "src/ir/expressions/BaseExpression.h" -#include + +#include +#include namespace storm { @@ -19,38 +21,49 @@ namespace expressions { class BinaryBooleanFunctionExpression : public BaseExpression { public: - enum FunctorType {AND, OR, XOR, IMPLIES} functor; - std::shared_ptr left; - std::shared_ptr right; + enum FunctionType {AND, OR}; + + BinaryBooleanFunctionExpression(std::shared_ptr left, std::shared_ptr right, FunctionType functionType) : BaseExpression(bool_), left(left), right(right), functionType(functionType) { - BinaryBooleanFunctionExpression(std::shared_ptr left, std::shared_ptr right, FunctorType functor) { - this->left = left; - this->right = right; - this->functor = functor; } virtual ~BinaryBooleanFunctionExpression() { } + virtual bool getValueAsBool(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + bool resultLeft = left->getValueAsBool(booleanVariableValues, integerVariableValues); + bool resultRight = right->getValueAsBool(booleanVariableValues, integerVariableValues); + switch(functionType) { + case AND: return resultLeft & resultRight; break; + case OR: return resultLeft | resultRight; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean binary operator: '" << functionType << "'."; + } + } + virtual std::string toString() const { - std::string result = left->toString(); - switch (functor) { - case AND: result += " & "; break; - case OR: result += " | "; break; - case XOR: result += " ^ "; break; - case IMPLIES: result += " => "; break; + std::stringstream result; + result << left->toString(); + switch (functionType) { + case AND: result << " & "; break; + case OR: result << " | "; break; } - result += right->toString(); + result << right->toString(); - return result; + return result.str(); } + +private: + std::shared_ptr left; + std::shared_ptr right; + FunctionType functionType; }; -} +} // namespace expressions -} +} // namespace ir -} +} // namespace storm -#endif /* BINARYBOOLEANFUNCTIONEXPRESSION_H_ */ +#endif /* STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ */ diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h index 5b928768e..28ba2b3f2 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.h +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.h @@ -18,23 +18,53 @@ namespace expressions { class BinaryNumericalFunctionExpression : public BaseExpression { public: - std::shared_ptr left; - std::shared_ptr right; - enum FunctorType {PLUS, MINUS, TIMES, DIVIDE} functor; + enum FunctionType {PLUS, MINUS, TIMES, DIVIDE}; + + BinaryNumericalFunctionExpression(ReturnType type, std::shared_ptr left, std::shared_ptr right, FunctionType functionType) : BaseExpression(type), left(left), right(right), functionType(functionType) { - BinaryNumericalFunctionExpression(std::shared_ptr left, std::shared_ptr right, FunctorType functor) { - this->left = left; - this->right = right; - this->functor = functor; } virtual ~BinaryNumericalFunctionExpression() { } + virtual int_fast64_t getValueAsInt(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + if (this->getType() != int_) { + BaseExpression::getValueAsInt(booleanVariableValues, integerVariableValues); + } + + int_fast64_t resultLeft = left->getValueAsInt(booleanVariableValues, integerVariableValues); + int_fast64_t resultRight = right->getValueAsInt(booleanVariableValues, integerVariableValues); + switch(functionType) { + case PLUS: return resultLeft + resultRight; break; + case MINUS: return resultLeft - resultRight; break; + case TIMES: return resultLeft * resultRight; break; + case DIVIDE: return resultLeft / resultRight; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown numeric binary operator: '" << functionType << "'."; + } + } + + virtual double getValueAsDouble(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + if (this->getType() != double_) { + BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues); + } + + double resultLeft = left->getValueAsDouble(booleanVariableValues, integerVariableValues); + double resultRight = right->getValueAsDouble(booleanVariableValues, integerVariableValues); + switch(functionType) { + case PLUS: return resultLeft + resultRight; break; + case MINUS: return resultLeft - resultRight; break; + case TIMES: return resultLeft * resultRight; break; + case DIVIDE: return resultLeft / resultRight; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown numeric binary operator: '" << functionType << "'."; + } + } + virtual std::string toString() const { std::string result = left->toString(); - switch (functor) { + switch (functionType) { case PLUS: result += " + "; break; case MINUS: result += " - "; break; case TIMES: result += " * "; break; @@ -44,7 +74,10 @@ public: return result; } - +private: + std::shared_ptr left; + std::shared_ptr right; + FunctionType functionType; }; } diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h index 625b801f5..db834ea93 100644 --- a/src/ir/expressions/BinaryRelationExpression.h +++ b/src/ir/expressions/BinaryRelationExpression.h @@ -18,23 +18,33 @@ namespace expressions { class BinaryRelationExpression : public BaseExpression { public: - std::shared_ptr left; - std::shared_ptr right; - enum RelationType {EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL} relation; + enum RelationType {EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL}; + + BinaryRelationExpression(std::shared_ptr left, std::shared_ptr right, RelationType relationType) : BaseExpression(bool_), left(left), right(right), relationType(relationType) { - BinaryRelationExpression(std::shared_ptr left, std::shared_ptr right, RelationType relation) { - this->left = left; - this->right = right; - this->relation = relation; } virtual ~BinaryRelationExpression() { } + virtual bool getValueAsBool(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + int_fast64_t resultLeft = left->getValueAsInt(booleanVariableValues, integerVariableValues); + int_fast64_t resultRight = right->getValueAsInt(booleanVariableValues, integerVariableValues); + switch(relationType) { + case EQUAL: return resultLeft == resultRight; break; + case LESS: return resultLeft < resultRight; break; + case LESS_OR_EQUAL: return resultLeft <= resultRight; break; + case GREATER: return resultLeft > resultRight; break; + case GREATER_OR_EQUAL: return resultLeft >= resultRight; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean binary relation: '" << relationType << "'."; + } + } + virtual std::string toString() const { std::string result = left->toString(); - switch (relation) { + switch (relationType) { case EQUAL: result += " = "; break; case LESS: result += " < "; break; case LESS_OR_EQUAL: result += " <= "; break; @@ -46,6 +56,10 @@ public: return result; } +private: + std::shared_ptr left; + std::shared_ptr right; + RelationType relationType; }; } diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h index a10c2363e..cfd6ae418 100644 --- a/src/ir/expressions/BooleanConstantExpression.h +++ b/src/ir/expressions/BooleanConstantExpression.h @@ -20,7 +20,7 @@ namespace expressions { class BooleanConstantExpression : public ConstantExpression { public: - BooleanConstantExpression(std::string constantName) : ConstantExpression(constantName) { + BooleanConstantExpression(std::string constantName) : ConstantExpression(bool_, constantName) { defined = false; value = false; } @@ -29,6 +29,15 @@ public: } + virtual bool getValueAsBool(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + if (!defined) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Boolean constant '" << this->getConstantName() << "' is undefined."; + } else { + return value; + } + } + virtual std::string toString() const { std::string result = this->constantName; if (defined) { diff --git a/src/ir/expressions/BooleanLiteral.h b/src/ir/expressions/BooleanLiteral.h index 81950e52a..f7d4e9957 100644 --- a/src/ir/expressions/BooleanLiteral.h +++ b/src/ir/expressions/BooleanLiteral.h @@ -20,14 +20,18 @@ class BooleanLiteral : public BaseExpression { public: bool value; - BooleanLiteral(bool value) { - this->value = value; + BooleanLiteral(bool value) : BaseExpression(bool_), value(value) { + } virtual ~BooleanLiteral() { } + virtual bool getValueAsBool(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + return value; + } + virtual std::string toString() const { if (value) { return std::string("true"); diff --git a/src/ir/expressions/ConstantExpression.h b/src/ir/expressions/ConstantExpression.h index 239b3dc68..79c356dba 100644 --- a/src/ir/expressions/ConstantExpression.h +++ b/src/ir/expressions/ConstantExpression.h @@ -20,14 +20,18 @@ class ConstantExpression : public BaseExpression { public: std::string constantName; - ConstantExpression(std::string constantName) { - this->constantName = constantName; + ConstantExpression(ReturnType type, std::string constantName) : BaseExpression(type), constantName(constantName) { + } virtual ~ConstantExpression() { } + std::string const& getConstantName() const { + return constantName; + } + virtual std::string toString() const { return constantName; } diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h index 3a7363a65..9ad1e61d6 100644 --- a/src/ir/expressions/DoubleConstantExpression.h +++ b/src/ir/expressions/DoubleConstantExpression.h @@ -18,15 +18,23 @@ namespace expressions { class DoubleConstantExpression : public ConstantExpression { public: - DoubleConstantExpression(std::string constantName) : ConstantExpression(constantName) { - defined = false; - value = 0.0; + DoubleConstantExpression(std::string constantName) : ConstantExpression(double_, constantName), defined(false), value(0) { + } virtual ~DoubleConstantExpression() { } + virtual double getValueAsDouble(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + if (!defined) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Double constant '" << this->getConstantName() << "' is undefined."; + } else { + return value; + } + } + virtual std::string toString() const { std::string result = this->constantName; if (defined) { @@ -48,8 +56,9 @@ public: this->value = value; } - double value; +private: bool defined; + double value; }; } diff --git a/src/ir/expressions/DoubleLiteral.h b/src/ir/expressions/DoubleLiteral.h index dbdcf55ca..e7854cfa5 100644 --- a/src/ir/expressions/DoubleLiteral.h +++ b/src/ir/expressions/DoubleLiteral.h @@ -22,14 +22,18 @@ class DoubleLiteral : public BaseExpression { public: double value; - DoubleLiteral(double value) { - this->value = value; + DoubleLiteral(double value) : BaseExpression(double_), value(value) { + } virtual ~DoubleLiteral() { } + virtual double getValueAsDouble(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + return value; + } + virtual std::string toString() const { return boost::lexical_cast(value); } diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h index 5ff4d7f87..5e7c46ee7 100644 --- a/src/ir/expressions/IntegerConstantExpression.h +++ b/src/ir/expressions/IntegerConstantExpression.h @@ -18,15 +18,23 @@ namespace expressions { class IntegerConstantExpression : public ConstantExpression { public: - IntegerConstantExpression(std::string constantName) : ConstantExpression(constantName) { - defined = false; - value = 0; + IntegerConstantExpression(std::string constantName) : ConstantExpression(int_, constantName), defined(false), value(0) { + } virtual ~IntegerConstantExpression() { } + virtual int_fast64_t getValueAsInt(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + if (!defined) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Integer constant '" << this->getConstantName() << "' is undefined."; + } else { + return value; + } + } + virtual std::string toString() const { std::string result = this->constantName; if (defined) { @@ -43,13 +51,14 @@ public: return value; } - void define(int value) { + void define(int_fast64_t value) { defined = true; this->value = value; } - int value; +private: bool defined; + int_fast64_t value; }; } diff --git a/src/ir/expressions/IntegerLiteral.h b/src/ir/expressions/IntegerLiteral.h index aef509321..36c78a948 100644 --- a/src/ir/expressions/IntegerLiteral.h +++ b/src/ir/expressions/IntegerLiteral.h @@ -18,16 +18,20 @@ namespace expressions { class IntegerLiteral : public BaseExpression { public: - int value; + int_fast64_t value; + + IntegerLiteral(int_fast64_t value) : BaseExpression(int_), value(value) { - IntegerLiteral(int value) { - this->value = value; } virtual ~IntegerLiteral() { } + virtual int_fast64_t getValueAsInt(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + return value; + } + virtual std::string toString() const { return boost::lexical_cast(value); } diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.h b/src/ir/expressions/UnaryBooleanFunctionExpression.h index 893169b51..b21a70f87 100644 --- a/src/ir/expressions/UnaryBooleanFunctionExpression.h +++ b/src/ir/expressions/UnaryBooleanFunctionExpression.h @@ -18,27 +18,38 @@ namespace expressions { class UnaryBooleanFunctionExpression : public BaseExpression { public: - std::shared_ptr child; - enum FunctorType {NOT} functor; + enum FunctionType {NOT}; + + UnaryBooleanFunctionExpression(std::shared_ptr child, FunctionType functionType) : BaseExpression(bool_), child(child), functionType(functionType) { - UnaryBooleanFunctionExpression(std::shared_ptr child, FunctorType functor) { - this->child = child; - this->functor = functor; } virtual ~UnaryBooleanFunctionExpression() { } + virtual bool getValueAsBool(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + bool resultChild = child->getValueAsBool(booleanVariableValues, integerVariableValues); + switch(functionType) { + case NOT: return !resultChild; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean unary operator: '" << functionType << "'."; + } + } + virtual std::string toString() const { std::string result = ""; - switch (functor) { + switch (functionType) { case NOT: result += "!"; break; } result += child->toString(); return result; } + +private: + std::shared_ptr child; + FunctionType functionType; }; } diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h index f697f35eb..db5cb2945 100644 --- a/src/ir/expressions/UnaryNumericalFunctionExpression.h +++ b/src/ir/expressions/UnaryNumericalFunctionExpression.h @@ -18,27 +18,55 @@ namespace expressions { class UnaryNumericalFunctionExpression : public BaseExpression { public: - std::shared_ptr child; - enum FunctorType {MINUS} functor; + enum FunctionType {MINUS}; + + UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr child, FunctionType functionType) : BaseExpression(type), child(child), functionType(functionType) { - UnaryNumericalFunctionExpression(std::shared_ptr child, FunctorType functor) { - this->child = child; - this->functor = functor; } virtual ~UnaryNumericalFunctionExpression() { } + virtual int_fast64_t getValueAsInt(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + if (this->getType() != int_) { + BaseExpression::getValueAsInt(booleanVariableValues, integerVariableValues); + } + + int_fast64_t resultChild = child->getValueAsInt(booleanVariableValues, integerVariableValues); + switch(functionType) { + case MINUS: return -resultChild; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown numerical unary operator: '" << functionType << "'."; + } + } + + virtual double getValueAsDouble(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + if (this->getType() != double_) { + BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues); + } + + double resultChild = child->getValueAsDouble(booleanVariableValues, integerVariableValues); + switch(functionType) { + case MINUS: return -resultChild; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown numerical unary operator: '" << functionType << "'."; + } + } + virtual std::string toString() const { std::string result = ""; - switch (functor) { + switch (functionType) { case MINUS: result += "-"; break; } result += child->toString(); return result; } + +private: + std::shared_ptr child; + FunctionType functionType; }; } diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h index a6a27fa43..02ca79a36 100644 --- a/src/ir/expressions/VariableExpression.h +++ b/src/ir/expressions/VariableExpression.h @@ -20,9 +20,7 @@ namespace expressions { class VariableExpression : public BaseExpression { public: - std::string variableName; - - VariableExpression(std::string variableName) : variableName(variableName) { + VariableExpression(ReturnType type, uint_fast64_t index, std::string variableName) : BaseExpression(type), index(index), variableName(variableName) { } @@ -33,6 +31,35 @@ public: virtual std::string toString() const { return variableName; } + + virtual int_fast64_t getValueAsInt(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + if (this->getType() != int_) { + BaseExpression::getValueAsInt(booleanVariableValues, integerVariableValues); + } + + return integerVariableValues[index]; + } + + virtual bool getValueAsBool(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + if (this->getType() != bool_) { + BaseExpression::getValueAsBool(booleanVariableValues, integerVariableValues); + } + + return booleanVariableValues[index]; + } + + virtual double getValueAsDouble(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + if (this->getType() != double_) { + BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues); + } + + throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression with " + << " variable '" << variableName << "' of type double."; + } + +private: + uint_fast64_t index; + std::string variableName; }; } diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 96ae88ca7..fe6c4fd8e 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -51,7 +51,7 @@ struct PrismParser::PrismGrammar : qi::grammar> *(qi::alnum | qi::char_('_'))) - booleanVariableNames_ - integerVariableNames_ - allConstantNames_ - labelNames_ - moduleNames_ - keywords_]]; freeIdentifierName.name("unused identifier"); @@ -87,9 +87,9 @@ struct PrismParser::PrismGrammar : qi::grammar> integerExpression >> qi::lit(")") | integerConstantExpression); atomicIntegerExpression.name("integer expression"); - integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; + integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; integerMultExpression.name("integer expression"); - integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; integerPlusExpression.name("integer expression"); integerExpression %= integerPlusExpression; integerExpression.name("integer expression"); @@ -97,9 +97,9 @@ struct PrismParser::PrismGrammar : qi::grammar> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); constantAtomicIntegerExpression.name("constant integer expression"); - constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; + constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; constantIntegerMultExpression.name("constant integer expression"); - constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantIntegerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantIntegerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; constantIntegerPlusExpression.name("constant integer expression"); constantIntegerExpression %= constantIntegerPlusExpression; constantIntegerExpression.name("constant integer expression"); @@ -107,9 +107,9 @@ struct PrismParser::PrismGrammar : qi::grammar> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression); constantAtomicDoubleExpression.name("constant double expression"); - constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicDoubleExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; + constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicDoubleExpression)[qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::double_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; constantDoubleMultExpression.name("constant double expression"); - constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantDoubleMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantDoubleMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::double_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; constantDoublePlusExpression.name("constant double expression"); constantDoubleExpression %= constantDoublePlusExpression; constantDoubleExpression.name("constant double expression"); @@ -119,7 +119,7 @@ struct PrismParser::PrismGrammar : qi::grammar> booleanExpression >> qi::lit(")") | booleanConstantExpression); atomicBooleanExpression.name("boolean expression"); - notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))]; + notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::NOT))]; notExpression.name("boolean expression"); andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))]; andExpression.name("boolean expression"); @@ -133,7 +133,7 @@ struct PrismParser::PrismGrammar : qi::grammar> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); constantAtomicBooleanExpression.name("constant boolean expression"); - constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))]; + constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::NOT))]; constantNotExpression.name("constant boolean expression"); constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))]; constantAndExpression.name("constant boolean expression"); @@ -175,11 +175,11 @@ struct PrismParser::PrismGrammar : qi::grammar> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > integerExpression > qi::lit(")"))[phoenix::bind(assignedLocalIntegerVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_2)))] | (qi::lit("(") > unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > booleanExpression > qi::lit(")"))[phoenix::bind(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("=") > integerExpression > qi::lit(")"))[phoenix::bind(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("=") > booleanExpression > qi::lit(")"))[phoenix::bind(assignedLocalBooleanVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_2)))]; assignmentDefinition.name("assignment"); - assignmentDefinitionList = assignmentDefinition(qi::_r1) % "&"; + assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&"; assignmentDefinitionList.name("assignment list"); - updateDefinition = (constantDoubleExpression > qi::lit(":")[phoenix::clear(phoenix::ref(assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a))[qi::_val = phoenix::construct(qi::_1, qi::_a)]; + updateDefinition = (constantDoubleExpression > qi::lit(":")[phoenix::clear(phoenix::ref(assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b)]; updateDefinition.name("update"); updateListDefinition = +updateDefinition % "+"; updateListDefinition.name("update list"); @@ -187,15 +187,15 @@ struct PrismParser::PrismGrammar : qi::grammar> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(phoenix::val(qi::_1), qi::_b))), qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1)]; + booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct(phoenix::val(nextBooleanVariableIndex), phoenix::val(qi::_1), qi::_b)), phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::val(nextBooleanVariableIndex))), qi::_a = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::bool_, phoenix::val(nextBooleanVariableIndex), qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1), phoenix::ref(nextBooleanVariableIndex)++]; booleanVariableDefinition.name("boolean variable declaration"); - integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_2, qi::_3, qi::_b))), qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1)]; + integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct(phoenix::val(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3, qi::_b)), phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::val(nextIntegerVariableIndex))), qi::_a = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, phoenix::val(nextIntegerVariableIndex), qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1), phoenix::ref(nextIntegerVariableIndex)++]; integerVariableDefinition.name("integer variable declaration"); - variableDefinition = (booleanVariableDefinition(qi::_r1) | integerVariableDefinition(qi::_r2)); + variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4)); variableDefinition.name("variable declaration"); // This block defines all entities that are needed for parsing a module. - moduleDefinition = (qi::lit("module")[phoenix::clear(phoenix::ref(localBooleanVariables_)), phoenix::clear(phoenix::ref(localIntegerVariables_))] > freeIdentifierName > *(variableDefinition(qi::_a, qi::_b)) > +commandDefinition > qi::lit("endmodule"))[phoenix::bind(moduleNames_.add, qi::_1, qi::_1), qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_2)]; + moduleDefinition = (qi::lit("module")[phoenix::clear(phoenix::ref(localBooleanVariables_)), phoenix::clear(phoenix::ref(localIntegerVariables_))] > freeIdentifierName > *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) > +commandDefinition > qi::lit("endmodule"))[phoenix::bind(moduleNames_.add, qi::_1, qi::_1), qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)]; moduleDefinition.name("module"); moduleDefinitionList %= +moduleDefinition; moduleDefinitionList.name("module list"); @@ -234,19 +234,19 @@ struct PrismParser::PrismGrammar : qi::grammar(), Skipper> moduleDefinitionList; // Rules for module definition. - qi::rule, std::map>, Skipper> moduleDefinition; + qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; // Rules for variable definitions. - qi::rule&, std::map&), Skipper> variableDefinition; - qi::rule&), qi::locals, std::shared_ptr>, Skipper> booleanVariableDefinition; - qi::rule&), qi::locals, std::shared_ptr>, Skipper> integerVariableDefinition; + qi::rule&, std::vector&, std::map&, std::map&), Skipper> variableDefinition; + qi::rule&, std::map&), qi::locals, std::shared_ptr>, Skipper> booleanVariableDefinition; + qi::rule&, std::map&), qi::locals, std::shared_ptr>, Skipper> integerVariableDefinition; // Rules for command definitions. qi::rule, Skipper> commandDefinition; qi::rule(), Skipper> updateListDefinition; - qi::rule>, Skipper> updateDefinition; - qi::rule&), Skipper> assignmentDefinitionList; - qi::rule&), Skipper> assignmentDefinition; + qi::rule, std::map>, Skipper> updateDefinition; + qi::rule&, std::map&), Skipper> assignmentDefinitionList; + qi::rule&, std::map&), Skipper> assignmentDefinition; // Rules for variable/command names. qi::rule integerVariableName; @@ -377,6 +377,10 @@ struct PrismParser::PrismGrammar : qi::grammar> integerVariables_, booleanVariables_; diff --git a/src/storm.cpp b/src/storm.cpp index c4c75d09a..678189be5 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -36,6 +36,7 @@ #include "log4cplus/fileappender.h" #include "src/parser/PrismParser.h" +#include "src/adapters/IntermediateRepresentationAdapter.h" #include "src/exceptions/InvalidSettingsException.h" @@ -241,7 +242,8 @@ int main(const int argc, const char* argv[]) { // testChecking(); storm::parser::PrismParser parser; - parser.parseFile("test.input"); + std::shared_ptr program = parser.parseFile("test.input"); + storm::storage::SquareSparseMatrix* result = storm::adapters::IntermediateRepresentationAdapter::toSparseMatrix(*program); cleanUp(); return 0; diff --git a/test.input b/test.input index 5339a8416..700951a05 100644 --- a/test.input +++ b/test.input @@ -1,24 +1,24 @@ +// Knuth's model of a fair die using only fair coins dtmc module die -// local state -s : [0..7] init 0; -// value of the dice -d : [0..6] init 0; + + // local state + s : [0..7] init 0; + // value of the dice + d : [0..6] init 0; + + [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); + [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); + [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); + [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); + [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); + [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); + [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); + [] s=7 -> 1: (s'=7); -[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); -[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); -[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); -[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); -[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); -[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); -[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); -[] s=7 -> 1 : (s'=7); endmodule rewards "coin_flips" [] s<7 : 1; - s>3 : 1; endrewards - -label test = s>2;