More testcases for multi-objective model checking with scheduler restrictions (including fixes).

resources/examples/testfiles/mdp/multiobj_compromise.nm

@@ -0,0 +1,13 @@
+mdp
+module main
+	
+	x : [0..3];
+	[l] x=0 -> 0.5 : (x'=1) + 0.5 : (x'=0);
+	[r] x=0 -> (x'=2);
+	[c] x=0 -> 0.3 : (x'=1) + 0.3 : (x'=2) + 0.4 : (x'=3);
+	[] x=1 -> (x'=0);
+endmodule
+
+rewards "test"
+	[l] true : 1;
+endrewards

resources/examples/testfiles/mdp/multiobj_mecs.nm

@@ -0,0 +1,20 @@
+mdp
+const double p1 = 0.5;
+const double p2 = 0.5;
+module main
+	
+	x : [0..4];
+	
+	[] x=0 -> p1 : (x'=1) + (1-p1) : (x'=3);
+	[up] x>=1 & x<=3 -> (x'=x+1);
+	[down] x>=2 & x<=3 -> (x'=1);
+endmodule
+
+label "t1" = x=4;
+label "t2" = x=3;
+
+rewards "test"
+	[down] x=2: 27;
+	[up] x=3: 2;
+endrewards
+

src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp

@@ -185,33 +185,19 @@ namespace storm {
                 // To compute l, we multiply the smallest transition probabilities occurring at each state and MEC-Choice
                 // as well as the smallest 'exit' probability
                 ValueType lpath = storm::utility::one<ValueType>();
-                ValueType minExitProbability = storm::utility::one<ValueType>();
                 for (auto const& stateChoices : ec) {
-                    auto state = stateChoices.first;
                     ValueType minProb = storm::utility::one<ValueType>();
-                    for (uint64_t choice = transitions.getRowGroupIndices()[state]; choice < transitions.getRowGroupIndices()[state + 1]; ++choice) {
-                        if (stateChoices.second.count(choice) == 0) {
-                            // The choice leaves the EC, so we take the sum over the exiting probabilities
-                            ValueType exitProbabilitySum = storm::utility::zero<ValueType>();
-                            for (auto const& transition : transitions.getRow(choice)) {
-                                if (!ec.containsState(transition.getColumn())) {
-                                    exitProbabilitySum += transition.getValue();
-                                }
-                            }
-                            minExitProbability = std::min(minExitProbability, exitProbabilitySum);
-                        } else {
-                            // Get the minimum over all transition probabilities
-                            for (auto const& transition : transitions.getRow(choice)) {
-                                if (!storm::utility::isZero(transition.getValue())) {
-                                    minProb = std::min(minProb, transition.getValue());
-                                }
+                    // Choices that leave the EC are not considered in the in[s] below. Hence, also do not need to consider them here.
+                    for (auto const& choice : stateChoices.second) {
+                        // Get the minimum over all transition probabilities
+                        for (auto const& transition : transitions.getRow(choice)) {
+                            if (!storm::utility::isZero(transition.getValue())) {
+                                minProb = std::min(minProb, transition.getValue());
                             }
-                            
                         }
                     }
                     lpath *= minProb;
                 }
-                lpath *= minExitProbability;
                 ValueType expVisitsUpperBound = storm::utility::one<ValueType>() / lpath;
                 STORM_LOG_WARN_COND(expVisitsUpperBound <= storm::utility::convertNumber<ValueType>(1000.0), "Large upper bound for expected visiting times: " << expVisitsUpperBound);
                 // create variables

src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp

@@ -493,7 +493,7 @@ namespace storm {
                         negateMinObjectives(point);
                     } else {
                         lpChecker->setCurrentWeightVector(env, weightVector);
-                        auto optionalPoint = lpChecker->check(env, negateMinObjectives(this->overApproximation));
+                        auto optionalPoint = lpChecker->check(env, overApproximation);
                         STORM_LOG_THROW(optionalPoint.is_initialized(), storm::exceptions::UnexpectedException, "Unable to find a point in the current overapproximation.");
                         point = std::move(optionalPoint.get());
                     }

src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp

@@ -151,7 +151,7 @@ namespace storm {
                                 storm::storage::BitVector statesWithoutReward = rewardModel.get().getStatesWithZeroReward(model->getTransitionMatrix());
                                 absorbingStatesForSubformula = storm::utility::graph::performProb0A(backwardTransitions, statesWithoutReward, ~statesWithoutReward);
                             } else if (pathFormula.isTotalRewardFormula()) {
-                                auto rewardModel = storm::utility::createFilteredRewardModel(baseRewardModel, model->isDiscreteTimeModel(), pathFormula.asCumulativeRewardFormula());
+                                auto rewardModel = storm::utility::createFilteredRewardModel(baseRewardModel, model->isDiscreteTimeModel(), pathFormula.asTotalRewardFormula());
                                 storm::storage::BitVector statesWithoutReward = rewardModel.get().getStatesWithZeroReward(model->getTransitionMatrix());
                                 absorbingStatesForSubformula = storm::utility::graph::performProb0A(backwardTransitions, statesWithoutReward, ~statesWithoutReward);
                             } else {

src/test/storm/modelchecker/MultiObjectiveSchedRestModelCheckerTest.cpp

@@ -16,7 +16,7 @@
 #include "storm/api/storm.h"
 #include "storm-parsers/api/storm-parsers.h"
 #include "storm/environment/Environment.h"
-
+#include "storm/exceptions/InvalidOperationException.h"
 
 namespace {
     
@@ -26,6 +26,12 @@ namespace {
         return env;
     }
     
+    storm::Environment getGoalDeterministicEnvironment() {
+        storm::Environment env;
+        env.modelchecker().multi().setSchedulerRestriction(storm::storage::SchedulerClass().setMemoryPattern(storm::storage::SchedulerClass::MemoryPattern::GoalMemory).setIsDeterministic());
+        return env;
+    }
+    
     typedef std::vector<storm::RationalNumber> Point;
     
     std::vector<Point> parsePoints(std::vector<std::string> const& input) {
@@ -81,9 +87,8 @@ namespace {
     }
     
     TEST(MultiObjectiveSchedRestModelCheckerTest, steps) {
-        storm::Environment env = getPositionalDeterministicEnvironment();
         
-        std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multi-obj_stairs.nm";
+        std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_stairs.nm";
         std::string constantsString = "N=3";
         std::string formulasAsString = "multi(Pmax=? [ F y=1], Pmax=? [ F y=2 ])";
         
@@ -95,14 +100,299 @@ namespace {
         std::vector<Point> expected, actual;
         std::set<Point> incorrectPoints, missingPoints;
         std::unique_ptr<storm::modelchecker::CheckResult> result;
+        
+        storm::Environment env = getPositionalDeterministicEnvironment();
+        
         expected = parsePoints({"0.875,0", "0,0.875", "0.125,0.75", "0.25,0.625", "0.375,0.5", "0.5,0.375", "0.625,0.25", "0.75,0.125"});
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow);
         result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
         ASSERT_TRUE(result->isParetoCurveCheckResult());
         actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
         missingPoints = setMinus(expected, actual);
-        ASSERT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+    }
+    
+    TEST(MultiObjectiveSchedRestModelCheckerTest, mecs) {
+        
+        std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_mecs.nm";
+        std::string constantsString = "";
+        std::string formulasAsString = "multi(Pmin=? [ F x=3], Pmax=? [ F x=4 ]);";
+        formulasAsString += "\nmulti(R{\"test\"}min=? [C], Pmin=? [F \"t1\"]);";
+        formulasAsString += "\nmulti(R{\"test\"}min=? [C], Pmin=? [F \"t2\"]);";
+        formulasAsString += "\nmulti(R{\"test\"}min=? [C], Pmin=? [F \"t2\"], Pmax=? [F \"t1\"]);";
+        // programm, model, formula
+        storm::prism::Program program = storm::api::parseProgram(programFile);
+        program = storm::utility::prism::preprocess(program, constantsString);
+        std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+        std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
+        std::vector<Point> expected, actual;
+        std::set<Point> incorrectPoints, missingPoints;
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        
+        storm::Environment env = getPositionalDeterministicEnvironment();
+        
+        uint64_t formulaIndex = 0;
+        expected = parsePoints({"0.5,0.5","1,1"});
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow);
+        EXPECT_THROW(storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula()), storm::exceptions::InvalidOperationException);
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        
+        ++formulaIndex;
+        expected = parsePoints({"0,0"});
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow);
+
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        
+        ++formulaIndex;
+        expected = parsePoints({"0,1"});
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow);
+        EXPECT_THROW(storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula()), storm::exceptions::InvalidOperationException);
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        
+        ++formulaIndex;
+        expected = parsePoints({"0,1,0", "2,1,1"});
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow);
+        EXPECT_THROW(storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula()), storm::exceptions::InvalidOperationException);
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
         incorrectPoints = setMinus(actual, expected);
-        ASSERT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+    }
+    
+    TEST(MultiObjectiveSchedRestModelCheckerTest, compromise) {
+        
+        std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_compromise.nm";
+        std::string constantsString = "";
+        std::string formulasAsString = "multi(Pmax=? [ F x=1], Pmax=? [ F x=2 ]);";
+        formulasAsString += "\nmulti(R{\"test\"}min=? [F x=1], Pmax=? [F x=1 ]);";
+        formulasAsString += "\nmulti(Pmax=? [F x=1], Pmax=? [F x=2 ], Pmax=? [F x=3 ]);";
+        formulasAsString += "\nmulti(R{\"test\"}min=? [C], Pmin=? [F x=2 ], Pmin=? [F x=3]);";
+        // programm, model, formula
+        storm::prism::Program program = storm::api::parseProgram(programFile);
+        program = storm::utility::prism::preprocess(program, constantsString);
+        std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+        std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
+        std::vector<Point> expected, actual;
+        std::set<Point> incorrectPoints, missingPoints;
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        
+        storm::Environment env = getPositionalDeterministicEnvironment();
+        
+        uint64_t formulaIndex = 0;
+        expected = parsePoints({"1,0","0,1", "0.3,3/7"});
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow);
+        EXPECT_THROW(storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula()), storm::exceptions::InvalidOperationException);
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        
+        ++formulaIndex;
+        expected = parsePoints({"0,0.3","2,1"});
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+  
+        ++formulaIndex;
+        expected = parsePoints({"1,0,0","0,1,0","0.3,3/7,4/7"});
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow);
+        EXPECT_THROW(storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula()), storm::exceptions::InvalidOperationException);
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+  
+        ++formulaIndex;
+        expected = parsePoints({"0,1,0","0,3/7,4/7"});
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        env = getGoalDeterministicEnvironment();
+        
+        formulaIndex = 0;
+        expected = parsePoints({"1,1"});
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        ++formulaIndex;
+        expected = parsePoints({"0,0.3","2,1"});
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+  
+        ++formulaIndex;
+        expected = parsePoints({"1,1,0","1,3/7,4/7"});
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+
+        ++formulaIndex;
+        expected = parsePoints({"0,1,0","0,3/7,4/7"});
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
+        env.modelchecker().multi().setEncodingType(storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic);
+        result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula());
+        ASSERT_TRUE(result->isParetoCurveCheckResult());
+        actual = result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getPoints();
+        missingPoints = setMinus(expected, actual);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the expected solution are missing:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        incorrectPoints = setMinus(actual, expected);
+        EXPECT_TRUE(incorrectPoints.empty()) << "Some points of the returned solution are not expected:" << std::endl << "Expected:" << std::endl << toString(expected, true) << "Actual:" << std::endl << toString(actual, true);
+        
     }
 }