diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index f658268e9..8d950c4ef 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp @@ -363,14 +363,19 @@ namespace storm { } } - storm::storage::BitVector statesWithNegativeRewardForAllChoices(data.preprocessedModel.getNumberOfStates(), true); + storm::storage::BitVector statesWithNegativeRewardForAllChoices(data.preprocessedModel.getNumberOfStates(), false); + storm::storage::BitVector submatrixRows = actionsWithNonNegativeReward; for(uint_fast64_t state = 0; state < data.preprocessedModel.getNumberOfStates(); ++state) { // state has negative reward for all choices iff there is no bit set in actionsWithNonNegativeReward for all actions of state - statesWithNegativeRewardForAllChoices.set(state, actionsWithNonNegativeReward.getNextSetIndex(data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]) >= data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]); + if(actionsWithNonNegativeReward.getNextSetIndex(data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]) >= data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]) { + statesWithNegativeRewardForAllChoices.set(state, true); + // enable one row for the current state to avoid deleting the row group + submatrixRows.set(data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state], true); + } } + storm::storage::SparseMatrix transitionsWithNonNegativeReward = data.preprocessedModel.getTransitionMatrix().restrictRows(submatrixRows); storm::storage::BitVector allStates(data.preprocessedModel.getNumberOfStates(), true); - storm::storage::SparseMatrix transitionsWithNonNegativeReward = data.preprocessedModel.getTransitionMatrix().restrictRows(actionsWithNonNegativeReward); storm::storage::BitVector statesNeverReachingNegativeRewardForSomeScheduler = storm::utility::graph::performProb0E(transitionsWithNonNegativeReward, transitionsWithNonNegativeReward.getRowGroupIndices(), transitionsWithNonNegativeReward.transpose(true), allStates, statesWithNegativeRewardForAllChoices); storm::storage::BitVector statesReachingNegativeRewardsFinitelyOftenForSomeScheduler = storm::utility::graph::performProb1E(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), data.preprocessedModel.getBackwardTransitions(), allStates, statesNeverReachingNegativeRewardForSomeScheduler); if((statesReachingNegativeRewardsFinitelyOftenForSomeScheduler & data.preprocessedModel.getInitialStates()).empty()) { diff --git a/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp index c7bb0979e..08605d2de 100644 --- a/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp @@ -76,6 +76,10 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, preprocessorResultsTest) { formulasAsString += "; \n multi(Rmax=? [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) "; formulasAsString += "; \n multi(R>=300 [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) "; formulasAsString += "; \n multi(R<10 [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) "; + formulasAsString += "; \n multi(Rmin=? [ C ]) "; + formulasAsString += "; \n multi(Rmax=? [ C ]) "; + formulasAsString += "; \n multi(R>1 [ C ]) "; + formulasAsString += "; \n multi(R<1 [ C ]) "; // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); @@ -119,6 +123,21 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, preprocessorResultsTest) { ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + result = checker.check(storm::modelchecker::CheckTask(*formulas[8], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::infinity(), result->asExplicitQuantitativeCheckResult()[initState]); + + result = checker.check(storm::modelchecker::CheckTask(*formulas[9], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::infinity(), result->asExplicitQuantitativeCheckResult()[initState]); + + result = checker.check(storm::modelchecker::CheckTask(*formulas[10], true)); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + + result = checker.check(storm::modelchecker::CheckTask(*formulas[11], true)); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMdpMultiObjectiveModelCheckerTest, consensus) { @@ -187,8 +206,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, zeroconfTb) { std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/zeroconf-tb/zeroconf-tb2_14.nm"; std::string formulasAsString = " multi(Pmax=? [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // numerical - formulasAsString += "; \n multi(Pmax>=0.00000008 [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // achievability (true) - formulasAsString += "; \n multi(Pmax>=0.000000081 [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // achievability (false) + formulasAsString += "; \n multi(P>=0.00000008 [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // achievability (true) + formulasAsString += "; \n multi(P>=0.000000081 [ F time_error=1 ] , P>=0.81[ G (error=0) ])"; // achievability (false) // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); @@ -218,8 +237,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, team3with2objectives) { std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/team/team2obj_3.nm"; std::string formulasAsString = " multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // numerical - formulasAsString += "; \n multi(Pmax>=0.871 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // achievability (true) - formulasAsString += "; \n multi(Pmax>=0.872 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // achievability (false) + formulasAsString += "; \n multi(P>=0.871 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // achievability (true) + formulasAsString += "; \n multi(P>=0.872 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ])"; // achievability (false) // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); @@ -249,8 +268,8 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, team3with3objectives) { std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/team/team3obj_3.nm"; std::string formulasAsString = "multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // numerical - formulasAsString += "; \n multi(Pmax>=0.744 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // achievability (true) - formulasAsString += "; \n multi(Pmax>=0.745 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // achievability (false) + formulasAsString += "; \n multi(P>=0.744 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // achievability (true) + formulasAsString += "; \n multi(P>=0.745 [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // achievability (false) // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); diff --git a/test/functional/modelchecker/multiobjective2.nm b/test/functional/modelchecker/multiobjective2.nm index c82411378..3df5018f5 100644 --- a/test/functional/modelchecker/multiobjective2.nm +++ b/test/functional/modelchecker/multiobjective2.nm @@ -15,5 +15,6 @@ endmodule rewards "rew" [A] true : 10; [C] true : 3; + [E] true : 1; endrewards