fix bug in rational number/function handling with sylvan

resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c

@@ -554,7 +554,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, a, size_t
     
     if (mtbdd_isleaf(a)) {
         storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a);
-        return storm_rational_function_less_or_equal(ma, value) ? mtbdd_false : mtbdd_true;
+        return storm_rational_function_less(ma, value) ? mtbdd_false : mtbdd_true;
     }
     
     return mtbdd_invalid;
@@ -566,7 +566,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, a,
     if (mtbdd_isleaf(a)) {
         storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a);
         
-        return storm_rational_function_less(ma, value) ? mtbdd_false : mtbdd_true;
+        return storm_rational_function_less_or_equal(ma, value) ? mtbdd_false : mtbdd_true;
     }
     
     return mtbdd_invalid;

resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c

@@ -588,7 +588,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, a, size_t*,
     
     if (mtbdd_isleaf(a)) {
         storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a);
-        return storm_rational_number_less_or_equal(ma, value) ? mtbdd_false : mtbdd_true;
+        return storm_rational_number_less(ma, value) ? mtbdd_false : mtbdd_true;
     }
     
     return mtbdd_invalid;
@@ -600,7 +600,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, a, s
     if (mtbdd_isleaf(a)) {
         storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a);
         
-        return storm_rational_number_less(ma, value) ? mtbdd_false : mtbdd_true;
+        return storm_rational_number_less_or_equal(ma, value) ? mtbdd_false : mtbdd_true;
     }
     
     return mtbdd_invalid;

src/storm/solver/SymbolicLinearEquationSolver.cpp

@@ -59,7 +59,6 @@ namespace storm {
             }
         }
         
-        
         template<storm::dd::DdType DdType>
         std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, storm::RationalFunction>> GeneralSymbolicLinearEquationSolverFactory<DdType, storm::RationalFunction>::create(storm::dd::Add<DdType, storm::RationalFunction> const& A, storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const {
             

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

@@ -846,7 +846,6 @@ namespace storm {
                 auto states = partition.getStates().swapVariables(model.getRowColumnMetaVariablePairs());
                 
                 storm::dd::Bdd<DdType> partitionAsBdd = partition.storedAsAdd() ? partition.asAdd().toBdd() : partition.asBdd();
-                partitionAsBdd.exportToDot("part.dot");
                 partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables());
 
                 auto start = std::chrono::high_resolution_clock::now();
@@ -968,13 +967,18 @@ namespace storm {
                     STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
 
                     start = std::chrono::high_resolution_clock::now();
-                    storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsBdd.renameVariables(blockVariableSet, blockPrimeVariableSet).renameVariables(model.getRowVariables(), model.getColumnVariables()), model.getColumnVariables());
+                    std::set<storm::expressions::Variable> blockAndRowVariables;
+                    std::set_union(blockVariableSet.begin(), blockVariableSet.end(), model.getRowVariables().begin(), model.getRowVariables().end(), std::inserter(blockAndRowVariables, blockAndRowVariables.end()));
+                    std::set<storm::expressions::Variable> blockPrimeAndColumnVariables;
+                    std::set_union(blockPrimeVariableSet.begin(), blockPrimeVariableSet.end(), model.getColumnVariables().begin(), model.getColumnVariables().end(), std::inserter(blockPrimeAndColumnVariables, blockPrimeAndColumnVariables.end()));
+                    storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
+                    storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables());
                     
                     // Pick a representative from each block.
                     auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
                     partitionAsBdd &= representatives;
-                    storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
-                    
+                    partitionAsAdd *= partitionAsBdd.template toAdd<ValueType>();
+
                     quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables());
                     end = std::chrono::high_resolution_clock::now();