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);