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 <storm::dd::DdType Type>
- DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions() {
+ DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels() {
// Intentionally left empty.
}
template <storm::dd::DdType Type>
- DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()) {
+ DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()) {
this->preserveFormula(formula);
}
+ template <storm::dd::DdType Type>
+ DdPrismModelBuilder<Type>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> 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 <storm::dd::DdType Type>
void DdPrismModelBuilder<Type>::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<std::reference_wrapper<storm::prism::RewardModel const>> 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<std::string, storm::models::symbolic::StandardRewardModel<Type, double>> 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 <code>preserveFormula</code>.
+ *
+ * @param formula Thes formula based on which to choose the building options.
+ */
+ Options(std::vector<std::shared_ptr<storm::logic::Formula>> 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<std::map<storm::expressions::Variable, storm::expressions::Expression>> 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<std::set<std::string>> 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<ValueType>(std::move(optionalStateRewardVector), std::move(optionalStateActionRewardVector), std::move(optionalTransitionRewardMatrix));
}
@@ -104,14 +104,26 @@ namespace storm {
}
template <typename ValueType, typename IndexType>
- ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions() {
+ ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels() {
// Intentionally left empty.
}
template <typename ValueType, typename IndexType>
- ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()) {
+ ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()) {
this->preserveFormula(formula);
}
+
+ template <typename ValueType, typename IndexType>
+ ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> 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 <typename ValueType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, IndexType>::Options::preserveFormula(storm::logic::Formula const& formula) {
@@ -124,9 +136,15 @@ namespace storm {
}
// Extract all the labels used in the formula.
- std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula.getAtomicLabelFormulas();
- for (auto const& formula : atomicLabelFormulas) {
- labelsToBuild.get().insert(formula.get()->getLabel());
+ if (!buildAllLabels) {
+ if (!labelsToBuild) {
+ labelsToBuild = std::set<std::string>();
+ }
+
+ std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> 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<std::reference_wrapper<storm::prism::RewardModel const>> 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<ValueType>());
+
+ 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<ValueType>());
+ }
+
+ if (rewardModelIt->get().hasStateActionRewards()) {
+ builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
+ }
+ }
+
++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<ValueType>());
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<ValueType>());
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<ValueType>());
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<ValueType>());
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 <code>preserveFormula</code>.
+ *
+ * @param formula Thes formula based on which to choose the building options.
+ */
+ Options(std::vector<std::shared_ptr<storm::logic::Formula>> 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<std::map<storm::expressions::Variable, storm::expressions::Expression>> 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<std::set<std::string>> 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<typename ValueType, typename RewardModelType>
- std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType> const&(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
+ std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> 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<ValueType> computeLongRunAverage(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
private:
- static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType> const&(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
+ static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> 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<typename ValueType, typename RewardModelType>
RewardModelType const& Model<ValueType, RewardModelType>::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<ValueType, RewardModelType>::printRewardModelsInformationToStream(std::ostream& out) const {
if (this->rewardModels.size()) {
std::vector<std::string> rewardModelNames;
- std::for_each(this->rewardModels.cbegin(), this->rewardModels.cend(), [&rewardModelNames] (typename std::pair<std::string, RewardModelType> 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<std::string, RewardModelType> 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::DdType Type>
storm::dd::Bdd<Type> Model<Type>::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<storm::dd::DdType Type>
typename Model<Type>::RewardModelType const& Model<Type>::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<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::Options::Options(storm::models::sparse::Model<ValueType> const& model, storm::logic::Formula const& formula) : Options() {
+ this->preserveSingleFormula(model, formula);
+ }
+
+ template<typename ValueType>
+ DeterministicModelBisimulationDecomposition<ValueType>::Options::Options(storm::models::sparse::Model<ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : Options() {
+ if (formulas.size() == 1) {
+ this->preserveSingleFormula(model, *formulas.front());
+ } else {
+ for (auto const& formula : formulas) {
+ std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> atomicExpressionFormulas = formula->getAtomicExpressionFormulas();
+ std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula->getAtomicLabelFormulas();
+
+ std::set<std::string> 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<typename ValueType>
+ DeterministicModelBisimulationDecomposition<ValueType>::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) {
+ // Intentionally left empty.
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Options::preserveSingleFormula(storm::models::sparse::Model<ValueType> const& model, storm::logic::Formula const& formula) {
if (!formula.containsRewardOperator()) {
this->keepRewards = false;
}
@@ -664,11 +701,6 @@ namespace storm {
}
}
- template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) {
- // Intentionally left empty.
- }
-
template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::sparse::Dtmc<ValueType> 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<ValueType> 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<ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula>> 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<ValueType> 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<boost::optional<std::shared_ptr<storm::logic::Formula>>> formulas;
+ std::vector<std::shared_ptr<storm::logic::Formula>> formulas;
if (settings.isPropertySet()) {
- boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
+ std::shared_ptr<storm::logic::Formula> 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<std::string> 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<std::shared_ptr<storm::logic::Formula>> 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<std::shared_ptr<storm::logic::Formula>> formula : formulas) {
- if (settings.isSymbolicSet()) {
+ if (settings.isSymbolicSet()) {
#ifdef STORM_HAVE_CARL
- if (settings.isParametricSet()) {
- buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formula);
- } else {
+ if (settings.isParametricSet()) {
+ buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formulas);
+ } else {
#endif
- buildAndCheckSymbolicModel<double>(program.get(), formula);
+ buildAndCheckSymbolicModel<double>(program.get(), formulas);
#ifdef STORM_HAVE_CARL
- }
+ }
#endif
- } else if (settings.isExplicitSet()) {
- buildAndCheckExplicitModel<double>(formula);
- } else {
- STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
- }
+ } else if (settings.isExplicitSet()) {
+ buildAndCheckExplicitModel<double>(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<typename ValueType>
- std::shared_ptr<storm::models::ModelBase> buildSymbolicModel(storm::prism::Program const& program, boost::optional<std::shared_ptr<storm::logic::Formula>> const& formula) {
+ std::shared_ptr<storm::models::ModelBase> buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::shared_ptr<storm::models::ModelBase> 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<ValueType>::Options options;
- if (formula) {
- options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get());
- }
+ options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::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<ValueType>::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<storm::dd::DdType::CUDD>::Options options;
- if (formula) {
- options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(*formula.get());
- }
+ options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(formulas);
options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
result = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
@@ -130,7 +126,7 @@ namespace storm {
}
template<typename ValueType>
- std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, boost::optional<std::shared_ptr<storm::logic::Formula>> const& formula) {
+ std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula>> 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<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
@@ -141,8 +137,8 @@ namespace storm {
std::cout << "Performing bisimulation minimization... ";
typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options;
- if (formula) {
- options = typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options(*sparseModel, *formula.get());
+ if (!formulas.empty()) {
+ options = typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options(*sparseModel, formulas);
}
if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
options.weak = true;
@@ -157,7 +153,7 @@ namespace storm {
}
template<typename ValueType>
- void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> formula) {
+ void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> 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<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> formula) {
+ inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
}
#endif
template<typename ValueType>
- void verifySparseModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> formula) {
+ void verifySparseModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> 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<ValueType>(program.get(), model, formula);
- } else {
- std::cout << std::endl << "Model checking property: " << *formula << " ...";
- std::unique_ptr<storm::modelchecker::CheckResult> result;
- if (model->getType() == storm::models::ModelType::Dtmc) {
- std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
- storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
- if (modelchecker.canHandle(*formula.get())) {
- result = modelchecker.check(*formula.get());
- } else {
- storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> 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<ValueType>(program.get(), model, formula);
+ } else {
+ std::cout << std::endl << "Model checking property: " << *formula << " ...";
+ std::unique_ptr<storm::modelchecker::CheckResult> result;
+ if (model->getType() == storm::models::ModelType::Dtmc) {
+ std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
+ storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
+ if (modelchecker.canHandle(*formula)) {
+ result = modelchecker.check(*formula);
+ } else {
+ storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker2(*dtmc);
+ if (modelchecker2.canHandle(*formula)) {
+ result = modelchecker2.check(*formula);
+ }
}
- }
- } else if (model->getType() == storm::models::ModelType::Mdp) {
- std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
+ } else if (model->getType() == storm::models::ModelType::Mdp) {
+ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
#ifdef STORM_HAVE_CUDA
- if (settings.isCudaSet()) {
- storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp);
- result = modelchecker.check(*formula.get());
- } else {
- storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
- result = modelchecker.check(*formula.get());
- }
+ if (settings.isCudaSet()) {
+ storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp);
+ result = modelchecker.check(*formula);
+ } else {
+ storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
+ result = modelchecker.check(*formula);
+ }
#else
- storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
- result = modelchecker.check(*formula.get());
+ storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
+ result = modelchecker.check(*formula);
#endif
- } else if (model->getType() == storm::models::ModelType::Ctmc) {
- std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
-
- storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> 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<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
+
+ storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> 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<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> formula) {
+ inline void verifySparseModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<storm::logic::Formula>> 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<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-
- std::cout << std::endl << "Model checking property: " << *formula << " ...";
- std::unique_ptr<storm::modelchecker::CheckResult> result;
-
- storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> 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<storm::RationalFunction>()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc<storm::RationalFunction>::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<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+
+ std::cout << std::endl << "Model checking property: " << *formula << " ...";
+ std::unique_ptr<storm::modelchecker::CheckResult> result;
+
+ storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> 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<storm::RationalFunction>()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector(*dtmc), parametricSettings.exportResultPath());
+ }
}
}
#endif
template<storm::dd::DdType DdType>
- void verifySymbolicModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<storm::logic::Formula> formula) {
-
- std::cout << std::endl << "Model checking property: " << *formula << " ...";
- std::unique_ptr<storm::modelchecker::CheckResult> result;
- if (model->getType() == storm::models::ModelType::Dtmc) {
- std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
- storm::modelchecker::HybridDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc);
- if (modelchecker.canHandle(*formula.get())) {
- result = modelchecker.check(*formula.get());
- }
- } else if (model->getType() == storm::models::ModelType::Ctmc) {
- std::shared_ptr<storm::models::symbolic::Ctmc<DdType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType>>();
- storm::modelchecker::HybridCtmcCslModelChecker<DdType, double> modelchecker(*ctmc);
- if (modelchecker.canHandle(*formula.get())) {
- result = modelchecker.check(*formula.get());
+ void verifySymbolicModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+ for (auto const& formula : formulas) {
+ std::cout << std::endl << "Model checking property: " << *formula << " ...";
+ std::unique_ptr<storm::modelchecker::CheckResult> result;
+ if (model->getType() == storm::models::ModelType::Dtmc) {
+ std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
+ storm::modelchecker::HybridDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc);
+ if (modelchecker.canHandle(*formula)) {
+ result = modelchecker.check(*formula);
+ }
+ } else if (model->getType() == storm::models::ModelType::Ctmc) {
+ std::shared_ptr<storm::models::symbolic::Ctmc<DdType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType>>();
+ storm::modelchecker::HybridCtmcCslModelChecker<DdType, double> modelchecker(*ctmc);
+ if (modelchecker.canHandle(*formula)) {
+ result = modelchecker.check(*formula);
+ }
+ } else if (model->getType() == storm::models::ModelType::Mdp) {
+ std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
+ storm::modelchecker::HybridMdpPrctlModelChecker<DdType, double> 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<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
- storm::modelchecker::HybridMdpPrctlModelChecker<DdType, double> 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<DdType>(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<DdType>(model->getReachableStates(), model->getInitialStates()));
- std::cout << *result << std::endl;
- } else {
- std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
}
}
template<typename ValueType>
- void buildAndCheckSymbolicModel(boost::optional<storm::prism::Program> const& program, boost::optional<std::shared_ptr<storm::logic::Formula>> formula) {
+ void buildAndCheckSymbolicModel(boost::optional<storm::prism::Program> const& program, std::vector<std::shared_ptr<storm::logic::Formula>> 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<storm::models::ModelBase> model = buildSymbolicModel<ValueType>(program.get(), formula);
+ std::shared_ptr<storm::models::ModelBase> model = buildSymbolicModel<ValueType>(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<ValueType>(model, formula);
+ model = preprocessModel<ValueType>(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<ValueType>(program, model->as<storm::models::sparse::Model<ValueType>>(), formula.get());
+ verifySparseModel<ValueType>(program, model->as<storm::models::sparse::Model<ValueType>>(), formulas);
} else if (model->isSymbolicModel()) {
if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
- verifySymbolicModel(program, model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formula.get());
+ verifySymbolicModel(program, model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), 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<typename ValueType>
- void buildAndCheckExplicitModel(boost::optional<std::shared_ptr<storm::logic::Formula>> formula) {
+ void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula>> 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<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>());
// Preprocess the model if needed.
- model = preprocessModel<ValueType>(model, formula);
+ model = preprocessModel<ValueType>(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<ValueType>(boost::optional<storm::prism::Program>(), model->as<storm::models::sparse::Model<ValueType>>(), formula.get());
+ verifySparseModel<ValueType>(boost::optional<storm::prism::Program>(), model->as<storm::models::sparse::Model<ValueType>>(), 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;
}
}
}