diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index 2d9be972d..f981f4c60 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -103,29 +103,7 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
- void DdJaniModelBuilder<Type, ValueType>::Options::addConstantDefinitionsFromString(storm::jani::Model const& model, std::string const& constantDefinitionString) {
- std::map<storm::expressions::Variable, storm::expressions::Expression> newConstantDefinitions = storm::utility::jani::parseConstantDefinitionString(model, 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>
- DdJaniModelBuilder<Type, ValueType>::DdJaniModelBuilder(storm::jani::Model const& model, Options const& options) : options(options) {
- if (options.constantDefinitions) {
- this->model = model.defineUndefinedConstants(options.constantDefinitions.get());
- } else {
- this->model = model;
- }
-
+ DdJaniModelBuilder<Type, ValueType>::DdJaniModelBuilder(storm::jani::Model const& model, Options const& options) : model(model), options(options) {
if (this->model->hasUndefinedConstants()) {
std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = this->model->getUndefinedConstants();
std::vector<std::string> strings;
diff --git a/src/builder/DdJaniModelBuilder.h b/src/builder/DdJaniModelBuilder.h
index 605a4ea9d..348d017ad 100644
--- a/src/builder/DdJaniModelBuilder.h
+++ b/src/builder/DdJaniModelBuilder.h
@@ -40,17 +40,7 @@ namespace storm {
* @param formula Thes formula based on which to choose the building options.
*/
Options(std::vector<std::shared_ptr<storm::logic::Formula const>> 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.
- *
- * @param program The program managing the constants that shall be defined. Note that the program itself
- * is not modified whatsoever.
- * @param constantDefinitionString The string from which to parse the constants' values.
- */
- void addConstantDefinitionsFromString(storm::jani::Model const& model, std::string const& constantDefinitionString);
-
+
/*!
* Changes the options in a way that ensures that the given formula can be checked on the model once it
* has been built.
diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp
index dbb5dd5d5..e99f2f37a 100644
--- a/src/builder/ExplicitModelBuilder.cpp
+++ b/src/builder/ExplicitModelBuilder.cpp
@@ -100,6 +100,11 @@ namespace storm {
// Intentionally left empty.
}
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ ExplicitModelBuilder<ValueType, RewardModelType, StateType>::ExplicitModelBuilder(storm::prism::Program const& program, storm::generator::NextStateGeneratorOptions const& generatorOptions, Options const& builderOptions) : ExplicitModelBuilder(std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, StateType>>(program, generatorOptions), builderOptions) {
+ // Intentionally left empty.
+ }
+
template <typename ValueType, typename RewardModelType, typename StateType>
storm::storage::sparse::StateValuations const& ExplicitModelBuilder<ValueType, RewardModelType, StateType>::getStateValuations() const {
STORM_LOG_THROW(static_cast<bool>(stateValuations), storm::exceptions::InvalidOperationException, "The state information was not properly build.");
diff --git a/src/builder/ExplicitModelBuilder.h b/src/builder/ExplicitModelBuilder.h
index ef7703033..c78c79493 100644
--- a/src/builder/ExplicitModelBuilder.h
+++ b/src/builder/ExplicitModelBuilder.h
@@ -10,7 +10,7 @@
#include <boost/container/flat_set.hpp>
#include <boost/container/flat_map.hpp>
#include <boost/variant.hpp>
-#include <src/models/sparse/StandardRewardModel.h>
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/ExpressionEvaluator.h"
@@ -28,6 +28,7 @@
#include "src/builder/ExplorationOrder.h"
+#include "src/generator/NextStateGenerator.h"
#include "src/generator/CompressedState.h"
#include "src/generator/VariableInformation.h"
@@ -35,11 +36,6 @@ namespace storm {
namespace utility {
template<typename ValueType> class ConstantsComparator;
}
-
- namespace generator {
- template<typename ValueType, typename StateType>
- class NextStateGenerator;
- }
namespace builder {
@@ -85,11 +81,18 @@ namespace storm {
};
/*!
- * Creates an explicit model builder that uses the provided generator..
+ * Creates an explicit model builder that uses the provided generator.
*
* @param generator The generator to use.
*/
ExplicitModelBuilder(std::shared_ptr<storm::generator::NextStateGenerator<ValueType, StateType>> const& generator, Options const& options = Options());
+
+ /*!
+ * Creates an explicit model builder for the given PRISM program..
+ *
+ * @param program The program for which to build the model.
+ */
+ ExplicitModelBuilder(storm::prism::Program const& program, storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions(), Options const& builderOptions = Options());
/*!
* Convert the program given at construction time to an abstract model. The type of the model is the one
diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index 3f97db791..a3702875b 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -59,8 +59,15 @@ namespace storm {
for (auto const& formula : formulas) {
STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs.");
std::cout << std::endl << "Model checking property: " << *formula << " ...";
- storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
- storm::modelchecker::SparseExplorationModelChecker<ValueType> checker(program, storm::utility::prism::parseConstantDefinitionString(program, storm::settings::getModule<storm::settings::modules::IOSettings>().getConstantDefinitionString()));
+
+ std::string constantDefinitionString = storm::settings::getModule<storm::settings::modules::IOSettings>().getConstantDefinitionString();
+ storm::prism::Program preprocessedProgram = storm::utility::prism::preprocess<ValueType>(program, constantDefinitionString);
+ std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = preprocessedProgram.getConstantsSubstitution();
+
+ storm::modelchecker::SparseExplorationModelChecker<ValueType> checker(program);
+
+ std::shared_ptr<storm::logic::Formula> substitutedFormula = formula->substitute(constantsSubstitution);
+ storm::modelchecker::CheckTask<storm::logic::Formula> task(*substitutedFormula, onlyInitialStatesRelevant);
std::unique_ptr<storm::modelchecker::CheckResult> result;
if (checker.canHandle(task)) {
result = checker.check(task);
diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp
index 05cdf7f1d..547b76c15 100644
--- a/src/generator/NextStateGenerator.cpp
+++ b/src/generator/NextStateGenerator.cpp
@@ -210,12 +210,7 @@ namespace storm {
NextStateGenerator<ValueType, StateType>::NextStateGenerator(NextStateGeneratorOptions const& options) : options(options) {
// Intentionally left empty.
}
-
- template<typename ValueType, typename StateType>
- std::size_t NextStateGenerator<ValueType, StateType>::getNumberOfRewardModels() const {
- return this->options.getRewardModelNames().size();
- }
-
+
template<typename ValueType, typename StateType>
NextStateGeneratorOptions const& NextStateGenerator<ValueType, StateType>::getOptions() const {
return options;
diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h
index a88285be8..668b2f0be 100644
--- a/src/generator/NextStateGenerator.h
+++ b/src/generator/NextStateGenerator.h
@@ -166,7 +166,7 @@ namespace storm {
virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) = 0;
virtual bool satisfies(storm::expressions::Expression const& expression) const = 0;
- std::size_t getNumberOfRewardModels() const;
+ virtual std::size_t getNumberOfRewardModels() const = 0;
virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0;
virtual storm::expressions::SimpleValuation toValuation(CompressedState const& state) const = 0;
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
index 30dc232fa..5e4a1d6ed 100644
--- a/src/generator/PrismNextStateGenerator.cpp
+++ b/src/generator/PrismNextStateGenerator.cpp
@@ -15,39 +15,44 @@ namespace storm {
namespace generator {
template<typename ValueType, typename StateType>
- 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.");
+ PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : NextStateGenerator<ValueType, StateType>(options), program(program.substituteConstants()), rewardModels(), variableInformation(this->program), evaluator(this->program.getManager()), state(nullptr), comparator() {
+ STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
if (this->options.isBuildAllRewardModelsSet()) {
- for (auto const& rewardModel : program.getRewardModels()) {
+ for (auto const& rewardModel : this->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));
+ if (this->program.hasRewardModel(rewardModelName)) {
+ rewardModels.push_back(this->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.");
+ STORM_LOG_THROW(this->program.getNumberOfRewardModels() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
+ STORM_LOG_THROW(this->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));
+ rewardModels.push_back(this->program.getRewardModel(0));
}
}
+ // Determine whether any reward model has state action rewards.
+ for (auto const& rewardModel : rewardModels) {
+ hasStateActionRewards |= rewardModel.get().hasStateActionRewards();
+ }
+
// If there are terminal states we need to handle, we now need to translate all labels to expressions.
if (this->options.hasTerminalStates()) {
for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
if (expressionOrLabelAndBool.first.isExpression()) {
terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
} else {
- terminalStates.push_back(std::make_pair(program.getLabelExpression(expressionOrLabelAndBool.first.getLabel()), expressionOrLabelAndBool.second));
+ terminalStates.push_back(std::make_pair(this->program.getLabelExpression(expressionOrLabelAndBool.first.getLabel()), expressionOrLabelAndBool.second));
}
}
}
@@ -521,6 +526,11 @@ namespace storm {
return result;
}
+ template<typename ValueType, typename StateType>
+ std::size_t PrismNextStateGenerator<ValueType, StateType>::getNumberOfRewardModels() const {
+ return rewardModels.size();
+ }
+
template<typename ValueType, typename StateType>
RewardModelInformation PrismNextStateGenerator<ValueType, StateType>::getRewardModelInformation(uint64_t const& index) const {
storm::prism::RewardModel const& rewardModel = rewardModels[index].get();
diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h
index c7fc61e16..c3d3c63d9 100644
--- a/src/generator/PrismNextStateGenerator.h
+++ b/src/generator/PrismNextStateGenerator.h
@@ -28,6 +28,7 @@ namespace storm {
virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
virtual bool satisfies(storm::expressions::Expression const& expression) const override;
+ virtual std::size_t getNumberOfRewardModels() const override;
virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
virtual storm::expressions::SimpleValuation toValuation(CompressedState const& state) const override;
@@ -79,7 +80,7 @@ namespace storm {
std::vector<Choice<ValueType>> getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
// The program used for the generation of next states.
- storm::prism::Program const& program;
+ storm::prism::Program program;
// The reward models that need to be considered.
std::vector<std::reference_wrapper<storm::prism::RewardModel const>> rewardModels;
diff --git a/src/modelchecker/exploration/SparseExplorationModelChecker.cpp b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp
index fe192aa9e..dba541891 100644
--- a/src/modelchecker/exploration/SparseExplorationModelChecker.cpp
+++ b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp
@@ -35,7 +35,7 @@ namespace storm {
namespace modelchecker {
template<typename ValueType, typename StateType>
- SparseExplorationModelChecker<ValueType, StateType>::SparseExplorationModelChecker(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions) : program(storm::utility::prism::preprocess<ValueType>(program, constantDefinitions.get())), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision()) {
+ SparseExplorationModelChecker<ValueType, StateType>::SparseExplorationModelChecker(storm::prism::Program const& program) : program(program.substituteConstants()), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision()) {
// Intentionally left empty.
}
diff --git a/src/modelchecker/exploration/SparseExplorationModelChecker.h b/src/modelchecker/exploration/SparseExplorationModelChecker.h
index 6c137d088..bc41ace7a 100644
--- a/src/modelchecker/exploration/SparseExplorationModelChecker.h
+++ b/src/modelchecker/exploration/SparseExplorationModelChecker.h
@@ -36,7 +36,7 @@ namespace storm {
typedef StateType ActionType;
typedef std::vector<std::pair<StateType, ActionType>> StateActionStack;
- SparseExplorationModelChecker(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions = boost::none);
+ SparseExplorationModelChecker(storm::prism::Program const& program);
virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
index 7cdbc2159..25763b37f 100644
--- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
@@ -28,14 +28,8 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
-#ifdef WINDOWS
- storm::builder::ExplicitModelBuilder<double>::Options options;
-#else
- typename storm::builder::ExplicitModelBuilder<double>::Options options;
-#endif
- options.buildAllRewardModels = false;
- options.rewardModelsToBuild.insert("num_repairs");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build();
+ storm::generator::NextStateGeneratorOptions options;
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("num_repairs")).build();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -111,14 +105,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
-#ifdef WINDOWS
- storm::builder::ExplicitModelBuilder<double>::Options options;
-#else
- typename storm::builder::ExplicitModelBuilder<double>::Options options;
-#endif
- options.buildAllRewardModels = false;
- options.rewardModelsToBuild.insert("up");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build();
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("up")).build();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -180,7 +167,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -221,13 +208,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
-#ifdef WINDOWS
- storm::builder::ExplicitModelBuilder<double>::Options options;
-#else
- typename storm::builder::ExplicitModelBuilder<double>::Options options;
-#endif
- options.rewardModelsToBuild.insert("customers");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build();
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("customers")).build();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
index 9feeda286..bb96f4511 100644
--- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
@@ -284,7 +284,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) {
TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/test_conditional.pm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(true, true)).build();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
ASSERT_EQ(4ul, model->getNumberOfStates());
ASSERT_EQ(5ul, model->getNumberOfTransitions());
diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
index 02ea39e5f..c5f7899dc 100644
--- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
@@ -197,7 +197,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) {
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+ storm::generator::NextStateGeneratorOptions options;
+ options.setBuildAllLabels();
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build();
EXPECT_EQ(4ul, model->getNumberOfStates());
EXPECT_EQ(11ul, model->getNumberOfTransitions());
@@ -241,13 +243,13 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) {
EXPECT_EQ(0, scheduler2.getChoice(3));
}
-TEST(GmmxxMdpPrctlModelCheckerTest, tiny_rewards) {
+TEST(GmmxxMdpPrctlModelCheckerTest, TinyRewards) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/tiny_rewards.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(true, true)).build();
EXPECT_EQ(3ul, model->getNumberOfStates());
EXPECT_EQ(4ul, model->getNumberOfTransitions());
diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
index fa3f89a02..65d58c19f 100644
--- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
@@ -26,14 +26,7 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
-#ifdef WINDOWS
- storm::builder::ExplicitModelBuilder<double>::Options options;
-#else
- typename storm::builder::ExplicitModelBuilder<double>::Options options;
-#endif
- options.buildAllRewardModels = false;
- options.rewardModelsToBuild.insert("num_repairs");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build();
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true). addRewardModel("num_repairs")).build();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -102,13 +95,8 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
-#ifdef WINDOWS
- storm::builder::ExplicitModelBuilder<double>::Options options;
-#else
- typename storm::builder::ExplicitModelBuilder<double>::Options options;
-#endif
- options.buildAllRewardModels = false;
- options.rewardModelsToBuild.insert("up");
+ storm::generator::NextStateGeneratorOptions options;
+ options.addRewardModel("up").setBuildAllLabels();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
@@ -164,7 +152,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model.
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
@@ -198,14 +186,7 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) {
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
// Build the model with the customers reward structure.
-#ifdef WINDOWS
- storm::builder::ExplicitModelBuilder<double>::Options options;
-#else
- typename storm::builder::ExplicitModelBuilder<double>::Options options;
-#endif
- options.buildAllRewardModels = false;
- options.rewardModelsToBuild.insert("customers");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build();
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true).addRewardModel("customers")).build();
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
diff --git a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
index 80b4184f4..696cc8b83 100644
--- a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
+++ b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
@@ -10,6 +10,8 @@
#include "src/models/sparse/StandardRewardModel.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#ifdef STORM_HAVE_GUROBI
+
TEST(MilpPermissiveSchedulerTest, DieSelection) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_c1.nm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
@@ -22,12 +24,8 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) {
auto formula001b = formulaParser.parseSingleFormulaFromString("P<=0.17 [ F \"one\"]")->asProbabilityOperatorFormula();
// Customize and perform model-building.
- typename storm::builder::ExplicitModelBuilder<double>::Options options;
-
- options = typename storm::builder::ExplicitModelBuilder<double>::Options(formula02);
- options.addConstantDefinitionsFromString(program, "");
- options.buildCommandLabels = true;
-
+ storm::generator::NextStateGeneratorOptions options;
+ options.setBuildAllLabels().setBuildChoiceLabels(true);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02);
@@ -58,3 +56,5 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) {
//
}
+
+#endif
\ No newline at end of file
diff --git a/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
index 045a26071..531d29f5a 100644
--- a/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
+++ b/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
@@ -14,7 +14,7 @@ TEST(NondeterministicModelBisimulationDecomposition, TwoDice) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
// Build the die model without its reward model.
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>();
diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp
index ae3893fa5..2813e1a9b 100644
--- a/test/functional/utility/GraphTest.cpp
+++ b/test/functional/utility/GraphTest.cpp
@@ -181,7 +181,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
TEST(GraphTest, ExplicitProb01) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
@@ -202,7 +202,7 @@ TEST(GraphTest, ExplicitProb01) {
TEST(GraphTest, ExplicitProb01MinMax) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
- std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+ std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -217,7 +217,7 @@ TEST(GraphTest, ExplicitProb01MinMax) {
EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
- model = storm::builder::ExplicitModelBuilder<double>(program).build();
+ model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -238,7 +238,7 @@ TEST(GraphTest, ExplicitProb01MinMax) {
EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
- model = storm::builder::ExplicitModelBuilder<double>(program).build();
+ model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp
index 5fbd811a6..c7a9c0e31 100644
--- a/test/functional/utility/ModelInstantiatorTest.cpp
+++ b/test/functional/utility/ModelInstantiatorTest.cpp
@@ -22,7 +22,6 @@ TEST(ModelInstantiatorTest, BrpProb) {
std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm";
std::string formulaAsString = "P=? [F s=5 ]";
- std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
// Program and formula
storm::prism::Program program = storm::parseProgram(programFile);
@@ -30,9 +29,7 @@ TEST(ModelInstantiatorTest, BrpProb) {
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
ASSERT_TRUE(formulas.size()==1);
// Parametric model
- typename storm::builder::ExplicitModelBuilder<storm::RationalFunction>::Options options = storm::builder::ExplicitModelBuilder<storm::RationalFunction>::Options(*formulas[0]);
- options.addConstantDefinitionsFromString(program, constantsAsString);
- options.preserveFormula(*formulas[0]);
+ storm::generator::NextStateGeneratorOptions options(*formulas.front());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
@@ -143,7 +140,6 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm";
std::string formulaAsString = "R=? [F ((s=5) | (s=0&srep=3)) ]";
- std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
// Program and formula
storm::prism::Program program = storm::parseProgram(programFile);
@@ -151,9 +147,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
ASSERT_TRUE(formulas.size()==1);
// Parametric model
- typename storm::builder::ExplicitModelBuilder<storm::RationalFunction>::Options options = storm::builder::ExplicitModelBuilder<storm::RationalFunction>::Options(*formulas[0]);
- options.addConstantDefinitionsFromString(program, constantsAsString);
- options.preserveFormula(*formulas[0]);
+ storm::generator::NextStateGeneratorOptions options(*formulas.front());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
@@ -216,7 +210,6 @@ TEST(ModelInstantiatorTest, Consensus) {
std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/coin2_2.pm";
std::string formulaAsString = "Pmin=? [F \"finished\"&\"all_coins_equal_1\" ]";
- std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
// Program and formula
storm::prism::Program program = storm::parseProgram(programFile);
@@ -224,9 +217,7 @@ TEST(ModelInstantiatorTest, Consensus) {
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
ASSERT_TRUE(formulas.size()==1);
// Parametric model
- typename storm::builder::ExplicitModelBuilder<storm::RationalFunction>::Options options = storm::builder::ExplicitModelBuilder<storm::RationalFunction>::Options(*formulas[0]);
- options.addConstantDefinitionsFromString(program, constantsAsString);
- options.preserveFormula(*formulas[0]);
+ storm::generator::NextStateGeneratorOptions options(*formulas.front());
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> mdp = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build()->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>> modelInstantiator(*mdp);