From 1a07b24682829864333bb72b959ee6f4eeb1adb3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 20 Aug 2015 16:41:25 +0200 Subject: [PATCH] added some convenience functions for reward model building Former-commit-id: 796963aee388dccaf7e508dc10c208ca9d52c3ec --- src/builder/DdPrismModelBuilder.cpp | 32 ++- src/builder/DdPrismModelBuilder.h | 10 + src/builder/ExplicitPrismModelBuilder.cpp | 81 ++++-- src/builder/ExplicitPrismModelBuilder.h | 10 + .../prctl/helper/SparseDtmcPrctlHelper.cpp | 2 +- .../prctl/helper/SparseDtmcPrctlHelper.h | 2 +- src/models/sparse/Model.cpp | 21 +- src/models/symbolic/Model.cpp | 16 +- src/parser/PrismParser.cpp | 27 +- ...ministicModelBisimulationDecomposition.cpp | 42 ++- ...erministicModelBisimulationDecomposition.h | 23 +- src/utility/cli.cpp | 72 +---- src/utility/cli.h | 246 +++++++++--------- src/utility/vector.h | 8 +- 14 files changed, 360 insertions(+), 232 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index cae09f43c..4b562a467 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -174,18 +174,28 @@ namespace storm { } }; - - template - DdPrismModelBuilder::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions() { + DdPrismModelBuilder::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels() { // Intentionally left empty. } template - DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), labelsToBuild(std::set()), expressionLabels(std::vector()) { + DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()) { this->preserveFormula(formula); } + template + DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels() { + if (formulas.empty()) { + this->buildAllRewardModels = true; + this->buildAllLabels = true; + } else { + for (auto const& formula : formulas) { + this->preserveFormula(*formula); + } + } + } + template void DdPrismModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { // If we are not required to build all reward models, we determine the reward models we need to build. @@ -844,6 +854,8 @@ namespace storm { preparedProgram = preparedProgram.substituteConstants(); + STORM_LOG_DEBUG("Building representation of program :" << std::endl << preparedProgram << std::endl); + // Start by initializing the structure used for storing all information needed during the model generation. // In particular, this creates the meta variables used to encode the model. GenerationInformation generationInfo(preparedProgram); @@ -857,12 +869,22 @@ namespace storm { // the reward computation might divide by the transition probabilities, which must therefore never be 0. // However, cutting it to the reachable fragment, there might be zero probability transitions. std::vector> selectedRewardModels; + + // First, we make sure that all selected reward models actually exist. + for (auto const& rewardModelName : options.rewardModelsToBuild) { + STORM_LOG_THROW(rewardModelName.empty() || preparedProgram.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'."); + } + for (auto const& rewardModel : preparedProgram.getRewardModels()) { if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) { selectedRewardModels.push_back(rewardModel); } } - + // If no reward model was selected until now and a referenced reward model appears to be unique, we build + // the only existing reward model (given that no explicit name was given for the referenced reward model). + if (selectedRewardModels.empty() && preparedProgram.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") { + selectedRewardModels.push_back(preparedProgram.getRewardModel(0)); + } std::unordered_map> rewardModels; if (options.buildAllRewardModels || !options.rewardModelsToBuild.empty()) { for (auto const& rewardModel : preparedProgram.getRewardModels()) { diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index c4cfe51c7..0c307983d 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -46,6 +46,13 @@ namespace storm { */ Options(storm::logic::Formula const& formula); + /*! Creates an object representing the suggested building options assuming that the given formulas are + * the only ones to check. Additional formulas may be preserved by calling preserveFormula. + * + * @param formula Thes formula based on which to choose the building options. + */ + Options(std::vector> const& formulas); + /*! * Sets the constants definitions from the given string. The string must be of the form 'X=a,Y=b,Z=c', * etc. where X,Y,Z are the variable names and a,b,c are the values of the constants. @@ -73,6 +80,9 @@ namespace storm { // An optional mapping that, if given, contains defining expressions for undefined constants. boost::optional> constantDefinitions; + // A flag indicating whether all labels are to be build. + bool buildAllLabels; + // An optional set of labels that, if given, restricts the labels that are built. boost::optional> labelsToBuild; diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 406cfeef7..669cc3512 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -43,7 +43,7 @@ namespace storm { if (hasTransitionRewards) { optionalTransitionRewardMatrix = transitionRewardMatrixBuilder.build(rowCount, columnCount, rowGroupCount); } - + return storm::models::sparse::StandardRewardModel(std::move(optionalStateRewardVector), std::move(optionalStateActionRewardVector), std::move(optionalTransitionRewardMatrix)); } @@ -104,14 +104,26 @@ namespace storm { } template - ExplicitPrismModelBuilder::Options::Options() : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions() { + ExplicitPrismModelBuilder::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels() { // Intentionally left empty. } template - ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), labelsToBuild(std::set()), expressionLabels(std::vector()) { + ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()) { this->preserveFormula(formula); } + + template + ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels() { + if (formulas.empty()) { + this->buildAllRewardModels = true; + this->buildAllLabels = true; + } else { + for (auto const& formula : formulas) { + this->preserveFormula(*formula); + } + } + } template void ExplicitPrismModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { @@ -124,9 +136,15 @@ namespace storm { } // Extract all the labels used in the formula. - std::vector> atomicLabelFormulas = formula.getAtomicLabelFormulas(); - for (auto const& formula : atomicLabelFormulas) { - labelsToBuild.get().insert(formula.get()->getLabel()); + if (!buildAllLabels) { + if (!labelsToBuild) { + labelsToBuild = std::set(); + } + + std::vector> atomicLabelFormulas = formula.getAtomicLabelFormulas(); + for (auto const& formula : atomicLabelFormulas) { + labelsToBuild.get().insert(formula.get()->getLabel()); + } } // Extract all the expressions used in the formula. @@ -191,7 +209,9 @@ namespace storm { // If the set of labels we are supposed to built is restricted, we need to remove the other labels from the program. if (options.labelsToBuild) { - preparedProgram.filterLabels(options.labelsToBuild.get()); + if (!options.buildAllLabels) { + preparedProgram.filterLabels(options.labelsToBuild.get()); + } } // If we need to build labels for expressions that may appear in some formula, we need to add appropriate @@ -210,15 +230,26 @@ namespace storm { // Now that the program is fixed, we we need to substitute all constants with their concrete value. preparedProgram = preparedProgram.substituteConstants(); - std::cout << preparedProgram << std::endl; + STORM_LOG_DEBUG("Building representation of program :" << std::endl << preparedProgram << std::endl); // Select the appropriate reward models (after the constants have been substituted). std::vector> selectedRewardModels; + + // First, we make sure that all selected reward models actually exist. + for (auto const& rewardModelName : options.rewardModelsToBuild) { + STORM_LOG_THROW(rewardModelName.empty() || preparedProgram.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'."); + } + for (auto const& rewardModel : preparedProgram.getRewardModels()) { if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) { selectedRewardModels.push_back(rewardModel); } } + // If no reward model was selected until now and a referenced reward model appears to be unique, we build + // the only existing reward model (given that no explicit name was given for the referenced reward model). + if (selectedRewardModels.empty() && preparedProgram.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") { + selectedRewardModels.push_back(preparedProgram.getRewardModel(0)); + } ModelComponents modelComponents = buildModelComponents(preparedProgram, selectedRewardModels, options); @@ -554,6 +585,18 @@ namespace storm { } transitionMatrixBuilder.addNextValue(currentRow, stateIndex, storm::utility::one()); + + auto builderIt = rewardModelBuilders.begin(); + for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { + if (rewardModelIt->get().hasStateRewards()) { + builderIt->stateRewardVector.push_back(storm::utility::zero()); + } + + if (rewardModelIt->get().hasStateActionRewards()) { + builderIt->stateActionRewardVector.push_back(storm::utility::zero()); + } + } + ++currentRow; } else { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); @@ -616,20 +659,20 @@ namespace storm { auto builderIt = rewardModelBuilders.begin(); for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { if (rewardModelIt->get().hasStateRewards()) { - builderIt->stateRewardVector.resize(currentRow + 1); + builderIt->stateRewardVector.push_back(storm::utility::zero()); for (auto const& stateReward : rewardModelIt->get().getStateRewards()) { if (evaluator.asBool(stateReward.getStatePredicateExpression())) { - builderIt->stateRewardVector[currentRow] += ValueType(evaluator.asRational(stateReward.getRewardValueExpression())); + builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression())); } } } if (rewardModelIt->get().hasStateActionRewards()) { - builderIt->stateActionRewardVector.resize(currentRow + 1); + builderIt->stateActionRewardVector.push_back(storm::utility::zero()); for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) { if (!stateActionReward.isLabeled()) { if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) { - builderIt->stateActionRewardVector[currentRow] += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) / totalNumberOfChoices; + builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) / totalNumberOfChoices; } } } @@ -652,20 +695,18 @@ namespace storm { auto builderIt = rewardModelBuilders.begin(); for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { if (rewardModelIt->get().hasStateRewards()) { - builderIt->stateRewardVector.resize(currentRow + 1); for (auto const& stateReward : rewardModelIt->get().getStateRewards()) { if (evaluator.asBool(stateReward.getStatePredicateExpression())) { - builderIt->stateRewardVector[currentRow] += ValueType(evaluator.asRational(stateReward.getRewardValueExpression())); + builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression())); } } } if (rewardModelIt->get().hasStateActionRewards()) { - builderIt->stateActionRewardVector.resize(currentRow + 1); for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) { if (stateActionReward.isLabeled() && stateActionReward.getActionIndex() == choice.getActionIndex()) { if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) { - builderIt->stateActionRewardVector[currentRow] += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) / totalNumberOfChoices; + builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) / totalNumberOfChoices; } } } @@ -719,11 +760,11 @@ namespace storm { auto builderIt = rewardModelBuilders.begin(); for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { if (rewardModelIt->get().hasStateActionRewards()) { - builderIt->stateActionRewardVector.resize(currentRow + 1); + builderIt->stateActionRewardVector.push_back(storm::utility::zero()); for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) { if (!stateActionReward.isLabeled()) { if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) { - builderIt->stateActionRewardVector[currentRow] += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())); + builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())); } } } @@ -747,11 +788,11 @@ namespace storm { auto builderIt = rewardModelBuilders.begin(); for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { if (rewardModelIt->get().hasStateActionRewards()) { - builderIt->stateActionRewardVector.resize(currentRow + 1); + builderIt->stateActionRewardVector.push_back(storm::utility::zero()); for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) { if (stateActionReward.isLabeled() && stateActionReward.getActionIndex() == choice.getActionIndex()) { if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) { - builderIt->stateActionRewardVector[currentRow] += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())); + builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())); } } } diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index c9fbac4c6..b7ee7fa9c 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -132,6 +132,13 @@ namespace storm { * @param formula The formula based on which to choose the building options. */ Options(storm::logic::Formula const& formula); + + /*! Creates an object representing the suggested building options assuming that the given formulas are + * the only ones to check. Additional formulas may be preserved by calling preserveFormula. + * + * @param formula Thes formula based on which to choose the building options. + */ + Options(std::vector> const& formulas); /*! * Sets the constants definitions from the given string. The string must be of the form 'X=a,Y=b,Z=c', @@ -163,6 +170,9 @@ namespace storm { // An optional mapping that, if given, contains defining expressions for undefined constants. boost::optional> constantDefinitions; + // A flag that indicates whether all labels are to be build. + bool buildAllLabels; + // An optional set of labels that, if given, restricts the labels that are built. boost::optional> labelsToBuild; diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 1f9a9552f..461181343 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -159,7 +159,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function const&(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Determine which states have a reward of infinity by definition. storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index b01d0cec1..d698ae29f 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -34,7 +34,7 @@ namespace storm { static std::vector computeLongRunAverage(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); private: - static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function const&(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); }; } diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index f438f7420..6e56003ba 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -90,7 +90,17 @@ namespace storm { template RewardModelType const& Model::getRewardModel(std::string const& rewardModelName) const { auto it = this->rewardModels.find(rewardModelName); - STORM_LOG_THROW(it != this->rewardModels.end(), storm::exceptions::IllegalArgumentException, "The requested reward model '" << rewardModelName << "' does not exist."); + if (it == this->rewardModels.end()) { + if (rewardModelName.empty()) { + if (this->hasUniqueRewardModel()) { + return this->getUniqueRewardModel()->second; + } 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."); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "The requested reward model '" << rewardModelName << "' does not exist."); + } + } return it->second; } @@ -178,10 +188,13 @@ namespace storm { void Model::printRewardModelsInformationToStream(std::ostream& out) const { if (this->rewardModels.size()) { std::vector rewardModelNames; - std::for_each(this->rewardModels.cbegin(), this->rewardModels.cend(), [&rewardModelNames] (typename std::pair const& nameRewardModelPair) { rewardModelNames.push_back(nameRewardModelPair.first); }); - out << "Reward Models: " << boost::join(rewardModelNames, ", ") << std::endl; + std::for_each(this->rewardModels.cbegin(), this->rewardModels.cend(), + [&rewardModelNames] (typename std::pair const& nameRewardModelPair) { + if (nameRewardModelPair.first.empty()) { rewardModelNames.push_back("(default)"); } else { rewardModelNames.push_back(nameRewardModelPair.first); } + }); + out << "Reward Models: " << boost::join(rewardModelNames, ", ") << std::endl; } else { - out << "Reward Models: none" << std::endl; + out << "Reward Models: none" << std::endl; } } diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 48384395d..e469e110f 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -1,6 +1,6 @@ #include "src/models/symbolic/Model.h" -#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/IllegalArgumentException.h" #include "src/adapters/AddExpressionAdapter.h" @@ -60,7 +60,7 @@ namespace storm { template storm::dd::Bdd Model::getStates(std::string const& label) const { - STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::InvalidArgumentException, "The label " << label << " is invalid for the labeling of the model."); + STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::IllegalArgumentException, "The label " << label << " is invalid for the labeling of the model."); return rowExpressionAdapter->translateExpression(labelToExpressionMap.at(label)).toBdd() && this->reachableStates; } @@ -132,7 +132,17 @@ namespace storm { template typename Model::RewardModelType const& Model::getRewardModel(std::string const& rewardModelName) const { auto it = this->rewardModels.find(rewardModelName); - STORM_LOG_THROW(it != this->rewardModels.end(), storm::exceptions::InvalidArgumentException, "The requested reward model '" << rewardModelName << "' does not exist."); + if (it == this->rewardModels.end()) { + if (rewardModelName.empty()) { + if (this->hasUniqueRewardModel()) { + return this->getUniqueRewardModel()->second; + } 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."); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "The requested reward model '" << rewardModelName << "' does not exist."); + } + } return it->second; } diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 3bc58ab88..fa5170a9c 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -406,13 +406,11 @@ namespace storm { STORM_LOG_ASSERT(!this->secondRun, "Dummy procedure must not be called in second run."); std::string realActionName = actionName ? actionName.get() : ""; - if (!actionName) { - // Register the action name if it has not appeared earlier. - auto nameIndexPair = globalProgramInformation.actionIndices.find(realActionName); - if (nameIndexPair == globalProgramInformation.actionIndices.end()) { - std::size_t nextIndex = globalProgramInformation.actionIndices.size(); - globalProgramInformation.actionIndices.emplace(realActionName, nextIndex); - } + // Register the action name if it has not appeared earlier. + auto nameIndexPair = globalProgramInformation.actionIndices.find(realActionName); + if (nameIndexPair == globalProgramInformation.actionIndices.end()) { + std::size_t nextIndex = globalProgramInformation.actionIndices.size(); + globalProgramInformation.actionIndices.emplace(realActionName, nextIndex); } return storm::prism::Command(); @@ -476,6 +474,21 @@ namespace storm { this->identifiers_.add(renamingPair->second, renamedVariable.getExpression()); } + for (auto const& command : moduleToRename.getCommands()) { + std::string newActionName = command.getActionName(); + auto const& renamingPair = renaming.find(command.getActionName()); + if (renamingPair != renaming.end()) { + newActionName = renamingPair->second; + } + + // Record any newly occurring action names/indices. + auto nameIndexPair = globalProgramInformation.actionIndices.find(newActionName); + if (nameIndexPair == globalProgramInformation.actionIndices.end()) { + std::size_t nextIndex = globalProgramInformation.actionIndices.size(); + globalProgramInformation.actionIndices.emplace(newActionName, nextIndex); + } + } + // Return a dummy module in the first pass. return storm::prism::Module(); } else { diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 7d6e6b2a2..725d46b02 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -602,6 +602,43 @@ namespace storm { template DeterministicModelBisimulationDecomposition::Options::Options(storm::models::sparse::Model const& model, storm::logic::Formula const& formula) : Options() { + this->preserveSingleFormula(model, formula); + } + + template + DeterministicModelBisimulationDecomposition::Options::Options(storm::models::sparse::Model const& model, std::vector> const& formulas) : Options() { + if (formulas.size() == 1) { + this->preserveSingleFormula(model, *formulas.front()); + } else { + for (auto const& formula : formulas) { + std::vector> atomicExpressionFormulas = formula->getAtomicExpressionFormulas(); + std::vector> atomicLabelFormulas = formula->getAtomicLabelFormulas(); + + std::set labelsToRespect; + for (auto const& labelFormula : atomicLabelFormulas) { + labelsToRespect.insert(labelFormula->getLabel()); + } + for (auto const& expressionFormula : atomicExpressionFormulas) { + std::stringstream stream; + stream << *expressionFormula; + labelsToRespect.insert(stream.str()); + } + if (!respectedAtomicPropositions) { + respectedAtomicPropositions = labelsToRespect; + } else { + respectedAtomicPropositions.get().insert(labelsToRespect.begin(), labelsToRespect.end()); + } + } + } + } + + template + DeterministicModelBisimulationDecomposition::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) { + // Intentionally left empty. + } + + template + void DeterministicModelBisimulationDecomposition::Options::preserveSingleFormula(storm::models::sparse::Model const& model, storm::logic::Formula const& formula) { if (!formula.containsRewardOperator()) { this->keepRewards = false; } @@ -664,11 +701,6 @@ namespace storm { } } - template - DeterministicModelBisimulationDecomposition::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) { - // Intentionally left empty. - } - template DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::sparse::Dtmc const& model, Options const& options) { STORM_LOG_THROW(!model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model."); diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index e824a76ed..56cbbd590 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -29,14 +29,24 @@ namespace storm { Options(); /*! - * Creates an object representing the options necessary to obtain the smallest quotient while still - * preserving the given formula. + * Creates an object representing the options necessary to obtain the quotient while still preserving + * the given formula. * * @param The model for which the quotient model shall be computed. This needs to be given in order to * derive a suitable initial partition. * @param formula The formula that is to be preserved. */ Options(storm::models::sparse::Model const& model, storm::logic::Formula const& formula); + + /*! + * Creates an object representing the options necessary to obtain the smallest quotient while still + * preserving the given formula. + * + * @param The model for which the quotient model shall be computed. This needs to be given in order to + * derive a suitable initial partition. + * @param formulas The formula that is to be preserved. + */ + Options(storm::models::sparse::Model const& model, std::vector> const& formulas); // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the @@ -62,6 +72,15 @@ namespace storm { // A flag that governs whether the quotient model is actually built or only the decomposition is computed. bool buildQuotient; + + private: + /*! + * Sets the options under the assumption that the given formula is the only one that is to be checked. + * + * @param model The model for which to preserve the formula. + * @param formula The only formula to check. + */ + void preserveSingleFormula(storm::models::sparse::Model const& model, storm::logic::Formula const& formula); }; /*! diff --git a/src/utility/cli.cpp b/src/utility/cli.cpp index f35075a58..b3867c299 100644 --- a/src/utility/cli.cpp +++ b/src/utility/cli.cpp @@ -218,9 +218,9 @@ namespace storm { } // Then proceed to parsing the property (if given), since the model we are building may depend on the property. - std::vector>> formulas; + std::vector> formulas; if (settings.isPropertySet()) { - boost::optional> formula; + std::shared_ptr formula; if (program) { storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); formula = formulaParser.parseFromString(settings.getProperty()); @@ -229,68 +229,24 @@ namespace storm { formula = formulaParser.parseFromString(settings.getProperty()); } formulas.push_back(formula); + } else if (settings.isPropertyFileSet()) { + // FIXME: asap. } - else if (settings.isPropertyFileSet()) { - std::cout << "Reading properties from " << settings.getPropertiesFilename() << std::endl; - std::ifstream inputFileStream(settings.getPropertiesFilename(), std::ios::in); - - std::vector properties; - - if (inputFileStream.good()) { - try { - while (inputFileStream.good()) { - std::string prop; - std::getline(inputFileStream, prop); - if (!prop.empty()) { - properties.push_back(prop); - } - } - } - catch (std::exception& e) { - inputFileStream.close(); - throw e; - } - inputFileStream.close(); - } else { - STORM_LOG_ERROR("Unable to read property file."); - } - - for (std::string prop : properties) { - boost::optional> formula; - try { - if (program) { - storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); - formula = formulaParser.parseFromString(prop); - } else { - storm::parser::FormulaParser formulaParser; - formula = formulaParser.parseFromString(prop); - } - formulas.push_back(formula); - } - catch (storm::exceptions::WrongFormatException &e) { - STORM_LOG_WARN("Unable to parse line as formula: " << prop); - } - } - std::cout << "Parsed " << formulas.size() << " properties from file " << settings.getPropertiesFilename() << std::endl; - } - - for (boost::optional> formula : formulas) { - if (settings.isSymbolicSet()) { + if (settings.isSymbolicSet()) { #ifdef STORM_HAVE_CARL - if (settings.isParametricSet()) { - buildAndCheckSymbolicModel(program.get(), formula); - } else { + if (settings.isParametricSet()) { + buildAndCheckSymbolicModel(program.get(), formulas); + } else { #endif - buildAndCheckSymbolicModel(program.get(), formula); + buildAndCheckSymbolicModel(program.get(), formulas); #ifdef STORM_HAVE_CARL - } + } #endif - } else if (settings.isExplicitSet()) { - buildAndCheckExplicitModel(formula); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); - } + } else if (settings.isExplicitSet()) { + buildAndCheckExplicitModel(formulas); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } } diff --git a/src/utility/cli.h b/src/utility/cli.h index d8e8ed04f..a47b12a50 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -93,7 +93,7 @@ namespace storm { } template - std::shared_ptr buildSymbolicModel(storm::prism::Program const& program, boost::optional> const& formula) { + std::shared_ptr buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { std::shared_ptr result(nullptr); storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings(); @@ -104,9 +104,7 @@ namespace storm { // Customize and perform model-building. if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Sparse) { typename storm::builder::ExplicitPrismModelBuilder::Options options; - if (formula) { - options = typename storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); - } + options = typename storm::builder::ExplicitPrismModelBuilder::Options(formulas); options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); // Generate command labels if we are going to build a counterexample later. @@ -117,9 +115,7 @@ namespace storm { result = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { typename storm::builder::DdPrismModelBuilder::Options options; - if (formula) { - options = typename storm::builder::DdPrismModelBuilder::Options(*formula.get()); - } + options = typename storm::builder::DdPrismModelBuilder::Options(formulas); options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); result = storm::builder::DdPrismModelBuilder::translateProgram(program, options); @@ -130,7 +126,7 @@ namespace storm { } template - std::shared_ptr preprocessModel(std::shared_ptr model, boost::optional> const& formula) { + std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { if (storm::settings::generalSettings().isBisimulationSet()) { STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models."); std::shared_ptr> sparseModel = model->template as>(); @@ -141,8 +137,8 @@ namespace storm { std::cout << "Performing bisimulation minimization... "; typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; - if (formula) { - options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*sparseModel, *formula.get()); + if (!formulas.empty()) { + options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*sparseModel, formulas); } if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { options.weak = true; @@ -157,7 +153,7 @@ namespace storm { } template - void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr formula) { + void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) { STORM_LOG_THROW(model->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs."); STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models."); @@ -180,63 +176,64 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr formula) { + inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); } #endif template - void verifySparseModel(boost::optional const& program, std::shared_ptr> model, std::shared_ptr formula) { + void verifySparseModel(boost::optional const& program, std::shared_ptr> model, std::vector> const& formulas) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); - // If we were requested to generate a counterexample, we now do so. - if (settings.isCounterexampleSet()) { - STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model."); - generateCounterexample(program.get(), model, formula); - } else { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(*formula.get())) { - result = modelchecker.check(*formula.get()); - } else { - storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker2(*dtmc); - if (modelchecker2.canHandle(*formula.get())) { - result = modelchecker2.check(*formula.get()); + for (auto const& formula : formulas) { + // If we were requested to generate a counterexample, we now do so. + if (settings.isCounterexampleSet()) { + STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model."); + generateCounterexample(program.get(), model, formula); + } else { + std::cout << std::endl << "Model checking property: " << *formula << " ..."; + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } else { + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker2(*dtmc); + if (modelchecker2.canHandle(*formula)) { + result = modelchecker2.check(*formula); + } } - } - } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); + } else if (model->getType() == storm::models::ModelType::Mdp) { + std::shared_ptr> mdp = model->template as>(); #ifdef STORM_HAVE_CUDA - if (settings.isCudaSet()) { - storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker modelchecker(*mdp); - result = modelchecker.check(*formula.get()); - } else { - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); - result = modelchecker.check(*formula.get()); - } + if (settings.isCudaSet()) { + storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker modelchecker(*mdp); + result = modelchecker.check(*formula); + } else { + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); + result = modelchecker.check(*formula); + } #else - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); - result = modelchecker.check(*formula.get()); + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); + result = modelchecker.check(*formula); #endif - } else if (model->getType() == storm::models::ModelType::Ctmc) { - std::shared_ptr> ctmc = model->template as>(); - - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc); - result = modelchecker.check(*formula.get()); - } - - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + } else if (model->getType() == storm::models::ModelType::Ctmc) { + std::shared_ptr> ctmc = model->template as>(); + + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc); + result = modelchecker.check(*formula); + } + + if (result) { + std::cout << " done." << std::endl; + std::cout << "Result (initial states): "; + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + std::cout << *result << std::endl; + } else { + std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + } } - } } @@ -258,95 +255,98 @@ namespace storm { } template<> - inline void verifySparseModel(boost::optional const& program, std::shared_ptr> model, std::shared_ptr formula) { + inline void verifySparseModel(boost::optional const& program, std::shared_ptr> model, std::vector> const& formulas) { - STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs."); - std::shared_ptr> dtmc = model->template as>(); - - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; - - storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(*formula.get())) { - result = modelchecker.check(*formula.get()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property."); - } - - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(dtmc->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; - } - - storm::settings::modules::ParametricSettings const& parametricSettings = storm::settings::parametricSettings(); - if (parametricSettings.exportResultToFile()) { - exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); + for (auto const& formula : formulas) { + STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs."); + std::shared_ptr> dtmc = model->template as>(); + + std::cout << std::endl << "Model checking property: " << *formula << " ..."; + std::unique_ptr result; + + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property."); + } + + if (result) { + std::cout << " done." << std::endl; + std::cout << "Result (initial states): "; + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(dtmc->getInitialStates())); + std::cout << *result << std::endl; + } else { + std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + } + + storm::settings::modules::ParametricSettings const& parametricSettings = storm::settings::parametricSettings(); + if (parametricSettings.exportResultToFile()) { + exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); + } } } #endif template - void verifySymbolicModel(boost::optional const& program, std::shared_ptr> model, std::shared_ptr formula) { - - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker modelchecker(*dtmc); - if (modelchecker.canHandle(*formula.get())) { - result = modelchecker.check(*formula.get()); - } - } else if (model->getType() == storm::models::ModelType::Ctmc) { - std::shared_ptr> ctmc = model->template as>(); - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc); - if (modelchecker.canHandle(*formula.get())) { - result = modelchecker.check(*formula.get()); + void verifySymbolicModel(boost::optional const& program, std::shared_ptr> model, std::vector> const& formulas) { + for (auto const& formula : formulas) { + std::cout << std::endl << "Model checking property: " << *formula << " ..."; + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::HybridDtmcPrctlModelChecker modelchecker(*dtmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } + } else if (model->getType() == storm::models::ModelType::Ctmc) { + std::shared_ptr> ctmc = model->template as>(); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } + } else if (model->getType() == storm::models::ModelType::Mdp) { + std::shared_ptr> mdp = model->template as>(); + storm::modelchecker::HybridMdpPrctlModelChecker modelchecker(*mdp); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); } - } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::HybridMdpPrctlModelChecker modelchecker(*mdp); - if (modelchecker.canHandle(*formula.get())) { - result = modelchecker.check(*formula.get()); + + if (result) { + std::cout << " done." << std::endl; + std::cout << "Result (initial states): "; + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + std::cout << *result << std::endl; + } else { + std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } - } else { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); - } - - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } } template - void buildAndCheckSymbolicModel(boost::optional const& program, boost::optional> formula) { + void buildAndCheckSymbolicModel(boost::optional const& program, std::vector> const& formulas) { // Now we are ready to actually build the model. STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed."); - std::shared_ptr model = buildSymbolicModel(program.get(), formula); + std::shared_ptr model = buildSymbolicModel(program.get(), formulas); STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); // Preprocess the model if needed. - model = preprocessModel(model, formula); + model = preprocessModel(model, formulas); // Print some information about the model. model->printModelInformationToStream(std::cout); // Verify the model, if a formula was given. - if (formula) { + if (!formulas.empty()) { if (model->isSparseModel()) { - verifySparseModel(program, model->as>(), formula.get()); + verifySparseModel(program, model->as>(), formulas); } else if (model->isSymbolicModel()) { if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { - verifySymbolicModel(program, model->as>(), formula.get()); + verifySymbolicModel(program, model->as>(), formulas); } else { // Not handled yet. STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); @@ -358,22 +358,22 @@ namespace storm { } template - void buildAndCheckExplicitModel(boost::optional> formula) { + void buildAndCheckExplicitModel(std::vector> const& formulas) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional()); // Preprocess the model if needed. - model = preprocessModel(model, formula); + model = preprocessModel(model, formulas); // Print some information about the model. model->printModelInformationToStream(std::cout); // Verify the model, if a formula was given. - if (formula) { + if (!formulas.empty()) { STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); - verifySparseModel(boost::optional(), model->as>(), formula.get()); + verifySparseModel(boost::optional(), model->as>(), formulas); } } diff --git a/src/utility/vector.h b/src/utility/vector.h index 51816ffb5..be9cc8f4c 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -136,7 +136,8 @@ namespace storm { auto it = source.cbegin() + rowGroupIndices[group]; auto ite = source.cbegin() + rowGroupIndices[group + 1]; while (it != ite) { - target[currentPosition] = *it; + target[currentPosition] += *it; + ++currentPosition; ++it; } } @@ -162,7 +163,7 @@ namespace storm { ++rowGroupIt; uint_fast64_t next = *rowGroupIt; while (current < next) { - *targetIt = *sourceIt; + *targetIt += *sourceIt; ++targetIt; } } @@ -183,8 +184,9 @@ namespace storm { uint_fast64_t current = rowGroupIndices[group]; uint_fast64_t next = rowGroupIndices[group + 1]; while (current < next) { - target[currentPosition] = source[group]; + target[currentPosition] += source[group]; ++currentPosition; + ++current; } } }