From c8521f0de3338046b67e4f9003f70229d1c68b25 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 17 May 2016 18:24:38 +0200
Subject: [PATCH] Changed more assert to STORM_LOG_ASSERT
Former-commit-id: b42fe54f45740931089ce3c421946d72441975a7
---
src/storage/dft/DFTBuilder.cpp | 18 +++++++++---------
src/storage/dft/DFTBuilder.h | 4 ++--
src/storage/dft/DFTStateGenerationInfo.h | 18 +++++++++---------
src/storage/dft/elements/DFTAnd.h | 2 +-
src/storage/dft/elements/DFTBE.h | 4 ++--
src/storage/dft/elements/DFTDependency.h | 10 +++++-----
src/storage/dft/elements/DFTElement.h | 7 +++----
src/storage/dft/elements/DFTOr.h | 2 +-
src/storage/dft/elements/DFTPand.h | 4 ++--
src/storage/dft/elements/DFTRestriction.h | 4 ++--
src/storage/dft/elements/DFTVot.h | 4 ++--
src/utility/storm.h | 2 +-
12 files changed, 39 insertions(+), 40 deletions(-)
diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp
index e6e4ef1ae..840f5b77b 100644
--- a/src/storage/dft/DFTBuilder.cpp
+++ b/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;
}
}
diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h
index 168b27755..3f9f25f4c 100644
--- a/src/storage/dft/DFTBuilder.h
+++ b/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;
diff --git a/src/storage/dft/DFTStateGenerationInfo.h b/src/storage/dft/DFTStateGenerationInfo.h
index 84680979a..bc7e56140 100644
--- a/src/storage/dft/DFTStateGenerationInfo.h
+++ b/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;
}
@@ -149,4 +149,4 @@ namespace storm {
};
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/dft/elements/DFTAnd.h b/src/storage/dft/elements/DFTAnd.h
index 5a5763166..00f671837 100644
--- a/src/storage/dft/elements/DFTAnd.h
+++ b/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);
diff --git a/src/storage/dft/elements/DFTBE.h b/src/storage/dft/elements/DFTBE.h
index d41e37344..216227af6 100644
--- a/src/storage/dft/elements/DFTBE.h
+++ b/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;
}
@@ -113,4 +113,4 @@ namespace storm {
return os << "{" << be.name() << "} BE(" << be.activeFailureRate() << ", " << be.passiveFailureRate() << ")";
}
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/dft/elements/DFTDependency.h b/src/storage/dft/elements/DFTDependency.h
index 44a5ab9df..2c5b7d0cc 100644
--- a/src/storage/dft/elements/DFTDependency.h
+++ b/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;
}
@@ -114,4 +114,4 @@ namespace storm {
};
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/dft/elements/DFTElement.h b/src/storage/dft/elements/DFTElement.h
index 366d0fe91..2eaaff12a 100644
--- a/src/storage/dft/elements/DFTElement.h
+++ b/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());
diff --git a/src/storage/dft/elements/DFTOr.h b/src/storage/dft/elements/DFTOr.h
index 93e481d35..3b0fc37d7 100644
--- a/src/storage/dft/elements/DFTOr.h
+++ b/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);
}
diff --git a/src/storage/dft/elements/DFTPand.h b/src/storage/dft/elements/DFTPand.h
index 86472d76f..bb18efe72 100644
--- a/src/storage/dft/elements/DFTPand.h
+++ b/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);
@@ -53,4 +53,4 @@ namespace storm {
}
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/dft/elements/DFTRestriction.h b/src/storage/dft/elements/DFTRestriction.h
index 25441b5b1..f4a03f688 100644
--- a/src/storage/dft/elements/DFTRestriction.h
+++ b/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)
{
@@ -207,4 +207,4 @@ namespace storm {
};
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/dft/elements/DFTVot.h b/src/storage/dft/elements/DFTVot.h
index 776055848..0b03954ca 100644
--- a/src/storage/dft/elements/DFTVot.h
+++ b/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)
@@ -77,4 +77,4 @@ namespace storm {
}
}
-}
\ No newline at end of file
+}
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 7fa292427..ce213cf08 100644
--- a/src/utility/storm.h
+++ b/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());