From c19418b8711893cbb3047111fa4c22f65632fe75 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 14 Jan 2013 16:59:15 +0100 Subject: [PATCH] Intermediate commit to switch workplace. --- .../IntermediateRepresentationAdapter.h | 112 ++++++++++++++++-- src/ir/TransitionReward.h | 2 + src/ir/Update.cpp | 4 +- src/ir/Variable.h | 1 + src/ir/expressions/BaseExpression.h | 6 +- .../BinaryBooleanFunctionExpression.h | 6 +- .../BinaryNumericalFunctionExpression.h | 16 +-- src/ir/expressions/BinaryRelationExpression.h | 6 +- .../expressions/BooleanConstantExpression.h | 2 +- src/ir/expressions/BooleanLiteral.h | 2 +- src/ir/expressions/DoubleConstantExpression.h | 2 +- src/ir/expressions/DoubleLiteral.h | 2 +- .../expressions/IntegerConstantExpression.h | 2 +- src/ir/expressions/IntegerLiteral.h | 2 +- .../UnaryBooleanFunctionExpression.h | 4 +- .../UnaryNumericalFunctionExpression.h | 12 +- src/ir/expressions/VariableExpression.h | 16 +-- src/parser/PrismParser.cpp | 7 +- src/storm.cpp | 2 + 19 files changed, 148 insertions(+), 58 deletions(-) diff --git a/src/adapters/IntermediateRepresentationAdapter.h b/src/adapters/IntermediateRepresentationAdapter.h index d60325b11..01e5a9a17 100644 --- a/src/adapters/IntermediateRepresentationAdapter.h +++ b/src/adapters/IntermediateRepresentationAdapter.h @@ -35,6 +35,13 @@ public: } }; +class StateCompare { +public: + bool operator()(StateType* state1, StateType* state2) const { + return *state1 == *state2; + } +}; + class IntermediateRepresentationAdapter { public: template @@ -72,24 +79,20 @@ public: } } - StateType* initialState = new StateType(std::vector(), std::vector()); - std::get<0>(*initialState).resize(numberOfBooleanVariables); - std::get<1>(*initialState).resize(numberOfIntegerVariables); + StateType* initialState = getNewState(numberOfBooleanVariables, numberOfIntegerVariables); for (uint_fast64_t i = 0; i < numberOfBooleanVariables; ++i) { - bool initialValue = booleanVariables[i].getInitialValue()->getValueAsBool(std::get<0>(*initialState), std::get<1>(*initialState)); + bool initialValue = booleanVariables[i].getInitialValue()->getValueAsBool(*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)); + int_fast64_t initialValue = integerVariables[i].getInitialValue()->getValueAsInt(*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::unordered_map stateToIndexMap; std::vector allStates; std::queue stateQueue; @@ -97,6 +100,7 @@ public: stateQueue.push(initialState); stateToIndexMap[initialState] = 0; + uint_fast64_t totalNumberOfTransitions = 0; while (!stateQueue.empty()) { // Get first state in queue. StateType* currentState = stateQueue.front(); @@ -111,15 +115,44 @@ public: 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))) { + if (command.getGuard()->getValueAsBool(*currentState)) { + std::unordered_map stateToProbabilityMap; for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { storm::ir::Update const& update = command.getUpdate(k); + StateType* newState = new StateType(*currentState); + 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 = + setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(*currentState)); + } + std::map const& integerAssignmentMap = update.getIntegerAssignments(); + for (auto assignedVariable : integerAssignmentMap) { + setValue(newState, integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(*currentState)); + } + + auto probIt = stateToProbabilityMap.find(newState); + if (probIt != stateToProbabilityMap.end()) { + stateToProbabilityMap[newState] += update.getLikelihoodExpression()->getValueAsDouble(*currentState); + } else { + ++totalNumberOfTransitions; + stateToProbabilityMap[newState] = update.getLikelihoodExpression()->getValueAsDouble(*currentState); + } + auto it = stateToIndexMap.find(newState); + if (it != stateToIndexMap.end()) { + // Delete the state object directly as we have already seen that state. + delete newState; + } else { + // Add state to the queue of states that are still to be explored. + stateQueue.push(newState); + + // Add state to list of all states so that we can delete it at the end. + allStates.push_back(newState); + + // Give a unique index to the newly found state. + stateToIndexMap[newState] = nextIndex; + ++nextIndex; } } } @@ -127,13 +160,68 @@ public: } } + std::cout << "Found " << allStates.size() << " reachable states and " << totalNumberOfTransitions << " transitions."; + + storm::storage::SquareSparseMatrix* resultMatrix = new storm::storage::SquareSparseMatrix(allStates.size()); + resultMatrix->initialize(totalNumberOfTransitions); + + for (StateType* state : allStates) { + // 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(*currentState)) { + std::unordered_map stateToProbabilityMap; + for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { + storm::ir::Update const& update = command.getUpdate(k); + + StateType* newState = new StateType(*currentState); + + std::map const& booleanAssignmentMap = update.getBooleanAssignments(); + for (auto assignedVariable : booleanAssignmentMap) { + setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(*currentState)); + } + std::map const& integerAssignmentMap = update.getIntegerAssignments(); + for (auto assignedVariable : integerAssignmentMap) { + setValue(newState, integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(*currentState)); + } + + auto probIt = stateToProbabilityMap.find(newState); + if (probIt != stateToProbabilityMap.end()) { + stateToProbabilityMap[newState] += update.getLikelihoodExpression()->getValueAsDouble(*currentState); + } else { + ++totalNumberOfTransitions; + stateToProbabilityMap[newState] = update.getLikelihoodExpression()->getValueAsDouble(*currentState); + } + } + // Now free all the elements we allocated. for (auto element : allStates) { delete element; } - return nullptr; + return resultMatrix; } +private: + static StateType* getNewState(uint_fast64_t numberOfBooleanVariables, uint_fast64_t numberOfIntegerVariables) { + StateType* result = new StateType(); + result->first.resize(numberOfBooleanVariables); + result->second.resize(numberOfIntegerVariables); + return result; + } + + static void setValue(StateType* state, uint_fast64_t index, bool value) { + std::get<0>(*state)[index] = value; + } + + static void setValue(StateType* state, uint_fast64_t index, int_fast64_t value) { + std::get<1>(*state)[index] = value; + } }; } diff --git a/src/ir/TransitionReward.h b/src/ir/TransitionReward.h index eaffe10ae..07e0084e0 100644 --- a/src/ir/TransitionReward.h +++ b/src/ir/TransitionReward.h @@ -10,6 +10,8 @@ #include "expressions/BaseExpression.h" +#include + namespace storm { namespace ir { diff --git a/src/ir/Update.cpp b/src/ir/Update.cpp index 668b543da..edacb6fe9 100644 --- a/src/ir/Update.cpp +++ b/src/ir/Update.cpp @@ -79,18 +79,18 @@ std::string Update::toString() const { uint_fast64_t i = 0; for (auto assignment : booleanAssignments) { result << assignment.second.toString(); - ++i; if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) { result << " & "; } + ++i; } i = 0; for (auto assignment : integerAssignments) { result << assignment.second.toString(); - ++i; if (i < integerAssignments.size() - 1) { result << " & "; } + ++i; } return result.str(); } diff --git a/src/ir/Variable.h b/src/ir/Variable.h index eed1e538c..2c065a004 100644 --- a/src/ir/Variable.h +++ b/src/ir/Variable.h @@ -11,6 +11,7 @@ #include "expressions/BaseExpression.h" #include +#include namespace storm { diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h index b88953dce..3e228d5cf 100644 --- a/src/ir/expressions/BaseExpression.h +++ b/src/ir/expressions/BaseExpression.h @@ -37,7 +37,7 @@ public: } - virtual int_fast64_t getValueAsInt(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const& variableValues) const { if (type != int_) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" << this->getTypeName() << "' as 'int'."; @@ -46,7 +46,7 @@ public: << this->getTypeName() << " because evaluation implementation is missing."; } - virtual bool getValueAsBool(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { if (type != bool_) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" << this->getTypeName() << "' as 'bool'."; @@ -55,7 +55,7 @@ public: << this->getTypeName() << " because evaluation implementation is missing."; } - virtual double getValueAsDouble(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual double getValueAsDouble(std::pair, std::vector> const& variableValues) const { if (type != bool_) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" << this->getTypeName() << "' as 'double'."; diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.h b/src/ir/expressions/BinaryBooleanFunctionExpression.h index e26bd22f3..957c08658 100644 --- a/src/ir/expressions/BinaryBooleanFunctionExpression.h +++ b/src/ir/expressions/BinaryBooleanFunctionExpression.h @@ -31,9 +31,9 @@ public: } - virtual bool getValueAsBool(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { - bool resultLeft = left->getValueAsBool(booleanVariableValues, integerVariableValues); - bool resultRight = right->getValueAsBool(booleanVariableValues, integerVariableValues); + virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { + bool resultLeft = left->getValueAsBool(variableValues); + bool resultRight = right->getValueAsBool(variableValues); switch(functionType) { case AND: return resultLeft & resultRight; break; case OR: return resultLeft | resultRight; break; diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h index 28ba2b3f2..7a76320a9 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.h +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.h @@ -28,13 +28,13 @@ public: } - virtual int_fast64_t getValueAsInt(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const& variableValues) const { if (this->getType() != int_) { - BaseExpression::getValueAsInt(booleanVariableValues, integerVariableValues); + BaseExpression::getValueAsInt(variableValues); } - int_fast64_t resultLeft = left->getValueAsInt(booleanVariableValues, integerVariableValues); - int_fast64_t resultRight = right->getValueAsInt(booleanVariableValues, integerVariableValues); + int_fast64_t resultLeft = left->getValueAsInt(variableValues); + int_fast64_t resultRight = right->getValueAsInt(variableValues); switch(functionType) { case PLUS: return resultLeft + resultRight; break; case MINUS: return resultLeft - resultRight; break; @@ -45,13 +45,13 @@ public: } } - virtual double getValueAsDouble(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual double getValueAsDouble(std::pair, std::vector> const& variableValues) const { if (this->getType() != double_) { - BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues); + BaseExpression::getValueAsDouble(variableValues); } - double resultLeft = left->getValueAsDouble(booleanVariableValues, integerVariableValues); - double resultRight = right->getValueAsDouble(booleanVariableValues, integerVariableValues); + double resultLeft = left->getValueAsDouble(variableValues); + double resultRight = right->getValueAsDouble(variableValues); switch(functionType) { case PLUS: return resultLeft + resultRight; break; case MINUS: return resultLeft - resultRight; break; diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h index db834ea93..fe07f0749 100644 --- a/src/ir/expressions/BinaryRelationExpression.h +++ b/src/ir/expressions/BinaryRelationExpression.h @@ -28,9 +28,9 @@ public: } - 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); + virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { + int_fast64_t resultLeft = left->getValueAsInt(variableValues); + int_fast64_t resultRight = right->getValueAsInt(variableValues); switch(relationType) { case EQUAL: return resultLeft == resultRight; break; case LESS: return resultLeft < resultRight; break; diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h index cfd6ae418..58204fee4 100644 --- a/src/ir/expressions/BooleanConstantExpression.h +++ b/src/ir/expressions/BooleanConstantExpression.h @@ -29,7 +29,7 @@ public: } - virtual bool getValueAsBool(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { if (!defined) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << "Boolean constant '" << this->getConstantName() << "' is undefined."; diff --git a/src/ir/expressions/BooleanLiteral.h b/src/ir/expressions/BooleanLiteral.h index f7d4e9957..b7ee88997 100644 --- a/src/ir/expressions/BooleanLiteral.h +++ b/src/ir/expressions/BooleanLiteral.h @@ -28,7 +28,7 @@ public: } - virtual bool getValueAsBool(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { return value; } diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h index 9ad1e61d6..c852329c1 100644 --- a/src/ir/expressions/DoubleConstantExpression.h +++ b/src/ir/expressions/DoubleConstantExpression.h @@ -26,7 +26,7 @@ public: } - virtual double getValueAsDouble(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual double getValueAsDouble(std::pair, std::vector> const& variableValues) const { if (!defined) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << "Double constant '" << this->getConstantName() << "' is undefined."; diff --git a/src/ir/expressions/DoubleLiteral.h b/src/ir/expressions/DoubleLiteral.h index e7854cfa5..2679a7a5d 100644 --- a/src/ir/expressions/DoubleLiteral.h +++ b/src/ir/expressions/DoubleLiteral.h @@ -30,7 +30,7 @@ public: } - virtual double getValueAsDouble(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual double getValueAsDouble(std::pair, std::vector> const& variableValues) const { return value; } diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h index 5e7c46ee7..250b085a3 100644 --- a/src/ir/expressions/IntegerConstantExpression.h +++ b/src/ir/expressions/IntegerConstantExpression.h @@ -26,7 +26,7 @@ public: } - virtual int_fast64_t getValueAsInt(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const& variableValues) const { if (!defined) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << "Integer constant '" << this->getConstantName() << "' is undefined."; diff --git a/src/ir/expressions/IntegerLiteral.h b/src/ir/expressions/IntegerLiteral.h index 36c78a948..c5cd06119 100644 --- a/src/ir/expressions/IntegerLiteral.h +++ b/src/ir/expressions/IntegerLiteral.h @@ -28,7 +28,7 @@ public: } - virtual int_fast64_t getValueAsInt(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const& variableValues) const { return value; } diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.h b/src/ir/expressions/UnaryBooleanFunctionExpression.h index b21a70f87..e0fae6c5b 100644 --- a/src/ir/expressions/UnaryBooleanFunctionExpression.h +++ b/src/ir/expressions/UnaryBooleanFunctionExpression.h @@ -28,8 +28,8 @@ public: } - virtual bool getValueAsBool(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { - bool resultChild = child->getValueAsBool(booleanVariableValues, integerVariableValues); + virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { + bool resultChild = child->getValueAsBool(variableValues); switch(functionType) { case NOT: return !resultChild; break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h index db5cb2945..8b746c1c7 100644 --- a/src/ir/expressions/UnaryNumericalFunctionExpression.h +++ b/src/ir/expressions/UnaryNumericalFunctionExpression.h @@ -28,12 +28,12 @@ public: } - virtual int_fast64_t getValueAsInt(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const& variableValues) const { if (this->getType() != int_) { - BaseExpression::getValueAsInt(booleanVariableValues, integerVariableValues); + BaseExpression::getValueAsInt(variableValues); } - int_fast64_t resultChild = child->getValueAsInt(booleanVariableValues, integerVariableValues); + int_fast64_t resultChild = child->getValueAsInt(variableValues); switch(functionType) { case MINUS: return -resultChild; break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " @@ -41,12 +41,12 @@ public: } } - virtual double getValueAsDouble(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual double getValueAsDouble(std::pair, std::vector> const& variableValues) const { if (this->getType() != double_) { - BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues); + BaseExpression::getValueAsDouble(variableValues); } - double resultChild = child->getValueAsDouble(booleanVariableValues, integerVariableValues); + double resultChild = child->getValueAsDouble(variableValues); switch(functionType) { case MINUS: return -resultChild; break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h index 02ca79a36..47b2087cd 100644 --- a/src/ir/expressions/VariableExpression.h +++ b/src/ir/expressions/VariableExpression.h @@ -32,25 +32,25 @@ public: return variableName; } - virtual int_fast64_t getValueAsInt(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const& variableValues) const { if (this->getType() != int_) { - BaseExpression::getValueAsInt(booleanVariableValues, integerVariableValues); + BaseExpression::getValueAsInt(variableValues); } - return integerVariableValues[index]; + return variableValues.second[index]; } - virtual bool getValueAsBool(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { if (this->getType() != bool_) { - BaseExpression::getValueAsBool(booleanVariableValues, integerVariableValues); + BaseExpression::getValueAsBool(variableValues); } - return booleanVariableValues[index]; + return variableValues.first[index]; } - virtual double getValueAsDouble(std::vector const& booleanVariableValues, std::vector const& integerVariableValues) const { + virtual double getValueAsDouble(std::pair, std::vector> const& variableValues) const { if (this->getType() != double_) { - BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues); + BaseExpression::getValueAsDouble(variableValues); } throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression with " diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index fe6c4fd8e..92b89fd17 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -459,11 +459,8 @@ std::shared_ptr PrismParser::parse(std::istream& inputStream } msg << std::endl; -// On Mac OS, exception messages are not displayed in case an exception is propagated to the -// operating system, so we need to display the message ourselves. -#if defined(MACOSX) - std::cout << msg.str(); -#endif + std::cerr << msg.str(); + // Now propagate exception. throw storm::exceptions::WrongFileFormatException() << msg.str(); } diff --git a/src/storm.cpp b/src/storm.cpp index 678189be5..cbf16faa8 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -244,6 +244,8 @@ int main(const int argc, const char* argv[]) { storm::parser::PrismParser parser; std::shared_ptr program = parser.parseFile("test.input"); storm::storage::SquareSparseMatrix* result = storm::adapters::IntermediateRepresentationAdapter::toSparseMatrix(*program); + result->print(); + delete result; cleanUp(); return 0;