Merge branch 'master' into TimParamSysAndSMT and minor stuff

Former-commit-id: 90ea514475

examples/pmdp/consensus/coin6_2.nm

@@ -60,7 +60,7 @@ label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=3 ;
 label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 & coin5=0 & coin6=0 ;
 label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1 ;
 label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 & coin4=coin5 & coin5=coin6 ;
-label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=4 & coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1;
+label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1;
 
 // rewards
 rewards "steps"

examples/pmdp/consensus/coin6_8.nm

@@ -61,7 +61,7 @@ label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 & coin5=0 & co
 label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1 ;
 label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 & coin4=coin5 & coin5=coin6 ;
 label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 ;
-label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=4 & coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1;
+label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1;
 
 // rewards
 rewards "steps"

src/builder/ExplicitPrismModelBuilder.cpp

@@ -469,8 +469,7 @@ namespace storm {
                     }
 
                     // Check that the resulting distribution is in fact a distribution.
-                    //STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
-                    STORM_LOG_ERROR_COND(!discreteTimeModel || comparator.isOne(probabilitySum), "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
+                    STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
                 }
             }
             
@@ -546,8 +545,7 @@ namespace storm {
                         }
                         
                         // Check that the resulting distribution is in fact a distribution.
-                        //STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
-                        STORM_LOG_ERROR_COND(!discreteTimeModel || comparator.isOne(probabilitySum), "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
+                        STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
                         
                         // Dispose of the temporary maps.
                         delete currentTargetStates;

src/utility/ConstantsComparator.cpp

@@ -11,12 +11,12 @@ namespace storm {
     namespace utility {
         template<typename ValueType>
         bool ConstantsComparator<ValueType>::isOne(ValueType const& value) const {
-            return isOne(value);
+            return storm::utility::isOne(value);
         }
         
         template<typename ValueType>
         bool ConstantsComparator<ValueType>::isZero(ValueType const& value) const {
-            return isZero(value);
+            return storm::utility::isZero(value);
         }
         
         template<typename ValueType>
@@ -26,7 +26,7 @@ namespace storm {
         
         template<typename ValueType>
         bool ConstantsComparator<ValueType>::isConstant(ValueType const& value) const {
-            return isConstant(value);
+            return storm::utility::isConstant(value);
         }
 
         template<typename ValueType>