sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Replaced assert with STORM_LOG_ASSERT 

Former-commit-id: 692ae47b1b
main
Mavo 9 years ago
parent
929a694a64
commit
e49582c7cf
28 changed files with 181 additions and 152 deletions
Unified View
  1. 12
      src/models/sparse/MarkovAutomaton.cpp
  2. 4
      src/models/sparse/Model.cpp
  3. 24
      src/models/sparse/StandardRewardModel.cpp
  4. 18
      src/permissivesched/MILPPermissiveSchedulers.h
  5. 2
      src/permissivesched/PermissiveSchedulerPenalty.h
  6. 4
      src/permissivesched/PermissiveSchedulers.cpp
  7. 2
      src/permissivesched/PermissiveSchedulers.h
  8. 14
      src/permissivesched/SmtBasedPermissiveSchedulers.h
  9. 2
      src/solver/MinMaxLinearEquationSolver.h
  10. 4
      src/solver/OptimizationDirection.cpp
  11. 2
      src/solver/stateelimination/StateEliminator.cpp
  12. 10
      src/storage/FlexibleSparseMatrix.cpp
  13. 14
      src/storage/SparseMatrix.cpp
  14. 1
      src/storage/SparseMatrix.h
  15. 2
      src/storage/bisimulation/BisimulationDecomposition.h
  16. 48
      src/storage/dft/DFT.cpp
  17. 14
      src/storage/dft/DFT.h
  18. 18
      src/storage/dft/DFTElementState.h
  19. 39
      src/storage/dft/DFTIsomorphism.h
  20. 36
      src/storage/dft/DFTState.cpp
  21. 3
      src/storage/dft/DFTState.h
  22. 2
      src/storage/dft/DFTStateSpaceGenerationQueues.h
  23. 3
      src/storage/expressions/Variable.cpp
  24. 1
      src/storage/expressions/Variable.h
  25. 3
      src/storage/prism/Assignment.cpp
  26. 3
      src/storage/prism/Command.cpp
  27. 2
      src/storage/prism/Program.cpp
  28. 34
      src/storm-dyftee.cpp

12
src/models/sparse/MarkovAutomaton.cpp
View File

