More refactoring

Former-commit-id: 26f95239bd

src/modelchecker/DFTAnalyser.h

@@ -38,7 +38,7 @@ public:
     
 private:
     ValueType checkHelper(storm::storage::DFT<ValueType> const& dft , std::shared_ptr<const storm::logic::Formula> 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<storm::storage::DFT<ValueType>> dfts = {dft};
         std::vector<ValueType> 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<storm::modelchecker::CheckResult> 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<ValueType>().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<size_t>(cK));
             do {
                 STORM_LOG_TRACE("Permutation="<<permutation);
@@ -141,31 +141,31 @@ private:
             if(symred) {
                 auto colouring = dft.colourDFT();
                 symmetries = dft.findSymmetries(colouring);
-                std::cout << "Found " << symmetries.groups.size() << " symmetries." << std::endl;
+                STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries.");
                 STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
             }
             std::chrono::high_resolution_clock::time_point buildingEnd = std::chrono::high_resolution_clock::now();
             buildingTime += buildingEnd - buildingStart;
             
             // Building Markov Automaton
-            std::cout << "Building Model..." << std::endl;
+            STORM_LOG_INFO("Building Model...");
             storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
             typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
             std::shared_ptr<storm::models::sparse::Model<ValueType>> 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<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
-                std::cout << "Bisimulation..." << std::endl;
+                STORM_LOG_INFO("Bisimulation...");
                 model =  storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), {formula}, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
                 //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);
         }

src/parser/DFTGalileoParser.cpp

@@ -130,7 +130,8 @@ namespace storm {
 
         template<typename ValueType>
         ValueType DFTGalileoParser<ValueType>::parseRationalExpression(std::string const& expr) {
-            assert(false);
+            STORM_LOG_ASSERT(false, "Specialized method should be called.");
+            return 0;
         }
 
         template<>

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

src/storm-dyftee.cpp

@@ -36,7 +36,7 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false,
     storm::parser::DFTGalileoParser<ValueType> parser;
     storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForExplicit(property);
-    assert(formulas.size() == 1);
+    STORM_LOG_ASSERT(formulas.size() == 1, "Wrong number of formulas.");
     
     DFTAnalyser<ValueType> 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

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<size_t>(0);
     return (1 << n) - 1;
 }
 
 inline size_t nextBitPermutation(size_t v) {
-    if(v==0) return static_cast<size_t>(0);
+    if (v==0) return static_cast<size_t>(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);  
 }
-        
-        

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_ */
+#endif /* STORM_UTILITY_MATH_H_ */

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<storm::modelchecker::CheckResult> resultPointer = propositionalModelchecker.check(eventuallyFormula.getSubformula());

src/utility/vector.h

@@ -70,7 +70,7 @@ namespace storm {
              * Constructs a vector [min, min+1, ...., max]
              */
             inline std::vector<uint_fast64_t> 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<uint_fast64_t> 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;
             }