diff --git a/examples/mdp/scc/scc.pctl b/examples/mdp/scc/scc.pctl index 393670a26..8a853a969 100644 --- a/examples/mdp/scc/scc.pctl +++ b/examples/mdp/scc/scc.pctl @@ -1,2 +1,2 @@ -Pmin=? [ F a ] -Pmax=? [ F a ] \ No newline at end of file +Pmin=? [ F end ] +Pmax=? [ F end ] \ No newline at end of file diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 114de1b47..874170a4f 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -16,12 +16,12 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> mdp = parser.getModel>(); - ASSERT_EQ(mdp->getNumberOfStates(), 169ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); + ASSERT_EQ(mdp->getNumberOfStates(), 11ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 17ull); storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker mc(*mdp); - storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("two"); + storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("end"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); @@ -30,7 +30,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; - + /* apFormula = new storm::property::prctl::Ap("two"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); @@ -149,7 +149,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; + delete rewardFormula;*/ } TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {