diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index ac02b9761..dae747228 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -473,18 +473,18 @@ namespace storm {
};
template <storm::dd::DdType Type, typename ValueType>
- DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), terminalStates(), negatedTerminalStates() {
+ DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), buildAllLabels(true), labelsToBuild(), terminalStates(), negatedTerminalStates() {
// Intentionally left empty.
}
template <storm::dd::DdType Type, typename ValueType>
- DdPrismModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), terminalStates(), negatedTerminalStates() {
+ DdPrismModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), terminalStates(), negatedTerminalStates() {
this->preserveFormula(formula);
this->setTerminalStatesFromFormula(formula);
}
template <storm::dd::DdType Type, typename ValueType>
- DdPrismModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() {
+ DdPrismModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
this->buildAllLabels = true;
@@ -554,22 +554,6 @@ namespace storm {
}
}
- template <storm::dd::DdType Type, typename ValueType>
- void DdPrismModelBuilder<Type, ValueType>::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
- std::map<storm::expressions::Variable, storm::expressions::Expression> newConstantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
-
- // If there is at least one constant that is defined, and the constant definition map does not yet exist,
- // we need to create it.
- if (!constantDefinitions && !newConstantDefinitions.empty()) {
- constantDefinitions = std::map<storm::expressions::Variable, storm::expressions::Expression>();
- }
-
- // Now insert all the entries that need to be defined.
- for (auto const& entry : newConstantDefinitions) {
- constantDefinitions.get().insert(entry);
- }
- }
-
template <storm::dd::DdType Type, typename ValueType>
struct DdPrismModelBuilder<Type, ValueType>::SystemResult {
SystemResult(storm::dd::Add<Type, ValueType> const& allTransitionsDd, DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& stateActionDd) : allTransitionsDd(allTransitionsDd), globalModule(globalModule), stateActionDd(stateActionDd) {
@@ -1248,11 +1232,7 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdPrismModelBuilder<Type, ValueType>::build(storm::prism::Program const& program, Options const& options) {
- if (options.constantDefinitions) {
- preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get());
- } else {
- preparedProgram = program;
- }
+ preparedProgram = program;
if (preparedProgram->hasUndefinedConstants()) {
std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram->getUndefinedConstants();
diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp
index 26563d408..05cdf7f1d 100644
--- a/src/generator/NextStateGenerator.cpp
+++ b/src/generator/NextStateGenerator.cpp
@@ -5,7 +5,7 @@
#include "src/logic/Formulas.h"
#include "src/utility/macros.h"
-#include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/InvalidSettingsException.h"
namespace storm {
namespace generator {
@@ -34,16 +34,16 @@ namespace storm {
return boost::get<storm::expressions::Expression const&>(labelOrExpression);
}
- NextStateGeneratorOptions::NextStateGeneratorOptions() : buildChoiceLabels(false) {
+ NextStateGeneratorOptions::NextStateGeneratorOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false) {
// Intentionally left empty.
}
- NextStateGeneratorOptions::NextStateGeneratorOptions(storm::logic::Formula const& formula) {
+ NextStateGeneratorOptions::NextStateGeneratorOptions(storm::logic::Formula const& formula) : NextStateGeneratorOptions() {
this->preserveFormula(formula);
this->setTerminalStatesFromFormula(formula);
}
- NextStateGeneratorOptions::NextStateGeneratorOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+ NextStateGeneratorOptions::NextStateGeneratorOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : NextStateGeneratorOptions() {
if (!formulas.empty()) {
for (auto const& formula : formulas) {
this->preserveFormula(*formula);
@@ -112,8 +112,8 @@ namespace storm {
return rewardModelNames;
}
- std::set<std::string> const& NextStateGeneratorOptions::getLabels() const {
- return labels;
+ std::set<std::string> const& NextStateGeneratorOptions::getLabelNames() const {
+ return labelNames;
}
std::vector<storm::expressions::Expression> const& NextStateGeneratorOptions::getExpressionLabels() const {
@@ -135,19 +135,39 @@ namespace storm {
bool NextStateGeneratorOptions::isBuildChoiceLabelsSet() const {
return buildChoiceLabels;
}
+
+ bool NextStateGeneratorOptions::isBuildAllRewardModelsSet() const {
+ return buildAllRewardModels;
+ }
+
+ bool NextStateGeneratorOptions::isBuildAllLabelsSet() const {
+ return buildAllLabels;
+ }
+ NextStateGeneratorOptions& NextStateGeneratorOptions::setBuildAllRewardModels() {
+ buildAllRewardModels = true;
+ return *this;
+ }
+
NextStateGeneratorOptions& NextStateGeneratorOptions::addRewardModel(std::string const& rewardModelName) {
+ STORM_LOG_THROW(!buildAllRewardModels, storm::exceptions::InvalidSettingsException, "Cannot add reward model, because all reward models are built anyway.");
rewardModelNames.emplace_back(rewardModelName);
return *this;
}
-
+
+ NextStateGeneratorOptions& NextStateGeneratorOptions::setBuildAllLabels() {
+ buildAllLabels = true;
+ return *this;
+ }
+
NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(storm::expressions::Expression const& expression) {
expressionLabels.emplace_back(expression);
return *this;
}
- NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(std::string const& label) {
- labels.insert(label);
+ NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(std::string const& labelName) {
+ STORM_LOG_THROW(!buildAllLabels, storm::exceptions::InvalidSettingsException, "Cannot add label, because all labels are built anyway.");
+ labelNames.insert(labelName);
return *this;
}
diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h
index 1b9c7a374..a88285be8 100644
--- a/src/generator/NextStateGenerator.h
+++ b/src/generator/NextStateGenerator.h
@@ -48,7 +48,7 @@ namespace storm {
/*!
* Creates an object representing the default options.
*/
- NextStateGeneratorOptions();
+ NextStateGeneratorOptions(bool buildAllRewardModels = false, bool buildAllLabels = false);
/*!
* Creates an object representing the suggested building options assuming that the given formula is the
@@ -85,26 +85,37 @@ namespace storm {
void setTerminalStatesFromFormula(storm::logic::Formula const& formula);
std::vector<std::string> const& getRewardModelNames() const;
- std::set<std::string> const& getLabels() const;
+ std::set<std::string> const& getLabelNames() const;
std::vector<storm::expressions::Expression> const& getExpressionLabels() const;
std::vector<std::pair<LabelOrExpression, bool>> const& getTerminalStates() const;
bool hasTerminalStates() const;
void clearTerminalStates();
bool isBuildChoiceLabelsSet() const;
+ bool isBuildAllRewardModelsSet() const;
+ bool isBuildAllLabelsSet() const;
+ NextStateGeneratorOptions& setBuildAllRewardModels();
NextStateGeneratorOptions& addRewardModel(std::string const& rewardModelName);
+ NextStateGeneratorOptions& setBuildAllLabels();
NextStateGeneratorOptions& addLabel(storm::expressions::Expression const& expression);
- NextStateGeneratorOptions& addLabel(std::string const& label);
+ NextStateGeneratorOptions& addLabel(std::string const& labelName);
NextStateGeneratorOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value);
NextStateGeneratorOptions& addTerminalLabel(std::string const& label, bool value);
NextStateGeneratorOptions& setBuildChoiceLabels(bool newValue);
private:
+ /// A flag that indicates whether all reward models are to be built. In this case, the reward model names are
+ /// to be ignored.
+ bool buildAllRewardModels;
+
/// The names of the reward models to generate.
std::vector<std::string> rewardModelNames;
+ /// A flag that indicates whether all labels are to be built. In this case, the label names are to be ignored.
+ bool buildAllLabels;
+
/// A set of labels to build.
- std::set<std::string> labels;
+ std::set<std::string> labelNames;
/// The expression that are to be used for creating the state labeling.
std::vector<storm::expressions::Expression> expressionLabels;
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
index 1ec8c3243..30dc232fa 100644
--- a/src/generator/PrismNextStateGenerator.cpp
+++ b/src/generator/PrismNextStateGenerator.cpp
@@ -18,21 +18,27 @@ namespace storm {
PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : NextStateGenerator<ValueType, StateType>(options), program(program), rewardModels(), variableInformation(program), evaluator(program.getManager()), state(nullptr), comparator() {
STORM_LOG_THROW(!program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
- // Extract the reward models from the program based on the names we were given.
- for (auto const& rewardModelName : this->options.getRewardModelNames()) {
- if (program.hasRewardModel(rewardModelName)) {
- rewardModels.push_back(program.getRewardModel(rewardModelName));
- } else {
- STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
- STORM_LOG_THROW(program.getNumberOfRewardModels() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
- STORM_LOG_THROW(program.getNumberOfRewardModels() > 0, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is invalid, because there is no reward model.");
+ if (this->options.isBuildAllRewardModelsSet()) {
+ for (auto const& rewardModel : program.getRewardModels()) {
+ rewardModels.push_back(rewardModel);
+ }
+ } else {
+ // Extract the reward models from the program based on the names we were given.
+ for (auto const& rewardModelName : this->options.getRewardModelNames()) {
+ if (program.hasRewardModel(rewardModelName)) {
+ rewardModels.push_back(program.getRewardModel(rewardModelName));
+ } else {
+ STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
+ STORM_LOG_THROW(program.getNumberOfRewardModels() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
+ STORM_LOG_THROW(program.getNumberOfRewardModels() > 0, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is invalid, because there is no reward model.");
+ }
+ }
+
+ // If no reward model was yet added, but there was one that was given in the options, we try to build
+ // standard reward model.
+ if (rewardModels.empty() && !this->options.getRewardModelNames().empty()) {
+ rewardModels.push_back(program.getRewardModel(0));
}
- }
-
- // If no reward model was yet added, but there was one that was given in the options, we try to build
- // standard reward model.
- if (rewardModels.empty() && !this->options.getRewardModelNames().empty()) {
- rewardModels.push_back(program.getRewardModel(0));
}
// If there are terminal states we need to handle, we now need to translate all labels to expressions.
@@ -467,10 +473,16 @@ namespace storm {
storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices) {
// Gather a vector of labels and their expressions so we can iterate it over it a lot.
std::vector<std::pair<std::string, storm::expressions::Expression>> labels;
- for (auto const& label : this->options.getLabels()) {
- labels.push_back(std::make_pair(label, program.getLabelExpression(label)));
+ if (this->options.isBuildAllLabelsSet()) {
+ for (auto const& label : program.getLabels()) {
+ labels.push_back(std::make_pair(label.getName(), label.getStatePredicateExpression()));
+ }
+ } else {
+ for (auto const& labelName : this->options.getLabelNames()) {
+ labels.push_back(std::make_pair(labelName, program.getLabelExpression(labelName)));
+ }
}
-
+
// Make the labels unique.
std::sort(labels.begin(), labels.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first < b.first; } );
auto it = std::unique(labels.begin(), labels.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first == b.first; } );
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 0676cf1ef..3e7a5d992 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -121,7 +121,6 @@ namespace storm {
} else if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Dd || storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) {
typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options;
options = typename storm::builder::DdPrismModelBuilder<LibraryType>::Options(formulas);
- options.addConstantDefinitionsFromString(program, constantDefinitionString);
storm::builder::DdPrismModelBuilder<LibraryType> builder;
result.model = builder.build(program, options);