From ea507a0b1310b52ad406056dbdab1161f51164c3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 19 Oct 2017 15:09:12 +0200 Subject: [PATCH] added dd-based partial quotient extraction for DTMCs --- .../ExplicitQuantitativeCheckResult.cpp | 6 +- .../results/QuantitativeCheckResult.h | 1 - .../storage/dd/BisimulationDecomposition.h | 2 +- .../bisimulation/PartialQuotientExtractor.cpp | 112 +++++++++-- .../bisimulation/PartialQuotientExtractor.h | 4 +- .../dd/bisimulation/PartitionRefiner.cpp | 5 + .../dd/bisimulation/PartitionRefiner.h | 5 + .../dd/bisimulation/SignatureComputer.h | 6 +- .../SymbolicMdpPrctlModelCheckerTest.cpp | 3 +- .../SymbolicBisimulationDecompositionTest.cpp | 184 ++++++++++++++++++ 10 files changed, 304 insertions(+), 24 deletions(-) diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 5077aa263..ad1f1e296 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -87,7 +87,7 @@ namespace storm { this->values = newMap; } } - + template ValueType ExplicitQuantitativeCheckResult::getMin() const { STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined."); @@ -123,7 +123,7 @@ namespace storm { template ValueType ExplicitQuantitativeCheckResult::sum() const { - STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Sum of empty set is not defined"); ValueType sum = storm::utility::zero(); if (this->isResultForAllStates()) { @@ -142,7 +142,7 @@ namespace storm { template ValueType ExplicitQuantitativeCheckResult::average() const { - STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Average of empty set is not defined"); ValueType sum = storm::utility::zero(); if (this->isResultForAllStates()) { diff --git a/src/storm/modelchecker/results/QuantitativeCheckResult.h b/src/storm/modelchecker/results/QuantitativeCheckResult.h index e0e32fb9a..285f60755 100644 --- a/src/storm/modelchecker/results/QuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/QuantitativeCheckResult.h @@ -15,7 +15,6 @@ namespace storm { virtual ValueType getMin() const = 0; - virtual ValueType getMax() const = 0; virtual ValueType average() const = 0; diff --git a/src/storm/storage/dd/BisimulationDecomposition.h b/src/storm/storage/dd/BisimulationDecomposition.h index d4ddfced4..ef9018f9a 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.h +++ b/src/storm/storage/dd/BisimulationDecomposition.h @@ -52,7 +52,7 @@ namespace storm { * * @return True iff the computation arrived at a fixpoint. */ - bool compute(uint64_t steps, bisimulation::SignatureMode const& mode); + bool compute(uint64_t steps, bisimulation::SignatureMode const& mode = bisimulation::SignatureMode::Eager); /*! * Retrieves the quotient model after the bisimulation decomposition was computed. diff --git a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp index cd179dce3..124c1c077 100644 --- a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp @@ -2,6 +2,9 @@ #include "storm/storage/dd/DdManager.h" +#include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StandardRewardModel.h" + #include "storm/settings/SettingsManager.h" #include "storm/utility/macros.h" @@ -17,17 +20,6 @@ namespace storm { this->quotientFormat = settings.getQuotientFormat(); STORM_LOG_THROW(this->quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Dd, storm::exceptions::NotSupportedException, "Only DD-based partial quotient extraction is currently supported."); - - // We need to create auxiliary variables that encode the nondeterminism arising from partion quotient extraction. - auto& manager = model.getManager(); - uint64_t numberOfDdVariables = 0; - for (auto const& metaVariable : model.getRowVariables()) { - auto const& ddMetaVariable = manager.getMetaVariable(metaVariable); - numberOfDdVariables += ddMetaVariable.getNumberOfDdVariables(); - } - std::vector auxVariables = manager.addBitVectorMetaVariable("quot", numberOfDdVariables, 1); - STORM_LOG_ASSERT(auxVariables.size() == 1, "Expected exactly one meta variable."); - nondeterminismVariable = auxVariables.front(); } template @@ -47,7 +39,103 @@ namespace storm { template std::shared_ptr> PartialQuotientExtractor::extractDdQuotient(Partition const& partition, PreservationInformation const& preservationInformation) { - return nullptr; + + auto modelType = model.getType(); + if (modelType == storm::models::ModelType::Dtmc) { + // Sanity checks. + STORM_LOG_ASSERT(partition.getNumberOfStates() == model.getNumberOfStates(), "Mismatching partition size."); + STORM_LOG_ASSERT(partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()) == model.getReachableStates(), "Mismatching partition."); + + std::set blockVariableSet = {partition.getBlockVariable()}; + std::set blockPrimeVariableSet = {partition.getPrimedBlockVariable()}; + std::vector> blockMetaVariablePairs = {std::make_pair(partition.getBlockVariable(), partition.getPrimedBlockVariable())}; + + storm::dd::Bdd partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero(); + + auto start = std::chrono::high_resolution_clock::now(); + partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); + storm::dd::Bdd reachableStates = partitionAsBdd.existsAbstract(model.getRowVariables()); + storm::dd::Bdd initialStates = (model.getInitialStates() && partitionAsBdd).existsAbstract(model.getRowVariables()); + + std::map> preservedLabelBdds; + for (auto const& label : preservationInformation.getLabels()) { + preservedLabelBdds.emplace(label, (model.getStates(label) && partitionAsBdd).existsAbstract(model.getRowVariables())); + } + for (auto const& expression : preservationInformation.getExpressions()) { + std::stringstream stream; + stream << expression; + std::string expressionAsString = stream.str(); + + auto it = preservedLabelBdds.find(expressionAsString); + if (it != preservedLabelBdds.end()) { + STORM_LOG_WARN("Duplicate label '" << expressionAsString << "', dropping second label definition."); + } else { + preservedLabelBdds.emplace(stream.str(), (model.getStates(expression) && partitionAsBdd).existsAbstract(model.getRowVariables())); + } + } + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + + start = std::chrono::high_resolution_clock::now(); + std::set blockAndRowVariables; + std::set_union(blockVariableSet.begin(), blockVariableSet.end(), model.getRowVariables().begin(), model.getRowVariables().end(), std::inserter(blockAndRowVariables, blockAndRowVariables.end())); + std::set blockPrimeAndColumnVariables; + std::set_union(blockPrimeVariableSet.begin(), blockPrimeVariableSet.end(), model.getColumnVariables().begin(), model.getColumnVariables().end(), std::inserter(blockPrimeAndColumnVariables, blockPrimeAndColumnVariables.end())); + storm::dd::Add partitionAsAdd = partitionAsBdd.template toAdd(); + storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables()); + +// // Pick a representative from each block. +// auto representatives = InternalRepresentativeComputer(partitionAsBdd, model.getRowVariables()).getRepresentatives(); +// partitionAsBdd &= representatives; +// partitionAsAdd *= partitionAsBdd.template toAdd(); + +// quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()); + quotientTransitionMatrix = quotientTransitionMatrix * partitionAsAdd; + end = std::chrono::high_resolution_clock::now(); + + // Check quotient matrix for sanity. + if (std::is_same::value) { + STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one()).isZero(), "Illegal entries in quotient matrix."); + } else { + STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one() + storm::utility::convertNumber(1e-6)).isZero(), "Illegal entries in quotient matrix."); + } + + STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + + storm::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); + storm::dd::Bdd deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates; + + start = std::chrono::high_resolution_clock::now(); + std::unordered_map> quotientRewardModels; + for (auto const& rewardModelName : preservationInformation.getRewardModelNames()) { + auto const& rewardModel = model.getRewardModel(rewardModelName); + + boost::optional> quotientStateRewards; + if (rewardModel.hasStateRewards()) { + quotientStateRewards = rewardModel.getStateRewardVector() * partitionAsAdd; + } + + boost::optional> quotientStateActionRewards; + if (rewardModel.hasStateActionRewards()) { + quotientStateActionRewards = rewardModel.getStateActionRewardVector() * partitionAsAdd; + } + + quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel(quotientStateRewards, quotientStateActionRewards, boost::none)); + } + end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + + std::set newNondeterminismVariables = model.getNondeterminismVariables(); + newNondeterminismVariables.insert(model.getRowVariables().begin(), model.getRowVariables().end()); + + if (modelType == storm::models::ModelType::Dtmc) { + return std::shared_ptr>(new storm::models::symbolic::Mdp(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, newNondeterminismVariables, preservedLabelBdds, quotientRewardModels)); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unsupported quotient type."); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract partial quotient for this model type."); + } } template class PartialQuotientExtractor; diff --git a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h index 92ab45ffb..ca32a8dbf 100644 --- a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h +++ b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h @@ -28,9 +28,7 @@ namespace storm { // The model for which to compute the partial quotient. storm::models::symbolic::Model const& model; - - storm::expressions::Variable nondeterminismVariable; - + storm::settings::modules::BisimulationSettings::QuotientFormat quotientFormat; }; diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index 6f587ad36..fdec559d8 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -123,6 +123,11 @@ namespace storm { return statePartition; } + template + Signature PartitionRefiner::getFullSignature() const { + return signatureComputer.getFullSignature(statePartition); + } + template Status PartitionRefiner::getStatus() const { return status; diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.h b/src/storm/storage/dd/bisimulation/PartitionRefiner.h index c3398e826..d4e59a207 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.h @@ -43,6 +43,11 @@ namespace storm { */ Partition const& getStatePartition() const; + /*! + * Retrieves the full signature of all states wrt. the current state partition. + */ + Signature getFullSignature() const; + /*! * Retrieves the status of the refinement process. */ diff --git a/src/storm/storage/dd/bisimulation/SignatureComputer.h b/src/storm/storage/dd/bisimulation/SignatureComputer.h index 421acc90a..0f347bc2f 100644 --- a/src/storm/storage/dd/bisimulation/SignatureComputer.h +++ b/src/storm/storage/dd/bisimulation/SignatureComputer.h @@ -50,12 +50,12 @@ namespace storm { void setSignatureMode(SignatureMode const& newMode); SignatureIterator compute(Partition const& partition); - - private: + /// Methods to compute the signatures. Signature getFullSignature(Partition const& partition) const; Signature getQualitativeSignature(Partition const& partition) const; - + + private: bool qualitativeTransitionMatrixIsBdd() const; storm::dd::Bdd const& getQualitativeTransitionMatrixAsBdd() const; storm::dd::Add const& getQualitativeTransitionMatrixAsAdd() const; diff --git a/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index ebeb02282..249de13d9 100644 --- a/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -2,12 +2,13 @@ #include "storm-config.h" #include "storm/logic/Formulas.h" +#include "storm/parser/FormulaParser.h" + #include "storm/utility/solver.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "storm/parser/FormulaParser.h" #include "storm/parser/PrismParser.h" #include "storm/builder/DdPrismModelBuilder.h" #include "storm/models/symbolic/Dtmc.h" diff --git a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp index 402410933..8bb43f73c 100644 --- a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp +++ b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp @@ -9,9 +9,22 @@ #include "storm/storage/dd/BisimulationDecomposition.h" #include "storm/storage/SymbolicModelDescription.h" +#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" +#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" +#include "storm/modelchecker/results/CheckResult.h" +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "storm/modelchecker/results/QuantitativeCheckResult.h" + +#include "storm/solver/SymbolicLinearEquationSolver.h" +#include "storm/solver/SymbolicMinMaxLinearEquationSolver.h" + +#include "storm/logic/Formulas.h" +#include "storm/parser/FormulaParser.h" + #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Mdp.h" #include "storm/models/symbolic/StandardRewardModel.h" @@ -51,7 +64,88 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Cudd) { std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); storm::dd::BisimulationDecomposition decomposition(*model, storm::storage::BisimulationType::Strong); + std::shared_ptr> quotient = decomposition.getQuotient(); + ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType()); + ASSERT_TRUE(quotient->isSymbolicModel()); + + std::shared_ptr> quotientMdp = quotient->as>(); + + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*quotientMdp, std::make_unique>()); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr minFormula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"one\"]"); + std::shared_ptr maxFormula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"one\"]"); + + std::pair resultBounds; + + std::unique_ptr result = checker.check(*minFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); + resultBounds.first = result->asQuantitativeCheckResult().sum(); + result = checker.check(*maxFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); + resultBounds.second = result->asQuantitativeCheckResult().sum(); + + EXPECT_EQ(resultBounds.first, storm::utility::zero()); + EXPECT_EQ(resultBounds.second, storm::utility::one()); + + // Perform only one step. + decomposition.compute(1); + + quotient = decomposition.getQuotient(); + ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType()); + ASSERT_TRUE(quotient->isSymbolicModel()); + quotientMdp = quotient->as>(); + + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker2(*quotientMdp, std::make_unique>()); + + result = checker2.check(*minFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); + resultBounds.first = result->asQuantitativeCheckResult().sum(); + result = checker2.check(*maxFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); + resultBounds.second = result->asQuantitativeCheckResult().sum(); + + EXPECT_EQ(resultBounds.first, storm::utility::zero()); + EXPECT_NEAR(resultBounds.second, static_cast(1)/3, 1e-6); + + // Perform only one step. + decomposition.compute(1); + + quotient = decomposition.getQuotient(); + ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType()); + ASSERT_TRUE(quotient->isSymbolicModel()); + quotientMdp = quotient->as>(); + + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker3(*quotientMdp, std::make_unique>()); + + result = checker3.check(*minFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); + resultBounds.first = result->asQuantitativeCheckResult().sum(); + result = checker3.check(*maxFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); + resultBounds.second = result->asQuantitativeCheckResult().sum(); + + EXPECT_NEAR(resultBounds.first, static_cast(1)/6, 1e-6); + EXPECT_NEAR(resultBounds.second, static_cast(1)/6, 1e-6); + EXPECT_NEAR(resultBounds.first, resultBounds.second, 1e-6); + + decomposition.compute(1); + + quotient = decomposition.getQuotient(); + ASSERT_EQ(storm::models::ModelType::Dtmc, quotient->getType()); + ASSERT_TRUE(quotient->isSymbolicModel()); + std::shared_ptr> quotientDtmc = quotient->as>(); + + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker4(*quotientDtmc); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + + result = checker4.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientDtmc->getReachableStates(), quotientDtmc->getInitialStates())); + resultBounds.first = resultBounds.second = result->asQuantitativeCheckResult().sum(); + + EXPECT_NEAR(resultBounds.first, static_cast(1)/6, 1e-6); } TEST(SymbolicModelBisimulationDecomposition, Die_Sylvan) { @@ -84,6 +178,96 @@ TEST(SymbolicModelBisimulationDecomposition, Die_Sylvan) { EXPECT_TRUE(quotient->isSymbolicModel()); } +TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Sylvan) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); + + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); + + storm::dd::BisimulationDecomposition decomposition(*model, storm::storage::BisimulationType::Strong); + + std::shared_ptr> quotient = decomposition.getQuotient(); + ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType()); + ASSERT_TRUE(quotient->isSymbolicModel()); + + std::shared_ptr> quotientMdp = quotient->as>(); + + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*quotientMdp, std::make_unique>()); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr minFormula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"one\"]"); + std::shared_ptr maxFormula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"one\"]"); + + std::pair resultBounds; + + std::unique_ptr result = checker.check(*minFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); + resultBounds.first = result->asQuantitativeCheckResult().sum(); + result = checker.check(*maxFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); + resultBounds.second = result->asQuantitativeCheckResult().sum(); + + EXPECT_EQ(resultBounds.first, storm::utility::zero()); + EXPECT_EQ(resultBounds.second, storm::utility::one()); + + // Perform only one step. + decomposition.compute(1); + + quotient = decomposition.getQuotient(); + ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType()); + ASSERT_TRUE(quotient->isSymbolicModel()); + quotientMdp = quotient->as>(); + + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker2(*quotientMdp, std::make_unique>()); + + result = checker2.check(*minFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); + resultBounds.first = result->asQuantitativeCheckResult().sum(); + result = checker2.check(*maxFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); + resultBounds.second = result->asQuantitativeCheckResult().sum(); + + EXPECT_EQ(resultBounds.first, storm::utility::zero()); + EXPECT_NEAR(resultBounds.second, static_cast(1)/3, 1e-6); + + // Perform only one step. + decomposition.compute(1); + + quotient = decomposition.getQuotient(); + ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType()); + ASSERT_TRUE(quotient->isSymbolicModel()); + quotientMdp = quotient->as>(); + + storm::modelchecker::SymbolicMdpPrctlModelChecker> checker3(*quotientMdp, std::make_unique>()); + + result = checker3.check(*minFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); + resultBounds.first = result->asQuantitativeCheckResult().sum(); + result = checker3.check(*maxFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientMdp->getReachableStates(), quotientMdp->getInitialStates())); + resultBounds.second = result->asQuantitativeCheckResult().sum(); + + EXPECT_NEAR(resultBounds.first, static_cast(1)/6, 1e-6); + EXPECT_NEAR(resultBounds.second, static_cast(1)/6, 1e-6); + EXPECT_NEAR(resultBounds.first, resultBounds.second, 1e-6); + + decomposition.compute(1); + + quotient = decomposition.getQuotient(); + ASSERT_EQ(storm::models::ModelType::Dtmc, quotient->getType()); + ASSERT_TRUE(quotient->isSymbolicModel()); + std::shared_ptr> quotientDtmc = quotient->as>(); + + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker4(*quotientDtmc); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + + result = checker4.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(quotientDtmc->getReachableStates(), quotientDtmc->getInitialStates())); + resultBounds.first = resultBounds.second = result->asQuantitativeCheckResult().sum(); + + EXPECT_NEAR(resultBounds.first, static_cast(1)/6, 1e-6); +} + TEST(SymbolicModelBisimulationDecomposition, Crowds_Cudd) { storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds5_5.pm");