Added functional test for the SparseMdpPrctlModelChecker. Fixed performance tests.

test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

@@ -0,0 +1,259 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "src/utility/Settings.h"
+#include "src/modelchecker/SparseMdpPrctlModelChecker.h"
+#include "src/parser/AutoParser.h"
+
+TEST(SparseMdpPrctlModelCheckerTest, Dice) {
+	storm::settings::Settings* s = storm::settings::instance();
+	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(), 169u);
+	ASSERT_EQ(mdp->getNumberOfTransitions(), 436u);
+    
+	storm::modelchecker::SparseMdpPrctlModelChecker<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_NE(nullptr, result);
+	ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get<double>("precision"));
+    
+	delete probFormula;
+	delete result;
+    
+	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->get<double>("precision"));
+    
+	delete probFormula;
+	delete result;
+    
+	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->get<double>("precision"));
+    
+	delete probFormula;
+	delete result;
+    
+	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->get<double>("precision"));
+    
+	delete probFormula;
+	delete result;
+    
+	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->get<double>("precision"));
+    
+	delete probFormula;
+	delete result;
+    
+	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->get<double>("precision"));
+    
+	delete probFormula;
+	delete result;
+    
+	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.3333294987678527832), s->get<double>("precision"));
+    
+	delete rewardFormula;
+	delete result;
+    
+	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.3333294987678527832), s->get<double>("precision"));
+    
+	delete rewardFormula;
+	delete result;
+    
+	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::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp);
+    
+	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.3333294987678527832), s->get<double>("precision"));
+    
+	delete rewardFormula;
+	delete result;
+    
+	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.3333294987678527832), s->get<double>("precision"));
+    
+	delete rewardFormula;
+	delete result;
+    
+	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::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
+    
+	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] - (2 * 7.3333294987678527832)), s->get<double>("precision"));
+    
+	delete rewardFormula;
+	delete result;
+    
+	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] - (2 * 7.3333294987678527832)), s->get<double>("precision"));
+    
+	delete rewardFormula;
+	delete result;
+}
+
+TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
+	storm::settings::Settings* s = storm::settings::instance();
+	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(), 3172u);
+	ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u);
+
+	storm::modelchecker::SparseMdpPrctlModelChecker<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_NE(nullptr, result);
+
+	ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	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_NE(nullptr, result);
+
+	ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	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, true);
+
+	result = mc.checkNoBoundOperator(*probFormula);
+
+	ASSERT_NE(nullptr, result);
+
+	ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	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, false);
+
+	result = mc.checkNoBoundOperator(*probFormula);
+
+	ASSERT_NE(nullptr, result);
+
+	ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	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.28568908480604982), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+
+	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_NE(nullptr, result);
+
+	ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+}

test/functional/storm-functional-tests.cpp

@@ -31,39 +31,21 @@ void setUpLogging() {
 }
 
 /*!
- * Function that parses the command line options.
- * @param argc The argc argument of main().
- * @param argv The argv argument of main().
- * @return True iff the program should continue to run after parsing the options.
+ * Creates an empty settings object as the standard instance of the Settings class.
  */
-bool parseOptions(int const argc, char const * const argv[]) {
-    storm::settings::Settings* s = nullptr;
-    try {
-        storm::settings::Settings::registerModule<storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>>();
-        s = storm::settings::newInstance(argc, argv, nullptr, true);
-    } catch (storm::exceptions::InvalidSettingsException& e) {
-        std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
-        std::cout << std::endl << storm::settings::help;
-        return false;
-    }
-    
-    if (s->isSet("help")) {
-        std::cout << storm::settings::help;
-        return false;
-    }
-    
-    return true; 
+void createEmptyOptions() {
+    storm::settings::Settings::registerModule<storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>>();
+    const char* newArgv[] = {"storm-performance-tests"};
+    storm::settings::Settings* s = storm::settings::newInstance(1, newArgv, nullptr, true);
 }
 
 int main(int argc, char* argv[]) {
 	setUpLogging();
-	if (!parseOptions(argc, argv)) {
-		return 0;
-	}
+	createEmptyOptions();
 	std::cout << "StoRM (Functional) Testing Suite" << std::endl;
 	
 	testing::InitGoogleTest(&argc, argv);
-
+    
     int result = RUN_ALL_TESTS();
     
     logger.closeNestedAppenders();

test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp

@@ -4,7 +4,7 @@
 #include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h"
 #include "src/parser/AutoParser.h"
 
-TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
+TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
 	storm::settings::Settings* s = storm::settings::instance();
 	s->set("fix-deadlocks");
 	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", "", "");
@@ -65,7 +65,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
 }
 
 
-TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
+TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
 	storm::settings::Settings* s = storm::settings::instance();
 	s->set("fix-deadlocks");
 	storm::parser::AutoParser<double> parser(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");

test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp

@@ -5,7 +5,7 @@
 #include "src/modelchecker/GmmxxMdpPrctlModelChecker.h"
 #include "src/parser/AutoParser.h"
 
-TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
+TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
 	storm::settings::Settings* s = storm::settings::instance();
 	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");
 
@@ -107,7 +107,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
 	delete result;
 }
 
-TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
+TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) {
 	storm::settings::Settings* s = storm::settings::instance();
     s->set<unsigned>("maxiter", 20000);
     
@@ -164,8 +164,8 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
 	result = mc.checkNoBoundOperator(*probFormula);
     LOG4CPLUS_WARN(logger, "Done.");
     
-	ASSERT_NE(nullptr, result);
-	ASSERT_LT(std::abs((*result)[31168] - 0.5282872761373342829216), s->get<double>("precision"));
+	ASSERT_NE(nullptr, result);    
+	ASSERT_LT(std::abs((*result)[31168] - 0.52932863686144482340267813924583606421947479248047), s->get<double>("precision"));
     
     delete probFormula;
     delete result;
@@ -182,7 +182,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
     LOG4CPLUS_WARN(logger, "Done.");
     
 	ASSERT_NE(nullptr, result);
-	ASSERT_LT(std::abs((*result)[31168] - 0.10343451035775527713), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[31168] - 0.1041409700076474653673841), s->get<double>("precision"));
     
     delete probFormula;
     delete result;
