diff --git a/resources/3rdparty/cudd-3.0.0/configure b/resources/3rdparty/cudd-3.0.0/configure index f0e0e742e..1494802d5 100755 --- a/resources/3rdparty/cudd-3.0.0/configure +++ b/resources/3rdparty/cudd-3.0.0/configure @@ -4419,6 +4419,7 @@ else fi + ac_ext=cpp ac_cpp='$CXXCPP $CPPFLAGS' ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5' diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index b4c01d13a..8fafb5093 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -195,12 +195,6 @@ namespace storm { return SparseDtmcPrctlHelper::computeUntilProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, phiStates, psiStates, qualitative, linearEquationSolverFactory); } - template - std::vector SparseCtmcCslHelper::computeUntilProbabilitiesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) { - // Use "normal" function again, if RationalFunction finally is supported. - return storm::modelchecker::SparseDtmcEliminationModelChecker>::computeUntilProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, initialStates, phiStates, psiStates, false); - } - template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return SparseDtmcPrctlHelper::computeNextProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), nextStates, linearEquationSolverFactory); @@ -675,37 +669,11 @@ namespace storm { return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory); } - - template - std::vector SparseCtmcCslHelper::computeReachabilityTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative) { - // Use "normal" function again, if RationalFunction finally is supported. - // Compute expected time on CTMC by reduction to DTMC with rewards. - storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); - - // Initialize rewards. - std::vector totalRewardVector; - for (size_t i = 0; i < exitRateVector.size(); ++i) { - if (targetStates[i] || storm::utility::isZero(exitRateVector[i])) { - // Set reward for target states or states without outgoing transitions to 0. - totalRewardVector.push_back(storm::utility::zero()); - } else { - // Reward is (1 / exitRate). - totalRewardVector.push_back(storm::utility::one() / exitRateVector[i]); - } - } - - return storm::modelchecker::SparseDtmcEliminationModelChecker>::computeReachabilityRewards(probabilityMatrix, backwardTransitions, initialStates, targetStates, totalRewardVector, false); - } - template class SparseCtmcCslHelper; template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); -#ifdef STORM_HAVE_CARL - template std::vector SparseCtmcCslHelper::computeUntilProbabilitiesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); - template std::vector SparseCtmcCslHelper::computeReachabilityTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative); -#endif } } } diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h index 2b4dd6043..69ca7faad 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -16,7 +16,6 @@ namespace storm { static std::vector computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::vector computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeUntilProbabilitiesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); template static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); @@ -30,7 +29,6 @@ namespace storm { static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::vector computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static std::vector computeReachabilityTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative); /*! * Computes the matrix representing the transitions of the uniformized CTMC. diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 5a6045f66..6fb3d79f1 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -98,7 +98,7 @@ namespace storm { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - + storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); if (psiStates.empty()) { @@ -157,7 +157,7 @@ namespace storm { // Do some sanity checks to establish some required properties. RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : ""); STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); - + storm::storage::BitVector const& initialStates = this->getModel().getInitialStates(); STORM_LOG_THROW(initialStates.getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states."); @@ -167,7 +167,7 @@ namespace storm { // Get the state-reward values from the reward model. std::vector stateRewardValues = rewardModel.getTotalRewardVector(this->getModel().getTransitionMatrix()); - + storm::storage::BitVector maybeStates(stateRewardValues.size()); uint_fast64_t index = 0; for (auto const& value : stateRewardValues) { @@ -183,7 +183,7 @@ namespace storm { maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, allStates, maybeStates); std::vector result(numberOfStates, storm::utility::zero()); - + // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; if (checkTask.isOnlyInitialStatesRelevantSet() && initialStates.isDisjointFrom(maybeStates)) { @@ -221,7 +221,7 @@ namespace storm { std::chrono::high_resolution_clock::time_point sccDecompositionStart = std::chrono::high_resolution_clock::now(); storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowCount(), true), false, true); auto sccDecompositionEnd = std::chrono::high_resolution_clock::now(); - + std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. @@ -232,7 +232,7 @@ namespace storm { auto conversionEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); - + storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); boost::optional> distanceBasedPriorities; if (eliminationOrderNeedsDistances(order)) { @@ -294,7 +294,7 @@ namespace storm { } stateValues[*representativeIt] = bsccValue; } - + FlexibleRowType& representativeForwardRow = flexibleMatrix.getRow(*representativeIt); representativeForwardRow.clear(); representativeForwardRow.shrink_to_fit(); @@ -307,10 +307,10 @@ namespace storm { } } representativeBackwardRow.erase(it); - + ++representativeIt; } - + // If there are states remaining that are not in BSCCs, we need to eliminate them now. storm::storage::BitVector remainingStates = maybeStates & ~regularStatesInBsccs; @@ -388,7 +388,7 @@ namespace storm { storm::storage::BitVector const& initialStates = this->getModel().getInitialStates(); std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); - + if (furtherComputationNeeded) { uint_fast64_t timeBound = pathFormula.getDiscreteTimeBound(); @@ -399,7 +399,7 @@ namespace storm { // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). statesWithProbabilityGreater0 &= reachableStates; } - + // We then build the submatrix that only has the transitions of the maybe states. storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, true); @@ -408,7 +408,7 @@ namespace storm { if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of initial states of the sub-model. storm::storage::BitVector subInitialStates = this->getModel().getInitialStates() % statesWithProbabilityGreater0; - + // Precompute the distances of the relevant states to the initial states. distancesFromInitialStates = storm::utility::graph::getDistances(submatrix, subInitialStates, statesWithProbabilityGreater0); @@ -471,23 +471,19 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - - std::vector result = computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), phiStates, psiStates, checkTask.isOnlyInitialStatesRelevantSet()); - - // Construct check result. - std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - return checkResult; + + return computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), phiStates, psiStates, checkTask.isOnlyInitialStatesRelevantSet()); } - + template - std::vector SparseDtmcEliminationModelChecker::computeUntilProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly) { - + std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly) { + // Then, compute the subset of states that has a probability of 0 or 1, respectively. std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); - + // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; if (computeForInitialStatesOnly && initialStates.isDisjointFrom(maybeStates)) { @@ -497,7 +493,7 @@ namespace storm { STORM_LOG_DEBUG("The probability for all states was found in a preprocessing step."); furtherComputationNeeded = false; } - + std::vector result(maybeStates.size()); if (furtherComputationNeeded) { // If we compute the results for the initial states only, we can cut off all maybe state that are not @@ -505,35 +501,39 @@ namespace storm { if (computeForInitialStatesOnly) { // Determine the set of states that is reachable from the initial state without jumping over a target state. storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(probabilityMatrix, initialStates, maybeStates, statesWithProbability1); - + // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). maybeStates &= reachableStates; } - + // Create a vector for the probabilities to go to a state with probability 1 in one step. std::vector oneStepProbabilities = probabilityMatrix.getConstrainedRowSumVector(maybeStates, statesWithProbability1); - + // Determine the set of initial states of the sub-model. storm::storage::BitVector newInitialStates = initialStates % maybeStates; - + // We then build the submatrix that only has the transitions of the maybe states. storm::storage::SparseMatrix submatrix = probabilityMatrix.getSubmatrix(false, maybeStates, maybeStates); storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); - + std::vector subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, computeForInitialStatesOnly, phiStates, psiStates, oneStepProbabilities); storm::utility::vector::setVectorValues(result, maybeStates, subresult); } - + // Construct full result. storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); - + if (computeForInitialStatesOnly) { // If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the // result to only communicate these results. - result = storm::utility::vector::filterVector(result, ~maybeStates | initialStates); + std::unique_ptr> checkResult = std::make_unique>(); + for (auto state : ~maybeStates | initialStates) { + (*checkResult)[state] = result[state]; + } + return std::move(checkResult); } - return result; + return std::make_unique>(result); } template @@ -547,21 +547,18 @@ namespace storm { // Do some sanity checks to establish some required properties. RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : ""); - + STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); - std::vector result = computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), targetStates, - [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { - return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates); - }, - checkTask.isOnlyInitialStatesRelevantSet()); - - // Construct check result. - std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - return checkResult; + return computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), targetStates, + [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { + return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates); + }, + checkTask.isOnlyInitialStatesRelevantSet()); + } - + template - std::vector SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector& stateRewardValues, bool computeForInitialStatesOnly) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector& stateRewardValues, bool computeForInitialStatesOnly) { return computeReachabilityRewards(probabilityMatrix, backwardTransitions, initialStates, targetStates, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { std::vector result(numberOfRows); @@ -570,10 +567,10 @@ namespace storm { }, computeForInitialStatesOnly); } - + template - std::vector SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly) { - + std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly) { + uint_fast64_t numberOfStates = probabilityMatrix.getRowCount(); // Compute the subset of states that has a reachability reward less than infinity. @@ -594,7 +591,7 @@ namespace storm { furtherComputationNeeded = false; } } - + std::vector result(maybeStates.size()); if (furtherComputationNeeded) { // If we compute the results for the initial states only, we can cut off all maybe state that are not @@ -609,14 +606,14 @@ namespace storm { // Determine the set of initial states of the sub-model. storm::storage::BitVector newInitialStates = initialStates % maybeStates; - + // We then build the submatrix that only has the transitions of the maybe states. storm::storage::SparseMatrix submatrix = probabilityMatrix.getSubmatrix(false, maybeStates, maybeStates); storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); // Project the state reward vector to all maybe-states. std::vector stateRewardValues = totalStateRewardVectorGetter(submatrix.getRowCount(), probabilityMatrix, maybeStates); - + std::vector subresult = computeReachabilityValues(submatrix, stateRewardValues, submatrixTransposed, newInitialStates, computeForInitialStatesOnly, trueStates, targetStates, probabilityMatrix.getConstrainedRowSumVector(maybeStates, targetStates)); storm::utility::vector::setVectorValues(result, maybeStates, subresult); } @@ -627,9 +624,13 @@ namespace storm { if (computeForInitialStatesOnly) { // If we computed the results for the initial (and inf) states only, we need to filter the result to // only communicate these results. - result = storm::utility::vector::filterVector(result, ~maybeStates | initialStates); + std::unique_ptr> checkResult = std::make_unique>(); + for (auto state : ~maybeStates | initialStates) { + (*checkResult)[state] = result[state]; + } + return std::move(checkResult); } - return result; + return std::make_unique>(result); } template @@ -711,15 +712,15 @@ namespace storm { storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); if (eliminationOrderNeedsDistances(order)) { distanceBasedPriorities = getDistanceBasedPriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities, - eliminationOrderNeedsForwardDistances(order), - eliminationOrderNeedsReversedDistances(order)); + eliminationOrderNeedsForwardDistances(order), + eliminationOrderNeedsReversedDistances(order)); } storm::storage::FlexibleSparseMatrix flexibleMatrix(submatrix); storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(submatrixTransposed, true); std::shared_ptr> statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate); - + STORM_LOG_INFO("Computing conditional probilities." << std::endl); uint_fast64_t numberOfStatesToEliminate = statePriorities->size(); STORM_LOG_INFO("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl); @@ -852,7 +853,7 @@ namespace storm { storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); std::vector sortedStates(states.begin(), states.end()); - + if (order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Random) { std::random_device randomDevice; std::mt19937 generator(randomDevice()); @@ -944,7 +945,7 @@ namespace storm { // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. storm::storage::FlexibleSparseMatrix flexibleMatrix(transitionMatrix); storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(backwardTransitions); - + storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); boost::optional> distanceBasedPriorities; if (eliminationOrderNeedsDistances(order)) { @@ -961,7 +962,7 @@ namespace storm { } else if (storm::settings::getModule().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) { maximalDepth = performHybridStateElimination(transitionMatrix, flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, computeResultsForInitialStatesOnly, values, distanceBasedPriorities); } - + STORM_LOG_ASSERT(flexibleMatrix.empty(), "Not all transitions were eliminated."); STORM_LOG_ASSERT(flexibleBackwardTransitions.empty(), "Not all transitions were eliminated."); @@ -1004,7 +1005,7 @@ namespace storm { STORM_LOG_TRACE("Eliminating " << statePriorities->size() << " trivial SCCs."); performPrioritizedStateElimination(statePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); STORM_LOG_TRACE("Eliminated all trivial SCCs."); - + // And then recursively treat the remaining sub-SCCs. STORM_LOG_TRACE("Eliminating " << remainingSccs.getNumberOfSetBits() << " remaining SCCs on level " << level << "."); for (auto sccIndex : remainingSccs) { @@ -1106,22 +1107,22 @@ namespace storm { for (auto const& predecessor : backwardTransitions.getRow(state)) { for (auto const& successor : transitionMatrix.getRow(state)) { penalty += estimateComplexity(predecessor.getValue()) * estimateComplexity(successor.getValue()); -// STORM_LOG_TRACE("1) penalty += " << (estimateComplexity(predecessor.getValue()) * estimateComplexity(successor.getValue())) << " because of " << predecessor.getValue() << " and " << successor.getValue() << "."); + // STORM_LOG_TRACE("1) penalty += " << (estimateComplexity(predecessor.getValue()) * estimateComplexity(successor.getValue())) << " because of " << predecessor.getValue() << " and " << successor.getValue() << "."); } if (predecessor.getColumn() == state) { hasParametricSelfLoop = !storm::utility::isConstant(predecessor.getValue()); } penalty += estimateComplexity(oneStepProbabilities[predecessor.getColumn()]) * estimateComplexity(predecessor.getValue()) * estimateComplexity(oneStepProbabilities[state]); -// STORM_LOG_TRACE("2) penalty += " << (estimateComplexity(oneStepProbabilities[predecessor.getColumn()]) * estimateComplexity(predecessor.getValue()) * estimateComplexity(oneStepProbabilities[state])) << " because of " << oneStepProbabilities[predecessor.getColumn()] << ", " << predecessor.getValue() << " and " << oneStepProbabilities[state] << "."); + // STORM_LOG_TRACE("2) penalty += " << (estimateComplexity(oneStepProbabilities[predecessor.getColumn()]) * estimateComplexity(predecessor.getValue()) * estimateComplexity(oneStepProbabilities[state])) << " because of " << oneStepProbabilities[predecessor.getColumn()] << ", " << predecessor.getValue() << " and " << oneStepProbabilities[state] << "."); } // If it is a self-loop that is parametric, we increase the penalty a lot. if (hasParametricSelfLoop) { penalty *= 10; -// STORM_LOG_TRACE("3) penalty *= 100, because of parametric self-loop."); + // STORM_LOG_TRACE("3) penalty *= 100, because of parametric self-loop."); } -// STORM_LOG_TRACE("New penalty of state " << state << " is " << penalty << "."); + // STORM_LOG_TRACE("New penalty of state " << state << " is " << penalty << "."); return penalty; } @@ -1238,8 +1239,8 @@ namespace storm { template class StatePriorityQueue; template class SparseDtmcEliminationModelChecker>; template uint_fast64_t estimateComplexity(double const& value); - - + + #ifdef STORM_HAVE_CARL template class StatePriorityQueue; template class SparseDtmcEliminationModelChecker>; diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 7359ac93f..ec61cb0ef 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -47,9 +47,9 @@ namespace storm { virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; // Static helper methods - static std::vector computeUntilProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly); + static std::unique_ptr computeUntilProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly); - static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector& stateRewardValues, bool computeForInitialStatesOnly); + static std::unique_ptr computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector& stateRewardValues, bool computeForInitialStatesOnly); private: @@ -91,7 +91,7 @@ namespace storm { static std::vector computeLongRunValues(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& maybeStates, bool computeResultsForInitialStatesOnly, std::vector& stateValues); - static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly); + static std::unique_ptr computeReachabilityRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly); static std::vector computeReachabilityValues(storm::storage::SparseMatrix const& transitionMatrix, std::vector& values, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& oneStepProbabilitiesToTarget); diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 0fa299321..5d4a891e5 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -60,7 +60,10 @@ namespace storm { if (this->isResultForAllStates()) { map_type newMap; + std::cout << filterTruthValues << std::endl; for (auto const& element : filterTruthValues) { + std::cout << element << std::endl; + std::cout << this->getValueVector().size() << std::endl; STORM_LOG_THROW(element < this->getValueVector().size(), storm::exceptions::InvalidAccessException, "Invalid index in results."); newMap.emplace(element, this->getValueVector()[element]); } diff --git a/src/utility/storm.h b/src/utility/storm.h index ce213cf08..5f47631e4 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -375,8 +375,8 @@ namespace storm { std::unique_ptr subResultPointer = propositionalModelchecker.check(eventuallyFormula.getSubformula()); storm::storage::BitVector const& targetStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityTimesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), targetStates, false); - result = std::unique_ptr(new storm::modelchecker::ExplicitQuantitativeCheckResult(std::move(numericResult))); +// std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityTimesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), targetStates, false); +// result = std::unique_ptr(new storm::modelchecker::ExplicitQuantitativeCheckResult(std::move(numericResult))); } else if (formula->isProbabilityOperatorFormula()) { // Compute reachability probability for pCTMCs @@ -406,8 +406,8 @@ namespace storm { psiStates = resultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); } - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeUntilProbabilitiesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), phiStates, psiStates, false); - result = std::unique_ptr(new storm::modelchecker::ExplicitQuantitativeCheckResult(std::move(numericResult))); +// std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeUntilProbabilitiesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), phiStates, psiStates, false); +// result = std::unique_ptr(new storm::modelchecker::ExplicitQuantitativeCheckResult(std::move(numericResult))); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support this property on CTMCs.");