From 20a5d8e96f025751cb0b31944b6f958a0465f4d8 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Sat, 9 Jan 2016 11:20:18 +0100
Subject: [PATCH] Side conditions for rational functions  cannot be checked
 directly

Former-commit-id: c5e6d79c9d597e11b09c40cbadf1b3af0688ba5f
---
 src/storage/dft/DFTBuilder.h | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h
index 88fdc6ef0..12d5e88c3 100644
--- a/src/storage/dft/DFTBuilder.h
+++ b/src/storage/dft/DFTBuilder.h
@@ -78,16 +78,10 @@ namespace storm {
             }
             
             bool addBasicElement(std::string const& name, ValueType failureRate, ValueType dormancyFactor) {
-                if(failureRate <= 0.0) {
-                    std::cerr << "Failure rate must be positive." << std::endl;
-                    return false;
-                }
-                
-                if(dormancyFactor < 0.0 || dormancyFactor > 1.0) {
-                    std::cerr << "Dormancy factor must be between 0 and 1." << std::endl;
-                    return false;
-                }
-                
+                //TODO Matthias: collect constraints for SMT solving
+                //failureRate > 0
+                //0 <= dormancyFactor <= 1
+
                 mElements[name] = std::make_shared<DFTBE<ValueType>>(mNextId++, name, failureRate, dormancyFactor);
                 return true;
             }