diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp
index 2a89e0662..edb31fda1 100644
--- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp
+++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp
@@ -484,7 +484,7 @@ storm_rational_function_ptr storm_rational_function_divide(storm_rational_functi
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
- *result_srf *= srf_b;
+ *result_srf /= srf_b;
return (storm_rational_function_ptr)result_srf;
}
diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c
index 5008607bf..692a6f607 100644
--- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c
+++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c
@@ -623,7 +623,7 @@ TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_minimum, MTBDD, a) {
if (cache_get3(CACHE_MTBDD_MINIMUM_RN, a, 0, 0, &result)) return result;
/* Call recursive */
- SPAWN(mtbdd_minimum, node_getlow(a, na));
+ SPAWN(sylvan_storm_rational_number_minimum, node_getlow(a, na));
MTBDD high = CALL(sylvan_storm_rational_number_minimum, node_gethigh(a, na));
MTBDD low = SYNC(sylvan_storm_rational_number_minimum);
@@ -656,7 +656,7 @@ TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_maximum, MTBDD, a)
if (cache_get3(CACHE_MTBDD_MAXIMUM_RN, a, 0, 0, &result)) return result;
/* Call recursive */
- SPAWN(mtbdd_minimum, node_getlow(a, na));
+ SPAWN(sylvan_storm_rational_number_maximum, node_getlow(a, na));
MTBDD high = CALL(sylvan_storm_rational_number_maximum, node_gethigh(a, na));
MTBDD low = SYNC(sylvan_storm_rational_number_maximum);
diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
index 4b7a486bb..88c9fac6a 100644
--- a/src/storm/builder/DdJaniModelBuilder.cpp
+++ b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -133,6 +133,65 @@ namespace storm {
labelNames.insert(labelName);
}
+ template <storm::dd::DdType Type, typename ValueType>
+ class ParameterCreator {
+ public:
+ void create(storm::jani::Model const& model, storm::adapters::AddExpressionAdapter<Type, ValueType>& rowExpressionAdapter, storm::adapters::AddExpressionAdapter<Type, ValueType>& columnExpressionAdapter) {
+ // Intentionally left empty: no support for parameters for this data type.
+ }
+
+ std::set<storm::RationalFunctionVariable> const& getParameters() const {
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Creating parameters for non-parametric model is not supported.");
+ }
+
+ private:
+
+ };
+
+ template <storm::dd::DdType Type>
+ class ParameterCreator<Type, storm::RationalFunction> {
+ public:
+ ParameterCreator() : cache(std::make_shared<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>>()) {
+ // Intentionally left empty.
+ }
+
+ void create(storm::jani::Model const& model, storm::adapters::AddExpressionAdapter<Type, storm::RationalFunction>& rowExpressionAdapter, storm::adapters::AddExpressionAdapter<Type, storm::RationalFunction>& columnExpressionAdapter) {
+ for (auto const& constant : model.getConstants()) {
+ if (!constant.isDefined()) {
+ carl::Variable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName());
+ parameters.insert(carlVariable);
+ auto rf = convertVariableToPolynomial(carlVariable);
+ rowExpressionAdapter.setValue(constant.getExpressionVariable(), rf);
+ columnExpressionAdapter.setValue(constant.getExpressionVariable(), rf);
+ }
+ }
+ }
+
+ template<typename RationalFunctionType = storm::RationalFunction, typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
+ RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
+ return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::PolyType::PolyType(variable), cache));
+ }
+
+ template<typename RationalFunctionType = storm::RationalFunction, typename TP = typename RationalFunctionType::PolyType, carl::DisableIf<carl::needs_cache<TP>> = carl::dummy>
+ RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
+ return RationalFunctionType(variable);
+ }
+
+ std::set<storm::RationalFunctionVariable> const& getParameters() const {
+ return parameters;
+ }
+
+ private:
+ // A mapping from our variables to carl's.
+ std::unordered_map<storm::expressions::Variable, carl::Variable> variableToVariableMap;
+
+ // The cache that is used in case the underlying type needs a cache.
+ std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
+
+ // All created parameters.
+ std::set<storm::RationalFunctionVariable> parameters;
+ };
+
template <storm::dd::DdType Type, typename ValueType>
struct CompositionVariables {
CompositionVariables() : manager(std::make_shared<storm::dd::DdManager<Type>>()),
@@ -191,6 +250,9 @@ namespace storm {
// A DD representing the valid ranges of the global variables.
storm::dd::Add<Type, ValueType> globalVariableRanges;
+
+ // The parameters that appear in the model.
+ std::set<storm::RationalFunctionVariable> parameters;
};
// A class responsible for creating the necessary variables for a subsequent composition of automata.
@@ -324,6 +386,12 @@ namespace storm {
result.automatonToRangeMap[automaton.getName()] = (range && globalVariableRanges).template toAdd<ValueType>();
}
+ ParameterCreator<Type, ValueType> parameterCreator;
+ parameterCreator.create(model, *result.rowExpressionAdapter, *result.columnExpressionAdapter);
+ if (std::is_same<ValueType, storm::RationalFunction>::value) {
+ result.parameters = parameterCreator.getParameters();
+ }
+
return result;
}
@@ -1631,16 +1699,22 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> createModel(storm::jani::ModelType const& modelType, CompositionVariables<Type, ValueType> const& variables, ModelComponents<Type, ValueType> const& modelComponents) {
-
+ std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> result;
if (modelType == storm::jani::ModelType::DTMC) {
- return std::make_shared<storm::models::symbolic::Dtmc<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
+ result = std::make_shared<storm::models::symbolic::Dtmc<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
} else if (modelType == storm::jani::ModelType::CTMC) {
- return std::make_shared<storm::models::symbolic::Ctmc<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
+ result = std::make_shared<storm::models::symbolic::Ctmc<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
} else if (modelType == storm::jani::ModelType::MDP) {
- return std::make_shared<storm::models::symbolic::Mdp<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
+ result = std::make_shared<storm::models::symbolic::Mdp<Type, ValueType>>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels);
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type.");
}
+
+ if (std::is_same<ValueType, storm::RationalFunction>::value) {
+ result->addParameters(variables.parameters);
+ }
+
+ return result;
}
template <storm::dd::DdType Type, typename ValueType>
diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp
index d5358c10f..b0749616d 100644
--- a/src/storm/builder/DdPrismModelBuilder.cpp
+++ b/src/storm/builder/DdPrismModelBuilder.cpp
@@ -37,6 +37,13 @@ namespace storm {
void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter<Type, ValueType>& rowExpressionAdapter, storm::adapters::AddExpressionAdapter<Type, ValueType>& columnExpressionAdapter) {
// Intentionally left empty: no support for parameters for this data type.
}
+
+ std::set<storm::RationalFunctionVariable> const& getParameters() const {
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Creating parameters for non-parametric model is not supported.");
+ }
+
+ private:
+
};
template <storm::dd::DdType Type>
@@ -50,6 +57,7 @@ namespace storm {
for (auto const& constant : program.getConstants()) {
if (!constant.isDefined()) {
carl::Variable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName());
+ parameters.insert(carlVariable);
auto rf = convertVariableToPolynomial(carlVariable);
rowExpressionAdapter.setValue(constant.getExpressionVariable(), rf);
columnExpressionAdapter.setValue(constant.getExpressionVariable(), rf);
@@ -67,17 +75,25 @@ namespace storm {
return RationalFunctionType(variable);
}
+ std::set<storm::RationalFunctionVariable> const& getParameters() const {
+ return parameters;
+ }
+
+ private:
// A mapping from our variables to carl's.
std::unordered_map<storm::expressions::Variable, carl::Variable> variableToVariableMap;
// The cache that is used in case the underlying type needs a cache.
std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
+
+ // All created parameters.
+ std::set<storm::RationalFunctionVariable> parameters;
};
template <storm::dd::DdType Type, typename ValueType>
class DdPrismModelBuilder<Type, ValueType>::GenerationInformation {
public:
- GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared<storm::dd::DdManager<Type>>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>()), rowExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>())), columnExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() {
+ GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared<storm::dd::DdManager<Type>>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>()), rowExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>())), columnExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap(), parameters() {
// Initializes variables and identity DDs.
createMetaVariablesAndIdentities();
@@ -85,6 +101,9 @@ namespace storm {
// Initialize the parameters (if any).
ParameterCreator<Type, ValueType> parameterCreator;
parameterCreator.create(this->program, *this->rowExpressionAdapter, *this->columnExpressionAdapter);
+ if (std::is_same<ValueType, storm::RationalFunction>::value) {
+ this->parameters = parameterCreator.getParameters();
+ }
}
// The program that is currently translated.
@@ -131,11 +150,10 @@ namespace storm {
// DDs representing the valid ranges of the variables of each module.
std::map<std::string, storm::dd::Add<Type, ValueType>> moduleToRangeMap;
- private:
- void createParameters() {
-
- }
+ // The parameters appearing in the model.
+ std::set<storm::RationalFunctionVariable> parameters;
+ private:
/*!
* Creates the required meta variables and variable/module identities.
*/
@@ -1464,15 +1482,22 @@ namespace storm {
labelToExpressionMapping.emplace(label.getName(), label.getStatePredicateExpression());
}
+ std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> result;
if (program.getModelType() == storm::prism::Program::ModelType::DTMC) {
- return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
+ result = std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
} else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) {
- return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, system.stateActionDd, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
+ result = std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, system.stateActionDd, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
} else if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
- return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels));
+ result = std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
}
+
+ if (std::is_same<ValueType, storm::RationalFunction>::value) {
+ result->addParameters(generationInfo.parameters);
+ }
+
+ return result;
}
template <storm::dd::DdType Type, typename ValueType>
diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp
index 44cedb816..45f286df0 100644
--- a/src/storm/modelchecker/results/CheckResult.cpp
+++ b/src/storm/modelchecker/results/CheckResult.cpp
@@ -173,6 +173,10 @@ namespace storm {
template SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan> const& CheckResult::asSymbolicQualitativeCheckResult() const;
template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asSymbolicQuantitativeCheckResult();
template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
+ template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>& CheckResult::asSymbolicQuantitativeCheckResult();
+ template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
+ template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& CheckResult::asSymbolicQuantitativeCheckResult();
+ template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
template SymbolicParetoCurveCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asSymbolicParetoCurveCheckResult();
template SymbolicParetoCurveCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asSymbolicParetoCurveCheckResult() const;
template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asHybridQuantitativeCheckResult();
diff --git a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h
index 5c02e8cf0..34e0e0bc6 100644
--- a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h
+++ b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h
@@ -37,7 +37,6 @@ namespace storm {
virtual void filter(QualitativeCheckResult const& filter) override;
virtual ValueType getMin() const override;
-
virtual ValueType getMax() const override;
virtual ValueType average() const override;
diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp
index 447867ea8..c2ca3650e 100644
--- a/src/storm/models/symbolic/Model.cpp
+++ b/src/storm/models/symbolic/Model.cpp
@@ -13,10 +13,10 @@
#include "storm/models/symbolic/StandardRewardModel.h"
+#include "storm/utility/macros.h"
#include "storm/utility/dd.h"
-#include "storm-config.h"
-#include "storm/adapters/CarlAdapter.h"
+#include "storm/exceptions/NotSupportedException.h"
namespace storm {
namespace models {
@@ -268,6 +268,26 @@ namespace storm {
return true;
}
+ template<storm::dd::DdType Type, typename ValueType>
+ void Model<Type, ValueType>::addParameters(std::set<storm::RationalFunctionVariable> const& parameters) {
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This value type does not support parameters.");
+ }
+
+ template<storm::dd::DdType Type, typename ValueType>
+ std::set<storm::RationalFunctionVariable> const& Model<Type, ValueType>::getParameters() const {
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This value type does not support parameters.");
+ }
+
+ template<>
+ void Model<storm::dd::DdType::Sylvan, storm::RationalFunction>::addParameters(std::set<storm::RationalFunctionVariable> const& parameters) {
+ this->parameters.insert(parameters.begin(), parameters.end());
+ }
+
+ template<>
+ std::set<storm::RationalFunctionVariable> const& Model<storm::dd::DdType::Sylvan, storm::RationalFunction>::getParameters() const {
+ return parameters;
+ }
+
// Explicitly instantiate the template class.
template class Model<storm::dd::DdType::CUDD, double>;
template class Model<storm::dd::DdType::Sylvan, double>;
diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h
index 4d70fbf1d..5c9382831 100644
--- a/src/storm/models/symbolic/Model.h
+++ b/src/storm/models/symbolic/Model.h
@@ -12,6 +12,9 @@
#include "storm/models/ModelBase.h"
#include "storm/utility/OsDetection.h"
+#include "storm-config.h"
+#include "storm/adapters/CarlAdapter.h"
+
namespace storm {
namespace dd {
@@ -267,6 +270,10 @@ namespace storm {
std::vector<std::string> getLabels() const;
+ void addParameters(std::set<storm::RationalFunctionVariable> const& parameters);
+
+ std::set<storm::RationalFunctionVariable> const& getParameters() const;
+
protected:
/*!
@@ -349,6 +356,9 @@ namespace storm {
// The reward models associated with the model.
std::unordered_map<std::string, RewardModelType> rewardModels;
+
+ // The parameters. Only meaningful for models over rational functions.
+ std::set<storm::RationalFunctionVariable> parameters;
};
} // namespace symbolic
diff --git a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp
index 84a343cda..02e93ecfd 100644
--- a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp
+++ b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp
@@ -21,10 +21,18 @@ namespace storm {
storm::dd::DdMetaVariable<DdType> const& metaVariable = ddManager.getMetaVariable(rowVariable);
std::vector<storm::expressions::Variable> newMetaVariables;
+
+ // Find a suitable name for the temporary variable.
+ uint64_t counter = 0;
+ std::string newMetaVariableName = "tmp_" + metaVariable.getName();
+ while (ddManager.hasMetaVariable(newMetaVariableName + std::to_string(counter))) {
+ ++counter;
+ }
+
if (metaVariable.getType() == storm::dd::MetaVariableType::Bool) {
- newMetaVariables = ddManager.addMetaVariable("tmp_" + metaVariable.getName(), 3);
+ newMetaVariables = ddManager.addMetaVariable(newMetaVariableName + std::to_string(counter), 3);
} else {
- newMetaVariables = ddManager.addMetaVariable("tmp_" + metaVariable.getName(), metaVariable.getLow(), metaVariable.getHigh(), 3);
+ newMetaVariables = ddManager.addMetaVariable(newMetaVariableName + std::to_string(counter), metaVariable.getLow(), metaVariable.getHigh(), 3);
}
newRowVariables.insert(newMetaVariables[0]);
@@ -56,7 +64,7 @@ namespace storm {
storm::dd::DdManager<DdType>& ddManager = x.getDdManager();
// Build diagonal BDD over new meta variables.
- storm::dd::Bdd<DdType> diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), this->rowColumnMetaVariablePairs);
+ storm::dd::Bdd<DdType> diagonal = storm::utility::dd::getRowColumnDiagonal(ddManager, this->rowColumnMetaVariablePairs);
diagonal &= this->allRows;
diagonal = diagonal.swapVariables(this->oldNewMetaVariablePairs);
@@ -72,11 +80,12 @@ namespace storm {
// As long as there are transitions, we eliminate them.
uint64_t iterations = 0;
while (!matrix.isZero()) {
- // Determine inverse loop probabilies
+ // Determine inverse loop probabilies.
storm::dd::Add<DdType, ValueType> inverseLoopProbabilities = rowsAdd / (rowsAdd - (diagonalAdd * matrix).sumAbstract(newColumnVariables));
// Scale all transitions with the inverse loop probabilities.
matrix *= inverseLoopProbabilities;
+
solution *= inverseLoopProbabilities;
// Delete diagonal elements, i.e. remove self-loops.
diff --git a/src/storm/solver/SymbolicEliminationLinearEquationSolver.h b/src/storm/solver/SymbolicEliminationLinearEquationSolver.h
index be8164d43..a77ac2a8c 100644
--- a/src/storm/solver/SymbolicEliminationLinearEquationSolver.h
+++ b/src/storm/solver/SymbolicEliminationLinearEquationSolver.h
@@ -32,7 +32,7 @@ namespace storm {
};
template<storm::dd::DdType DdType, typename ValueType>
- class SymbolicEliminationLinearEquationSolverFactory {
+ class SymbolicEliminationLinearEquationSolverFactory : public SymbolicLinearEquationSolverFactory<DdType, ValueType> {
public:
virtual std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> create(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const;
diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
index 1ded07a38..78e889b1b 100644
--- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
@@ -155,15 +155,14 @@ namespace storm {
storm::dd::Add<DdType, ValueType> schedulerX = linearEquationSolver->solveEquations(currentSolution, schedulerB);
// Policy improvement step.
- storm::dd::Add<DdType, ValueType> tmp = this->A.multiplyMatrix(schedulerX.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables);
- tmp += b;
+ storm::dd::Add<DdType, ValueType> choiceValues = this->A.multiplyMatrix(schedulerX.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables) + b;
storm::dd::Bdd<DdType> nextScheduler;
if (minimize) {
- tmp += illegalMaskAdd;
- nextScheduler = tmp.minAbstractRepresentative(this->choiceVariables);
+ choiceValues += illegalMaskAdd;
+ nextScheduler = choiceValues.minAbstractRepresentative(this->choiceVariables);
} else {
- nextScheduler = tmp.maxAbstractRepresentative(this->choiceVariables);
+ nextScheduler = choiceValues.maxAbstractRepresentative(this->choiceVariables);
}
// Check for convergence.
diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp
index 7b2718e51..e1ff17ce0 100644
--- a/src/storm/utility/constants.cpp
+++ b/src/storm/utility/constants.cpp
@@ -216,7 +216,7 @@ namespace storm {
template<>
storm::ClnRationalNumber infinity() {
// FIXME: this should be treated more properly.
- return storm::ClnRationalNumber(-1);
+ return storm::ClnRationalNumber(100000000000);
}
template<>
@@ -326,7 +326,7 @@ namespace storm {
template<>
storm::GmpRationalNumber infinity() {
// FIXME: this should be treated more properly.
- return storm::GmpRationalNumber(-1);
+ return storm::GmpRationalNumber(100000000000);
}
template<>
@@ -468,7 +468,7 @@ namespace storm {
template<>
storm::RationalFunction infinity() {
// FIXME: this should be treated more properly.
- return storm::RationalFunction(-1.0);
+ return storm::RationalFunction(convertNumber<RationalFunctionCoefficient>(100000000000));
}
template<>
diff --git a/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
index 05176b4f5..97ed361ce 100644
--- a/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
+++ b/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
@@ -8,6 +8,7 @@
#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+#include "storm/solver/SymbolicEliminationLinearEquationSolver.h"
#include "storm/parser/PrismParser.h"
#include "storm/builder/DdPrismModelBuilder.h"
#include "storm/models/symbolic/StandardRewardModel.h"
@@ -41,7 +42,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) {
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>();
- storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
+ storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
@@ -103,7 +104,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) {
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
- storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
+ storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
@@ -143,6 +144,122 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) {
EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMax(), 10 * storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
+TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalNumber_Sylvan) {
+ storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
+ storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+
+ // A parser that we use for conveniently constructing the formulas.
+ storm::parser::FormulaParser formulaParser;
+
+ // Build the die model with its reward model.
+ typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalNumber>::Options options;
+ options.buildAllRewardModels = false;
+ options.rewardModelsToBuild.insert("coin_flips");
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalNumber>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalNumber>().build(program, options);
+ EXPECT_EQ(13ul, model->getNumberOfStates());
+ EXPECT_EQ(20ul, model->getNumberOfTransitions());
+
+ ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
+
+ std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalNumber>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalNumber>>();
+
+ storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalNumber>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalNumber>>(new storm::solver::SymbolicEliminationLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalNumber>()));
+
+ std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+
+ 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, storm::RationalNumber>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>();
+
+ EXPECT_EQ(quantitativeResult1.getMin(), storm::utility::convertNumber<storm::RationalNumber>(std::string("1/6")));
+ EXPECT_EQ(quantitativeResult1.getMax(), storm::utility::convertNumber<storm::RationalNumber>(std::string("1/6")));
+
+ formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
+
+ result = checker.check(*formula);
+ result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+ storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>();
+
+ EXPECT_EQ(quantitativeResult2.getMin(), storm::utility::convertNumber<storm::RationalNumber>(std::string("1/6")));
+ EXPECT_EQ(quantitativeResult2.getMax(), storm::utility::convertNumber<storm::RationalNumber>(std::string("1/6")));
+
+ formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
+
+ result = checker.check(*formula);
+ result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+ storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>();
+
+ EXPECT_EQ(quantitativeResult3.getMin(), storm::utility::convertNumber<storm::RationalNumber>(std::string("1/6")));
+ EXPECT_EQ(quantitativeResult3.getMax(), storm::utility::convertNumber<storm::RationalNumber>(std::string("1/6")));
+
+ formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
+
+ result = checker.check(*formula);
+ result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+ storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>();
+
+ EXPECT_EQ(quantitativeResult4.getMin(), storm::utility::convertNumber<storm::RationalNumber>(std::string("11/3")));
+ EXPECT_EQ(quantitativeResult4.getMax(), storm::utility::convertNumber<storm::RationalNumber>(std::string("11/3")));
+}
+
+TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) {
+ storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm");
+ storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+
+ // A parser that we use for conveniently constructing the formulas.
+ storm::parser::FormulaParser formulaParser;
+
+ // Build the die model with its reward model.
+ typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalFunction>::Options options;
+ options.buildAllRewardModels = false;
+ options.rewardModelsToBuild.insert("coin_flips");
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalFunction>().build(program, options);
+ EXPECT_EQ(13ul, model->getNumberOfStates());
+ EXPECT_EQ(20ul, model->getNumberOfTransitions());
+ ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
+
+ std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> instantiation;
+ std::set<storm::RationalFunctionVariable> variables = model->getParameters();
+ ASSERT_EQ(1ull, variables.size());
+ instantiation.emplace(*variables.begin(), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/2")));
+
+ std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>();
+
+ storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalFunction>>(new storm::solver::SymbolicEliminationLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalFunction>()));
+
+ std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+
+ 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, storm::RationalFunction>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
+
+ EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult1.sum().evaluate(instantiation)), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
+
+ formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
+
+ result = checker.check(*formula);
+ result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+ storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
+
+ EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult2.sum().evaluate(instantiation)), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
+
+ formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
+
+ result = checker.check(*formula);
+ result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+ storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
+
+ EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult3.sum().evaluate(instantiation)), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
+
+ formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
+
+ result = checker.check(*formula);
+ result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+ storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
+
+ EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult4.sum().evaluate(instantiation)), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("11/3")));
+}
+
TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
@@ -158,7 +275,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>();
- storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
+ storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
@@ -203,7 +320,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
- storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
+ storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
@@ -259,7 +376,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>();
- storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
+ storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
@@ -312,7 +429,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
- storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
+ storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
diff --git a/src/test/storage/SylvanDdTest.cpp b/src/test/storage/SylvanDdTest.cpp
index a4e4764b0..6c426fc4b 100644
--- a/src/test/storage/SylvanDdTest.cpp
+++ b/src/test/storage/SylvanDdTest.cpp
@@ -520,7 +520,7 @@ TEST(SylvanDd, RationalFunctionEncodingTest) {
storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> add;
ASSERT_NO_THROW(add = encoding.template toAdd<storm::RationalFunction>());
-
+
// As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6.
EXPECT_EQ(6ul, add.getNodeCount());
EXPECT_EQ(2ul, add.getLeafCount());