Browse Source

reverted increasing CUDD precision by default

tempestpy_adaptions
dehnert 8 years ago
parent
commit
b4685f36d4
  1. 2
      src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
  2. 2
      src/storm/settings/modules/CuddSettings.cpp

2
src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp

@ -58,7 +58,7 @@ namespace storm {
// Solve the equation system. // Solve the equation system.
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs());
storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector);
storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().getConstant(0.0) * maybeStatesAdd, subvector);
return statesWithProbability01.second.template toAdd<ValueType>() + result; return statesWithProbability01.second.template toAdd<ValueType>() + result;
} else { } else {

2
src/storm/settings/modules/CuddSettings.cpp

@ -20,7 +20,7 @@ namespace storm {
const std::string CuddSettings::reorderOptionName = "reorder"; const std::string CuddSettings::reorderOptionName = "reorder";
CuddSettings::CuddSettings() : ModuleSettings(moduleName) { 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()); 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());

Loading…
Cancel
Save