From 64891af7854e0136c6d0ff72f31a9ac974889a39 Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 3 Feb 2014 04:21:35 +0100 Subject: [PATCH] Trying to refurbish the TopologicalValueIterationMdpPrctlModelChecker Former-commit-id: 2963c774b04a9b8e3afa1f4b8f30d9563884c9a6 --- ...ogicalValueIterationMdpPrctlModelChecker.h | 2 +- ...tiveNondeterministicLinearEquationSolver.h | 2 +- ...tiveNondeterministicLinearEquationSolver.h | 39 +++ ...onNondeterministicLinearEquationSolver.cpp | 197 +++++++++++++++ ...ValueIterationMdpPrctlModelCheckerTest.cpp | 224 ++++++++++++++++++ 5 files changed, 462 insertions(+), 2 deletions(-) create mode 100644 src/solver/TopologicalValueIterationNativeNondeterministicLinearEquationSolver.h create mode 100644 src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp create mode 100644 test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp diff --git a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h index 77fa27543..84bc1764d 100644 --- a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h @@ -37,7 +37,7 @@ public: * Copy constructs a SparseMdpPrctlModelChecker from the given model checker. In particular, this means that the newly * constructed model checker will have the model of the given model checker as its associated model. */ - explicit TopologicalValueIterationMdpPrctlModelChecker(storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker const& modelchecker) + explicit TopologicalValueIterationMdpPrctlModelChecker(storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker const& modelchecker) : SparseMdpPrctlModelChecker(modelchecker), minimumOperatorStack() { // Intentionally left empty. } diff --git a/src/solver/NativeNondeterministicLinearEquationSolver.h b/src/solver/NativeNondeterministicLinearEquationSolver.h index 51c8ddd97..64b361acb 100644 --- a/src/solver/NativeNondeterministicLinearEquationSolver.h +++ b/src/solver/NativeNondeterministicLinearEquationSolver.h @@ -34,7 +34,7 @@ namespace storm { virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; - private: + protected: // The required precision for the iterative methods. double precision; diff --git a/src/solver/TopologicalValueIterationNativeNondeterministicLinearEquationSolver.h b/src/solver/TopologicalValueIterationNativeNondeterministicLinearEquationSolver.h new file mode 100644 index 000000000..2dfc0206d --- /dev/null +++ b/src/solver/TopologicalValueIterationNativeNondeterministicLinearEquationSolver.h @@ -0,0 +1,39 @@ +#ifndef STORM_SOLVER_TOPOLOGICALVALUEITERATIONNONDETERMINISTICLINEAREQUATIONSOLVER_H_ +#define STORM_SOLVER_TOPOLOGICALVALUEITERATIONNONDETERMINISTICLINEAREQUATIONSOLVER_H_ + +#include "src/solver/NondeterministicLinearEquationSolver.h" +#include "src/solver/NativeNondeterministicLinearEquationSolver.h" + +namespace storm { + namespace solver { + + /*! + * A class that uses SCC Decompositions to solve a linear equation system + */ + template + class TopologicalValueIterationNondeterministicLinearEquationSolver : public NondeterministicLinearEquationSolver { + public: + /*! + * Constructs a nondeterministic linear equation solver with parameters being set according to the settings + * object. + */ + TopologicalValueIterationNondeterministicLinearEquationSolver(); + + /*! + * Constructs a nondeterminstic linear equation solver with the given parameters. + * + * @param precision The precision to use for convergence detection. + * @param maximalNumberOfIterations The maximal number of iterations do perform before iteration is aborted. + * @param relative If set, the relative error rather than the absolute error is considered for convergence + * detection. + */ + TopologicalValueIterationNondeterministicLinearEquationSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); + + virtual NondeterministicLinearEquationSolver* clone() const override; + + virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; + }; + } // namespace solver +} // namespace storm + +#endif /* STORM_SOLVER_NATIVENONDETERMINISTICLINEAREQUATIONSOLVER_H_ */ diff --git a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp new file mode 100644 index 000000000..4b90dbb40 --- /dev/null +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp @@ -0,0 +1,197 @@ +#include "src/solver/TopologicalValueIterationNativeNondeterministicLinearEquationSolver.h" + +#include + +#include "src/settings/Settings.h" +#include "src/utility/vector.h" + +namespace storm { + namespace solver { + + template + TopologicalValueIterationNondeterministicLinearEquationSolver::TopologicalValueIterationNondeterministicLinearEquationSolver() { + // // Intentionally left empty. + } + + template + TopologicalValueIterationNondeterministicLinearEquationSolver::TopologicalValueIterationNondeterministicLinearEquationSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : NativeNondeterministicLinearEquationSolver(precision, maximalNumberOfIterations, relative) { + // Intentionally left empty. + } + + template + TopologicalValueIterationNondeterministicLinearEquationSolver* TopologicalValueIterationNondeterministicLinearEquationSolver::clone() const { + return new NativeNondeterministicLinearEquationSolver(*this); + } + + template + void TopologicalValueIterationNondeterministicLinearEquationSolver::solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, std::vector* multiplyResult, std::vector* newX) const { + + // Now, we need to determine the SCCs of the MDP and a topological sort. + std::vector> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); + storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents); + std::vector topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); + + // Set up the environment for the power method. + bool multiplyResultMemoryProvided = true; + if (multiplyResult == nullptr) { + multiplyResult = new std::vector(A.getRowCount()); + multiplyResultMemoryProvided = false; + } + std::vector* currentX = &x; + bool xMemoryProvided = true; + if (newX == nullptr) { + newX = new std::vector(x.size()); + xMemoryProvided = false; + } + std::vector* swap = nullptr; + uint_fast64_t currentMaxLocalIterations = 0; + uint_fast64_t localIterations = 0; + uint_fast64_t globalIterations = 0; + bool converged = true; + + // Iterate over all SCCs of the MDP as specified by the topological sort. This guarantees that an SCC is only + // solved after all SCCs it depends on have been solved. + for (auto sccIndexIt = topologicalSort.begin(); sccIndexIt != topologicalSort.end() && converged; ++sccIndexIt) { + std::vector const& scc = stronglyConnectedComponents[*sccIndexIt]; + + // For the current SCC, we need to perform value iteration until convergence. + localIterations = 0; + converged = false; + while (!converged && localIterations < maxIterations) { + // Compute x' = A*x + b. + matrix.multiplyWithVector(scc, nondeterministicChoiceIndices, *currentX, multiplyResult); + storm::utility::addVectors(scc, nondeterministicChoiceIndices, multiplyResult, b); + + /* + Versus: + A.multiplyWithVector(*currentX, *multiplyResult); + storm::utility::vector::addVectorsInPlace(*multiplyResult, b); + */ + + // Reduce the vector x' by applying min/max for all non-deterministic choices. + if (minimize) { + storm::utility::reduceVectorMin(*multiplyResult, *newX, scc, nondeterministicChoiceIndices); + } + else { + storm::utility::reduceVectorMax(*multiplyResult, *newX, scc, nondeterministicChoiceIndices); + } + + // Determine whether the method converged. + // TODO: It seems that the equalModuloPrecision call that compares all values should have a higher + // running time. In fact, it is faster. This has to be investigated. + // converged = storm::utility::equalModuloPrecision(*currentX, *newX, scc, precision, relative); + converged = storm::utility::equalModuloPrecision(*currentX, *newX, precision, relative); + + // Update environment variables. + swap = currentX; + currentX = newX; + newX = swap; + ++localIterations; + ++globalIterations; + } + + // As the "number of iterations" of the full method is the maximum of the local iterations, we need to keep + // track of the maximum. + if (localIterations > currentMaxLocalIterations) { + currentMaxLocalIterations = localIterations; + } + } + + // If we performed an odd number of global iterations, we need to swap the x and currentX, because the newest + // result is currently stored in currentX, but x is the output vector. + // TODO: Check whether this is correct or should be put into the for-loop over SCCs. + if (globalIterations % 2 == 1) { + std::swap(x, *currentX); + } + + if (!xMemoryProvided) { + delete copyX; + } + + if (!multiplyResultMemoryProvided) { + delete multiplyResult; + } + + // Check if the solver converged and issue a warning otherwise. + if (converged) { + LOG4CPLUS_INFO(logger, "Iterative solver converged after " << currentMaxLocalIterations << " iterations."); + } + else { + LOG4CPLUS_WARN(logger, "Iterative solver did not converged after " << currentMaxLocalIterations << " iterations."); + } + + + /* + + !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + + */ + + // Set up the environment for the power method. If scratch memory was not provided, we need to create it. + bool multiplyResultMemoryProvided = true; + if (multiplyResult == nullptr) { + multiplyResult = new std::vector(A.getRowCount()); + multiplyResultMemoryProvided = false; + } + std::vector* currentX = &x; + bool xMemoryProvided = true; + if (newX == nullptr) { + newX = new std::vector(x.size()); + xMemoryProvided = false; + } + std::vector* swap = nullptr; + uint_fast64_t iterations = 0; + bool converged = false; + + // Keep track of which of the vectors for x is the auxiliary copy. + std::vector* copyX = newX; + + // Proceed with the iterations as long as the method did not converge or reach the + // user-specified maximum number of iterations. + while (!converged && iterations < maximalNumberOfIterations) { + // Compute x' = A*x + b. + A.multiplyWithVector(*currentX, *multiplyResult); + storm::utility::vector::addVectorsInPlace(*multiplyResult, b); + + // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost + // element of the min/max operator stack. + if (minimize) { + storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, nondeterministicChoiceIndices); + } else { + storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, nondeterministicChoiceIndices); + } + + // Determine whether the method converged. + converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, precision, relative); + + // Update environment variables. + std::swap(currentX, newX); + ++iterations; + } + + // Check if the solver converged and issue a warning otherwise. + if (converged) { + LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations."); + } else { + LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations."); + } + + // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result + // is currently stored in currentX, but x is the output vector. + if (currentX == copyX) { + std::swap(x, *currentX); + } + + if (!xMemoryProvided) { + delete copyX; + } + + if (!multiplyResultMemoryProvided) { + delete multiplyResult; + } + } + + // Explicitly instantiate the solver. + template class TopologicalValueIterationNondeterministicLinearEquationSolver; + } // namespace solver +} // namespace storm diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..7ccb05369 --- /dev/null +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,224 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/solver/NativeNondeterministicLinearEquationSolver.h" +#include "src/settings/Settings.h" +#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h" +#include "src/parser/AutoParser.h" + +TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + storm::parser::AutoParser parser(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.trans.rew"); + + ASSERT_EQ(parser.getType(), storm::models::MDP); + + std::shared_ptr> mdp = parser.getModel>(); + + ASSERT_EQ(mdp->getNumberOfStates(), 169ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); + + storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker mc(*mdp); + + storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("two"); + storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); + storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + std::vector result = mc.checkNoBoundOperator(*probFormula); + + 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); + + result = mc.checkNoBoundOperator(*probFormula); + + 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()); + + 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); + + ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + 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);; + + ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + delete rewardFormula; + + storm::parser::AutoParser stateRewardParser(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", ""); + + ASSERT_EQ(stateRewardParser.getType(), storm::models::MDP); + + std::shared_ptr> stateRewardMdp = stateRewardParser.getModel>(); + + storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); + + 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); + + ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + 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); + + ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + delete rewardFormula; + + storm::parser::AutoParser stateAndTransitionRewardParser(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"); + + ASSERT_EQ(stateAndTransitionRewardParser.getType(), storm::models::MDP); + + std::shared_ptr> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel>(); + + storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); + + 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); + + ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + 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); + + ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + delete rewardFormula; +} + +TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + storm::parser::AutoParser parser(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"); + + ASSERT_EQ(parser.getType(), storm::models::MDP); + + std::shared_ptr> mdp = parser.getModel>(); + + 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); + + std::vector result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + + delete probFormula; + + apFormula = new storm::property::prctl::Ap("elected"); + 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] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + + delete probFormula; + + 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); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + + delete probFormula; + + apFormula = new storm::property::prctl::Ap("elected"); + boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); + probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + + result = mc.checkNoBoundOperator(*probFormula); + + ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + + delete probFormula; + + 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); + + result = mc.checkNoBoundOperator(*rewardFormula);; + + ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + delete rewardFormula; + + apFormula = new storm::property::prctl::Ap("elected"); + reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); + rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); + + result = mc.checkNoBoundOperator(*rewardFormula);; + + ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + delete rewardFormula; +}