diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index e7fb71382..b6483b306 100644 --- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -143,54 +143,83 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(3172ull, mdp->getNumberOfStates()); ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - auto labelFormula = std::make_shared("elected"); - auto eventuallyFormula = std::make_shared(labelFormula); - auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + 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::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); - - result = checker.check(*maxProbabilityOperatorFormula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - + auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(1, quantitativeResult2[0], 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::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - + 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::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); - - result = checker.check(*maxProbabilityOperatorFormula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.0625, quantitativeResult4[0], 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); + 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::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - result = checker.check(*minRewardOperatorFormula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = checker.check(*maxRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - result = checker.check(*maxRewardOperatorFormula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); } + +TEST(SparseMdpPrctlModelCheckerTest, LRA) { + storm::storage::SparseMatrixBuilder matrixBuilder; + std::shared_ptr> mdp; + + { + matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); + matrixBuilder.addNextValue(0, 1, 1.); + matrixBuilder.addNextValue(1, 0, 1.); + storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); + + storm::models::AtomicPropositionsLabeling ap(2, 1); + ap.addAtomicProposition("a"); + ap.addAtomicPropositionToState("a", 1); + + mdp.reset(new storm::models::Mdp(transitionMatrix, ap, boost::none, boost::none, boost::none)); + + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); + + auto labelFormula = std::make_shared("a"); + auto lraFormula = std::make_shared(storm::logic::OptimalityType::Minimize, labelFormula); + + std::unique_ptr result = checker.check(*lraFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(.5, quantitativeResult[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(.5, quantitativeResult[1], storm::settings::nativeEquationSolverSettings().getPrecision()); + } +}