@@ -238,7 +238,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
     LOG4CPLUS_WARN(logger, "Done.");
     
 	ASSERT_NE(nullptr, result);
-	ASSERT_LT(std::abs((*result)[31168] - 2179.014847073392047605011), s->get<double>("precision"));
+	ASSERT_LT(std::abs((*result)[31168] - 2183.1424220082612919213715), s->get<double>("precision"));
     
 	delete rewardFormula;
 	delete result;

test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

@@ -0,0 +1,244 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "src/utility/Settings.h"
+#include "src/modelchecker/SparseMdpPrctlModelChecker.h"
+#include "src/parser/AutoParser.h"
+
+TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
+	storm::settings::Settings* s = storm::settings::instance();
+	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");
+
+	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(), 2095783u);
+	ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385u);
+
+	storm::modelchecker::SparseMdpPrctlModelChecker<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);
+
+    LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F elected] on asynchronous_leader/leader7...");
+	std::vector<double>* result = mc.checkNoBoundOperator(*probFormula);
+    LOG4CPLUS_WARN(logger, "Done.");
+
+	ASSERT_NE(nullptr, result);
+	ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	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);
+
+    LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F elected] on asynchronous_leader/leader7...");
+	result = mc.checkNoBoundOperator(*probFormula);
+    LOG4CPLUS_WARN(logger, "Done.");
+
+	ASSERT_NE(nullptr, result);
+
+	ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	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, true);
+
+    LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F<=25 elected] on asynchronous_leader/leader7...");
+	result = mc.checkNoBoundOperator(*probFormula);
+    LOG4CPLUS_WARN(logger, "Done.");
+
+	ASSERT_NE(nullptr, result);
+
+	ASSERT_LT(std::abs((*result)[0] - 0), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	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, false);
+
+    LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F<=25 elected] on asynchronous_leader/leader7...");
+	result = mc.checkNoBoundOperator(*probFormula);
+    LOG4CPLUS_WARN(logger, "Done.");
+
+	ASSERT_NE(nullptr, result);
+	ASSERT_LT(std::abs((*result)[0] - 0), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	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);
+
+    LOG4CPLUS_WARN(logger, "Model Checking Rmin=? [F elected] on asynchronous_leader/leader7...");
+	result = mc.checkNoBoundOperator(*rewardFormula);
+    LOG4CPLUS_WARN(logger, "Done.");
+
+	ASSERT_LT(std::abs((*result)[0] - 6.172433512), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+
+	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);
+
+    LOG4CPLUS_WARN(logger, "Model Checking Rmax=? [F elected] on asynchronous_leader/leader7...");
+	result = mc.checkNoBoundOperator(*rewardFormula);
+    LOG4CPLUS_WARN(logger, "Done");
+
+	ASSERT_NE(nullptr, result);
+
+	ASSERT_LT(std::abs((*result)[0] - 6.1724344), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+}
+
+TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
+	storm::settings::Settings* s = storm::settings::instance();
+    // Increase the maximal number of iterations, because the solver does not converge otherwise.
+    s->set<unsigned>("maxiter", 20000);
+    
+	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::SparseMdpPrctlModelChecker<double> mc(*mdp);
+    
+    storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("finished");
+	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);
+    
+    LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F finished] on consensus/coin4_6...");
+	std::vector<double>* result = mc.checkNoBoundOperator(*probFormula);
+    LOG4CPLUS_WARN(logger, "Done.");
+    
+	ASSERT_NE(nullptr, result);
+    
+	ASSERT_LT(std::abs((*result)[31168] - 1), s->get<double>("precision"));
+    
+    delete probFormula;
+    delete result;
+    
+    apFormula = new storm::property::prctl::Ap<double>("finished");
+    storm::property::prctl::Ap<double>* apFormula2 = new storm::property::prctl::Ap<double>("all_coins_equal_0");
+    storm::property::prctl::And<double>* 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);
+    
+    LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F finished & all_coins_equal_0] on consensus/coin4_6...");
+	result = mc.checkNoBoundOperator(*probFormula);
+    LOG4CPLUS_WARN(logger, "Done.");
+    
+	ASSERT_NE(nullptr, result);
+	ASSERT_LT(std::abs((*result)[31168] - 0.43742828319177884388579), s->get<double>("precision"));
+    
+    delete probFormula;
+    delete result;
+    
+    apFormula = new storm::property::prctl::Ap<double>("finished");
+    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, false);
+    
+    LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F finished & all_coins_equal_1] on consensus/coin4_6...");
+	result = mc.checkNoBoundOperator(*probFormula);
+    LOG4CPLUS_WARN(logger, "Done.");
+    
+	ASSERT_NE(nullptr, result);    
+	ASSERT_LT(std::abs((*result)[31168] - 0.52932863686144482340267813924583606421947479248047), s->get<double>("precision"));
+    
+    delete probFormula;
+    delete result;
+    
+    apFormula = new storm::property::prctl::Ap<double>("finished");
+    apFormula2 = new storm::property::prctl::Ap<double>("agree");
+    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, false);
+    
+    LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F finished & !agree] on consensus/coin4_6...");
+	result = mc.checkNoBoundOperator(*probFormula);
+    LOG4CPLUS_WARN(logger, "Done.");
+    
+	ASSERT_NE(nullptr, result);
+	ASSERT_LT(std::abs((*result)[31168] - 0.1041409700076474653673841), s->get<double>("precision"));
+    
+    delete probFormula;
+    delete result;
+    
+    apFormula = new storm::property::prctl::Ap<double>("finished");
+	storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50);
+	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
+    
+    LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F<=50 finished] on consensus/coin4_6...");
+	result = mc.checkNoBoundOperator(*probFormula);
+    LOG4CPLUS_WARN(logger, "Done.");
+    
+	ASSERT_NE(nullptr, result);
+	ASSERT_LT(std::abs((*result)[31168] - 0), s->get<double>("precision"));
+    
+    delete probFormula;
+    delete result;
+    
+    apFormula = new storm::property::prctl::Ap<double>("finished");
+	boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50);
+	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
+    
+    LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F<=50 finished] on consensus/coin4_6...");
+	result = mc.checkNoBoundOperator(*probFormula);
+    LOG4CPLUS_WARN(logger, "Done.");
+    
+	ASSERT_NE(nullptr, result);
+	ASSERT_LT(std::abs((*result)[31168] - 0), s->get<double>("precision"));
+    
+    delete probFormula;
+    delete result;
+    
+    apFormula = new storm::property::prctl::Ap<double>("finished");
+	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);
+    
+    LOG4CPLUS_WARN(logger, "Model Checking Rmin=? [F finished] on consensus/coin4_6...");
+	result = mc.checkNoBoundOperator(*rewardFormula);
+    LOG4CPLUS_WARN(logger, "Done.");
+    
+    ASSERT_NE(nullptr, result);
+	ASSERT_LT(std::abs((*result)[31168] - 1725.5933133943854045), s->get<double>("precision"));
+    
+	delete rewardFormula;
+	delete result;
+    
+	apFormula = new storm::property::prctl::Ap<double>("finished");
+	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+    
+    LOG4CPLUS_WARN(logger, "Model Checking Rmax=? [F finished] on consensus/coin4_6...");
+	result = mc.checkNoBoundOperator(*rewardFormula);
+    LOG4CPLUS_WARN(logger, "Done.");
+    
+	ASSERT_NE(nullptr, result);
+	ASSERT_LT(std::abs((*result)[31168] - 2183.1424220082612919213715), s->get<double>("precision"));
+    
+	delete rewardFormula;
+	delete result;
+
+}

