From 4d20e099bf125c951fdaed17bbd0cf76937e851c Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 16 Oct 2014 04:41:08 +0200 Subject: [PATCH] Added stuff, you know? Former-commit-id: 4895a964b8bfa73c620f35d48da1fbae69017bee --- .../reachability/SparseSccModelChecker.cpp | 42 +++++++++++-------- .../reachability/SparseSccModelChecker.h | 2 +- ...icModelStrongBisimulationDecomposition.cpp | 2 +- .../expressions/ExpressionEvaluation.h | 2 +- src/stormParametric.cpp | 18 +++++++- src/utility/ConstantsComparator.cpp | 20 +++++++-- src/utility/ConstantsComparator.h | 10 ++++- 7 files changed, 68 insertions(+), 28 deletions(-) diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index a293335f5..3911f1a6f 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/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 comparator; auto modelCheckingStart = std::chrono::high_resolution_clock::now(); std::vector 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 - uint_fast64_t SparseSccModelChecker::treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, boost::optional> const& distances) { + uint_fast64_t SparseSccModelChecker::treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, storm::utility::ConstantsComparator const& comparator, boost::optional> 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 const& actualDistances = distances.get(); - std::sort(trivialSccs.begin(), trivialSccs.end(), [&actualDistances] (std::pair const& state1, std::pair const& state2) -> bool { return actualDistances[state1.first] > actualDistances[state2.first]; } ); +// std::sort(trivialSccs.begin(), trivialSccs.end(), [&actualDistances] (std::pair const& state1, std::pair const& state2) -> bool { return actualDistances[state1.first] > actualDistances[state2.first]; } ); + + std::sort(trivialSccs.begin(), trivialSccs.end(), [&oneStepProbabilities,&comparator] (std::pair const& state1, std::pair 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 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."); - std::vector 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]; } ); +// STORM_LOG_THROW(distances, storm::exceptions::IllegalFunctionCallException, "Cannot sort according to distances because none were provided."); +// std::vector 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(), [&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(); - auto tmp1 = multiplyFactor * oneStepProbabilities[state]; - multiplicationTime += std::chrono::high_resolution_clock::now() - multiplicationClock; - simplifyClock = std::chrono::high_resolution_clock::now(); - tmp1 = storm::utility::simplify(tmp1); - simplifyTime += std::chrono::high_resolution_clock::now() - simplifyClock; +// multiplicationClock = std::chrono::high_resolution_clock::now(); +// auto tmp1 = multiplyFactor * oneStepProbabilities[state]; +// multiplicationTime += std::chrono::high_resolution_clock::now() - multiplicationClock; +// simplifyClock = std::chrono::high_resolution_clock::now(); +// tmp1 = storm::utility::simplify(tmp1); +// 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."); } diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h index 6c530448e..039d30cc1 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.h +++ b/src/modelchecker/reachability/SparseSccModelChecker.h @@ -40,7 +40,7 @@ namespace storm { static ValueType computeReachabilityProbability(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional> const& distances = {}); private: - static uint_fast64_t treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, boost::optional> const& distances); + static uint_fast64_t treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, storm::utility::ConstantsComparator const& comparator, boost::optional> const& distances); static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne = false); static void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions); static bool eliminateStateInPlace(storm::storage::SparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix& backwardTransitions); diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp index adf78306c..aefa5f6a7 100644 --- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp @@ -648,7 +648,7 @@ namespace storm { } } } - + // Now check which of the blocks of the partition contain at least one initial state. for (auto initialState : model.getInitialStates()) { Block const& initialBlock = partition.getBlock(initialState); diff --git a/src/storage/expressions/ExpressionEvaluation.h b/src/storage/expressions/ExpressionEvaluation.h index 29b05ea31..71439792a 100644 --- a/src/storage/expressions/ExpressionEvaluation.h +++ b/src/storage/expressions/ExpressionEvaluation.h @@ -167,7 +167,7 @@ namespace storm { class ExpressionEvaluation { public: - ExpressionEvaluation() : mState(), cache(new carl::Cache>()) + ExpressionEvaluation() : mState(), cache(new carl::Cache>(100000)) { // Intentionally left empty. } diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 24fb2287a..967e39813 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -160,7 +160,7 @@ int main(const int argc, const char** argv) { dtmc->printModelInformationToStream(std::cout); } - + assert(dtmc); storm::modelchecker::reachability::CollectConstraints constraintCollector; constraintCollector(*dtmc); @@ -172,7 +172,21 @@ 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 bisimulationDecomposition(*dtmc, true); +// dtmc = bisimulationDecomposition.getQuotient()->as>(); +// +// 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 parameters; for(auto constant : program.getConstants()) diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp index d90766ee6..71d2bb165 100644 --- a/src/utility/ConstantsComparator.cpp +++ b/src/utility/ConstantsComparator.cpp @@ -26,7 +26,14 @@ namespace storm { // supposed to happen here, the templated function can be specialized for this particular type. return value; } - + + template + 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 bool ConstantsComparator::isOne(ValueType const& value) const { return value == one(); @@ -69,11 +76,15 @@ 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::isOne(storm::RationalFunction const& value) const { return value.isOne(); @@ -131,6 +142,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& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h index 431bb974f..6bc668445 100644 --- a/src/utility/ConstantsComparator.h +++ b/src/utility/ConstantsComparator.h @@ -29,7 +29,10 @@ namespace storm { template ValueType& simplify(ValueType& value); - + + template + ValueType&& simplify(ValueType&& value); + // A class that can be used for comparing constants. template class ConstantsComparator { @@ -65,7 +68,10 @@ namespace storm { #ifdef PARAMETRIC_SYSTEMS template<> RationalFunction& simplify(RationalFunction& value); - + + template<> + RationalFunction&& simplify(RationalFunction&& value); + template<> class ConstantsComparator { public: