From c2abd9968f7471284cd7a243f6bfbee8083ec5ff Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 15 Oct 2014 13:39:46 +0200 Subject: [PATCH] Introduced constants comparator in explicit model adapter. Former-commit-id: 88015244ed82b58e8ab2762b91c6d7e018cbe0f7 --- src/adapters/ExplicitModelAdapter.h | 21 ++++++++++----------- src/utility/ConstantsComparator.h | 12 ++++++------ 2 files changed, 16 insertions(+), 17 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 95d39eb6d..89dce2caf 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -29,6 +29,7 @@ #include "src/storage/SparseMatrix.h" #include "src/settings/SettingsManager.h" #include "src/utility/macros.h" +#include "src/utility/ConstantsComparator.h" #include "src/exceptions/WrongFormatException.h" #include "src/storage/expressions/ExpressionEvaluation.h" @@ -269,7 +270,7 @@ namespace storm { return result; } - static std::list> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue, expressions::ExpressionEvaluation& eval) { + static std::list> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator, expressions::ExpressionEvaluation& eval) { std::list> result; StateType const* currentState = stateInformation.reachableStates[stateIndex]; @@ -316,14 +317,14 @@ namespace storm { } // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(storm::utility::isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (sum = " << probabilitySum << ")."); + STORM_LOG_THROW(!comparator.isConstant(probabilitySum) || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (sum = " << probabilitySum << ")."); } } return result; } - static std::list> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue, expressions::ExpressionEvaluation& eval) { + static std::list> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator, expressions::ExpressionEvaluation& eval) { std::list> result; for (std::string const& action : program.getActions()) { @@ -422,10 +423,7 @@ namespace storm { } // Check that the resulting distribution is in fact a distribution. - if (!storm::utility::isOne(probabilitySum)) { - LOG4CPLUS_ERROR(logger, "Sum of update probabilities (" << probabilitySum << ") is not one for some command."); - throw storm::exceptions::WrongFormatException() << "Sum of update probabilities do sum to " << probabilitySum << " to one for some command."; - } + STORM_LOG_THROW(!comparator.isConstant(probabilitySum) || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do sum to " << probabilitySum << " to one for some command."); // Dispose of the temporary maps. delete currentTargetStates; @@ -467,7 +465,7 @@ namespace storm { * @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin * and a vector containing the labels associated with each choice. */ - static std::vector> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder& transitionRewardMatrixBuilder, expressions::ExpressionEvaluation& eval) { + static std::vector> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder& transitionRewardMatrixBuilder, storm::utility::ConstantsComparator const& comparator, expressions::ExpressionEvaluation& eval) { std::vector> choiceLabels; // Initialize a queue and insert the initial state. @@ -498,8 +496,8 @@ namespace storm { uint_fast64_t currentState = stateQueue.front(); // Retrieve all choices for the current state. - std::list> allUnlabeledChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue, eval); - std::list> allLabeledChoices = getLabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue, eval); + std::list> allUnlabeledChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue, comparator, eval); + std::list> allLabeledChoices = getLabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue, comparator, eval); uint_fast64_t totalNumberOfChoices = allUnlabeledChoices.size() + allLabeledChoices.size(); @@ -669,7 +667,8 @@ namespace storm { // Build the transition and reward matrices. storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); - modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder, eval); + storm::utility::ConstantsComparator comparator; + modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder, comparator, eval); // Finalize the resulting matrices. modelComponents.transitionMatrix = transitionMatrixBuilder.build(); diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h index d3d4fba38..d97c4ef93 100644 --- a/src/utility/ConstantsComparator.h +++ b/src/utility/ConstantsComparator.h @@ -86,15 +86,15 @@ namespace storm { template<> class ConstantsComparator { public: - bool isOne(storm::RationalFunction const& value) { + bool isOne(storm::RationalFunction const& value) const { return value.isOne(); } - bool isZero(storm::RationalFunction const& value) { + bool isZero(storm::RationalFunction const& value) const { return value.isZero(); } - bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) { + bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const { return value1 == value2; } @@ -106,15 +106,15 @@ namespace storm { template<> class ConstantsComparator { public: - bool isOne(storm::Polynomial const& value) { + bool isOne(storm::Polynomial const& value) const { return value.isOne(); } - bool isZero(storm::Polynomial const& value) { + bool isZero(storm::Polynomial const& value) const { return value.isZero(); } - bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) { + bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const { return value1 == value2; }