diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp
index b3b416cfc..7b997293f 100644
--- a/src/models/sparse/MarkovAutomaton.cpp
+++ b/src/models/sparse/MarkovAutomaton.cpp
@@ -43,8 +43,8 @@ namespace storm {
std::unordered_map<std::string, RewardModelType>&& rewardModels,
boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
: NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(this->checkIsClosed()) {
- assert(probabilities);
- assert(this->getTransitionMatrix().isProbabilistic());
+ STORM_LOG_ASSERT(probabilities, "Matrix must be probabilistic.");
+ STORM_LOG_ASSERT(this->getTransitionMatrix().isProbabilistic(), "Matrix must be probabilistic.");
}
template <typename ValueType, typename RewardModelType>
@@ -244,10 +244,10 @@ namespace storm {
// Get number of choices in current state
uint_fast64_t numberChoices = this->getTransitionMatrix().getRowGroupIndices()[state + 1] - this->getTransitionMatrix().getRowGroupIndices()[state];
if (isMarkovianState(state)) {
- assert(numberChoices == 1);
+ STORM_LOG_ASSERT(numberChoices == 1, "Wrong number of choices for markovian state.");
}
if (numberChoices > 1) {
- assert(isProbabilisticState(state));
+ STORM_LOG_ASSERT(isProbabilisticState(state), "State is not probabilistic.");
return false;
}
}
@@ -276,7 +276,7 @@ namespace storm {
storm::solver::stateelimination::MAEliminator<storm::models::sparse::Dtmc<ValueType>> stateEliminator(flexibleMatrix, flexibleBackwardTransitions);
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
- assert(!this->isHybridState(state));
+ STORM_LOG_ASSERT(!this->isHybridState(state), "State is hybrid.");
if (this->isProbabilisticState(state)) {
// Eliminate this probabilistic state
stateEliminator.eliminateState(state, true);
@@ -293,7 +293,7 @@ namespace storm {
// State is eliminated and can be discarded
keepStates.set(state, false);
} else {
- assert(this->isMarkovianState(state));
+ STORM_LOG_ASSERT(this->isMarkovianState(state), "State is not markovian.");
// Copy transitions
for (uint_fast64_t row = flexibleMatrix.getRowGroupIndices()[state]; row < flexibleMatrix.getRowGroupIndices()[state + 1]; ++row) {
for (auto const& entry : flexibleMatrix.getRow(row)) {
diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp
index 265f0d8b0..a47214753 100644
--- a/src/models/sparse/Model.cpp
+++ b/src/models/sparse/Model.cpp
@@ -91,7 +91,7 @@ namespace storm {
template<typename ValueType, typename RewardModelType>
RewardModelType& Model<ValueType, RewardModelType>::rewardModel(std::string const& rewardModelName) {
- assert(this->hasRewardModel(rewardModelName));
+ STORM_LOG_ASSERT(this->hasRewardModel(rewardModelName), "Model has no reward model.");
return this->rewardModels.find(rewardModelName)->second;
}
@@ -117,7 +117,7 @@ namespace storm {
if(this->hasRewardModel(rewardModelName)) {
STORM_LOG_THROW(!(this->hasRewardModel(rewardModelName)), storm::exceptions::IllegalArgumentException, "A reward model with the given name '" << rewardModelName << "' already exists.");
}
- assert(newRewardModel.isCompatible(this->getNumberOfStates(), this->getTransitionMatrix().getRowCount()));
+ STORM_LOG_ASSERT(newRewardModel.isCompatible(this->getNumberOfStates(), this->getTransitionMatrix().getRowCount()), "New reward model is not compatible.");
this->rewardModels.emplace(rewardModelName, newRewardModel);
}
diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp
index 4cab9bbb4..0c9b6de89 100644
--- a/src/models/sparse/StandardRewardModel.cpp
+++ b/src/models/sparse/StandardRewardModel.cpp
@@ -37,13 +37,13 @@ namespace storm {
template<typename ValueType>
std::vector<ValueType> const& StandardRewardModel<ValueType>::getStateRewardVector() const {
- assert(this->hasStateRewards());
+ STORM_LOG_ASSERT(this->hasStateRewards(), "No state rewards available.");
return this->optionalStateRewardVector.get();
}
template<typename ValueType>
std::vector<ValueType>& StandardRewardModel<ValueType>::getStateRewardVector() {
- assert(this->hasStateRewards());
+ STORM_LOG_ASSERT(this->hasStateRewards(), "No state rewards available.");
return this->optionalStateRewardVector.get();
}
@@ -54,16 +54,16 @@ namespace storm {
template<typename ValueType>
ValueType const& StandardRewardModel<ValueType>::getStateReward(uint_fast64_t state) const {
- assert(this->hasStateRewards());
- assert(state < this->optionalStateRewardVector.get().size());
+ STORM_LOG_ASSERT(this->hasStateRewards(), "No state rewards available.");
+ STORM_LOG_ASSERT(state < this->optionalStateRewardVector.get().size(), "Invalid state.");
return this->optionalStateRewardVector.get()[state];
}
template<typename ValueType>
template<typename T>
void StandardRewardModel<ValueType>::setStateReward(uint_fast64_t state, T const & newReward) {
- assert(this->hasStateRewards());
- assert(state < this->optionalStateRewardVector.get().size());
+ STORM_LOG_ASSERT(this->hasStateRewards(), "No state rewards available.");
+ STORM_LOG_ASSERT(state < this->optionalStateRewardVector.get().size(), "Invalid state.");
this->optionalStateRewardVector.get()[state] = newReward;
}
@@ -76,28 +76,28 @@ namespace storm {
template<typename ValueType>
std::vector<ValueType> const& StandardRewardModel<ValueType>::getStateActionRewardVector() const {
- assert(this->hasStateActionRewards());
+ STORM_LOG_ASSERT(this->hasStateActionRewards(), "No state action rewards available.");
return this->optionalStateActionRewardVector.get();
}
template<typename ValueType>
std::vector<ValueType>& StandardRewardModel<ValueType>::getStateActionRewardVector() {
- assert(this->hasStateActionRewards());
+ STORM_LOG_ASSERT(this->hasStateActionRewards(), "No state action rewards available.");
return this->optionalStateActionRewardVector.get();
}
template<typename ValueType>
ValueType const& StandardRewardModel<ValueType>::getStateActionReward(uint_fast64_t choiceIndex) const {
- assert(this->hasStateActionRewards());
- assert(choiceIndex < this->optionalStateActionRewardVector.get().size());
+ STORM_LOG_ASSERT(this->hasStateActionRewards(), "No state action rewards available.");
+ STORM_LOG_ASSERT(choiceIndex < this->optionalStateActionRewardVector.get().size(), "Invalid choiceIndex.");
return this->optionalStateActionRewardVector.get()[choiceIndex];
}
template<typename ValueType>
template<typename T>
void StandardRewardModel<ValueType>::setStateActionReward(uint_fast64_t choiceIndex, T const &newValue) {
- assert(this->hasStateActionRewards());
- assert(choiceIndex < this->optionalStateActionRewardVector.get().size());
+ STORM_LOG_ASSERT(this->hasStateActionRewards(), "No state action rewards available.");
+ STORM_LOG_ASSERT(choiceIndex < this->optionalStateActionRewardVector.get().size(), "Invalid choiceIndex.");
this->optionalStateActionRewardVector.get()[choiceIndex] = newValue;
}
@@ -330,4 +330,4 @@ namespace storm {
}
}
-}
\ No newline at end of file
+}
diff --git a/src/permissivesched/MILPPermissiveSchedulers.h b/src/permissivesched/MILPPermissiveSchedulers.h
index b0f6b4529..fe5a48e11 100644
--- a/src/permissivesched/MILPPermissiveSchedulers.h
+++ b/src/permissivesched/MILPPermissiveSchedulers.h
@@ -51,13 +51,13 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
bool foundSolution() const override {
- assert(mCalledOptimizer);
+ STORM_LOG_ASSERT(mCalledOptimizer, "Optimizer not called.");
return !solver.isInfeasible();
}
SubMDPPermissiveScheduler<RM> getScheduler() const override {
- assert(mCalledOptimizer);
- assert(foundSolution());
+ STORM_LOG_ASSERT(mCalledOptimizer, "Optimizer not called.");
+ STORM_LOG_ASSERT(foundSolution(), "Solution not found.");
SubMDPPermissiveScheduler<RM> result(this->mdp, true);
@@ -103,7 +103,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
*/
void createVariables(PermissiveSchedulerPenalties const& penalties, storm::storage::BitVector const& relevantStates) {
// We need the unique initial state later, so we get that one before looping.
- assert(this->mdp.getInitialStates().getNumberOfSetBits() == 1);
+ STORM_LOG_ASSERT(this->mdp.getInitialStates().getNumberOfSetBits() == 1, "No unique initial state.");
uint_fast64_t initialStateIndex = this->mdp.getInitialStates().getNextSetIndex(0);
storm::expressions::Variable var;
@@ -151,9 +151,9 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
// (5) and (7) are omitted on purpose (-- we currenty do not support controllability of actions -- )
// (1)
- assert(this->mdp.getInitialStates().getNumberOfSetBits() == 1);
+ STORM_LOG_ASSERT(this->mdp.getInitialStates().getNumberOfSetBits() == 1, "No unique initial state.");
uint_fast64_t initialStateIndex = this->mdp.getInitialStates().getNextSetIndex(0);
- assert(relevantStates[initialStateIndex]);
+ STORM_LOG_ASSERT(relevantStates[initialStateIndex], "Initial state not relevant.");
if(lowerBound) {
solver.addConstraint("c1", mProbVariables[initialStateIndex] >= solver.getConstant(boundary));
} else {
@@ -206,9 +206,9 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
std::string satstring = to_string(sat);
// (8)
if(relevantStates[entry.getColumn()]) {
- assert(mGammaVariables.count(entry.getColumn()) > 0);
- assert(mGammaVariables.count(s) > 0);
- assert(mBetaVariables.count(sat) > 0);
+ STORM_LOG_ASSERT(mGammaVariables.count(entry.getColumn()) > 0, "Entry not found.");
+ STORM_LOG_ASSERT(mGammaVariables.count(s) > 0, "Entry not found.");
+ STORM_LOG_ASSERT(mBetaVariables.count(sat) > 0, "Entry not found.");
solver.addConstraint("c8-" + satstring, mGammaVariables[entry.getColumn()] < mGammaVariables[s] + (solver.getConstant(1) - mBetaVariables[sat]));
}
}
diff --git a/src/permissivesched/PermissiveSchedulerPenalty.h b/src/permissivesched/PermissiveSchedulerPenalty.h
index bb680defa..f25f61ac1 100644
--- a/src/permissivesched/PermissiveSchedulerPenalty.h
+++ b/src/permissivesched/PermissiveSchedulerPenalty.h
@@ -30,7 +30,7 @@ namespace storm {
}
void set(uint_fast64_t state, uint_fast64_t action, double penalty) {
- assert(penalty >= 1.0);
+ STORM_LOG_ASSERT(penalty >= 1.0, "Penalty too low.");
if(penalty == 1.0) {
auto it = mPenalties.find(std::make_pair(state, action));
if(it != mPenalties.end()) {
diff --git a/src/permissivesched/PermissiveSchedulers.cpp b/src/permissivesched/PermissiveSchedulers.cpp
index 21aa9227c..b35f9549c 100644
--- a/src/permissivesched/PermissiveSchedulers.cpp
+++ b/src/permissivesched/PermissiveSchedulers.cpp
@@ -17,7 +17,7 @@ namespace storm {
template<typename RM>
boost::optional<SubMDPPermissiveScheduler<RM>> computePermissiveSchedulerViaMILP(storm::models::sparse::Mdp<double, RM> const& mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Mdp<double, RM>> propMC(mdp);
- assert(safeProp.getSubformula().isEventuallyFormula());
+ STORM_LOG_ASSERT(safeProp.getSubformula().isEventuallyFormula(), "No eventually formula.");
auto backwardTransitions = mdp.getBackwardTransitions();
storm::storage::BitVector goalstates = propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
goalstates = storm::utility::graph::performProb1A(mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates);
@@ -44,7 +44,7 @@ namespace storm {
template<typename RM>
boost::optional<SubMDPPermissiveScheduler<RM>> computePermissiveSchedulerViaSMT(storm::models::sparse::Mdp<double, RM> const& mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Mdp<double, RM>> propMC(mdp);
- assert(safeProp.getSubformula().isEventuallyFormula());
+ STORM_LOG_ASSERT(safeProp.getSubformula().isEventuallyFormula(), "No eventually formula.");
auto backwardTransitions = mdp.getBackwardTransitions();
storm::storage::BitVector goalstates = propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
goalstates = storm::utility::graph::performProb1A(mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates);
diff --git a/src/permissivesched/PermissiveSchedulers.h b/src/permissivesched/PermissiveSchedulers.h
index 7d0bdb3f7..eb09d4b24 100644
--- a/src/permissivesched/PermissiveSchedulers.h
+++ b/src/permissivesched/PermissiveSchedulers.h
@@ -32,7 +32,7 @@ namespace storm {
}
void disable(uint_fast64_t choiceIndex) {
- assert(choiceIndex < enabledChoices.size());
+ STORM_LOG_ASSERT(choiceIndex < enabledChoices.size(), "Invalid choiceIndex.");
enabledChoices.set(choiceIndex, false);
}
diff --git a/src/permissivesched/SmtBasedPermissiveSchedulers.h b/src/permissivesched/SmtBasedPermissiveSchedulers.h
index bfc1530b8..ed183866c 100644
--- a/src/permissivesched/SmtBasedPermissiveSchedulers.h
+++ b/src/permissivesched/SmtBasedPermissiveSchedulers.h
@@ -34,12 +34,12 @@ namespace storm {
}
bool foundSolution() const override {
- assert(mPerformedSmtLoop);
+ STORM_LOG_ASSERT(mPerformedSmtLoop, "SMT loop not performed.");
return mFoundSolution;
}
SubMDPPermissiveScheduler<RM> getScheduler() const override {
- assert(foundSolution());
+ STORM_LOG_ASSERT(foundSolution(), "Solution not found.");
SubMDPPermissiveScheduler<RM> result(this->mdp, true);
for(auto const& entry : multistrategyVariables) {
if(!multistrategyVariablesToTakenMap.at(entry.second)) {
@@ -98,9 +98,9 @@ namespace storm {
// (4) and (7) are omitted on purpose (-- we currenty do not support controllability of actions -- )
// (1)
- assert(this->mdp.getInitialStates().getNumberOfSetBits() == 1);
+ STORM_LOG_ASSERT(this->mdp.getInitialStates().getNumberOfSetBits() == 1, "No unique initial state.");
uint_fast64_t initialStateIndex = this->mdp.getInitialStates().getNextSetIndex(0);
- assert(relevantStates[initialStateIndex]);
+ STORM_LOG_ASSERT(relevantStates[initialStateIndex], "Initial state not relevant.");
if(lowerBound) {
solver.add(mProbVariables[initialStateIndex] >= manager.rational(boundary));
} else {
@@ -162,9 +162,9 @@ namespace storm {
// std::string satstring = to_string(sat);
// // (8)
// if(relevantStates[entry.getColumn()]) {
-// assert(mGammaVariables.count(entry.getColumn()) > 0);
-// assert(mGammaVariables.count(s) > 0);
-// assert(mBetaVariables.count(sat) > 0);
+// STORM_LOG_ASSERT(mGammaVariables.count(entry.getColumn()) > 0, "Entry not found.");
+// STORM_LOG_ASSERT(mGammaVariables.count(s) > 0, "Entry not found.");
+// STORM_LOG_ASSERT(mBetaVariables.count(sat) > 0, "Entry not found.");
// solver.addConstraint("c8-" + satstring, mGammaVariables[entry.getColumn()] < mGammaVariables[s] + (solver.getConstant(1) - mBetaVariables[sat]) + mProbVariables[s]); // With rewards, we have to change this.
// }
// }
diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h
index 71ea10ee2..a9c497d45 100644
--- a/src/solver/MinMaxLinearEquationSolver.h
+++ b/src/solver/MinMaxLinearEquationSolver.h
@@ -102,7 +102,7 @@ namespace storm {
* Can only be called after the direction has been set.
*/
virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const {
- assert(isSet(this->direction));
+ STORM_LOG_ASSERT(isSet(this->direction), "Direction not set.");
solveEquationSystem(convert(this->direction), x, b, multiplyResult, newX);
}
diff --git a/src/solver/OptimizationDirection.cpp b/src/solver/OptimizationDirection.cpp
index cd88657b9..71d0760ed 100644
--- a/src/solver/OptimizationDirection.cpp
+++ b/src/solver/OptimizationDirection.cpp
@@ -1,6 +1,6 @@
#include "OptimizationDirection.h"
#include <iostream>
-#include <cassert>
+#include "src/utility/macros.h"
namespace storm {
namespace solver {
@@ -18,7 +18,7 @@ namespace storm {
}
OptimizationDirection convert(OptimizationDirectionSetting s) {
- assert(isSet(s));
+ STORM_LOG_ASSERT(isSet(s), "Setting is not set.");
return static_cast<OptimizationDirection>(s);
}
diff --git a/src/solver/stateelimination/StateEliminator.cpp b/src/solver/stateelimination/StateEliminator.cpp
index 01dc8a5af..6189cb2b0 100644
--- a/src/solver/stateelimination/StateEliminator.cpp
+++ b/src/solver/stateelimination/StateEliminator.cpp
@@ -70,7 +70,7 @@ namespace storm {
// Skip the state itself as one of its predecessors.
if (predecessor == state) {
- assert(hasSelfLoop);
+ STORM_LOG_ASSERT(hasSelfLoop, "State has no self loop.");
continue;
}
diff --git a/src/storage/FlexibleSparseMatrix.cpp b/src/storage/FlexibleSparseMatrix.cpp
index 2e3a4e876..5ee31060e 100644
--- a/src/storage/FlexibleSparseMatrix.cpp
+++ b/src/storage/FlexibleSparseMatrix.cpp
@@ -51,15 +51,15 @@ namespace storm {
template<typename ValueType>
typename FlexibleSparseMatrix<ValueType>::row_type& FlexibleSparseMatrix<ValueType>::getRow(index_type rowGroup, index_type offset) {
- assert(rowGroup < this->getRowGroupCount());
- assert(offset < this->getRowGroupSize(rowGroup));
+ STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Invalid rowGroup.");
+ STORM_LOG_ASSERT(offset < this->getRowGroupSize(rowGroup), "Invalid offset.");
return getRow(rowGroupIndices[rowGroup] + offset);
}
template<typename ValueType>
typename FlexibleSparseMatrix<ValueType>::row_type const& FlexibleSparseMatrix<ValueType>::getRow(index_type rowGroup, index_type offset) const {
- assert(rowGroup < this->getRowGroupCount());
- assert(offset < this->getRowGroupSize(rowGroup));
+ STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Invalid rowGroup.");
+ STORM_LOG_ASSERT(offset < this->getRowGroupSize(rowGroup), "Invalid offset.");
return getRow(rowGroupIndices[rowGroup] + offset);
}
@@ -112,7 +112,7 @@ namespace storm {
this->columnCount = 0;
for (auto const& row : this->data) {
for (auto const& element : row) {
- assert(!storm::utility::isZero(element.getValue()));
+ STORM_LOG_ASSERT(!storm::utility::isZero(element.getValue()), "Entry is 0.");
++this->nonzeroEntryCount;
this->columnCount = std::max(element.getColumn() + 1, this->columnCount);
}
@@ -252,4 +252,4 @@ namespace storm {
#endif
} // namespace storage
-} // namespace storm
\ No newline at end of file
+} // namespace storm
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index bfed8f49c..4b763e383 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -277,9 +277,9 @@ namespace storm {
}
maxColumn = std::max(maxColumn, elem.getColumn());
}
- assert(changed || highestColumn == maxColumn);
+ STORM_LOG_ASSERT(changed || highestColumn == maxColumn, "Incorrect maximal column.");
highestColumn = maxColumn;
- assert(changed || lastColumn == columnsAndValues[columnsAndValues.size() - 1].getColumn());
+ STORM_LOG_ASSERT(changed || lastColumn == columnsAndValues[columnsAndValues.size() - 1].getColumn(), "Incorrect last column.");
lastColumn = columnsAndValues[columnsAndValues.size() - 1].getColumn();
if (changed) {
@@ -305,10 +305,10 @@ namespace storm {
return a.getColumn() < b.getColumn();
});
// Assert no equal elements
- assert(std::is_sorted(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows,
+ STORM_LOG_ASSERT(std::is_sorted(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows,
[](MatrixEntry<index_type, value_type> const& a, MatrixEntry<index_type, value_type> const& b) {
return a.getColumn() <= b.getColumn();
- }));
+ }), "Columns not sorted.");
}
}
} else {
@@ -320,10 +320,10 @@ namespace storm {
return a.getColumn() < b.getColumn();
});
// Assert no equal elements
- assert(std::is_sorted(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows,
+ STORM_LOG_ASSERT(std::is_sorted(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows,
[](MatrixEntry<index_type, value_type> const& a, MatrixEntry<index_type, value_type> const& b) {
return a.getColumn() <= b.getColumn();
- }));
+ }), "Columns not sorted.");
}
}
@@ -1368,7 +1368,7 @@ namespace storm {
void SparseMatrix<ValueType>::printAsMatlabMatrix(std::ostream& out) const {
// Iterate over all row groups.
for (typename SparseMatrix<ValueType>::index_type group = 0; group < this->getRowGroupCount(); ++group) {
- assert(this->getRowGroupSize(group) == 1);
+ STORM_LOG_ASSERT(this->getRowGroupSize(group) == 1, "Incorrect row group size.");
for (typename SparseMatrix<ValueType>::index_type i = this->getRowGroupIndices()[group]; i < this->getRowGroupIndices()[group + 1]; ++i) {
typename SparseMatrix<ValueType>::index_type nextIndex = this->rowIndications[i];
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 374859af5..c170d43a9 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -11,6 +11,7 @@
#include <boost/optional.hpp>
#include "src/utility/OsDetection.h"
+#include "src/utility/macros.h"
#include "src/adapters/CarlAdapter.h"
// Forward declaration for adapter classes.
diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h
index 6507e3b07..6d86f2df9 100644
--- a/src/storage/bisimulation/BisimulationDecomposition.h
+++ b/src/storage/bisimulation/BisimulationDecomposition.h
@@ -120,7 +120,7 @@ namespace storm {
}
OptimizationDirection getOptimizationDirection() const {
- assert(optimalityType);
+ STORM_LOG_ASSERT(optimalityType, "Optimality type not set.");
return optimalityType.get();
}
// A flag that indicates whether a measure driven initial partition is to be used. If this flag is set
diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index 5c70c475d..5fdf44ab3 100644
--- a/src/storage/dft/DFT.cpp
+++ b/src/storage/dft/DFT.cpp
@@ -14,7 +14,7 @@ namespace storm {
template<typename ValueType>
DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) {
- assert(elementIndicesCorrect());
+ STORM_LOG_ASSERT(elementIndicesCorrect(), "Ids incorrect.");
size_t nrRepresentatives = 0;
for (auto& elem : mElements) {
@@ -100,9 +100,9 @@ namespace storm {
} else {
// Generate information according to symmetries
for (size_t symmetryIndex : symmetries.sortedSymmetries) {
- assert(!visited[symmetryIndex]);
+ STORM_LOG_ASSERT(!visited[symmetryIndex], "Element already considered for symmetry.");
auto const& symmetryGroup = symmetries.groups.at(symmetryIndex);
- assert(!symmetryGroup.empty());
+ STORM_LOG_ASSERT(!symmetryGroup.empty(), "No symmetry available.");
// Insert all elements of first subtree of each symmetry
size_t groupIndex = stateIndex;
@@ -117,14 +117,14 @@ namespace storm {
// Mirror symmetries
size_t noSymmetricElements = symmetryGroup.front().size();
- assert(noSymmetricElements > 1);
+ STORM_LOG_ASSERT(noSymmetricElements > 1, "No symmetry available.");
for (std::vector<size_t> symmetricElements : symmetryGroup) {
- assert(symmetricElements.size() == noSymmetricElements);
+ STORM_LOG_ASSERT(symmetricElements.size() == noSymmetricElements, "No. of symmetric elements do not coincide.");
if (visited[symmetricElements[1]]) {
// Elements already mirrored
for (size_t index : symmetricElements) {
- assert(visited[index]);
+ STORM_LOG_ASSERT(visited[index], "Element not mirrored.");
}
continue;
}
@@ -143,13 +143,13 @@ namespace storm {
generationInfo.addStateIndex(symmetricElement, index + offset * i);
stateIndex += 2;
- assert((activationIndex > 0) == isRepresentative(symmetricElement));
+ STORM_LOG_ASSERT((activationIndex > 0) == isRepresentative(symmetricElement), "Bits for representative incorrect.");
if (activationIndex > 0) {
generationInfo.addSpareActivationIndex(symmetricElement, activationIndex + offset * i);
++stateIndex;
}
- assert((usageIndex > 0) == mElements[symmetricElement]->isSpareGate());
+ STORM_LOG_ASSERT((usageIndex > 0) == mElements[symmetricElement]->isSpareGate(), "Bits for usage incorrect.");
if (usageIndex > 0) {
generationInfo.addSpareUsageIndex(symmetricElement, usageIndex + offset * i);
stateIndex += generationInfo.usageInfoBits();
@@ -187,15 +187,15 @@ namespace storm {
generationInfo.generateSymmetries(symmetries);
STORM_LOG_TRACE(generationInfo);
- assert(stateIndex == mStateVectorSize);
- assert(visited.full());
+ STORM_LOG_ASSERT(stateIndex == mStateVectorSize, "Id incorrect.");
+ STORM_LOG_ASSERT(visited.full(), "Not all elements considered.");
return generationInfo;
}
template<typename ValueType>
size_t DFT<ValueType>::generateStateInfo(DFTStateGenerationInfo& generationInfo, size_t id, storm::storage::BitVector& visited, size_t stateIndex) const {
- assert(!visited[id]);
+ STORM_LOG_ASSERT(!visited[id], "Element already visited.");
visited.set(id);
// Reserve bits for element
@@ -238,7 +238,7 @@ namespace storm {
template<typename ValueType>
std::vector<DFT<ValueType>> DFT<ValueType>::topModularisation() const {
- assert(isGate(mTopLevelIndex));
+ STORM_LOG_ASSERT(isGate(mTopLevelIndex), "Top level element is no gate.");
auto const& children = getGate(mTopLevelIndex)->children();
std::map<size_t, std::vector<size_t>> subdfts;
for(auto const& child : children) {
@@ -250,7 +250,7 @@ namespace storm {
if (isGate(child->id())) {
isubdft = getGate(child->id())->independentSubDft(false);
} else {
- assert(isBasicElement(child->id()));
+ STORM_LOG_ASSERT(isBasicElement(child->id()), "Child is no BE.");
if(getBasicElement(child->id())->hasIngoingDependencies()) {
STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation.");
return {*this};
@@ -309,16 +309,16 @@ namespace storm {
// Add rewritten elements
for (std::vector<size_t> rewrites : rewriteIds) {
- assert(rewrites.size() > 1);
- assert(mElements[rewrites[1]]->hasParents());
- assert(mElements[rewrites[1]]->parents().front()->isGate());
+ STORM_LOG_ASSERT(rewrites.size() > 1, "No rewritten elements.");
+ STORM_LOG_ASSERT(mElements[rewrites[1]]->hasParents(), "Rewritten elements has no parents.");
+ STORM_LOG_ASSERT(mElements[rewrites[1]]->parents().front()->isGate(), "Rewritten element has no parent gate.");
DFTGatePointer originalParent = std::static_pointer_cast<DFTGate<ValueType>>(mElements[rewrites[1]]->parents().front());
std::string newParentName = builder.getUniqueName(originalParent->name());
// Accumulate children names
std::vector<std::string> childrenNames;
for (size_t i = 1; i < rewrites.size(); ++i) {
- assert(mElements[rewrites[i]]->parents().front()->id() == originalParent->id()); // Children have the same father
+ STORM_LOG_ASSERT(mElements[rewrites[i]]->parents().front()->id() == originalParent->id(), "Children have the same father");
childrenNames.push_back(mElements[rewrites[i]]->name());
}
@@ -390,7 +390,7 @@ namespace storm {
stream << "}" << std::endl;
return stream.str();
}
- assert(it != mTopModule.end());
+ STORM_LOG_ASSERT(it != mTopModule.end(), "Element not found.");
stream << mElements[(*it)]->name();
++it;
while(it != mTopModule.end()) {
@@ -403,7 +403,7 @@ namespace storm {
stream << "[" << mElements[spareModule.first]->name() << "] = {";
if (!spareModule.second.empty()) {
std::vector<size_t>::const_iterator it = spareModule.second.begin();
- assert(it != spareModule.second.end());
+ STORM_LOG_ASSERT(it != spareModule.second.end(), "Element not found.");
stream << mElements[(*it)]->name();
++it;
while(it != spareModule.second.end()) {
@@ -494,13 +494,13 @@ namespace storm {
template<typename ValueType>
size_t DFT<ValueType>::getChild(size_t spareId, size_t nrUsedChild) const {
- assert(mElements[spareId]->isSpareGate());
+ STORM_LOG_ASSERT(mElements[spareId]->isSpareGate(), "Element is no spare.");
return getGate(spareId)->children()[nrUsedChild]->id();
}
template<typename ValueType>
size_t DFT<ValueType>::getNrChild(size_t spareId, size_t childId) const {
- assert(mElements[spareId]->isSpareGate());
+ STORM_LOG_ASSERT(mElements[spareId]->isSpareGate(), "Element is no spare.");
DFTElementVector children = getGate(spareId)->children();
for (size_t nrChild = 0; nrChild < children.size(); ++nrChild) {
if (children[nrChild]->id() == childId) {
@@ -551,8 +551,8 @@ namespace storm {
}
}
- assert(isGate(index1));
- assert(isGate(index2));
+ STORM_LOG_ASSERT(isGate(index1), "Element is no gate.");
+ STORM_LOG_ASSERT(isGate(index2), "Element is no gate.");
std::vector<size_t> isubdft1 = getGate(index1)->independentSubDft(false);
std::vector<size_t> isubdft2 = getGate(index2)->independentSubDft(false);
if(isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) {
@@ -591,7 +591,7 @@ namespace storm {
size_t childLeftId = spareLeft->children().at(i)->id();
size_t childRightId = spareRight->children().at(i)->id();
- assert(bijection.count(childLeftId) == 0);
+ STORM_LOG_ASSERT(bijection.count(childLeftId) == 0, "Child already part of bijection.");
if (childLeftId == childRightId) {
// Ignore shared child
continue;
diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index 6fdfd08ef..7b0177d07 100644
--- a/src/storage/dft/DFT.h
+++ b/src/storage/dft/DFT.h
@@ -118,7 +118,7 @@ namespace storm {
if(representativeId == mTopLevelIndex) {
return mTopModule;
} else {
- assert(mSpareModules.count(representativeId)>0);
+ STORM_LOG_ASSERT(mSpareModules.count(representativeId) > 0, "Representative not found.");
return mSpareModules.find(representativeId)->second;
}
}
@@ -145,7 +145,7 @@ namespace storm {
* @param index The id of the element
*/
DFTElementCPointer getElement(size_t index) const {
- assert(index < nrElements());
+ STORM_LOG_ASSERT(index < nrElements(), "Index invalid.");
return mElements[index];
}
@@ -166,7 +166,7 @@ namespace storm {
}
std::shared_ptr<DFTBE<ValueType> const> getBasicElement(size_t index) const {
- assert(isBasicElement(index));
+ STORM_LOG_ASSERT(isBasicElement(index), "Element is no BE.");
return std::static_pointer_cast<DFTBE<ValueType> const>(mElements[index]);
}
@@ -175,17 +175,17 @@ namespace storm {
}
std::shared_ptr<DFTGate<ValueType> const> getGate(size_t index) const {
- assert(isGate(index));
+ STORM_LOG_ASSERT(isGate(index), "Element is no gate.");
return std::static_pointer_cast<DFTGate<ValueType> const>(mElements[index]);
}
std::shared_ptr<DFTDependency<ValueType> const> getDependency(size_t index) const {
- assert(isDependency(index));
+ STORM_LOG_ASSERT(isDependency(index), "Element is no dependency.");
return std::static_pointer_cast<DFTDependency<ValueType> const>(mElements[index]);
}
std::shared_ptr<DFTRestriction<ValueType> const> getRestriction(size_t index) const {
- assert(isRestriction(index));
+ STORM_LOG_ASSERT(isRestriction(index), "Element is no restriction.");
return std::static_pointer_cast<DFTRestriction<ValueType> const>(mElements[index]);
}
@@ -215,7 +215,7 @@ namespace storm {
}
DFTElementCPointer getRepresentant(size_t id) const {
- assert(hasRepresentant(id));
+ STORM_LOG_ASSERT(hasRepresentant(id), "Element has no representant.");
return getElement(mRepresentants.find(id)->second);
}
diff --git a/src/storage/dft/DFTElementState.h b/src/storage/dft/DFTElementState.h
index d191cc2d9..548eb6c88 100644
--- a/src/storage/dft/DFTElementState.h
+++ b/src/storage/dft/DFTElementState.h
@@ -2,7 +2,7 @@
#ifndef DFTELEMENTSTATE_H
#define DFTELEMENTSTATE_H
-#include <cassert>
+#include "src/utility/macros.h"
namespace storm {
namespace storage {
@@ -18,8 +18,10 @@ namespace storm {
return os << "Failsafe";
case DFTElementState::DontCare:
return os << "Don't Care";
+ default:
+ STORM_LOG_ASSERT(false, "Element state not known.");
+ return os;
}
- assert(false);
}
inline char toChar(DFTElementState st) {
@@ -32,8 +34,10 @@ namespace storm {
return 'S';
case DFTElementState::DontCare:
return '-';
+ default:
+ STORM_LOG_ASSERT(false, "Element state not known.");
+ return ' ';
}
- assert(false);
}
enum class DFTDependencyState {Passive = 0, Unsuccessful = 1, Successful = 2, DontCare = 3};
@@ -48,8 +52,10 @@ namespace storm {
return os << "Unsuccessful";
case DFTDependencyState::DontCare:
return os << "Don't Care";
+ default:
+ STORM_LOG_ASSERT(false, "Element state not known.");
+ return os;
}
- assert(false);
}
inline char toChar(DFTDependencyState st) {
@@ -62,8 +68,10 @@ namespace storm {
return 'U';
case DFTDependencyState::DontCare:
return '-';
+ default:
+ STORM_LOG_ASSERT(false, "Element state not known.");
+ return ' ';
}
- assert(false);
}
}
diff --git a/src/storage/dft/DFTIsomorphism.h b/src/storage/dft/DFTIsomorphism.h
index d94640d9c..1f66e5449 100644
--- a/src/storage/dft/DFTIsomorphism.h
+++ b/src/storage/dft/DFTIsomorphism.h
@@ -1,6 +1,5 @@
#pragma once
-#include <cassert>
#include <vector>
#include <unordered_map>
#include <utility>
@@ -197,7 +196,7 @@ namespace storage {
} else if(dft.isDependency(id)) {
colourize(dft.getDependency(id));
} else {
- assert(dft.isRestriction(id));
+ STORM_LOG_ASSERT(dft.isRestriction(id), "Element is no restriction.");
colourize(dft.getRestriction(id));
}
}
@@ -233,7 +232,7 @@ namespace storage {
res.pdepCandidates[depColour.at(index)] = std::vector<size_t>({index});
}
} else {
- assert(dft.isRestriction(index));
+ STORM_LOG_ASSERT(dft.isRestriction(index), "Element is no restriction.");
auto it = res.restrictionCandidates.find(restrictionColour.at(index));
if(it != res.restrictionCandidates.end()) {
it->second.push_back(index);
@@ -342,14 +341,14 @@ namespace storage {
* Construct the initial bijection.
*/
void constructInitialBijection() {
- assert(candidatesCompatible);
+ STORM_LOG_ASSERT(candidatesCompatible, "Candidates are not compatible.");
// We first construct the currentPermutations, which helps to determine the current state of the check.
initializePermutationsAndTreatTrivialGroups(bleft.beCandidates, bright.beCandidates, currentPermutations.beCandidates);
initializePermutationsAndTreatTrivialGroups(bleft.gateCandidates, bright.gateCandidates, currentPermutations.gateCandidates);
initializePermutationsAndTreatTrivialGroups(bleft.pdepCandidates, bright.pdepCandidates, currentPermutations.pdepCandidates);
initializePermutationsAndTreatTrivialGroups(bleft.restrictionCandidates, bright.restrictionCandidates, currentPermutations.restrictionCandidates);
STORM_LOG_TRACE(bijection.size() << " vs. " << bleft.size() << " vs. " << bright.size());
- assert(bijection.size() == bleft.size());
+ STORM_LOG_ASSERT(bijection.size() == bleft.size(), "No. of bijection elements do not match.");
}
@@ -358,7 +357,7 @@ namespace storage {
* @return true if a next bijection exists.
*/
bool findNextBijection() {
- assert(candidatesCompatible);
+ STORM_LOG_ASSERT(candidatesCompatible, "Candidates are not compatible.");
bool foundNext = false;
if(!currentPermutations.beCandidates.empty()) {
auto it = currentPermutations.beCandidates.begin();
@@ -395,28 +394,28 @@ namespace storage {
if(foundNext) {
for(auto const& colour : bleft.beCandidates) {
if (colour.second.size() > 1) {
- assert(currentPermutations.beCandidates.find(colour.first) != currentPermutations.beCandidates.end());
+ STORM_LOG_ASSERT(currentPermutations.beCandidates.find(colour.first) != currentPermutations.beCandidates.end(), "Colour not found.");
zipVectorsIntoMap(colour.second, currentPermutations.beCandidates.find(colour.first)->second, bijection);
}
}
for(auto const& colour : bleft.gateCandidates) {
if (colour.second.size() > 1) {
- assert(currentPermutations.gateCandidates.find(colour.first) != currentPermutations.gateCandidates.end());
+ STORM_LOG_ASSERT(currentPermutations.gateCandidates.find(colour.first) != currentPermutations.gateCandidates.end(), "Colour not found.");
zipVectorsIntoMap(colour.second, currentPermutations.gateCandidates.find(colour.first)->second, bijection);
}
}
for(auto const& colour : bleft.pdepCandidates) {
if (colour.second.size() > 1) {
- assert(currentPermutations.pdepCandidates.find(colour.first) != currentPermutations.pdepCandidates.end());
+ STORM_LOG_ASSERT(currentPermutations.pdepCandidates.find(colour.first) != currentPermutations.pdepCandidates.end(), "Colour not found.");
zipVectorsIntoMap(colour.second, currentPermutations.pdepCandidates.find(colour.first)->second, bijection);
}
}
for(auto const& colour : bleft.restrictionCandidates) {
if (colour.second.size() > 1) {
- assert(currentPermutations.restrictionCandidates.find(colour.first) != currentPermutations.restrictionCandidates.end());
+ STORM_LOG_ASSERT(currentPermutations.restrictionCandidates.find(colour.first) != currentPermutations.restrictionCandidates.end(), "Colour not found.");
zipVectorsIntoMap(colour.second, currentPermutations.restrictionCandidates.find(colour.first)->second, bijection);
}
}
@@ -430,13 +429,13 @@ namespace storage {
*
*/
bool check() const {
- assert(bijection.size() == bleft.size());
+ STORM_LOG_ASSERT(bijection.size() == bleft.size(), "No. of bijection elements do not match.");
// We can skip BEs, as they are identified by they're homomorphic if they are in the same class
for(auto const& indexpair : bijection) {
// Check type first. Colouring takes care of a lot, but not necesarily everything (e.g. voting thresholds)
equalType(*dft.getElement(indexpair.first), *dft.getElement(indexpair.second));
if(dft.isGate(indexpair.first)) {
- assert(dft.isGate(indexpair.second));
+ STORM_LOG_ASSERT(dft.isGate(indexpair.second), "Element is no gate.");
auto const& lGate = dft.getGate(indexpair.first);
auto const& rGate = dft.getGate(indexpair.second);
if(lGate->isDynamicGate()) {
@@ -483,7 +482,7 @@ namespace storage {
} else if(dft.isDependency(indexpair.first)) {
- assert(dft.isDependency(indexpair.second));
+ STORM_LOG_ASSERT(dft.isDependency(indexpair.second), "Element is no dependency.");
auto const& lDep = dft.getDependency(indexpair.first);
auto const& rDep = dft.getDependency(indexpair.second);
if(bijection.at(lDep->triggerEvent()->id()) != rDep->triggerEvent()->id()) {
@@ -493,7 +492,7 @@ namespace storage {
return false;
}
} else if(dft.isRestriction(indexpair.first)) {
- assert(dft.isRestriction(indexpair.second));
+ STORM_LOG_ASSERT(dft.isRestriction(indexpair.second), "Element is no restriction.");
auto const& lRestr = dft.getRestriction(indexpair.first);
std::vector<size_t> childrenLeftMapped;
for(auto const& child : lRestr->children() ) {
@@ -521,8 +520,8 @@ namespace storage {
}
}
else {
- assert(dft.isBasicElement(indexpair.first));
- assert(dft.isBasicElement(indexpair.second));
+ STORM_LOG_ASSERT(dft.isBasicElement(indexpair.first), "Element is no BE.");
+ STORM_LOG_ASSERT(dft.isBasicElement(indexpair.second), "Element is no BE.");
// No operations required.
}
}
@@ -590,12 +589,12 @@ namespace storage {
for(auto const& colour : right) {
if(colour.second.size()>1) {
auto it = permutations.insert(colour);
- assert(it.second);
+ STORM_LOG_ASSERT(it.second, "Element already contained.");
std::sort(it.first->second.begin(), it.first->second.end());
zipVectorsIntoMap(left.at(colour.first), it.first->second, bijection);
} else {
- assert(colour.second.size() == 1);
- assert(bijection.count(left.at(colour.first).front()) == 0);
+ STORM_LOG_ASSERT(colour.second.size() == 1, "No elements for colour.");
+ STORM_LOG_ASSERT(bijection.count(left.at(colour.first).front()) == 0, "Element already contained.");
bijection[left.at(colour.first).front()] = colour.second.front();
}
}
@@ -606,7 +605,7 @@ namespace storage {
*/
void zipVectorsIntoMap(std::vector<size_t> const& a, std::vector<size_t> const& b, std::map<size_t, size_t>& map) const {
// Assert should pass due to compatibility check
- assert(a.size() == b.size());
+ STORM_LOG_ASSERT(a.size() == b.size(), "Sizes do not match.");
auto it = b.cbegin();
for(size_t lIndex : a) {
map[lIndex] = *it;
@@ -638,4 +637,4 @@ namespace std {
return hasher(p.first) ^ hasher(p.second);
}
};
-}
\ No newline at end of file
+}
diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index 25edf1d38..9a0a16dba 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/src/storage/dft/DFTState.cpp
@@ -11,8 +11,8 @@ namespace storm {
// Initialize uses
for(size_t id : mDft.getSpareIndices()) {
std::shared_ptr<DFTGate<ValueType> const> elem = mDft.getGate(id);
- assert(elem->isSpareGate());
- assert(elem->nrChildren() > 0);
+ STORM_LOG_ASSERT(elem->isSpareGate(), "Element is no spare gate.");
+ STORM_LOG_ASSERT(elem->nrChildren() > 0, "Element has no child.");
this->setUses(id, elem->children()[0]->id());
}
@@ -47,7 +47,7 @@ namespace storm {
// Initialize failable dependencies
for (size_t dependencyId : mDft.getDependencies()) {
std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(dependencyId);
- assert(dependencyId == dependency->id());
+ STORM_LOG_ASSERT(dependencyId == dependency->id(), "Ids do not match.");
if (hasFailed(dependency->triggerEvent()->id()) && getElementState(dependency->dependentEvent()->id()) == DFTElementState::Operational) {
mFailableDependencies.push_back(dependencyId);
STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
@@ -182,9 +182,9 @@ namespace storm {
}
for (auto dependency : mDft.getElement(id)->outgoingDependencies()) {
- assert(dependency->triggerEvent()->id() == id);
+ STORM_LOG_ASSERT(dependency->triggerEvent()->id() == id, "Ids do not match.");
if (getElementState(dependency->dependentEvent()->id()) == DFTElementState::Operational) {
- assert(!isFailsafe(dependency->dependentEvent()->id()));
+ STORM_LOG_ASSERT(!isFailsafe(dependency->dependentEvent()->id()), "Dependent event is failsafe.");
mFailableDependencies.push_back(dependency->id());
STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
}
@@ -194,11 +194,11 @@ namespace storm {
template<typename ValueType>
void DFTState<ValueType>::updateDontCareDependencies(size_t id) {
- assert(mDft.isBasicElement(id));
- assert(hasFailed(id));
+ STORM_LOG_ASSERT(mDft.isBasicElement(id), "Element is no BE.");
+ STORM_LOG_ASSERT(hasFailed(id), "Element has not failed.");
for (auto dependency : mDft.getBasicElement(id)->ingoingDependencies()) {
- assert(dependency->dependentEvent()->id() == id);
+ STORM_LOG_ASSERT(dependency->dependentEvent()->id() == id, "Ids do not match.");
setDependencyDontCare(dependency->id());
}
}
@@ -209,7 +209,7 @@ namespace storm {
STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString());
if (nrFailableDependencies() > 0) {
// Consider failure due to dependency
- assert(index < nrFailableDependencies());
+ STORM_LOG_ASSERT(index < nrFailableDependencies(), "Index invalid.");
std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(mFailableDependencies[index]);
std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true);
mFailableDependencies.erase(mFailableDependencies.begin() + index);
@@ -218,9 +218,9 @@ namespace storm {
return res;
} else {
// Consider "normal" failure
- assert(index < nrFailableBEs());
+ STORM_LOG_ASSERT(index < nrFailableBEs(), "Index invalid.");
std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false);
- assert(res.first->canFail());
+ STORM_LOG_ASSERT(res.first->canFail(), "Element cannot fail.");
mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index);
setFailed(res.first->id());
return res;
@@ -229,7 +229,7 @@ namespace storm {
template<typename ValueType>
void DFTState<ValueType>::letDependencyBeUnsuccessful(size_t index) {
- assert(nrFailableDependencies() > 0 && index < nrFailableDependencies());
+ STORM_LOG_ASSERT(nrFailableDependencies() > 0 && index < nrFailableDependencies(), "Index invalid.");
std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(getDependencyId(index));
mFailableDependencies.erase(mFailableDependencies.begin() + index);
setDependencyUnsuccessful(dependency->id());
@@ -243,7 +243,7 @@ namespace storm {
template<typename ValueType>
bool DFTState<ValueType>::isActive(size_t id) const {
- assert(mDft.isRepresentative(id));
+ STORM_LOG_ASSERT(mDft.isRepresentative(id), "Element is no representative.");
return mStatus[mStateGenerationInfo.getSpareActivationIndex(id)];
}
@@ -277,7 +277,7 @@ namespace storm {
template<typename ValueType>
uint_fast64_t DFTState<ValueType>::extractUses(size_t from) const {
- assert(mStateGenerationInfo.usageInfoBits() < 64);
+ STORM_LOG_ASSERT(mStateGenerationInfo.usageInfoBits() < 64, "UsageInfoBit size too large.");
return mStatus.getAsInt(from, mStateGenerationInfo.usageInfoBits());
}
@@ -294,14 +294,14 @@ namespace storm {
template<typename ValueType>
void DFTState<ValueType>::finalizeUses(size_t spareId) {
- assert(hasFailed(spareId));
+ STORM_LOG_ASSERT(hasFailed(spareId), "Spare has not failed.");
mStatus.setFromInt(mStateGenerationInfo.getSpareUsageIndex(spareId), mStateGenerationInfo.usageInfoBits(), mDft.getMaxSpareChildCount());
}
template<typename ValueType>
bool DFTState<ValueType>::hasOperationalPostSeqElements(size_t id) const {
- assert(!mDft.isDependency(id));
- assert(!mDft.isRestriction(id));
+ STORM_LOG_ASSERT(!mDft.isDependency(id), "Element is dependency.");
+ STORM_LOG_ASSERT(!mDft.isRestriction(id), "Element is restriction.");
auto const& postIds = mStateGenerationInfo.seqRestrictionPostElements(id);
for(size_t id : postIds) {
if(isOperational(id)) {
@@ -315,7 +315,7 @@ namespace storm {
bool DFTState<ValueType>::claimNew(size_t spareId, size_t currentlyUses, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children) {
auto it = children.begin();
while ((*it)->id() != currentlyUses) {
- assert(it != children.end());
+ STORM_LOG_ASSERT(it != children.end(), "Currently used element not found.");
++it;
}
++it;
@@ -377,4 +377,4 @@ namespace storm {
#endif
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h
index f647aae17..8562559b3 100644
--- a/src/storage/dft/DFTState.h
+++ b/src/storage/dft/DFTState.h
@@ -6,7 +6,6 @@
#include <sstream>
#include <memory>
-#include <cassert>
namespace storm {
namespace storage {
@@ -156,7 +155,7 @@ namespace storm {
* @return Id of the dependency
*/
size_t getDependencyId(size_t index) const {
- assert(index < nrFailableDependencies());
+ STORM_LOG_ASSERT(index < nrFailableDependencies(), "Index invalid.");
return mFailableDependencies[index];
}
diff --git a/src/storage/dft/DFTStateSpaceGenerationQueues.h b/src/storage/dft/DFTStateSpaceGenerationQueues.h
index 6ded7cb38..bd71b5fbf 100644
--- a/src/storage/dft/DFTStateSpaceGenerationQueues.h
+++ b/src/storage/dft/DFTStateSpaceGenerationQueues.h
@@ -55,7 +55,7 @@ namespace storm {
}
DFTRestrictionPointer nextRestrictionCheck() {
- assert(!restrictionChecksDone());
+ STORM_LOG_ASSERT(!restrictionChecksDone(), "All restriction checks done already.");
DFTRestrictionPointer next = restrictionChecks.back();
restrictionChecks.pop_back();
return next;
diff --git a/src/storage/expressions/Variable.cpp b/src/storage/expressions/Variable.cpp
index aeb432f2a..5c9660b83 100644
--- a/src/storage/expressions/Variable.cpp
+++ b/src/storage/expressions/Variable.cpp
@@ -1,6 +1,5 @@
#include "src/storage/expressions/Variable.h"
#include "src/storage/expressions/ExpressionManager.h"
-#include <cassert>
namespace storm {
namespace expressions {
@@ -41,7 +40,7 @@ namespace storm {
}
ExpressionManager const& Variable::getManager() const {
- assert(manager != nullptr);
+ STORM_LOG_ASSERT(manager != nullptr, "Manager is null.");
return *manager;
}
@@ -65,4 +64,4 @@ namespace storm {
return this->getType().isNumericalType();
}
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/expressions/Variable.h b/src/storage/expressions/Variable.h
index 3ade039ed..79b430f65 100644
--- a/src/storage/expressions/Variable.h
+++ b/src/storage/expressions/Variable.h
@@ -6,6 +6,7 @@
#include <functional>
#include "src/utility/OsDetection.h"
+#include "src/utility/macros.h"
namespace storm {
namespace expressions {
@@ -155,4 +156,4 @@ namespace std {
};
}
-#endif /* STORM_STORAGE_EXPRESSIONS_VARIABLE_H_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_EXPRESSIONS_VARIABLE_H_ */
diff --git a/src/storage/prism/Assignment.cpp b/src/storage/prism/Assignment.cpp
index a6c8b4456..7aa685a6d 100644
--- a/src/storage/prism/Assignment.cpp
+++ b/src/storage/prism/Assignment.cpp
@@ -1,5 +1,4 @@
#include "Assignment.h"
-#include <cassert>
namespace storm {
namespace prism {
@@ -25,7 +24,7 @@ namespace storm {
bool Assignment::isIdentity() const {
if(this->expression.isVariable()) {
- assert(this->expression.getVariables().size() == 1);
+ STORM_LOG_ASSERT(this->expression.getVariables().size() == 1, "Invalid number of variables.");
//if( variable == *(this->expression.getVariables().begin())) {
// std::cout << variable.getName() << " == " << (this->expression.getVariables().begin())->getName() << std::endl;
//}
diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp
index 5cad634e7..a5a59522d 100644
--- a/src/storage/prism/Command.cpp
+++ b/src/storage/prism/Command.cpp
@@ -1,5 +1,4 @@
#include "Command.h"
-#include <cassert>
namespace storm {
namespace prism {
@@ -32,7 +31,7 @@ namespace storm {
}
storm::prism::Update const& Command::getUpdate(uint_fast64_t index) const {
- assert(index < getNumberOfUpdates());
+ STORM_LOG_ASSERT(index < getNumberOfUpdates(), "Invalid index.");
return this->updates[index];
}
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 0a7b11bd6..ca55258b3 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -1297,7 +1297,7 @@ namespace storm {
}
uint_fast64_t Program::largestActionIndex() const {
- assert(numberOfActions() != 0);
+ STORM_LOG_ASSERT(numberOfActions() != 0, "No actions available.");
return this->indexToActionMap.rbegin()->first;
}
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index 3ffd665ad..4cfd1f58f 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -5,6 +5,7 @@
#include "src/cli/cli.h"
#include "src/exceptions/BaseException.h"
#include "src/utility/macros.h"
+#include "src/builder/DftSmtBuilder.h"
#include <boost/lexical_cast.hpp>
#include "src/settings/modules/GeneralSettings.h"
@@ -44,6 +45,18 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false,
analyser.printResult();
}
+template<typename ValueType>
+void analyzeWithSMT(std::string filename) {
+ std::cout << "Running DFT analysis on file " << filename << " with use of SMT" << std::endl;
+
+ storm::parser::DFTGalileoParser<ValueType> parser;
+ storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
+ storm::builder::DFTSMTBuilder<ValueType> dftSmtBuilder;
+ dftSmtBuilder.convertToSMT(dft);
+ bool sat = dftSmtBuilder.check();
+ std::cout << "SMT result: " << sat << std::endl;
+}
+
/*!
* Initialize the settings manager.
*/
@@ -92,6 +105,22 @@ int main(const int argc, const char** argv) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
+ bool parametric = false;
+#ifdef STORM_HAVE_CARL
+ parametric = generalSettings.isParametricSet();
+#endif
+
+ if (dftSettings.solveWithSMT()) {
+ // Solve with SMT
+ if (parametric) {
+ analyzeWithSMT<storm::RationalFunction>(dftSettings.getDftFilename());
+ } else {
+ analyzeWithSMT<double>(dftSettings.getDftFilename());
+ }
+ storm::utility::cleanUp();
+ return 0;
+ }
+
// Set min or max
bool minimal = true;
if (dftSettings.isComputeMaximalValue()) {
@@ -132,11 +161,6 @@ int main(const int argc, const char** argv) {
STORM_LOG_ASSERT(!pctlFormula.empty(), "Pctl formula empty.");
- bool parametric = false;
-#ifdef STORM_HAVE_CARL
- parametric = generalSettings.isParametricSet();
-#endif
-
// From this point on we are ready to carry out the actual computations.
if (parametric) {
analyzeDFT<storm::RationalFunction>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC() );