From 29f0f66689c6fd5fccf4dadd3ddeb6a9d3168967 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 23 Sep 2016 18:45:31 +0200 Subject: [PATCH] reworked getUniqueRewardModel a little Former-commit-id: b0a3677c1aacbb4ff36673ebcbf5fa68a0ab8e72 [formerly a2124b3363044f49ba48e08e3b8b35fc1e83f153] Former-commit-id: c76a56a1684241f740ae34768f7478b2b752b7cb --- src/modelchecker/region/ApproximationModel.cpp | 10 +++++----- src/modelchecker/region/SamplingModel.cpp | 4 ++-- .../region/SparseDtmcRegionModelChecker.cpp | 4 ++-- src/models/sparse/Model.cpp | 10 +++++----- src/models/sparse/Model.h | 8 ++++---- src/models/symbolic/Model.cpp | 14 ++++++++++---- src/models/symbolic/Model.h | 11 +++++++++-- src/parser/ExpressionParser.cpp | 2 -- .../bisimulation/BisimulationDecomposition.cpp | 4 ++-- ...DeterministicModelBisimulationDecomposition.cpp | 6 +++--- ...deterministicModelBisimulationDecomposition.cpp | 8 ++++---- 11 files changed, 46 insertions(+), 35 deletions(-) diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index 2c5ab2e3c..1c9b9d5c2 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -33,7 +33,7 @@ namespace storm { this->computeRewards=true; STORM_LOG_THROW(this->typeOfParametricModel==storm::models::ModelType::Dtmc, storm::exceptions::InvalidArgumentException, "Approximation with rewards is only implemented for Dtmcs"); STORM_LOG_THROW(parametricModel.hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the approximation model should be unique"); - STORM_LOG_THROW(parametricModel.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the approximation model should have state rewards only"); + STORM_LOG_THROW(parametricModel.getUniqueRewardModel().hasOnlyStateRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the approximation model should have state rewards only"); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid formula: " << formula << ". Approximation model only supports eventually or reachability reward formulae."); } @@ -211,8 +211,8 @@ namespace storm { ConstantType dummyNonZeroValue = storm::utility::one(); auto vectorIt = this->vectorData.vector.begin(); for(auto oldState : this->maybeStates){ - if(storm::utility::isConstant(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[oldState])){ - ConstantType reward = storm::utility::region::convertNumber(storm::utility::region::getConstantPart(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[oldState])); + if(storm::utility::isConstant(parametricModel.getUniqueRewardModel().getStateRewardVector()[oldState])){ + ConstantType reward = storm::utility::region::convertNumber(storm::utility::region::getConstantPart(parametricModel.getUniqueRewardModel().getStateRewardVector()[oldState])); //Add one of these entries for every row in the row group of oldState for(auto matrixRow=this->matrixData.matrix.getRowGroupIndices()[oldState]; matrixRowmatrixData.matrix.getRowGroupIndices()[oldState+1]; ++matrixRow){ *vectorIt = reward; @@ -220,7 +220,7 @@ namespace storm { } } else { std::set occurringRewVariables; - storm::utility::region::gatherOccurringVariables(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[oldState], occurringRewVariables); + storm::utility::region::gatherOccurringVariables(parametricModel.getUniqueRewardModel().getStateRewardVector()[oldState], occurringRewVariables); // For each row in the row group of oldState, we get the corresponding substitution and insert the FunctionSubstitution for(auto matrixRow=this->matrixData.matrix.getRowGroupIndices()[oldState]; matrixRowmatrixData.matrix.getRowGroupIndices()[oldState+1]; ++matrixRow){ //Extend the substitution for the probabilities with the reward parameters @@ -230,7 +230,7 @@ namespace storm { substitution.insert(typename std::map::value_type(rewardVar, RegionBoundary::UNSPECIFIED)); } // insert the FunctionSubstitution - auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[oldState], this->matrixData.rowSubstitutions[matrixRow]), dummyNonZeroValue)).first; + auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(parametricModel.getUniqueRewardModel().getStateRewardVector()[oldState], this->matrixData.rowSubstitutions[matrixRow]), dummyNonZeroValue)).first; //insert assignment and dummy data this->vectorData.assignment.emplace_back(vectorIt, functionsIt->second); *vectorIt = dummyNonZeroValue; diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index 81c7aa61f..2a3d960dc 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -43,7 +43,7 @@ namespace storm { this->computeRewards=true; STORM_LOG_THROW(this->typeOfParametricModel==storm::models::ModelType::Dtmc, storm::exceptions::InvalidArgumentException, "Sampling with rewards is only implemented for Dtmcs"); STORM_LOG_THROW(parametricModel.hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sampling model should be unique"); - STORM_LOG_THROW(parametricModel.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sampling model should have state rewards only"); + STORM_LOG_THROW(parametricModel.getUniqueRewardModel().hasOnlyStateRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sampling model should have state rewards only"); STORM_LOG_THROW(formula->getSubformula().isEventuallyFormula(), storm::exceptions::InvalidArgumentException, "The subformula should be a reachabilityreward formula"); STORM_LOG_THROW(formula->getSubformula().asEventuallyFormula().getSubformula().isInFragment(storm::logic::propositional()), storm::exceptions::InvalidArgumentException, "The subsubformula should be a propositional formula"); } else { @@ -131,7 +131,7 @@ namespace storm { std::vector b; if(this->computeRewards){ b.resize(submatrix.getRowCount()); - storm::utility::vector::selectVectorValues(b, this->maybeStates, instantiatedModel.getUniqueRewardModel()->second.getStateRewardVector()); + storm::utility::vector::selectVectorValues(b, this->maybeStates, instantiatedModel.getUniqueRewardModel().getStateRewardVector()); } else { b = instantiatedModel.getTransitionMatrix().getConstrainedRowSumVector(this->maybeStates, this->targetStates); } diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index 099eeb62f..3c091ab9f 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -317,7 +317,7 @@ namespace storm { } else { STORM_LOG_THROW(this->getModel()->hasRewardModel(), storm::exceptions::InvalidArgumentException, "No reward model specified"); STORM_LOG_THROW(this->getModel()->hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "Ambiguous reward model. Specify it in the formula!"); - rewardModel=&(this->getModel()->getUniqueRewardModel()->second); + rewardModel=&(this->getModel()->getUniqueRewardModel()); } //Get target states storm::modelchecker::SparsePropositionalModelChecker modelChecker(*(this->getModel())); @@ -416,7 +416,7 @@ namespace storm { storm::storage::BitVector phiStates(simpleModel.getNumberOfStates(), true); std::vector values; if(this->isComputeRewards()){ - values = simpleModel.getUniqueRewardModel()->second.getTotalRewardVector(maybeStates.getNumberOfSetBits(), simpleModel.getTransitionMatrix(), maybeStates); + values = simpleModel.getUniqueRewardModel().getTotalRewardVector(maybeStates.getNumberOfSetBits(), simpleModel.getTransitionMatrix(), maybeStates); } else { values = oneStepProbabilities; } diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index 5e4b5d54b..14f9fa8a3 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -101,7 +101,7 @@ namespace storm { if (it == this->rewardModels.end()) { if (rewardModelName.empty()) { if (this->hasUniqueRewardModel()) { - return this->getUniqueRewardModel()->second; + return this->getUniqueRewardModel(); } else { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unable to refer to default reward model, because there is no default model or it is not unique."); } @@ -142,15 +142,15 @@ namespace storm { } template - typename std::unordered_map::const_iterator Model::getUniqueRewardModel() const { + RewardModelType const& Model::getUniqueRewardModel() const { STORM_LOG_THROW(this->getNumberOfRewardModels() == 1, storm::exceptions::IllegalFunctionCallException, "The reward model is not unique."); - return this->rewardModels.cbegin(); + return this->rewardModels.cbegin()->second; } template - typename std::unordered_map::iterator Model::getUniqueRewardModel() { + RewardModelType& Model::getUniqueRewardModel() { STORM_LOG_THROW(this->getNumberOfRewardModels() == 1, storm::exceptions::IllegalFunctionCallException, "The reward model is not unique."); - return this->rewardModels.begin(); + return this->rewardModels.begin()->second; } template diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index 99288fd4a..8087df6a9 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -180,16 +180,16 @@ namespace storm { /*! * Retrieves the unique reward model, if there exists exactly one. Otherwise, an exception is thrown. * - * @return An iterator to the name and the reward model. + * @return The requested reward model. */ - typename std::unordered_map::const_iterator getUniqueRewardModel() const; + RewardModelType const& getUniqueRewardModel() const; /*! * Retrieves the unique reward model, if there exists exactly one. Otherwise, an exception is thrown. * - * @return An iterator to the name and the reward model. + * @return The requested reward model. */ - typename std::unordered_map::iterator getUniqueRewardModel(); + RewardModelType& getUniqueRewardModel(); /*! * Retrieves whether the model has a unique reward model. diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 16339c0d1..cfca623dc 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -156,7 +156,7 @@ namespace storm { if (it == this->rewardModels.end()) { if (rewardModelName.empty()) { if (this->hasUniqueRewardModel()) { - return this->getUniqueRewardModel()->second; + return this->getUniqueRewardModel(); } else { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unable to refer to default reward model, because there is no default model or it is not unique."); } @@ -168,11 +168,17 @@ namespace storm { } template - typename std::unordered_map::RewardModelType>::const_iterator Model::getUniqueRewardModel() const { + typename Model::RewardModelType const& Model::getUniqueRewardModel() const { STORM_LOG_THROW(this->hasUniqueRewardModel(), storm::exceptions::InvalidOperationException, "Cannot retrieve unique reward model, because there is no unique one."); - return this->rewardModels.begin(); + return this->rewardModels.cbegin()->second; } - + + template + typename Model::RewardModelType& Model::getUniqueRewardModel() { + STORM_LOG_THROW(this->hasUniqueRewardModel(), storm::exceptions::InvalidOperationException, "Cannot retrieve unique reward model, because there is no unique one."); + return this->rewardModels.begin()->second; + } + template bool Model::hasUniqueRewardModel() const { return this->rewardModels.size() == 1; diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h index b2e9d3e87..e9ebf8ddf 100644 --- a/src/models/symbolic/Model.h +++ b/src/models/symbolic/Model.h @@ -207,9 +207,16 @@ namespace storm { /*! * Retrieves the unique reward model, if there exists exactly one. Otherwise, an exception is thrown. * - * @return An iterator to the name and the reward model. + * @return The requested reward model. */ - typename std::unordered_map::const_iterator getUniqueRewardModel() const; + RewardModelType const& getUniqueRewardModel() const; + + /*! + * Retrieves the unique reward model, if there exists exactly one. Otherwise, an exception is thrown. + * + * @return The requested reward model. + */ + RewardModelType& getUniqueRewardModel(); /*! * Retrieves whether the model has a unique reward model. diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index 64a0f9213..3054f2fe0 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -379,8 +379,6 @@ namespace storm { STORM_LOG_THROW(this->identifiers_ != nullptr, storm::exceptions::WrongFormatException, "Unable to substitute identifier expressions without given mapping."); storm::expressions::Expression const* expression = this->identifiers_->find(identifier); if (expression == nullptr) { - std::cout << "didn't find " << identifier << std::endl; - identifiers_->for_each([] (std::string const& name, storm::expressions::Expression const& expr) { std::cout << "name: " << name << ", " << expr << std::endl; }); pass = false; return manager->boolean(false); } diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index dbad8c633..cfd43923b 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -168,7 +168,7 @@ namespace storm { template BisimulationDecomposition::BisimulationDecomposition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Options const& options) : model(model), backwardTransitions(backwardTransitions), options(options), partition(), comparator(), quotient(nullptr) { STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model."); - STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls)."); + STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || model.getUniqueRewardModel().hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls)."); STORM_LOG_THROW(options.getType() != BisimulationType::Weak || !options.getBounded(), storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties."); // Fix the respected atomic propositions if they were not explicitly given. @@ -260,7 +260,7 @@ namespace storm { template void BisimulationDecomposition::splitInitialPartitionBasedOnStateRewards() { - std::vector const& stateRewardVector = model.getUniqueRewardModel()->second.getStateRewardVector(); + std::vector const& stateRewardVector = model.getUniqueRewardModel().getStateRewardVector(); partition.split([&stateRewardVector] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return stateRewardVector[a] < stateRewardVector[b]; }); } diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index 3f70fd379..0b0574737 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -627,8 +627,7 @@ namespace storm { // If the model has state rewards, we simply copy the state reward of the representative state, because // all states in a block are guaranteed to have the same state reward. if (this->options.getKeepRewards() && this->model.hasRewardModel()) { - typename std::unordered_map::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel(); - stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState]; + stateRewards.get()[blockIndex] = this->model.getUniqueRewardModel().getStateRewardVector()[representativeState]; } } @@ -641,7 +640,8 @@ namespace storm { // Construct the reward model mapping. std::unordered_map rewardModels; if (this->options.getKeepRewards() && this->model.hasRewardModel()) { - typename std::unordered_map::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel(); + STORM_LOG_THROW(this->model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Cannot preserve more than one reward model."); + typename std::unordered_map::const_iterator nameRewardModelPair = this->model.getRewardModels().begin(); rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards))); } diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index 64a7efe45..547d4dc29 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -170,8 +170,7 @@ namespace storm { // If the model has state rewards, we simply copy the state reward of the representative state, because // all states in a block are guaranteed to have the same state reward. if (this->options.getKeepRewards() && this->model.hasRewardModel()) { - typename std::unordered_map::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel(); - stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState]; + stateRewards.get()[blockIndex] = this->model.getUniqueRewardModel().getStateRewardVector()[representativeState]; } } @@ -184,12 +183,13 @@ namespace storm { // Construct the reward model mapping. std::unordered_map rewardModels; if (this->options.getKeepRewards() && this->model.hasRewardModel()) { - typename std::unordered_map::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel(); + STORM_LOG_THROW(this->model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Cannot preserve more than one reward model."); + typename std::unordered_map::const_iterator nameRewardModelPair = this->model.getRewardModels().begin(); rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards))); } // Finally construct the quotient model. - this->quotient = std::shared_ptr(new ModelType(builder.build(), std::move(newLabeling), std::move(rewardModels))); + this->quotient = std::make_shared(builder.build(), std::move(newLabeling), std::move(rewardModels)); } template