diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index 538bfc6f8..f3d817c9f 100644 --- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -82,11 +82,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true); + result = stateRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true); ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false); + result = stateRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, false); ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); @@ -103,11 +103,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true); + result = stateAndTransitionRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true); ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false); + result = stateAndTransitionRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, false); ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());