From 8b4309e53cdec2d38b1df997e0a1fd0f30c54be1 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Mon, 2 Feb 2015 18:49:23 +0100 Subject: [PATCH] Adapted first test to new interface. Test passes. Former-commit-id: 49dc8228f397db3582ec83bc71a4bb525be1f97d --- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 257 ++++++++++-------- 1 file changed, 147 insertions(+), 110 deletions(-) diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 91388c958..699d4d477 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -22,153 +22,190 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker mc(*mdp); + //storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("two"); auto apFormula = std::make_shared("two"); - //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); + auto eventuallyFormula = std::make_shared(apFormula); //storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + auto probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); - std::unique_ptr result = mc.check(*minProbabilityOperatorFormula); //std::vector result = mc.checkNoBoundOperator(*probFormula); + std::unique_ptr result = mc.check(*probabilityOperatorFormula); + //ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0277777612209320068), storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - //ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + + //delete probFormula; + probabilityOperatorFormula.reset(); //apFormula = new storm::property::prctl::Ap("two"); + apFormula = std::make_shared("two"); //eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + eventuallyFormula = std::make_shared(apFormula); //probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - // + probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + //result = mc.checkNoBoundOperator(*probFormula); - // + result = mc.check(*probabilityOperatorFormula); + //ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - // - //delete probFormula; - // - //apFormula = new storm::property::prctl::Ap("three"); - //eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - //probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - // - //result = mc.checkNoBoundOperator(*probFormula); - // - //ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - // - //delete probFormula; - // - //apFormula = new storm::property::prctl::Ap("three"); - //eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - //probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - // - //result = mc.checkNoBoundOperator(*probFormula); - // - //ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - // - //delete probFormula; - // - //apFormula = new storm::property::prctl::Ap("four"); - //eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - //probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - // - //result = mc.checkNoBoundOperator(*probFormula); - // - //ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - // - //delete probFormula; - // - //apFormula = new storm::property::prctl::Ap("four"); - //eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - //probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - // - //result = mc.checkNoBoundOperator(*probFormula); - // - //ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - // + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0277777612209320068), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + //delete probFormula; - // - //apFormula = new storm::property::prctl::Ap("done"); - //storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - //storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - // - //result = mc.checkNoBoundOperator(*rewardFormula); + probabilityOperatorFormula.reset(); + + // ---------------- test ap "three" ---------------- + apFormula = std::make_shared("three"); + eventuallyFormula = std::make_shared(apFormula); + probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + result = mc.check(*probabilityOperatorFormula); + + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0555555224418640136), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + + probabilityOperatorFormula.reset(); + + apFormula = std::make_shared("three"); + eventuallyFormula = std::make_shared(apFormula); + probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = mc.check(*probabilityOperatorFormula); + + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0555555224418640136), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + + probabilityOperatorFormula.reset(); + + // ---------------- test ap "four" ---------------- + apFormula = std::make_shared("four"); + eventuallyFormula = std::make_shared(apFormula); + probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + result = mc.check(*probabilityOperatorFormula); + + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.083333283662796020508), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + + probabilityOperatorFormula.reset(); + + apFormula = std::make_shared("four"); + eventuallyFormula = std::make_shared(apFormula); + probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = mc.check(*probabilityOperatorFormula); + + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.083333283662796020508), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + + probabilityOperatorFormula.reset(); + + + // ---------------- test ap "done" ---------------- + apFormula = std::make_shared("done"); + auto reachabilityRewardFormula = std::make_shared(apFormula); + auto rewardFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = mc.check(*rewardFormula); #ifdef STORM_HAVE_CUDAFORSTORM - //ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.333329499), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - //ASSERT_LT(std::abs(result[0] - 7.33332904), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.33332904), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - //delete rewardFormula; - // - //apFormula = new storm::property::prctl::Ap("done"); - //reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - //rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - // - //result = mc.checkNoBoundOperator(*rewardFormula);; + rewardFormula.reset(); + + + apFormula = std::make_shared("done"); + reachabilityRewardFormula = std::make_shared(apFormula); + rewardFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = mc.check(*rewardFormula); #ifdef STORM_HAVE_CUDAFORSTORM - //ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.333329499), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - //ASSERT_LT(std::abs(result[0] - 7.33333151), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.33333151), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - //delete rewardFormula; - //std::shared_ptr> stateRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "")->as>(); - // - //storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp); + rewardFormula.reset(); + + // ------------- state rewards -------------- + std::shared_ptr> stateRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "")->as>(); + + storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp); + + + apFormula = std::make_shared("done"); + reachabilityRewardFormula = std::make_shared(apFormula); + rewardFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = stateRewardModelChecker.check(*rewardFormula); - //apFormula = new storm::property::prctl::Ap("done"); - //reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - //rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - // - //result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula); - #ifdef STORM_HAVE_CUDAFORSTORM - //ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.333329499), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - //ASSERT_LT(std::abs(result[0] - 7.33332904), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.33332904), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - //delete rewardFormula; - // - //apFormula = new storm::property::prctl::Ap("done"); - //reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - //rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - // - //result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula); - + rewardFormula.reset(); + + apFormula = std::make_shared("done"); + reachabilityRewardFormula = std::make_shared(apFormula); + rewardFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = stateRewardModelChecker.check(*rewardFormula); + #ifdef STORM_HAVE_CUDAFORSTORM - //ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.333329499), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - //ASSERT_LT(std::abs(result[0] - 7.33333151), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 7.33333151), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - //delete rewardFormula; - //std::shared_ptr> stateAndTransitionRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as>(); - // - //storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); - // - //apFormula = new storm::property::prctl::Ap("done"); - //reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - //rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - // - //result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); + rewardFormula.reset(); + + // -------------------------------- state and transition reward ------------------------ + std::shared_ptr> stateAndTransitionRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as>(); + + storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); + + apFormula = std::make_shared("done"); + reachabilityRewardFormula = std::make_shared(apFormula); + rewardFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = stateAndTransitionRewardModelChecker.check(*rewardFormula); + #ifdef STORM_HAVE_CUDAFORSTORM - //ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 14.666658998), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - //ASSERT_LT(std::abs(result[0] - 14.6666581), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 14.6666581), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - //delete rewardFormula; - // - //apFormula = new storm::property::prctl::Ap("done"); - //reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - //rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - // - //result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); - + rewardFormula.reset(); + + apFormula = std::make_shared("done"); + reachabilityRewardFormula = std::make_shared(apFormula); + rewardFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = stateAndTransitionRewardModelChecker.check(*rewardFormula); + #ifdef STORM_HAVE_CUDAFORSTORM - //ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 14.666658998), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - //ASSERT_LT(std::abs(result[0] - 14.666663), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 14.666663), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - //delete rewardFormula; + rewardFormula.reset(); } TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {