Added stuff, you know?

Former-commit-id: 4895a964b8

src/modelchecker/reachability/SparseSccModelChecker.cpp

@@ -30,9 +30,10 @@ namespace storm {
                 auto conversionEnd = std::chrono::high_resolution_clock::now();
                 
                 // Then, we recursively treat all SCCs.
+                storm::utility::ConstantsComparator<ValueType> comparator;
                 auto modelCheckingStart = std::chrono::high_resolution_clock::now();
                 std::vector<storm::storage::sparse::state_type> entryStateQueue;
-                uint_fast64_t maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::parametricSettings().getMaximalSccSize(), entryStateQueue, distances);
+                uint_fast64_t maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::parametricSettings().getMaximalSccSize(), entryStateQueue, comparator, distances);
                 
                 // If the entry states were to be eliminated last, we need to do so now.
                 STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step.");
@@ -169,7 +170,7 @@ namespace storm {
             }
             
             template<typename ValueType>
-            uint_fast64_t SparseSccModelChecker<ValueType>::treatScc(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, boost::optional<std::vector<std::size_t>> const& distances) {
+            uint_fast64_t SparseSccModelChecker<ValueType>::treatScc(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<std::size_t>> const& distances) {
                 uint_fast64_t maximalDepth = level;
                 
                 // If the SCCs are large enough, we try to split them further.
@@ -198,7 +199,9 @@ namespace storm {
                     if (storm::settings::parametricSettings().isSortTrivialSccsSet()) {
                         STORM_LOG_THROW(distances, storm::exceptions::IllegalFunctionCallException, "Cannot sort according to distances because none were provided.");
                         std::vector<std::size_t> const& actualDistances = distances.get();
-                        std::sort(trivialSccs.begin(), trivialSccs.end(), [&actualDistances] (std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& state1, std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& state2) -> bool { return actualDistances[state1.first] > actualDistances[state2.first]; } );
+//                        std::sort(trivialSccs.begin(), trivialSccs.end(), [&actualDistances] (std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& state1, std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& state2) -> bool { return actualDistances[state1.first] > actualDistances[state2.first]; } );
+
+                        std::sort(trivialSccs.begin(), trivialSccs.end(), [&oneStepProbabilities,&comparator] (std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& state1, std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& state2) -> bool { return comparator.isZero(oneStepProbabilities[state1.first]) && !comparator.isZero(oneStepProbabilities[state2.first]); } );
                     }
                     for (auto const& stateIndexPair : trivialSccs) {
                         eliminateState(matrix, oneStepProbabilities, stateIndexPair.first, backwardTransitions);
@@ -225,7 +228,7 @@ namespace storm {
                         }
                         
                         // Recursively descend in SCC-hierarchy.
-                        uint_fast64_t depth = treatScc(matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::parametricSettings().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, distances);
+                        uint_fast64_t depth = treatScc(matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::parametricSettings().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, comparator, distances);
                         maximalDepth = std::max(maximalDepth, depth);
                     }
                     
@@ -236,9 +239,12 @@ namespace storm {
                     
                     std::vector<uint_fast64_t> statesToEliminate(remainingStates.begin(), remainingStates.end());
                     if (storm::settings::parametricSettings().isSortTrivialSccsSet()) {
-                        STORM_LOG_THROW(distances, storm::exceptions::IllegalFunctionCallException, "Cannot sort according to distances because none were provided.");
+//                        STORM_LOG_THROW(distances, storm::exceptions::IllegalFunctionCallException, "Cannot sort according to distances because none were provided.");
-                        std::vector<std::size_t> const& actualDistances = distances.get();
+//                        std::vector<std::size_t> const& actualDistances = distances.get();
-                        std::sort(statesToEliminate.begin(), statesToEliminate.end(), [&actualDistances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) -> bool { return actualDistances[state1] > actualDistances[state2]; } );
+//                        std::sort(statesToEliminate.begin(), statesToEliminate.end(), [&actualDistances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) -> bool { return actualDistances[state1] > actualDistances[state2]; } );
+
+                        std::sort(statesToEliminate.begin(), statesToEliminate.end(), [&oneStepProbabilities,&comparator] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) -> bool { return comparator.isZero(oneStepProbabilities[state1]) && !comparator.isZero(oneStepProbabilities[state2]); } );
+
                     }
                     
                     // Eliminate the remaining states that do not have a self-loop (in the current, i.e. modified)
@@ -434,19 +440,19 @@ namespace storm {
                     predecessorForwardTransitions = std::move(newSuccessors);
                     
                     // Add the probabilities to go to a target state in just one step.
-                    multiplicationClock = std::chrono::high_resolution_clock::now();
+//                    multiplicationClock = std::chrono::high_resolution_clock::now();
-                    auto tmp1 = multiplyFactor * oneStepProbabilities[state];
+//                    auto tmp1 = multiplyFactor * oneStepProbabilities[state];
-                    multiplicationTime += std::chrono::high_resolution_clock::now() - multiplicationClock;
+//                    multiplicationTime += std::chrono::high_resolution_clock::now() - multiplicationClock;
-                    simplifyClock = std::chrono::high_resolution_clock::now();
+//                    simplifyClock = std::chrono::high_resolution_clock::now();
-                    tmp1 = storm::utility::simplify(tmp1);
+//                    tmp1 = storm::utility::simplify(tmp1);
-                    simplifyTime += std::chrono::high_resolution_clock::now() - simplifyClock;
+//                    simplifyTime += std::chrono::high_resolution_clock::now() - simplifyClock;
+//                    auto tmp2 = oneStepProbabilities[predecessor] + tmp1;
+//                    simplifyClock = std::chrono::high_resolution_clock::now();
+//                    tmp2 = storm::utility::simplify(tmp2);
+//                    simplifyTime += std::chrono::high_resolution_clock::now() - simplifyClock;
                     additionClock2 = std::chrono::high_resolution_clock::now();
-                    auto tmp2 = oneStepProbabilities[predecessor] + tmp1;
+                    oneStepProbabilities[predecessor] += storm::utility::simplify(multiplyFactor * oneStepProbabilities[state]);
                     additionTime2 += std::chrono::high_resolution_clock::now() - additionClock2;
-                    simplifyClock = std::chrono::high_resolution_clock::now();
-                    tmp2 = storm::utility::simplify(tmp2);
-                    simplifyTime += std::chrono::high_resolution_clock::now() - simplifyClock;
-                    oneStepProbabilities[predecessor] = tmp2;
                     
                     STORM_LOG_DEBUG("Fixed new next-state probabilities of predecessor states.");
                 }

src/modelchecker/reachability/SparseSccModelChecker.h

@@ -40,7 +40,7 @@ namespace storm {
                 static ValueType computeReachabilityProbability(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<std::size_t>> const& distances = {});
 
             private:
-                static uint_fast64_t treatScc(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, boost::optional<std::vector<std::size_t>> const& distances);
+                static uint_fast64_t treatScc(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<std::size_t>> const& distances);
                 static FlexibleSparseMatrix<ValueType> getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne = false);
                 static void eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions);
                 static bool eliminateStateInPlace(storm::storage::SparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix<ValueType>& backwardTransitions);

src/storage/expressions/ExpressionEvaluation.h

@@ -167,7 +167,7 @@ namespace storm {
         class ExpressionEvaluation
         {
 		public:
-            ExpressionEvaluation() : mState(), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>())
+            ExpressionEvaluation() : mState(), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>(100000))
             {
                 // Intentionally left empty.
             }

src/stormParametric.cpp

@@ -173,6 +173,20 @@ int main(const int argc, const char** argv) {
         storm::RationalFunction valueFunction = modelchecker.computeReachabilityProbability(*dtmc, filterFormula);
         STORM_PRINT_AND_LOG(std::endl << "computed value " << valueFunction << std::endl);
     
+//    // Perform bisimulation minimization if requested.
+//    if (storm::settings::generalSettings().isBisimulationSet()) {
+//        storm::storage::DeterministicModelStrongBisimulationDecomposition<storm::RationalFunction> bisimulationDecomposition(*dtmc, true);
+//        dtmc = bisimulationDecomposition.getQuotient()->as<storm::models::Dtmc<storm::RationalFunction>>();
+//        
+//        dtmc->printModelInformationToStream(std::cout);
+//    }
+//
+//    storm::RationalFunction valueFunction2 = modelchecker.computeReachabilityProbability(*dtmc, filterFormula);
+//    STORM_PRINT_AND_LOG(std::endl << "computed value2 " << valueFunction2 << std::endl);
+//
+//    storm::RationalFunction diff = storm::utility::simplify(valueFunction - valueFunction2);
+//    STORM_PRINT_AND_LOG(std::endl << "difference: " << diff << std::endl);
+    
         // Get variables from parameter definitions in prism program.
         std::set<storm::Variable> parameters;
         for(auto constant : program.getConstants())

src/utility/ConstantsComparator.cpp

@@ -27,6 +27,13 @@ namespace storm {
             return value;
         }
 
+        template<typename ValueType>
+        ValueType&& simplify(ValueType&& value) {
+            // In the general case, we don't to anything here, but merely return the value. If something else is
+            // supposed to happen here, the templated function can be specialized for this particular type.
+            return std::move(value);
+        }
+
         template<typename ValueType>
         bool ConstantsComparator<ValueType>::isOne(ValueType const& value) const {
             return value == one<ValueType>();
@@ -69,12 +76,16 @@ namespace storm {
 #ifdef PARAMETRIC_SYSTEMS
         template<>
         RationalFunction& simplify(RationalFunction& value) {
-            STORM_LOG_DEBUG("Simplifying " << value);
             value.simplify();
-            STORM_LOG_DEBUG("done.");
             return value;
         }
 
+        template<>
+        RationalFunction&& simplify(RationalFunction&& value) {
+            value.simplify();
+            return std::move(value);
+        }
+        
         bool ConstantsComparator<storm::RationalFunction>::isOne(storm::RationalFunction const& value) const {
             return value.isOne();
         }
@@ -132,6 +143,9 @@ namespace storm {
         template double& simplify(double& value);
         template RationalFunction& simplify(RationalFunction& value);
 
+        template double&& simplify(double&& value);
+        template RationalFunction&& simplify(RationalFunction&& value);
+        
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);
     }

src/utility/ConstantsComparator.h

@@ -30,6 +30,9 @@ namespace storm {
         template<typename ValueType>
         ValueType& simplify(ValueType& value);
 
+        template<typename ValueType>
+        ValueType&& simplify(ValueType&& value);
+
         // A class that can be used for comparing constants.
         template<typename ValueType>
         class ConstantsComparator {
@@ -66,6 +69,9 @@ namespace storm {
         template<>
         RationalFunction& simplify(RationalFunction& value);
 
+        template<>
+        RationalFunction&& simplify(RationalFunction&& value);
+
         template<>
         class ConstantsComparator<storm::RationalFunction> {
         public: