From 4dca7abd3f6c7540c3dcd67796752a74b4a40659 Mon Sep 17 00:00:00 2001 From: masawei Date: Wed, 16 Oct 2013 00:01:33 +0200 Subject: [PATCH] Implementaed methods for checking until formula by providing the left and right states instead of the whole formula (same with bounded Until) in the SparseDtmcPrctlModelChecker, analouge to the SparseMdpPrctlModelChecker. Reverted unnecessary changes to the AbstractModel checker. Next on the list: Adapting the subsystem generation routine to the new method of providing the subsystem to the model checker. Former-commit-id: 6c90c064a2b222101ad98f1da594cdf6ef3e153d --- .../PathBasedSubsystemGenerator.h | 10 ++-- src/modelchecker/prctl/AbstractModelChecker.h | 40 ++------------ .../prctl/SparseDtmcPrctlModelChecker.h | 52 +++++++++++++++---- 3 files changed, 50 insertions(+), 52 deletions(-) diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h index b29ac334a..ae8a997d4 100644 --- a/src/counterexamples/PathBasedSubsystemGenerator.h +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -64,7 +64,7 @@ public: distances[*init].second = (T) 1; } - typename storm::storage::SparseMatrix::ConstRowsIterator trans = transMat.begin(*init); + typename storm::storage::SparseMatrix::ConstRowIterator trans = transMat.begin(*init); for(; trans != transMat.end(*init); ++trans) { //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { @@ -111,7 +111,7 @@ public: // Same goes for forbidden states since they may not be used on a path, except as last node. if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { // Look at all neighbors - for(typename storm::storage::SparseMatrix::ConstRowsIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) { + for(typename storm::storage::SparseMatrix::ConstRowIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) { // Only consider the transition if it's not virtual if(trans.value() != (T) 0) { @@ -178,7 +178,7 @@ public: continue; } - typename storm::storage::SparseMatrix::ConstRowsIterator trans = transMat.begin(*init); + typename storm::storage::SparseMatrix::ConstRowIterator trans = transMat.begin(*init); for(; trans != transMat.end(*init); ++trans) { //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { @@ -230,7 +230,7 @@ public: // Same goes for forbidden states since they may not be used on a path, except as last node. if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { // Look at all neighbors - for(typename storm::storage::SparseMatrix::ConstRowsIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) { + for(typename storm::storage::SparseMatrix::ConstRowIterator trans = transMat.begin(activeState.first); trans != transMat.end(activeState.first); ++trans) { // Only consider the transition if it's not virtual if(trans.value() != (T) 0) { @@ -508,7 +508,7 @@ public: /*! * */ - static void computeCriticalSubsystem(storm::modelchecker::prctl::AbstractModelChecker const& modelCheck, storm::property::prctl::AbstractStateFormula const& stateFormula) { + static void computeCriticalSubsystem(storm::modelchecker::prctl::AbstractModelChecker& modelCheck, storm::property::prctl::AbstractStateFormula const& stateFormula) { //------------------------------------------------------------- // 1. Strip and handle formulas diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index a45a1dc50..713413478 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -68,14 +68,14 @@ public: /*! * Constructs an AbstractModelChecker with the given model. */ - explicit AbstractModelChecker(storm::models::AbstractModel const& model, storm::storage::BitVector* subSystem = nullptr) : model(model), subSystem(subSystem) { + explicit AbstractModelChecker(storm::models::AbstractModel const& model) : model(model){ // Intentionally left empty. } /*! * Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly * constructed model checker will have the model of the given model checker as its associated model. */ - explicit AbstractModelChecker(AbstractModelChecker const& modelchecker) : model(modelchecker.model), subSystem(modelchecker.subSystem) { + explicit AbstractModelChecker(AbstractModelChecker const& modelchecker) : model(modelchecker.model) { // Intentionally left empty. } @@ -147,7 +147,6 @@ public: LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString()); std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl; storm::storage::BitVector result; - bool allSatisfied = true; try { result = stateFormula.check(*this); LOG4CPLUS_INFO(logger, "Result for initial states:"); @@ -155,19 +154,12 @@ public: for (auto initialState : model.getInitialStates()) { LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied")); std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl; - allSatisfied &= result.get(initialState); } } catch (std::exception& e) { std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property."); } - if(!allSatisfied && storm::settings::Settings::getInstance()->getOptionByLongName("prctl").getArgumentByName("subSys").getValueAsBoolean()) { - //generate critical subsystem - storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(*this, stateFormula); - } - - std::cout << std::endl << "-------------------------------------------" << std::endl; } @@ -205,11 +197,7 @@ public: */ storm::storage::BitVector checkAp(storm::property::prctl::Ap const& formula) const { if (formula.getAp() == "true") { - if(subSystem != nullptr) { - return *subSystem; - } else { - return storm::storage::BitVector(model.getNumberOfStates(), true); - } + return storm::storage::BitVector(model.getNumberOfStates(), true); } else if (formula.getAp() == "false") { return storm::storage::BitVector(model.getNumberOfStates()); } @@ -219,11 +207,7 @@ public: throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; } - if(subSystem != nullptr) { - return *subSystem & storm::storage::BitVector(model.getLabeledStates(formula.getAp())); - } else { - return storm::storage::BitVector(model.getLabeledStates(formula.getAp())); - } + return storm::storage::BitVector(model.getLabeledStates(formula.getAp())); } /*! @@ -313,15 +297,6 @@ public: return result; } - /*! - * Sets the subsystem. - * - * @param subSystem The subsystem the model check is to be confined to. - */ - void setSubSystem(storm::storage::BitVector* subSys) { - subSystem = subSys; - } - private: /*! @@ -331,13 +306,6 @@ private: * model checker object is unsafe after the object has been destroyed. */ storm::models::AbstractModel const& model; - - /*! - * A pointer to the subsystem of the Model to which the check of the model is to be confined. - * - * @note that this is a nullptr iff the check is not to be confined. - */ - storm::storage::BitVector* subSystem; }; } // namespace prctl diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 03245000d..45ae525c7 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -74,6 +74,7 @@ public: return formula.check(*this, false); } + /*! * Checks the given formula that is a bounded-until formula. * @@ -86,14 +87,29 @@ public: * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector checkBoundedUntil(storm::property::prctl::BoundedUntil const& formula, bool qualitative) const { - // First, we need to compute the states that satisfy the sub-formulas of the bounded until-formula. - storm::storage::BitVector leftStates = formula.getLeft().check(*this); - storm::storage::BitVector rightStates = formula.getRight().check(*this); + return this->checkBoundedUntil(formula.getLeft().check(*this), formula.getRight().check(*this), formula.getBound(), qualitative); + } + + + /*! + * Computes the probability to satisfy phi until psi inside a given bound for each state in the model. + * + * @param phiStates A bit vector indicating which states satisfy phi. + * @param psiStates A bit vector indicating which states satisfy psi. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. + */ + virtual std::vector checkBoundedUntil(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, bool qualitative) const { + std::vector result(this->getModel().getNumberOfStates()); // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the // further analysis. - storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), leftStates, rightStates, true, formula.getBound()); + storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), phiStates, psiStates, true, stepBound); LOG4CPLUS_INFO(logger, "Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states."); // Check if we already know the result (i.e. probability 0) for all initial states and @@ -111,7 +127,7 @@ public: storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0); // Compute the new set of target states in the reduced system. - storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % rightStates; + storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % psiStates; // Make all rows absorbing that satisfy the second sub-formula. submatrix.makeRowsAbsorbing(rightStatesInReducedSystem); @@ -122,7 +138,7 @@ public: // Perform the matrix vector multiplication as often as required by the formula bound. if (linearEquationSolver != nullptr) { - this->linearEquationSolver->performMatrixVectorMultiplication(submatrix, subresult, nullptr, formula.getBound()); + this->linearEquationSolver->performMatrixVectorMultiplication(submatrix, subresult, nullptr, stepBound); } else { throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; } @@ -219,6 +235,7 @@ public: return result; } + /*! * Check the given formula that is an until formula. * @@ -231,13 +248,26 @@ public: * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector checkUntil(storm::property::prctl::Until const& formula, bool qualitative) const { - // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - storm::storage::BitVector leftStates = formula.getLeft().check(*this); - storm::storage::BitVector rightStates = formula.getRight().check(*this); + return this->checkUntil(formula.getLeft().check(*this), formula.getRight().check(*this), qualitative); + } + + /*! + * Computes the probability to satisfy phi until psi for each state in the model. + * + * @param phiStates A bit vector indicating which states satisfy phi. + * @param psiStates A bit vector indicating which states satisfy psi. + * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the + * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only + * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the + * bounds 0 and 1. + * @returns The probabilities for the given formula to hold on every state of the model associated with this model + * checker. If the qualitative flag is set, exact probabilities might not be computed. + */ + virtual std::vector checkUntil(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const { - // Then, we need to identify the states which have to be taken out of the matrix, i.e. + // We need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. - std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), leftStates, rightStates); + std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), phiStates, psiStates); storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);