From 5eaa46c7de42ab73ad748af80dfe196c452b3d5b Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 17 May 2016 18:05:03 +0200 Subject: [PATCH] More refactoring Former-commit-id: 26f95239bd77362eacb975bef05246cbc296e47b --- src/modelchecker/DFTAnalyser.h | 26 +++++------ src/parser/DFTGalileoParser.cpp | 3 +- src/storage/BitVector.cpp | 76 +++++++++++++++++++-------------- src/storm-dyftee.cpp | 8 ++-- src/utility/bitoperations.h | 8 ++-- src/utility/math.h | 4 +- src/utility/storm.h | 2 +- src/utility/vector.h | 4 +- 8 files changed, 71 insertions(+), 60 deletions(-) diff --git a/src/modelchecker/DFTAnalyser.h b/src/modelchecker/DFTAnalyser.h index 189338b70..24c1068ba 100644 --- a/src/modelchecker/DFTAnalyser.h +++ b/src/modelchecker/DFTAnalyser.h @@ -38,7 +38,7 @@ public: private: ValueType checkHelper(storm::storage::DFT const& dft , std::shared_ptr const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true) { - std::cout << "check helper called" << std::endl; + STORM_LOG_TRACE("Check helper called"); bool invResults = false; std::vector> dfts = {dft}; std::vector res; @@ -86,11 +86,11 @@ private: for (auto const& model : models) { // Model checking - std::cout << "Model checking..." << std::endl; + STORM_LOG_INFO("Model checking..."); std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); std::unique_ptr result(storm::verifySparseModel(model, formula)); - std::cout << "done." << std::endl; - assert(result); + STORM_LOG_INFO("Model checking done."); + STORM_LOG_ASSERT(result, "Result does not exist."); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); modelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingStart; res.push_back(result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second); @@ -98,7 +98,7 @@ private: } if(nrM <= 1) { // No modularisation done. - assert(res.size()==1); + STORM_LOG_ASSERT(res.size()==1, "Result size not 1."); return res[0]; } @@ -107,7 +107,7 @@ private: int limK = invResults ? -1 : nrM+1; int chK = invResults ? -1 : 1; for(int cK = nrK; cK != limK; cK += chK ) { - assert(cK >= 0); + STORM_LOG_ASSERT(cK >= 0, "ck negative."); size_t permutation = smallestIntWithNBitsSet(static_cast(cK)); do { STORM_LOG_TRACE("Permutation="< builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; // TODO initialize this with the formula std::shared_ptr> model = builder.buildModel(labeloptions); //model->printModelInformationToStream(std::cout); - std::cout << "No. states (Explored): " << model->getNumberOfStates() << std::endl; - std::cout << "No. transitions (Explored): " << model->getNumberOfTransitions() << std::endl; + STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); + STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); std::chrono::high_resolution_clock::time_point explorationEnd = std::chrono::high_resolution_clock::now(); explorationTime += explorationEnd -buildingEnd; // Bisimulation if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule().isBisimulationSet()) { - std::cout << "Bisimulation..." << std::endl; + STORM_LOG_INFO("Bisimulation..."); model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), {formula}, storm::storage::BisimulationType::Weak)->template as>(); //model->printModelInformationToStream(std::cout); } - std::cout << "No. states (Bisimulation): " << model->getNumberOfStates() << std::endl; - std::cout << "No. transitions (Bisimulation): " << model->getNumberOfTransitions() << std::endl; + STORM_LOG_INFO("No. states (Bisimulation): " << model->getNumberOfStates()); + STORM_LOG_INFO("No. transitions (Bisimulation): " << model->getNumberOfTransitions()); bisimulationTime += std::chrono::high_resolution_clock::now() - explorationEnd; models.push_back(model); } diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index 0a0aa5b32..2cdda4929 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -130,7 +130,8 @@ namespace storm { template ValueType DFTGalileoParser::parseRationalExpression(std::string const& expr) { - assert(false); + STORM_LOG_ASSERT(false, "Specialized method should be called."); + return 0; } template<> diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 28f6bdcff..fcbceca7b 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -454,7 +454,7 @@ namespace storm { uint_fast64_t BitVector::getTwoBitsAligned(uint_fast64_t bitIndex) const { // Check whether it is aligned. - assert(bitIndex % 64 != 63); + STORM_LOG_ASSERT(bitIndex % 64 != 63, "Bits not aligned."); uint64_t bucket = bitIndex >> 6; uint64_t bitIndexInBucket = bitIndex & mod64mask; @@ -662,7 +662,7 @@ namespace storm { } storm::storage::BitVector BitVector::getAsBitVector(uint_fast64_t start, uint_fast64_t length) const { - assert(start + length <= bitCount); + STORM_LOG_ASSERT(start + length <= bitCount, "Invalid range."); #ifdef ASSERT_BITVECTOR BitVector original(*this); #endif @@ -699,12 +699,12 @@ namespace storm { // Write last bits uint_fast64_t remainingBits = length - noBits; - assert(getBucket != buckets + bucketCount()); + STORM_LOG_ASSERT(getBucket != buckets + bucketCount(), "Bucket index incorrect."); // Get remaining bits getValue = (*getBucket >> (64-remainingBits)) << (64-remainingBits); - assert(remainingBits < 64); + STORM_LOG_ASSERT(remainingBits < 64, "Too many remaining bits."); // Write bucket - assert(insertBucket != result.buckets + result.bucketCount()); + STORM_LOG_ASSERT(insertBucket != result.buckets + result.bucketCount(), "Bucket index incorrect."); if (offset == 0) { *insertBucket = getValue; } else { @@ -714,7 +714,7 @@ namespace storm { // Write last bits in new value writeValue = (getValue << offset); ++insertBucket; - assert(insertBucket != result.buckets + result.bucketCount()); + STORM_LOG_ASSERT(insertBucket != result.buckets + result.bucketCount(), "Bucket index incorrect."); *insertBucket = writeValue; } } @@ -723,21 +723,27 @@ namespace storm { // Check correctness of getter for (uint_fast64_t i = 0; i < length; ++i) { if (result.get(i) != get(start + i)) { - std::cout << "Getting of bits not correct for index " << i << std::endl; - std::cout << "Getting from " << start << " with length " << length << std::endl; - printBits(std::cout); - result.printBits(std::cout); - assert(false); + STORM_LOG_ERROR("Getting of bits not correct for index " << i); + STORM_LOG_ERROR("Getting from " << start << " with length " << length); + stringstream stream; + printBits(stream); + stream << std::endl; + result.printBits(stream); + STORM_LOG_ERROR(stream); + STORM_LOG_ASSERT(false, "Getting of bits not correct."); } } for (uint_fast64_t i = 0; i < bitCount; ++i) { if (i < start || i >= start+length) { if (original.get(i) != get(i)) { - std::cout << "Getting did change bitvector at index " << i << std::endl; - std::cout << "Getting from " << start << " with length " << length << std::endl; - printBits(std::cout); - original.printBits(std::cout); - assert(false); + STORM_LOG_ERROR("Getting did change bitvector at index " << i); + STORM_LOG_ERROR("Getting from " << start << " with length " << length); + stringstream stream; + printBits(stream); + stream << std::endl; + original.printBits(stream); + STORM_LOG_ERROR(stream); + STORM_LOG_ASSERT(false, "Getting of bits not correct."); } } } @@ -750,7 +756,7 @@ namespace storm { #ifdef ASSERT_BITVECTOR BitVector original(*this); #endif - assert(start + other.bitCount <= bitCount); + STORM_LOG_ASSERT(start + other.bitCount <= bitCount, "Range invalid."); uint_fast64_t offset = start % 64; uint64_t* insertBucket = buckets + (start / 64); @@ -786,9 +792,9 @@ namespace storm { // Write last bits uint_fast64_t remainingBits = other.bitCount - noBits; - assert(remainingBits < 64); - assert(insertBucket != buckets + bucketCount()); - assert(getBucket != other.buckets + other.bucketCount()); + STORM_LOG_ASSERT(remainingBits < 64, "Too many remaining bits."); + STORM_LOG_ASSERT(insertBucket != buckets + bucketCount(), "Bucket index incorrect."); + STORM_LOG_ASSERT(getBucket != other.buckets + other.bucketCount(), "Bucket index incorrect."); // Get remaining bits of bucket getValue = *getBucket; if (offset > 0) { @@ -799,7 +805,7 @@ namespace storm { if (remainingBits > offset && offset > 0) { // Remaining bits do not come from one bucket -> consider next bucket ++getBucket; - assert(getBucket != other.buckets + other.bucketCount()); + STORM_LOG_ASSERT(getBucket != other.buckets + other.bucketCount(), "Bucket index incorrect."); getValue |= *getBucket >> offset; } // Write completely @@ -810,21 +816,27 @@ namespace storm { // Check correctness of setter for (uint_fast64_t i = 0; i < other.bitCount; ++i) { if (other.get(i) != get(start + i)) { - std::cout << "Setting of bits not correct for index " << i << std::endl; - std::cout << "Setting from " << start << " with length " << other.bitCount << std::endl; - printBits(std::cout); - other.printBits(std::cout); - assert(false); + STORM_LOG_ERROR("Setting of bits not correct for index " << i); + STORM_LOG_ERROR("Setting from " << start << " with length " << other.bitCount); + stringstream stream; + printBits(stream); + stream << std::endl; + other.printBits(stream); + STORM_LOG_ERROR(stream); + STORM_LOG_ASSERT(false, "Setting of bits not correct."); } } for (uint_fast64_t i = 0; i < bitCount; ++i) { if (i < start || i >= start+other.bitCount) { if (original.get(i) != get(i)) { - std::cout << "Setting did change bitvector at index " << i << std::endl; - std::cout << "Setting from " << start << " with length " << other.bitCount << std::endl; - printBits(std::cout); - original.printBits(std::cout); - assert(false); + STORM_LOG_ERROR("Setting did change bitvector at index " << i); + STORM_LOG_ERROR("Setting from " << start << " with length " << other.bitCount); + stringstream stream; + printBits(stream); + stream << std::endl; + original.printBits(stream); + STORM_LOG_ERROR(stream); + STORM_LOG_ASSERT(false, "Setting of bits not correct."); } } } @@ -928,7 +940,7 @@ namespace storm { // Print last bits if (index * 64 < bitCount) { - assert(index == bucketCount() - 1); + STORM_LOG_ASSERT(index == bucketCount() - 1, "Not last bucket."); std::bitset<64> tmp(buckets[index]); for (size_t i = 0; i + index * 64 < bitCount; ++i) { // Bits are counted from rightmost in bitset diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index ced13bf4d..3ffd665ad 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -36,7 +36,7 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false, storm::parser::DFTGalileoParser parser; storm::storage::DFT dft = parser.parseDFT(filename); std::vector> formulas = storm::parseFormulasForExplicit(property); - assert(formulas.size() == 1); + STORM_LOG_ASSERT(formulas.size() == 1, "Wrong number of formulas."); DFTAnalyser analyser; analyser.check(dft, formulas[0], symred, allowModularisation, enableDC); @@ -95,7 +95,7 @@ int main(const int argc, const char** argv) { // Set min or max bool minimal = true; if (dftSettings.isComputeMaximalValue()) { - assert(!dftSettings.isComputeMinimalValue()); + STORM_LOG_THROW(!dftSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time."); minimal = false; } @@ -126,11 +126,11 @@ int main(const int argc, const char** argv) { } if (!targetFormula.empty()) { - assert(pctlFormula.empty()); + STORM_LOG_ASSERT(pctlFormula.empty(), "Pctl formula not empty."); pctlFormula = operatorType + (minimal ? "min" : "max") + "=?[" + targetFormula + "]"; } - assert(!pctlFormula.empty()); + STORM_LOG_ASSERT(!pctlFormula.empty(), "Pctl formula empty."); bool parametric = false; #ifdef STORM_HAVE_CARL diff --git a/src/utility/bitoperations.h b/src/utility/bitoperations.h index 55456dd61..bec6a6414 100644 --- a/src/utility/bitoperations.h +++ b/src/utility/bitoperations.h @@ -1,17 +1,15 @@ #pragma once inline size_t smallestIntWithNBitsSet(size_t n) { - assert(sizeof(size_t) == 8); - assert(n < 64); // TODO fix this for 32 bit architectures! + static_assert(sizeof(size_t) == 8, "size_t has wrong size."); + STORM_LOG_ASSERT(n < 64, "Input is too large."); // TODO fix this for 32 bit architectures! if(n==0) return static_cast(0); return (1 << n) - 1; } inline size_t nextBitPermutation(size_t v) { - if(v==0) return static_cast(0); + if (v==0) return static_cast(0); // From https://graphics.stanford.edu/~seander/bithacks.html#NextBitPermutation unsigned int t = (v | (v - 1)) + 1; return t | ((((t & -t) / (v & -v)) >> 1) - 1); } - - \ No newline at end of file diff --git a/src/utility/math.h b/src/utility/math.h index b2c41adc2..dd2fe9052 100644 --- a/src/utility/math.h +++ b/src/utility/math.h @@ -20,7 +20,7 @@ namespace storm { inline uint64_t uint64_log2(uint64_t n) { - assert(n != 0); + STORM_LOG_ASSERT(n != 0, "N is 0."); #define S(k) if (n >= (UINT64_C(1) << k)) { i += k; n >>= k; } uint64_t i = 0; S(32); S(16); S(8); S(4); S(2); S(1); return i; #undef S @@ -29,4 +29,4 @@ namespace storm { } } -#endif /* STORM_UTILITY_MATH_H_ */ \ No newline at end of file +#endif /* STORM_UTILITY_MATH_H_ */ diff --git a/src/utility/storm.h b/src/utility/storm.h index e3c4798f4..7fa292427 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -399,7 +399,7 @@ namespace storm { psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); } else { // Eventually formula - assert(probOpFormula.getSubformula().isEventuallyFormula()); + STORM_LOG_THROW(!probOpFormula.getSubformula().isEventuallyFormula(), storm::exceptions::NotSupportedException, "The parametric engine only supports eventually formulas on CTMCs"); storm::logic::EventuallyFormula eventuallyFormula = probOpFormula.getSubformula().asEventuallyFormula(); STORM_LOG_THROW(eventuallyFormula.getSubformula().isInFragment(storm::logic::propositional()), storm::exceptions::NotSupportedException, "The parametric engine does not support nested formulas on CTMCs"); std::unique_ptr resultPointer = propositionalModelchecker.check(eventuallyFormula.getSubformula()); diff --git a/src/utility/vector.h b/src/utility/vector.h index 211340106..0a4da1e03 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -70,7 +70,7 @@ namespace storm { * Constructs a vector [min, min+1, ...., max] */ inline std::vector buildVectorForRange(uint_fast64_t min, uint_fast64_t max) { - assert(min < max); + STORM_LOG_ASSERT(min < max, "Invalid range."); uint_fast64_t diff = max - min; std::vector v; v.reserve(diff); @@ -700,7 +700,7 @@ namespace storm { for(auto index : filter) { result.push_back(in[index]); } - assert(result.size() == filter.getNumberOfSetBits()); + STORM_LOG_ASSERT(result.size() == filter.getNumberOfSetBits(), "Result does not match."); return result; }