Merge branch 'master' into PrctlParser

CMakeLists.txt

@@ -95,7 +95,7 @@ else(CLANG)
 	# As CLANG is not set as a variable, we need to set it in case we have not matched another compiler.
 	set (CLANG ON)
     # Set standard flags for clang
-    set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O4")
+    set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O3")
     set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE")
     
     set (CMAKE_CXX_FLAGS_DEBUG "-g")

examples/dtmc/synchronous_leader/leader.pctl

@@ -1,3 +1,4 @@
 P=? [ F elected ]
-P=? [ F<=(4*(N+1)) elected ]
+// P=? [ F<=(4*(N+1)) elected ]
+P=? [ F<=28 elected ]
 R=? [ F elected ]

examples/mdp/consensus/coin.pctl

@@ -11,8 +11,8 @@ Pmin=? [ F finished & all_coins_equal_1 ]
 Pmax=? [ F finished & !agree ]
 
 // Min/max probability of finishing within k steps
-Pmin=? [ F<=k finished ]
-Pmax=? [ F<=k finished ]
+Pmin=? [ F<=50 finished ]
+Pmax=? [ F<=50 finished ]
 
 // Min/max expected steps to finish
 Rmin=? [ F finished ]

src/models/AbstractDeterministicModel.h

@@ -52,7 +52,7 @@ class AbstractDeterministicModel: public AbstractModel<T> {
          * @param state The state for which to return the iterator.
          * @return An iterator to the successors of the given state.
          */
-        virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) {
+        virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const {
             return this->getTransitionMatrix()->constColumnIteratorBegin(state);
         }
     
@@ -62,7 +62,7 @@ class AbstractDeterministicModel: public AbstractModel<T> {
          * @param state The state for which to return the iterator.
          * @return An iterator pointing to the element past the successors of the given state.
          */
-        virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) {
+        virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const {
             return this->getTransitionMatrix()->constColumnIteratorEnd(state);
         }
 };

src/models/AbstractModel.h

@@ -91,7 +91,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
          * @param stronglyConnectedComponents A vector containing the SCCs of the system.
          * @param stateToSccMap A mapping from state indices to
          */
-        virtual storm::storage::SparseMatrix<bool> extractSccDependencyGraph(std::vector<std::vector<uint_fast64_t>> const& stronglyConnectedComponents, std::map<uint_fast64_t, uint_fast64_t> const& stateToSccMap) {
+        storm::storage::SparseMatrix<bool> extractSccDependencyGraph(std::vector<std::vector<uint_fast64_t>> const& stronglyConnectedComponents, std::map<uint_fast64_t, uint_fast64_t> const& stateToSccMap) const {
             // The resulting sparse matrix will have as many rows/columns as there are SCCs.
             uint_fast64_t numberOfStates = stronglyConnectedComponents.size();
             storm::storage::SparseMatrix<bool> sccDependencyGraph(numberOfStates);
@@ -132,7 +132,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
          * @param state The state for which to return the iterator.
          * @return An iterator to the successors of the given state.
          */
-        virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) = 0;
+        virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const = 0;
     
         /*!
          * Returns an iterator pointing to the element past the successors of the given state.
@@ -140,7 +140,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
          * @param state The state for which to return the iterator.
          * @return An iterator pointing to the element past the successors of the given state.
          */
-        virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) = 0;
+        virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const = 0;
     
 		/*!
 		 * Returns the state space size of the model.

src/models/AbstractNondeterministicModel.h

@@ -84,7 +84,7 @@ class AbstractNondeterministicModel: public AbstractModel<T> {
          * @param state The state for which to return the iterator.
          * @return An iterator to the successors of the given state.
          */
-        virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) {
+        virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const {
             return this->getTransitionMatrix()->constColumnIteratorBegin((*nondeterministicChoiceIndices)[state]);
         }
     
@@ -94,7 +94,7 @@ class AbstractNondeterministicModel: public AbstractModel<T> {
          * @param state The state for which to return the iterator.
          * @return An iterator pointing to the element past the successors of the given state.
          */
-        virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) {
+        virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const {
             return this->getTransitionMatrix()->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1);
         }
 

src/storage/SparseMatrix.h

@@ -219,7 +219,7 @@ public:
 	 *
 	 * @param size The number of rows and columns of the matrix.
 	 */
-	SparseMatrix(uint_fast64_t size)
+	SparseMatrix(uint_fast64_t size = 0)
 			: rowCount(size), colCount(size), nonZeroEntryCount(0),
 			  internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) {
 			  

src/utility/GraphAnalyzer.h

@@ -428,10 +428,10 @@ public:
      * graph of the SCCs.
      */
 	template <typename T>
-	static std::pair<std::vector<std::vector<uint_fast64_t>>, storm::models::GraphTransitions<T>> performSccDecomposition(storm::models::AbstractNondeterministicModel<T> const& model) {
+	static std::pair<std::vector<std::vector<uint_fast64_t>>, storm::storage::SparseMatrix<bool>> performSccDecomposition(storm::models::AbstractModel<T> const& model) {
 		LOG4CPLUS_INFO(logger, "Computing SCC decomposition.");
         
-        std::pair<std::vector<std::vector<uint_fast64_t>>, storm::models::GraphTransitions<T>> sccDecomposition;
+        std::pair<std::vector<std::vector<uint_fast64_t>>, storm::storage::SparseMatrix<bool>> sccDecomposition;
         uint_fast64_t numberOfStates = model.getNumberOfStates();
             
         // Set up the environment of Tarjan's algorithm.
@@ -447,7 +447,7 @@ public:
         uint_fast64_t currentIndex = 0;
         for (uint_fast64_t state = 0; state < numberOfStates; ++state) {
             if (!visitedStates.get(state)) {
-                performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, model.getTransitionMatrix(), sccDecomposition.first, stateToSccMap);
+                performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, *model.getTransitionMatrix(), sccDecomposition.first, stateToSccMap);
             }
         }
             

test/performance/graph/GraphTest.cpp

@@ -0,0 +1,117 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/utility/Settings.h"
+#include "src/parser/AutoParser.h"
+#include "src/utility/GraphAnalyzer.h"
+
+TEST(GraphAnalyzerTest, PerformProb01) {
+	storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
+
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+
+    LOG4CPLUS_INFO(logger, "Computing prob01 (3 times) for crowds/crowds20_5.");
+    std::pair<storm::storage::BitVector, storm::storage::BitVector> prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observe0Greater1")));
+    
+    ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1724414u);
+    ASSERT_EQ(prob01.second.getNumberOfSetBits(), 46046u);
+    
+    prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeIGreater1")));
+
+    ASSERT_EQ(prob01.first.getNumberOfSetBits(), 574016u);
+    ASSERT_EQ(prob01.second.getNumberOfSetBits(), 825797u);
+    
+    prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeOnlyTrueSender")));
+
+    ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1785309u);
+    ASSERT_EQ(prob01.second.getNumberOfSetBits(), 40992u);
+    LOG4CPLUS_INFO(logger, "Done computing prob01 (3 times) for crowds/crowds20_5.");
+    
+    storm::parser::AutoParser<double> parser2(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew");
+    
+    std::shared_ptr<storm::models::Dtmc<double>> dtmc2 = parser2.getModel<storm::models::Dtmc<double>>();
+    
+    LOG4CPLUS_INFO(logger, "Computing prob01 for synchronous_leader/leader6_8");
+    prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc2, storm::storage::BitVector(dtmc2->getNumberOfStates(), true), storm::storage::BitVector(dtmc2->getLabeledStates("elected")));
+    LOG4CPLUS_INFO(logger, "Done computing prob01 for synchronous_leader/leader6_8");
+
+    ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u);
+    ASSERT_EQ(prob01.second.getNumberOfSetBits(), 1312334u);
+}
+
+TEST(GraphAnalyzerTest, PerformProb01MinMax) {
+    storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew");
+	std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+    
+    LOG4CPLUS_INFO(logger, "Computing prob01min for asynchronous_leader/leader7");
+    std::pair<storm::storage::BitVector, storm::storage::BitVector> prob01 = storm::utility::GraphAnalyzer::performProb01Min(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected"));
+    LOG4CPLUS_INFO(logger, "Done computing prob01min for asynchronous_leader/leader7");
+    
+    ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u);
+    ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u);
+    
+    LOG4CPLUS_INFO(logger, "Computing prob01max for asynchronous_leader/leader7");
+    prob01 = storm::utility::GraphAnalyzer::performProb01Max(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected"));
+    LOG4CPLUS_INFO(logger, "Done computing prob01max for asynchronous_leader/leader7");
+
+    ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u);
+    ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u);
+
+    storm::parser::AutoParser<double> parser2(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "");
+	std::shared_ptr<storm::models::Mdp<double>> mdp2 = parser2.getModel<storm::models::Mdp<double>>();
+
+    LOG4CPLUS_INFO(logger, "Computing prob01min for consensus/coin4_6");
+    prob01 = storm::utility::GraphAnalyzer::performProb01Min(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished"));
+    LOG4CPLUS_INFO(logger, "Done computing prob01min for consensus/coin4_6");
+
+    ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u);
+    ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u);
+
+    LOG4CPLUS_INFO(logger, "Computing prob01max for consensus/coin4_6");
+    prob01 = storm::utility::GraphAnalyzer::performProb01Max(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished"));
+    LOG4CPLUS_INFO(logger, "Done computing prob01max for consensus/coin4_6");
+
+    ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u);
+    ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u);
+}
+
+TEST(GraphAnalyzerTest, PerformSCCDecomposition) {
+    storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+    
+    LOG4CPLUS_INFO(logger, "Computing SCC decomposition of crowds/crowds20_5.");
+    std::pair<std::vector<std::vector<uint_fast64_t>>, storm::storage::SparseMatrix<bool>> sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc);
+    LOG4CPLUS_INFO(logger, "Done computing SCC decomposition of crowds/crowds20_5.");
+    
+    ASSERT_EQ(sccDecomposition.first.size(), 1290297u);
+    ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 1371253u);
+    
+    storm::parser::AutoParser<double> parser2(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew");
+    std::shared_ptr<storm::models::Dtmc<double>> dtmc2 = parser2.getModel<storm::models::Dtmc<double>>();
+
+    LOG4CPLUS_INFO(logger, "Computing SCC decomposition of synchronous_leader/leader6_8");
+    sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc2);
+    LOG4CPLUS_INFO(logger, "Computing SCC decomposition of synchronous_leader/leader6_8.");
+
+    ASSERT_EQ(sccDecomposition.first.size(), 1279673u);
+    ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 1535367u);
+    
+    storm::parser::AutoParser<double> parser3(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew");
+	std::shared_ptr<storm::models::Mdp<double>> mdp = parser3.getModel<storm::models::Mdp<double>>();
+    
+    LOG4CPLUS_INFO(logger, "Computing SCC decomposition of asynchronous_leader/leader7");
+    sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*mdp);
+    LOG4CPLUS_INFO(logger, "Done computing SCC decomposition of asynchronous_leader/leader7");
+
+    ASSERT_EQ(sccDecomposition.first.size(), 1914691u);
+    ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 7023587u);
+    
+    storm::parser::AutoParser<double> parser4(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "");
+	std::shared_ptr<storm::models::Mdp<double>> mdp2 = parser4.getModel<storm::models::Mdp<double>>();
+
+    LOG4CPLUS_INFO(logger, "Computing SCC decomposition of consensus/coin4_6");
+    sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*mdp2);
+    LOG4CPLUS_INFO(logger, "Computing SCC decomposition of consensus/coin4_6");
+
+    ASSERT_EQ(sccDecomposition.first.size(), 63611u);
+    ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 213400u);
+}

