diff --git a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp index 7de319261..fc7d7c527 100644 --- a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp @@ -73,10 +73,10 @@ namespace storm { // For testing only if (sizeof(ValueType) == sizeof(double)) { - std::cout << "<<< Using CUDA-DOUBLE Kernels >>>" << std::endl; + //std::cout << "<<< Using CUDA-DOUBLE Kernels >>>" << std::endl; LOG4CPLUS_INFO(logger, "<<< Using CUDA-DOUBLE Kernels >>>"); } else { - std::cout << "<<< Using CUDA-FLOAT Kernels >>>" << std::endl; + //std::cout << "<<< Using CUDA-FLOAT Kernels >>>" << std::endl; LOG4CPLUS_INFO(logger, "<<< Using CUDA-FLOAT Kernels >>>"); } @@ -96,7 +96,7 @@ namespace storm { std::vector> sccDecomposition; if (__USE_CUDAFORSTORM_OPT && (gpuSizeOfCompleteSystem < cudaFreeMemory)) { // Dummy output for SCC Times - std::cout << "Computing the SCC Decomposition took 0ms" << std::endl; + //std::cout << "Computing the SCC Decomposition took 0ms" << std::endl; #ifdef STORM_HAVE_CUDAFORSTORM if (!resetCudaDevice()) { @@ -124,9 +124,9 @@ namespace storm { } std::chrono::high_resolution_clock::time_point calcEndTime = std::chrono::high_resolution_clock::now(); - std::cout << "Obtaining the fixpoint solution took " << std::chrono::duration_cast(calcEndTime - calcStartTime).count() << "ms." << std::endl; + //std::cout << "Obtaining the fixpoint solution took " << std::chrono::duration_cast(calcEndTime - calcStartTime).count() << "ms." << std::endl; - std::cout << "Used a total of " << globalIterations << " iterations with a maximum of " << globalIterations << " iterations in a single block." << std::endl; + //std::cout << "Used a total of " << globalIterations << " iterations with a maximum of " << globalIterations << " iterations in a single block." << std::endl; // Check if the solver converged and issue a warning otherwise. if (converged) { @@ -157,7 +157,7 @@ namespace storm { LOG4CPLUS_INFO(logger, "Optimized SCC Decomposition, originally " << topologicalSort.size() << " SCCs, optimized to " << optimalSccs.size() << " SCCs."); std::chrono::high_resolution_clock::time_point sccEndTime = std::chrono::high_resolution_clock::now(); - std::cout << "Computing the SCC Decomposition took " << std::chrono::duration_cast(sccEndTime - sccStartTime).count() << "ms." << std::endl; + //std::cout << "Computing the SCC Decomposition took " << std::chrono::duration_cast(sccEndTime - sccStartTime).count() << "ms." << std::endl; std::chrono::high_resolution_clock::time_point calcStartTime = std::chrono::high_resolution_clock::now(); @@ -255,7 +255,8 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!"; #endif } else { - std::cout << "WARNING: Using CPU based TopoSolver! (double)" << std::endl; + //std::cout << "WARNING: Using CPU based TopoSolver! (double)" << std::endl; + LOG4CPLUS_INFO(logger, "Performance Warning: Using CPU based TopoSolver! (double)"); localIterations = 0; converged = false; while (!converged && localIterations < this->maximalNumberOfIterations) { @@ -313,7 +314,7 @@ namespace storm { } } - std::cout << "Used a total of " << globalIterations << " iterations with a maximum of " << localIterations << " iterations in a single block." << std::endl; + //std::cout << "Used a total of " << globalIterations << " iterations with a maximum of " << localIterations << " iterations in a single block." << std::endl; // Check if the solver converged and issue a warning otherwise. if (converged) { @@ -323,7 +324,7 @@ namespace storm { } std::chrono::high_resolution_clock::time_point calcEndTime = std::chrono::high_resolution_clock::now(); - std::cout << "Obtaining the fixpoint solution took " << std::chrono::duration_cast(calcEndTime - calcStartTime).count() << "ms." << std::endl; + //std::cout << "Obtaining the fixpoint solution took " << std::chrono::duration_cast(calcEndTime - calcStartTime).count() << "ms." << std::endl; } } diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 699d4d477..194de520c 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -209,77 +209,86 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { } TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { - //storm::settings::Settings* s = storm::settings::Settings::getInstance(); std::shared_ptr> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew")->as>(); - //ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); - //ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); + ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); - //storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker mc(*mdp); - - //storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); - //storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - //storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker mc(*mdp); - //std::vector result = mc.checkNoBoundOperator(*probFormula); + auto apFormula = std::make_shared("elected"); + auto eventuallyFormula = std::make_shared(apFormula); + auto probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + std::unique_ptr result = mc.check(*probabilityOperatorFormula); - //ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 1), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - //delete probFormula; + probabilityOperatorFormula.reset(); - //apFormula = new storm::property::prctl::Ap("elected"); - //eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - //probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); + apFormula = std::make_shared("elected"); + eventuallyFormula = std::make_shared(apFormula); + probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); - //result = mc.checkNoBoundOperator(*probFormula); + result = mc.check(*probabilityOperatorFormula); - //ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 1), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - //delete probFormula; + probabilityOperatorFormula.reset(); - //apFormula = new storm::property::prctl::Ap("elected"); - //storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); - //probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + apFormula = std::make_shared("elected"); + auto boundedEventuallyFormula = std::make_shared(std::make_shared(true), apFormula, 25); + probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedEventuallyFormula); - //result = mc.checkNoBoundOperator(*probFormula); + result = mc.check(*probabilityOperatorFormula); - //ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0625), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - //delete probFormula; + probabilityOperatorFormula.reset(); - //apFormula = new storm::property::prctl::Ap("elected"); - //boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); - //probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + apFormula = std::make_shared("elected"); + boundedEventuallyFormula = std::make_shared(std::make_shared(true), apFormula, 25); + probabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedEventuallyFormula); - //result = mc.checkNoBoundOperator(*probFormula); + result = mc.check(*probabilityOperatorFormula); - //ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 0.0625), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - //delete probFormula; + probabilityOperatorFormula.reset(); - //apFormula = new storm::property::prctl::Ap("elected"); - //storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - //storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); + apFormula = std::make_shared("elected"); + auto reachabilityRewardFormula = std::make_shared(apFormula); + auto rewardFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); - //result = mc.checkNoBoundOperator(*rewardFormula); + result = mc.check(*rewardFormula); #ifdef STORM_HAVE_CUDAFORSTORM - //ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 4.285689611), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - //ASSERT_LT(std::abs(result[0] - 4.285701547), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 4.285701547), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - //delete rewardFormula; - //apFormula = new storm::property::prctl::Ap("elected"); - //reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - //rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); + probabilityOperatorFormula.reset(); - //result = mc.checkNoBoundOperator(*rewardFormula); + apFormula = std::make_shared("elected"); + 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] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 4.285689611), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #else - //ASSERT_LT(std::abs(result[0] - 4.285703591), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 4.285703591), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - //delete rewardFormula; + + probabilityOperatorFormula.reset(); }