completed interface of (sylvan) ADDs for storing rational functions

resources/3rdparty/sylvan/src/storm_function_wrapper.cpp

@@ -8,8 +8,11 @@
 #include <mutex>
 
 #include "storm/adapters/CarlAdapter.h"
+#include "storm/utility/constants.h"
 #include "sylvan_storm_rational_function.h"
 
+#include "storm/exceptions/InvalidOperationException.h"
+
 #include <sylvan_config.h>
 #include <sylvan.h>
 #include <sylvan_common.h>
@@ -128,22 +131,140 @@ storm_rational_function_ptr storm_rational_function_divide(storm_rational_functi
 			std::cerr << "Could not allocate memory in storm_rational_function_divide()!" << std::endl;
 			return result;
 		}
-		
+		        
 		*result_srf /= srf_b;
 		result = (storm_rational_function_ptr)result_srf;
 	}
 	return result;
 }
 
+storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+    std::lock_guard<std::mutex> lock(carlMutex);
+    storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr;
+    
+    {
+        storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+        storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
+        
+        uint64_t exponentAsInteger = carl::toInt<unsigned long>(srf_b.nominatorAsNumber());
+        storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger));
+        if (result_srf == nullptr) {
+            std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl;
+            return result;
+        }
+        result = (storm_rational_function_ptr)result_srf;
+    }
+    return result;
+}
+
+storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+    std::lock_guard<std::mutex> lock(carlMutex);
+    storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr;
+    
+    {
+        storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+        storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
+        if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) {
+            throw storm::exceptions::InvalidOperationException() << "Operands of mod must not be rational function.";
+        }
+        throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rationals.";
+        
+        // storm::RationalFunction* result_srf = new storm::RationalFunction(carl::mod(srf_a.nominatorAsNumber(), srf_b.nominatorAsNumber()));
+//        if (result_srf == nullptr) {
+//            std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl;
+//            return result;
+//        }
+//        result = (storm_rational_function_ptr)result_srf;
+    
+    }
+    return result;
+}
+
+storm_rational_function_ptr storm_rational_function_min(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+    std::lock_guard<std::mutex> lock(carlMutex);
+    storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr;
+    
+    {
+        storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+        storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
+        if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) {
+            throw storm::exceptions::InvalidOperationException() << "Operands of min must not be rational function.";
+        }
+
+        storm::RationalFunction* result_srf = new storm::RationalFunction(std::min(srf_a.nominatorAsNumber(), srf_b.nominatorAsNumber()));
+        if (result_srf == nullptr) {
+            std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl;
+            return result;
+        }
+        result = (storm_rational_function_ptr)result_srf;
+    
+    }
+    return result;
+}
+
+storm_rational_function_ptr storm_rational_function_max(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+    std::lock_guard<std::mutex> lock(carlMutex);
+    storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr;
+    
+    {
+        storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+        storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
+        if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) {
+            throw storm::exceptions::InvalidOperationException() << "Operands of max must not be rational function.";
+        }
+
+        storm::RationalFunction* result_srf = new storm::RationalFunction(std::max(srf_a.nominatorAsNumber(), srf_b.nominatorAsNumber()));
+        if (result_srf == nullptr) {
+            std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl;
+            return result;
+        }
+        result = (storm_rational_function_ptr)result_srf;
+    }
+    return result;
+}
+
+int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+    std::lock_guard<std::mutex> lock(carlMutex);
+    
+    storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+    storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
+    if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) {
+        throw storm::exceptions::InvalidOperationException() << "Operands of less must not be rational functions.";
+    }
+    
+    if (srf_a.nominatorAsNumber() < srf_b.nominatorAsNumber()) {
+        return 1;
+    } else {
+        return 0;
+    }
+    return -1;
+}
+
+int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_rational_function_ptr b) {
+    std::lock_guard<std::mutex> lock(carlMutex);
+    
+    storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+    storm::RationalFunction& srf_b = *(storm::RationalFunction*)b;
+    if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) {
+        throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be rational functions.";
+    }
+    if (srf_a.nominatorAsNumber() <= srf_b.nominatorAsNumber()) {
+        return 1;
+    } else {
+        return 0;
+    }
+    
+    return -1;
+}
+
 uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) {
 	std::lock_guard<std::mutex> lock(carlMutex);
 	
-	uint64_t result = 0;
+	uint64_t result = seed;
 	{
 		storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
-		size_t hash = carl::hash_value(srf_a);
-	
-		result = hash ^ seed;
+        // carl::hash_add(result, srf_a);
+        result = seed ^ (carl::hash_value(srf_a) + 0x9e3779b9 + (seed<<6) + (seed>>2));
 	}
 	return result;
 }
@@ -167,6 +288,51 @@ storm_rational_function_ptr storm_rational_function_negate(storm_rational_functi
 	return result;
 }
 
+storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a) {
+    std::lock_guard<std::mutex> lock(carlMutex);
+    storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr;
+    
+    {
+        storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+        if (!storm::utility::isInteger(srf_a)) {
+            throw storm::exceptions::InvalidOperationException() << "Operand of floor must not be rational function.";
+        }
+        storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
+        
+        if (result_srf == nullptr) {
+            std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl;
+            return result;
+        }
+        
+        *result_srf = storm::RationalFunction(carl::floor(srf_a.nominatorAsNumber()));
+        result = (storm_rational_function_ptr)result_srf;
+        
+    }
+    return result;
+}
+
+storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a) {
+    std::lock_guard<std::mutex> lock(carlMutex);
+    storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr;
+    
+    {
+        storm::RationalFunction& srf_a = *(storm::RationalFunction*)a;
+        if (!storm::utility::isInteger(srf_a)) {
+            throw storm::exceptions::InvalidOperationException() << "Operand of ceil must not be rational function.";
+        }
+        storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
+        
+        if (result_srf == nullptr) {
+            std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl;
+            return result;
+        }
+        
+        *result_srf = storm::RationalFunction(carl::ceil(srf_a.nominatorAsNumber()));
+        result = (storm_rational_function_ptr)result_srf;
+    }
+    return result;
+}
+
 int storm_rational_function_is_zero(storm_rational_function_ptr a) {
 	std::lock_guard<std::mutex> lock(carlMutex);
 

resources/3rdparty/sylvan/src/storm_function_wrapper.h

@@ -11,15 +11,31 @@ extern "C" {
 
 typedef void* storm_rational_function_ptr;
 
-// equals, plus, minus, divide, times, create, destroy
+// basic functions (for sylvan)
 void storm_rational_function_init(storm_rational_function_ptr* a);
 void storm_rational_function_destroy(storm_rational_function_ptr a);
 int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b);
+
+// binary
 storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b);
 storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b);
 storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b);
 storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b);
+storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ptr a, storm_rational_function_ptr b);
+
+storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ptr a, storm_rational_function_ptr b);
+storm_rational_function_ptr storm_rational_function_min(storm_rational_function_ptr a, storm_rational_function_ptr b);
+storm_rational_function_ptr storm_rational_function_max(storm_rational_function_ptr a, storm_rational_function_ptr b);
+
+int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b);
+int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_rational_function_ptr b);
+
+// unary
 storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a);
+    
+storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a);
+storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a);
+    
 uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed);
 int storm_rational_function_is_zero(storm_rational_function_ptr a);
 
@@ -29,8 +45,6 @@ storm_rational_function_ptr storm_rational_function_get_one();
 void print_storm_rational_function(storm_rational_function_ptr a);
 void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out);
 
-int storm_rational_function_is_zero(storm_rational_function_ptr a);
-
 MTBDD storm_rational_function_leaf_parameter_replacement(MTBDD dd, storm_rational_function_ptr a, void* context);
 
 double storm_rational_function_get_constant(storm_rational_function_ptr a);

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

@@ -308,7 +308,7 @@ _mtbdd_hash_cb(uint64_t a, uint64_t b, uint64_t seed)
     if (type >= cl_registry_count) return llmsset_hash(a, b, seed);
     customleaf_t *c = cl_registry + type;
     if (c->hash_cb == NULL) return llmsset_hash(a, b, seed);
-    return c->hash_cb(b, seed ^ a);
+    return c->hash_cb(b, seed);
 }
 
 static int

resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp

@@ -9,6 +9,14 @@
     Mtbdd Divide(const Mtbdd &other) const;
     
 #if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+
+    Bdd EqualsRF(const Mtbdd& other) const;
+    Bdd LessRF(const Mtbdd& other) const;
+    Bdd LessOrEqualRF(const Mtbdd& other) const;
+
+    Mtbdd MinRF(const Mtbdd& other) const;
+    Mtbdd MaxRF(const Mtbdd& other) const;
+
 	/**
      * @brief Computes f + g for Rational Functions
      */
@@ -18,7 +26,9 @@
      * @brief Computes f * g for Rational Functions
      */
     Mtbdd TimesRF(const Mtbdd &other) const;
-	
+
+    Mtbdd AndExistsRF(const Mtbdd &other, const BddSet &variables) const;
+
 	/**
      * @brief Computes f - g for Rational Functions
      */
@@ -28,11 +38,25 @@
      * @brief Computes f / g for Rational Functions
      */
     Mtbdd DivideRF(const Mtbdd &other) const;
-	
+
+    Mtbdd PowRF(const Mtbdd& other) const;
+
 	Mtbdd AbstractPlusRF(const BddSet &variables) const;
 	
 	Mtbdd ReplaceLeavesRF(void* context) const;
-	
+
+    Mtbdd FloorRF() const;
+    Mtbdd CeilRF() const;
+
+    Mtbdd AbstractMinRF(const BddSet &variables) const;
+    Mtbdd AbstractMaxRF(const BddSet &variables) const;
+
+    Bdd BddThresholdRF(storm::RationalFunction const& rf) const;
+    Bdd BddStrictThresholdRF(storm::RationalFunction const& rf) const;
+
+    Mtbdd MinimumRF() const;
+    Mtbdd MaximumRF() const;
+
 	Mtbdd ToDoubleRF() const;
 #endif
 	

resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp

@@ -23,7 +23,37 @@ Bdd::toStormRationalFunctionMtbdd() const {
     return mtbdd_bool_to_storm_rational_function(bdd);
 }
 
-Mtbdd 
+Bdd
+Mtbdd::EqualsRF(const Mtbdd& other) const {
+    LACE_ME;
+    return mtbdd_equals_rational_function(mtbdd, other.mtbdd);
+}
+
+Bdd
+Mtbdd::LessRF(const Mtbdd& other) const {
+    LACE_ME;
+    return sylvan_storm_rational_function_less(mtbdd, other.mtbdd);
+}
+
+Bdd
+Mtbdd::LessOrEqualRF(const Mtbdd& other) const {
+    LACE_ME;
+    return sylvan_storm_rational_function_less_or_equal(mtbdd, other.mtbdd);
+}
+
+Mtbdd
+Mtbdd::MinRF(const Mtbdd& other) const {
+    LACE_ME;
+    return sylvan_storm_rational_function_min(mtbdd, other.mtbdd);
+}
+
+Mtbdd
+Mtbdd::MaxRF(const Mtbdd& other) const {
+    LACE_ME;
+    return sylvan_storm_rational_function_max(mtbdd, other.mtbdd);
+}
+
+Mtbdd
 Mtbdd::ToDoubleRF() const {
     LACE_ME;
     return sylvan_storm_rational_function_to_double(mtbdd);
@@ -44,6 +74,12 @@ Mtbdd::TimesRF(const Mtbdd &other) const
     return sylvan_storm_rational_function_times(mtbdd, other.mtbdd);
 }
 
+Mtbdd
+Mtbdd::AndExistsRF(const Mtbdd &other, const BddSet &variables) const {
+    LACE_ME;
+    return sylvan_storm_rational_function_and_exists(mtbdd, other.mtbdd, variables.set.bdd);
+}
+
 Mtbdd
 Mtbdd::MinusRF(const Mtbdd &other) const
 {
@@ -58,6 +94,13 @@ Mtbdd::DivideRF(const Mtbdd &other) const
     return sylvan_storm_rational_function_divide(mtbdd, other.mtbdd);
 }
 
+Mtbdd
+Mtbdd::PowRF(const Mtbdd& other) const {
+    LACE_ME;
+    return sylvan_storm_rational_function_pow(mtbdd, other.mtbdd);
+}
+
+
 Mtbdd Mtbdd::AbstractPlusRF(const BddSet &variables) const {
 	LACE_ME;
     return sylvan_storm_rational_function_abstract_plus(mtbdd, variables.set.bdd);
@@ -68,6 +111,53 @@ Mtbdd Mtbdd::ReplaceLeavesRF(void* context) const {
     return sylvan_storm_rational_function_replace_leaves(mtbdd, (size_t)context);
 }
 
+
+Mtbdd
+Mtbdd::FloorRF() const {
+    LACE_ME;
+    return sylvan_storm_rational_function_floor(mtbdd);
+}
+
+Mtbdd
+Mtbdd::CeilRF() const {
+    LACE_ME;
+    return sylvan_storm_rational_function_ceil(mtbdd);
+}
+
+Mtbdd Mtbdd::AbstractMinRF(const BddSet &variables) const {
+    LACE_ME;
+    return sylvan_storm_rational_function_abstract_min(mtbdd, variables.set.bdd);
+}
+
+Mtbdd Mtbdd::AbstractMaxRF(const BddSet &variables) const {
+    LACE_ME;
+    return sylvan_storm_rational_function_abstract_max(mtbdd, variables.set.bdd);
+}
+
+Bdd
+Mtbdd::BddStrictThresholdRF(storm::RationalFunction const& rf) const {
+    LACE_ME;
+    return sylvan_storm_rational_function_strict_threshold(mtbdd, (void*)&rf);
+}
+
+Bdd
+Mtbdd::BddThresholdRF(storm::RationalFunction const& rf) const {
+    LACE_ME;
+    return sylvan_storm_rational_function_threshold(mtbdd, (void*)&rf);
+}
+
+Mtbdd
+Mtbdd::MinimumRF() const {
+    LACE_ME;
+    return sylvan_storm_rational_function_minimum(mtbdd);
+}
+
+Mtbdd
+Mtbdd::MaximumRF() const {
+    LACE_ME;
+    return sylvan_storm_rational_function_maximum(mtbdd);
+}
+
 #endif
 
 Mtbdd

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

@@ -38,6 +38,11 @@ int depth = 0;
 //}
 #endif
 
+storm_rational_function_ptr mtbdd_getstorm_rational_function_ptr(MTBDD terminal) {
+    uint64_t value = mtbdd_getvalue(terminal);
+    return (storm_rational_function_ptr*)value;
+}
+
 static uint64_t
 sylvan_storm_rational_function_hash(const uint64_t v, const uint64_t seed)
 {
@@ -111,7 +116,10 @@ sylvan_storm_rational_function_destroy(uint64_t val)
 }
 
 static uint32_t sylvan_storm_rational_function_type;
-static uint64_t CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS;
+
+static uint64_t CACHE_MTBDD_AND_EXISTS_RF;
+static uint64_t CACHE_MTBDD_MINIMUM_RF;
+static uint64_t CACHE_MTBDD_MAXIMUM_RF;
 
 /**
  * Initialize storm::RationalFunction custom leaves
@@ -123,11 +131,13 @@ sylvan_storm_rational_function_init()
     sylvan_storm_rational_function_type = mtbdd_register_custom_leaf(sylvan_storm_rational_function_hash, sylvan_storm_rational_function_equals, sylvan_storm_rational_function_create, sylvan_storm_rational_function_destroy);
 	
 	if (SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID != sylvan_storm_rational_function_type) {
-		printf("ERROR - ERROR - ERROR\nThe Sylvan Type ID is NOT correct.\nIt was assumed to be %u, but it is actually %u!\nYou NEED to fix this by changing the macro \"SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\" and recompiling StoRM!\n\n", SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID, sylvan_storm_rational_function_type);
+		printf("ERROR - ERROR - ERROR\nThe Sylvan Type ID is NOT correct.\nIt was assumed to be %u, but it is actually %u!\nYou NEED to fix this by changing the macro \"SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\" and recompiling Storm!\n\n", SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID, sylvan_storm_rational_function_type);
 		assert(0);
 	}	
 	
-	CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS = cache_next_opid();
+	CACHE_MTBDD_AND_EXISTS_RF = cache_next_opid();
+    CACHE_MTBDD_MINIMUM_RF = cache_next_opid();
+    CACHE_MTBDD_MAXIMUM_RF = cache_next_opid();
 }
 
 uint32_t sylvan_storm_rational_function_get_type() {
@@ -184,6 +194,35 @@ TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD, dd)
     return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_storm_rational_function), 0);
 }
 
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_equals, MTBDD*, pa, MTBDD*, pb)
+{
+    LOG_I("task_impl_2 op_equals")
+    MTBDD a = *pa, b = *pb;
+    
+    /* Check for partial functions */
+    if (a == mtbdd_false) return b;
+    if (b == mtbdd_false) return a;
+    
+    /* If both leaves, compute plus */
+    if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) {
+        storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
+        storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b);
+        if (storm_rational_function_equals(ma, mb)) {
+            return mtbdd_true;
+        } else {
+            return mtbdd_false;   
+        }
+    }
+    
+    /* Commutative, so swap a,b for better cache performance */
+    if (a < b) {
+        *pa = b;
+        *pb = a;
+    }
+    
+    return mtbdd_invalid;
+}
+
 /**
  * Operation "plus" for two storm::RationalFunction MTBDDs
  * Interpret partial function as "0"
@@ -302,11 +341,14 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*,
     /* Handle division of leaves */
     if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) {
 		storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
-		storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b);
-
-		storm_rational_function_ptr mres = storm_rational_function_divide(ma, mb);
+        storm_rational_function_ptr mres;
+        if (storm_rational_function_is_zero(ma)) {
+            mres = storm_rational_function_get_zero();
+        } else {
+            storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b);
+            mres = storm_rational_function_divide(ma, mb);
+        }
 		MTBDD res = mtbdd_storm_rational_function(mres);
-
 		storm_rational_function_destroy(mres);
 
         return res;
@@ -315,6 +357,216 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*,
     return mtbdd_invalid;
 }
 
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_less, MTBDD*, pa, MTBDD*, pb)
+{
+    LOG_I("task_impl_2 op_less")
+    MTBDD a = *pa, b = *pb;
+    
+    /* Check for partial functions and for Boolean (filter) */
+    if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false;
+    
+    /* If one of Boolean, interpret as filter */
+    if (a == mtbdd_true) return b;
+    if (b == mtbdd_true) return a;
+    
+    /* Handle multiplication of leaves */
+    if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) {
+        storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
+        storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b);
+        
+        if (storm_rational_function_less(ma, mb)) {
+            return mtbdd_true;
+        } else {
+            return mtbdd_false;
+        }
+    }
+    
+    return mtbdd_invalid;
+}
+
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_less_or_equal, MTBDD*, pa, MTBDD*, pb)
+{
+    LOG_I("task_impl_2 op_less_or_equal")
+    MTBDD a = *pa, b = *pb;
+    
+    /* Check for partial functions and for Boolean (filter) */
+    if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false;
+    
+    /* If one of Boolean, interpret as filter */
+    if (a == mtbdd_true) return b;
+    if (b == mtbdd_true) return a;
+    
+    /* Handle multiplication of leaves */
+    if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) {
+        storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
+        storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b);
+        
+        if (storm_rational_function_less_or_equal(ma, mb)) {
+            return mtbdd_true;
+        } else {
+            return mtbdd_false;
+        }
+    }
+    
+    return mtbdd_invalid;
+}
+
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_mod, MTBDD*, pa, MTBDD*, pb)
+{
+    LOG_I("task_impl_2 op_mod")
+    MTBDD a = *pa, b = *pb;
+    
+    /* Check for partial functions and for Boolean (filter) */
+    if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false;
+    
+    /* If one of Boolean, interpret as filter */
+    if (a == mtbdd_true) return b;
+    if (b == mtbdd_true) return a;
+    
+    /* Handle multiplication of leaves */
+    if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) {
+        storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
+        storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b);
+        
+        storm_rational_function_ptr mres = storm_rational_function_mod(ma, mb);
+        MTBDD res = mtbdd_storm_rational_function(mres);
+        
+        storm_rational_function_destroy(mres);
+        
+        return res;
+    }
+    
+    return mtbdd_invalid;
+}
+
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_min, MTBDD*, pa, MTBDD*, pb)
+{
+    LOG_I("task_impl_2 op_mod")
+    MTBDD a = *pa, b = *pb;
+    
+    /* Check for partial functions and for Boolean (filter) */
+    if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false;
+    
+    /* If one of Boolean, interpret as filter */
+    if (a == mtbdd_true) return b;
+    if (b == mtbdd_true) return a;
+    
+    /* Handle multiplication of leaves */
+    if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) {
+        storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
+        storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b);
+        
+        storm_rational_function_ptr mres = storm_rational_function_min(ma, mb);
+        MTBDD res = mtbdd_storm_rational_function(mres);
+        
+        storm_rational_function_destroy(mres);
+        
+        return res;
+    }
+    
+    /* Commutative, so make "a" the lowest for better cache performance */
+    if (a < b) {
+        *pa = b;
+        *pb = a;
+    }
+    
+    return mtbdd_invalid;
+}
+
+TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_min, MTBDD, a, MTBDD, b, int, k)
+{
+    LOG_I("task_impl_3 abstract_op_min")
+    if (k==0) {
+        return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_min));
+    } else {
+        MTBDD res = a;
+        for (int i=0; i<k; i++) {
+            mtbdd_refs_push(res);
+            res = mtbdd_apply(res, res, TASK(sylvan_storm_rational_function_op_min));
+            mtbdd_refs_pop(1);
+        }
+        return res;
+    }
+}
+
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_max, MTBDD*, pa, MTBDD*, pb)
+{
+    LOG_I("task_impl_2 op_mod")
+    MTBDD a = *pa, b = *pb;
+    
+    /* Check for partial functions and for Boolean (filter) */
+    if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false;
+    
+    /* If one of Boolean, interpret as filter */
+    if (a == mtbdd_true) return b;
+    if (b == mtbdd_true) return a;
+    
+    /* Handle multiplication of leaves */
+    if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) {
+        storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
+        storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b);
+        
+        storm_rational_function_ptr mres = storm_rational_function_max(ma, mb);
+        MTBDD res = mtbdd_storm_rational_function(mres);
+        
+        storm_rational_function_destroy(mres);
+        
+        return res;
+    }
+    
+    /* Commutative, so make "a" the lowest for better cache performance */
+    if (a < b) {
+        *pa = b;
+        *pb = a;
+    }
+    
+    return mtbdd_invalid;
+}
+
+TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_max, MTBDD, a, MTBDD, b, int, k)
+{
+    LOG_I("task_impl_3 abstract_op_max")
+    if (k==0) {
+        return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_max));
+    } else {
+        MTBDD res = a;
+        for (int i=0; i<k; i++) {
+            mtbdd_refs_push(res);
+            res = mtbdd_apply(res, res, TASK(sylvan_storm_rational_function_op_max));
+            mtbdd_refs_pop(1);
+        }
+        return res;
+    }
+}
+
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_pow, MTBDD*, pa, MTBDD*, pb)
+{
+    LOG_I("task_impl_2 op_pow")
+    MTBDD a = *pa, b = *pb;
+    
+    /* Check for partial functions and for Boolean (filter) */
+    if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false;
+    
+    /* If one of Boolean, interpret as filter */
+    if (a == mtbdd_true) return b;
+    if (b == mtbdd_true) return a;
+    
+    /* Handle multiplication of leaves */
+    if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) {
+        storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
+        storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b);
+        
+        storm_rational_function_ptr mres = storm_rational_function_pow(ma, mb);
+        MTBDD res = mtbdd_storm_rational_function(mres);
+        
+        storm_rational_function_destroy(mres);
+        
+        return res;
+    }
+    
+    return mtbdd_invalid;
+}
+
 /**
  * The abstraction operators are called in either of two ways:
  * - with k=0, then just calculate "a op b"
@@ -378,6 +630,50 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, dd, size_t, p)
     (void)p;
 }
 
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_floor, MTBDD, dd, size_t, p)
+{
+    LOG_I("task_impl_2 op_neg")
+    /* Handle partial functions */
+    if (dd == mtbdd_false) return mtbdd_false;
+    
+    /* Compute result for leaf */
+    if (mtbdd_isleaf(dd)) {
+        storm_rational_function_ptr mdd = (storm_rational_function_ptr)mtbdd_getvalue(dd);
+        
+        storm_rational_function_ptr mres = storm_rational_function_floor(mdd);
+        MTBDD res = mtbdd_storm_rational_function(mres);
+        
+        storm_rational_function_destroy(mres);
+        
+        return res;
+    }
+    
+    return mtbdd_invalid;
+    (void)p;
+}
+
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_ceil, MTBDD, dd, size_t, p)
+{
+    LOG_I("task_impl_2 op_neg")
+    /* Handle partial functions */
+    if (dd == mtbdd_false) return mtbdd_false;
+    
+    /* Compute result for leaf */
+    if (mtbdd_isleaf(dd)) {
+        storm_rational_function_ptr mdd = (storm_rational_function_ptr)mtbdd_getvalue(dd);
+        
+        storm_rational_function_ptr mres = storm_rational_function_ceil(mdd);
+        MTBDD res = mtbdd_storm_rational_function(mres);
+        
+        storm_rational_function_destroy(mres);
+        
+        return res;
+    }
+    
+    return mtbdd_invalid;
+    (void)p;
+}
+
 /**
  * Operation "replace leaves" for one storm::RationalFunction MTBDD
  */
@@ -451,7 +747,7 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, a, MTBDD, b
     sylvan_gc_test();
 
     /* Check cache. Note that we do this now, since the times operator might swap a and b (commutative) */
-    if (cache_get3(CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS, a, b, v, &result)) return result;
+    if (cache_get3(CACHE_MTBDD_AND_EXISTS_RF, a, b, v, &result)) return result;
 
     /* Now, v is not a constant, and either a or b is not a constant */
 
@@ -499,7 +795,7 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, a, MTBDD, b
     }
 
     /* Store in cache */
-    cache_put3(CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS, a, b, v, result);
+    cache_put3(CACHE_MTBDD_AND_EXISTS_RF, a, b, v, result);
     return result;
 }
 
@@ -539,3 +835,121 @@ TASK_IMPL_3(MTBDD, mtbdd_uapply_nocache, MTBDD, dd, mtbdd_uapply_op, op, size_t,
     //cache_put3(CACHE_MTBDD_UAPPLY, dd, (size_t)op, param, result);
     return result;
 }
+
+/**
+ * Monad that converts double/fraction to a Boolean MTBDD, translate terminals >= value to 1 and to 0 otherwise;
+ */
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, a, size_t, svalue)
+{
+    LOG_I("task_impl_2 op_threshold")
+    storm_rational_function_ptr value = (storm_rational_function_ptr)svalue;
+    
+    if (mtbdd_isleaf(a)) {
+        storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
+        
+        if (storm_rational_function_less_or_equal(ma, value)) {
+            return mtbdd_false;
+        } else {
+            return mtbdd_true;
+        }
+    }
+    
+    return mtbdd_invalid;
+}
+
+/**
+ * Monad that converts double/fraction to a Boolean BDD, translate terminals > value to 1 and to 0 otherwise;
+ */
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, a, size_t, svalue)
+{
+    LOG_I("task_impl_2 op_strict_threshold")
+    storm_rational_function_ptr value = (storm_rational_function_ptr)svalue;
+
+    if (mtbdd_isleaf(a)) {
+        storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a);
+        
+        if (storm_rational_function_less(ma, value)) {
+            return mtbdd_false;
+        } else {
+            return mtbdd_true;
+        }
+    }
+    
+    return mtbdd_invalid;
+}
+
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_threshold, MTBDD, dd, storm_rational_function_ptr, value)
+{
+    return mtbdd_uapply(dd, TASK(sylvan_storm_rational_function_op_threshold), *(size_t*)value);
+}
+
+TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_strict_threshold, MTBDD, dd, storm_rational_function_ptr, value)
+{
+    return mtbdd_uapply(dd, TASK(sylvan_storm_rational_function_op_strict_threshold), *(size_t*)value);
+}
+
+TASK_IMPL_1(MTBDD, sylvan_storm_rational_function_minimum, MTBDD, a)
+{
+    /* Check terminal case */
+    if (a == mtbdd_false) return mtbdd_false;
+    mtbddnode_t na = MTBDD_GETNODE(a);
+    if (mtbddnode_isleaf(na)) return a;
+    
+    /* Maybe perform garbage collection */
+    sylvan_gc_test();
+    
+    /* Check cache */
+    MTBDD result;
+    if (cache_get3(CACHE_MTBDD_MINIMUM_RF, a, 0, 0, &result)) return result;
+    
+    /* Call recursive */
+    SPAWN(mtbdd_minimum, node_getlow(a, na));
+    MTBDD high = CALL(sylvan_storm_rational_function_minimum, node_gethigh(a, na));
+    MTBDD low = SYNC(sylvan_storm_rational_function_minimum);
+    
+    storm_rational_function_ptr fl = mtbdd_getstorm_rational_function_ptr(low);
+    storm_rational_function_ptr fh = mtbdd_getstorm_rational_function_ptr(high);
+    
+    if (storm_rational_function_less_or_equal(fl, fh)) {
+        return low;
+    } else {
+        return high;
+    }
+    
+    /* Store in cache */
+    cache_put3(CACHE_MTBDD_MINIMUM_RF, a, 0, 0, result);
+    return result;
+}
+
+TASK_IMPL_1(MTBDD, sylvan_storm_rational_function_maximum, MTBDD, a)
+{
+    /* Check terminal case */
+    if (a == mtbdd_false) return mtbdd_false;
+    mtbddnode_t na = MTBDD_GETNODE(a);
+    if (mtbddnode_isleaf(na)) return a;
+    
+    /* Maybe perform garbage collection */
+    sylvan_gc_test();
+    
+    /* Check cache */
+    MTBDD result;
+    if (cache_get3(CACHE_MTBDD_MAXIMUM_RF, a, 0, 0, &result)) return result;
+    
+    /* Call recursive */
+    SPAWN(mtbdd_minimum, node_getlow(a, na));
+    MTBDD high = CALL(sylvan_storm_rational_function_maximum, node_gethigh(a, na));
+    MTBDD low = SYNC(sylvan_storm_rational_function_maximum);
+    
+    storm_rational_function_ptr fl = mtbdd_getstorm_rational_function_ptr(low);
+    storm_rational_function_ptr fh = mtbdd_getstorm_rational_function_ptr(high);
+    
+    if (storm_rational_function_less(fl, fh)) {
+        return high;
+    } else {
+        return low;
+    }
+    
+    /* Store in cache */
+    cache_put3(CACHE_MTBDD_MAXIMUM_RF, a, 0, 0, result);
+    return result;
+}

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

@@ -33,6 +33,8 @@ uint32_t sylvan_storm_rational_function_get_type();
  */
 MTBDD mtbdd_storm_rational_function(storm_rational_function_ptr val);
 
+storm_rational_function_ptr mtbdd_getstorm_rational_function_ptr(MTBDD terminal);
+    
 /**
  * Monad that converts Boolean to a storm::RationalFunction MTBDD, translate terminals true to 1 and to 0 otherwise;
  */
@@ -40,6 +42,10 @@ TASK_DECL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, size_t)
 TASK_DECL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD)
 #define mtbdd_bool_to_storm_rational_function(dd) CALL(mtbdd_bool_to_storm_rational_function, dd)
 
+// Operation "equals"
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_equals, MTBDD*, MTBDD*)
+#define mtbdd_equals_rational_function(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_equals))
+    
 /**
  * Operation "plus" for two storm::RationalFunction MTBDDs
  */
@@ -62,11 +68,23 @@ TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, MTBD
  */
 TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, MTBDD*)
 
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_less, MTBDD*, MTBDD*)
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_less_or_equal, MTBDD*, MTBDD*)
+
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_mod, MTBDD*, MTBDD*)
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_min, MTBDD*, MTBDD*)
+TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_min, MTBDD, MTBDD, int)
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_max, MTBDD*, MTBDD*)
+TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_max, MTBDD, MTBDD, int)
+
 /**
  * Operation "negate" for one storm::RationalFunction MTBDD
  */
 TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, size_t)
 
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_floor, MTBDD, size_t)
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_ceil, MTBDD, size_t)
+
 /**
  * Compute a + b
  */
@@ -87,11 +105,53 @@ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, size_t)
  */
 #define sylvan_storm_rational_function_divide(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_divide))
 
+/**
+ * Compute a < b
+ */
+#define sylvan_storm_rational_function_less(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_less))
+
+/**
+ * Compute a <= b
+ */
+#define sylvan_storm_rational_function_less_or_equal(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_less_or_equal))
+
+/**
+ * Compute a mod b
+ */
+#define sylvan_storm_rational_function_mod(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_less_or_equal))
+
+/**
+ * Compute min(a, b)
+ */
+#define sylvan_storm_rational_function_min(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_min))
+
+/**
+ * Compute max(a, b)
+ */
+#define sylvan_storm_rational_function_max(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_max))
+
 /**
  * Compute -a
  */
 #define sylvan_storm_rational_function_neg(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_neg), 0)
 
+/**
+ * Compute floor(a)
+ */
+#define sylvan_storm_rational_function_floor(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_floor), 0)
+
+/**
+ * Compute ceil(a)
+ */
+#define sylvan_storm_rational_function_ceil(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_ceil), 0)
+
+/**
+ * Compute a^b
+ */
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_pow, MTBDD*, MTBDD*)
+#define sylvan_storm_rational_function_pow(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_pow))
+
+    
 /**
  * Multiply <a> and <b>, and abstract variables <vars> using summation.
  * This is similar to the "and_exists" operation in BDDs.
@@ -103,7 +163,9 @@ TASK_DECL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, MTBDD, MTBD
  * Abstract the variables in <v> from <a> by taking the sum of all values
  */
 #define sylvan_storm_rational_function_abstract_plus(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_plus))
-
+#define sylvan_storm_rational_function_abstract_min(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_min))
+#define sylvan_storm_rational_function_abstract_max(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_max))
+    
 /**
  * Apply a unary operation <op> to <dd>.
  * Callback <op> is consulted after the cache, thus the application to a terminal is cached.
@@ -135,6 +197,24 @@ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_to_double, MTBDD, size_t)
  */
 #define sylvan_storm_rational_function_to_double(a) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_function_op_to_double), 0)
 
+    
+TASK_DECL_1(MTBDD, sylvan_storm_rational_function_minimum, MTBDD);
+#define sylvan_storm_rational_function_minimum(dd) CALL(sylvan_storm_rational_function_minimum, dd)
+    
+TASK_DECL_1(MTBDD, sylvan_storm_rational_function_maximum, MTBDD);
+#define sylvan_storm_rational_function_maximum(dd) CALL(sylvan_storm_rational_function_maximum, dd)
+
+    
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, size_t)
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, size_t)
+
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_threshold, MTBDD, storm_rational_function_ptr);
+#define sylvan_storm_rational_function_threshold(dd, value) CALL(sylvan_storm_rational_function_strict_threshold, dd, value)
+    
+
+TASK_DECL_2(MTBDD, sylvan_storm_rational_function_strict_threshold, MTBDD, storm_rational_function_ptr);
+#define sylvan_storm_rational_function_strict_threshold(dd, value) CALL(sylvan_storm_rational_function_strict_threshold, dd, value)
+    
 #ifdef __cplusplus
 }
 #endif /* __cplusplus */

src/storm/adapters/AddExpressionAdapter.cpp

@@ -34,6 +34,11 @@ namespace storm {
             return boost::any_cast<storm::dd::Bdd<Type>>(expression.accept(*this, boost::none));
         }
         
+        template<storm::dd::DdType Type, typename ValueType>
+        void AddExpressionAdapter<Type, ValueType>::setValue(storm::expressions::Variable const& variable, ValueType const& value) {
+            valueMapping[variable] = value;
+        }
+        
         template<storm::dd::DdType Type, typename ValueType>
         boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) {
             if (expression.hasBooleanType()) {
@@ -143,12 +148,17 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ValueType>
         boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::VariableExpression const& expression, boost::any const&) {
-            auto const& variablePair = variableMapping->find(expression.getVariable());
-            STORM_LOG_THROW(variablePair != variableMapping->end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains the variable '" << expression.getVariableName() << "' for which no DD counterpart is known.");
-            if (expression.hasBooleanType()) {
-                return ddManager->template getIdentity<ValueType>(variablePair->second).toBdd();
+            auto valueIt = valueMapping.find(expression.getVariable());
+            if (valueIt != valueMapping.end()) {
+                return ddManager->getConstant(valueIt->second);
             } else {
-                return ddManager->template getIdentity<ValueType>(variablePair->second);
+                auto const& variablePair = variableMapping->find(expression.getVariable());
+                STORM_LOG_THROW(variablePair != variableMapping->end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains the variable '" << expression.getVariableName() << "' for which no DD counterpart is known.");
+                if (expression.hasBooleanType()) {
+                    return ddManager->template getIdentity<ValueType>(variablePair->second).toBdd();
+                } else {
+                    return ddManager->template getIdentity<ValueType>(variablePair->second);
+                }
             }
         }
         

src/storm/adapters/AddExpressionAdapter.h

@@ -21,7 +21,9 @@ namespace storm {
             
             storm::dd::Add<Type, ValueType> translateExpression(storm::expressions::Expression const& expression);
             storm::dd::Bdd<Type> translateBooleanExpression(storm::expressions::Expression const& expression);
-            
+
+            void setValue(storm::expressions::Variable const& variable, ValueType const& value);
+
             virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) override;
             virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) override;
             virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) override;
@@ -32,13 +34,16 @@ namespace storm {
             virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) override;
             virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) override;
             virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) override;
-
+            
         private:
             // The manager responsible for the DDs built by this adapter.
             std::shared_ptr<storm::dd::DdManager<Type>> ddManager;
             
             // This member maps the variables used in the expressions to the variables used by the DD manager.
             std::shared_ptr<std::map<storm::expressions::Variable, storm::expressions::Variable>> variableMapping;
+            
+            // A mapping of variables to their values (if set).
+            std::unordered_map<storm::expressions::Variable, ValueType> valueMapping;
         };
         
     } // namespace adapters

src/storm/adapters/EigenAdapter.h

@@ -36,8 +36,8 @@ namespace std {
     struct hash<StormEigen::Matrix<ValueType, StormEigen::Dynamic, 1>> {
         std::size_t operator()(StormEigen::Matrix<ValueType, StormEigen::Dynamic, 1> const &vector) const {
             size_t seed = 0;
-            for (uint_fast64_t i = 0; i < vector.rows(); ++i) {
-                carl::hash_add(seed,  std::hash<ValueType>()(vector(i)));
+            for (uint_fast64_t i = 0; i < static_cast<uint_fast64_t>(vector.rows()); ++i) {
+                carl::hash_add(seed, std::hash<ValueType>()(vector(i)));
             }
             return seed;
         }

src/storm/builder/DdJaniModelBuilder.cpp

@@ -1845,7 +1845,7 @@ namespace storm {
         
         template <storm::dd::DdType Type, typename ValueType>
         std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::build(storm::jani::Model const& model, Options const& options) {
-            if (model.hasUndefinedConstants()) {
+            if (!std::is_same<ValueType, storm::RationalFunction>::value && model.hasUndefinedConstants()) {
                 std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = model.getUndefinedConstants();
                 std::vector<std::string> strings;
                 for (auto const& constant : undefinedConstants) {

src/storm/builder/DdPrismModelBuilder.cpp

@@ -31,12 +31,60 @@
 namespace storm {
     namespace builder {
         
+        template <storm::dd::DdType Type, typename ValueType>
+        class ParameterCreator {
+        public:
+            void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter<Type, ValueType>& rowExpressionAdapter, storm::adapters::AddExpressionAdapter<Type, ValueType>& columnExpressionAdapter) {
+                // Intentionally left empty: no support for parameters for this data type.
+            }
+        };
+        
+        template <storm::dd::DdType Type>
+        class ParameterCreator<Type, storm::RationalFunction> {
+        public:
+            ParameterCreator() : cache(std::make_shared<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>>()) {
+                // Intentionally left empty.
+            }
+            
+            void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter<Type, storm::RationalFunction>& rowExpressionAdapter, storm::adapters::AddExpressionAdapter<Type, storm::RationalFunction>& columnExpressionAdapter) {
+                for (auto const& constant : program.getConstants()) {
+                    if (!constant.isDefined()) {
+                        carl::Variable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName());
+                        auto rf = convertVariableToPolynomial(carlVariable);
+                        rowExpressionAdapter.setValue(constant.getExpressionVariable(), rf);
+                        columnExpressionAdapter.setValue(constant.getExpressionVariable(), rf);
+                    }
+                }
+            }
+            
+            template<typename RationalFunctionType = storm::RationalFunction, typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
+            RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
+                return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::PolyType::PolyType(variable), cache));
+            }
+            
+            template<typename RationalFunctionType = storm::RationalFunction, typename TP = typename RationalFunctionType::PolyType, carl::DisableIf<carl::needs_cache<TP>> = carl::dummy>
+            RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
+                return RationalFunctionType(variable);
+            }
+            
+            // A mapping from our variables to carl's.
+            std::unordered_map<storm::expressions::Variable, carl::Variable> variableToVariableMap;
+            
+            // The cache that is used in case the underlying type needs a cache.
+            std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
+        };
+        
         template <storm::dd::DdType Type, typename ValueType>
         class DdPrismModelBuilder<Type, ValueType>::GenerationInformation {
         public:
             GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared<storm::dd::DdManager<Type>>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>()), rowExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>())), columnExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() {
+                
                 // Initializes variables and identity DDs.
                 createMetaVariablesAndIdentities();
+                
+                // Initialize the parameters (if any).
+                ParameterCreator<Type, ValueType> parameterCreator;
+                parameterCreator.create(this->program, *this->rowExpressionAdapter, *this->columnExpressionAdapter);
             }
             
             // The program that is currently translated.
@@ -84,6 +132,10 @@ namespace storm {
             std::map<std::string, storm::dd::Add<Type, ValueType>> moduleToRangeMap;
             
         private:
+            void createParameters() {
+                
+            }
+            
             /*!
              * Creates the required meta variables and variable/module identities.
              */
@@ -663,6 +715,8 @@ namespace storm {
                     commandDd += updateResultsIt->updateDd * probabilityDd;
                 }
                 
+                commandDd.exportToDot("command.dot");
+                
                 return ActionDecisionDiagram(guard, guard.template toAdd<ValueType>() * commandDd, globalVariablesInSomeUpdate);
             } else {
                 return ActionDecisionDiagram(*generationInfo.manager);
@@ -1245,7 +1299,7 @@ namespace storm {
         
         template <storm::dd::DdType Type, typename ValueType>
         std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdPrismModelBuilder<Type, ValueType>::build(storm::prism::Program const& program, Options const& options) {
-            if (program.hasUndefinedConstants()) {
+            if (!std::is_same<ValueType, storm::RationalFunction>::value && program.hasUndefinedConstants()) {
                 std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = program.getUndefinedConstants();
                 std::stringstream stream;
                 bool printComma = false;
@@ -1342,6 +1396,8 @@ namespace storm {
             storm::dd::Bdd<Type> statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables);
             storm::dd::Bdd<Type> deadlockStates = reachableStates && !statesWithTransition;
             
+            transitionMatrix.exportToDot("trans.dot");
+            
             // If there are deadlocks, either fix them or raise an error.
             if (!deadlockStates.isZero()) {
                 // If we need to fix deadlocks, we do so now.

src/storm/cli/entrypoints.h

@@ -381,12 +381,11 @@ namespace storm {
                 auto ddlib = storm::settings::getModule<storm::settings::modules::CoreSettings>().getDdLibraryType();
                 STORM_LOG_THROW(ddlib == storm::dd::DdType::Sylvan, storm::exceptions::InvalidSettingsException, "This data-type is only available when selecting sylvan.");
                 buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::Sylvan, storm::RationalFunction>(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, model, formulas, onlyInitialStatesRelevant);
-            } else {
-                STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Illegal engine.");
+            } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
                 buildAndCheckSymbolicModelWithSparseEngine<storm::RationalFunction>(model, formulas, onlyInitialStatesRelevant);
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot use this data type with this engine.");
             }
-         
-            STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot use this data type with this engine.");
         }
 #endif
         

src/storm/modelchecker/AbstractModelChecker.cpp

@@ -316,9 +316,12 @@ namespace storm {
         // DD
         template class AbstractModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>;
         template class AbstractModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>;
+        template class AbstractModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
         template class AbstractModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;
         template class AbstractModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>;
+        template class AbstractModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
         template class AbstractModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double>>;
         template class AbstractModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double>>;
+        template class AbstractModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
     }
 }

src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp

@@ -118,5 +118,7 @@ namespace storm {
         
         template class HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>;
         template class HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>;
+
+        template class HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
     }
 }

src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp

@@ -28,7 +28,7 @@ namespace storm {
         }
         
         template<typename ModelType>
-        SymbolicDtmcPrctlModelChecker<ModelType>::SymbolicDtmcPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>()) {
+        SymbolicDtmcPrctlModelChecker<ModelType>::SymbolicDtmcPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker<ModelType>(model), linearEquationSolverFactory(std::make_unique<storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType>>()) {
             // Intentionally left empty.
         }
         
@@ -45,8 +45,8 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
-            return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
+            storm::dd::Add<DdType, ValueType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
+            return std::make_unique<SymbolicQuantitativeCheckResult<DdType, ValueType>>(this->getModel().getReachableStates(), numericResult);
         }
         
         template<typename ModelType>
@@ -54,8 +54,8 @@ namespace storm {
             storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula();
             std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
             SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
-            return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
+            storm::dd::Add<DdType, ValueType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
+            return std::make_unique<SymbolicQuantitativeCheckResult<DdType, ValueType>>(this->getModel().getReachableStates(), numericResult);
         }
         
         template<typename ModelType>
@@ -63,8 +63,8 @@ namespace storm {
             storm::logic::NextFormula const& pathFormula = checkTask.getFormula();
             std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
             SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
-            return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
+            storm::dd::Add<DdType, ValueType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
+            return std::make_unique<SymbolicQuantitativeCheckResult<DdType, ValueType>>(this->getModel().getReachableStates(), numericResult);
         }
                 
         template<typename ModelType>
@@ -76,24 +76,24 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
-            return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
+            storm::dd::Add<DdType, ValueType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound<uint64_t>() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            return std::make_unique<SymbolicQuantitativeCheckResult<DdType, ValueType>>(this->getModel().getReachableStates(), numericResult);
         }
         
         template<typename ModelType>
         std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
-            return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
+            storm::dd::Add<DdType, ValueType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory);
+            return std::make_unique<SymbolicQuantitativeCheckResult<DdType, ValueType>>(this->getModel().getReachableStates(), numericResult);
         }
         
         template<typename ModelType>
         std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<ModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) {
             storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>(), *this->linearEquationSolverFactory);
-            return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
+            storm::dd::Add<DdType, ValueType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound<uint64_t>(), *this->linearEquationSolverFactory);
+            return std::make_unique<SymbolicQuantitativeCheckResult<DdType, ValueType>>(this->getModel().getReachableStates(), numericResult);
         }
         
         template<typename ModelType>
@@ -101,12 +101,14 @@ namespace storm {
             storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
-            return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
+            storm::dd::Add<DdType, ValueType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
+            return std::make_unique<SymbolicQuantitativeCheckResult<DdType, ValueType>>(this->getModel().getReachableStates(), numericResult);
         }
 
 
         template class SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>;
         template class SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>;
+
+        template class SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
     }
 }

src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp

@@ -39,7 +39,7 @@ namespace storm {
                 // Check whether we need to compute exact probabilities for some states.
                 if (qualitative) {
                     // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
-                    return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), statesWithProbability01.second.template toAdd<ValueType>() + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(0.5)));
+                    return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), statesWithProbability01.second.template toAdd<ValueType>() + maybeStates.template toAdd<ValueType>() * model.getManager().template getConstant<ValueType>(storm::utility::convertNumber<ValueType>(0.5))));
                 } else {
                     // If there are maybe states, we need to solve an equation system.
                     if (!maybeStates.isZero()) {
@@ -77,9 +77,9 @@ namespace storm {
                         solver->solveEquations(x, b);
                         
                         // Return a hybrid check result that stores the numerical values explicitly.
-                        return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.template toAdd<ValueType>(), maybeStates, odd, x));
+                        return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.template toAdd<ValueType>(), maybeStates, odd, x));
                     } else {
-                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), statesWithProbability01.second.template toAdd<ValueType>()));
+                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), statesWithProbability01.second.template toAdd<ValueType>()));
                     }
                 }
             }
@@ -94,7 +94,7 @@ namespace storm {
             template<storm::dd::DdType DdType, typename ValueType>
             std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeNextProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates) {
                 storm::dd::Add<DdType, ValueType> result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>();
-                return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), result.sumAbstract(model.getColumnVariables())));
+                return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), result.sumAbstract(model.getColumnVariables())));
             }
 
             template<storm::dd::DdType DdType, typename ValueType>
@@ -135,9 +135,9 @@ namespace storm {
                     solver->repeatedMultiply(x, &b, stepBound);
                     
                     // Return a hybrid check result that stores the numerical values explicitly.
-                    return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.template toAdd<ValueType>(), maybeStates, odd, x));
+                    return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.template toAdd<ValueType>(), maybeStates, odd, x));
                 } else {
-                    return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), psiStates.template toAdd<ValueType>()));
+                    return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), psiStates.template toAdd<ValueType>()));
                 }
             }
 
@@ -160,7 +160,7 @@ namespace storm {
                 solver->repeatedMultiply(x, nullptr, stepBound);
                 
                 // Return a hybrid check result that stores the numerical values explicitly.
-                return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), odd, x));
+                return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), odd, x));
             }
             
             template<storm::dd::DdType DdType, typename ValueType>
@@ -186,7 +186,7 @@ namespace storm {
                 solver->repeatedMultiply(x, &b, stepBound);
                 
                 // Return a hybrid check result that stores the numerical values explicitly.
-                return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), odd, x));
+                return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), odd, x));
             }
             
             template<storm::dd::DdType DdType, typename ValueType>
@@ -207,7 +207,7 @@ namespace storm {
                 if (qualitative) {
                     // Set the values for all maybe-states to 1 to indicate that their reward values
                     // are neither 0 nor infinity.
-                    return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()) + maybeStates.template toAdd<ValueType>() * model.getManager().template getAddOne<ValueType>()));
+                    return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()) + maybeStates.template toAdd<ValueType>() * model.getManager().template getAddOne<ValueType>()));
                 } else {
                     // If there are maybe states, we need to solve an equation system.
                     if (!maybeStates.isZero()) {
@@ -242,9 +242,9 @@ namespace storm {
                         solver->solveEquations(x, b);
                         
                         // Return a hybrid check result that stores the numerical values explicitly.
-                        return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()), maybeStates, odd, x));
+                        return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()), maybeStates, odd, x));
                     } else {
-                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>())));
+                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>())));
                     }
                 }
             }
@@ -256,7 +256,7 @@ namespace storm {
                 storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd);
 
                 std::vector<ValueType> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeLongRunAverageProbabilities(explicitProbabilityMatrix, targetStates.toVector(odd), linearEquationSolverFactory);
-                return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
+                return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
             }
 
             template<storm::dd::DdType DdType, typename ValueType>
@@ -266,11 +266,13 @@ namespace storm {
                 storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd);
                 
                 std::vector<ValueType> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getTotalRewardVector(model.getTransitionMatrix(), model.getColumnVariables()).toVector(odd), linearEquationSolverFactory);
-                return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
+                return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
             }
             
             template class HybridDtmcPrctlHelper<storm::dd::DdType::CUDD, double>;
             template class HybridDtmcPrctlHelper<storm::dd::DdType::Sylvan, double>;
+
+            template class HybridDtmcPrctlHelper<storm::dd::DdType::Sylvan, storm::RationalFunction>;
         }
     }
 }

src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp

@@ -33,7 +33,7 @@ namespace storm {
                 // Check whether we need to compute exact probabilities for some states.
                 if (qualitative) {
                     // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
-                    return statesWithProbability01.second.template toAdd<ValueType>() + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(0.5);
+                    return statesWithProbability01.second.template toAdd<ValueType>() + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(ValueType(0.5));
                 } else {
                     // If there are maybe states, we need to solve an equation system.
                     if (!maybeStates.isZero()) {
@@ -58,7 +58,7 @@ namespace storm {
                         
                         // Solve the equation system.
                         std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs());
-                        storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().getConstant(0.0), subvector);
+                        storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().template getAddZero<ValueType>(), subvector);
                         
                         return statesWithProbability01.second.template toAdd<ValueType>() + result;
                     } else {
@@ -175,7 +175,7 @@ namespace storm {
                         
                         // Solve the equation system.
                         std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs());
-                        storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().getConstant(0.0), subvector);
+                        storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().template getAddZero<ValueType>(), subvector);
                         
                         return infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), result);
                     } else {
@@ -186,7 +186,8 @@ namespace storm {
             
             template class SymbolicDtmcPrctlHelper<storm::dd::DdType::CUDD, double>;
             template class SymbolicDtmcPrctlHelper<storm::dd::DdType::Sylvan, double>;
-            
+
+            template class SymbolicDtmcPrctlHelper<storm::dd::DdType::Sylvan, storm::RationalFunction>;
         }
     }
 }

src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp

@@ -66,6 +66,9 @@ namespace storm {
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>;
+        template class SymbolicPropositionalModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
+        template class SymbolicPropositionalModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
+        template class SymbolicPropositionalModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
 
     }
 }

src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp

@@ -35,7 +35,7 @@ namespace storm {
             }
             
             // Then translate the explicit part to a symbolic format and simultaneously to a qualitative result.
-            symbolicResult |= storm::dd::Bdd<Type>::fromVector(this->reachableStates.getDdManager(), this->explicitValues, this->odd, this->symbolicValues.getContainedMetaVariables(), comparisonType, bound);
+            symbolicResult |= storm::dd::Bdd<Type>::template fromVector<ValueType>(this->reachableStates.getDdManager(), this->explicitValues, this->odd, this->symbolicValues.getContainedMetaVariables(), comparisonType, storm::utility::convertNumber<ValueType>(bound));
             
             return std::unique_ptr<SymbolicQualitativeCheckResult<Type>>(new SymbolicQualitativeCheckResult<Type>(reachableStates, symbolicResult));
         }
@@ -98,9 +98,9 @@ namespace storm {
                 if (this->symbolicStates.isZero()) {
                     out << *this->explicitValues.begin();
                 } else {
-                    out << this->symbolicValues.getMax();
+                    out << this->symbolicValues.sumAbstract(this->symbolicValues.getContainedMetaVariables()).getValue();
                 }
-            } else if (totalNumberOfStates < 10) {
+            } else if (totalNumberOfStates < 10 || std::is_same<storm::RationalFunction, ValueType>::value) {
                 out << "{";
                 bool first = true;
                 if (!this->symbolicStates.isZero()) {
@@ -165,7 +165,7 @@ namespace storm {
         ValueType HybridQuantitativeCheckResult<Type, ValueType>::getMin() const {
             // In order to not get false zeros, we need to set the values of all states whose values is not stored
             // symbolically to infinity.
-            storm::dd::Add<Type, ValueType> tmp = symbolicStates.ite(this->symbolicValues, reachableStates.getDdManager().getConstant(storm::utility::infinity<double>()));
+            storm::dd::Add<Type, ValueType> tmp = symbolicStates.ite(this->symbolicValues, reachableStates.getDdManager().getConstant(storm::utility::infinity<ValueType>()));
             ValueType min = tmp.getMin();
             if (!explicitStates.isZero()) {
                 for (auto const& element : explicitValues) {
@@ -202,8 +202,8 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ValueType>
         void HybridQuantitativeCheckResult<Type, ValueType>::oneMinus() {
-            storm::dd::Add<Type> one = symbolicValues.getDdManager().template getAddOne<ValueType>();
-            storm::dd::Add<Type> zero = symbolicValues.getDdManager().template getAddZero<ValueType>();
+            storm::dd::Add<Type, ValueType> one = symbolicValues.getDdManager().template getAddOne<ValueType>();
+            storm::dd::Add<Type, ValueType> zero = symbolicValues.getDdManager().template getAddZero<ValueType>();
             symbolicValues = symbolicStates.ite(one - symbolicValues, zero);
 
             for (auto& element : explicitValues) {
@@ -215,5 +215,7 @@ namespace storm {
         // Explicitly instantiate the class.
         template class HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>;
         template class HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>;
+
+        template class HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>;
     }
 }

src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp

@@ -60,8 +60,8 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         std::ostream& SymbolicQuantitativeCheckResult<Type, ValueType>::writeToStream(std::ostream& out) const {
             if (states.getNonZeroCount() == 1) {
-                out << this->values.getMax();
-            } else if (states.getNonZeroCount() < 10) {
+                out << this->values.sumAbstract(this->values.getContainedMetaVariables()).getValue();
+            } else if (states.getNonZeroCount() < 10 || std::is_same<storm::RationalFunction, ValueType>::value) {
                 out << "{";
                 if (this->values.isZero()) {
                     out << "0";
@@ -100,7 +100,7 @@ namespace storm {
         ValueType SymbolicQuantitativeCheckResult<Type, ValueType>::getMin() const {
             // In order to not get false zeros, we need to set the values of all states whose values is not stored
             // symbolically to infinity.
-            return states.ite(this->values, states.getDdManager().getConstant(storm::utility::infinity<double>())).getMin();
+            return states.ite(this->values, states.getDdManager().getConstant(storm::utility::infinity<ValueType>())).getMin();
         }
         
         template<storm::dd::DdType Type, typename ValueType>
@@ -120,12 +120,14 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ValueType>
         void SymbolicQuantitativeCheckResult<Type, ValueType>::oneMinus() {
-            storm::dd::Add<Type> one = values.getDdManager().template getAddOne<ValueType>();
+            storm::dd::Add<Type, ValueType> one = values.getDdManager().template getAddOne<ValueType>();
             values = one - values;
         }
         
         // Explicitly instantiate the class.
         template class SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>;
         template class SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>;
+
+        template class SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>;
     }
 }

src/storm/storage/dd/Add.cpp

@@ -11,6 +11,7 @@
 #include "storm/utility/constants.h"
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/exceptions/InvalidOperationException.h"
 
 #include "storm-config.h"
 #include "storm/adapters/CarlAdapter.h"
@@ -168,12 +169,6 @@ namespace storm {
             return Bdd<LibraryType>(this->getDdManager(), internalAdd.minAbstractRepresentative(cube), this->getContainedMetaVariables());
         }
         
-        template<DdType LibraryType, typename ValueType>
-        Add<LibraryType, ValueType> Add<LibraryType, ValueType>::minAbstractExcept0(std::set<storm::expressions::Variable> const& metaVariables) const {
-            Bdd<LibraryType> cube = Bdd<LibraryType>::getCube(this->getDdManager(), metaVariables);
-            return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.minAbstractExcept0(cube), Dd<LibraryType>::subtractMetaVariables(*this, cube));
-        }
-        
         template<DdType LibraryType, typename ValueType>
         Add<LibraryType, ValueType> Add<LibraryType, ValueType>::maxAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
             Bdd<LibraryType> cube = Bdd<LibraryType>::getCube(this->getDdManager(), metaVariables);
@@ -859,13 +854,18 @@ namespace storm {
 		}
 		
 		template<DdType LibraryType, typename ValueType>
-		Add<LibraryType, double> Add<LibraryType, ValueType>::toDouble() const {
-			STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Not yet implemented: replaceLeaves");
+        template<typename TargetValueType>
+		Add<LibraryType, TargetValueType> Add<LibraryType, ValueType>::toValueType() const {
+            if (std::is_same<TargetValueType, ValueType>::value) {
+                return *this;
+            }
+			STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot convert this ADD to the target type.");
 		}
 
 		template<>
-		Add<storm::dd::DdType::Sylvan, double> Add<storm::dd::DdType::Sylvan, storm::RationalFunction>::toDouble() const {
-			return Add<storm::dd::DdType::Sylvan, double>(this->getDdManager(), internalAdd.toDouble(), this->getContainedMetaVariables());
+        template<>
+		Add<storm::dd::DdType::Sylvan, double> Add<storm::dd::DdType::Sylvan, storm::RationalFunction>::toValueType() const {
+			return Add<storm::dd::DdType::Sylvan, double>(this->getDdManager(), internalAdd.toValueType<double>(), this->getContainedMetaVariables());
 		}
 #endif
 		

src/storm/storage/dd/Add.h

@@ -260,7 +260,8 @@ namespace storm {
              *
              * @return The resulting function represented as an ADD.
              */
-            Add<LibraryType, double> toDouble() const;
+            template<typename TargetValueType>
+            Add<LibraryType, TargetValueType> toValueType() const;
 #endif
 			
             /*!
@@ -277,13 +278,6 @@ namespace storm {
              */
             Add<LibraryType, ValueType> minAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
 
-            /*!
-             * Min-abstracts from the given meta variables but treats 0 as the largest possible value.
-             *
-             * @param metaVariables The meta variables from which to abstract.
-             */
-            Add<LibraryType, ValueType> minAbstractExcept0(std::set<storm::expressions::Variable> const& metaVariables) const;
-
 			/*!
              * Similar to <code>minAbstract</code>, but does not abstract from the variables but rather picks a
              * valuation of each of the meta variables "to abstract from" such that for this valuation, there exists a

src/storm/storage/dd/Bdd.cpp

@@ -14,6 +14,7 @@
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/exceptions/InvalidOperationException.h"
 
 #include "storm-config.h"
 #include "storm/adapters/CarlAdapter.h"
@@ -26,25 +27,39 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        template<DdType LibraryType, typename ValueType>
+        struct FromVectorHelper {
+            static Bdd<LibraryType> fromVector(DdManager<LibraryType> const& ddManager, std::vector<ValueType> const& explicitValues, storm::dd::Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, ValueType value) {
+                switch (comparisonType) {
+                    case storm::logic::ComparisonType::Less:
+                        return fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater<ValueType>(), value, std::placeholders::_1));
+                    case storm::logic::ComparisonType::LessEqual:
+                        return fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal<ValueType>(), value, std::placeholders::_1));
+                    case storm::logic::ComparisonType::Greater:
+                        return fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less<ValueType>(), value, std::placeholders::_1));
+                    case storm::logic::ComparisonType::GreaterEqual:
+                        return fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal<ValueType>(), value, std::placeholders::_1));
+                }
+                return Bdd<LibraryType>();
+            }
+            
+            static Bdd<LibraryType> fromVector(DdManager<LibraryType> const& ddManager, std::vector<ValueType> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter) {
+                return Bdd<LibraryType>(ddManager, InternalBdd<LibraryType>::fromVector(&ddManager.getInternalDdManager(), values, odd, ddManager.getSortedVariableIndices(metaVariables), filter), metaVariables);
+            }
+        };
+        
         template<DdType LibraryType>
-        Bdd<LibraryType> Bdd<LibraryType>::fromVector(DdManager<LibraryType> const& ddManager, std::vector<double> const& explicitValues, storm::dd::Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value) {
-            switch (comparisonType) {
-                case storm::logic::ComparisonType::Less:
-                    return fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater<double>(), value, std::placeholders::_1));
-                case storm::logic::ComparisonType::LessEqual:
-                    return fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal<double>(), value, std::placeholders::_1));
-                case storm::logic::ComparisonType::Greater:
-                    return fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less<double>(), value, std::placeholders::_1));
-                case storm::logic::ComparisonType::GreaterEqual:
-                    return fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal<double>(), value, std::placeholders::_1));
+        struct FromVectorHelper<LibraryType, storm::RationalFunction> {
+            static Bdd<LibraryType> fromVector(DdManager<LibraryType> const& ddManager, std::vector<storm::RationalFunction> const& explicitValues, storm::dd::Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, storm::RationalFunction value) {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot compare rational functions to bound.");
+                return Bdd<LibraryType>();
             }
-            return Bdd<LibraryType>();
-        }
+        };
         
         template<DdType LibraryType>
         template<typename ValueType>
-        Bdd<LibraryType> Bdd<LibraryType>::fromVector(DdManager<LibraryType> const& ddManager, std::vector<ValueType> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter) {
-            return Bdd<LibraryType>(ddManager, InternalBdd<LibraryType>::fromVector(&ddManager.internalDdManager, values, odd, ddManager.getSortedVariableIndices(metaVariables), filter), metaVariables);
+        Bdd<LibraryType> Bdd<LibraryType>::fromVector(DdManager<LibraryType> const& ddManager, std::vector<ValueType> const& explicitValues, storm::dd::Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, ValueType value) {
+            return FromVectorHelper<LibraryType, ValueType>::fromVector(ddManager, explicitValues, odd, metaVariables, comparisonType, value);
         }
         
         template<DdType LibraryType>
@@ -355,8 +370,7 @@ namespace storm {
         
         template class Bdd<DdType::CUDD>;
         
-        template Bdd<DdType::CUDD> Bdd<DdType::CUDD>::fromVector(DdManager<DdType::CUDD> const& ddManager, std::vector<double> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (double const&)> const& filter);
-        template Bdd<DdType::CUDD> Bdd<DdType::CUDD>::fromVector(DdManager<DdType::CUDD> const& ddManager, std::vector<uint_fast64_t> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (uint_fast64_t const&)> const& filter);
+        template Bdd<DdType::CUDD> Bdd<DdType::CUDD>::fromVector(DdManager<DdType::CUDD> const& ddManager, std::vector<double> const& explicitValues, storm::dd::Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
         
         template Add<DdType::CUDD, double> Bdd<DdType::CUDD>::toAdd() const;
         template Add<DdType::CUDD, uint_fast64_t> Bdd<DdType::CUDD>::toAdd() const;
@@ -370,10 +384,10 @@ namespace storm {
         
         template class Bdd<DdType::Sylvan>;
 
-        template Bdd<DdType::Sylvan> Bdd<DdType::Sylvan>::fromVector(DdManager<DdType::Sylvan> const& ddManager, std::vector<double> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (double const&)> const& filter);
-        template Bdd<DdType::Sylvan> Bdd<DdType::Sylvan>::fromVector(DdManager<DdType::Sylvan> const& ddManager, std::vector<uint_fast64_t> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (uint_fast64_t const&)> const& filter);
+        template Bdd<DdType::Sylvan> Bdd<DdType::Sylvan>::fromVector(DdManager<DdType::Sylvan> const& ddManager, std::vector<double> const& explicitValues, storm::dd::Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
+
 #ifdef STORM_HAVE_CARL
-		template Bdd<DdType::Sylvan> Bdd<DdType::Sylvan>::fromVector(DdManager<DdType::Sylvan> const& ddManager, std::vector<storm::RationalFunction> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (storm::RationalFunction const&)> const& filter);
+        template Bdd<DdType::Sylvan> Bdd<DdType::Sylvan>::fromVector(DdManager<DdType::Sylvan> const& ddManager, std::vector<storm::RationalFunction> const& explicitValues, storm::dd::Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, storm::RationalFunction value);
 #endif
         
         template Add<DdType::Sylvan, double> Bdd<DdType::Sylvan>::toAdd() const;

src/storm/storage/dd/Bdd.h

@@ -46,7 +46,8 @@ namespace storm {
              * @param comparisonType The relation that needs to hold for the values (wrt. to the given value).
              * @param value The value to compare with.
              */
-            static Bdd<LibraryType> fromVector(DdManager<LibraryType> const& ddManager, std::vector<double> const& explicitValues, storm::dd::Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
+            template <typename ValueType>
+            static Bdd<LibraryType> fromVector(DdManager<LibraryType> const& ddManager, std::vector<ValueType> const& explicitValues, storm::dd::Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, ValueType value);
             
             /*!
              * Retrieves whether the two BDDs represent the same function.
@@ -335,6 +336,9 @@ namespace storm {
             
             friend struct std::hash<storm::dd::Bdd<LibraryType>>;
             
+            template<DdType LibraryTypePrime, typename ValueType>
+            friend struct FromVectorHelper;
+            
         private:
             /*!
              * We provide a conversion operator from the BDD to its internal type to ease calling the internal functions.
@@ -350,19 +354,6 @@ namespace storm {
              */
             Bdd(DdManager<LibraryType> const& ddManager, InternalBdd<LibraryType> const& internalBdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
             
-            /*!
-             * Builds a BDD representing the values that make the given filter function evaluate to true.
-             *
-             * @param ddManager The manager responsible for the BDD.
-             * @param values The values that are to be checked against the filter function.
-             * @param odd The ODD used for the translation.
-             * @param metaVariables The meta variables used for the translation.
-             * @param filter The filter that evaluates whether an encoding is to be mapped to 0 or 1.
-             * @return The resulting BDD.
-             */
-            template<typename ValueType>
-            static Bdd<LibraryType> fromVector(DdManager<LibraryType> const& ddManager, std::vector<ValueType> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter);
-            
             // The internal BDD that depends on the chosen library.
             InternalBdd<LibraryType> internalBdd;
         };

src/storm/storage/dd/Odd.cpp

@@ -8,6 +8,8 @@
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/utility/file.h"
 
+#include "storm/adapters/CarlAdapter.h"
+
 namespace storm {
     namespace dd {
         Odd::Odd(std::shared_ptr<Odd> elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd> thenNode, uint_fast64_t thenOffset) : elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) {
@@ -69,11 +71,13 @@ namespace storm {
             return this->elseNode == nullptr && this->thenNode == nullptr;
         }
         
-        void Odd::expandExplicitVector(storm::dd::Odd const& newOdd, std::vector<double> const& oldValues, std::vector<double>& newValues) const {
+        template <typename ValueType>
+        void Odd::expandExplicitVector(storm::dd::Odd const& newOdd, std::vector<ValueType> const& oldValues, std::vector<ValueType>& newValues) const {
             expandValuesToVectorRec(0, *this, oldValues, 0, newOdd, newValues);
         }
         
-        void Odd::expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector<double> const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector<double>& newValues) {
+        template <typename ValueType>
+        void Odd::expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector<ValueType> const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector<ValueType>& newValues) {
             if (oldOdd.isTerminalNode()) {
                 STORM_LOG_THROW(newOdd.isTerminalNode(), storm::exceptions::InvalidArgumentException, "The ODDs for the translation must have the same height.");
                 if (oldOdd.getThenOffset() != 0) {
@@ -140,5 +144,8 @@ namespace storm {
                 this->getThenSuccessor().addToLevelToOddNodesMap(levelToOddNodesMap, level + 1);
             }
         }
+        
+        template void Odd::expandExplicitVector(storm::dd::Odd const& newOdd, std::vector<double> const& oldValues, std::vector<double>& newValues) const;
+        template void Odd::expandExplicitVector(storm::dd::Odd const& newOdd, std::vector<storm::RationalFunction> const& oldValues, std::vector<storm::RationalFunction>& newValues) const;
     }
 }

src/storm/storage/dd/Odd.h

@@ -108,7 +108,8 @@ namespace storm {
              * @param oldValues The old vector of values (which is being read).
              * @param newValues The new vector of values (which is being written).
              */
-            void expandExplicitVector(storm::dd::Odd const& newOdd, std::vector<double> const& oldValues, std::vector<double>& newValues) const;
+            template <typename ValueType>
+            void expandExplicitVector(storm::dd::Odd const& newOdd, std::vector<ValueType> const& oldValues, std::vector<ValueType>& newValues) const;
             
             /*!
              * Exports the ODD in the dot format to the given file.
@@ -137,7 +138,8 @@ namespace storm {
              * @param newOdd The ODD to use for the new explicit values.
              * @param newValues The vector of new values.
              */
-            static void expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector<double> const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector<double>& newValues);
+            template <typename ValueType>
+            static void expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector<ValueType> const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector<ValueType>& newValues);
             
             // The then- and else-nodes.
             std::shared_ptr<Odd> elseNode;

src/storm/storage/dd/cudd/InternalCuddAdd.cpp

@@ -152,11 +152,6 @@ namespace storm {
 			return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd<ValueType>().getCuddAdd()));
         }
         
-        template<typename ValueType>
-        InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::minAbstractExcept0(InternalBdd<DdType::CUDD> const& cube) const {
-            return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MinAbstractExcept0(cube.toAdd<ValueType>().getCuddAdd()));
-        }
-        
         template<typename ValueType>
         InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::maxAbstract(InternalBdd<DdType::CUDD> const& cube) const {
             return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MaxAbstract(cube.toAdd<ValueType>().getCuddAdd()));

src/storm/storage/dd/cudd/InternalCuddAdd.h

@@ -260,13 +260,6 @@ namespace storm {
              */
             InternalAdd<DdType::CUDD, ValueType> minAbstract(InternalBdd<DdType::CUDD> const& cube) const;
 
-            /*!
-             * Min-abstracts from the given cube, but treats 0 as the largest possible value.
-             *
-             * @param cube The cube from which to abstract.
-             */
-            InternalAdd<DdType::CUDD, ValueType> minAbstractExcept0(InternalBdd<DdType::CUDD> const& cube) const;
-
 			/*!
              * Min-abstracts from the given cube and returns a representative.
              *

src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -9,6 +9,7 @@
 #include "storm/utility/macros.h"
 #include "storm/utility/constants.h"
 #include "storm/exceptions/NotImplementedException.h"
+#include "storm/exceptions/InvalidOperationException.h"
 
 #include "storm-config.h"
 
@@ -24,6 +25,47 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        template<typename ValueType>
+        ValueType InternalAdd<DdType::Sylvan, ValueType>::getValue(MTBDD const& node) {
+            STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << ".");
+            
+            bool negated = mtbdd_hascomp(node);
+            MTBDD n = mtbdd_regular(node);
+            
+            if (std::is_same<ValueType, double>::value) {
+                STORM_LOG_ASSERT(mtbdd_gettype(n) == 1, "Expected a double value.");
+                return negated ? -mtbdd_getdouble(n) : mtbdd_getdouble(n);
+            } else if (std::is_same<ValueType, uint_fast64_t>::value) {
+                STORM_LOG_ASSERT(mtbdd_gettype(node) == 0, "Expected an unsigned value.");
+                return negated ? -mtbdd_getint64(node) : mtbdd_getint64(node);
+            }
+#ifdef STORM_HAVE_CARL
+            else if (std::is_same<ValueType, storm::RationalFunction>::value) {
+                STORM_LOG_ASSERT(false, "Non-specialized version of getValue() called for storm::RationalFunction value.");
+            }
+#endif
+            else {
+                STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD.");
+            }
+        }
+        
+#ifdef STORM_HAVE_CARL
+        template<>
+        storm::RationalFunction InternalAdd<DdType::Sylvan, storm::RationalFunction>::getValue(MTBDD const& node) {
+            STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << ".");
+            
+            bool negated = mtbdd_hascomp(node);
+            
+            STORM_LOG_ASSERT(mtbdd_gettype(node) == sylvan_storm_rational_function_get_type(), "Expected a storm::RationalFunction value.");
+            uint64_t value = mtbdd_getvalue(node);
+            storm_rational_function_ptr ptr = (storm_rational_function_ptr)value;
+            
+            storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(ptr);
+            
+            return negated ? -(*rationalFunction) : (*rationalFunction);
+        }
+#endif
+        
         template<typename ValueType>
         bool InternalAdd<DdType::Sylvan, ValueType>::operator==(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return this->sylvanMtbdd == other.sylvanMtbdd;
@@ -145,8 +187,8 @@ namespace storm {
 
 #ifdef STORM_HAVE_CARL
 		template<>
-        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::equals(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Equals");
+        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::equals(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            return InternalBdd<DdType::Sylvan>(ddManager,  this->sylvanMtbdd.EqualsRF(other.sylvanMtbdd));
         }
 #endif
 
@@ -155,13 +197,6 @@ namespace storm {
             return !this->equals(other);
         }
 
-#ifdef STORM_HAVE_CARL
-		template<>
-        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::notEquals(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Not Equals");
-        }
-#endif
-
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::less(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.Less(other.sylvanMtbdd));
@@ -169,8 +204,8 @@ namespace storm {
 
 #ifdef STORM_HAVE_CARL
 		template<>
-        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::less(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Less");
+        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::less(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.LessRF(other.sylvanMtbdd));
         }
 #endif
 
@@ -181,8 +216,8 @@ namespace storm {
 
 #ifdef STORM_HAVE_CARL
 		template<>
-        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::lessOrEqual(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Less or Equal");
+        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::lessOrEqual(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.LessOrEqualRF(other.sylvanMtbdd));
         }
 #endif
 
@@ -191,25 +226,11 @@ namespace storm {
             return !this->lessOrEqual(other);
         }
 
-#ifdef STORM_HAVE_CARL
-		template<>
-        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::greater(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Greater");
-        }
-#endif
-
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::greaterOrEqual(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return !this->less(other);
         }
 
-#ifdef STORM_HAVE_CARL
-		template<>
-        InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::greaterOrEqual(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Greater or Equal");
-        }
-#endif
-
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::pow(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Pow(other.sylvanMtbdd));
@@ -217,8 +238,8 @@ namespace storm {
 
 #ifdef STORM_HAVE_CARL
 		template<>
-        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::pow(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Pow");
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::pow(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.PowRF(other.sylvanMtbdd));
         }
 #endif
 
@@ -230,7 +251,7 @@ namespace storm {
 #ifdef STORM_HAVE_CARL
 		template<>
         InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::mod(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Mod");
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (mod) not supported by rational functions.");
         }
 #endif
 
@@ -242,7 +263,7 @@ namespace storm {
 #ifdef STORM_HAVE_CARL
 		template<>
         InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::logxy(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: logxy");
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (logxy) not supported by rational functions.");
         }
 #endif
 
@@ -254,7 +275,7 @@ namespace storm {
 #ifdef STORM_HAVE_CARL
 		template<>
         InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::floor() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Floor");
+            return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.FloorRF());
         }
 #endif
 
@@ -266,7 +287,7 @@ namespace storm {
 #ifdef STORM_HAVE_CARL
 		template<>
         InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::ceil() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Ceil");
+            return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.CeilRF());
         }
 #endif
 
@@ -277,8 +298,8 @@ namespace storm {
 
 #ifdef STORM_HAVE_CARL
 		template<>
-        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::minimum(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Minimum");
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::minimum(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.MinRF(other.sylvanMtbdd));
         }
 #endif
 
@@ -289,14 +310,14 @@ namespace storm {
 
 #ifdef STORM_HAVE_CARL
 		template<>
-        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::maximum(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Maximum");
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::maximum(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& other) const {
+            return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.MaxRF(other.sylvanMtbdd));
         }
 #endif
 
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::replaceLeaves(std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: replaceLeaves");
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Replacing leaves is not supported for types other than rational functions.");
         }
 
 #ifdef STORM_HAVE_CARL
@@ -307,13 +328,18 @@ namespace storm {
 #endif
 
         template<typename ValueType>
-        InternalAdd<DdType::Sylvan, double> InternalAdd<DdType::Sylvan, ValueType>::toDouble() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: toDouble");
+        template<typename TargetValueType>
+        InternalAdd<DdType::Sylvan, TargetValueType> InternalAdd<DdType::Sylvan, ValueType>::toValueType() const {
+            if (std::is_same<TargetValueType, ValueType>::value) {
+                return *this;
+            }
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot convert this ADD to the target type.");
         }
-
+        
 #ifdef STORM_HAVE_CARL
 		template<>
-        InternalAdd<DdType::Sylvan, double> InternalAdd<DdType::Sylvan, storm::RationalFunction>::toDouble() const {
+        template<>
+        InternalAdd<DdType::Sylvan, double> InternalAdd<DdType::Sylvan, storm::RationalFunction>::toValueType() const {
             return InternalAdd<DdType::Sylvan, double>(ddManager, this->sylvanMtbdd.ToDoubleRF());
         }
 #endif
@@ -342,20 +368,8 @@ namespace storm {
 
 #ifdef STORM_HAVE_CARL
 		template<>
-        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::minAbstract(InternalBdd<DdType::Sylvan> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstract");
-        }
-#endif
-        
-        template<typename ValueType>
-        InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::minAbstractExcept0(InternalBdd<DdType::Sylvan> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractExcept0");
-        }
-
-#ifdef STORM_HAVE_CARL
-        template<>
-        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::minAbstractExcept0(InternalBdd<DdType::Sylvan> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractExcept0");
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::minAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
+            return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.AbstractMinRF(cube.sylvanBdd));
         }
 #endif
 
@@ -371,8 +385,8 @@ namespace storm {
 
 #ifdef STORM_HAVE_CARL
 		template<>
-        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::maxAbstract(InternalBdd<DdType::Sylvan> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: maxAbstract");
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::maxAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
+            return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.AbstractMaxRF(cube.sylvanBdd));
         }
 #endif
 
@@ -388,7 +402,7 @@ namespace storm {
 #ifdef STORM_HAVE_CARL
 		template<>
         bool InternalAdd<DdType::Sylvan, storm::RationalFunction>::equalModuloPrecision(InternalAdd<DdType::Sylvan, storm::RationalFunction> const&, double, bool) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: equalModuloPrecision");
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (equal modulo precision) not supported by rational functions.");
         }
 #endif
 
@@ -426,14 +440,26 @@ namespace storm {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AndExists(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd()));
         }
         
+#ifdef STORM_HAVE_CARL
+        template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::multiplyMatrix(InternalAdd<DdType::Sylvan, storm::RationalFunction> const& otherMatrix, std::vector<InternalBdd<DdType::Sylvan>> const& summationDdVariables) const {
+            InternalBdd<DdType::Sylvan> summationVariables = ddManager->getBddOne();
+            for (auto const& ddVariable : summationDdVariables) {
+                summationVariables &= ddVariable;
+            }
+            
+            return InternalAdd<DdType::Sylvan, storm::RationalFunction>(ddManager, this->sylvanMtbdd.AndExistsRF(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd()));
+        }
+#endif
+        
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::greater(ValueType const& value) const {
             return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.BddStrictThreshold(value));
         }
 
 		template<>
-		InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::greater(storm::RationalFunction const& ) const {
-			STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+		InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::greater(storm::RationalFunction const& value) const {
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.BddStrictThresholdRF(value));
 		}
         
         template<typename ValueType>
@@ -442,8 +468,8 @@ namespace storm {
         }
         
 		template<>
-		InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::greaterOrEqual(storm::RationalFunction const&) const {
-			STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+		InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, storm::RationalFunction>::greaterOrEqual(storm::RationalFunction const& value) const {
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.BddThresholdRF(value));
 		}
 
         template<typename ValueType>
@@ -463,12 +489,12 @@ namespace storm {
         
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::constrain(InternalAdd<DdType::Sylvan, ValueType> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Operation (constrain) not yet implemented.");
         }
         
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::restrict(InternalAdd<DdType::Sylvan, ValueType> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Operation (restrict) not yet implemented.");
         }
         
         template<typename ValueType>
@@ -499,10 +525,20 @@ namespace storm {
             return getValue(this->sylvanMtbdd.Minimum().GetMTBDD());
         }
         
+        template <>
+        storm::RationalFunction InternalAdd<DdType::Sylvan, storm::RationalFunction>::getMin() const {
+            return getValue(this->sylvanMtbdd.MinimumRF().GetMTBDD());
+        }
+        
         template<typename ValueType>
         ValueType InternalAdd<DdType::Sylvan, ValueType>::getMax() const {
             return getValue(this->sylvanMtbdd.Maximum().GetMTBDD());
         }
+
+        template<>
+        storm::RationalFunction InternalAdd<DdType::Sylvan, storm::RationalFunction>::getMax() const {
+            return getValue(this->sylvanMtbdd.MaximumRF().GetMTBDD());
+        }
         
         template<typename ValueType>
         ValueType InternalAdd<DdType::Sylvan, ValueType>::getValue() const {
@@ -871,47 +907,6 @@ namespace storm {
 
 			return mtbdd_storm_rational_function(ptr);
 		}
-        
-        template<typename ValueType>
-        ValueType InternalAdd<DdType::Sylvan, ValueType>::getValue(MTBDD const& node) {
-            STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << ".");
-            
-            bool negated = mtbdd_hascomp(node);
-            MTBDD n = mtbdd_regular(node);
-            
-            if (std::is_same<ValueType, double>::value) {
-                STORM_LOG_ASSERT(mtbdd_gettype(n) == 1, "Expected a double value.");
-                return negated ? -mtbdd_getdouble(n) : mtbdd_getdouble(n);
-            } else if (std::is_same<ValueType, uint_fast64_t>::value) {
-                STORM_LOG_ASSERT(mtbdd_gettype(node) == 0, "Expected an unsigned value.");
-                return negated ? -mtbdd_getint64(node) : mtbdd_getint64(node);
-			} 
-#ifdef STORM_HAVE_CARL
-			else if (std::is_same<ValueType, storm::RationalFunction>::value) {
-				STORM_LOG_ASSERT(false, "Non-specialized version of getValue() called for storm::RationalFunction value.");
-			} 
-#endif
-			else {
-                STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD.");
-            }
-        }
-        
-#ifdef STORM_HAVE_CARL
-		template<>
-		storm::RationalFunction InternalAdd<DdType::Sylvan, storm::RationalFunction>::getValue(MTBDD const& node) {
-			STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << ".");
-
-			bool negated = mtbdd_hascomp(node);
-
-			STORM_LOG_ASSERT(mtbdd_gettype(node) == sylvan_storm_rational_function_get_type(), "Expected a storm::RationalFunction value.");
-			uint64_t value = mtbdd_getvalue(node);
-			storm_rational_function_ptr ptr = (storm_rational_function_ptr)value;
-
-			storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(ptr);
-
-			return negated ? -(*rationalFunction) : (*rationalFunction);
-		}
-#endif
 
         template<typename ValueType>
         sylvan::Mtbdd InternalAdd<DdType::Sylvan, ValueType>::getSylvanMtbdd() const {
@@ -920,6 +915,7 @@ namespace storm {
         
         template class InternalAdd<DdType::Sylvan, double>;
         template class InternalAdd<DdType::Sylvan, uint_fast64_t>;
+        
 #ifdef STORM_HAVE_CARL
 		template class InternalAdd<DdType::Sylvan, storm::RationalFunction>;
 #endif

src/storm/storage/dd/sylvan/InternalSylvanAdd.h

@@ -262,7 +262,8 @@ namespace storm {
              *
              * @return The resulting function represented as an ADD.
              */
-            InternalAdd<DdType::Sylvan, double> toDouble() const;
+            template<typename TargetValueType>
+            InternalAdd<DdType::Sylvan, TargetValueType> toValueType() const;
 #endif
 			
             /*!
@@ -278,13 +279,6 @@ namespace storm {
              * @param cube The cube from which to abstract.
              */
             InternalAdd<DdType::Sylvan, ValueType> minAbstract(InternalBdd<DdType::Sylvan> const& cube) const;
-
-            /*!
-             * Min-abstracts from the given cube, but treats 0 as the largest possible value.
-             *
-             * @param cube The cube from which to abstract.
-             */
-            InternalAdd<DdType::Sylvan, ValueType> minAbstractExcept0(InternalBdd<DdType::Sylvan> const& cube) const;
 			
 			/*!
              * Min-abstracts from the given cube and returns a representative.

src/storm/utility/constants.cpp

@@ -356,7 +356,7 @@ namespace storm {
             value.simplify();
             return std::move(value);
         }
-
+        
         template<>
         double convertNumber(RationalNumber const& number){
             return carl::toDouble(number);
@@ -414,6 +414,11 @@ namespace storm {
         uint_fast64_t convertNumber(RationalFunction const& func) {
             return carl::toInt<unsigned long>(func.nominatorAsNumber());
         }
+        
+        template<>
+        RationalFunction convertNumber(RationalFunction const& number){
+            return number;
+        }
 
         template<>
         RationalNumber sqrt(RationalNumber const& number) {
@@ -603,6 +608,8 @@ namespace storm {
         template RationalFunction zero();
         template storm::RationalFunction infinity();
 
+        template storm::RationalFunction convertNumber(storm::RationalFunction const& number);
+        
         template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
         template RationalFunction simplify(RationalFunction value);
         template RationalFunction& simplify(RationalFunction& value);

src/storm/utility/graph.cpp

@@ -1411,7 +1411,7 @@ namespace storm {
             
             template GameProb01Result<storm::dd::DdType::CUDD> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional<storm::dd::Bdd<storm::dd::DdType::CUDD>> const& player1Candidates);
 
-            // Instantiations for Sylvan.
+            // Instantiations for Sylvan (double).
             
             template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProbGreater0(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, boost::optional<uint_fast64_t> const& stepBound = boost::optional<uint_fast64_t>());
             
@@ -1443,6 +1443,34 @@ namespace storm {
 
             template GameProb01Result<storm::dd::DdType::Sylvan> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional<storm::dd::Bdd<storm::dd::DdType::Sylvan>> const& player1Candidates);
 
+            // Instantiations for Sylvan (rational function).
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProbGreater0(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, boost::optional<uint_fast64_t> const& stepBound = boost::optional<uint_fast64_t>());
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb1(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& statesWithProbabilityGreater0);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb1(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01(storm::models::symbolic::DeterministicModel<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProbGreater0E(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb0A(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProbGreater0A(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb0E(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb1A(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& statesWithProbabilityGreater0A);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb1E(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& statesWithProbabilityGreater0E);
+            
+            template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01Max(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01Min(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
         } // namespace graph
     } // namespace utility
 } // namespace storm

src/storm/utility/solver.cpp

@@ -33,12 +33,26 @@ namespace storm {
                     case storm::solver::EquationSolverType::Elimination: return std::make_unique<storm::solver::SymbolicEliminationLinearEquationSolver<Type, ValueType>>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs);
                         break;
                         case storm::solver::EquationSolverType::Native: return std::make_unique<storm::solver::SymbolicNativeLinearEquationSolver<Type, ValueType>>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs);
+                        break;
                     default:
                         STORM_LOG_WARN("The selected equation solver is not available in the DD setting. Falling back to native solver.");
                         return std::make_unique<storm::solver::SymbolicNativeLinearEquationSolver<Type, ValueType>>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs);
                 }
             }
-            
+
+            template<storm::dd::DdType Type>
+            std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<Type, storm::RationalFunction>> SymbolicLinearEquationSolverFactory<Type, storm::RationalFunction>::create(storm::dd::Add<Type, storm::RationalFunction> const& A, storm::dd::Bdd<Type> 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 {
+                
+                storm::solver::EquationSolverType equationSolver = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver();
+                switch (equationSolver) {
+                    case storm::solver::EquationSolverType::Elimination: return std::make_unique<storm::solver::SymbolicEliminationLinearEquationSolver<Type, storm::RationalFunction>>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs);
+                        break;
+                    default:
+                        STORM_LOG_WARN("The selected equation solver is not available in the DD setting. Falling back to elimination solver.");
+                        return std::make_unique<storm::solver::SymbolicEliminationLinearEquationSolver<Type, storm::RationalFunction>>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs);
+                }
+            }
+
             template<storm::dd::DdType Type, typename ValueType>
             std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<Type, ValueType>> SymbolicMinMaxLinearEquationSolverFactory<Type, ValueType>::create(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const {
                 return std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<Type, ValueType>>(new storm::solver::SymbolicMinMaxLinearEquationSolver<Type, ValueType>(A, allRows, illegalMask, rowMetaVariables, columnMetaVariables, choiceVariables, rowColumnMetaVariablePairs));
@@ -114,6 +128,7 @@ namespace storm {
             
             template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
             template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>;
+            template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalFunction>;
             template class SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
             template class SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>;
             template class SymbolicGameSolverFactory<storm::dd::DdType::CUDD, double>;

src/storm/utility/solver.h

@@ -63,6 +63,12 @@ namespace storm {
                 virtual std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<Type, ValueType>> create(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> 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;
             };
             
+            template<storm::dd::DdType Type>
+            class SymbolicLinearEquationSolverFactory<Type, storm::RationalFunction> {
+            public:
+                virtual std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<Type, storm::RationalFunction>> create(storm::dd::Add<Type, storm::RationalFunction> const& A, storm::dd::Bdd<Type> 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;
+            };
+            
             template<storm::dd::DdType Type, typename ValueType>
             class SymbolicMinMaxLinearEquationSolverFactory {
                 public:

src/storm/utility/storm.h

@@ -580,31 +580,16 @@ namespace storm {
     
     template<storm::dd::DdType DdType>
     std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant = false) {
-//        std::unique_ptr<storm::modelchecker::CheckResult> result;
-//        storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> task(*formula, onlyInitialStatesRelevant);
-//        if (model->getType() == storm::models::ModelType::Dtmc) {
-//            std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType, ValueType>>();
-//            storm::modelchecker::HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> modelchecker(*dtmc);
-//            if (modelchecker.canHandle(task)) {
-//                result = modelchecker.check(task);
-//            }
-//        } else if (model->getType() == storm::models::ModelType::Ctmc) {
-//            std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType, ValueType>>();
-//            storm::modelchecker::HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<DdType, ValueType>> modelchecker(*ctmc);
-//            if (modelchecker.canHandle(task)) {
-//                result = modelchecker.check(task);
-//            }
-//        } else if (model->getType() == storm::models::ModelType::Mdp) {
-//            std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType, ValueType>>();
-//            storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> modelchecker(*mdp);
-//            if (modelchecker.canHandle(task)) {
-//                result = modelchecker.check(task);
-//            }
-//        } else {
-//            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
-//        }
-//        return result;
-        return nullptr;
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction> task(*formula, onlyInitialStatesRelevant);
+
+        STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::NotSupportedException, "Only DTMCs are supported by this engine (in parametric mode).");
+        std::shared_ptr<storm::models::symbolic::Dtmc<DdType, storm::RationalFunction>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType, storm::RationalFunction>>();
+        storm::modelchecker::HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, storm::RationalFunction>> modelchecker(*dtmc);
+        if (modelchecker.canHandle(task)) {
+            result = modelchecker.check(task);
+        }
+        return result;
     }
 
     template<storm::dd::DdType DdType, typename ValueType = double>
@@ -631,25 +616,16 @@ namespace storm {
     
     template<storm::dd::DdType DdType>
     std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant) {
-//        std::unique_ptr<storm::modelchecker::CheckResult> result;
-//        storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> task(*formula, onlyInitialStatesRelevant);
-//        if (model->getType() == storm::models::ModelType::Dtmc) {
-//            std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType, ValueType>>();
-//            storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> modelchecker(*dtmc);
-//            if (modelchecker.canHandle(task)) {
-//                result = modelchecker.check(task);
-//            }
-//        } else if (model->getType() == storm::models::ModelType::Mdp) {
-//            std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType, ValueType>>();
-//            storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> modelchecker(*mdp);
-//            if (modelchecker.canHandle(task)) {
-//                result = modelchecker.check(task);
-//            }
-//        } else {
-//            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
-//        }
-//        return result;
-        return nullptr;
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction> task(*formula, onlyInitialStatesRelevant);
+        
+        STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::NotSupportedException, "Only DTMCs are supported by this engine (in parametric mode).");
+        std::shared_ptr<storm::models::symbolic::Dtmc<DdType, storm::RationalFunction>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType, storm::RationalFunction>>();
+        storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, storm::RationalFunction>> modelchecker(*dtmc);
+        if (modelchecker.canHandle(task)) {
+            result = modelchecker.check(task);
+        }
+        return result;
     }
     
     template<storm::dd::DdType DdType, typename ValueType>