From f1ca2853f7efa822e44b59911ef5dc38257e1593 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 29 Jul 2017 11:25:05 +0200 Subject: [PATCH] fixed some typo and added some documentation --- src/storm/settings/modules/JitBuilderSettings.cpp | 4 ++-- src/storm/storage/dd/cudd/InternalCuddDdManager.cpp | 4 +++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/storm/settings/modules/JitBuilderSettings.cpp b/src/storm/settings/modules/JitBuilderSettings.cpp index b779f23f5..7dc6808e9 100644 --- a/src/storm/settings/modules/JitBuilderSettings.cpp +++ b/src/storm/settings/modules/JitBuilderSettings.cpp @@ -34,8 +34,8 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the carl headers.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, compilerFlagsOptionName, false, "The flags passed to the compiler.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("flags", "The compiler flags.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, optimizationLevelOptionName, false, "The optimization level to use.") - .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("level", "The compiler flags.").setDefaultValueUnsignedInteger(3).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, optimizationLevelOptionName, false, "Sets the optimization level.") + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("level", "The level to use.").setDefaultValueUnsignedInteger(3).build()).build()); } bool JitBuilderSettings::isCompilerSet() const { diff --git a/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp b/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp index e7b7961fe..952c7199c 100644 --- a/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp @@ -85,7 +85,9 @@ namespace storm { } } - // Connect the two variables so they are not 'torn apart' during dynamic reordering. + // Connect the variables so they are not 'torn apart' by dynamic reordering. + // Note that MTR_FIXED preserves the order of the layers. While this is not always necessary to preserve, + // (for example) the hybrid engine relies on this connection, so we choose MTR_FIXED instead of MTR_DEFAULT. cuddManager.MakeTreeNode(result.front().getIndex(), numberOfLayers, MTR_FIXED); // Keep track of the number of variables.