test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp

@@ -1,6 +1,5 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
-
 #include "src/utility/Settings.h"
 #include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h"
 #include "src/parser/AutoParser.h"
@@ -14,8 +13,8 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
 
 	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
 
-	ASSERT_EQ(dtmc->getNumberOfStates(), 8607u);
-	ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460u);
+	ASSERT_EQ(dtmc->getNumberOfStates(), 2036647u);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 8973900u);
 
 	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
 
@@ -27,7 +26,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
 
 	ASSERT_NE(nullptr, result);
 
-	ASSERT_LT(std::abs((*result)[0] - 0.3328800375801578281), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[0] - 0.2296803699), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
@@ -40,7 +39,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
 
 	ASSERT_NE(nullptr, result);
 
-	ASSERT_LT(std::abs((*result)[0] - 0.1522173670950556501), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[0] - 0.05072232915), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
@@ -53,13 +52,13 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
 
 	ASSERT_NE(nullptr, result);
 
-	ASSERT_LT(std::abs((*result)[0] - 0.32153724292835045), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[0] - 0.2274230551), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
 }
 
-/*
+
 TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
 	storm::settings::Settings* s = storm::settings::instance();
 	s->set("fix-deadlocks");
@@ -69,8 +68,8 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
 
 	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
 
-	ASSERT_EQ(dtmc->getNumberOfStates(), 12400u);
-	ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894u);
+	ASSERT_EQ(dtmc->getNumberOfStates(), 1312334u);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810u);
 
 	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
 
@@ -95,7 +94,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
 
 	ASSERT_NE(nullptr, result);
 
-	ASSERT_LT(std::abs((*result)[0] - 0.9999965911265462636), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[0] - 0.999394979327824395376467), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
@@ -108,9 +107,8 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
 
 	ASSERT_NE(nullptr, result);
 
-	ASSERT_LT(std::abs((*result)[0] - 1.0448979591835938496), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[0] - 1.02521744572240791626427), s->get<double>("precision"));
 
 	delete rewardFormula;
 	delete result;
-}
-*/
+}

