diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 513f9d8cb..5b296a5a2 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -30,7 +30,7 @@ namespace storm { SparseCtmcCslModelChecker::SparseCtmcCslModelChecker(SparseCtmcModelType const& model) : SparsePropositionalModelChecker(model) { // Intentionally left empty. } - + template bool SparseCtmcCslModelChecker::canHandleStatic(CheckTask const& checkTask) { auto fragment = storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setTotalRewardFormulasAllowed(true).setRewardAccumulationAllowed(true); @@ -39,12 +39,12 @@ namespace storm { } return checkTask.getFormula().isInFragment(fragment); } - + template bool SparseCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { return canHandleStatic(checkTask); } - + template std::unique_ptr SparseCtmcCslModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); @@ -68,7 +68,7 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), lowerBound, upperBound); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + template std::unique_ptr SparseCtmcCslModelChecker::computeNextProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); @@ -77,7 +77,7 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeNextProbabilities(env, this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + template std::unique_ptr SparseCtmcCslModelChecker::computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); @@ -88,7 +88,61 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + + template + std::unique_ptr SparseCtmcCslModelChecker::computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); + + std::vector extracted; + std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted); + + STORM_LOG_INFO("Extracting maximal state formulas and computing satisfaction sets for path formula: " << pathFormula); + + std::map apSets; + + for (auto& p : extracted) { + STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "..."); + + std::unique_ptr subResultPointer = this->check(env, *p.second); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + auto sat = subResult.getTruthValuesVector(); + + STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states."); + + apSets[p.first] = std::move(sat); + } + + STORM_LOG_INFO("Resulting LTL path formula: " << *ltlFormula); + STORM_LOG_INFO(" in prefix format: " << ltlFormula->toPrefixString()); + + std::shared_ptr da = storm::automata::LTL2DeterministicAutomaton::ltl2da(*ltlFormula, false); + + STORM_LOG_INFO("Deterministic automaton for LTL formula has " + << da->getNumberOfStates() << " states, " + << da->getAPSet().size() << " atomic propositions and " + << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition."); + + const SparseCtmcModelType& ctmc = this->getModel(); + typedef typename storm::models::sparse::Dtmc SparseDtmcModelType; + + STORM_LOG_INFO("Computing embedded DTMC..."); + // compute probability matrix (embedded DTMC) + storm::storage::SparseMatrix probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(ctmc.getTransitionMatrix(), ctmc.getExitRateVector()); + // copy of the state labelings of the CTMC + storm::models::sparse::StateLabeling labeling(ctmc.getStateLabeling()); + + // the embedded DTMC, used for building the product and computing the probabilities in the product + SparseDtmcModelType embeddedDtmc(std::move(probabilityMatrix), std::move(labeling)); + storm::solver::SolveGoal goal(embeddedDtmc, checkTask); + + + STORM_LOG_INFO("Performing DA product and probability computations in embedded DTMC..."); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeDAProductProbabilities(env, embeddedDtmc, std::move(goal), *da, apSets, checkTask.isQualitativeSet()); + // we can directly return the numericResult vector as the state space of the CTMC and the embedded DTMC are exactly the same + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + + template std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); @@ -96,7 +150,7 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + template std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); @@ -105,7 +159,7 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModel.get(), rewardPathFormula.getNonStrictBound()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + template std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); @@ -115,25 +169,25 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + template std::unique_ptr SparseCtmcCslModelChecker::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTotalRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), rewardModel.get(), checkTask.isQualitativeSet()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - + template std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - + auto probabilisticTransitions = this->getModel().computeProbabilityMatrix(); storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(probabilisticTransitions, this->getModel().getExitRateVector()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector()); - + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(values))); } @@ -146,7 +200,7 @@ namespace storm { auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(values))); } - + template std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); @@ -172,13 +226,13 @@ namespace storm { std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities(env, this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), upperBound); return result; } - + template std::unique_ptr SparseCtmcCslModelChecker::computeSteadyStateDistribution(Environment const& env) { // Initialize helper auto probabilisticTransitions = this->getModel().computeProbabilityMatrix(); storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(probabilisticTransitions, this->getModel().getExitRateVector()); - + // Compute result std::vector result; auto const& initialStates = this->getModel().getInitialStates(); diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 12b51dcf4..36a066da6 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -23,9 +23,8 @@ namespace storm { } - // todo only for MDP and change name! template - storm::storage::BitVector SparseLTLHelper::computeSurelyAcceptingPmaxStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions) { + storm::storage::BitVector SparseLTLHelper::computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions) { STORM_LOG_INFO("Computing accepting states for acceptance condition " << *acceptance.getAcceptanceExpression()); if (acceptance.getAcceptanceExpression()->isTRUE()) { STORM_LOG_INFO(" TRUE -> all states accepting (assumes no deadlock in the model)"); @@ -135,9 +134,8 @@ namespace storm { return acceptingStates; } - // todo only for dtmc and change name! template - storm::storage::BitVector SparseLTLHelper::computeAcceptingComponentStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix) { + storm::storage::BitVector SparseLTLHelper::computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix) { storm::storage::StronglyConnectedComponentDecomposition bottomSccs(transitionMatrix, storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs().dropNaiveSccs()); //storm::storage::BitVector acceptingStates = storm::storage::BitVector(product->getProductModel().getNumberOfStates()); storm::storage::BitVector acceptingStates(transitionMatrix.getRowGroupCount(), false); @@ -179,7 +177,6 @@ namespace storm { } - // todo change text STORM_LOG_INFO("Building "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +"product with deterministic automaton, starting from " << statesOfInterest.getNumberOfSetBits() << " model states..."); storm::transformer::DAProductBuilder productBuilder(da, apLabels); @@ -200,19 +197,15 @@ namespace storm { STORM_LOG_TRACE(str.str()); } - // DTMC: BCC - // MDP: computeSurelyAcceptingPmaxStates + // Compute accepting states storm::storage::BitVector acceptingStates; if (Nondeterministic) { - STORM_LOG_INFO("Computing accepting end components..."); - // todo compute accepting states, same as below - acceptingStates = computeSurelyAcceptingPmaxStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions()); - + STORM_LOG_INFO("Computing MECs and checking for acceptance..."); + acceptingStates = computeAcceptingECs(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions()); } else { STORM_LOG_INFO("Computing BSCCs and checking for acceptance..."); - // todo compute accepting states, (no btm) - acceptingStates = computeAcceptingComponentStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix()); + acceptingStates = computeAcceptingBCCs(*product->getAcceptance(), product->getProductModel().getTransitionMatrix()); } @@ -227,7 +220,7 @@ namespace storm { storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true); storm::storage::BitVector soiProduct(product->getStatesOfInterest()); - // Create goal for computeUntilProbabilities, compute maximizing probabilities for DA product with MDP + // Create goal for computeUntilProbabilities, always compute maximizing probabilities storm::solver::SolveGoal solveGoalProduct; if (this->isValueThresholdSet()) { solveGoalProduct = storm::solver::SolveGoal(OptimizationDirection::Maximize, this->getValueThresholdComparisonType(), this->getValueThresholdValue(), std::move(soiProduct)); @@ -263,6 +256,7 @@ namespace storm { return numericResult; } + template std::vector SparseLTLHelper::computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map& apSatSets) { std::shared_ptr ltlFormula; @@ -279,7 +273,7 @@ namespace storm { STORM_LOG_INFO("Resulting LTL path formula: " << ltlFormula->toString()); STORM_LOG_INFO(" in prefix format: " << ltlFormula->toPrefixString()); - std::shared_ptr da = storm::automata::LTL2DeterministicAutomaton::ltl2da(*ltlFormula); + std::shared_ptr da = storm::automata::LTL2DeterministicAutomaton::ltl2da(*ltlFormula, Nondeterministic); STORM_LOG_INFO("Deterministic automaton for LTL formula has " << da->getNumberOfStates() << " states, " @@ -287,7 +281,6 @@ namespace storm { << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition."); - // compute Pmax for MDP std::vector numericResult = computeDAProductProbabilities(env, *da, apSatSets, this->isQualitativeSet()); if(Nondeterministic && this->getOptimizationDirection()==OptimizationDirection::Minimize) { @@ -297,7 +290,6 @@ namespace storm { } } - return numericResult; } diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index b8944446c..29ab7a100 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -12,7 +12,7 @@ namespace storm { namespace helper { /*! - * Helper class for todo... + * Helper class for LTL model checking * @tparam ValueType the type a value can have * @tparam Nondeterministic true if there is nondeterminism in the Model (MDP) */ @@ -22,47 +22,59 @@ namespace storm { public: /*! - * The type of the product automaton model // todo + * The type of the product automaton (DTMC or MDP) that is used during the computation. */ using productModelType = typename std::conditional, storm::models::sparse::Dtmc>::type; /*! - * Initializes the helper for a discrete time (i.e. DTMC, MDP) + * Initializes the helper for a discrete time model (i.e. DTMC, MDP) + * @param the transition matrix of the model + * @param the number of states of the model */ SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix, std::size_t numberOfSates); /*! - * todo - * Computes maximizing(!) probabilties for DA product with MDP - * @return + * Computes the LTL probabilities + * @param the LTL formula + * @param the atomic propositions and satisfaction sets + * @return a value for each state */ - std::vector computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative); - + std::vector computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map& apSatSets); /*! - * Computes the ltl probabilities ...todo + * Computes the (maximizing) probabilities for the constructed DA product + * @param the DA to build the product with + * @param the atomic propositions and satisfaction sets + * @param a flag indicating whether qualitative model checking is performed * @return a value for each state */ - std::vector computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map& apSatSets); //todo was brauchen wir hier aps und ..? + std::vector computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative); private: - /*! todo only relevant for MDP - enable_if_t ? - * Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance conditon. + /*! + * Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance condition (in DNF). * More precisely, let * accEC be the set of states that are contained in end components that satisfy the acceptance condition * and let * P1acc be the set of states that satisfy Pmax=1[ F accEC ]. * This function then computes a set that contains accEC and is contained by P1acc. * However, if the acceptance condition consists of 'true', the whole state space can be returned. + * @param the acceptance condition (in DNF) + * @param the transition matrix of the model + * @param the reversed transition relation */ - static storm::storage::BitVector computeSurelyAcceptingPmaxStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions); - - //todo only for dtmc, different to mdp: no backward tm - static storm::storage::BitVector computeAcceptingComponentStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix); + static storm::storage::BitVector computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions); + + /** + * Compute a set S of states that are contained in BSCCs that satisfy the given acceptance conditon. + * @tparam the acceptance condition + * @tparam the transition matrix of the model + */ + static storm::storage::BitVector computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix); storm::storage::SparseMatrix const& _transitionMatrix; diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 28009225c..95e87164f 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -176,7 +176,6 @@ namespace storm { const SparseDtmcModelType& dtmc = this->getModel(); - // TODO if (storm::settings::getModule().isTraceSet()) { STORM_LOG_TRACE("Writing model to model.dot"); std::ofstream modelDot("model.dot");