From 853b03547312bf5c6a5a8e77e40377f9129ab65c Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 1 Apr 2017 19:32:29 +0200 Subject: [PATCH] fixed bug and added testsfor symbolic linear equation solver (rational number and rational function) --- .../3rdparty/sylvan/src/storm_wrapper.cpp | 2 +- .../sylvan/src/sylvan_storm_rational_number.c | 4 +- src/storm/builder/DdJaniModelBuilder.cpp | 82 ++++++++++- src/storm/builder/DdPrismModelBuilder.cpp | 41 ++++-- .../modelchecker/results/CheckResult.cpp | 4 + .../results/SymbolicQuantitativeCheckResult.h | 1 - src/storm/models/symbolic/Model.cpp | 24 +++- src/storm/models/symbolic/Model.h | 10 ++ ...ymbolicEliminationLinearEquationSolver.cpp | 17 ++- .../SymbolicEliminationLinearEquationSolver.h | 2 +- .../SymbolicMinMaxLinearEquationSolver.cpp | 9 +- src/storm/utility/constants.cpp | 6 +- .../SymbolicDtmcPrctlModelCheckerTest.cpp | 129 +++++++++++++++++- src/test/storage/SylvanDdTest.cpp | 2 +- 14 files changed, 295 insertions(+), 38 deletions(-) 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 + class ParameterCreator { + public: + void create(storm::jani::Model const& model, storm::adapters::AddExpressionAdapter& rowExpressionAdapter, storm::adapters::AddExpressionAdapter& columnExpressionAdapter) { + // Intentionally left empty: no support for parameters for this data type. + } + + std::set const& getParameters() const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Creating parameters for non-parametric model is not supported."); + } + + private: + + }; + + template + class ParameterCreator { + public: + ParameterCreator() : cache(std::make_shared>>()) { + // Intentionally left empty. + } + + void create(storm::jani::Model const& model, storm::adapters::AddExpressionAdapter& rowExpressionAdapter, storm::adapters::AddExpressionAdapter& 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> = carl::dummy> + RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) { + return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::PolyType::PolyType(variable), cache)); + } + + template> = carl::dummy> + RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) { + return RationalFunctionType(variable); + } + + std::set const& getParameters() const { + return parameters; + } + + private: + // A mapping from our variables to carl's. + std::unordered_map variableToVariableMap; + + // The cache that is used in case the underlying type needs a cache. + std::shared_ptr>> cache; + + // All created parameters. + std::set parameters; + }; + template struct CompositionVariables { CompositionVariables() : manager(std::make_shared>()), @@ -191,6 +250,9 @@ namespace storm { // A DD representing the valid ranges of the global variables. storm::dd::Add globalVariableRanges; + + // The parameters that appear in the model. + std::set 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(); } + ParameterCreator parameterCreator; + parameterCreator.create(model, *result.rowExpressionAdapter, *result.columnExpressionAdapter); + if (std::is_same::value) { + result.parameters = parameterCreator.getParameters(); + } + return result; } @@ -1631,16 +1699,22 @@ namespace storm { template std::shared_ptr> createModel(storm::jani::ModelType const& modelType, CompositionVariables const& variables, ModelComponents const& modelComponents) { - + std::shared_ptr> result; if (modelType == storm::jani::ModelType::DTMC) { - return std::make_shared>(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>(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>(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>(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>(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>(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::value) { + result->addParameters(variables.parameters); + } + + return result; } template 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& rowExpressionAdapter, storm::adapters::AddExpressionAdapter& columnExpressionAdapter) { // Intentionally left empty: no support for parameters for this data type. } + + std::set const& getParameters() const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Creating parameters for non-parametric model is not supported."); + } + + private: + }; template @@ -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 const& getParameters() const { + return parameters; + } + + private: // A mapping from our variables to carl's. std::unordered_map variableToVariableMap; // The cache that is used in case the underlying type needs a cache. std::shared_ptr>> cache; + + // All created parameters. + std::set parameters; }; template class DdPrismModelBuilder::GenerationInformation { public: - GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared>()), rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared>())), columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() { + GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared>()), rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared>())), columnExpressionAdapter(std::make_shared>(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 parameterCreator; parameterCreator.create(this->program, *this->rowExpressionAdapter, *this->columnExpressionAdapter); + if (std::is_same::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> moduleToRangeMap; - private: - void createParameters() { - - } + // The parameters appearing in the model. + std::set 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> result; if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { - return std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); + result = std::shared_ptr>(new storm::models::symbolic::Dtmc(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>(new storm::models::symbolic::Ctmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, system.stateActionDd, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); + result = std::shared_ptr>(new storm::models::symbolic::Ctmc(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>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels)); + result = std::shared_ptr>(new storm::models::symbolic::Mdp(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::value) { + result->addParameters(generationInfo.parameters); + } + + return result; } template 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 const& CheckResult::asSymbolicQualitativeCheckResult() const; template SymbolicQuantitativeCheckResult& CheckResult::asSymbolicQuantitativeCheckResult(); template SymbolicQuantitativeCheckResult const& CheckResult::asSymbolicQuantitativeCheckResult() const; + template SymbolicQuantitativeCheckResult& CheckResult::asSymbolicQuantitativeCheckResult(); + template SymbolicQuantitativeCheckResult const& CheckResult::asSymbolicQuantitativeCheckResult() const; + template SymbolicQuantitativeCheckResult& CheckResult::asSymbolicQuantitativeCheckResult(); + template SymbolicQuantitativeCheckResult const& CheckResult::asSymbolicQuantitativeCheckResult() const; template SymbolicParetoCurveCheckResult& CheckResult::asSymbolicParetoCurveCheckResult(); template SymbolicParetoCurveCheckResult const& CheckResult::asSymbolicParetoCurveCheckResult() const; template HybridQuantitativeCheckResult& 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 + void Model::addParameters(std::set const& parameters) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This value type does not support parameters."); + } + + template + std::set const& Model::getParameters() const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This value type does not support parameters."); + } + + template<> + void Model::addParameters(std::set const& parameters) { + this->parameters.insert(parameters.begin(), parameters.end()); + } + + template<> + std::set const& Model::getParameters() const { + return parameters; + } + // Explicitly instantiate the template class. template class Model; template class Model; 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 getLabels() const; + void addParameters(std::set const& parameters); + + std::set const& getParameters() const; + protected: /*! @@ -349,6 +356,9 @@ namespace storm { // The reward models associated with the model. std::unordered_map rewardModels; + + // The parameters. Only meaningful for models over rational functions. + std::set 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 const& metaVariable = ddManager.getMetaVariable(rowVariable); std::vector 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& ddManager = x.getDdManager(); // Build diagonal BDD over new meta variables. - storm::dd::Bdd diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), this->rowColumnMetaVariablePairs); + storm::dd::Bdd 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 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 - class SymbolicEliminationLinearEquationSolverFactory { + class SymbolicEliminationLinearEquationSolverFactory : public SymbolicLinearEquationSolverFactory { public: virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> 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 schedulerX = linearEquationSolver->solveEquations(currentSolution, schedulerB); // Policy improvement step. - storm::dd::Add tmp = this->A.multiplyMatrix(schedulerX.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables); - tmp += b; + storm::dd::Add choiceValues = this->A.multiplyMatrix(schedulerX.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables) + b; storm::dd::Bdd 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(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> dtmc = model->as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolverFactory())); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); @@ -103,7 +104,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolverFactory())); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); @@ -143,6 +144,122 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) { EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMax(), 10 * storm::settings::getModule().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::Options options; + options.buildAllRewardModels = false; + options.rewardModelsToBuild.insert("coin_flips"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicEliminationLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_EQ(quantitativeResult1.getMin(), storm::utility::convertNumber(std::string("1/6"))); + EXPECT_EQ(quantitativeResult1.getMax(), storm::utility::convertNumber(std::string("1/6"))); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_EQ(quantitativeResult2.getMin(), storm::utility::convertNumber(std::string("1/6"))); + EXPECT_EQ(quantitativeResult2.getMax(), storm::utility::convertNumber(std::string("1/6"))); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_EQ(quantitativeResult3.getMin(), storm::utility::convertNumber(std::string("1/6"))); + EXPECT_EQ(quantitativeResult3.getMax(), storm::utility::convertNumber(std::string("1/6"))); + + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_EQ(quantitativeResult4.getMin(), storm::utility::convertNumber(std::string("11/3"))); + EXPECT_EQ(quantitativeResult4.getMax(), storm::utility::convertNumber(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::Options options; + options.buildAllRewardModels = false; + options.rewardModelsToBuild.insert("coin_flips"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::map instantiation; + std::set variables = model->getParameters(); + ASSERT_EQ(1ull, variables.size()); + instantiation.emplace(*variables.begin(), storm::utility::convertNumber(std::string("1/2"))); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicEliminationLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_EQ(storm::utility::convertNumber(quantitativeResult1.sum().evaluate(instantiation)), storm::utility::convertNumber(std::string("1/6"))); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_EQ(storm::utility::convertNumber(quantitativeResult2.sum().evaluate(instantiation)), storm::utility::convertNumber(std::string("1/6"))); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_EQ(storm::utility::convertNumber(quantitativeResult3.sum().evaluate(instantiation)), storm::utility::convertNumber(std::string("1/6"))); + + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_EQ(storm::utility::convertNumber(quantitativeResult4.sum().evaluate(instantiation)), storm::utility::convertNumber(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> dtmc = model->as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolverFactory())); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); @@ -203,7 +320,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolverFactory())); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); @@ -259,7 +376,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolverFactory())); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); @@ -312,7 +429,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolverFactory())); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GeneralSymbolicLinearEquationSolverFactory())); std::shared_ptr 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 add; ASSERT_NO_THROW(add = encoding.template toAdd()); - + // 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());