diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 86936c58e..91388c958 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -26,9 +26,10 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { //storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("two"); auto eventuallyFormula = std::make_shared(apFormula); //storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); //storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - std::unique_ptr result = mc.check(*eventuallyFormula); + std::unique_ptr result = mc.check(*minProbabilityOperatorFormula); //std::vector result = mc.checkNoBoundOperator(*probFormula); ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0277777612209320068),