test/performance/storm-performance-tests.cpp

@@ -31,34 +31,17 @@ void setUpLogging() {
 }
 
 /*!
- * Function that parses the command line options.
- * @param argc The argc argument of main().
- * @param argv The argv argument of main().
- * @return True iff the program should continue to run after parsing the options.
+ * Creates an empty settings object as the standard instance of the Settings class.
  */
-bool parseOptions(int const argc, char const * const argv[]) {
-    storm::settings::Settings* s = nullptr;
-    try {
-        storm::settings::Settings::registerModule<storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>>();
-        s = storm::settings::newInstance(argc, argv, nullptr, true);
-    } catch (storm::exceptions::InvalidSettingsException& e) {
-        // Ignore this case.
-        return true;
-    }
-    
-    if (s->isSet("help")) {
-        std::cout << storm::settings::help;
-        return false;
-    }
-    
-    return true; 
+void createEmptyOptions() {
+    storm::settings::Settings::registerModule<storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>>();
+    const char* newArgv[] = {"storm-performance-tests"};
+    storm::settings::Settings* s = storm::settings::newInstance(1, newArgv, nullptr, true);
 }
 
 int main(int argc, char* argv[]) {
 	setUpLogging();
-	if (!parseOptions(argc, argv)) {
-		return 0;
-	}
+	createEmptyOptions();
 	std::cout << "StoRM (Performance) Testing Suite" << std::endl;
 	
 	testing::InitGoogleTest(&argc, argv);