@ -43,8 +43,8 @@ namespace storm {
std::unordered_map<std::string, RewardModelType>&& rewardModels, std::unordered_map<std::string, RewardModelType>&& rewardModels,
boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling) 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()) { : 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); STORM_LOG_ASSERT(probabilities, "Matrix must be probabilistic.");
assert(this->getTransitionMatrix().isProbabilistic()); STORM_LOG_ASSERT(this->getTransitionMatrix().isProbabilistic(), "Matrix must be probabilistic.");
} }
template <typename ValueType, typename RewardModelType> template <typename ValueType, typename RewardModelType>
@ -244,10 +244,10 @@ namespace storm {
// Get number of choices in current state // Get number of choices in current state
uint_fast64_t numberChoices = this->getTransitionMatrix().getRowGroupIndices()[state + 1] - this->getTransitionMatrix().getRowGroupIndices()[state]; uint_fast64_t numberChoices = this->getTransitionMatrix().getRowGroupIndices()[state + 1] - this->getTransitionMatrix().getRowGroupIndices()[state];
if (isMarkovianState(state)) { if (isMarkovianState(state)) {
assert(numberChoices == 1); STORM_LOG_ASSERT(numberChoices == 1, "Wrong number of choices for markovian state.");
} }
if (numberChoices > 1) { if (numberChoices > 1) {
assert(isProbabilisticState(state)); STORM_LOG_ASSERT(isProbabilisticState(state), "State is not probabilistic.");
return false; return false;
} }
} }
@ -276,7 +276,7 @@ namespace storm {
storm::solver::stateelimination::MAEliminator<storm::models::sparse::Dtmc<ValueType>> stateEliminator(flexibleMatrix, flexibleBackwardTransitions); storm::solver::stateelimination::MAEliminator<storm::models::sparse::Dtmc<ValueType>> stateEliminator(flexibleMatrix, flexibleBackwardTransitions);
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { 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)) { if (this->isProbabilisticState(state)) {
// Eliminate this probabilistic state // Eliminate this probabilistic state
stateEliminator.eliminateState(state, true); stateEliminator.eliminateState(state, true);
@ -293,7 +293,7 @@ namespace storm {
// State is eliminated and can be discarded // State is eliminated and can be discarded
keepStates.set(state, false); keepStates.set(state, false);
} else { } else {
assert(this->isMarkovianState(state)); STORM_LOG_ASSERT(this->isMarkovianState(state), "State is not markovian.");
// Copy transitions // Copy transitions
for (uint_fast64_t row = flexibleMatrix.getRowGroupIndices()[state]; row < flexibleMatrix.getRowGroupIndices()[state + 1]; ++row) { for (uint_fast64_t row = flexibleMatrix.getRowGroupIndices()[state]; row < flexibleMatrix.getRowGroupIndices()[state + 1]; ++row) {
for (auto const& entry : flexibleMatrix.getRow(row)) { for (auto const& entry : flexibleMatrix.getRow(row)) {

4
src/models/sparse/Model.cpp
View File

@ -91,7 +91,7 @@ namespace storm {
template<typename ValueType, typename RewardModelType> template<typename ValueType, typename RewardModelType>
RewardModelType& Model<ValueType, RewardModelType>::rewardModel(std::string const& rewardModelName) { 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; return this->rewardModels.find(rewardModelName)->second;
} }
@ -117,7 +117,7 @@ namespace storm {
if(this->hasRewardModel(rewardModelName)) { if(this->hasRewardModel(rewardModelName)) {
STORM_LOG_THROW(!(this->hasRewardModel(rewardModelName)), storm::exceptions::IllegalArgumentException, "A reward model with the given name '" << rewardModelName << "' already exists."); 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); this->rewardModels.emplace(rewardModelName, newRewardModel);
} }

24
src/models/sparse/StandardRewardModel.cpp
View File

@ -37,13 +37,13 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
std::vector<ValueType> const& StandardRewardModel<ValueType>::getStateRewardVector() const { std::vector<ValueType> const& StandardRewardModel<ValueType>::getStateRewardVector() const {
assert(this->hasStateRewards()); STORM_LOG_ASSERT(this->hasStateRewards(), "No state rewards available.");
return this->optionalStateRewardVector.get(); return this->optionalStateRewardVector.get();
} }
template<typename ValueType> template<typename ValueType>
std::vector<ValueType>& StandardRewardModel<ValueType>::getStateRewardVector() { std::vector<ValueType>& StandardRewardModel<ValueType>::getStateRewardVector() {
assert(this->hasStateRewards()); STORM_LOG_ASSERT(this->hasStateRewards(), "No state rewards available.");
return this->optionalStateRewardVector.get(); return this->optionalStateRewardVector.get();
} }
@ -54,16 +54,16 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
ValueType const& StandardRewardModel<ValueType>::getStateReward(uint_fast64_t state) const { ValueType const& StandardRewardModel<ValueType>::getStateReward(uint_fast64_t state) const {
assert(this->hasStateRewards()); STORM_LOG_ASSERT(this->hasStateRewards(), "No state rewards available.");
assert(state < this->optionalStateRewardVector.get().size()); STORM_LOG_ASSERT(state < this->optionalStateRewardVector.get().size(), "Invalid state.");
return this->optionalStateRewardVector.get()[state]; return this->optionalStateRewardVector.get()[state];
} }
template<typename ValueType> template<typename ValueType>
template<typename T> template<typename T>
void StandardRewardModel<ValueType>::setStateReward(uint_fast64_t state, T const & newReward) { void StandardRewardModel<ValueType>::setStateReward(uint_fast64_t state, T const & newReward) {
assert(this->hasStateRewards()); STORM_LOG_ASSERT(this->hasStateRewards(), "No state rewards available.");
assert(state < this->optionalStateRewardVector.get().size()); STORM_LOG_ASSERT(state < this->optionalStateRewardVector.get().size(), "Invalid state.");
this->optionalStateRewardVector.get()[state] = newReward; this->optionalStateRewardVector.get()[state] = newReward;
} }
@ -76,28 +76,28 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
std::vector<ValueType> const& StandardRewardModel<ValueType>::getStateActionRewardVector() const { 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(); return this->optionalStateActionRewardVector.get();
} }
template<typename ValueType> template<typename ValueType>
std::vector<ValueType>& StandardRewardModel<ValueType>::getStateActionRewardVector() { std::vector<ValueType>& StandardRewardModel<ValueType>::getStateActionRewardVector() {
assert(this->hasStateActionRewards()); STORM_LOG_ASSERT(this->hasStateActionRewards(), "No state action rewards available.");
return this->optionalStateActionRewardVector.get(); return this->optionalStateActionRewardVector.get();
} }
template<typename ValueType> template<typename ValueType>
ValueType const& StandardRewardModel<ValueType>::getStateActionReward(uint_fast64_t choiceIndex) const { ValueType const& StandardRewardModel<ValueType>::getStateActionReward(uint_fast64_t choiceIndex) const {
assert(this->hasStateActionRewards()); STORM_LOG_ASSERT(this->hasStateActionRewards(), "No state action rewards available.");
assert(choiceIndex < this->optionalStateActionRewardVector.get().size()); STORM_LOG_ASSERT(choiceIndex < this->optionalStateActionRewardVector.get().size(), "Invalid choiceIndex.");
return this->optionalStateActionRewardVector.get()[choiceIndex]; return this->optionalStateActionRewardVector.get()[choiceIndex];
} }
template<typename ValueType> template<typename ValueType>
template<typename T> template<typename T>
void StandardRewardModel<ValueType>::setStateActionReward(uint_fast64_t choiceIndex, T const &newValue) { void StandardRewardModel<ValueType>::setStateActionReward(uint_fast64_t choiceIndex, T const &newValue) {
assert(this->hasStateActionRewards()); STORM_LOG_ASSERT(this->hasStateActionRewards(), "No state action rewards available.");
assert(choiceIndex < this->optionalStateActionRewardVector.get().size()); STORM_LOG_ASSERT(choiceIndex < this->optionalStateActionRewardVector.get().size(), "Invalid choiceIndex.");
this->optionalStateActionRewardVector.get()[choiceIndex] = newValue; this->optionalStateActionRewardVector.get()[choiceIndex] = newValue;
} }

18
src/permissivesched/MILPPermissiveSchedulers.h
View File

@ -51,13 +51,13 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
bool foundSolution() const override { bool foundSolution() const override {
assert(mCalledOptimizer); STORM_LOG_ASSERT(mCalledOptimizer, "Optimizer not called.");
return !solver.isInfeasible(); return !solver.isInfeasible();
} }
SubMDPPermissiveScheduler<RM> getScheduler() const override { SubMDPPermissiveScheduler<RM> getScheduler() const override {
assert(mCalledOptimizer); STORM_LOG_ASSERT(mCalledOptimizer, "Optimizer not called.");
assert(foundSolution()); STORM_LOG_ASSERT(foundSolution(), "Solution not found.");
SubMDPPermissiveScheduler<RM> result(this->mdp, true); SubMDPPermissiveScheduler<RM> result(this->mdp, true);
@ -103,7 +103,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
*/ */
void createVariables(PermissiveSchedulerPenalties const& penalties, storm::storage::BitVector const& relevantStates) { void createVariables(PermissiveSchedulerPenalties const& penalties, storm::storage::BitVector const& relevantStates) {
// We need the unique initial state later, so we get that one before looping. // 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); uint_fast64_t initialStateIndex = this->mdp.getInitialStates().getNextSetIndex(0);
storm::expressions::Variable var; 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 -- ) // (5) and (7) are omitted on purpose (-- we currenty do not support controllability of actions -- )
// (1) // (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); uint_fast64_t initialStateIndex = this->mdp.getInitialStates().getNextSetIndex(0);
assert(relevantStates[initialStateIndex]); STORM_LOG_ASSERT(relevantStates[initialStateIndex], "Initial state not relevant.");
if(lowerBound) { if(lowerBound) {
solver.addConstraint("c1", mProbVariables[initialStateIndex] >= solver.getConstant(boundary)); solver.addConstraint("c1", mProbVariables[initialStateIndex] >= solver.getConstant(boundary));
} else { } else {
@ -206,9 +206,9 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
std::string satstring = to_string(sat); std::string satstring = to_string(sat);
// (8) // (8)
if(relevantStates[entry.getColumn()]) { if(relevantStates[entry.getColumn()]) {
assert(mGammaVariables.count(entry.getColumn()) > 0); STORM_LOG_ASSERT(mGammaVariables.count(entry.getColumn()) > 0, "Entry not found.");
assert(mGammaVariables.count(s) > 0); STORM_LOG_ASSERT(mGammaVariables.count(s) > 0, "Entry not found.");
assert(mBetaVariables.count(sat) > 0); STORM_LOG_ASSERT(mBetaVariables.count(sat) > 0, "Entry not found.");
solver.addConstraint("c8-" + satstring, mGammaVariables[entry.getColumn()] < mGammaVariables[s] + (solver.getConstant(1) - mBetaVariables[sat])); solver.addConstraint("c8-" + satstring, mGammaVariables[entry.getColumn()] < mGammaVariables[s] + (solver.getConstant(1) - mBetaVariables[sat]));
} }
} }

2
src/permissivesched/PermissiveSchedulerPenalty.h
View File

@ -30,7 +30,7 @@ namespace storm {
} }
void set(uint_fast64_t state, uint_fast64_t action, double penalty) { 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) { if(penalty == 1.0) {
auto it = mPenalties.find(std::make_pair(state, action)); auto it = mPenalties.find(std::make_pair(state, action));
if(it != mPenalties.end()) { if(it != mPenalties.end()) {

4
src/permissivesched/PermissiveSchedulers.cpp
View File

@ -17,7 +17,7 @@ namespace storm {
template<typename RM> template<typename RM>
boost::optional<SubMDPPermissiveScheduler<RM>> computePermissiveSchedulerViaMILP(storm::models::sparse::Mdp<double, RM> const& mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { 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); 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(); auto backwardTransitions = mdp.getBackwardTransitions();
storm::storage::BitVector goalstates = propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); 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); goalstates = storm::utility::graph::performProb1A(mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates);
@ -44,7 +44,7 @@ namespace storm {
template<typename RM> template<typename RM>
boost::optional<SubMDPPermissiveScheduler<RM>> computePermissiveSchedulerViaSMT(storm::models::sparse::Mdp<double, RM> const& mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { 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); 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(); auto backwardTransitions = mdp.getBackwardTransitions();
storm::storage::BitVector goalstates = propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); 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); goalstates = storm::utility::graph::performProb1A(mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates);

2
src/permissivesched/PermissiveSchedulers.h
View File

@ -32,7 +32,7 @@ namespace storm {
} }
void disable(uint_fast64_t choiceIndex) { void disable(uint_fast64_t choiceIndex) {
assert(choiceIndex < enabledChoices.size()); STORM_LOG_ASSERT(choiceIndex < enabledChoices.size(), "Invalid choiceIndex.");
enabledChoices.set(choiceIndex, false); enabledChoices.set(choiceIndex, false);
} }

14
src/permissivesched/SmtBasedPermissiveSchedulers.h
View File

@ -34,12 +34,12 @@ namespace storm {
} }
bool foundSolution() const override { bool foundSolution() const override {
assert(mPerformedSmtLoop); STORM_LOG_ASSERT(mPerformedSmtLoop, "SMT loop not performed.");
return mFoundSolution; return mFoundSolution;
} }
SubMDPPermissiveScheduler<RM> getScheduler() const override { SubMDPPermissiveScheduler<RM> getScheduler() const override {
assert(foundSolution()); STORM_LOG_ASSERT(foundSolution(), "Solution not found.");
SubMDPPermissiveScheduler<RM> result(this->mdp, true); SubMDPPermissiveScheduler<RM> result(this->mdp, true);
for(auto const& entry : multistrategyVariables) { for(auto const& entry : multistrategyVariables) {
if(!multistrategyVariablesToTakenMap.at(entry.second)) { 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 -- ) // (4) and (7) are omitted on purpose (-- we currenty do not support controllability of actions -- )
// (1) // (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); uint_fast64_t initialStateIndex = this->mdp.getInitialStates().getNextSetIndex(0);
assert(relevantStates[initialStateIndex]); STORM_LOG_ASSERT(relevantStates[initialStateIndex], "Initial state not relevant.");
if(lowerBound) { if(lowerBound) {
solver.add(mProbVariables[initialStateIndex] >= manager.rational(boundary)); solver.add(mProbVariables[initialStateIndex] >= manager.rational(boundary));
} else { } else {
@ -162,9 +162,9 @@ namespace storm {
// std::string satstring = to_string(sat); // std::string satstring = to_string(sat);
// // (8) // // (8)
// if(relevantStates[entry.getColumn()]) { // if(relevantStates[entry.getColumn()]) {
// assert(mGammaVariables.count(entry.getColumn()) > 0); // STORM_LOG_ASSERT(mGammaVariables.count(entry.getColumn()) > 0, "Entry not found.");
// assert(mGammaVariables.count(s) > 0); // STORM_LOG_ASSERT(mGammaVariables.count(s) > 0, "Entry not found.");
// assert(mBetaVariables.count(sat) > 0); // 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. // solver.addConstraint("c8-" + satstring, mGammaVariables[entry.getColumn()] < mGammaVariables[s] + (solver.getConstant(1) - mBetaVariables[sat]) + mProbVariables[s]); // With rewards, we have to change this.
// } // }
// } // }

2
src/solver/MinMaxLinearEquationSolver.h
View File

@ -102,7 +102,7 @@ namespace storm {
* Can only be called after the direction has been set. * 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 { 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); solveEquationSystem(convert(this->direction), x, b, multiplyResult, newX);
} }

4
src/solver/OptimizationDirection.cpp
View File

@ -1,6 +1,6 @@
#include "OptimizationDirection.h" #include "OptimizationDirection.h"
#include <iostream> #include <iostream>
#include <cassert> #include "src/utility/macros.h"
namespace storm { namespace storm {
namespace solver { namespace solver {
@ -18,7 +18,7 @@ namespace storm {
} }
OptimizationDirection convert(OptimizationDirectionSetting s) { OptimizationDirection convert(OptimizationDirectionSetting s) {
assert(isSet(s)); STORM_LOG_ASSERT(isSet(s), "Setting is not set.");
return static_cast<OptimizationDirection>(s); return static_cast<OptimizationDirection>(s);
} }

2
src/solver/stateelimination/StateEliminator.cpp
View File

@ -70,7 +70,7 @@ namespace storm {
// Skip the state itself as one of its predecessors. // Skip the state itself as one of its predecessors.
if (predecessor == state) { if (predecessor == state) {
assert(hasSelfLoop); STORM_LOG_ASSERT(hasSelfLoop, "State has no self loop.");
continue; continue;
} }

10
src/storage/FlexibleSparseMatrix.cpp
View File

@ -51,15 +51,15 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
typename FlexibleSparseMatrix<ValueType>::row_type& FlexibleSparseMatrix<ValueType>::getRow(index_type rowGroup, index_type offset) { typename FlexibleSparseMatrix<ValueType>::row_type& FlexibleSparseMatrix<ValueType>::getRow(index_type rowGroup, index_type offset) {
assert(rowGroup < this->getRowGroupCount()); STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Invalid rowGroup.");
assert(offset < this->getRowGroupSize(rowGroup)); STORM_LOG_ASSERT(offset < this->getRowGroupSize(rowGroup), "Invalid offset.");
return getRow(rowGroupIndices[rowGroup] + offset); return getRow(rowGroupIndices[rowGroup] + offset);
} }
template<typename ValueType> template<typename ValueType>
typename FlexibleSparseMatrix<ValueType>::row_type const& FlexibleSparseMatrix<ValueType>::getRow(index_type rowGroup, index_type offset) const { typename FlexibleSparseMatrix<ValueType>::row_type const& FlexibleSparseMatrix<ValueType>::getRow(index_type rowGroup, index_type offset) const {
assert(rowGroup < this->getRowGroupCount()); STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Invalid rowGroup.");
assert(offset < this->getRowGroupSize(rowGroup)); STORM_LOG_ASSERT(offset < this->getRowGroupSize(rowGroup), "Invalid offset.");
return getRow(rowGroupIndices[rowGroup] + offset); return getRow(rowGroupIndices[rowGroup] + offset);
} }
@ -112,7 +112,7 @@ namespace storm {
this->columnCount = 0; this->columnCount = 0;
for (auto const& row : this->data) { for (auto const& row : this->data) {
for (auto const& element : row) { 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->nonzeroEntryCount;
this->columnCount = std::max(element.getColumn() + 1, this->columnCount); this->columnCount = std::max(element.getColumn() + 1, this->columnCount);
} }

14
src/storage/SparseMatrix.cpp
View File

@ -277,9 +277,9 @@ namespace storm {
} }
maxColumn = std::max(maxColumn, elem.getColumn()); maxColumn = std::max(maxColumn, elem.getColumn());
} }
assert(changed || highestColumn == maxColumn); STORM_LOG_ASSERT(changed || highestColumn == maxColumn, "Incorrect maximal column.");
highestColumn = maxColumn; 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(); lastColumn = columnsAndValues[columnsAndValues.size() - 1].getColumn();
if (changed) { if (changed) {
@ -305,10 +305,10 @@ namespace storm {
return a.getColumn() < b.getColumn(); return a.getColumn() < b.getColumn();
}); });
// Assert no equal elements // 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) { [](MatrixEntry<index_type, value_type> const& a, MatrixEntry<index_type, value_type> const& b) {
return a.getColumn() <= b.getColumn(); return a.getColumn() <= b.getColumn();
})); }), "Columns not sorted.");
} }
} }
} else { } else {
@ -320,10 +320,10 @@ namespace storm {
return a.getColumn() < b.getColumn(); return a.getColumn() < b.getColumn();
}); });
// Assert no equal elements // 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) { [](MatrixEntry<index_type, value_type> const& a, MatrixEntry<index_type, value_type> const& b) {
return a.getColumn() <= b.getColumn(); return a.getColumn() <= b.getColumn();
})); }), "Columns not sorted.");
} }
} }
@ -1368,7 +1368,7 @@ namespace storm {
void SparseMatrix<ValueType>::printAsMatlabMatrix(std::ostream& out) const { void SparseMatrix<ValueType>::printAsMatlabMatrix(std::ostream& out) const {
// Iterate over all row groups. // Iterate over all row groups.
for (typename SparseMatrix<ValueType>::index_type group = 0; group < this->getRowGroupCount(); ++group) { 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) { 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]; typename SparseMatrix<ValueType>::index_type nextIndex = this->rowIndications[i];

1
src/storage/SparseMatrix.h
View File

@ -11,6 +11,7 @@
#include <boost/optional.hpp> #include <boost/optional.hpp>
#include "src/utility/OsDetection.h" #include "src/utility/OsDetection.h"
#include "src/utility/macros.h"
#include "src/adapters/CarlAdapter.h" #include "src/adapters/CarlAdapter.h"
// Forward declaration for adapter classes. // Forward declaration for adapter classes.

2
src/storage/bisimulation/BisimulationDecomposition.h
View File

@ -120,7 +120,7 @@ namespace storm {
} }
OptimizationDirection getOptimizationDirection() const { OptimizationDirection getOptimizationDirection() const {
assert(optimalityType); STORM_LOG_ASSERT(optimalityType, "Optimality type not set.");
return optimalityType.get(); return optimalityType.get();
} }
// A flag that indicates whether a measure driven initial partition is to be used. If this flag is set // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set

48
src/storage/dft/DFT.cpp
View File

@ -14,7 +14,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) { 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; size_t nrRepresentatives = 0;
for (auto& elem : mElements) { for (auto& elem : mElements) {
@ -100,9 +100,9 @@ namespace storm {
} else { } else {
// Generate information according to symmetries // Generate information according to symmetries
for (size_t symmetryIndex : symmetries.sortedSymmetries) { 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); 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 // Insert all elements of first subtree of each symmetry
size_t groupIndex = stateIndex; size_t groupIndex = stateIndex;
@ -117,14 +117,14 @@ namespace storm {
// Mirror symmetries // Mirror symmetries
size_t noSymmetricElements = symmetryGroup.front().size(); size_t noSymmetricElements = symmetryGroup.front().size();
assert(noSymmetricElements > 1); STORM_LOG_ASSERT(noSymmetricElements > 1, "No symmetry available.");
for (std::vector<size_t> symmetricElements : symmetryGroup) { 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]]) { if (visited[symmetricElements[1]]) {
// Elements already mirrored // Elements already mirrored
for (size_t index : symmetricElements) { for (size_t index : symmetricElements) {
assert(visited[index]); STORM_LOG_ASSERT(visited[index], "Element not mirrored.");
} }
continue; continue;
} }
@ -143,13 +143,13 @@ namespace storm {
generationInfo.addStateIndex(symmetricElement, index + offset * i); generationInfo.addStateIndex(symmetricElement, index + offset * i);
stateIndex += 2; stateIndex += 2;
assert((activationIndex > 0) == isRepresentative(symmetricElement)); STORM_LOG_ASSERT((activationIndex > 0) == isRepresentative(symmetricElement), "Bits for representative incorrect.");
if (activationIndex > 0) { if (activationIndex > 0) {
generationInfo.addSpareActivationIndex(symmetricElement, activationIndex + offset * i); generationInfo.addSpareActivationIndex(symmetricElement, activationIndex + offset * i);
++stateIndex; ++stateIndex;
} }
assert((usageIndex > 0) == mElements[symmetricElement]->isSpareGate()); STORM_LOG_ASSERT((usageIndex > 0) == mElements[symmetricElement]->isSpareGate(), "Bits for usage incorrect.");
if (usageIndex > 0) { if (usageIndex > 0) {
generationInfo.addSpareUsageIndex(symmetricElement, usageIndex + offset * i); generationInfo.addSpareUsageIndex(symmetricElement, usageIndex + offset * i);
stateIndex += generationInfo.usageInfoBits(); stateIndex += generationInfo.usageInfoBits();
@ -187,15 +187,15 @@ namespace storm {
generationInfo.generateSymmetries(symmetries); generationInfo.generateSymmetries(symmetries);
STORM_LOG_TRACE(generationInfo); STORM_LOG_TRACE(generationInfo);
assert(stateIndex == mStateVectorSize); STORM_LOG_ASSERT(stateIndex == mStateVectorSize, "Id incorrect.");
assert(visited.full()); STORM_LOG_ASSERT(visited.full(), "Not all elements considered.");
return generationInfo; return generationInfo;
} }
template<typename ValueType> template<typename ValueType>
size_t DFT<ValueType>::generateStateInfo(DFTStateGenerationInfo& generationInfo, size_t id, storm::storage::BitVector& visited, size_t stateIndex) const { 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); visited.set(id);
// Reserve bits for element // Reserve bits for element
@ -238,7 +238,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
std::vector<DFT<ValueType>> DFT<ValueType>::topModularisation() const { 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(); auto const& children = getGate(mTopLevelIndex)->children();
std::map<size_t, std::vector<size_t>> subdfts; std::map<size_t, std::vector<size_t>> subdfts;
for(auto const& child : children) { for(auto const& child : children) {
@ -250,7 +250,7 @@ namespace storm {
if (isGate(child->id())) { if (isGate(child->id())) {
isubdft = getGate(child->id())->independentSubDft(false); isubdft = getGate(child->id())->independentSubDft(false);
} else { } else {
assert(isBasicElement(child->id())); STORM_LOG_ASSERT(isBasicElement(child->id()), "Child is no BE.");
if(getBasicElement(child->id())->hasIngoingDependencies()) { if(getBasicElement(child->id())->hasIngoingDependencies()) {
STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation."); STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation.");
return {*this}; return {*this};
@ -309,16 +309,16 @@ namespace storm {
// Add rewritten elements // Add rewritten elements
for (std::vector<size_t> rewrites : rewriteIds) { for (std::vector<size_t> rewrites : rewriteIds) {
assert(rewrites.size() > 1); STORM_LOG_ASSERT(rewrites.size() > 1, "No rewritten elements.");
assert(mElements[rewrites[1]]->hasParents()); STORM_LOG_ASSERT(mElements[rewrites[1]]->hasParents(), "Rewritten elements has no parents.");
assert(mElements[rewrites[1]]->parents().front()->isGate()); 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()); DFTGatePointer originalParent = std::static_pointer_cast<DFTGate<ValueType>>(mElements[rewrites[1]]->parents().front());
std::string newParentName = builder.getUniqueName(originalParent->name()); std::string newParentName = builder.getUniqueName(originalParent->name());
// Accumulate children names // Accumulate children names
std::vector<std::string> childrenNames; std::vector<std::string> childrenNames;
for (size_t i = 1; i < rewrites.size(); ++i) { 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()); childrenNames.push_back(mElements[rewrites[i]]->name());
} }
@ -390,7 +390,7 @@ namespace storm {
stream << "}" << std::endl; stream << "}" << std::endl;
return stream.str(); return stream.str();
} }
assert(it != mTopModule.end()); STORM_LOG_ASSERT(it != mTopModule.end(), "Element not found.");
stream << mElements[(*it)]->name(); stream << mElements[(*it)]->name();
++it; ++it;
while(it != mTopModule.end()) { while(it != mTopModule.end()) {
@ -403,7 +403,7 @@ namespace storm {
stream << "[" << mElements[spareModule.first]->name() << "] = {"; stream << "[" << mElements[spareModule.first]->name() << "] = {";
if (!spareModule.second.empty()) { if (!spareModule.second.empty()) {
std::vector<size_t>::const_iterator it = spareModule.second.begin(); 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(); stream << mElements[(*it)]->name();
++it; ++it;
while(it != spareModule.second.end()) { while(it != spareModule.second.end()) {
@ -494,13 +494,13 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
size_t DFT<ValueType>::getChild(size_t spareId, size_t nrUsedChild) const { 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(); return getGate(spareId)->children()[nrUsedChild]->id();
} }
template<typename ValueType> template<typename ValueType>
size_t DFT<ValueType>::getNrChild(size_t spareId, size_t childId) const { 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(); DFTElementVector children = getGate(spareId)->children();
for (size_t nrChild = 0; nrChild < children.size(); ++nrChild) { for (size_t nrChild = 0; nrChild < children.size(); ++nrChild) {
if (children[nrChild]->id() == childId) { if (children[nrChild]->id() == childId) {
@ -551,8 +551,8 @@ namespace storm {
} }
} }
assert(isGate(index1)); STORM_LOG_ASSERT(isGate(index1), "Element is no gate.");
assert(isGate(index2)); STORM_LOG_ASSERT(isGate(index2), "Element is no gate.");
std::vector<size_t> isubdft1 = getGate(index1)->independentSubDft(false); std::vector<size_t> isubdft1 = getGate(index1)->independentSubDft(false);
std::vector<size_t> isubdft2 = getGate(index2)->independentSubDft(false); std::vector<size_t> isubdft2 = getGate(index2)->independentSubDft(false);
if(isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) { 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 childLeftId = spareLeft->children().at(i)->id();
size_t childRightId = spareRight->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) { if (childLeftId == childRightId) {
// Ignore shared child // Ignore shared child
continue; continue;

14
src/storage/dft/DFT.h
View File

@ -118,7 +118,7 @@ namespace storm {
if(representativeId == mTopLevelIndex) { if(representativeId == mTopLevelIndex) {
return mTopModule; return mTopModule;
} else { } else {
assert(mSpareModules.count(representativeId)>0); STORM_LOG_ASSERT(mSpareModules.count(representativeId) > 0, "Representative not found.");
return mSpareModules.find(representativeId)->second; return mSpareModules.find(representativeId)->second;
} }
} }
@ -145,7 +145,7 @@ namespace storm {
* @param index The id of the element * @param index The id of the element
*/ */
DFTElementCPointer getElement(size_t index) const { DFTElementCPointer getElement(size_t index) const {
assert(index < nrElements()); STORM_LOG_ASSERT(index < nrElements(), "Index invalid.");
return mElements[index]; return mElements[index];
} }
@ -166,7 +166,7 @@ namespace storm {
} }
std::shared_ptr<DFTBE<ValueType> const> getBasicElement(size_t index) const { 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]); 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 { 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]); return std::static_pointer_cast<DFTGate<ValueType> const>(mElements[index]);
} }
std::shared_ptr<DFTDependency<ValueType> const> getDependency(size_t index) const { 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]); return std::static_pointer_cast<DFTDependency<ValueType> const>(mElements[index]);
} }
std::shared_ptr<DFTRestriction<ValueType> const> getRestriction(size_t index) const { 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]); return std::static_pointer_cast<DFTRestriction<ValueType> const>(mElements[index]);
} }
@ -215,7 +215,7 @@ namespace storm {
} }
DFTElementCPointer getRepresentant(size_t id) const { DFTElementCPointer getRepresentant(size_t id) const {
assert(hasRepresentant(id)); STORM_LOG_ASSERT(hasRepresentant(id), "Element has no representant.");
return getElement(mRepresentants.find(id)->second); return getElement(mRepresentants.find(id)->second);
} }

18
src/storage/dft/DFTElementState.h
View File

@ -2,7 +2,7 @@
#ifndef DFTELEMENTSTATE_H #ifndef DFTELEMENTSTATE_H
#define DFTELEMENTSTATE_H #define DFTELEMENTSTATE_H
#include <cassert> #include "src/utility/macros.h"
namespace storm { namespace storm {
namespace storage { namespace storage {
@ -18,8 +18,10 @@ namespace storm {
return os << "Failsafe"; return os << "Failsafe";
case DFTElementState::DontCare: case DFTElementState::DontCare:
return os << "Don't Care"; return os << "Don't Care";
default:
STORM_LOG_ASSERT(false, "Element state not known.");
return os;
} }
assert(false);
} }
inline char toChar(DFTElementState st) { inline char toChar(DFTElementState st) {
@ -32,8 +34,10 @@ namespace storm {
return 'S'; return 'S';
case DFTElementState::DontCare: case DFTElementState::DontCare:
return '-'; return '-';
default:
STORM_LOG_ASSERT(false, "Element state not known.");
return ' ';
} }
assert(false);
} }
enum class DFTDependencyState {Passive = 0, Unsuccessful = 1, Successful = 2, DontCare = 3}; enum class DFTDependencyState {Passive = 0, Unsuccessful = 1, Successful = 2, DontCare = 3};
@ -48,8 +52,10 @@ namespace storm {
return os << "Unsuccessful"; return os << "Unsuccessful";
case DFTDependencyState::DontCare: case DFTDependencyState::DontCare:
return os << "Don't Care"; return os << "Don't Care";
default:
STORM_LOG_ASSERT(false, "Element state not known.");
return os;
} }
assert(false);
} }
inline char toChar(DFTDependencyState st) { inline char toChar(DFTDependencyState st) {
@ -62,8 +68,10 @@ namespace storm {
return 'U'; return 'U';
case DFTDependencyState::DontCare: case DFTDependencyState::DontCare:
return '-'; return '-';
default:
STORM_LOG_ASSERT(false, "Element state not known.");
return ' ';
} }
assert(false);
} }
} }

39
src/storage/dft/DFTIsomorphism.h
View File

@ -1,6 +1,5 @@
#pragma once #pragma once
#include <cassert>
#include <vector> #include <vector>
#include <unordered_map> #include <unordered_map>
#include <utility> #include <utility>
@ -197,7 +196,7 @@ namespace storage {
} else if(dft.isDependency(id)) { } else if(dft.isDependency(id)) {
colourize(dft.getDependency(id)); colourize(dft.getDependency(id));
} else { } else {
assert(dft.isRestriction(id)); STORM_LOG_ASSERT(dft.isRestriction(id), "Element is no restriction.");
colourize(dft.getRestriction(id)); colourize(dft.getRestriction(id));
} }
} }
@ -233,7 +232,7 @@ namespace storage {
res.pdepCandidates[depColour.at(index)] = std::vector<size_t>({index}); res.pdepCandidates[depColour.at(index)] = std::vector<size_t>({index});
} }
} else { } else {
assert(dft.isRestriction(index)); STORM_LOG_ASSERT(dft.isRestriction(index), "Element is no restriction.");
auto it = res.restrictionCandidates.find(restrictionColour.at(index)); auto it = res.restrictionCandidates.find(restrictionColour.at(index));
if(it != res.restrictionCandidates.end()) { if(it != res.restrictionCandidates.end()) {
it->second.push_back(index); it->second.push_back(index);
@ -342,14 +341,14 @@ namespace storage {
* Construct the initial bijection. * Construct the initial bijection.
*/ */
void constructInitialBijection() { 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. // We first construct the currentPermutations, which helps to determine the current state of the check.
initializePermutationsAndTreatTrivialGroups(bleft.beCandidates, bright.beCandidates, currentPermutations.beCandidates); initializePermutationsAndTreatTrivialGroups(bleft.beCandidates, bright.beCandidates, currentPermutations.beCandidates);
initializePermutationsAndTreatTrivialGroups(bleft.gateCandidates, bright.gateCandidates, currentPermutations.gateCandidates); initializePermutationsAndTreatTrivialGroups(bleft.gateCandidates, bright.gateCandidates, currentPermutations.gateCandidates);
initializePermutationsAndTreatTrivialGroups(bleft.pdepCandidates, bright.pdepCandidates, currentPermutations.pdepCandidates); initializePermutationsAndTreatTrivialGroups(bleft.pdepCandidates, bright.pdepCandidates, currentPermutations.pdepCandidates);
initializePermutationsAndTreatTrivialGroups(bleft.restrictionCandidates, bright.restrictionCandidates, currentPermutations.restrictionCandidates); initializePermutationsAndTreatTrivialGroups(bleft.restrictionCandidates, bright.restrictionCandidates, currentPermutations.restrictionCandidates);
STORM_LOG_TRACE(bijection.size() << " vs. " << bleft.size() << " vs. " << bright.size()); 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. * @return true if a next bijection exists.
*/ */
bool findNextBijection() { bool findNextBijection() {
assert(candidatesCompatible); STORM_LOG_ASSERT(candidatesCompatible, "Candidates are not compatible.");
bool foundNext = false; bool foundNext = false;
if(!currentPermutations.beCandidates.empty()) { if(!currentPermutations.beCandidates.empty()) {
auto it = currentPermutations.beCandidates.begin(); auto it = currentPermutations.beCandidates.begin();
@ -395,28 +394,28 @@ namespace storage {
if(foundNext) { if(foundNext) {
for(auto const& colour : bleft.beCandidates) { for(auto const& colour : bleft.beCandidates) {
if (colour.second.size() > 1) { 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); zipVectorsIntoMap(colour.second, currentPermutations.beCandidates.find(colour.first)->second, bijection);
} }
} }
for(auto const& colour : bleft.gateCandidates) { for(auto const& colour : bleft.gateCandidates) {
if (colour.second.size() > 1) { 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); zipVectorsIntoMap(colour.second, currentPermutations.gateCandidates.find(colour.first)->second, bijection);
} }
} }
for(auto const& colour : bleft.pdepCandidates) { for(auto const& colour : bleft.pdepCandidates) {
if (colour.second.size() > 1) { 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); zipVectorsIntoMap(colour.second, currentPermutations.pdepCandidates.find(colour.first)->second, bijection);
} }
} }
for(auto const& colour : bleft.restrictionCandidates) { for(auto const& colour : bleft.restrictionCandidates) {
if (colour.second.size() > 1) { 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); zipVectorsIntoMap(colour.second, currentPermutations.restrictionCandidates.find(colour.first)->second, bijection);
} }
} }
@ -430,13 +429,13 @@ namespace storage {
* *
*/ */
bool check() const { 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 // We can skip BEs, as they are identified by they're homomorphic if they are in the same class
for(auto const& indexpair : bijection) { for(auto const& indexpair : bijection) {
// Check type first. Colouring takes care of a lot, but not necesarily everything (e.g. voting thresholds) // 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)); equalType(*dft.getElement(indexpair.first), *dft.getElement(indexpair.second));
if(dft.isGate(indexpair.first)) { 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& lGate = dft.getGate(indexpair.first);
auto const& rGate = dft.getGate(indexpair.second); auto const& rGate = dft.getGate(indexpair.second);
if(lGate->isDynamicGate()) { if(lGate->isDynamicGate()) {
@ -483,7 +482,7 @@ namespace storage {
} else if(dft.isDependency(indexpair.first)) { } 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& lDep = dft.getDependency(indexpair.first);
auto const& rDep = dft.getDependency(indexpair.second); auto const& rDep = dft.getDependency(indexpair.second);
if(bijection.at(lDep->triggerEvent()->id()) != rDep->triggerEvent()->id()) { if(bijection.at(lDep->triggerEvent()->id()) != rDep->triggerEvent()->id()) {
@ -493,7 +492,7 @@ namespace storage {
return false; return false;
} }
} else if(dft.isRestriction(indexpair.first)) { } 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); auto const& lRestr = dft.getRestriction(indexpair.first);
std::vector<size_t> childrenLeftMapped; std::vector<size_t> childrenLeftMapped;
for(auto const& child : lRestr->children() ) { for(auto const& child : lRestr->children() ) {
@ -521,8 +520,8 @@ namespace storage {
} }
} }
else { else {
assert(dft.isBasicElement(indexpair.first)); STORM_LOG_ASSERT(dft.isBasicElement(indexpair.first), "Element is no BE.");
assert(dft.isBasicElement(indexpair.second)); STORM_LOG_ASSERT(dft.isBasicElement(indexpair.second), "Element is no BE.");
// No operations required. // No operations required.
} }
} }
@ -590,12 +589,12 @@ namespace storage {
for(auto const& colour : right) { for(auto const& colour : right) {
if(colour.second.size()>1) { if(colour.second.size()>1) {
auto it = permutations.insert(colour); 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()); std::sort(it.first->second.begin(), it.first->second.end());
zipVectorsIntoMap(left.at(colour.first), it.first->second, bijection); zipVectorsIntoMap(left.at(colour.first), it.first->second, bijection);
} else { } else {
assert(colour.second.size() == 1); STORM_LOG_ASSERT(colour.second.size() == 1, "No elements for colour.");
assert(bijection.count(left.at(colour.first).front()) == 0); STORM_LOG_ASSERT(bijection.count(left.at(colour.first).front()) == 0, "Element already contained.");
bijection[left.at(colour.first).front()] = colour.second.front(); 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 { 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 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(); auto it = b.cbegin();
for(size_t lIndex : a) { for(size_t lIndex : a) {
map[lIndex] = *it; map[lIndex] = *it;

36
src/storage/dft/DFTState.cpp
View File

@ -11,8 +11,8 @@ namespace storm {
// Initialize uses // Initialize uses
for(size_t id : mDft.getSpareIndices()) { for(size_t id : mDft.getSpareIndices()) {
std::shared_ptr<DFTGate<ValueType> const> elem = mDft.getGate(id); std::shared_ptr<DFTGate<ValueType> const> elem = mDft.getGate(id);
assert(elem->isSpareGate()); STORM_LOG_ASSERT(elem->isSpareGate(), "Element is no spare gate.");
assert(elem->nrChildren() > 0); STORM_LOG_ASSERT(elem->nrChildren() > 0, "Element has no child.");
this->setUses(id, elem->children()[0]->id()); this->setUses(id, elem->children()[0]->id());
} }
@ -47,7 +47,7 @@ namespace storm {
// Initialize failable dependencies // Initialize failable dependencies
for (size_t dependencyId : mDft.getDependencies()) { for (size_t dependencyId : mDft.getDependencies()) {
std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(dependencyId); 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) { if (hasFailed(dependency->triggerEvent()->id()) && getElementState(dependency->dependentEvent()->id()) == DFTElementState::Operational) {
mFailableDependencies.push_back(dependencyId); mFailableDependencies.push_back(dependencyId);
STORM_LOG_TRACE("New dependency failure: " << dependency->toString()); STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
@ -182,9 +182,9 @@ namespace storm {
} }
for (auto dependency : mDft.getElement(id)->outgoingDependencies()) { 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) { 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()); mFailableDependencies.push_back(dependency->id());
STORM_LOG_TRACE("New dependency failure: " << dependency->toString()); STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
} }
@ -194,11 +194,11 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void DFTState<ValueType>::updateDontCareDependencies(size_t id) { void DFTState<ValueType>::updateDontCareDependencies(size_t id) {
assert(mDft.isBasicElement(id)); STORM_LOG_ASSERT(mDft.isBasicElement(id), "Element is no BE.");
assert(hasFailed(id)); STORM_LOG_ASSERT(hasFailed(id), "Element has not failed.");
for (auto dependency : mDft.getBasicElement(id)->ingoingDependencies()) { 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()); setDependencyDontCare(dependency->id());
} }
} }
@ -209,7 +209,7 @@ namespace storm {
STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString()); STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString());
if (nrFailableDependencies() > 0) { if (nrFailableDependencies() > 0) {
// Consider failure due to dependency // 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::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); std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true);
mFailableDependencies.erase(mFailableDependencies.begin() + index); mFailableDependencies.erase(mFailableDependencies.begin() + index);
@ -218,9 +218,9 @@ namespace storm {
return res; return res;
} else { } else {
// Consider "normal" failure // 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); 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); mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index);
setFailed(res.first->id()); setFailed(res.first->id());
return res; return res;
@ -229,7 +229,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void DFTState<ValueType>::letDependencyBeUnsuccessful(size_t index) { 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)); std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(getDependencyId(index));
mFailableDependencies.erase(mFailableDependencies.begin() + index); mFailableDependencies.erase(mFailableDependencies.begin() + index);
setDependencyUnsuccessful(dependency->id()); setDependencyUnsuccessful(dependency->id());
@ -243,7 +243,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
bool DFTState<ValueType>::isActive(size_t id) const { 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)]; return mStatus[mStateGenerationInfo.getSpareActivationIndex(id)];
} }
@ -277,7 +277,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
uint_fast64_t DFTState<ValueType>::extractUses(size_t from) const { 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()); return mStatus.getAsInt(from, mStateGenerationInfo.usageInfoBits());
} }
@ -294,14 +294,14 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void DFTState<ValueType>::finalizeUses(size_t spareId) { 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()); mStatus.setFromInt(mStateGenerationInfo.getSpareUsageIndex(spareId), mStateGenerationInfo.usageInfoBits(), mDft.getMaxSpareChildCount());
} }
template<typename ValueType> template<typename ValueType>
bool DFTState<ValueType>::hasOperationalPostSeqElements(size_t id) const { bool DFTState<ValueType>::hasOperationalPostSeqElements(size_t id) const {
assert(!mDft.isDependency(id)); STORM_LOG_ASSERT(!mDft.isDependency(id), "Element is dependency.");
assert(!mDft.isRestriction(id)); STORM_LOG_ASSERT(!mDft.isRestriction(id), "Element is restriction.");
auto const& postIds = mStateGenerationInfo.seqRestrictionPostElements(id); auto const& postIds = mStateGenerationInfo.seqRestrictionPostElements(id);
for(size_t id : postIds) { for(size_t id : postIds) {
if(isOperational(id)) { 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) { bool DFTState<ValueType>::claimNew(size_t spareId, size_t currentlyUses, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children) {
auto it = children.begin(); auto it = children.begin();
while ((*it)->id() != currentlyUses) { while ((*it)->id() != currentlyUses) {
assert(it != children.end()); STORM_LOG_ASSERT(it != children.end(), "Currently used element not found.");
++it; ++it;
} }
++it; ++it;

3
src/storage/dft/DFTState.h
View File

@ -6,7 +6,6 @@
#include <sstream> #include <sstream>
#include <memory> #include <memory>
#include <cassert>
namespace storm { namespace storm {
namespace storage { namespace storage {
@ -156,7 +155,7 @@ namespace storm {
* @return Id of the dependency * @return Id of the dependency
*/ */
size_t getDependencyId(size_t index) const { size_t getDependencyId(size_t index) const {
assert(index < nrFailableDependencies()); STORM_LOG_ASSERT(index < nrFailableDependencies(), "Index invalid.");
return mFailableDependencies[index]; return mFailableDependencies[index];
} }

2
src/storage/dft/DFTStateSpaceGenerationQueues.h
View File

@ -55,7 +55,7 @@ namespace storm {
} }
DFTRestrictionPointer nextRestrictionCheck() { DFTRestrictionPointer nextRestrictionCheck() {
assert(!restrictionChecksDone()); STORM_LOG_ASSERT(!restrictionChecksDone(), "All restriction checks done already.");
DFTRestrictionPointer next = restrictionChecks.back(); DFTRestrictionPointer next = restrictionChecks.back();
restrictionChecks.pop_back(); restrictionChecks.pop_back();
return next; return next;

3
src/storage/expressions/Variable.cpp
View File

@ -1,6 +1,5 @@
#include "src/storage/expressions/Variable.h" #include "src/storage/expressions/Variable.h"
#include "src/storage/expressions/ExpressionManager.h" #include "src/storage/expressions/ExpressionManager.h"
#include <cassert>
namespace storm { namespace storm {
namespace expressions { namespace expressions {
@ -41,7 +40,7 @@ namespace storm {
} }
ExpressionManager const& Variable::getManager() const { ExpressionManager const& Variable::getManager() const {
assert(manager != nullptr); STORM_LOG_ASSERT(manager != nullptr, "Manager is null.");
return *manager; return *manager;
} }

1
src/storage/expressions/Variable.h
View File

@ -6,6 +6,7 @@
#include <functional> #include <functional>
#include "src/utility/OsDetection.h" #include "src/utility/OsDetection.h"
#include "src/utility/macros.h"
namespace storm { namespace storm {
namespace expressions { namespace expressions {

3
src/storage/prism/Assignment.cpp
View File

@ -1,5 +1,4 @@
#include "Assignment.h" #include "Assignment.h"
#include <cassert>
namespace storm { namespace storm {
namespace prism { namespace prism {
@ -25,7 +24,7 @@ namespace storm {
bool Assignment::isIdentity() const { bool Assignment::isIdentity() const {
if(this->expression.isVariable()) { 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())) { //if( variable == *(this->expression.getVariables().begin())) {
// std::cout << variable.getName() << " == " << (this->expression.getVariables().begin())->getName() << std::endl; // std::cout << variable.getName() << " == " << (this->expression.getVariables().begin())->getName() << std::endl;
//} //}

3
src/storage/prism/Command.cpp
View File

@ -1,5 +1,4 @@
#include "Command.h" #include "Command.h"
#include <cassert>
namespace storm { namespace storm {
namespace prism { namespace prism {
@ -32,7 +31,7 @@ namespace storm {
} }
storm::prism::Update const& Command::getUpdate(uint_fast64_t index) const { 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]; return this->updates[index];
} }

2
src/storage/prism/Program.cpp
View File

@ -1297,7 +1297,7 @@ namespace storm {
} }
uint_fast64_t Program::largestActionIndex() const { uint_fast64_t Program::largestActionIndex() const {
assert(numberOfActions() != 0); STORM_LOG_ASSERT(numberOfActions() != 0, "No actions available.");
return this->indexToActionMap.rbegin()->first; return this->indexToActionMap.rbegin()->first;
} }

34
src/storm-dyftee.cpp
View File

@ -5,6 +5,7 @@
#include "src/cli/cli.h" #include "src/cli/cli.h"
#include "src/exceptions/BaseException.h" #include "src/exceptions/BaseException.h"
#include "src/utility/macros.h" #include "src/utility/macros.h"
#include "src/builder/DftSmtBuilder.h"
#include <boost/lexical_cast.hpp> #include <boost/lexical_cast.hpp>
#include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GeneralSettings.h"
@ -44,6 +45,18 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false,
analyser.printResult(); 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. * 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."); 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 // Set min or max
bool minimal = true; bool minimal = true;
if (dftSettings.isComputeMaximalValue()) { if (dftSettings.isComputeMaximalValue()) {
@ -132,11 +161,6 @@ int main(const int argc, const char** argv) {
STORM_LOG_ASSERT(!pctlFormula.empty(), "Pctl formula empty."); 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. // From this point on we are ready to carry out the actual computations.
if (parametric) { if (parametric) {
analyzeDFT<storm::RationalFunction>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC() ); analyzeDFT<storm::RationalFunction>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC() );

Write Preview
|||||||
100:0
Loading…
Cancel
Save