fixed some recently introduced issues

src/storm/storage/dd/BisimulationDecomposition.cpp

@@ -94,7 +94,7 @@ namespace storm {
             }
             auto end = std::chrono::high_resolution_clock::now();
             
-            STORM_LOG_DEBUG("Partition refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "s (" << iterations << " iterations).");
+            STORM_LOG_DEBUG("Partition refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms (" << iterations << " iterations).");
         }
 
         template <storm::dd::DdType DdType, typename ValueType>
@@ -117,7 +117,7 @@ namespace storm {
                     auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
                     if (static_cast<uint64_t>(durationSinceLastMessage) >= showProgressDelay) {
                         auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(now - start).count();
-                        STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "s) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
+                        STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "ms) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
                         timeOfLastMessage = std::chrono::high_resolution_clock::now();
                     }
                 }

src/storm/storage/dd/bisimulation/SignatureRefiner.cpp

@@ -466,7 +466,7 @@ namespace storm {
                 spp::sparse_hash_map<DdNode const*, ReuseWrapper> reuseBlocksCache;
             };
             
-            TASK_DECL_5(BDD, refine_double, BDD, MTBDD, BDD, BDD, void*);
+            TASK_DECL_5(BDD, refine_parallel, BDD, MTBDD, BDD, BDD, void*);
 
             template<storm::dd::DdType DdType>
             class InternalSignatureRefinerBase;
@@ -709,7 +709,7 @@ namespace storm {
                 
                 std::pair<BDD, BDD> refineParallel(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) {
                     LACE_ME;
-                    return std::make_pair(CALL(refine_double, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, this), 0);
+                    return std::make_pair(CALL(refine_parallel, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, this), 0);
                 }
                 
                 std::pair<BDD, BDD> refineSequential(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) {
@@ -868,7 +868,7 @@ namespace storm {
                 
             };
             
-            TASK_IMPL_5(BDD, refine_double, BDD, partitionNode, MTBDD, signatureNode, BDD, nondeterminismVariablesNode, BDD, nonBlockVariablesNode, void*, refinerPtr)
+            TASK_IMPL_5(BDD, refine_parallel, BDD, partitionNode, MTBDD, signatureNode, BDD, nondeterminismVariablesNode, BDD, nonBlockVariablesNode, void*, refinerPtr)
             {
                 auto& refiner = *static_cast<InternalSignatureRefinerBase<storm::dd::DdType::Sylvan>*>(refinerPtr);
                 std::unique_lock<std::mutex> lock(refiner.mutex, std::defer_lock);
@@ -881,8 +881,12 @@ namespace storm {
                 
                 STORM_LOG_ASSERT(partitionNode != mtbdd_false, "Expected non-false node.");
                 
+                // Check the cache whether we have seen the same node before.
                 BDD result;
-
+                if (cache_get(signatureNode|(256LL<<42), nonBlockVariablesNode, partitionNode|(refiner.numberOfRefinements<<40), &result)) {
+                    return result;
+                }
+                
                 if (sylvan_isconst(nonBlockVariablesNode)) {
                     // Get the lock so we can modify the signature cache.
                     lock.lock();
@@ -911,11 +915,10 @@ namespace storm {
                     result = refiner.encodeBlock(refiner.nextFreeBlockIndex++);
                     refiner.signatureCacheSingle[nodePair] = result;
                     lock.unlock();
-                    return result;
-                }
-                
-                // Check the cache whether we have seen the same node before.
-                if (cache_get(signatureNode|(256LL<<42), nonBlockVariablesNode, partitionNode|(refiner.numberOfRefinements<<40), &result)) {
+                    
+                    // Store the result in the cache.
+                    cache_put(signatureNode|(256LL<<42), nonBlockVariablesNode, partitionNode|(refiner.numberOfRefinements<<40), result);
+                    
                     return result;
                 }
                 
@@ -966,15 +969,15 @@ namespace storm {
                 
                 // If there are no more non-block variables remaining, make a recursive call to enter the base case.
                 if (sylvan_isconst(nonBlockVariablesNode)) {
-                    return CALL(refine_double, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, refinerPtr);
+                    return CALL(refine_parallel, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, refinerPtr);
                 }
                 
                 BDD nextNondeterminismVariables = isNondeterminismVariable ? sylvan_set_next(nondeterminismVariablesNode) : nondeterminismVariablesNode;
                 BDD nextNonBlockVariables = sylvan_set_next(nonBlockVariablesNode);
-                bdd_refs_spawn(SPAWN(refine_double, partitionThen, signatureThen, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr));
+                bdd_refs_spawn(SPAWN(refine_parallel, partitionElse, signatureElse, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr));
                 
-                BDD elseResult = bdd_refs_push(CALL(refine_double, partitionElse, signatureElse, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr));
-                BDD thenResult = bdd_refs_sync(SYNC(refine_double));
+                BDD thenResult = bdd_refs_push(CALL(refine_parallel, partitionThen, signatureThen, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr));
+                BDD elseResult = bdd_refs_sync(SYNC(refine_parallel));
                 bdd_refs_pop(1);
                 
                 if (thenResult == elseResult) {

src/storm/utility/sylvan.cpp

@@ -0,0 +1,15 @@
+#include "storm/utility/sylvan.h"
+
+namespace storm {
+    namespace dd {
+        
+        bool sylvan_bdd_matches_variable_index(BDD node, uint64_t variableIndex, int64_t offset) {
+            return !sylvan_isconst(node) && static_cast<uint64_t>(sylvan_var(node) + offset) == variableIndex;
+        }
+        
+        bool sylvan_mtbdd_matches_variable_index(MTBDD node, uint64_t variableIndex, int64_t offset) {
+            return !mtbdd_isleaf(node) && static_cast<uint64_t>(sylvan_var(node) + offset) == variableIndex;
+        }
+        
+    }
+}

src/storm/utility/sylvan.h

@@ -28,9 +28,7 @@ namespace storm {
          * @param offset An offset that is applied to the index of the top variable in the BDD.
          * @return True iff the BDD's top variable has the given index.
          */
-        bool sylvan_bdd_matches_variable_index(BDD node, uint64_t variableIndex, int64_t offset = 0) {
-            return !sylvan_isconst(node) && static_cast<uint64_t>(sylvan_var(node) + offset) == variableIndex;
-        }
+        bool sylvan_bdd_matches_variable_index(BDD node, uint64_t variableIndex, int64_t offset = 0);
         
         /*!
          * Retrieves whether the topmost variable in the MTBDD is the one with the given index.
@@ -40,9 +38,7 @@ namespace storm {
          * @param offset An offset that is applied to the index of the top variable in the BDD.
          * @return True iff the BDD's top variable has the given index.
          */
-        bool sylvan_mtbdd_matches_variable_index(MTBDD node, uint64_t variableIndex, int64_t offset = 0) {
-            return !mtbdd_isleaf(node) && static_cast<uint64_t>(sylvan_var(node) + offset) == variableIndex;
-        }
+        bool sylvan_mtbdd_matches_variable_index(MTBDD node, uint64_t variableIndex, int64_t offset = 0);
         
     }
 }