diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index e1dd96467..9b6818884 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -498,6 +498,8 @@ namespace storm { // Start by decomposing the DTMC into its BSCCs. storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowCount(), true), false, true); + STORM_LOG_DEBUG("Found " << bsccDecomposition.size() << " BSCCs."); + // Get some data members for convenience. ValueType one = storm::utility::one(); ValueType zero = storm::utility::zero(); @@ -524,6 +526,8 @@ namespace storm { } storm::storage::BitVector statesNotInBsccs = ~statesInBsccs; + STORM_LOG_DEBUG("Found " << statesInBsccs.getNumberOfSetBits() << " states in BSCCs."); + // Prepare a vector holding the index within all states that are in BSCCs for every state. std::vector indexInStatesInBsccs; @@ -629,6 +633,10 @@ namespace storm { } } } + + for (uint_fast64_t bsccIndex = 0; bsccIndex < bsccDecomposition.size(); ++bsccIndex) { + STORM_LOG_DEBUG("Found LRA " << bsccLra[bsccIndex] << " for BSCC " << bsccIndex << "."); + } } else { for (uint_fast64_t bsccIndex = 0; bsccIndex < bsccDecomposition.size(); ++bsccIndex) { storm::storage::StronglyConnectedComponent const& bscc = bsccDecomposition[bsccIndex]; @@ -639,6 +647,10 @@ namespace storm { bsccLra[bsccIndex] = 1; } } + + for (uint_fast64_t bsccIndex = 0; bsccIndex < bsccDecomposition.size(); ++bsccIndex) { + STORM_LOG_DEBUG("Found LRA " << bsccLra[bsccIndex] << " for BSCC " << bsccIndex << "."); + } } std::vector rewardSolution; diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 25a02adff..3b61ded53 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -1,4 +1,5 @@ #include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" +#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/storage/dd/CuddOdd.h" @@ -301,6 +302,20 @@ namespace storm { return this->template getModelAs>(); } + template + std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr subResultPointer = this->check(stateFormula); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + + // Create ODD for the translation. + storm::dd::Odd odd(this->getModel().getReachableStates()); + + storm::storage::SparseMatrix explicitProbabilityMatrix = this->getModel().getTransitionMatrix().toMatrix(odd, odd); + + std::vector result = SparseDtmcPrctlModelChecker::computeLongRunAverageHelper(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), qualitative, *this->linearEquationSolverFactory); + return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().getAddZero(), this->getModel().getReachableStates(), std::move(odd), std::move(result))); + } + template class HybridDtmcPrctlModelChecker; } } \ No newline at end of file diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index b3ab51279..8964d29d7 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -26,6 +26,7 @@ namespace storm { 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; + virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; protected: storm::models::symbolic::Dtmc const& getModel() const override; diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 8c15f0bd8..d49075faa 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -303,12 +303,17 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeReachabilityRewardsHelper(this->getModel().getTransitionMatrix(), this->getModel().getOptionalStateRewardVector(), this->getModel().getOptionalTransitionRewardMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *this->linearEquationSolverFactory, qualitative))); } + template + std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr subResultPointer = this->check(stateFormula); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + + return std::unique_ptr(new ExplicitQuantitativeCheckResult(computeLongRunAverageHelper(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory))); + } + template - std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { - std::unique_ptr subResultPointer = this->check(stateFormula); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - - return std::unique_ptr(new ExplicitQuantitativeCheckResult(SparseCtmcCslModelChecker::computeLongRunAverageHelper(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, qualitative, *linearEquationSolverFactory))); + std::vector SparseDtmcPrctlModelChecker::computeLongRunAverageHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + return SparseCtmcCslModelChecker::computeLongRunAverageHelper(transitionMatrix, psiStates, nullptr, qualitative, linearEquationSolverFactory); } template diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 5409091fd..d37023948 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -9,12 +9,16 @@ namespace storm { namespace modelchecker { + template + class HybridDtmcPrctlModelChecker; + // Forward-declare CTMC model checker so we can make it a friend. template class SparseCtmcCslModelChecker; template class SparseDtmcPrctlModelChecker : public SparsePropositionalModelChecker { public: + friend class HybridDtmcPrctlModelChecker; friend class SparseCtmcCslModelChecker; explicit SparseDtmcPrctlModelChecker(storm::models::sparse::Dtmc const& model); @@ -41,7 +45,7 @@ namespace storm { std::vector computeInstantaneousRewardsHelper(uint_fast64_t stepCount) const; std::vector computeCumulativeRewardsHelper(uint_fast64_t stepBound) const; static std::vector computeReachabilityRewardsHelper(storm::storage::SparseMatrix const& transitionMatrix, boost::optional> const& stateRewardVector, boost::optional> const& transitionRewardMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, bool qualitative); - static std::vector computeLongRunAverageHelper(storm::models::sparse::DeterministicModel const& model, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeLongRunAverageHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); // An object that is used for retrieving linear equation solvers. std::unique_ptr> linearEquationSolverFactory; diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index dc3d7a5c7..80300f1f4 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -190,6 +190,13 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) { ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("LRA=?[\"target\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision()); } TEST(GmmxxCtmcCslModelCheckerTest, Fms) { diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index 968a9476b..a720507a4 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -102,6 +102,14 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("LRA=? [\"minimum\"]"); + checkResult = modelchecker.check(*formula); + + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult8 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(0.99999766034263426, quantitativeCheckResult8.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.99999766034263426, quantitativeCheckResult8.getMax(), storm::settings::generalSettings().getPrecision()); } TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { @@ -173,6 +181,14 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("LRA=? [\"fail_sensors\"]"); + checkResult = modelchecker.check(*formula); + + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(0.934586179, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.934586179, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision()); } TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling) { @@ -201,6 +217,15 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling) { storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("LRA=? [\"target\"]"); + checkResult = modelchecker.check(*formula); + + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.20079750055570736, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); + } TEST(GmmxxHybridCtmcCslModelCheckerTest, Fms) { @@ -288,4 +313,12 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("LRA=? [\"first_queue_full\"]"); + checkResult = modelchecker.check(*formula); + + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMax(), storm::settings::generalSettings().getPrecision()); }