test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp

@@ -13,8 +13,8 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
 
 	std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
 
-	ASSERT_EQ(mdp->getNumberOfStates(), 3172u);
-	ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u);
+	ASSERT_EQ(mdp->getNumberOfStates(), 2095783u);
+	ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385u);
 
 	storm::modelchecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
 
@@ -52,7 +52,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
 
 	ASSERT_NE(nullptr, result);
 
-	ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[0] - 0), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
@@ -65,7 +65,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
 
 	ASSERT_NE(nullptr, result);
 
-	ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[0] - 0), s->get<double>("precision"));
 
 	delete probFormula;
 	delete result;
@@ -76,7 +76,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
 
 	result = mc.checkNoBoundOperator(*rewardFormula);
 
-	ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[0] - 6.172433512), s->get<double>("precision"));
 
 	delete rewardFormula;
 	delete result;
@@ -89,7 +89,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
 
 	ASSERT_NE(nullptr, result);
 
-	ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[0] - 6.1724344), s->get<double>("precision"));
 
 	delete rewardFormula;
 	delete result;
@@ -97,12 +97,15 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
 
 TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
 	storm::settings::Settings* s = storm::settings::instance();
-	storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.steps.state.rew", "");
+	storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.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(), 63616u);
+	ASSERT_EQ(mdp->getNumberOfTransitions(), 213472u);
+    
     storm::modelchecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
     
     storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("finished");
