From 231d2223a9731e49bccc47b9c62f49652b536d60 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 14 Jan 2015 21:15:39 +0100 Subject: [PATCH] Model building works again (more or less) Former-commit-id: fa6843fcdc435ba75e3fabf290ce2db04b9930ee --- src/adapters/ExplicitModelAdapter.h | 35 ++++++-------- src/parser/PrismParser.cpp | 18 +++++-- src/storage/BitVector.cpp | 2 +- src/storage/BitVectorHashMap.cpp | 1 + .../expressions/ExprtkExpressionEvaluator.cpp | 3 ++ .../expressions/ToExprtkStringVisitor.cpp | 48 ++++++++++++++----- src/storage/prism/Assignment.cpp | 2 +- src/storage/prism/Update.cpp | 1 + 8 files changed, 70 insertions(+), 40 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index db495f849..06c9a2ba4 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -194,14 +194,11 @@ namespace storm { private: static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExprtkExpressionEvaluator& evaluator) { - std::cout << "unpacking state... " << std::endl; for (auto const& booleanVariable : variableInformation.booleanVariables) { evaluator.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset)); - std::cout << booleanVariable.variable.getName() << " -> " << currentState.get(booleanVariable.bitOffset) << std::endl; } for (auto const& integerVariable : variableInformation.integerVariables) { evaluator.setIntegerValue(integerVariable.variable, currentState.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound); - std::cout << integerVariable.variable.getName() << " -> " << currentState.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound << std::endl; } } @@ -335,6 +332,7 @@ namespace storm { result.get().push_back(std::move(commands)); } + return result; } @@ -371,11 +369,13 @@ namespace storm { uint32_t stateIndex = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update, evaluator), stateInformation, stateQueue); // Update the choice by adding the probability/target state to it. - choice.addProbability(stateIndex, evaluator.asDouble(update.getLikelihoodExpression())); + ValueType probability = evaluator.asDouble(update.getLikelihoodExpression()); + choice.addProbability(stateIndex, probability); + probabilitySum += probability; } // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(std::abs(1 - probabilitySum) < storm::settings::generalSettings().getPrecision(), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "'."); + STORM_LOG_THROW(std::abs(1 - probabilitySum) < storm::settings::generalSettings().getPrecision(), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); } } @@ -445,13 +445,11 @@ namespace storm { for (auto const& stateProbabilityPair : *newTargetStates) { uint32_t actualIndex = getOrAddStateIndex(stateProbabilityPair.first, stateInformation, stateQueue); choice.addProbability(actualIndex, stateProbabilityPair.second); + probabilitySum += stateProbabilityPair.second; } // Check that the resulting distribution is in fact a distribution. - if (std::abs(1 - probabilitySum) > storm::settings::generalSettings().getPrecision()) { - LOG4CPLUS_ERROR(logger, "Sum of update probabilities do not some to one for some command."); - throw storm::exceptions::WrongFormatException() << "Sum of update probabilities do not some to one for some command."; - } + STORM_LOG_THROW(std::abs(1 - probabilitySum) <= storm::settings::generalSettings().getPrecision(), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); // Dispose of the temporary maps. delete currentTargetStates; @@ -507,10 +505,10 @@ namespace storm { for (auto const& integerVariable : variableInformation.integerVariables) { initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(integerVariable.initialValue - integerVariable.lowerBound)); } - std::cout << "initial state: " << initialState << std::endl; // Insert the initial state in the global state to index mapping and state queue. - getOrAddStateIndex(initialState, stateInformation, stateQueue); + uint32_t stateIndex = getOrAddStateIndex(initialState, stateInformation, stateQueue); + stateInformation.initialStateIndices.push_back(stateIndex); // Now explore the current state until there is no more reachable state. uint_fast64_t currentRow = 0; @@ -520,7 +518,6 @@ namespace storm { std::size_t currentStateBucket = stateQueue.front(); std::pair stateValuePair = stateInformation.stateToIndexMap.getBucketAndValue(currentStateBucket); storm::storage::BitVector const& currentState = stateValuePair.first; - std::cout << "current state: " << initialState << std::endl; unpackStateIntoEvaluator(currentState, variableInformation, evaluator); // Retrieve all choices for the current state. @@ -679,7 +676,7 @@ namespace storm { for (auto const& integerVariable : program.getGlobalIntegerVariables()) { int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound))); + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); variableInformation.integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, bitOffset, bitwidth); bitOffset += bitwidth; variableInformation.integerVariableToIndexMap[integerVariable.getExpressionVariable()] = variableInformation.integerVariables.size() - 1; @@ -693,7 +690,7 @@ namespace storm { for (auto const& integerVariable : module.getIntegerVariables()) { int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound))); + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); variableInformation.integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, bitOffset, bitwidth); bitOffset += bitwidth; variableInformation.integerVariableToIndexMap[integerVariable.getExpressionVariable()] = variableInformation.integerVariables.size() - 1; @@ -702,7 +699,6 @@ namespace storm { // Create the structure for storing the reachable state space. uint64_t bitsPerState = ((bitOffset / 64) + 1) * 64; - std::cout << "states have " << bitsPerState << " bits" << std::endl; StateInformation stateInformation(bitsPerState); // Determine whether we have to combine different choices to one or whether this model can have more than @@ -747,9 +743,8 @@ namespace storm { result.addAtomicProposition(label.getName()); } for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) { + unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getBucketAndValue(stateInformation.reachableStates[index]).first, variableInformation, evaluator); for (auto const& label : labels) { - unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getValue(stateInformation.reachableStates[index]), variableInformation, evaluator); - // Add label to state, if the corresponding expression is true. if (evaluator.asBool(label.getStatePredicateExpression())) { result.addAtomicPropositionToState(label.getName(), index); @@ -759,7 +754,7 @@ namespace storm { // Also label the initial state with the special label "init". result.addAtomicProposition("init"); - for (auto const& index : stateInformation.initialStateIndices) { + for (auto index : stateInformation.initialStateIndices) { result.addAtomicPropositionToState("init", index); } @@ -778,9 +773,9 @@ namespace storm { std::vector result(stateInformation.reachableStates.size()); for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) { - result[index] = ValueType(0); + result[index] = storm::utility::zero(); + unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getBucketAndValue(stateInformation.reachableStates[index]).first, variableInformation, evaluator); for (auto const& reward : rewards) { - unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getValue(stateInformation.reachableStates[index]), variableInformation, evaluator); // Add this reward to the state if the state is included in the state reward. if (evaluator.asBool(reward.getStatePredicateExpression())) { diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index d00cfcc52..b46684786 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -357,7 +357,13 @@ namespace storm { storm::prism::Command PrismParser::createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector const& updates, GlobalProgramInformation& globalProgramInformation) const { ++globalProgramInformation.currentCommandIndex; - return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, globalProgramInformation.actionIndices[actionName], actionName, guardExpression, updates, this->getFilename()); + if (!actionName.empty()) { + auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName); + if (nameIndexPair == globalProgramInformation.actionIndices.end()) { + globalProgramInformation.actionIndices[actionName] = globalProgramInformation.actionIndices.size(); + } + } + return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, actionName.empty() ? 0 : globalProgramInformation.actionIndices[actionName], actionName, guardExpression, updates, this->getFilename()); } storm::prism::Command PrismParser::createCommand(std::string const& actionName, GlobalProgramInformation& globalProgramInformation) const { @@ -490,12 +496,14 @@ namespace storm { newActionName = renamingPair->second; } - auto const& nameIndexPair = globalProgramInformation.actionIndices.find(newActionName); - if (nameIndexPair == globalProgramInformation.actionIndices.end()) { - globalProgramInformation.actionIndices[newActionName] = globalProgramInformation.actionIndices.size(); + if (!newActionName.empty()) { + auto const& nameIndexPair = globalProgramInformation.actionIndices.find(newActionName); + if (nameIndexPair == globalProgramInformation.actionIndices.end()) { + globalProgramInformation.actionIndices[newActionName] = globalProgramInformation.actionIndices.size(); + } } - commands.emplace_back(globalProgramInformation.currentCommandIndex, globalProgramInformation.actionIndices[newActionName], newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1)); + commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName.empty() ? 0 : globalProgramInformation.actionIndices[newActionName], newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1)); ++globalProgramInformation.currentCommandIndex; } diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 9c458ea7b..4f7d4fff8 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -441,7 +441,7 @@ namespace storm { } void BitVector::setFromInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits, uint64_t value) { - STORM_LOG_ASSERT((value >> numberOfBits) == 0, "Integer value to large to fit in the given number of bits."); + STORM_LOG_ASSERT((value >> numberOfBits) == 0, "Integer value too large to fit in the given number of bits."); uint64_t bucket = bitIndex >> 6; uint64_t bitIndexInBucket = bitIndex & mod64mask; diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp index d02ce69a2..115d25cd6 100644 --- a/src/storage/BitVectorHashMap.cpp +++ b/src/storage/BitVectorHashMap.cpp @@ -81,6 +81,7 @@ namespace storm { template ValueType BitVectorHashMap::getValue(storm::storage::BitVector const& key) const { + std::cout << "calling getValue with key " << key << std::endl; std::pair flagBucketPair = this->findBucket(key); STORM_LOG_ASSERT(flagBucketPair.first, "Unknown key."); return flagBucketPair.second; diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storage/expressions/ExprtkExpressionEvaluator.cpp index 83b3e725d..9cec207af 100644 --- a/src/storage/expressions/ExprtkExpressionEvaluator.cpp +++ b/src/storage/expressions/ExprtkExpressionEvaluator.cpp @@ -1,6 +1,8 @@ #include "src/storage/expressions/ExprtkExpressionEvaluator.h" #include "src/storage/expressions/ExpressionManager.h" +#include "src/utility/macros.h" + namespace storm { namespace expressions { ExprtkExpressionEvaluator::ExprtkExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : manager(manager.getSharedPointer()), booleanValues(manager.getNumberOfBooleanVariables()), integerValues(manager.getNumberOfIntegerVariables()), rationalValues(manager.getNumberOfRationalVariables()) { @@ -52,6 +54,7 @@ namespace storm { CompiledExpressionType& compiledExpression = result.first->second; compiledExpression.register_symbol_table(symbolTable); bool parsingOk = parser.compile(ToExprtkStringVisitor().toString(expression), compiledExpression); + STORM_LOG_ASSERT(parsingOk, "Expression was not properly parsed by ExprTk."); return compiledExpression; } diff --git a/src/storage/expressions/ToExprtkStringVisitor.cpp b/src/storage/expressions/ToExprtkStringVisitor.cpp index e9d2db2c0..9a1aac389 100644 --- a/src/storage/expressions/ToExprtkStringVisitor.cpp +++ b/src/storage/expressions/ToExprtkStringVisitor.cpp @@ -26,37 +26,37 @@ namespace storm { boost::any ToExprtkStringVisitor::visit(BinaryBooleanFunctionExpression const& expression) { switch (expression.getOperatorType()) { case BinaryBooleanFunctionExpression::OperatorType::And: - stream << "and("; - expression.getFirstOperand()->accept(*this); - stream << ","; + stream << "("; expression.getFirstOperand()->accept(*this); + stream << " and "; + expression.getSecondOperand()->accept(*this); stream << ")"; break; case BinaryBooleanFunctionExpression::OperatorType::Or: - stream << "or("; - expression.getFirstOperand()->accept(*this); - stream << ","; + stream << "("; expression.getFirstOperand()->accept(*this); + stream << " or "; + expression.getSecondOperand()->accept(*this); stream << ")"; break; case BinaryBooleanFunctionExpression::OperatorType::Xor: - stream << "xor("; - expression.getFirstOperand()->accept(*this); - stream << ","; + stream << "("; expression.getFirstOperand()->accept(*this); + stream << " xor "; + expression.getSecondOperand()->accept(*this); stream << ")"; break; case BinaryBooleanFunctionExpression::OperatorType::Implies: - stream << "or(not("; - expression.getFirstOperand()->accept(*this); - stream << "),"; + stream << "(not("; expression.getFirstOperand()->accept(*this); + stream << ") or "; + expression.getSecondOperand()->accept(*this); stream << ")"; break; case BinaryBooleanFunctionExpression::OperatorType::Iff: expression.getFirstOperand()->accept(*this); stream << "=="; - expression.getFirstOperand()->accept(*this); + expression.getSecondOperand()->accept(*this); break; } return boost::any(); @@ -65,29 +65,39 @@ namespace storm { boost::any ToExprtkStringVisitor::visit(BinaryNumericalFunctionExpression const& expression) { switch (expression.getOperatorType()) { case BinaryNumericalFunctionExpression::OperatorType::Plus: + stream << "("; expression.getFirstOperand()->accept(*this); stream << "+"; expression.getSecondOperand()->accept(*this); + stream << ")"; break; case BinaryNumericalFunctionExpression::OperatorType::Minus: + stream << "("; expression.getFirstOperand()->accept(*this); stream << "-"; expression.getSecondOperand()->accept(*this); + stream << ")"; break; case BinaryNumericalFunctionExpression::OperatorType::Times: + stream << "("; expression.getFirstOperand()->accept(*this); stream << "*"; expression.getSecondOperand()->accept(*this); + stream << ")"; break; case BinaryNumericalFunctionExpression::OperatorType::Divide: + stream << "("; expression.getFirstOperand()->accept(*this); stream << "/"; expression.getSecondOperand()->accept(*this); + stream << ")"; break; case BinaryNumericalFunctionExpression::OperatorType::Power: + stream << "("; expression.getFirstOperand()->accept(*this); stream << "^"; expression.getSecondOperand()->accept(*this); + stream << ")"; break; case BinaryNumericalFunctionExpression::OperatorType::Max: stream << "max("; @@ -110,34 +120,46 @@ namespace storm { boost::any ToExprtkStringVisitor::visit(BinaryRelationExpression const& expression) { switch (expression.getRelationType()) { case BinaryRelationExpression::RelationType::Equal: + stream << "("; expression.getFirstOperand()->accept(*this); stream << "=="; expression.getSecondOperand()->accept(*this); + stream << ")"; break; case BinaryRelationExpression::RelationType::NotEqual: + stream << "("; expression.getFirstOperand()->accept(*this); stream << "!="; expression.getSecondOperand()->accept(*this); + stream << ")"; break; case BinaryRelationExpression::RelationType::Less: + stream << "("; expression.getFirstOperand()->accept(*this); stream << "<"; expression.getSecondOperand()->accept(*this); + stream << ")"; break; case BinaryRelationExpression::RelationType::LessOrEqual: + stream << "("; expression.getFirstOperand()->accept(*this); stream << "<="; expression.getSecondOperand()->accept(*this); + stream << ")"; break; case BinaryRelationExpression::RelationType::Greater: + stream << "("; expression.getFirstOperand()->accept(*this); stream << ">"; expression.getSecondOperand()->accept(*this); + stream << ")"; break; case BinaryRelationExpression::RelationType::GreaterOrEqual: + stream << "("; expression.getFirstOperand()->accept(*this); stream << ">="; expression.getSecondOperand()->accept(*this); + stream << ")"; break; } return boost::any(); diff --git a/src/storage/prism/Assignment.cpp b/src/storage/prism/Assignment.cpp index c4973e231..3628c76ef 100644 --- a/src/storage/prism/Assignment.cpp +++ b/src/storage/prism/Assignment.cpp @@ -19,7 +19,7 @@ namespace storm { } Assignment Assignment::substitute(std::map const& substitution) const { - return Assignment(this->getVariable(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return Assignment(this->getVariable(), this->getExpression().substitute(substitution).simplify(), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) { diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp index abd5f1dd1..c00a9fbd2 100644 --- a/src/storage/prism/Update.cpp +++ b/src/storage/prism/Update.cpp @@ -48,6 +48,7 @@ namespace storm { newAssignments.emplace_back(assignment.substitute(substitution)); } + // FIXME: The expression could be simplified, but 1/K (where K is an int) is then resolved to 0, which is incorrect (for probabilities). return Update(this->getGlobalIndex(), this->getLikelihoodExpression().substitute(substitution), newAssignments, this->getFilename(), this->getLineNumber()); }