From 2096c54b84b619f6e102ecf6d21284ac8ef57934 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 19 Jun 2016 23:20:05 +0200 Subject: [PATCH] more explicit instantiations for rational function and some more tests for eigen solver Former-commit-id: b97e838b22a01d5b54e2fa6f37f5f98e23cd36dc --- .../csl/helper/SparseCtmcCslHelper.cpp | 7 +- .../prctl/SparseDtmcPrctlModelChecker.cpp | 1 + .../prctl/helper/SparseDtmcPrctlHelper.cpp | 1 + src/storage/SparseMatrix.cpp | 12 ++- src/utility/solver.cpp | 2 + .../EigenDtmcPrctlModelCheckerTest.cpp | 94 +++++++++++++++++++ 6 files changed, 113 insertions(+), 4 deletions(-) diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index b4c01d13a..c9ee33622 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -445,7 +445,7 @@ namespace storm { } // Start by decomposing the DTMC into its BSCCs. - storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(probabilityMatrix, storm::storage::BitVector(probabilityMatrix.getRowCount(), true), false, true); + storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(probabilityMatrix, storm::storage::BitVector(probabilityMatrix.getRowCount(), true), false, true); STORM_LOG_DEBUG("Found " << bsccDecomposition.size() << " BSCCs."); @@ -593,7 +593,7 @@ namespace storm { // At this point, all BSCCs are known to contain exactly one state, which is why we can set all values // directly (based on whether or not the contained state is a psi state). if (psiStates.get(*bscc.begin())) { - bsccLra[bsccIndex] = 1; + bsccLra[bsccIndex] = storm::utility::one(); } } @@ -701,10 +701,11 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - + #ifdef STORM_HAVE_CARL template std::vector SparseCtmcCslHelper::computeUntilProbabilitiesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); template std::vector SparseCtmcCslHelper::computeReachabilityTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); #endif } } diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index d110f067d..bf8ea19ff 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -146,5 +146,6 @@ namespace storm { } template class SparseDtmcPrctlModelChecker>; + template class SparseDtmcPrctlModelChecker>; } } \ No newline at end of file diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 891acda3f..22d80d46a 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -401,6 +401,7 @@ namespace storm { } template class SparseDtmcPrctlHelper; + template class SparseDtmcPrctlHelper; } } } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index bfed8f49c..c84b03cef 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -1018,6 +1018,11 @@ namespace storm { typename std::pair, std::vector> SparseMatrix::getJacobiDecomposition() const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported."); } + + template<> + typename std::pair, std::vector> SparseMatrix::getJacobiDecomposition() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported."); + } #endif template @@ -1144,6 +1149,11 @@ namespace storm { } } + template<> + void SparseMatrix::performSuccessiveOverRelaxationStep(Interval omega, std::vector& x, std::vector const& b) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported."); + } + template void SparseMatrix::multiplyVectorWithMatrix(std::vector const& vector, std::vector& result) const { const_iterator it = this->begin(); @@ -1457,7 +1467,7 @@ namespace storm { template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; #ifdef STORM_HAVE_CARL - // Rat Function + // Rat Number template class MatrixEntry::index_type, RationalNumber>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 58ef940f7..92f2b8e94 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -215,6 +215,8 @@ namespace storm { template class NativeLinearEquationSolverFactory; template class MinMaxLinearEquationSolverFactory; template class GameSolverFactory; + + template class EigenLinearEquationSolverFactory; } } } diff --git a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp index 0a339713b..f8b262e2d 100644 --- a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp @@ -60,6 +60,100 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(11.0 / 3.0, quantitativeResult4[0], storm::settings::getModule().getPrecision()); } +TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) { + // FIXME: this should use rational numbers not functions. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); + + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + + std::unique_ptr result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult1[0]); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult2[0]); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult3[0]); + + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_EQ(storm::RationalFunction(11) / storm::RationalFunction(3), quantitativeResult4[0]); +} + +TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) { + // FIXME: this should use rational numbers not functions. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/parametric_die.pm"); + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); + + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::make_unique>()); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + + std::unique_ptr result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + std::cout << quantitativeResult1 << std::endl; +// EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult1[0]); +// +// formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); +// +// result = checker.check(*formula); +// storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); +// +// EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult2[0]); +// +// formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); +// +// result = checker.check(*formula); +// storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); +// +// EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult3[0]); +// +// formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); +// +// result = checker.check(*formula); +// storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); +// +// EXPECT_EQ(storm::RationalFunction(11) / storm::RationalFunction(3), quantitativeResult4[0]); +} + + TEST(EigenDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", "");