diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp index 8c03c27c3..8ed66dbdf 100644 --- a/src/storm/settings/modules/BisimulationSettings.cpp +++ b/src/storm/settings/modules/BisimulationSettings.cpp @@ -20,7 +20,6 @@ namespace storm { const std::string BisimulationSettings::reuseOptionName = "reuse"; const std::string BisimulationSettings::initialPartitionOptionName = "init"; const std::string BisimulationSettings::refinementModeOptionName = "refine"; - const std::string BisimulationSettings::parallelismModeOptionName = "parallel"; BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) { std::vector types = { "strong", "weak" }; @@ -51,12 +50,6 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(refinementModes)) .setDefaultValueString("full").build()) .build()); - - std::vector parallelismModes = {"on", "off"}; - this->addOption(storm::settings::OptionBuilder(moduleName, parallelismModeOptionName, true, "Sets whether to use parallelism mode or not.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(parallelismModes)) - .setDefaultValueString("on").build()) - .build()); } bool BisimulationSettings::isStrongBisimulationSet() const { @@ -125,16 +118,6 @@ namespace storm { return RefinementMode::Full; } - BisimulationSettings::ParallelismMode BisimulationSettings::getParallelismMode() const { - std::string parallelismModeAsString = this->getOption(parallelismModeOptionName).getArgumentByName("mode").getValueAsString(); - if (parallelismModeAsString == "on") { - return ParallelismMode::Parallel; - } else if (parallelismModeAsString == "off") { - return ParallelismMode::Sequential; - } - return ParallelismMode::Parallel; - } - bool BisimulationSettings::check() const { bool optionsSet = this->getOption(typeOptionName).getHasOptionBeenSet(); STORM_LOG_WARN_COND(storm::settings::getModule().isBisimulationSet() || !optionsSet, "Bisimulation minimization is not selected, so setting options for bisimulation has no effect."); diff --git a/src/storm/settings/modules/BisimulationSettings.h b/src/storm/settings/modules/BisimulationSettings.h index 4a12a4f28..a482263bc 100644 --- a/src/storm/settings/modules/BisimulationSettings.h +++ b/src/storm/settings/modules/BisimulationSettings.h @@ -25,8 +25,6 @@ namespace storm { enum class RefinementMode { Full, ChangedStates }; - enum class ParallelismMode { Parallel, Sequential }; - /*! * Creates a new set of bisimulation settings. */ @@ -77,12 +75,7 @@ namespace storm { * Retrieves the refinement mode to use. */ RefinementMode getRefinementMode() const; - - /*! - * Retrieves whether parallel is set. - */ - ParallelismMode getParallelismMode() const; - + virtual bool check() const override; // The name of the module. diff --git a/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.cpp index 90aebf216..c4b2f6467 100644 --- a/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.cpp @@ -11,7 +11,7 @@ namespace storm { // Intentionally left empty. } - InternalSignatureRefinerOptions::InternalSignatureRefinerOptions(bool shiftStateVariables) : shiftStateVariables(shiftStateVariables), createChangedStates(true), parallel(false) { + InternalSignatureRefinerOptions::InternalSignatureRefinerOptions(bool shiftStateVariables) : shiftStateVariables(shiftStateVariables), createChangedStates(true) { auto const& bisimulationSettings = storm::settings::getModule(); storm::settings::modules::BisimulationSettings::ReuseMode reuseMode = bisimulationSettings.getReuseMode(); @@ -19,9 +19,6 @@ namespace storm { storm::settings::modules::BisimulationSettings::RefinementMode refinementMode = bisimulationSettings.getRefinementMode(); this->createChangedStates = refinementMode == storm::settings::modules::BisimulationSettings::RefinementMode::ChangedStates; - - storm::settings::modules::BisimulationSettings::ParallelismMode parallelismMode = bisimulationSettings.getParallelismMode(); - this->parallel = parallelismMode == storm::settings::modules::BisimulationSettings::ParallelismMode::Parallel; } ReuseWrapper::ReuseWrapper() : ReuseWrapper(false) { diff --git a/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.h b/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.h index 0b3f3309a..a700e7e43 100644 --- a/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.h +++ b/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.h @@ -16,7 +16,6 @@ namespace storm { bool shiftStateVariables; bool reuseBlockNumbers; bool createChangedStates; - bool parallel; }; class ReuseWrapper { diff --git a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp index a236a7b04..07c46fc3c 100644 --- a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp @@ -83,6 +83,18 @@ namespace storm { return hash ^ (hash>>32); } + /*! + * The code below was taken from the SigrefMC implementation by Tom van Dijk, available at + * + * https://github.com/utwente-fmt/sigrefmc/ + * + * It provides a fully multi-threaded version of signature-based partition refinement and includes, amongst + * other things, a small custom-tailored hashmap that supports multi-threaded insertion. + * + * The code was modified in minor places to account for necessary changes, for example to handle + * nondeterminism variables. + */ + #pragma clang diagnostic push #pragma clang diagnostic ignored "-Wc99-extensions" #pragma GCC diagnostic push @@ -181,16 +193,6 @@ namespace storm { } } - TASK_3(BDD, sylvan_encode_block, BDD, vars, uint64_t, numberOfVariables, uint64_t, blockIndex) - { - std::vector e(numberOfVariables); - for (uint64_t i = 0; i < numberOfVariables; ++i) { - e[i] = blockIndex & 1 ? 1 : 0; - blockIndex >>= 1; - } - return sylvan_cube(vars, e.data()); - } - TASK_1(uint64_t, sylvan_decode_block, BDD, block) { uint64_t result = 0; @@ -208,6 +210,16 @@ namespace storm { return result; } + TASK_3(BDD, sylvan_encode_block, BDD, vars, uint64_t, numberOfVariables, uint64_t, blockIndex) + { + std::vector e(numberOfVariables); + for (uint64_t i = 0; i < numberOfVariables; ++i) { + e[i] = blockIndex & 1 ? 1 : 0; + blockIndex >>= 1; + } + return sylvan_cube(vars, e.data()); + } + TASK_3(BDD, sylvan_assign_block, BDD, sig, BDD, previous_block, InternalSylvanSignatureRefinerBase*, refiner) { assert(previous_block != mtbdd_false); // if so, incorrect call! @@ -223,7 +235,8 @@ namespace storm { // try to claim previous block number assert(previous_block != sylvan_false); const uint64_t p_b = CALL(sylvan_decode_block, previous_block); - + assert(p_b < refiner->signatures.size()); + for (;;) { BDD cur = *(volatile BDD*)&refiner->signatures[p_b]; if (cur == sig) return previous_block; @@ -269,7 +282,7 @@ namespace storm { bool nondet = nondetvars_var == vars_var; uint64_t offset = (nondet || !refiner->options.shiftStateVariables) ? 0 : 1; - while (vars_var < dd_var && vars_var < pp_var+offset) { + while (vars_var < dd_var && vars_var+offset < pp_var) { vars = sylvan_set_next(vars); if (nondet) { nondetvars = sylvan_set_next(nondetvars);