From 2bf7eafb4bfcf982986e42803ca364b86a44e67f Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 10 Apr 2015 20:37:57 +0200 Subject: [PATCH] Further work on hybrid MDP model checker. Former-commit-id: 3192a13f55eedf309d59f75cc3e00cd8f23acd13 --- .../prctl/HybridMdpPrctlModelChecker.cpp | 18 +- src/storage/dd/CuddAdd.cpp | 28 +- src/storage/dd/CuddAdd.h | 4 +- ....cpp => NativeCtmcCslModelCheckerTest.cpp} | 0 ...pp => NativeDtmcPrctlModelCheckerTest.cpp} | 0 .../NativeHybridCtmcCslModelCheckerTest.cpp | 279 ++++++++++++++++++ .../NativeHybridDtmcPrctlModelCheckerTest.cpp | 165 +++++++++++ .../NativeHybridMdpPrctlModelCheckerTest.cpp | 184 ++++++++++++ ...cpp => NativeMdpPrctlModelCheckerTest.cpp} | 0 9 files changed, 645 insertions(+), 33 deletions(-) rename test/functional/modelchecker/{SparseCtmcCslModelCheckerTest.cpp => NativeCtmcCslModelCheckerTest.cpp} (100%) rename test/functional/modelchecker/{SparseDtmcPrctlModelCheckerTest.cpp => NativeDtmcPrctlModelCheckerTest.cpp} (100%) create mode 100644 test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp create mode 100644 test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp create mode 100644 test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp rename test/functional/modelchecker/{SparseMdpPrctlModelCheckerTest.cpp => NativeMdpPrctlModelCheckerTest.cpp} (100%) diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 9f1c263f4..0893a8ac4 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -73,14 +73,13 @@ namespace storm { // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed // for solving the equation system (i.e. compute (I-A)). submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); - submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; // Create the solution vector. std::vector x(maybeStates.getNonZeroCount(), ValueType(0.5)); // Translate the symbolic matrix/vector to their explicit representations and solve the equation system. storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); - std::vector b = subvector.template toVector(odd); + std::vector b = subvector.template toVector(model.getNondeterminismVariables(), odd, explicitSubmatrix.getRowGroupIndices()); std::unique_ptr> solver = linearEquationSolverFactory.create(explicitSubmatrix); solver->solveEquationSystem(minimize, x, b); @@ -165,7 +164,7 @@ namespace storm { // Translate the symbolic matrix/vector to their explicit representations. storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); - std::vector b = subvector.template toVector(odd); + std::vector b = subvector.template toVector(model.getNondeterminismVariables(), odd, explicitSubmatrix.getRowGroupIndices()); std::unique_ptr> solver = linearEquationSolverFactory.create(explicitSubmatrix); solver->performMatrixVectorMultiplication(minimize, x, &b, stepBound); @@ -203,7 +202,7 @@ namespace storm { // Translate the symbolic matrix/vector to their explicit representations. storm::storage::SparseMatrix explicitMatrix = transitionMatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); - std::vector b = totalRewardVector.template toVector(odd); + std::vector b = totalRewardVector.template toVector(model.getNondeterminismVariables(), odd, explicitMatrix.getRowGroupIndices()); // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(explicitMatrix); @@ -227,12 +226,12 @@ namespace storm { // Create the ODD for the translation between symbolic and explicit storage. storm::dd::Odd odd(model.getReachableStates()); - - // Create the solution vector (and initialize it to the state rewards of the model). - std::vector x = model.getStateRewardVector().template toVector(odd); - + // Translate the symbolic matrix to its explicit representations. storm::storage::SparseMatrix explicitMatrix = transitionMatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); + + // Create the solution vector (and initialize it to the state rewards of the model). + std::vector x = model.getStateRewardVector().template toVector(model.getNondeterminismVariables(), odd, explicitMatrix.getRowGroupIndices()); // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(explicitMatrix); @@ -297,14 +296,13 @@ namespace storm { // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed // for solving the equation system (i.e. compute (I-A)). submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); - submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; // Create the solution vector. std::vector x(maybeStates.getNonZeroCount(), ValueType(0.5)); // Translate the symbolic matrix/vector to their explicit representations. storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); - std::vector b = subvector.template toVector(odd); + std::vector b = subvector.template toVector(model.getNondeterminismVariables(), odd, explicitSubmatrix.getRowGroupIndices()); // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(explicitSubmatrix); diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp index 2bc170615..1dbf60803 100644 --- a/src/storage/dd/CuddAdd.cpp +++ b/src/storage/dd/CuddAdd.cpp @@ -429,7 +429,7 @@ namespace storm { } template - std::vector Add::toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd) const { + std::vector Add::toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector groupOffsets) const { std::set rowMetaVariables; // Prepare the proper sets of meta variables. @@ -455,30 +455,14 @@ namespace storm { } } - // Start by computing the offsets (in terms of rows) for each row group. - Add stateToNumberOfChoices = this->notZero().toAdd().sumAbstract(groupMetaVariables); - std::vector rowGroupIndices = stateToNumberOfChoices.toVector(rowOdd); - rowGroupIndices.resize(rowGroupIndices.size() + 1); - uint_fast64_t tmp = 0; - uint_fast64_t tmp2 = 0; - for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { - tmp2 = rowGroupIndices[i]; - rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowGroupIndices[0] = 0; - - // Then split the symbolic vector into groups. + // Start by splitting the symbolic vector into groups. std::vector> groups; splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowMetaVariables); // Now iterate over the groups and add them to the resulting vector. - std::vector result(rowGroupIndices.back(), storm::utility::zero()); + std::vector result(groupOffsets.back(), storm::utility::zero()); for (uint_fast64_t i = 0; i < groups.size(); ++i) { - auto const& dd = groups[i]; - - toVectorRec(dd.getCuddDdNode(), result, rowGroupIndices, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); - addToVectorRec(dd.notZero().toAdd().getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); + toVectorRec(groups[i].getCuddDdNode(), result, groupOffsets, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); } return result; @@ -702,7 +686,7 @@ namespace storm { } template - void Add::toVectorRec(DdNode const* dd, std::vector& result, std::vector& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) { + void Add::toVectorRec(DdNode const* dd, std::vector& result, std::vector& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const { // For the empty DD, we do not need to add any entries. if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { return; @@ -927,6 +911,8 @@ namespace storm { template std::vector Add::toVector() const; template std::vector Add::toVector(Odd const& rowOdd) const; template void Add::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + template std::vector Add::toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector groupOffsets) const; + template void Add::toVectorRec(DdNode const* dd, std::vector& result, std::vector& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const; template std::vector Add::toVector() const; template std::vector Add::toVector(Odd const& rowOdd) const; template void Add::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; diff --git a/src/storage/dd/CuddAdd.h b/src/storage/dd/CuddAdd.h index 78e29eb4f..6b91e514b 100644 --- a/src/storage/dd/CuddAdd.h +++ b/src/storage/dd/CuddAdd.h @@ -537,7 +537,7 @@ namespace storm { * @return The vector that is represented by this ADD. */ template - std::vector toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd) const; + std::vector toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector groupOffsets) const; /*! * Converts the ADD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the @@ -698,7 +698,7 @@ namespace storm { * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. */ template - void toVectorRec(DdNode const* dd, std::vector& result, std::vector& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices); + void toVectorRec(DdNode const* dd, std::vector& result, std::vector& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const; /*! * Splits the given matrix DD into the groups using the given group variables. diff --git a/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp similarity index 100% rename from test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp rename to test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp diff --git a/test/functional/modelchecker/SparseDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp similarity index 100% rename from test/functional/modelchecker/SparseDtmcPrctlModelCheckerTest.cpp rename to test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp new file mode 100644 index 000000000..ab90e8960 --- /dev/null +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -0,0 +1,279 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/settings/SettingMemento.h" +#include "src/parser/PrismParser.h" +#include "src/parser/FormulaParser.h" +#include "src/logic/Formulas.h" +#include "src/builder/DdPrismModelBuilder.h" +#include "src/storage/dd/DdType.h" + +#include "src/utility/solver.h" +#include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" +#include "src/modelchecker/results/HybridQuantitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" + +#include "src/settings/SettingsManager.h" + +TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { + // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. + std::unique_ptr enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true); + + // Parse the model description. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + std::shared_ptr formula(nullptr); + + // Build the model. + typename storm::builder::DdPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "num_repairs"; + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); + std::shared_ptr> ctmc = model->as>(); + + // Create model checker. + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + + // Start checking properties. + formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]"); + std::unique_ptr checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ F[100,100] !\"minimum\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ F[100,2000] !\"minimum\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("R=? [C<=100]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + 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()); +} + +TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) { + // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. + std::unique_ptr enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true); + + // Parse the model description. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + std::shared_ptr formula(nullptr); + + // Build the model. + typename storm::builder::DdPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "up"; + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); + std::shared_ptr> ctmc = model->as>(); + + // Create model checker. + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + + // Start checking properties. + formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]"); + std::unique_ptr checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("R=? [C<=10000]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + 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()); +} + +TEST(NativeHybridCtmcCslModelCheckerTest, Polling) { + // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. + std::unique_ptr enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true); + + // Parse the model description. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + std::shared_ptr formula(nullptr); + + // Build the model. + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); + ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); + std::shared_ptr> ctmc = model->as>(); + + // Create model checker. + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + + // Start checking properties. + formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]"); + std::unique_ptr checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(1, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(1, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); +} + +TEST(NativeHybridCtmcCslModelCheckerTest, Fms) { + // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. + std::unique_ptr enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true); + + // No properties to check at this point. +} + +TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { + // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. + std::unique_ptr enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true); + + // Parse the model description. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + std::shared_ptr formula(nullptr); + + // Build the model with the customers reward structure. + typename storm::builder::DdPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "customers"; + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); + std::shared_ptr> ctmc = model->as>(); + + // Create model checker. + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + + // Start checking properties. + formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]"); + std::unique_ptr checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ F<=10 \"first_queue_full\" ]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(1, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(1, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("R=? [I=10]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("R=? [C<=10]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); + checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult(); + EXPECT_NEAR(262.78571505691389, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(262.78571505691389, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision()); +} diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..8cd46bcb1 --- /dev/null +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -0,0 +1,165 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/logic/Formulas.h" +#include "src/utility/solver.h" +#include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" +#include "src/modelchecker/results/HybridQuantitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/parser/PrismParser.h" +#include "src/builder/DdPrismModelBuilder.h" +#include "src/models/symbolic/Dtmc.h" +#include "src/settings/SettingsManager.h" + +TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + + // Build the die model with its reward model. + typename storm::builder::DdPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "coin_flips"; + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(13, model->getNumberOfStates()); + EXPECT_EQ(20, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("one"); + auto eventuallyFormula = std::make_shared(labelFormula); + + std::unique_ptr result = checker.check(*eventuallyFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("two"); + eventuallyFormula = std::make_shared(labelFormula); + + result = checker.check(*eventuallyFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("three"); + eventuallyFormula = std::make_shared(labelFormula); + + result = checker.check(*eventuallyFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + auto done = std::make_shared("done"); + auto reachabilityRewardFormula = std::make_shared(done); + + result = checker.check(*reachabilityRewardFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); +} + +TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(8607, model->getNumberOfStates()); + EXPECT_EQ(15113, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("observe0Greater1"); + auto eventuallyFormula = std::make_shared(labelFormula); + + std::unique_ptr result = checker.check(*eventuallyFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("observeIGreater1"); + eventuallyFormula = std::make_shared(labelFormula); + + result = checker.check(*eventuallyFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("observeOnlyTrueSender"); + eventuallyFormula = std::make_shared(labelFormula); + + result = checker.check(*eventuallyFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.32153900158185761, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.32153900158185761, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); +} + +TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + + // Build the die model with its reward model. + typename storm::builder::DdPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "num_rounds"; + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(273, model->getNumberOfStates()); + EXPECT_EQ(397, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("elected"); + auto eventuallyFormula = std::make_shared(labelFormula); + + std::unique_ptr result = checker.check(*eventuallyFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("elected"); + auto trueFormula = std::make_shared(true); + auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 20); + + result = checker.check(*boundedUntilFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("elected"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); + + result = checker.check(*reachabilityRewardFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); +} + diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..ccc9ed7e3 --- /dev/null +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,184 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/logic/Formulas.h" +#include "src/utility/solver.h" +#include "src/modelchecker/prctl/HybridMdpPrctlModelChecker.h" +#include "src/modelchecker/results/HybridQuantitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/parser/PrismParser.h" +#include "src/builder/DdPrismModelBuilder.h" +#include "src/models/symbolic/Dtmc.h" +#include "src/settings/SettingsManager.h" + +TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + + // Build the die model with its reward model. + typename storm::builder::DdPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "coinflips"; + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(169, model->getNumberOfStates()); + EXPECT_EQ(436, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("two"); + auto eventuallyFormula = std::make_shared(labelFormula); + auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("three"); + eventuallyFormula = std::make_shared(labelFormula); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + result = checker.check(*minProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("four"); + eventuallyFormula = std::make_shared(labelFormula); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + result = checker.check(*minProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("done"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); + auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = checker.check(*minRewardOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(7.333329499, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(7.333329499, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = checker.check(*maxRewardOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult8 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(7.333329499, quantitativeResult8.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(7.333329499, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} + +TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + + // Build the die model with its reward model. + typename storm::builder::DdPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "rounds"; + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(169, model->getNumberOfStates()); + EXPECT_EQ(436, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("elected"); + auto eventuallyFormula = std::make_shared(labelFormula); + auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("elected"); + auto trueFormula = std::make_shared(true); + auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 25); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); + + result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("elected"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); + auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = checker.check(*minRewardOperatorFormula); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(4.285689611, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(4.285689611, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = checker.check(*maxRewardOperatorFormula); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(4.285689611, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(4.285689611, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp similarity index 100% rename from test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp rename to test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp