made dfs as exploration order available

Former-commit-id: 46ea31af78

src/builder/ExplicitPrismModelBuilder.cpp

@@ -231,8 +231,8 @@ namespace storm {
             }
             
             // Now that the program is fixed, we we need to substitute all constants with their concrete value.
-            this->program = program.substituteConstants();
-            
+            this->program = this->program.substituteConstants();
+
             // Create the variable information for the transformed program.
             this->variableInformation = VariableInformation(this->program);
             
@@ -481,13 +481,7 @@ namespace storm {
                 this->internalStateInformation.initialStateIndices = std::move(newInitialStateIndices);
                 
                 // Fix (c).
-                std::unordered_map<StateType, StateType> valueRemapping;
-                for (StateType index = 0; index < remapping.size(); ++index) {
-                    if (remapping[index] != index) {
-                        valueRemapping.emplace(index, static_cast<StateType>(remapping[index]));
-                    }
-                }
-                this->internalStateInformation.stateStorage.remap(valueRemapping);
+                this->internalStateInformation.stateStorage.remap([&remapping] (StateType const& state) { return remapping[state]; } );
             }
             
             return choiceLabels;

src/parser/PrismParser.cpp

@@ -11,7 +11,7 @@ namespace storm {
     namespace parser {
         storm::prism::Program PrismParser::parse(std::string const& filename) {
             // Open file and initialize result.
-            std::ifstream inputFileStream(filename, std::ios::in);
+            std::ifstream inputFileStream(filename);
             STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
             
             storm::prism::Program result;
@@ -35,7 +35,7 @@ namespace storm {
             PositionIteratorType first(input.begin());
             PositionIteratorType iter = first;
             PositionIteratorType last(input.end());
-            assert(first != last);
+            STORM_LOG_ASSERT(first != last, "Illegal input to PRISM parser.");
             
             // Create empty result;
             storm::prism::Program result;

src/settings/ArgumentValidators.h

@@ -18,6 +18,7 @@
 #include "src/exceptions/IllegalArgumentValueException.h"
 #include "src/exceptions/IllegalFunctionCallException.h"
 
+#include <sys/stat.h>
 
 namespace storm {
 	namespace settings {
@@ -97,11 +98,16 @@ namespace storm {
              */
 			static std::function<bool (std::string const&)> existingReadableFileValidator() {
 				return [] (std::string const fileName) -> bool {
-					std::ifstream targetFile(fileName);
-					bool isFileGood = targetFile.good();
-
-                    STORM_LOG_THROW(isFileGood, storm::exceptions::IllegalArgumentValueException, "The file " << fileName << " does not exist or is not readable.");
-					return isFileGood;
+                    // First check existence as ifstream::good apparently als returns true for directories.
+                    struct stat info;
+                    stat(fileName.c_str(), &info);
+                    STORM_LOG_THROW(info.st_mode & S_IFREG, storm::exceptions::IllegalArgumentValueException, "Unable to read from non-existing file '" << fileName << "'.");
+                    
+                    // Now that we know it's a file, we can check its readability.
+                    std::ifstream istream(fileName);
+                    STORM_LOG_THROW(istream.good(), storm::exceptions::IllegalArgumentValueException, "Unable to read from file '" << fileName << "'.");
+                    
+                    return true;
 				};
 			}
 

src/storage/BitVectorHashMap.cpp

@@ -234,12 +234,9 @@ namespace storm {
         }
         
         template<class ValueType, class Hash1, class Hash2>
-        void BitVectorHashMap<ValueType, Hash1, Hash2>::remap(std::unordered_map<ValueType, ValueType> const& remapping) {
+        void BitVectorHashMap<ValueType, Hash1, Hash2>::remap(std::function<ValueType(ValueType const&)> const& remapping) {
             for (auto pos : occupied) {
-                auto it = remapping.find(values[pos]);
-                if (it != remapping.end()) {
-                    values[pos] = it->second;
-                }
+                values[pos] = remapping(values[pos]);
             }
         }
         

src/storage/BitVectorHashMap.h

@@ -3,7 +3,6 @@
 
 #include <cstdint>
 #include <functional>
-#include <unordered_map>
 
 #include "src/storage/BitVector.h"
 
@@ -129,7 +128,7 @@ namespace storm {
              *
              * @param remapping The remapping to apply.
              */
-            void remap(std::unordered_map<ValueType, ValueType> const& remapping);
+            void remap(std::function<ValueType(ValueType const&)> const& remapping);
             
         private:
             /*!

src/storage/SparseMatrix.cpp

@@ -218,68 +218,40 @@ namespace storm {
         
         template<typename ValueType>
         bool SparseMatrixBuilder<ValueType>::replaceColumns(std::vector<index_type> const& replacements, index_type offset) {
-            bool changed = false;
+            bool matrixChanged = false;
             
-            // Sort columns per row.
-            typename SparseMatrix<ValueType>::index_type endGroups;
-            typename SparseMatrix<ValueType>::index_type endRows;
-            for (index_type group = 0; group < rowGroupIndices.size(); ++group) {
-                endGroups = group < rowGroupIndices.size()-1 ? rowGroupIndices[group+1] : rowIndications.size();
-                for (index_type i = rowGroupIndices[group]; i < endGroups; ++i) {
-                    bool changedRow = false;
-                    endRows = i < rowIndications.size()-1 ? rowIndications[i+1] : columnsAndValues.size();
-                    
-                    for (auto it = columnsAndValues.begin() + rowIndications[i], ite = columnsAndValues.begin() + endRows; it != ite; ++it) {
-                        if (it->getColumn() >= offset) {
-                            it->setColumn(replacements[it->getColumn() - offset]);
-                            changedRow = true;
-                        }
-                        // Update highest column in a way that only works if the highest appearing index does not become
-                        // lower during performing the replacement.
-                        highestColumn = std::max(highestColumn, it->getColumn());
-                    }
-                    
-                    if (changedRow) {
-                        changed = true;
-                        
-                        // Sort the row.
-                        std::sort(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows,
-                                  [](MatrixEntry<index_type, value_type> const& a, MatrixEntry<index_type, value_type> const& b) {
-                                      return a.getColumn() < b.getColumn();
-                                  });
-                        // Assert no equal elements
-                        STORM_LOG_ASSERT(std::is_sorted(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows,
-                                                        [](MatrixEntry<index_type, value_type> const& a, MatrixEntry<index_type, value_type> const& b) {
-                                                            return a.getColumn() <= b.getColumn();
-                                                        }), "Must not have different elements with the same column in a row.");
+            // Walk through all rows.
+            for (index_type row = 0; row < rowIndications.size(); ++row) {
+                bool rowChanged = false;
+                index_type rowEnd = row < rowIndications.size()-1 ? rowIndications[row+1] : columnsAndValues.size();
+                
+                for (auto it = columnsAndValues.begin() + rowIndications[row], ite = columnsAndValues.begin() + rowEnd; it != ite; ++it) {
+                    if (it->getColumn() >= offset && it->getColumn() != replacements[it->getColumn() - offset]) {
+                        it->setColumn(replacements[it->getColumn() - offset]);
+                        rowChanged = true;
                     }
+                    // Update highest column in a way that only works if the highest appearing index does not become
+                    // lower during performing the replacement.
+                    highestColumn = std::max(highestColumn, it->getColumn());
                 }
-            }
-            
-            return changed;
-        }
-        
-        template<typename ValueType>
-        void SparseMatrixBuilder<ValueType>::fixColumns() {
-            // Sort columns per row.
-            typename SparseMatrix<ValueType>::index_type endGroups;
-            typename SparseMatrix<ValueType>::index_type endRows;
-            for (index_type group = 0; group < rowGroupIndices.size(); ++group) {
-                endGroups = group < rowGroupIndices.size()-1 ? rowGroupIndices[group+1] : rowIndications.size();
-                for (index_type i = rowGroupIndices[group]; i < endGroups; ++i) {
-                    endRows = i < rowIndications.size()-1 ? rowIndications[i+1] : columnsAndValues.size();
+                
+                if (rowChanged) {
+                    matrixChanged = true;
+                    
                     // Sort the row.
-                    std::sort(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows,
+                    std::sort(columnsAndValues.begin() + rowIndications[row], columnsAndValues.begin() + rowEnd,
                               [](MatrixEntry<index_type, value_type> const& a, MatrixEntry<index_type, value_type> const& b) {
                                   return a.getColumn() < b.getColumn();
                               });
                     // Assert no equal elements
-                    STORM_LOG_ASSERT(std::is_sorted(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows,
+                    STORM_LOG_ASSERT(std::is_sorted(columnsAndValues.begin() + rowIndications[row], columnsAndValues.begin() + rowEnd,
                                                     [](MatrixEntry<index_type, value_type> const& a, MatrixEntry<index_type, value_type> const& b) {
                                                         return a.getColumn() <= b.getColumn();
                                                     }), "Must not have different elements with the same column in a row.");
                 }
             }
+            
+            return matrixChanged;
         }
         
         template<typename ValueType>

src/storage/SparseMatrix.h

@@ -288,11 +288,6 @@ namespace storm {
             // Stores the currently active row group. This is used for correctly constructing the row grouping of the
             // matrix.
             index_type currentRowGroup;
-            
-            /*!
-             * Fixes the matrix by sorting the columns to gain increasing order again.
-             */
-            void fixColumns();
         };
         
         /*!