From 60510d07f720f7ac24d32c8c896af362d0151082 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 15 Oct 2014 22:32:30 +0200 Subject: [PATCH] Fixed one parametric model. Added debug output. Former-commit-id: 38a219ce0c6f8ba1c9a53a6d54838635bfb9a87a --- examples/pdtmc/crowds/crowds_10-5.pm | 2 +- .../reachability/SparseSccModelChecker.cpp | 23 +++++++++++++------ src/utility/ConstantsComparator.cpp | 2 ++ 3 files changed, 19 insertions(+), 8 deletions(-) diff --git a/examples/pdtmc/crowds/crowds_10-5.pm b/examples/pdtmc/crowds/crowds_10-5.pm index dcf6e7930..ab5dbd438 100644 --- a/examples/pdtmc/crowds/crowds_10-5.pm +++ b/examples/pdtmc/crowds/crowds_10-5.pm @@ -10,7 +10,7 @@ dtmc // Model parameters const double PF; // forwarding probability -const double badC = 0.167; // probability that member is untrustworthy +const double badC; // probability that member is untrustworthy // Probability of forwarding // const double PF = 0.8; diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index 1284af269..a293335f5 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -234,21 +234,28 @@ namespace storm { STORM_LOG_DEBUG("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly."); storm::storage::BitVector remainingStates = scc & ~entryStates; + 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]; } ); + } + // Eliminate the remaining states that do not have a self-loop (in the current, i.e. modified) // transition probability matrix. - for (auto const& state : remainingStates) { - if (!hasSelfLoop(state, matrix)) { + for (auto const& state : statesToEliminate) { +// if (!hasSelfLoop(state, matrix)) { eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); - remainingStates.set(state, false); - } +// remainingStates.set(state, false); +// } } STORM_LOG_DEBUG("Eliminated all states without self-loop."); // Eliminate the remaining states. - for (auto const& state : remainingStates) { - eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); - } +// for (auto const& state : statesToEliminate) { +// eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); +// } STORM_LOG_DEBUG("Eliminated all states with self-loop."); } @@ -495,6 +502,8 @@ namespace storm { // Clear the eliminated row to reduce memory consumption. currentStateSuccessors.clear(); currentStateSuccessors.shrink_to_fit(); + currentStatePredecessors.clear(); + currentStatePredecessors.shrink_to_fit(); auto eliminationEnd = std::chrono::high_resolution_clock::now(); auto eliminationTime = eliminationEnd - eliminationStart; diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp index 24b86231e..d90766ee6 100644 --- a/src/utility/ConstantsComparator.cpp +++ b/src/utility/ConstantsComparator.cpp @@ -69,7 +69,9 @@ namespace storm { #ifdef PARAMETRIC_SYSTEMS template<> RationalFunction& simplify(RationalFunction& value) { + STORM_LOG_DEBUG("Simplifying " << value); value.simplify(); + STORM_LOG_DEBUG("done."); return value; }