From d0e15d1a4fa2fda2860934cc7ab4b94e54811053 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 15 Dec 2015 17:02:58 +0100
Subject: [PATCH] more work (and stuff, you know?)
Former-commit-id: ec9f6746b8bf1c3e274a46746054011d25d54ae5
---
src/builder/DdPrismModelBuilder.cpp | 62 ++++++++--------
src/builder/DdPrismModelBuilder.h | 25 +++----
src/builder/ExplicitPrismModelBuilder.cpp | 49 ++++++-------
src/builder/ExplicitPrismModelBuilder.h | 11 +++
src/cli/entrypoints.h | 38 +++++++---
src/logic/AtomicExpressionFormula.cpp | 6 +-
src/logic/AtomicExpressionFormula.h | 3 +-
src/logic/AtomicLabelFormula.cpp | 4 ++
src/logic/AtomicLabelFormula.h | 4 +-
src/logic/BinaryBooleanStateFormula.cpp | 4 ++
src/logic/BinaryBooleanStateFormula.h | 4 ++
src/logic/BinaryPathFormula.h | 2 +-
src/logic/BooleanLiteralFormula.cpp | 4 ++
src/logic/BooleanLiteralFormula.h | 4 +-
src/logic/BoundedUntilFormula.cpp | 8 +++
src/logic/BoundedUntilFormula.h | 3 +
src/logic/ConditionalPathFormula.cpp | 4 ++
src/logic/ConditionalPathFormula.h | 2 +
src/logic/CumulativeRewardFormula.cpp | 4 ++
src/logic/CumulativeRewardFormula.h | 2 +
src/logic/EventuallyFormula.cpp | 4 ++
src/logic/EventuallyFormula.h | 3 +
src/logic/ExpectedTimeOperatorFormula.cpp | 4 ++
src/logic/ExpectedTimeOperatorFormula.h | 2 +
src/logic/Formula.cpp | 2 +-
src/logic/Formula.h | 5 ++
src/logic/GloballyFormula.cpp | 4 ++
src/logic/GloballyFormula.h | 2 +
src/logic/InstantaneousRewardFormula.cpp | 4 ++
src/logic/InstantaneousRewardFormula.h | 2 +
src/logic/LongRunAverageOperatorFormula.cpp | 4 ++
src/logic/LongRunAverageOperatorFormula.h | 2 +
src/logic/NextFormula.cpp | 4 ++
src/logic/NextFormula.h | 2 +
src/logic/OperatorFormula.h | 2 +-
src/logic/ProbabilityOperatorFormula.cpp | 4 ++
src/logic/ProbabilityOperatorFormula.h | 2 +
src/logic/ReachabilityRewardFormula.cpp | 4 ++
src/logic/ReachabilityRewardFormula.h | 2 +
src/logic/RewardOperatorFormula.cpp | 4 ++
src/logic/RewardOperatorFormula.h | 2 +
src/logic/UnaryBooleanStateFormula.cpp | 4 ++
src/logic/UnaryBooleanStateFormula.h | 2 +
src/logic/UnaryPathFormula.h | 2 +-
src/logic/UntilFormula.cpp | 4 ++
src/logic/UntilFormula.h | 2 +
src/parser/ExpressionParser.cpp | 4 +-
src/storage/prism/Program.cpp | 11 +++
src/storage/prism/Program.h | 7 ++
src/utility/storm.h | 12 ++--
.../builder/DdPrismModelBuilderTest.cpp | 64 ++++++++---------
.../GmmxxHybridCtmcCslModelCheckerTest.cpp | 16 ++---
.../GmmxxHybridDtmcPrctlModelCheckerTest.cpp | 12 ++--
.../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 8 +--
.../NativeHybridCtmcCslModelCheckerTest.cpp | 16 ++---
.../NativeHybridDtmcPrctlModelCheckerTest.cpp | 12 ++--
.../NativeHybridMdpPrctlModelCheckerTest.cpp | 8 +--
.../SymbolicDtmcPrctlModelCheckerTest.cpp | 12 ++--
.../SymbolicMdpPrctlModelCheckerTest.cpp | 8 +--
test/functional/utility/GraphTest.cpp | 16 ++---
.../SymbolicDtmcPrctlModelCheckerTest.cpp | 8 +--
.../SymbolicMdpPrctlModelCheckerTest.cpp | 72 +++++++++++++++++--
62 files changed, 418 insertions(+), 189 deletions(-)
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 59fc4bbd7..20929afc7 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -190,18 +190,18 @@ namespace storm {
};
template <storm::dd::DdType Type, typename ValueType>
- DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
+ DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), 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>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
+ DdPrismModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), 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& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
+ DdPrismModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
this->buildAllLabels = true;
@@ -241,15 +241,6 @@ namespace storm {
}
labelsToBuild.get().insert(formula.get()->getLabel());
}
-
- // Extract all the expressions used in the formula.
- std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> atomicExpressionFormulas = formula.getAtomicExpressionFormulas();
- for (auto const& formula : atomicExpressionFormulas) {
- if (!expressionLabels) {
- expressionLabels = std::vector<storm::expressions::Expression>();
- }
- expressionLabels.get().push_back(formula.get()->getExpression());
- }
}
template <storm::dd::DdType Type, typename ValueType>
@@ -992,18 +983,21 @@ namespace storm {
return storm::models::symbolic::StandardRewardModel<Type, double>(stateRewards, stateActionRewards, transitionRewards);
}
+ template <storm::dd::DdType Type, typename ValueType>
+ storm::prism::Program const& DdPrismModelBuilder<Type, ValueType>::getTranslatedProgram() const {
+ return preparedProgram.get();
+ }
+
template <storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdPrismModelBuilder<Type, ValueType>::translateProgram(storm::prism::Program const& program, Options const& options) {
- // There might be nondeterministic variables. In that case the program must be prepared before translating.
- storm::prism::Program preparedProgram;
if (options.constantDefinitions) {
preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get());
} else {
preparedProgram = program;
}
- if (preparedProgram.hasUndefinedConstants()) {
- std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram.getUndefinedConstants();
+ if (preparedProgram->hasUndefinedConstants()) {
+ std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram->getUndefinedConstants();
std::stringstream stream;
bool printComma = false;
for (auto const& constant : undefinedConstants) {
@@ -1018,13 +1012,13 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
}
- preparedProgram = preparedProgram.substituteConstants();
+ preparedProgram = preparedProgram->substituteConstants();
- STORM_LOG_DEBUG("Building representation of program:" << std::endl << preparedProgram << std::endl);
+ 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);
+ GenerationInformation generationInfo(*preparedProgram);
SystemResult system = createSystemDecisionDiagram(generationInfo);
storm::dd::Add<Type, ValueType> transitionMatrix = system.allTransitionsDd;
@@ -1034,6 +1028,8 @@ namespace storm {
// If we were asked to treat some states as terminal states, we cut away their transitions now.
if (options.terminalStates || options.negatedTerminalStates) {
+ std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = preparedProgram->getConstantsSubstitution();
+
storm::dd::Bdd<Type> terminalStatesBdd = generationInfo.manager->getBddZero();
if (options.terminalStates) {
storm::expressions::Expression terminalExpression;
@@ -1041,23 +1037,29 @@ namespace storm {
terminalExpression = boost::get<storm::expressions::Expression>(options.terminalStates.get());
} else {
std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
- terminalExpression = preparedProgram.getLabelExpression(labelName);
+ terminalExpression = preparedProgram->getLabelExpression(labelName);
}
+ // If the expression refers to constants of the model, we need to substitute them.
+ terminalExpression = terminalExpression.substitute(constantsSubstitution);
+
STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
terminalStatesBdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression).toBdd();
}
if (options.negatedTerminalStates) {
- storm::expressions::Expression nonTerminalExpression;
+ storm::expressions::Expression negatedTerminalExpression;
if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) {
- nonTerminalExpression = boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
+ negatedTerminalExpression = boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
} else {
std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
- nonTerminalExpression = preparedProgram.getLabelExpression(labelName);
+ negatedTerminalExpression = preparedProgram->getLabelExpression(labelName);
}
- STORM_LOG_TRACE("Making the states *not* satisfying " << nonTerminalExpression << " terminal.");
- terminalStatesBdd |= !generationInfo.rowExpressionAdapter->translateExpression(nonTerminalExpression).toBdd();
+ // If the expression refers to constants of the model, we need to substitute them.
+ negatedTerminalExpression = negatedTerminalExpression.substitute(constantsSubstitution);
+
+ STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal.");
+ terminalStatesBdd |= !generationInfo.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd();
}
transitionMatrix *= (!terminalStatesBdd).template toAdd<ValueType>();
@@ -1116,18 +1118,18 @@ namespace storm {
// 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 << "'.");
+ 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()) {
+ 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));
+ 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;
@@ -1137,7 +1139,7 @@ namespace storm {
// Build the labels that can be accessed as a shortcut.
std::map<std::string, storm::expressions::Expression> labelToExpressionMapping;
- for (auto const& label : preparedProgram.getLabels()) {
+ for (auto const& label : preparedProgram->getLabels()) {
labelToExpressionMapping.emplace(label.getName(), label.getStatePredicateExpression());
}
diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h
index 92be0edeb..1ee9e5168 100644
--- a/src/builder/DdPrismModelBuilder.h
+++ b/src/builder/DdPrismModelBuilder.h
@@ -4,19 +4,13 @@
#include <map>
#include <boost/optional.hpp>
+#include "src/storage/prism/Program.h"
+
#include "src/logic/Formulas.h"
#include "src/adapters/AddExpressionAdapter.h"
#include "src/utility/macros.h"
namespace storm {
- namespace prism {
- class Program;
- class Module;
- class RewardModel;
- class Update;
- class Command;
- }
-
namespace dd {
template<storm::dd::DdType T> class Bdd;
}
@@ -99,9 +93,6 @@ namespace storm {
// An optional set of labels that, if given, restricts the labels that are built.
boost::optional<std::set<std::string>> labelsToBuild;
- // An optional set of expressions for which labels need to be built.
- boost::optional<std::vector<storm::expressions::Expression>> expressionLabels;
-
// An optional expression or label that (a subset of) characterizes the terminal states of the model.
// If this is set, the outgoing transitions of these states are replaced with a self-loop.
boost::optional<boost::variant<storm::expressions::Expression, std::string>> terminalStates;
@@ -118,7 +109,15 @@ namespace storm {
* @param program The program to translate.
* @return A pointer to the resulting model.
*/
- static std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> translateProgram(storm::prism::Program const& program, Options const& options = Options());
+ std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> translateProgram(storm::prism::Program const& program, Options const& options = Options());
+
+ /*!
+ * Retrieves the program that was actually translated (i.e. including constant substitutions etc.). Note
+ * that this function may only be called after a succesful translation.
+ *
+ * @return The translated program.
+ */
+ storm::prism::Program const& getTranslatedProgram() const;
private:
// This structure can store the decision diagrams representing a particular action.
@@ -246,6 +245,8 @@ namespace storm {
static storm::dd::Bdd<Type> computeReachableStates(GenerationInformation& generationInfo, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& transitions);
+ // This member holds the program that was most recently translated (if any).
+ boost::optional<storm::prism::Program> preparedProgram;
};
} // namespace adapters
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index 4f6117c9c..e82f20ff4 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -215,18 +215,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::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);
- }
+ constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
}
template <typename ValueType, typename RewardModelType, typename IndexType>
@@ -235,10 +224,14 @@ namespace storm {
return stateInformation.get();
}
+ template <typename ValueType, typename RewardModelType, typename IndexType>
+ storm::prism::Program const& ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getTranslatedProgram() const {
+ return preparedProgram.get();
+ }
+
template <typename ValueType, typename RewardModelType, typename IndexType>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::translateProgram(storm::prism::Program program, Options const& options) {
// Start by defining the undefined constants in the model.
- storm::prism::Program preparedProgram;
if (options.constantDefinitions) {
preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get());
} else {
@@ -249,11 +242,11 @@ namespace storm {
#ifdef STORM_HAVE_CARL
// If the program either has undefined constants or we are building a parametric model, but the parameters
// not only appear in the probabilities, we re
- if (!std::is_same<ValueType, storm::RationalFunction>::value && preparedProgram.hasUndefinedConstants()) {
+ if (!std::is_same<ValueType, storm::RationalFunction>::value && preparedProgram->hasUndefinedConstants()) {
#else
if (preparedProgram.hasUndefinedConstants()) {
#endif
- std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram.getUndefinedConstants();
+ std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram->getUndefinedConstants();
std::stringstream stream;
bool printComma = false;
for (auto const& constant : undefinedConstants) {
@@ -267,7 +260,7 @@ namespace storm {
stream << ".";
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
#ifdef STORM_HAVE_CARL
- } else if (std::is_same<ValueType, storm::RationalFunction>::value && !preparedProgram.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
+ } else if (std::is_same<ValueType, storm::RationalFunction>::value && !preparedProgram->hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted.");
#endif
}
@@ -275,48 +268,50 @@ 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) {
if (!options.buildAllLabels) {
- preparedProgram.filterLabels(options.labelsToBuild.get());
+ preparedProgram->filterLabels(options.labelsToBuild.get());
}
}
// If we need to build labels for expressions that may appear in some formula, we need to add appropriate
// labels to the program.
if (options.expressionLabels) {
+ std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = preparedProgram->getConstantsSubstitution();
+
for (auto const& expression : options.expressionLabels.get()) {
std::stringstream stream;
- stream << expression;
+ stream << expression.substitute(constantsSubstitution);
std::string name = stream.str();
- if (!preparedProgram.hasLabel(name)) {
- preparedProgram.addLabel(name, expression);
+ if (!preparedProgram->hasLabel(name)) {
+ preparedProgram->addLabel(name, expression);
}
}
}
// Now that the program is fixed, we we need to substitute all constants with their concrete value.
- preparedProgram = preparedProgram.substituteConstants();
+ preparedProgram = preparedProgram->substituteConstants();
- STORM_LOG_DEBUG("Building representation of program:" << std::endl << 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 << "'.");
+ 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()) {
+ 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));
+ 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);
+ ModelComponents modelComponents = buildModelComponents(*preparedProgram, selectedRewardModels, options);
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> result;
switch (program.getModelType()) {
diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h
index dfab62136..31b8e03b7 100644
--- a/src/builder/ExplicitPrismModelBuilder.h
+++ b/src/builder/ExplicitPrismModelBuilder.h
@@ -248,6 +248,14 @@ namespace storm {
*/
StateInformation const& getStateInformation() const;
+ /*!
+ * Retrieves the program that was actually translated (i.e. including constant substitutions etc.). Note
+ * that this function may only be called after a succesful translation.
+ *
+ * @return The translated program.
+ */
+ storm::prism::Program const& getTranslatedProgram() const;
+
private:
static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator);
@@ -350,6 +358,9 @@ namespace storm {
// This member holds information about reachable states that can be retrieved from the outside after a
// successful build.
boost::optional<StateInformation> stateInformation;
+
+ // This member holds the program that was most recently translated (if any).
+ boost::optional<storm::prism::Program> preparedProgram;
};
} // namespace adapters
diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index 47a7857d4..550c3a5da 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -112,31 +112,47 @@ namespace storm {
template<typename ValueType, storm::dd::DdType LibraryType>
void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
- std::shared_ptr<storm::models::ModelBase> model = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
- STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
+ std::pair<std::shared_ptr<storm::models::ModelBase>, storm::prism::Program> modelProgramPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
+ STORM_LOG_THROW(modelProgramPair.first != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
// Preprocess the model if needed.
- BRANCH_ON_MODELTYPE(model, model, ValueType, LibraryType, preprocessModel, formulas);
+ BRANCH_ON_MODELTYPE(modelProgramPair.first, modelProgramPair.first, ValueType, LibraryType, preprocessModel, formulas);
// Print some information about the model.
- model->printModelInformationToStream(std::cout);
+ modelProgramPair.first->printModelInformationToStream(std::cout);
// Verify the model, if a formula was given.
if (!formulas.empty()) {
- if (model->isSparseModel()) {
+ // There may be constants of the model appearing in the formulas, so we replace all their occurrences
+ // by their definitions in the translated program.
+
+ // Start by building a mapping from constants of the (translated) model to their defining expressions.
+ std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
+ for (auto const& constant : modelProgramPair.second.getConstants()) {
+ if (constant.isDefined()) {
+ constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
+ }
+ }
+
+ std::vector<std::shared_ptr<storm::logic::Formula>> preparedFormulas;
+ for (auto const& formula : formulas) {
+ preparedFormulas.emplace_back(formula->substitute(constantSubstitution));
+ }
+
+ if (modelProgramPair.first->isSparseModel()) {
if(storm::settings::generalSettings().isCounterexampleSet()) {
// If we were requested to generate a counterexample, we now do so for each formula.
- for(auto const& formula : formulas) {
- generateCounterexample<ValueType>(program, model->as<storm::models::sparse::Model<ValueType>>(), formula);
+ for(auto const& formula : preparedFormulas) {
+ generateCounterexample<ValueType>(program, modelProgramPair.first->as<storm::models::sparse::Model<ValueType>>(), formula);
}
} else {
- verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas);
+ verifySparseModel<ValueType>(modelProgramPair.first->as<storm::models::sparse::Model<ValueType>>(), preparedFormulas);
}
- } else if (model->isSymbolicModel()) {
+ } else if (modelProgramPair.first->isSymbolicModel()) {
if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
- verifySymbolicModelWithHybridEngine(model->as<storm::models::symbolic::Model<LibraryType>>(), formulas);
+ verifySymbolicModelWithHybridEngine(modelProgramPair.first->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
} else {
- verifySymbolicModelWithSymbolicEngine(model->as<storm::models::symbolic::Model<LibraryType>>(), formulas);
+ verifySymbolicModelWithSymbolicEngine(modelProgramPair.first->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
diff --git a/src/logic/AtomicExpressionFormula.cpp b/src/logic/AtomicExpressionFormula.cpp
index 7f3a26b2c..6747d2ab5 100644
--- a/src/logic/AtomicExpressionFormula.cpp
+++ b/src/logic/AtomicExpressionFormula.cpp
@@ -29,7 +29,11 @@ namespace storm {
void AtomicExpressionFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
atomicExpressionFormulas.push_back(std::dynamic_pointer_cast<AtomicExpressionFormula const>(this->shared_from_this()));
}
-
+
+ std::shared_ptr<Formula> AtomicExpressionFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<AtomicExpressionFormula>(this->expression.substitute(substitution));
+ }
+
std::ostream& AtomicExpressionFormula::writeToStream(std::ostream& out) const {
out << expression;
return out;
diff --git a/src/logic/AtomicExpressionFormula.h b/src/logic/AtomicExpressionFormula.h
index 61fa50aa2..f054c9e42 100644
--- a/src/logic/AtomicExpressionFormula.h
+++ b/src/logic/AtomicExpressionFormula.h
@@ -2,7 +2,6 @@
#define STORM_LOGIC_ATOMICEXPRESSIONFORMULA_H_
#include "src/logic/StateFormula.h"
-#include "src/storage/expressions/Expression.h"
namespace storm {
namespace logic {
@@ -26,6 +25,8 @@ namespace storm {
virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
private:
// The atomic expression represented by this node in the formula tree.
storm::expressions::Expression expression;
diff --git a/src/logic/AtomicLabelFormula.cpp b/src/logic/AtomicLabelFormula.cpp
index 01ceb0d44..0555ff56a 100644
--- a/src/logic/AtomicLabelFormula.cpp
+++ b/src/logic/AtomicLabelFormula.cpp
@@ -30,6 +30,10 @@ namespace storm {
atomicExpressionFormulas.push_back(std::dynamic_pointer_cast<AtomicLabelFormula const>(this->shared_from_this()));
}
+ std::shared_ptr<Formula> AtomicLabelFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<AtomicLabelFormula>(*this);
+ }
+
std::ostream& AtomicLabelFormula::writeToStream(std::ostream& out) const {
out << "\"" << label << "\"";
return out;
diff --git a/src/logic/AtomicLabelFormula.h b/src/logic/AtomicLabelFormula.h
index 554de08df..8cd2f51f1 100644
--- a/src/logic/AtomicLabelFormula.h
+++ b/src/logic/AtomicLabelFormula.h
@@ -25,8 +25,10 @@ namespace storm {
virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
- virtual std::ostream& writeToStream(std::ostream& out) const override;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+ virtual std::ostream& writeToStream(std::ostream& out) const override;
+
private:
std::string label;
};
diff --git a/src/logic/BinaryBooleanStateFormula.cpp b/src/logic/BinaryBooleanStateFormula.cpp
index 70f2e9287..521869129 100644
--- a/src/logic/BinaryBooleanStateFormula.cpp
+++ b/src/logic/BinaryBooleanStateFormula.cpp
@@ -26,6 +26,10 @@ namespace storm {
return this->getOperator() == OperatorType::Or;
}
+ std::shared_ptr<Formula> BinaryBooleanStateFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<BinaryBooleanStateFormula>(this->operatorType, this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution));
+ }
+
std::ostream& BinaryBooleanStateFormula::writeToStream(std::ostream& out) const {
out << "(";
this->getLeftSubformula().writeToStream(out);
diff --git a/src/logic/BinaryBooleanStateFormula.h b/src/logic/BinaryBooleanStateFormula.h
index 5e77bbf88..23a330ae0 100644
--- a/src/logic/BinaryBooleanStateFormula.h
+++ b/src/logic/BinaryBooleanStateFormula.h
@@ -1,6 +1,8 @@
#ifndef STORM_LOGIC_BINARYBOOLEANSTATEFORMULA_H_
#define STORM_LOGIC_BINARYBOOLEANSTATEFORMULA_H_
+#include <map>
+
#include "src/logic/BinaryStateFormula.h"
namespace storm {
@@ -26,6 +28,8 @@ namespace storm {
virtual std::ostream& writeToStream(std::ostream& out) const override;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
private:
OperatorType operatorType;
};
diff --git a/src/logic/BinaryPathFormula.h b/src/logic/BinaryPathFormula.h
index 9f2278132..928d21728 100644
--- a/src/logic/BinaryPathFormula.h
+++ b/src/logic/BinaryPathFormula.h
@@ -33,7 +33,7 @@ namespace storm {
virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
-
+
private:
std::shared_ptr<Formula const> leftSubformula;
std::shared_ptr<Formula const> rightSubformula;
diff --git a/src/logic/BooleanLiteralFormula.cpp b/src/logic/BooleanLiteralFormula.cpp
index 5d3fe0c49..aa78a6772 100644
--- a/src/logic/BooleanLiteralFormula.cpp
+++ b/src/logic/BooleanLiteralFormula.cpp
@@ -30,6 +30,10 @@ namespace storm {
return true;
}
+ std::shared_ptr<Formula> BooleanLiteralFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<BooleanLiteralFormula>(*this);
+ }
+
std::ostream& BooleanLiteralFormula::writeToStream(std::ostream& out) const {
if (value) {
out << "true";
diff --git a/src/logic/BooleanLiteralFormula.h b/src/logic/BooleanLiteralFormula.h
index 491ecdaa3..d8df08651 100644
--- a/src/logic/BooleanLiteralFormula.h
+++ b/src/logic/BooleanLiteralFormula.h
@@ -21,8 +21,10 @@ namespace storm {
virtual bool isLtlFormula() const override;
virtual bool isPropositionalFormula() const override;
- virtual std::ostream& writeToStream(std::ostream& out) const override;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+ virtual std::ostream& writeToStream(std::ostream& out) const override;
+
private:
bool value;
};
diff --git a/src/logic/BoundedUntilFormula.cpp b/src/logic/BoundedUntilFormula.cpp
index be9ea4f9b..2c7ed2cde 100644
--- a/src/logic/BoundedUntilFormula.cpp
+++ b/src/logic/BoundedUntilFormula.cpp
@@ -14,6 +14,10 @@ namespace storm {
// Intentionally left empty.
}
+ BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::variant<uint_fast64_t, std::pair<double, double>> const& bounds) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(bounds) {
+ // Intentionally left empty.
+ }
+
bool BoundedUntilFormula::isBoundedUntilFormula() const {
return true;
}
@@ -42,6 +46,10 @@ namespace storm {
return boost::get<uint_fast64_t>(bounds);
}
+ std::shared_ptr<Formula> BoundedUntilFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<BoundedUntilFormula>(this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution), bounds);
+ }
+
std::ostream& BoundedUntilFormula::writeToStream(std::ostream& out) const {
this->getLeftSubformula().writeToStream(out);
diff --git a/src/logic/BoundedUntilFormula.h b/src/logic/BoundedUntilFormula.h
index ffb0f0d32..4d72abdc1 100644
--- a/src/logic/BoundedUntilFormula.h
+++ b/src/logic/BoundedUntilFormula.h
@@ -11,6 +11,7 @@ namespace storm {
public:
BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, double lowerBound, double upperBound);
BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, uint_fast64_t upperBound);
+ BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::variant<uint_fast64_t, std::pair<double, double>> const& bounds);
virtual bool isBoundedUntilFormula() const override;
@@ -26,6 +27,8 @@ namespace storm {
virtual std::ostream& writeToStream(std::ostream& out) const override;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
private:
boost::variant<uint_fast64_t, std::pair<double, double>> bounds;
};
diff --git a/src/logic/ConditionalPathFormula.cpp b/src/logic/ConditionalPathFormula.cpp
index c1e7078b2..b5d8af81d 100644
--- a/src/logic/ConditionalPathFormula.cpp
+++ b/src/logic/ConditionalPathFormula.cpp
@@ -10,6 +10,10 @@ namespace storm {
return true;
}
+ std::shared_ptr<Formula> ConditionalPathFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<ConditionalPathFormula>(this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution));
+ }
+
std::ostream& ConditionalPathFormula::writeToStream(std::ostream& out) const {
this->getLeftSubformula().writeToStream(out);
out << " || ";
diff --git a/src/logic/ConditionalPathFormula.h b/src/logic/ConditionalPathFormula.h
index 9cbfa7ccc..bd5f3852c 100644
--- a/src/logic/ConditionalPathFormula.h
+++ b/src/logic/ConditionalPathFormula.h
@@ -16,6 +16,8 @@ namespace storm {
virtual bool isConditionalPathFormula() const override;
virtual std::ostream& writeToStream(std::ostream& out) const override;
+
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
};
}
}
diff --git a/src/logic/CumulativeRewardFormula.cpp b/src/logic/CumulativeRewardFormula.cpp
index ef1dde50e..ed4b18c85 100644
--- a/src/logic/CumulativeRewardFormula.cpp
+++ b/src/logic/CumulativeRewardFormula.cpp
@@ -34,6 +34,10 @@ namespace storm {
}
}
+ std::shared_ptr<Formula> CumulativeRewardFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<CumulativeRewardFormula>(*this);
+ }
+
std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const {
if (this->hasDiscreteTimeBound()) {
out << "C<=" << this->getDiscreteTimeBound();
diff --git a/src/logic/CumulativeRewardFormula.h b/src/logic/CumulativeRewardFormula.h
index d48df1ac4..8b8692743 100644
--- a/src/logic/CumulativeRewardFormula.h
+++ b/src/logic/CumulativeRewardFormula.h
@@ -29,6 +29,8 @@ namespace storm {
double getContinuousTimeBound() const;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
private:
boost::variant<uint_fast64_t, double> timeBound;
};
diff --git a/src/logic/EventuallyFormula.cpp b/src/logic/EventuallyFormula.cpp
index 30ca7fabe..b8ea1aa35 100644
--- a/src/logic/EventuallyFormula.cpp
+++ b/src/logic/EventuallyFormula.cpp
@@ -10,6 +10,10 @@ namespace storm {
return true;
}
+ std::shared_ptr<Formula> EventuallyFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<EventuallyFormula>(this->getSubformula().substitute(substitution));
+ }
+
std::ostream& EventuallyFormula::writeToStream(std::ostream& out) const {
out << "F ";
this->getSubformula().writeToStream(out);
diff --git a/src/logic/EventuallyFormula.h b/src/logic/EventuallyFormula.h
index cf8a09e38..816f93c82 100644
--- a/src/logic/EventuallyFormula.h
+++ b/src/logic/EventuallyFormula.h
@@ -16,6 +16,9 @@ namespace storm {
virtual bool isEventuallyFormula() const override;
virtual std::ostream& writeToStream(std::ostream& out) const override;
+
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
};
}
}
diff --git a/src/logic/ExpectedTimeOperatorFormula.cpp b/src/logic/ExpectedTimeOperatorFormula.cpp
index 2b0cdcb70..98ed6d8cc 100644
--- a/src/logic/ExpectedTimeOperatorFormula.cpp
+++ b/src/logic/ExpectedTimeOperatorFormula.cpp
@@ -38,6 +38,10 @@ namespace storm {
// Intentionally left empty.
}
+ std::shared_ptr<Formula> ExpectedTimeOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<ExpectedTimeOperatorFormula>(this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution));
+ }
+
std::ostream& ExpectedTimeOperatorFormula::writeToStream(std::ostream& out) const {
out << "ET";
OperatorFormula::writeToStream(out);
diff --git a/src/logic/ExpectedTimeOperatorFormula.h b/src/logic/ExpectedTimeOperatorFormula.h
index 8be07520d..b9b6d57ee 100644
--- a/src/logic/ExpectedTimeOperatorFormula.h
+++ b/src/logic/ExpectedTimeOperatorFormula.h
@@ -23,6 +23,8 @@ namespace storm {
virtual bool containsProbabilityOperator() const override;
virtual bool containsNestedProbabilityOperators() const override;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
virtual std::ostream& writeToStream(std::ostream& out) const override;
};
}
diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp
index e621c1c78..8f96b19cd 100644
--- a/src/logic/Formula.cpp
+++ b/src/logic/Formula.cpp
@@ -404,7 +404,7 @@ namespace storm {
void Formula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
return;
}
-
+
std::string Formula::toString() const {
std::stringstream str2;
writeToStream(str2);
diff --git a/src/logic/Formula.h b/src/logic/Formula.h
index 4d831e456..98b1ac349 100644
--- a/src/logic/Formula.h
+++ b/src/logic/Formula.h
@@ -6,6 +6,9 @@
#include <iostream>
#include <set>
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/expressions/Expression.h"
+
namespace storm {
namespace logic {
// Forward-declare all formula classes.
@@ -174,6 +177,8 @@ namespace storm {
std::shared_ptr<Formula const> asSharedPointer();
std::shared_ptr<Formula const> asSharedPointer() const;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const = 0;
+
std::string toString() const;
virtual std::ostream& writeToStream(std::ostream& out) const = 0;
diff --git a/src/logic/GloballyFormula.cpp b/src/logic/GloballyFormula.cpp
index f4f6935dd..8d2d1c92a 100644
--- a/src/logic/GloballyFormula.cpp
+++ b/src/logic/GloballyFormula.cpp
@@ -10,6 +10,10 @@ namespace storm {
return true;
}
+ std::shared_ptr<Formula> GloballyFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<GloballyFormula>(this->getSubformula().substitute(substitution));
+ }
+
std::ostream& GloballyFormula::writeToStream(std::ostream& out) const {
out << "G ";
this->getSubformula().writeToStream(out);
diff --git a/src/logic/GloballyFormula.h b/src/logic/GloballyFormula.h
index 043a9849e..6346200c8 100644
--- a/src/logic/GloballyFormula.h
+++ b/src/logic/GloballyFormula.h
@@ -15,6 +15,8 @@ namespace storm {
virtual bool isGloballyFormula() const override;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
virtual std::ostream& writeToStream(std::ostream& out) const override;
};
}
diff --git a/src/logic/InstantaneousRewardFormula.cpp b/src/logic/InstantaneousRewardFormula.cpp
index 579b88413..7d81f1234 100644
--- a/src/logic/InstantaneousRewardFormula.cpp
+++ b/src/logic/InstantaneousRewardFormula.cpp
@@ -34,6 +34,10 @@ namespace storm {
}
}
+ std::shared_ptr<Formula> InstantaneousRewardFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<InstantaneousRewardFormula>(*this);
+ }
+
std::ostream& InstantaneousRewardFormula::writeToStream(std::ostream& out) const {
if (this->hasDiscreteTimeBound()) {
out << "I=" << this->getDiscreteTimeBound();
diff --git a/src/logic/InstantaneousRewardFormula.h b/src/logic/InstantaneousRewardFormula.h
index 21e605494..8b29fa740 100644
--- a/src/logic/InstantaneousRewardFormula.h
+++ b/src/logic/InstantaneousRewardFormula.h
@@ -29,6 +29,8 @@ namespace storm {
double getContinuousTimeBound() const;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
private:
boost::variant<uint_fast64_t, double> timeBound;
};
diff --git a/src/logic/LongRunAverageOperatorFormula.cpp b/src/logic/LongRunAverageOperatorFormula.cpp
index c540c9577..d72317b7d 100644
--- a/src/logic/LongRunAverageOperatorFormula.cpp
+++ b/src/logic/LongRunAverageOperatorFormula.cpp
@@ -38,6 +38,10 @@ namespace storm {
// Intentionally left empty.
}
+ std::shared_ptr<Formula> LongRunAverageOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<LongRunAverageOperatorFormula>(this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution));
+ }
+
std::ostream& LongRunAverageOperatorFormula::writeToStream(std::ostream& out) const {
out << "LRA";
OperatorFormula::writeToStream(out);
diff --git a/src/logic/LongRunAverageOperatorFormula.h b/src/logic/LongRunAverageOperatorFormula.h
index ddc8118a9..161823314 100644
--- a/src/logic/LongRunAverageOperatorFormula.h
+++ b/src/logic/LongRunAverageOperatorFormula.h
@@ -23,6 +23,8 @@ namespace storm {
virtual bool containsProbabilityOperator() const override;
virtual bool containsNestedProbabilityOperators() const override;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
virtual std::ostream& writeToStream(std::ostream& out) const override;
};
}
diff --git a/src/logic/NextFormula.cpp b/src/logic/NextFormula.cpp
index 4bdf98d1f..b5064253f 100644
--- a/src/logic/NextFormula.cpp
+++ b/src/logic/NextFormula.cpp
@@ -14,6 +14,10 @@ namespace storm {
return true;
}
+ std::shared_ptr<Formula> NextFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<NextFormula>(this->getSubformula().substitute(substitution));
+ }
+
std::ostream& NextFormula::writeToStream(std::ostream& out) const {
out << "X ";
this->getSubformula().writeToStream(out);
diff --git a/src/logic/NextFormula.h b/src/logic/NextFormula.h
index 179185f48..2466d0b3d 100644
--- a/src/logic/NextFormula.h
+++ b/src/logic/NextFormula.h
@@ -17,6 +17,8 @@ namespace storm {
virtual bool containsNextFormula() const override;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
virtual std::ostream& writeToStream(std::ostream& out) const override;
};
}
diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h
index c849b0a41..8bdc14d21 100644
--- a/src/logic/OperatorFormula.h
+++ b/src/logic/OperatorFormula.h
@@ -25,7 +25,7 @@ namespace storm {
virtual std::ostream& writeToStream(std::ostream& out) const override;
- private:
+ protected:
std::string operatorSymbol;
boost::optional<ComparisonType> comparisonType;
boost::optional<double> bound;
diff --git a/src/logic/ProbabilityOperatorFormula.cpp b/src/logic/ProbabilityOperatorFormula.cpp
index 93426262b..e6cde140d 100644
--- a/src/logic/ProbabilityOperatorFormula.cpp
+++ b/src/logic/ProbabilityOperatorFormula.cpp
@@ -46,6 +46,10 @@ namespace storm {
// Intentionally left empty.
}
+ std::shared_ptr<Formula> ProbabilityOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<ProbabilityOperatorFormula>(this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution));
+ }
+
std::ostream& ProbabilityOperatorFormula::writeToStream(std::ostream& out) const {
out << "P";
OperatorFormula::writeToStream(out);
diff --git a/src/logic/ProbabilityOperatorFormula.h b/src/logic/ProbabilityOperatorFormula.h
index 1ccbb3985..7f30dd92d 100644
--- a/src/logic/ProbabilityOperatorFormula.h
+++ b/src/logic/ProbabilityOperatorFormula.h
@@ -25,6 +25,8 @@ namespace storm {
virtual bool isProbabilityOperatorFormula() const override;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
virtual std::ostream& writeToStream(std::ostream& out) const override;
};
}
diff --git a/src/logic/ReachabilityRewardFormula.cpp b/src/logic/ReachabilityRewardFormula.cpp
index 4312dc72c..83ba52f91 100644
--- a/src/logic/ReachabilityRewardFormula.cpp
+++ b/src/logic/ReachabilityRewardFormula.cpp
@@ -22,6 +22,10 @@ namespace storm {
this->getSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
}
+ std::shared_ptr<Formula> ReachabilityRewardFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<ReachabilityRewardFormula>(this->getSubformula().substitute(substitution));
+ }
+
std::ostream& ReachabilityRewardFormula::writeToStream(std::ostream& out) const {
out << "F ";
this->getSubformula().writeToStream(out);
diff --git a/src/logic/ReachabilityRewardFormula.h b/src/logic/ReachabilityRewardFormula.h
index 064b9acb2..bfef88188 100644
--- a/src/logic/ReachabilityRewardFormula.h
+++ b/src/logic/ReachabilityRewardFormula.h
@@ -25,6 +25,8 @@ namespace storm {
virtual std::ostream& writeToStream(std::ostream& out) const override;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
private:
std::shared_ptr<Formula const> subformula;
};
diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp
index 32899d021..627263d36 100644
--- a/src/logic/RewardOperatorFormula.cpp
+++ b/src/logic/RewardOperatorFormula.cpp
@@ -59,6 +59,10 @@ namespace storm {
// Intentionally left empty.
}
+ std::shared_ptr<Formula> RewardOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<RewardOperatorFormula>(this->rewardModelName, this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution));
+ }
+
std::ostream& RewardOperatorFormula::writeToStream(std::ostream& out) const {
out << "R";
if (this->hasRewardModelName()) {
diff --git a/src/logic/RewardOperatorFormula.h b/src/logic/RewardOperatorFormula.h
index 82e2d74f0..37287c6e8 100644
--- a/src/logic/RewardOperatorFormula.h
+++ b/src/logic/RewardOperatorFormula.h
@@ -50,6 +50,8 @@ namespace storm {
*/
std::string const& getRewardModelName() const;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
private:
// The (optional) name of the reward model this property refers to.
boost::optional<std::string> rewardModelName;
diff --git a/src/logic/UnaryBooleanStateFormula.cpp b/src/logic/UnaryBooleanStateFormula.cpp
index 926b56037..ec9a4ff0a 100644
--- a/src/logic/UnaryBooleanStateFormula.cpp
+++ b/src/logic/UnaryBooleanStateFormula.cpp
@@ -18,6 +18,10 @@ namespace storm {
return this->getOperator() == OperatorType::Not;
}
+ std::shared_ptr<Formula> UnaryBooleanStateFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<UnaryBooleanStateFormula>(this->operatorType, this->getSubformula().substitute(substitution));
+ }
+
std::ostream& UnaryBooleanStateFormula::writeToStream(std::ostream& out) const {
switch (operatorType) {
case OperatorType::Not: out << "!("; break;
diff --git a/src/logic/UnaryBooleanStateFormula.h b/src/logic/UnaryBooleanStateFormula.h
index 317e89af7..fa0a83023 100644
--- a/src/logic/UnaryBooleanStateFormula.h
+++ b/src/logic/UnaryBooleanStateFormula.h
@@ -20,6 +20,8 @@ namespace storm {
OperatorType getOperator() const;
virtual bool isNot() const;
+
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
virtual std::ostream& writeToStream(std::ostream& out) const override;
diff --git a/src/logic/UnaryPathFormula.h b/src/logic/UnaryPathFormula.h
index a91ffe38f..8d168585c 100644
--- a/src/logic/UnaryPathFormula.h
+++ b/src/logic/UnaryPathFormula.h
@@ -31,7 +31,7 @@ namespace storm {
virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
-
+
private:
std::shared_ptr<Formula const> subformula;
};
diff --git a/src/logic/UntilFormula.cpp b/src/logic/UntilFormula.cpp
index 74893fa68..94d7c62a8 100644
--- a/src/logic/UntilFormula.cpp
+++ b/src/logic/UntilFormula.cpp
@@ -10,6 +10,10 @@ namespace storm {
return true;
}
+ std::shared_ptr<Formula> UntilFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+ return std::make_shared<UntilFormula>(this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution));
+ }
+
std::ostream& UntilFormula::writeToStream(std::ostream& out) const {
this->getLeftSubformula().writeToStream(out);
out << " U ";
diff --git a/src/logic/UntilFormula.h b/src/logic/UntilFormula.h
index a0c80cecf..45a721252 100644
--- a/src/logic/UntilFormula.h
+++ b/src/logic/UntilFormula.h
@@ -15,6 +15,8 @@ namespace storm {
virtual bool isUntilFormula() const override;
+ virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+
virtual std::ostream& writeToStream(std::ostream& out) const override;
};
}
diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp
index 8bb55c625..2647f4f25 100644
--- a/src/parser/ExpressionParser.cpp
+++ b/src/parser/ExpressionParser.cpp
@@ -17,9 +17,9 @@ namespace storm {
floorCeilExpression.name("floor/ceil expression");
if (allowBacktracking) {
- minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) >> iteExpression[qi::_val = qi::_1] >> +(qi::lit(",") >> iteExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_val, qi::_a, qi::_1)]);
+ minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) >> iteExpression[qi::_val = qi::_1] >> +(qi::lit(",") >> iteExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_val, qi::_a, qi::_1)]) >> qi::lit(")");
} else {
- minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] > qi::lit("(")) > iteExpression[qi::_val = qi::_1] > +(qi::lit(",") > iteExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_val, qi::_a, qi::_1)]);
+ minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] > qi::lit("(")) > iteExpression[qi::_val = qi::_1] > +(qi::lit(",") > iteExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_val, qi::_a, qi::_1)]) > qi::lit(")");
}
minMaxExpression.name("min/max expression");
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 3b4be36aa..fc7a7c08c 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -184,6 +184,17 @@ namespace storm {
return this->constants;
}
+ std::map<storm::expressions::Variable, storm::expressions::Expression> Program::getConstantsSubstitution() const {
+ std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution;
+ for (auto const& constant : this->getConstants()) {
+ if (constant.isDefined()) {
+ constantsSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
+ }
+ }
+ return constantsSubstitution;
+ }
+
+
std::size_t Program::getNumberOfConstants() const {
return this->getConstants().size();
}
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index 2917182e6..b4e6d45b5 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -106,6 +106,13 @@ namespace storm {
*/
Constant const& getConstant(std::string const& constantName) const;
+ /*!
+ * Retrieves a mapping of all defined constants to their defining expressions.
+ *
+ * @return A mapping from constants to their 'values'.
+ */
+ std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsSubstitution() const;
+
/*!
* Retrieves all constants defined in the program.
*
diff --git a/src/utility/storm.h b/src/utility/storm.h
index fa2ac1b1e..bf1e2262c 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -83,8 +83,8 @@ namespace storm {
std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
- 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);
+ std::pair<std::shared_ptr<storm::models::ModelBase>, storm::prism::Program> buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+ std::pair<std::shared_ptr<storm::models::ModelBase>, storm::prism::Program> result;
storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
@@ -102,13 +102,17 @@ namespace storm {
options.buildCommandLabels = true;
}
- result = storm::builder::ExplicitPrismModelBuilder<ValueType>().translateProgram(program, options);
+ storm::builder::ExplicitPrismModelBuilder<ValueType> builder;
+ result.first = builder.translateProgram(program, options);
+ result.second = builder.getTranslatedProgram();
} else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options;
options = typename storm::builder::DdPrismModelBuilder<LibraryType>::Options(formulas);
options.addConstantDefinitionsFromString(program, constants);
- result = storm::builder::DdPrismModelBuilder<LibraryType>::translateProgram(program, options);
+ storm::builder::DdPrismModelBuilder<LibraryType> builder;
+ result.first = builder.translateProgram(program, options);
+ result.second = builder.getTranslatedProgram();
}
return result;
diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp
index ac29790e5..102b7fb2a 100644
--- a/test/functional/builder/DdPrismModelBuilderTest.cpp
+++ b/test/functional/builder/DdPrismModelBuilderTest.cpp
@@ -13,27 +13,27 @@
TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(1728ul, model->getNumberOfStates());
EXPECT_EQ(2505ul, model->getNumberOfTransitions());
}
@@ -41,27 +41,27 @@ TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) {
TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(1728ul, model->getNumberOfStates());
EXPECT_EQ(2505ul, model->getNumberOfTransitions());
}
@@ -72,27 +72,27 @@ TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(66ul, model->getNumberOfStates());
EXPECT_EQ(189ul, model->getNumberOfTransitions());
}
@@ -103,34 +103,34 @@ TEST(DdPrismModelBuilderTest_Cudd, Ctmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(66ul, model->getNumberOfStates());
EXPECT_EQ(189ul, model->getNumberOfTransitions());
}
TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -140,7 +140,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(254ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -150,7 +150,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(573ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -160,7 +160,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(400ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -170,7 +170,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -180,7 +180,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -192,7 +192,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -202,7 +202,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(254ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -212,7 +212,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(573ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -222,7 +222,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(400ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -232,7 +232,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -242,7 +242,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
index 7be9c2d98..401402f6e 100644
--- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
@@ -37,7 +37,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
@@ -134,7 +134,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>>();
@@ -231,7 +231,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
@@ -310,7 +310,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>>();
@@ -382,7 +382,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) {
std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model.
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
@@ -418,7 +418,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model.
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>>();
@@ -468,7 +468,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("customers");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
@@ -556,7 +556,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("customers");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>>();
diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
index aec762f2b..bb7c2eb5a 100644
--- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
@@ -32,7 +32,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coin_flips");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
@@ -93,7 +93,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coin_flips");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
@@ -146,7 +146,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) {
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
@@ -190,7 +190,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
@@ -242,7 +242,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
@@ -294,7 +294,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
index 62f4596b3..5b83e5558 100644
--- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
@@ -34,7 +34,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coinflips");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
@@ -131,7 +131,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coinflips");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
@@ -228,7 +228,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(3172ul, model->getNumberOfStates());
EXPECT_EQ(7144ul, model->getNumberOfTransitions());
@@ -307,7 +307,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(3172ul, model->getNumberOfStates());
EXPECT_EQ(7144ul, model->getNumberOfTransitions());
diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
index e4cf97dfe..65a8d4ec2 100644
--- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
@@ -36,7 +36,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
@@ -133,7 +133,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_repairs");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>>();
@@ -230,7 +230,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
@@ -309,7 +309,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("up");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>>();
@@ -381,7 +381,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) {
std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model.
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
@@ -417,7 +417,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model.
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>>();
@@ -467,7 +467,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("customers");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
@@ -557,7 +557,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("customers");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan>>();
diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
index 032066175..559979667 100644
--- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
@@ -33,7 +33,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coin_flips");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
@@ -94,7 +94,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coin_flips");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
@@ -147,7 +147,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) {
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
@@ -191,7 +191,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
@@ -243,7 +243,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
@@ -295,7 +295,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
index 83a1fc2f2..c66c5b6d2 100644
--- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
@@ -32,7 +32,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coinflips");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
@@ -128,7 +128,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coinflips");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
@@ -224,7 +224,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(3172ul, model->getNumberOfStates());
EXPECT_EQ(7144ul, model->getNumberOfTransitions());
@@ -303,7 +303,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(3172ul, model->getNumberOfStates());
EXPECT_EQ(7144ul, model->getNumberOfTransitions());
diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
index a46a33843..b8443686a 100644
--- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
@@ -31,7 +31,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coin_flips");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
@@ -92,7 +92,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coin_flips");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
@@ -146,7 +146,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
@@ -190,7 +190,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
@@ -245,7 +245,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
@@ -297,7 +297,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
diff --git a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
index cb33cea0f..81c02ac38 100644
--- a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
@@ -31,7 +31,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coinflips");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
@@ -128,7 +128,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coinflips");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
@@ -225,7 +225,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(3172ul, model->getNumberOfStates());
EXPECT_EQ(7144ul, model->getNumberOfTransitions());
@@ -304,7 +304,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(3172ul, model->getNumberOfStates());
EXPECT_EQ(7144ul, model->getNumberOfTransitions());
diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp
index b337b0ca9..d209998d7 100644
--- a/test/functional/utility/GraphTest.cpp
+++ b/test/functional/utility/GraphTest.cpp
@@ -17,7 +17,7 @@
TEST(GraphTest, SymbolicProb01_Cudd) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
@@ -38,7 +38,7 @@ TEST(GraphTest, SymbolicProb01_Cudd) {
TEST(GraphTest, SymbolicProb01_Sylvan) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
@@ -59,7 +59,7 @@ TEST(GraphTest, SymbolicProb01_Sylvan) {
TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -76,7 +76,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
}
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -101,7 +101,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
}
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -120,7 +120,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -137,7 +137,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
}
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -162,7 +162,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
}
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
- model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
diff --git a/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
index fafc8101c..4de317610 100644
--- a/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
@@ -31,7 +31,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(131521ul, model->getNumberOfStates());
EXPECT_EQ(164288ul, model->getNumberOfTransitions());
@@ -83,7 +83,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(131521ul, model->getNumberOfStates());
EXPECT_EQ(164288ul, model->getNumberOfTransitions());
@@ -127,7 +127,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(586242ul, model->getNumberOfStates());
EXPECT_EQ(1753883ul, model->getNumberOfTransitions());
@@ -171,7 +171,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program);
EXPECT_EQ(586242ul, model->getNumberOfStates());
EXPECT_EQ(1753883ul, model->getNumberOfTransitions());
diff --git a/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
index f6ad1823f..4b39ad40f 100644
--- a/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
@@ -31,7 +31,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program, options);
EXPECT_EQ(27299ul, model->getNumberOfStates());
EXPECT_EQ(74365ul, model->getNumberOfTransitions());
@@ -83,7 +83,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().translateProgram(program, options);
EXPECT_EQ(27299ul, model->getNumberOfStates());
EXPECT_EQ(74365ul, model->getNumberOfTransitions());
@@ -135,7 +135,11 @@ TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Cudd) {
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("time");
- std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+
+ storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD> builder;
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.translateProgram(program, options);
+ storm::prism::Program translatedProgram = builder.getTranslatedProgram();
+
EXPECT_EQ(1460287ul, model->getNumberOfStates());
EXPECT_EQ(2396727ul, model->getNumberOfTransitions());
@@ -155,13 +159,14 @@ TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Cudd) {
EXPECT_NEAR(0.90468935682619855, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ F (min_backoff_after_success < 4) ]");
+ formula = formula->substitute(translatedProgram.getConstantsSubstitution());
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
- EXPECT_NEAR(0, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
- EXPECT_NEAR(0, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+ EXPECT_NEAR(0.98952073326388401, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+ EXPECT_NEAR(0.98952073326388401, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [ F \"all_delivered\" ]");
@@ -169,6 +174,63 @@ TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Cudd) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
+ EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+ EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+}
+
+TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Sylvan) {
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/csma3_4.nm");
+
+ // A parser that we use for conveniently constructing the formulas.
+ storm::parser::FormulaParser formulaParser(program);
+
+ // Build the die model with its reward model.
+#ifdef WINDOWS
+ storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
+#else
+ typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
+#endif
+ options.buildAllRewardModels = false;
+ options.rewardModelsToBuild.insert("time");
+
+ storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan> builder;
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.translateProgram(program, options);
+ storm::prism::Program translatedProgram = builder.getTranslatedProgram();
+
+ EXPECT_EQ(1460287ul, model->getNumberOfStates());
+ EXPECT_EQ(2396727ul, model->getNumberOfTransitions());
+
+ ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
+
+ std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
+
+ storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
+
+ std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]");
+
+ std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
+ result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+ storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
+
+ EXPECT_NEAR(0.90469132950001963, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+ EXPECT_NEAR(0.90469132950001963, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+
+ formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ F (min_backoff_after_success < 4) ]");
+ formula = formula->substitute(translatedProgram.getConstantsSubstitution());
+
+ result = checker.check(*formula);
+ result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+ storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
+
+ EXPECT_NEAR(0.98952073326388401, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+ EXPECT_NEAR(, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+
+ formula = formulaParser.parseSingleFormulaFromString("Rmin=? [ F \"all_delivered\" ]");
+
+ result = checker.check(*formula);
+ result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+ storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
+
EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
}
\ No newline at end of file