Trying to refurbish the TopologicalValueIterationMdpPrctlModelChecker

Former-commit-id: 2963c774b0
11 years ago · 64891af785
5 changed files with 462 additions and 2 deletions
--- 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<Type> const& modelchecker)
+	explicit TopologicalValueIterationMdpPrctlModelChecker(storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<Type> const& modelchecker)
 		: SparseMdpPrctlModelChecker<Type>(modelchecker),  minimumOperatorStack() {
 		// Intentionally left empty.
 	}
--- a/src/solver/NativeNondeterministicLinearEquationSolver.h
+++ b/src/solver/NativeNondeterministicLinearEquationSolver.h
@ -34,7 +34,7 @@ namespace storm {
            
            virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const override;

-        private:
+        protected:
            // The required precision for the iterative methods.
            double precision;
            
--- a/src/solver/TopologicalValueIterationNativeNondeterministicLinearEquationSolver.h
+++ 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 ValueType>
+		class TopologicalValueIterationNondeterministicLinearEquationSolver : public NondeterministicLinearEquationSolver<ValueType> {
+        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<ValueType>* clone() const override;
+            
+            virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const override;
+        };
+    } // namespace solver
+} // namespace storm
+
+#endif /* STORM_SOLVER_NATIVENONDETERMINISTICLINEAREQUATIONSOLVER_H_ */
--- a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
+++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
@ -0,0 +1,197 @@
+#include "src/solver/TopologicalValueIterationNativeNondeterministicLinearEquationSolver.h"
+
+#include <utility>
+
+#include "src/settings/Settings.h"
+#include "src/utility/vector.h"
+
+namespace storm {
+    namespace solver {
+        
+        template<typename ValueType>
+		TopologicalValueIterationNondeterministicLinearEquationSolver<ValueType>::TopologicalValueIterationNondeterministicLinearEquationSolver() {
+            // // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+		TopologicalValueIterationNondeterministicLinearEquationSolver<ValueType>::TopologicalValueIterationNondeterministicLinearEquationSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : NativeNondeterministicLinearEquationSolver<ValueType>(precision, maximalNumberOfIterations, relative) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+		TopologicalValueIterationNondeterministicLinearEquationSolver<ValueType>* TopologicalValueIterationNondeterministicLinearEquationSolver<ValueType>::clone() const {
+            return new NativeNondeterministicLinearEquationSolver<ValueType>(*this);
+        }
+        
+        template<typename ValueType>
+		void TopologicalValueIterationNondeterministicLinearEquationSolver<ValueType>::solveEquationSystem(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
+            
+			// Now, we need to determine the SCCs of the MDP and a topological sort.
+			std::vector<std::vector<uint_fast64_t>> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph);
+			storm::storage::SparseMatrix<T> stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents);
+			std::vector<uint_fast64_t> topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph);
+
+			// Set up the environment for the power method.
+			bool multiplyResultMemoryProvided = true;
+			if (multiplyResult == nullptr) {
+				multiplyResult = new std::vector<ValueType>(A.getRowCount());
+				multiplyResultMemoryProvided = false;
+			}
+			std::vector<ValueType>* currentX = &x;
+			bool xMemoryProvided = true;
+			if (newX == nullptr) {
+				newX = new std::vector<ValueType>(x.size());
+				xMemoryProvided = false;
+			}
+			std::vector<ValueType>* 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<uint_fast64_t> 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<ValueType>(A.getRowCount());
+                multiplyResultMemoryProvided = false;
+            }
+            std::vector<ValueType>* currentX = &x;
+            bool xMemoryProvided = true;
+            if (newX == nullptr) {
+                newX = new std::vector<ValueType>(x.size());
+                xMemoryProvided = false;
+            }
+            std::vector<ValueType>* 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<ValueType>* 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<double>;
+    } // namespace solver
+} // namespace storm
--- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
+++ 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<double> 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<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+    
+	ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
+	ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
+    
+	storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
+    
+	storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
+	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
+	storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+    
+	std::vector<double> 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<double>("two");
+	eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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<double>("three");
+	eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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<double>("three");
+	eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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<double>("four");
+	eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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<double>("four");
+	eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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<double>("done");
+	storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
+	storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(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<double>("done");
+	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(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<double> 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<storm::models::Mdp<double>> stateRewardMdp = stateRewardParser.getModel<storm::models::Mdp<double>>();
+    
+    storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
+
+	apFormula = new storm::property::prctl::Ap<double>("done");
+	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(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<double>("done");
+	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(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<double> 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<storm::models::Mdp<double>> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel<storm::models::Mdp<double>>();
+    
+	storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
+    
+	apFormula = new storm::property::prctl::Ap<double>("done");
+	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(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<double>("done");
+	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(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<double> 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<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+
+	ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
+	ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
+
+	storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
+
+	storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
+	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
+	storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+
+	std::vector<double> 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<double>("elected");
+	eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
+	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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<double>("elected");
+	storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
+	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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<double>("elected");
+	boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
+	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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<double>("elected");
+	storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
+	storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(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<double>("elected");
+	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+
+	result = mc.checkNoBoundOperator(*rewardFormula);;
+
+	ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	delete rewardFormula;
+}