From b4685f36d467763e787de4a6737e5d5b1f8b5228 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 16 Jan 2017 20:49:15 +0100 Subject: [PATCH] reverted increasing CUDD precision by default --- src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp | 2 +- src/storm/settings/modules/CuddSettings.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index 0b912c623..84d7bcd15 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -58,7 +58,7 @@ namespace storm { // Solve the equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector); + storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.0) * maybeStatesAdd, subvector); return statesWithProbability01.second.template toAdd() + result; } else { diff --git a/src/storm/settings/modules/CuddSettings.cpp b/src/storm/settings/modules/CuddSettings.cpp index 0a2313757..e680276bf 100644 --- a/src/storm/settings/modules/CuddSettings.cpp +++ b/src/storm/settings/modules/CuddSettings.cpp @@ -20,7 +20,7 @@ namespace storm { const std::string CuddSettings::reorderOptionName = "reorder"; CuddSettings::CuddSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-16).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(4096).build()).build());