@@ -113,7 +116,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
     
 	ASSERT_NE(nullptr, result);
     
-	ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[31168] - 1), s->get<double>("precision"));
     
     delete probFormula;
     delete result;
@@ -128,7 +131,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
     
 	ASSERT_NE(nullptr, result);
     
-	ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[31168] - 0.4370098591707694546393), s->get<double>("precision"));
     
     delete probFormula;
     delete result;
@@ -137,13 +140,13 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
     apFormula2 = new storm::property::prctl::Ap<double>("all_coins_equal_1");
     andFormula = new storm::property::prctl::And<double>(apFormula, apFormula2);
     eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
     
 	result = mc.checkNoBoundOperator(*probFormula);
     
 	ASSERT_NE(nullptr, result);
     
-	ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[31168] - 0.5282872761373342829216), s->get<double>("precision"));
     
     delete probFormula;
     delete result;
@@ -153,13 +156,13 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
     storm::property::prctl::Not<double>* notFormula = new storm::property::prctl::Not<double>(apFormula2);
     andFormula = new storm::property::prctl::And<double>(apFormula, notFormula);
     eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
-	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
     
 	result = mc.checkNoBoundOperator(*probFormula);
     
 	ASSERT_NE(nullptr, result);
     
-	ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[31168] - 0.10343451035775527713), s->get<double>("precision"));
     
     delete probFormula;
     delete result;
@@ -172,7 +175,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
     
 	ASSERT_NE(nullptr, result);
     
-	ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[31168] - 0), s->get<double>("precision"));
     
     delete probFormula;
     delete result;
@@ -185,7 +188,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
     
 	ASSERT_NE(nullptr, result);
     
-	ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[31168] - 0), s->get<double>("precision"));
     
     delete probFormula;
     delete result;
@@ -196,7 +199,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
     
 	result = mc.checkNoBoundOperator(*rewardFormula);
     
-	ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[31168] - 1725.5933133943854045), s->get<double>("precision"));
     
 	delete rewardFormula;
 	delete result;
@@ -209,7 +212,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
     
 	ASSERT_NE(nullptr, result);
     
-	ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[31168] - 2179.014847073392047605011), s->get<double>("precision"));
     
 	delete rewardFormula;
 	delete result;

test/performance/storm-performance-tests.cpp

@@ -15,10 +15,12 @@ log4cplus::Logger logger;
  * Initializes the logging framework.
  */
 void setUpLogging() {
-	log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-functional-tests.log"));
+	logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main"));
+	logger.setLogLevel(log4cplus::INFO_LOG_LEVEL);
+	log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-performance-tests.log"));
 	fileLogAppender->setName("mainFileAppender");
+	fileLogAppender->setThreshold(log4cplus::WARN_LOG_LEVEL);
 	fileLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M} (%r ms) - %F:%L : %m%n")));
-	logger = log4cplus::Logger::getInstance("mainLogger");
 	logger.addAppender(fileLogAppender);
 
 	// Uncomment these lines to enable console logging output