Changed more assert to STORM_LOG_ASSERT

Former-commit-id: b42fe54f45

src/storage/dft/DFTBuilder.cpp

@@ -25,7 +25,7 @@ namespace storm {
                     if (itFind != mElements.end()) {
                         // Child found
                         DFTElementPointer childElement = itFind->second;
-                        assert(!childElement->isDependency());
+                        STORM_LOG_ASSERT(!childElement->isDependency(), "Child is dependency.");
                         gate->pushBackChild(childElement);
                         childElement->addParent(gate);
                     } else {
@@ -42,9 +42,9 @@ namespace storm {
             for(auto& elem : mRestrictionChildNames) {
                 for(auto const& childName : elem.second) {
                     auto itFind = mElements.find(childName);
-                    assert(itFind != mElements.end());
+                    STORM_LOG_ASSERT(itFind != mElements.end(), "Child not found.");
                     DFTElementPointer childElement = itFind->second;
-                    assert(!childElement->isDependency() && !childElement->isRestriction());
+                    STORM_LOG_ASSERT(!childElement->isDependency() && !childElement->isRestriction(), "Child has invalid type.");
                     elem.first->pushBackChild(childElement);
                     childElement->addRestriction(elem.first);
                 }
@@ -53,7 +53,7 @@ namespace storm {
             // Initialize dependencies
             for (auto& dependency : mDependencies) {
                 DFTGatePointer triggerEvent = std::static_pointer_cast<DFTGate<ValueType>>(mElements[dependency->nameTrigger()]);
-                assert(mElements[dependency->nameDependent()]->isBasicElement());
+                STORM_LOG_ASSERT(mElements[dependency->nameDependent()]->isBasicElement(), "Dependent element is not BE.");
                 std::shared_ptr<DFTBE<ValueType>> dependentEvent = std::static_pointer_cast<DFTBE<ValueType>>(mElements[dependency->nameDependent()]);
                 dependency->initialize(triggerEvent, dependentEvent);
                 triggerEvent->addOutgoingDependency(dependency);
@@ -73,7 +73,7 @@ namespace storm {
             for(DFTElementPointer e : elems) {
                 e->setId(id++);
             }
-            assert(!mTopLevelIdentifier.empty());
+            STORM_LOG_ASSERT(!mTopLevelIdentifier.empty(), "No top level element.");
             return DFT<ValueType>(elems, mElements[mTopLevelIdentifier]);
         }
 
@@ -130,7 +130,7 @@ namespace storm {
 
         template<typename ValueType>
         bool DFTBuilder<ValueType>::addStandardGate(std::string const& name, std::vector<std::string> const& children, DFTElementType tp) {
-            assert(children.size() > 0);
+            STORM_LOG_ASSERT(children.size() > 0, "No child.");
             if(mElements.count(name) != 0) {
                 // Element with that name already exists.
                 return false;
@@ -234,7 +234,7 @@ namespace storm {
                 case DFTElementType::CONSTF:
                 case DFTElementType::CONSTS:
                     // TODO
-                    assert(false);
+                    STORM_LOG_ASSERT(false, "Const elements not supported.");
                     break;
                 case DFTElementType::PDEP:
                 {
@@ -254,7 +254,7 @@ namespace storm {
                     break;
                 }
                 default:
-                    assert(false);
+                    STORM_LOG_ASSERT(false, "Dft type not known.");
                     break;
             }
         }
@@ -273,7 +273,7 @@ namespace storm {
                     addVotElement(gate->name(), std::static_pointer_cast<DFTVot<ValueType>>(gate)->threshold(), children);
                     break;
                 default:
-                    assert(false);
+                    STORM_LOG_ASSERT(false, "Dft type not known.");
                     break;
             }
         }

src/storage/dft/DFTBuilder.h

@@ -104,7 +104,7 @@ namespace storm {
                             STORM_LOG_ERROR("Element with name: " << nameDep << " already exists.");
                             return false;
                         }
-                        assert(storm::utility::isOne(probability) || children.size() == 2);
+                        STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, "PDep with multiple children supported.");
                         DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, nameDep, trigger, children[i], probability);
                         mElements[element->name()] = element;
                         mDependencies.push_back(element);
@@ -114,7 +114,7 @@ namespace storm {
             }
 
             bool addVotElement(std::string const& name, unsigned threshold, std::vector<std::string> const& children) {
-                assert(children.size() > 0);
+                STORM_LOG_ASSERT(children.size() > 0, "Has no child.");
                 if(mElements.count(name) != 0) {
                     STORM_LOG_ERROR("Element with name: " << name << " already exists.");
                     return false;

src/storage/dft/DFTStateGenerationInfo.h

@@ -18,7 +18,7 @@ namespace storm {
                 mUsageInfoBits(storm::utility::math::uint64_log2(maxSpareChildCount) + 1), 
                 mIdToStateIndex(nrElements)
             {
-                assert(maxSpareChildCount < pow(2, mUsageInfoBits));
+                STORM_LOG_ASSERT(maxSpareChildCount < pow(2, mUsageInfoBits), "Bit length incorrect.");
             }
 
             size_t usageInfoBits() const {
@@ -26,7 +26,7 @@ namespace storm {
             }
 
             void addStateIndex(size_t id, size_t index) {
-                assert(id < mIdToStateIndex.size());
+                STORM_LOG_ASSERT(id < mIdToStateIndex.size(), "Id invalid.");
                 mIdToStateIndex[id] = index;
             }
 
@@ -39,7 +39,7 @@ namespace storm {
             }
             
             std::vector<size_t> const& seqRestrictionPostElements(size_t index) const {
-                assert(mSeqRestrictionPostElements.count(index) > 0);
+                STORM_LOG_ASSERT(mSeqRestrictionPostElements.count(index) > 0, "Index invalid.");
                 return mSeqRestrictionPostElements.at(index);
             }
             
@@ -53,17 +53,17 @@ namespace storm {
             }
 
             size_t getStateIndex(size_t id) const {
-                assert(id < mIdToStateIndex.size());
+                STORM_LOG_ASSERT(id < mIdToStateIndex.size(), "Id invalid.");
                 return mIdToStateIndex[id];
             }
 
             size_t getSpareUsageIndex(size_t id) const {
-                assert(mSpareUsageIndex.count(id) > 0);
+                STORM_LOG_ASSERT(mSpareUsageIndex.count(id) > 0, "Id invalid.");
                 return mSpareUsageIndex.at(id);
             }
 
             size_t getSpareActivationIndex(size_t id) const {
-                assert(mSpareActivationIndex.count(id) > 0);
+                STORM_LOG_ASSERT(mSpareActivationIndex.count(id) > 0, "Id invalid.");
                 return mSpareActivationIndex.at(id);
             }
 
@@ -114,12 +114,12 @@ namespace storm {
             }
 
             size_t getSymmetryLength(size_t pos) const {
-                assert(pos < mSymmetries.size());
+                STORM_LOG_ASSERT(pos < mSymmetries.size(), "Pos invalid.");
                 return mSymmetries[pos].first;
             }
 
             std::vector<size_t> const& getSymmetryIndices(size_t pos) const {
-                assert(pos < mSymmetries.size());
+                STORM_LOG_ASSERT(pos < mSymmetries.size(), "Pos invalid.");
                 return mSymmetries[pos].second;
             }
 

src/storage/dft/elements/DFTAnd.h

@@ -24,7 +24,7 @@ namespace storm {
             }
 
             void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
-                assert(this->hasFailsafeChild(state));
+                STORM_LOG_ASSERT(this->hasFailsafeChild(state), "No failsafe child.");
                 if(state.isOperational(this->mId)) {
                     this->failsafe(state, queues);
                     this->childrenDontCare(state, queues);

src/storage/dft/elements/DFTBE.h

@@ -38,7 +38,7 @@ namespace storm {
             }
             
             bool addIngoingDependency(DFTDependencyPointer const& e) {
-                assert(e->dependentEvent()->id() == this->id());
+                STORM_LOG_ASSERT(e->dependentEvent()->id() == this->id(), "Ids do not match.");
                 if(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), e) != mIngoingDependencies.end()) {
                     return false;
                 }

src/storage/dft/elements/DFTDependency.h

@@ -27,8 +27,8 @@ namespace storm {
             virtual ~DFTDependency() {}
 
             void initialize(DFTGatePointer triggerEvent, DFTBEPointer dependentEvent) {
-                assert(triggerEvent->name() == mNameTrigger);
-                assert(dependentEvent->name() == mNameDependent);
+                STORM_LOG_ASSERT(triggerEvent->name() == mNameTrigger, "Name does not match.");
+                STORM_LOG_ASSERT(dependentEvent->name() == mNameDependent, "Name does not match.");
                 mTriggerEvent = triggerEvent;
                 mDependentEvent = dependentEvent;
             }
@@ -46,12 +46,12 @@ namespace storm {
             }
 
             DFTGatePointer const& triggerEvent() const {
-                assert(mTriggerEvent);
+                STORM_LOG_ASSERT(mTriggerEvent, "Trigger does not exist.");
                 return mTriggerEvent;
             }
 
             DFTBEPointer const& dependentEvent() const {
-                assert(mDependentEvent);
+                STORM_LOG_ASSERT(mDependentEvent, "Dependent element does not exists.");
                 return mDependentEvent;
             }
 

src/storage/dft/elements/DFTElement.h

@@ -1,7 +1,6 @@
 #pragma once 
 
 #include <string>
-#include <cassert>
 #include <cstdlib>
 #include <iostream>
 #include <functional>
@@ -182,7 +181,7 @@ namespace storm {
             }
             
             bool addOutgoingDependency(DFTDependencyPointer const& e) {
-                assert(e->triggerEvent()->id() == this->id());
+                STORM_LOG_ASSERT(e->triggerEvent()->id() == this->id(), "Ids do not match.");
                 if(std::find(mOutgoingDependencies.begin(), mOutgoingDependencies.end(), e) != mOutgoingDependencies.end()) {
                     return false;
                 }
@@ -217,7 +216,7 @@ namespace storm {
                             break;
                         }
                     }
-                    assert(it != restr->children().cend());
+                    STORM_LOG_ASSERT(it != restr->children().cend(), "Child not found.");
                     ++it;
                     if(it != restr->children().cend()) {
                         res.push_back((*it)->id());
@@ -242,7 +241,7 @@ namespace storm {
                             break;
                         }
                     }
-                    assert(it != restr->children().cend());
+                    STORM_LOG_ASSERT(it != restr->children().cend(), "Child not found.");
                     if(it != restr->children().cbegin()) {
                         --it;
                         res.push_back((*it)->id());

src/storage/dft/elements/DFTOr.h

@@ -12,7 +12,7 @@ namespace storm {
             {}
 
             void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
-                assert(this->hasFailedChild(state));
+                STORM_LOG_ASSERT(this->hasFailedChild(state), "No failed child.");
                 if(state.isOperational(this->mId)) {
                     this->fail(state, queues);
                 }

src/storage/dft/elements/DFTPand.h

@@ -31,7 +31,7 @@ namespace storm {
             }
 
             void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
-                assert(this->hasFailsafeChild(state));
+                STORM_LOG_ASSERT(this->hasFailsafeChild(state), "No failsafe child.");
                 if(state.isOperational(this->mId)) {
                     this->failsafe(state, queues);
                     this->childrenDontCare(state, queues);

src/storage/dft/elements/DFTRestriction.h

@@ -173,7 +173,7 @@ namespace storm {
 
             
             void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
-                assert(queues.failurePropagationDone());
+                STORM_LOG_ASSERT(queues.failurePropagationDone(), "Failure propagation not finished.");
                 bool childOperationalBefore = false;
                 for(auto const& child : this->mChildren)
                 {

src/storage/dft/elements/DFTVot.h

@@ -34,7 +34,7 @@ namespace storm {
             }
 
             void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
-                assert(this->hasFailsafeChild(state));
+                STORM_LOG_ASSERT(this->hasFailsafeChild(state), "No failsafe child.");
                 if(state.isOperational(this->mId)) {
                     unsigned nrFailsafeChildren = 0;
                     for(auto const& child : this->mChildren)

src/utility/storm.h

@@ -399,7 +399,7 @@ namespace storm {
                     psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
                 } else {
                     // Eventually formula
-                    STORM_LOG_THROW(!probOpFormula.getSubformula().isEventuallyFormula(), storm::exceptions::NotSupportedException, "The parametric engine only supports eventually formulas on CTMCs");
+                    STORM_LOG_THROW(probOpFormula.getSubformula().isEventuallyFormula(), storm::exceptions::NotSupportedException, "The parametric engine only supports eventually formulas on CTMCs");
                     storm::logic::EventuallyFormula eventuallyFormula = probOpFormula.getSubformula().asEventuallyFormula();
                     STORM_LOG_THROW(eventuallyFormula.getSubformula().isInFragment(storm::logic::propositional()), storm::exceptions::NotSupportedException, "The parametric engine does not support nested formulas on CTMCs");
                     std::unique_ptr<storm::modelchecker::CheckResult> resultPointer = propositionalModelchecker.check(eventuallyFormula.getSubformula());