diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index fa7fb98b0..742038c50 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -34,9 +34,8 @@ namespace storm { STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute time-bounded reachability probabilities in non-closed Markov automaton."); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - return storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds()); - std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeBoundedUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds()))); - return result; + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds(), *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template @@ -46,34 +45,38 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative))); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - STORM_LOG_THROW(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute reachability rewards in non-closed Markov automaton."); + STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute reachability rewards in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative))); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - STORM_LOG_THROW(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute long-run average in non-closed Markov automaton."); + STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute long-run average in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeLongRunAverageHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative))); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverage(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - STORM_LOG_THROW(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute expected times in non-closed Markov automaton."); + STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute expected times in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeExpectedTimesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative))); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeExpectedTimes(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template class SparseMarkovAutomatonCslModelChecker>; diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 0ae832563..d24d3c9ae 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -20,13 +20,13 @@ namespace storm { namespace modelchecker { - template - SparseDtmcEliminationModelChecker::SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model) : model(model) { + template + SparseDtmcEliminationModelChecker::SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model) : SparsePropositionalModelChecker(model) { // Intentionally left empty. } - template - bool SparseDtmcEliminationModelChecker::canHandle(storm::logic::Formula const& formula) const { + template + bool SparseDtmcEliminationModelChecker::canHandle(storm::logic::Formula const& formula) const { if (formula.isProbabilityOperatorFormula()) { storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); return this->canHandle(probabilityOperatorFormula.getSubformula()); @@ -61,8 +61,8 @@ namespace storm { return false; } - template - std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + template + std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -70,35 +70,35 @@ namespace storm { storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); // Do some sanity checks to establish some required properties. - STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - storm::storage::sparse::state_type initialState = *model.getInitialStates().begin(); + STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); + storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); // Then, compute the subset of states that has a probability of 0 or 1, respectively. - std::pair statesWithProbability01 = storm::utility::graph::performProb01(model, phiStates, psiStates); + std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), phiStates, psiStates); storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); // If the initial state is known to have either probability 0 or 1, we can directly return the result. - if (model.getInitialStates().isDisjointFrom(maybeStates)) { + if (this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { STORM_LOG_DEBUG("The probability of all initial states was found in a preprocessing step."); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, statesWithProbability0.get(*model.getInitialStates().begin()) ? storm::utility::zero() : storm::utility::one())); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, statesWithProbability0.get(*this->getModel().getInitialStates().begin()) ? storm::utility::zero() : storm::utility::one())); } // 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(model.getTransitionMatrix(), model.getInitialStates(), maybeStates, statesWithProbability1); + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), 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 = model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); + std::vector oneStepProbabilities = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); // Determine the set of initial states of the sub-model. - storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates; + storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; // We then build the submatrix that only has the transitions of the maybe states. - storm::storage::SparseMatrix submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); // Before starting the model checking process, we assign priorities to states so we can use them to @@ -109,21 +109,22 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, missingStateRewards, statePriorities))); } - template - std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + template + std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); - storm::storage::BitVector phiStates(model.getNumberOfStates(), true); + storm::storage::BitVector phiStates(this->getModel().getNumberOfStates(), true); storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); // Do some sanity checks to establish some required properties. - STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); - STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - storm::storage::sparse::state_type initialState = *model.getInitialStates().begin(); + RewardModelType const& rewardModel = this->getModel().getRewardModel(rewardModelName ? rewardModelName.get() : ""); + STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); + STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); + storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); // Then, compute the subset of states that has a reachability reward less than infinity. - storm::storage::BitVector trueStates(model.getNumberOfStates(), true); - storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(model.getBackwardTransitions(), trueStates, psiStates); + storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); + storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel().getBackwardTransitions(), trueStates, psiStates); infinityStates.complement(); storm::storage::BitVector maybeStates = ~psiStates & ~infinityStates; @@ -140,19 +141,19 @@ namespace storm { } // 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(model.getTransitionMatrix(), model.getInitialStates(), maybeStates, psiStates); + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, psiStates); // 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 = model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates); + std::vector oneStepProbabilities = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates); // Determine the set of initial states of the sub-model. - storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates; + storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; // We then build the submatrix that only has the transitions of the maybe states. - storm::storage::SparseMatrix submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); // Before starting the model checking process, we assign priorities to states so we can use them to @@ -160,37 +161,12 @@ namespace storm { std::vector statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities); // Project the state reward vector to all maybe-states. - boost::optional> optionalStateRewards(maybeStates.getNumberOfSetBits()); - std::vector& stateRewards = optionalStateRewards.get(); - if (model.hasTransitionRewards()) { - // If a transition-based reward model is available, we initialize the right-hand - // side to the vector resulting from summing the rows of the pointwise product - // of the transition probability matrix and the transition reward matrix. - std::vector pointwiseProductRowSumVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix()); - storm::utility::vector::selectVectorValues(stateRewards, maybeStates, pointwiseProductRowSumVector); - - if (model.hasStateRewards()) { - // If a state-based reward model is also available, we need to add this vector - // as well. As the state reward vector contains entries not just for the states - // that we still consider (i.e. maybeStates), we need to extract these values - // first. - std::vector subStateRewards(stateRewards.size()); - storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, model.getStateRewardVector()); - storm::utility::vector::addVectors(stateRewards, subStateRewards, stateRewards); - } - } else { - // If only a state-based reward model is available, we take this vector as the - // right-hand side. As the state reward vector contains entries not just for the - // states that we still consider (i.e. maybeStates), we need to extract these values - // first. - storm::utility::vector::selectVectorValues(stateRewards, maybeStates, model.getStateRewardVector()); - } - + boost::optional> optionalStateRewards = rewardModel.getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->getModel().getTransitionMatrix(), maybeStates); return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, optionalStateRewards, statePriorities))); } - template - std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + template + std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); // Retrieve the appropriate bitvectors by model checking the subformulas. @@ -201,26 +177,26 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula().asEventuallyFormula().getSubformula()); storm::storage::BitVector phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - storm::storage::BitVector trueStates(model.getNumberOfStates(), true); + storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); // Do some sanity checks to establish some required properties. // STORM_LOG_WARN_COND(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, "The chosen elimination method is not available for computing conditional probabilities. Falling back to regular state elimination."); - STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - storm::storage::sparse::state_type initialState = *model.getInitialStates().begin(); + STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); + storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + storm::storage::SparseMatrix backwardTransitions = this->getModel().getBackwardTransitions(); // Compute the 'true' psi states, i.e. those psi states that can be reached without passing through another psi state first. - psiStates = storm::utility::graph::getReachableStates(model.getTransitionMatrix(), model.getInitialStates(), trueStates, psiStates) & psiStates; + psiStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), trueStates, psiStates) & psiStates; std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, trueStates, psiStates); storm::storage::BitVector statesWithProbabilityGreater0 = ~statesWithProbability01.first; storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); - STORM_LOG_THROW(model.getInitialStates().isSubsetOf(statesWithProbabilityGreater0), storm::exceptions::InvalidPropertyException, "The condition of the conditional probability has zero probability."); + STORM_LOG_THROW(this->getModel().getInitialStates().isSubsetOf(statesWithProbabilityGreater0), storm::exceptions::InvalidPropertyException, "The condition of the conditional probability has zero probability."); // If the initial state is known to have probability 1 of satisfying the condition, we can apply regular model checking. - if (model.getInitialStates().isSubsetOf(statesWithProbability1)) { + if (this->getModel().getInitialStates().isSubsetOf(statesWithProbability1)) { STORM_LOG_INFO("The condition holds with probability 1, so the regular reachability probability is computed."); std::shared_ptr trueFormula = std::make_shared(true); std::shared_ptr untilFormula = std::make_shared(trueFormula, pathFormula.getLeftSubformula().asSharedPointer()); @@ -230,11 +206,11 @@ namespace storm { // From now on, we know the condition does not have a trivial probability in the initial state. // Compute the states that can be reached on a path that has a psi state in it. - storm::storage::BitVector statesWithPsiPredecessor = storm::utility::graph::performProbGreater0(model.getTransitionMatrix(), trueStates, psiStates); + storm::storage::BitVector statesWithPsiPredecessor = storm::utility::graph::performProbGreater0(this->getModel().getTransitionMatrix(), trueStates, psiStates); storm::storage::BitVector statesReachingPhi = storm::utility::graph::performProbGreater0(backwardTransitions, trueStates, phiStates); // The set of states we need to consider are those that have a non-zero probability to satisfy the condition or are on some path that has a psi state in it. - STORM_LOG_TRACE("Initial state: " << model.getInitialStates()); + STORM_LOG_TRACE("Initial state: " << this->getModel().getInitialStates()); STORM_LOG_TRACE("Phi states: " << phiStates); STORM_LOG_TRACE("Psi state: " << psiStates); STORM_LOG_TRACE("States with probability greater 0 of satisfying the condition: " << statesWithProbabilityGreater0); @@ -244,14 +220,14 @@ namespace storm { STORM_LOG_TRACE("Found " << maybeStates.getNumberOfSetBits() << " relevant states: " << maybeStates); // Determine the set of initial states of the sub-DTMC. - storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates; - STORM_LOG_TRACE("Found new initial states: " << newInitialStates << " (old: " << model.getInitialStates() << ")"); + storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; + STORM_LOG_TRACE("Found new initial states: " << newInitialStates << " (old: " << this->getModel().getInitialStates() << ")"); // Create a dummy vector for the one-step probabilities. std::vector oneStepProbabilities(maybeStates.getNumberOfSetBits(), storm::utility::zero()); // We then build the submatrix that only has the transitions of the maybe states. - storm::storage::SparseMatrix submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); // The states we want to eliminate are those that are tagged with "maybe" but are not a phi or psi state. @@ -425,23 +401,8 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, numerator / denominator)); } - template - std::unique_ptr SparseDtmcEliminationModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) { - if (stateFormula.isTrueFormula()) { - return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true))); - } else { - return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates()))); - } - } - - template - std::unique_ptr SparseDtmcEliminationModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { - STORM_LOG_THROW(model.hasLabel(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); - return std::unique_ptr(new ExplicitQualitativeCheckResult(model.getStates(stateFormula.getLabel()))); - } - - template - ValueType SparseDtmcEliminationModelChecker::computeReachabilityValue(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>& stateRewards, boost::optional> const& statePriorities) { + template + typename SparseDtmcEliminationModelChecker::ValueType SparseDtmcEliminationModelChecker::computeReachabilityValue(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>& stateRewards, boost::optional> const& statePriorities) { std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); // Create a bit vector that represents the subsystem of states we still have to eliminate. @@ -549,8 +510,8 @@ namespace storm { } } - template - std::vector SparseDtmcEliminationModelChecker::getStatePriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities) { + template + std::vector SparseDtmcEliminationModelChecker::getStatePriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities) { std::vector statePriorities(transitionMatrix.getRowCount()); std::vector states(transitionMatrix.getRowCount()); for (std::size_t index = 0; index < states.size(); ++index) { @@ -594,8 +555,8 @@ namespace storm { return statePriorities; } - template - uint_fast64_t SparseDtmcEliminationModelChecker::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>& stateRewards, boost::optional> const& statePriorities) { + template + uint_fast64_t SparseDtmcEliminationModelChecker::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>& stateRewards, boost::optional> const& statePriorities) { uint_fast64_t maximalDepth = level; // If the SCCs are large enough, we try to split them further. @@ -692,8 +653,8 @@ namespace storm { return maximalDepth; } - template - void SparseDtmcEliminationModelChecker::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) { + template + void SparseDtmcEliminationModelChecker::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) { bool hasSelfLoop = false; ValueType loopProbability = storm::utility::zero(); @@ -918,33 +879,33 @@ namespace storm { } } - template - SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::FlexibleSparseMatrix(index_type rows) : data(rows) { + template + SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::FlexibleSparseMatrix(index_type rows) : data(rows) { // Intentionally left empty. } - template - void SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::reserveInRow(index_type row, index_type numberOfElements) { + template + void SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::reserveInRow(index_type row, index_type numberOfElements) { this->data[row].reserve(numberOfElements); } - template - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type& SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::getRow(index_type index) { + template + typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type& SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::getRow(index_type index) { return this->data[index]; } - template - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type const& SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::getRow(index_type index) const { + template + typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::row_type const& SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::getRow(index_type index) const { return this->data[index]; } - template - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::index_type SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::getNumberOfRows() const { + template + typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::index_type SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::getNumberOfRows() const { return this->data.size(); } - template - bool SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::hasSelfLoop(storm::storage::sparse::state_type state) { + template + bool SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::hasSelfLoop(storm::storage::sparse::state_type state) { for (auto const& entry : this->getRow(state)) { if (entry.getColumn() < state) { continue; @@ -957,8 +918,8 @@ namespace storm { return false; } - template - void SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::print() const { + template + void SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::print() const { for (uint_fast64_t index = 0; index < this->data.size(); ++index) { std::cout << index << " - "; for (auto const& element : this->getRow(index)) { @@ -968,8 +929,8 @@ namespace storm { } } - template - typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix SparseDtmcEliminationModelChecker::getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) { + template + typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix SparseDtmcEliminationModelChecker::getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) { FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount()); // A comparator used for comparing probabilities. @@ -996,10 +957,10 @@ namespace storm { return flexibleMatrix; } - template class SparseDtmcEliminationModelChecker; + template class SparseDtmcEliminationModelChecker>; #ifdef STORM_HAVE_CARL - template class SparseDtmcEliminationModelChecker; + template class SparseDtmcEliminationModelChecker>; #endif } // namespace modelchecker } // namespace storm diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 2449f9542..7dd35bb17 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -3,24 +3,25 @@ #include "src/storage/sparse/StateType.h" #include "src/models/sparse/Dtmc.h" -#include "src/modelchecker/AbstractModelChecker.h" +#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/utility/constants.h" namespace storm { namespace modelchecker { - template - class SparseDtmcEliminationModelChecker : public AbstractModelChecker { + template + class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker { public: + typedef typename SparseDtmcModelType::ValueType ValueType; + typedef typename SparseDtmcModelType::RewardModelType RewardModelType; + explicit SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override; - virtual std::unique_ptr checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override; private: class FlexibleSparseMatrix { @@ -66,9 +67,6 @@ namespace storm { std::vector getStatePriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities); - // The model this model checker is supposed to analyze. - storm::models::sparse::Dtmc const& model; - // A comparator that can be used to compare constants. storm::utility::ConstantsComparator comparator; }; diff --git a/src/models/sparse/DeterministicModel.cpp b/src/models/sparse/DeterministicModel.cpp index 0694f4883..976535596 100644 --- a/src/models/sparse/DeterministicModel.cpp +++ b/src/models/sparse/DeterministicModel.cpp @@ -47,6 +47,13 @@ namespace storm { } } + template + void DeterministicModel::reduceToStateBasedRewards() { + for (auto& rewardModel : this->getRewardModels()) { + rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), true); + } + } + template class DeterministicModel; template class DeterministicModel; diff --git a/src/models/sparse/DeterministicModel.h b/src/models/sparse/DeterministicModel.h index 7abb3501e..4061f742f 100644 --- a/src/models/sparse/DeterministicModel.h +++ b/src/models/sparse/DeterministicModel.h @@ -52,6 +52,8 @@ namespace storm { DeterministicModel& operator=(DeterministicModel&& model) = default; #endif + virtual void reduceToStateBasedRewards() override; + virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const; }; diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index 82c88f3d9..f8d04654d 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -91,6 +91,27 @@ namespace storm { return it->second; } + template + bool Model::hasUniqueRewardModel() const { + return this->getNumberOfRewardModels() == 1; + } + + template + bool Model::hasRewardModel() const { + return !this->rewardModels.empty(); + } + + template + typename std::map::const_iterator Model::getUniqueRewardModel() const { + STORM_LOG_THROW(this->getNumberOfRewardModels() == 1, storm::exceptions::IllegalFunctionCallException, "The reward model is not unique."); + return this->rewardModels.cbegin(); + } + + template + uint_fast64_t Model::getNumberOfRewardModels() const { + return this->rewardModels.size(); + } + template std::vector const& Model::getChoiceLabeling() const { return choiceLabeling.get(); @@ -116,13 +137,6 @@ namespace storm { return static_cast(choiceLabeling); } - template - void Model::convertTransitionRewardsToStateActionRewards() { - for (auto& rewardModel : this->rewardModels) { - rewardModel.second.convertTransitionRewardsToStateActionRewards(this->getTransitionMatrix()); - } - } - template std::size_t Model::getSizeInBytes() const { std::size_t result = transitionMatrix.getSizeInBytes() + stateLabeling.getSizeInBytes(); @@ -161,7 +175,7 @@ namespace storm { void Model::printRewardModelsInformationToStream(std::ostream& out) const { if (this->rewardModels.size()) { std::vector rewardModelNames; - std::for_each(this->rewardModels.begin(), this->rewardModels.end(), [&rewardModelNames] (typename std::map::const_iterator const& it) { rewardModelNames.push_back(it->first); }); + std::for_each(this->rewardModels.cbegin(), this->rewardModels.cend(), [&rewardModelNames] (typename std::pair const& nameRewardModelPair) { rewardModelNames.push_back(nameRewardModelPair.first); }); out << "Reward Models: " << boost::join(rewardModelNames, ", ") << std::endl; } else { out << "Reward Models: none" << std::endl; @@ -252,6 +266,17 @@ namespace storm { return true; } + template + std::map& Model::getRewardModels() { + return this->rewardModels; + } + + template + std::map const& Model::getRewardModels() const { + return this->rewardModels; + } + + template class Model; template class Model; diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index 02fe59024..4cd0d3ada 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -148,6 +148,34 @@ namespace storm { */ RewardModelType const& getRewardModel(std::string const& rewardModelName) const; + /*! + * Retrieves the unique reward model, if there exists exactly one. Otherwise, an exception is thrown. + * + * @return An iterator to the name and the reward model. + */ + typename std::map::const_iterator getUniqueRewardModel() const; + + /*! + * Retrieves whether the model has a unique reward model. + * + * @return True iff the model has a unique reward model. + */ + bool hasUniqueRewardModel() const; + + /*! + * Retrieves whether the model has at least one reward model. + * + * @return True iff the model has a reward model. + */ + bool hasRewardModel() const; + + /*! + * Retrieves the number of reward models associated with this model. + * + * @return The number of reward models associated with this model. + */ + uint_fast64_t getNumberOfRewardModels() const; + /*! * Retrieves the labels for the choices of the model. Note that calling this method is only valid if the * model has a choice labeling. @@ -185,11 +213,12 @@ namespace storm { bool hasChoiceLabeling() const; /*! - * Converts the transition rewards of all reward models to state rewards. Note that calling this method - * is only valid if the model has transition rewards. Also note that this does not preserve all + * Converts the transition rewards of all reward models to state-based rewards. For deterministic models, + * this reduces the rewards to state rewards only. For nondeterminstic models, the reward models will + * contain state rewards and state-action rewards. Note that this transformation does not preserve all * properties, but it preserves expected rewards. */ - void convertTransitionRewardsToStateActionRewards(); + virtual void reduceToStateBasedRewards() = 0; /*! * Retrieves (an approximation of) the size of the model in bytes. @@ -274,6 +303,13 @@ namespace storm { */ std::map const& getRewardModels() const; + /*! + * Retrieves the reward models. + * + * @return A mapping from reward model names to the reward models. + */ + std::map& getRewardModels(); + private: // A matrix representing transition relation. storm::storage::SparseMatrix transitionMatrix; diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp index 38888a39e..a620095cc 100644 --- a/src/models/sparse/NondeterministicModel.cpp +++ b/src/models/sparse/NondeterministicModel.cpp @@ -43,6 +43,13 @@ namespace storm { return indices[state+1] - indices[state]; } + template + void NondeterministicModel::reduceToStateBasedRewards() { + for (auto& rewardModel : this->getRewardModels()) { + rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), false); + } + } + template void NondeterministicModel::printModelInformationToStream(std::ostream& out) const { this->printModelInformationHeaderToStream(out); diff --git a/src/models/sparse/NondeterministicModel.h b/src/models/sparse/NondeterministicModel.h index 901b146ba..1476506c3 100644 --- a/src/models/sparse/NondeterministicModel.h +++ b/src/models/sparse/NondeterministicModel.h @@ -73,6 +73,8 @@ namespace storm { */ uint_fast64_t getNumberOfChoices(uint_fast64_t state) const; + virtual void reduceToStateBasedRewards() override; + virtual void printModelInformationToStream(std::ostream& out) const; virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const; diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp index f33672c07..fbd76593a 100644 --- a/src/models/sparse/StandardRewardModel.cpp +++ b/src/models/sparse/StandardRewardModel.cpp @@ -28,6 +28,11 @@ namespace storm { return static_cast(this->optionalStateRewardVector); } + template + bool StandardRewardModel::hasOnlyStateRewards() const { + return static_cast(this->optionalStateRewardVector) && !static_cast(this->optionalStateActionRewardVector) && !static_cast(this->optionalTransitionRewardMatrix); + } + template std::vector const& StandardRewardModel::getStateRewardVector() const { return this->optionalStateRewardVector.get(); @@ -85,14 +90,23 @@ namespace storm { template template - void StandardRewardModel::convertTransitionRewardsToStateActionRewards(storm::storage::SparseMatrix const& transitionMatrix) { - STORM_LOG_THROW(this->hasTransitionRewards(), storm::exceptions::InvalidOperationException, "Cannot reduce non-existant transition rewards to state rewards."); - if (this->hasStateActionRewards()) { - storm::utility::vector::addVectors(this->getStateActionRewardVector(), transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()), this->getStateActionRewardVector); - } else { - this->optionalStateActionRewardVector = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()); + void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards) { + if (this->hasTransitionRewards()) { + if (this->hasStateActionRewards()) { + storm::utility::vector::addVectors(this->getStateActionRewardVector(), transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()), this->getStateActionRewardVector); + } else { + this->optionalStateActionRewardVector = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()); + } + } + + if (reduceToStateRewards && this->hasStateActionRewards()) { + if (this->hasStateRewards()) { + STORM_LOG_THROW(this->getStateRewardVector.size() == this->getStateActionRewardVector().size(), storm::exceptions::InvalidOperationException, "The reduction to state rewards is only possible of both the state and the state-action rewards have the same dimension."); + storm::utility::vector::addVectors(this->getStateActionRewardVector(), this->getStateRewardVector(), this->getStateRewardVector()); + } else { + this->optionalStateRewardVector = std::move(this->optionalStateRewardVector); + } } - this->optionalTransitionRewardMatrix = boost::optional>(); } template diff --git a/src/models/sparse/StandardRewardModel.h b/src/models/sparse/StandardRewardModel.h index 7723a3d72..52727ffad 100644 --- a/src/models/sparse/StandardRewardModel.h +++ b/src/models/sparse/StandardRewardModel.h @@ -49,6 +49,13 @@ namespace storm { * @return True iff the reward model has state rewards. */ bool hasStateRewards() const; + + /*! + * Retrieves whether the reward model only has state rewards (and hence no other rewards). + * + * @return True iff the reward model only has state rewards. + */ + bool hasOnlyStateRewards() const; /*! * Retrieves the state rewards of the reward model. Note that it is illegal to call this function if the @@ -118,15 +125,16 @@ namespace storm { StandardRewardModel restrictActions(storm::storage::BitVector const& enabledActions) const; /*! - * Converts the transition-based rewards to state-action rewards by taking the average of each row. Note - * that this preserves expected rewards, but not all reward-based properties. Also note that it is only - * legal to do this transformation if the reward model has transition rewards. + * Reduces the transition-based rewards to state-action rewards by taking the average of each row. If + * the corresponding flag is set, the state-action rewards and the state rewards are summed so the model + * only has a state reward vector left. Note that this transformation only preserves expected rewards, + * but not all reward-based properties. * * @param transitionMatrix The transition matrix that is used to weight the rewards in the reward matrix. */ template - void convertTransitionRewardsToStateActionRewards(storm::storage::SparseMatrix const& transitionMatrix); - + void reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards = false); + /*! * Creates a vector representing the complete reward vector based on the state-, state-action- and * transition-based rewards in the reward model. diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index 32b3209ea..9b33a647d 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -37,15 +37,19 @@ namespace storm { } storm::models::sparse::Dtmc DeterministicModelParser::parseDtmc(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) { + DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))); - DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))); - return storm::models::sparse::Dtmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + std::map> rewardModels; + rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(parserResult.stateRewards, boost::optional>(), parserResult.transitionRewards))); + return storm::models::sparse::Dtmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), boost::optional>>()); } storm::models::sparse::Ctmc DeterministicModelParser::parseCtmc(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) { + DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))); - DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))); - return storm::models::sparse::Ctmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + std::map> rewardModels; + rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(parserResult.stateRewards, boost::optional>(), parserResult.transitionRewards))); + return storm::models::sparse::Ctmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), boost::optional>>()); } } /* namespace parser */ diff --git a/src/parser/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp index dfb64ce34..4f7898d1e 100644 --- a/src/parser/MarkovAutomatonParser.cpp +++ b/src/parser/MarkovAutomatonParser.cpp @@ -22,10 +22,12 @@ namespace storm { storm::models::sparse::StateLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(transitionMatrix.getColumnCount(), labelingFilename)); // If given, parse the state rewards file. - boost::optional> stateRewards; + boost::optional> stateRewards; if (stateRewardFilename != "") { stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(transitionMatrix.getColumnCount(), stateRewardFilename)); } + std::map> rewardModels; + rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(stateRewards, boost::optional>(), boost::optional>()))); // Since Markov Automata do not support transition rewards no path should be given here. if (transitionRewardFilename != "") { @@ -34,7 +36,7 @@ namespace storm { } // Put the pieces together to generate the Markov Automaton. - storm::models::sparse::MarkovAutomaton resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional>(), boost::optional>>()); + storm::models::sparse::MarkovAutomaton resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), rewardModels, boost::optional>>()); return resultingAutomaton; } diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index 080c86d65..b127ede6a 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -41,9 +41,11 @@ namespace storm { } storm::models::sparse::Mdp NondeterministicModelParser::parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) { - - Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename); - return storm::models::sparse::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename); + + std::map> rewardModels; + rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(parserResult.stateRewards, boost::optional>(), parserResult.transitionRewards))); + return storm::models::sparse::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), boost::optional>>()); } } /* namespace parser */ diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 395202ed1..e6834121f 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -651,7 +651,7 @@ namespace storm { } if (measureDrivenInitialPartition) { - storm::modelchecker::SparsePropositionalModelChecker checker(model); + storm::modelchecker::SparsePropositionalModelChecker> checker(model); std::unique_ptr phiStatesCheckResult = checker.check(*leftSubformula); std::unique_ptr psiStatesCheckResult = checker.check(*rightSubformula); phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector(); @@ -666,7 +666,8 @@ namespace storm { template DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::sparse::Dtmc const& model, Options const& options) { - STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards. Consider converting the transition rewards to state rewards (via suitable function calls)."); + STORM_LOG_THROW(!model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model."); + STORM_LOG_THROW(!model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls)."); STORM_LOG_THROW(!options.weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); BisimulationType bisimulationType = options.weak ? BisimulationType::WeakDtmc : BisimulationType::Strong; @@ -680,8 +681,8 @@ namespace storm { Partition initialPartition; if (options.measureDrivenInitialPartition) { - STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); - STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); + STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi states."); + STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without psi states."); initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded); } else { initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards); @@ -692,7 +693,8 @@ namespace storm { template DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::sparse::Ctmc const& model, Options const& options) { - STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards. Consider converting the transition rewards to state rewards (via suitable function calls)."); + STORM_LOG_THROW(!model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model."); + STORM_LOG_THROW(!model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls)."); STORM_LOG_THROW(!options.weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); BisimulationType bisimulationType = options.weak ? BisimulationType::WeakCtmc : BisimulationType::Strong; @@ -744,7 +746,7 @@ namespace storm { // If the model had state rewards, we need to build the state rewards for the quotient as well. boost::optional> stateRewards; - if (keepRewards && model.hasStateRewards()) { + if (keepRewards && model.hasRewardModel()) { stateRewards = std::vector(this->blocks.size()); } @@ -824,8 +826,9 @@ namespace storm { // If the model has state rewards, we simply copy the state reward of the representative state, because // all states in a block are guaranteed to have the same state reward. - if (keepRewards && model.hasStateRewards()) { - stateRewards.get()[blockIndex] = model.getStateRewardVector()[representativeState]; + if (keepRewards && model.hasRewardModel()) { + typename std::map::const_iterator nameRewardModelPair = model.getUniqueRewardModel(); + stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState]; } } @@ -835,8 +838,15 @@ namespace storm { newLabeling.addLabelToState("init", initialBlock.getId()); } + // Construct the reward model mapping. + std::map rewardModels; + if (keepRewards && model.hasRewardModel()) { + typename std::map::const_iterator nameRewardModelPair = model.getUniqueRewardModel(); + rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards))); + } + // Finally construct the quotient model. - this->quotient = std::shared_ptr>(new ModelType(builder.build(), std::move(newLabeling), std::move(stateRewards))); + this->quotient = std::shared_ptr>(new ModelType(builder.build(), std::move(newLabeling), std::move(rewardModels))); } template @@ -1304,8 +1314,8 @@ namespace storm { // If the model has state rewards, we need to consider them, because otherwise reward properties are not // preserved. - if (keepRewards && model.hasStateRewards()) { - this->splitRewards(model, partition); + if (keepRewards && model.hasRewardModel()) { + this->splitRewards(model.getUniqueRewardModel()->second.getStateRewardVector(), partition); } // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent @@ -1409,8 +1419,8 @@ namespace storm { // If the model has state rewards, we need to consider them, because otherwise reward properties are not // preserved. - if (keepRewards && model.hasStateRewards()) { - this->splitRewards(model, partition); + if (keepRewards && model.hasRewardModel()) { + this->splitRewards(model.getUniqueRewardModel()->second.getStateRewardVector(), partition); } // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent @@ -1441,20 +1451,15 @@ namespace storm { } template - template - void DeterministicModelBisimulationDecomposition::splitRewards(ModelType const& model, Partition& partition) { - if (!model.hasStateRewards()) { - return; - } - + void DeterministicModelBisimulationDecomposition::splitRewards(std::vector const& stateRewardVector, Partition& partition) { for (auto& block : partition.getBlocks()) { - std::sort(partition.getBegin(block), partition.getEnd(block), [&model] (std::pair const& a, std::pair const& b) { return model.getStateRewardVector()[a.first] < model.getStateRewardVector()[b.first]; } ); + std::sort(partition.getBegin(block), partition.getEnd(block), [&stateRewardVector] (std::pair const& a, std::pair const& b) { return stateRewardVector[a.first] < stateRewardVector[b.first]; } ); // Update the positions vector and put the (state) reward values next to the states so we can easily compare them later. storm::storage::sparse::state_type position = block.getBegin(); for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) { partition.setPosition(stateIt->first, position); - stateIt->second = model.getStateRewardVector()[stateIt->first]; + stateIt->second = stateRewardVector[stateIt->first]; } // Finally, we need to scan the ranges of states that agree on the probability. diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index 7dcc67614..e824a76ed 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -544,11 +544,10 @@ namespace storm { /*! * Splits all blocks of the partition in a way such that the states of each block agree on the rewards. * - * @param model The model from which to look-up the rewards. + * @param stateRewardVector The state reward vector of the model. * @param partition The partition that is to be split. */ - template - void splitRewards(ModelType const& model, Partition& partition); + void splitRewards(std::vector const& stateRewardVector, Partition& partition); // If required, a quotient model is built and stored in this member. std::shared_ptr> quotient; diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp index fb1a944ba..b97fb6cc8 100644 --- a/src/storage/prism/Update.cpp +++ b/src/storage/prism/Update.cpp @@ -58,7 +58,9 @@ namespace storm { if (update.getAssignments().empty()) { stream << " true "; } else { - stream << boost::algorithm::join(update.getAssignments(), " & "); + std::vector assignmentsAsStrings; + std::for_each(update.getAssignments().cbegin(), update.getAssignments().cend(), [&assignmentsAsStrings] (Assignment const& assignment) { std::stringstream stream; stream << assignment; assignmentsAsStrings.push_back(stream.str()); }); + stream << boost::algorithm::join(assignmentsAsStrings, " & "); } return stream; } diff --git a/src/utility/cli.h b/src/utility/cli.h index 63de731b3..a51e5072d 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -145,9 +145,7 @@ namespace storm { STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs."); std::shared_ptr> dtmc = sparseModel->template as>(); - if (dtmc->hasTransitionRewards()) { - dtmc->convertTransitionRewardsToStateRewards(); - } + dtmc->reduceToStateBasedRewards(); std::cout << "Performing bisimulation minimization... "; typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; diff --git a/src/utility/vector.h b/src/utility/vector.h index 52556fd0c..51816ffb5 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -153,7 +153,6 @@ namespace storm { template void addVectorToGroupedVector(std::vector& target, std::vector const& source, std::vector const& rowGroupIndices) { auto targetIt = target.begin(); - auto targetIte = target.end(); auto sourceIt = source.cbegin(); auto sourceIte = source.cend(); auto rowGroupIt = rowGroupIndices.cbegin(); @@ -163,7 +162,7 @@ namespace storm { ++rowGroupIt; uint_fast64_t next = *rowGroupIt; while (current < next) { - *targetIt = *source; + *targetIt = *sourceIt; ++targetIt; } }