diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp new file mode 100644 index 000000000..56d48344d --- /dev/null +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -0,0 +1,88 @@ +#include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" + +#include + +#include "src/utility/macros.h" +#include "src/utility/vector.h" +#include "src/utility/graph.h" +#include "src/utility/solver.h" + +#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" + +#include "src/exceptions/InvalidPropertyException.h" +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace modelchecker { + template + SparseCtmcCslModelChecker::SparseCtmcCslModelChecker(storm::models::Ctmc const& model) : SparsePropositionalModelChecker(model), linearEquationSolver(storm::utility::solver::getLinearEquationSolver()) { + // Intentionally left empty. + } + + template + SparseCtmcCslModelChecker::SparseCtmcCslModelChecker(storm::models::Ctmc const& model, std::unique_ptr>&& linearEquationSolver) : SparsePropositionalModelChecker(model), linearEquationSolver(std::move(linearEquationSolver)) { + // Intentionally left empty. + } + + template + bool SparseCtmcCslModelChecker::canHandle(storm::logic::Formula const& formula) const { + // FIXME: refine. + return formula.isCslStateFormula() || formula.isCslPathFormula() || formula.isRewardPathFormula(); + } + + template + std::unique_ptr SparseCtmcCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + STORM_LOG_THROW(pathFormula.isIntervalBounded(), storm::exceptions::InvalidPropertyException, "Cannot treat non-interval bounded until."); + + std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();; + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + std::pair const& intervalBounds = pathFormula.getIntervalBounds(); + std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), intervalBounds.first, intervalBounds.second))); + + return result; + } + + template + std::unique_ptr SparseCtmcCslModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + std::vector result = SparseDtmcPrctlModelChecker::computeNextProbabilitiesHelper(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *this->linearEquationSolver); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); + } + + template + std::unique_ptr SparseCtmcCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + std::vector result = SparseDtmcPrctlModelChecker::computeUntilProbabilitiesHelper(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolver); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); + } + +// template +// std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { +// +// } + + template + storm::models::Ctmc const& SparseCtmcCslModelChecker::getModel() const { + return this->template getModelAs>(); + } + + template + std::vector SparseCtmcCslModelChecker::computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double lowerBound, double upperBound) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "not yet implemented, sorry"); + } + +// template +// std::vector SparseCtmcCslModelChecker::computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const { +// +// } + + } // namespace modelchecker +} // namespace storm \ No newline at end of file diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h new file mode 100644 index 000000000..7c5617a5e --- /dev/null +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -0,0 +1,44 @@ +#ifndef STORM_MODELCHECKER_SPARSECTMCCSLMODELCHECKER_H_ +#define STORM_MODELCHECKER_SPARSECTMCCSLMODELCHECKER_H_ + +#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "src/models/Ctmc.h" +#include "src/solver/LinearEquationSolver.h" + +namespace storm { + namespace modelchecker { + + template + class SparseCtmcCslModelChecker : public SparsePropositionalModelChecker { + public: + explicit SparseCtmcCslModelChecker(storm::models::Ctmc const& model); + explicit SparseCtmcCslModelChecker(storm::models::Ctmc const& model, std::unique_ptr>&& linearEquationSolver); + + // The implemented methods of the AbstractModelChecker interface. + virtual bool canHandle(storm::logic::Formula const& formula) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) 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 computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; +// virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, 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; + + protected: + storm::models::Ctmc const& getModel() const override; + + private: + // The methods that perform the actual checking. + std::vector computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double lowerBound, double upperBound) const; + std::vector computeUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const; +// std::vector computeInstantaneousRewardsHelper(uint_fast64_t stepCount) const; +// std::vector computeCumulativeRewardsHelper(uint_fast64_t stepBound) const; +// std::vector computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const; + + // An object that is used for solving linear equations and performing matrix-vector multiplication. + std::unique_ptr> linearEquationSolver; + }; + + } // namespace modelchecker +} // namespace storm + +#endif /* STORM_MODELCHECKER_SPARSECTMCCSLMODELCHECKER_H_ */ diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 9d12d6166..d3a01be83 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -5,6 +5,7 @@ #include "src/utility/macros.h" #include "src/utility/vector.h" #include "src/utility/graph.h" +#include "src/utility/solver.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -74,14 +75,13 @@ namespace storm { } template - std::vector SparseDtmcPrctlModelChecker::computeNextProbabilitiesHelper(storm::storage::BitVector const& nextStates) { + std::vector SparseDtmcPrctlModelChecker::computeNextProbabilitiesHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolver const& linearEquationSolver) { // Create the vector with which to multiply and initialize it correctly. - std::vector result(this->getModel().getNumberOfStates()); + std::vector result(transitionMatrix.getRowCount()); storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); // Perform one single matrix-vector multiplication. - STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available."); - this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result); + linearEquationSolver.performMatrixVectorMultiplication(transitionMatrix, result); return result; } @@ -89,14 +89,14 @@ namespace storm { std::unique_ptr SparseDtmcPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeNextProbabilitiesHelper(subResult.getTruthValuesVector()))); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeNextProbabilitiesHelper(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *this->linearEquationSolver))); } template - std::vector SparseDtmcPrctlModelChecker::computeUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const { + std::vector SparseDtmcPrctlModelChecker::computeUntilProbabilitiesHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolver const& linearEquationSolver) { // 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(), phiStates, psiStates); + std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); @@ -107,7 +107,7 @@ namespace storm { STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); // Create resulting vector. - std::vector result(this->getModel().getNumberOfStates()); + std::vector result(transitionMatrix.getRowCount()); // Check whether we need to compute exact probabilities for some states. if (qualitative) { @@ -118,7 +118,7 @@ namespace storm { // In this case we have have to compute the probabilities. // We can eliminate the rows and columns from the original transition probability matrix. - storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, true); + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, true); // Converting the matrix from the fixpoint notation to the form needed for the equation // system. That is, we go from x = A*x + b to (I-A)x = b. @@ -131,11 +131,10 @@ namespace storm { // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. - std::vector b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); + std::vector b = transitionMatrix.getConstrainedRowSumVector(maybeStates, statesWithProbability1); // Now solve the created system of linear equations. - STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available."); - this->linearEquationSolver->solveEquationSystem(submatrix, x, b); + linearEquationSolver.solveEquationSystem(submatrix, x, b); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, x); @@ -155,7 +154,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();; ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();; - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative))); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeUntilProbabilitiesHelper(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolver))); } template diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index f7557d63b..9fe58e0f2 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -3,15 +3,18 @@ #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/models/Dtmc.h" -#include "src/utility/solver.h" #include "src/solver/LinearEquationSolver.h" namespace storm { namespace modelchecker { + // Forward-declare CTMC model checker so we can make it a friend. + template class SparseCtmcCslModelChecker; template class SparseDtmcPrctlModelChecker : public SparsePropositionalModelChecker { public: + friend class SparseCtmcCslModelChecker; + explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc const& model); explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc const& model, std::unique_ptr>&& linearEquationSolver); @@ -30,8 +33,8 @@ namespace storm { private: // The methods that perform the actual checking. std::vector computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound) const; - std::vector computeNextProbabilitiesHelper(storm::storage::BitVector const& nextStates); - std::vector computeUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const; + static std::vector computeNextProbabilitiesHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolver const& linearEquationSolver); + static std::vector computeUntilProbabilitiesHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolver const& linearEquationSolver); std::vector computeInstantaneousRewardsHelper(uint_fast64_t stepCount) const; std::vector computeCumulativeRewardsHelper(uint_fast64_t stepBound) const; std::vector computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const; diff --git a/src/utility/cli.h b/src/utility/cli.h index c493c5acd..0486b13e3 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -75,9 +75,6 @@ log4cplus::Logger printer; #include "src/exceptions/InvalidSettingsException.h" #include "src/exceptions/InvalidTypeException.h" -// FIXME: remove this -#include "src/utility/numerical.h" - namespace storm { namespace utility { namespace cli { @@ -510,8 +507,6 @@ namespace storm { initializeFileLogging(); } - auto fgresult = storm::utility::numerical::getFoxGlynnCutoff(500, 1e-300, 1e+300, 1e-6); - std::cout << "left: " << std::get<0>(fgresult) << " and right: " << std::get<1>(fgresult) << std::endl; std::cout << "weight: " << std::get<2>(fgresult) << std::endl; int pos = 0;