removed parallel flag for bisimulation as this is now governed by sylvan:threads already, fixed bug in DD traversal

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<std::string> 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<std::string> 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<storm::settings::modules::GeneralSettings>().isBisimulationSet() || !optionsSet, "Bisimulation minimization is not selected, so setting options for bisimulation has no effect.");

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.

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>();
                 
                 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) {

src/storm/storage/dd/bisimulation/InternalSignatureRefiner.h

@@ -16,7 +16,6 @@ namespace storm {
                 bool shiftStateVariables;
                 bool reuseBlockNumbers;
                 bool createChangedStates;
-                bool parallel;
             };
             
             class ReuseWrapper {

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<uint8_t> 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<uint8_t> 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);