From 2fed3b647c418f940400fddd1278644aae1a12d5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 19 Jun 2016 12:35:50 +0200 Subject: [PATCH] scheduler benchmark now considers expected reachability reward (total reward was infinite). Bugfix. Former-commit-id: f53d19194cfe42be23b82325b9e7150cc4cc4937 --- .../mdp/scheduler/scheduler05_numerical.pctl | 5 +- .../mdp/scheduler/scheduler05_pareto.pctl | 5 +- .../mdp/scheduler/scheduler25_numerical.pctl | 5 +- .../mdp/scheduler/scheduler25_pareto.pctl | 5 +- .../mdp/scheduler/scheduler50_numerical.pctl | 5 +- .../mdp/scheduler/scheduler50_pareto.pctl | 5 +- .../SparseMultiObjectivePreprocessor.cpp | 46 ++++++++++++++----- 7 files changed, 58 insertions(+), 18 deletions(-) diff --git a/examples/multi-objective/mdp/scheduler/scheduler05_numerical.pctl b/examples/multi-objective/mdp/scheduler/scheduler05_numerical.pctl index 09581f07f..47ab6d61e 100644 --- a/examples/multi-objective/mdp/scheduler/scheduler05_numerical.pctl +++ b/examples/multi-objective/mdp/scheduler/scheduler05_numerical.pctl @@ -1 +1,4 @@ - multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) \ No newline at end of file +multi(R{"time"}min=?[ F "tasks_complete" ], R{"energy"}<=1.45 [ F "tasks_complete" ]) +// Original query: +//multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) +// Note that the min values are actually infinity and prism (currently) gives wrong results for this, e.g., R{"time"}min=?[ C<=2000 ] gives a larger value than multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) . \ No newline at end of file diff --git a/examples/multi-objective/mdp/scheduler/scheduler05_pareto.pctl b/examples/multi-objective/mdp/scheduler/scheduler05_pareto.pctl index 36ce7ae23..494a78895 100644 --- a/examples/multi-objective/mdp/scheduler/scheduler05_pareto.pctl +++ b/examples/multi-objective/mdp/scheduler/scheduler05_pareto.pctl @@ -1 +1,4 @@ - multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) + multi(R{"energy"}min=?[ F "tasks_complete" ], R{"time"}min=? [ F "tasks_complete" ]) + // Original query: + //multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) +// Note that the min values are actually infinity and prism (currently) gives wrong results for this, e.g., R{"time"}min=?[ C<=2000 ] gives a larger value than multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) . \ No newline at end of file diff --git a/examples/multi-objective/mdp/scheduler/scheduler25_numerical.pctl b/examples/multi-objective/mdp/scheduler/scheduler25_numerical.pctl index 09581f07f..6d91107a4 100644 --- a/examples/multi-objective/mdp/scheduler/scheduler25_numerical.pctl +++ b/examples/multi-objective/mdp/scheduler/scheduler25_numerical.pctl @@ -1 +1,4 @@ - multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) \ No newline at end of file + multi(R{"time"}min=?[ F "tasks_complete" ], R{"energy"}<=1.45 [ F "tasks_complete" ]) +// Original query: +// multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) +// Note that the min values are actually infinity and prism (currently) gives wrong results for this, e.g., R{"time"}min=?[ C<=2000 ] gives a larger value than multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) . \ No newline at end of file diff --git a/examples/multi-objective/mdp/scheduler/scheduler25_pareto.pctl b/examples/multi-objective/mdp/scheduler/scheduler25_pareto.pctl index 36ce7ae23..a9188a837 100644 --- a/examples/multi-objective/mdp/scheduler/scheduler25_pareto.pctl +++ b/examples/multi-objective/mdp/scheduler/scheduler25_pareto.pctl @@ -1 +1,4 @@ - multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) + multi(R{"energy"}min=?[ F "tasks_complete" ], R{"time"}min=? [ F "tasks_complete" ]) +// Original query: +// multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) +// Note that the min values are actually infinity and prism (currently) gives wrong results for this, e.g., R{"time"}min=?[ C<=2000 ] gives a larger value than multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) . \ No newline at end of file diff --git a/examples/multi-objective/mdp/scheduler/scheduler50_numerical.pctl b/examples/multi-objective/mdp/scheduler/scheduler50_numerical.pctl index 09581f07f..6d91107a4 100644 --- a/examples/multi-objective/mdp/scheduler/scheduler50_numerical.pctl +++ b/examples/multi-objective/mdp/scheduler/scheduler50_numerical.pctl @@ -1 +1,4 @@ - multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) \ No newline at end of file + multi(R{"time"}min=?[ F "tasks_complete" ], R{"energy"}<=1.45 [ F "tasks_complete" ]) +// Original query: +// multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) +// Note that the min values are actually infinity and prism (currently) gives wrong results for this, e.g., R{"time"}min=?[ C<=2000 ] gives a larger value than multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) . \ No newline at end of file diff --git a/examples/multi-objective/mdp/scheduler/scheduler50_pareto.pctl b/examples/multi-objective/mdp/scheduler/scheduler50_pareto.pctl index 36ce7ae23..74bd8ba03 100644 --- a/examples/multi-objective/mdp/scheduler/scheduler50_pareto.pctl +++ b/examples/multi-objective/mdp/scheduler/scheduler50_pareto.pctl @@ -1 +1,4 @@ - multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) + multi(R{"energy"}min=?[ F "tasks_complete" ], R{"time"}min=? [ F "tasks_complete" ]) +// Original query: +// multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) +// Note that the min values are actually infinity and prism (currently) gives wrong results for this, e.g., R{"time"}min=?[ C<=2000 ] gives a larger value than multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) . \ No newline at end of file diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index 83b2892cf..930bfe58c 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp @@ -257,6 +257,21 @@ namespace storm { auto duplicatorResult = storm::transformer::StateDuplicator::transform(data.preprocessedModel, targetStates); updatePreprocessedModel(data, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping); + // Add a reward model that gives zero reward to the actions of states of the second copy. + std::vector objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "").getTotalRewardVector(data.preprocessedModel.getTransitionMatrix()); + for(auto secondCopyState : duplicatorResult.secondCopy) { + for(uint_fast64_t choice = data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[secondCopyState]; choice < data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[secondCopyState+1]; ++choice) { + objectiveRewards[choice] = storm::utility::zero(); + } + } + storm::storage::BitVector positiveRewards = storm::utility::vector::filterGreaterZero(objectiveRewards); + storm::storage::BitVector nonNegativeRewards = positiveRewards | storm::utility::vector::filterZero(objectiveRewards); + STORM_LOG_THROW(nonNegativeRewards.full() || positiveRewards.empty(), storm::exceptions::InvalidPropertyException, "The reward model for the formula " << formula << " has positive and negative rewards which is not supported."); + if(!currentObjective.rewardsArePositive){ + storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one()); + } + data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards)); + // States of the first copy from which the second copy is not reachable with prob 1 under any scheduler can // be removed as the expected reward is not defined for these states. // We also need to enforce that the second copy will be reached eventually with prob 1. @@ -269,17 +284,6 @@ namespace storm { auto subsystemBuilderResult = storm::transformer::SubsystemBuilder::transform(data.preprocessedModel, subsystemStates, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), true)); updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping); } - - // Add a reward model that gives zero reward to the states of the second copy. - std::vector objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "").getTotalRewardVector(data.preprocessedModel.getTransitionMatrix()); - storm::utility::vector::setVectorValues(objectiveRewards, duplicatorResult.secondCopy, storm::utility::zero()); - storm::storage::BitVector positiveRewards = storm::utility::vector::filterGreaterZero(objectiveRewards); - storm::storage::BitVector nonNegativeRewards = positiveRewards | storm::utility::vector::filterZero(objectiveRewards); - STORM_LOG_THROW(nonNegativeRewards.full() || positiveRewards.empty(), storm::exceptions::InvalidPropertyException, "The reward model for the formula " << formula << " has positive and negative rewards which is not supported."); - if(!currentObjective.rewardsArePositive){ - storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one()); - } - data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards)); } template @@ -343,6 +347,21 @@ namespace storm { 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(state == 31963) { + std::cout << " state 31963:" << std::endl; + if(statesWithNegativeRewardForAllChoices.get(state)) { + std::cout << " negative reward for all choices: " << std::endl; + for(uint_fast64_t choice = data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; choice < data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1] ;++choice) { + std::cout << choice << ": " << (actionsWithNonNegativeReward.get(choice) ? "non" : "") << "negative with values: "; + for(auto& obj : data.objectives) { + std::cout << data.preprocessedModel.getRewardModel(obj.rewardModelName).getStateActionRewardVector()[choice] << ", "; + } + std::cout << std::endl; + } + + } + } + } storm::storage::BitVector submatrixRows = actionsWithNonNegativeReward; @@ -351,11 +370,14 @@ namespace storm { submatrixRows.set(data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state], true); } storm::storage::BitVector allStates(data.preprocessedModel.getNumberOfStates(), true); - storm::storage::SparseMatrix transitionsWithNonNegativeReward = data.preprocessedModel.getTransitionMatrix().getSubmatrix(false, submatrixRows, allStates, true); + storm::storage::SparseMatrix transitionsWithNonNegativeReward = data.preprocessedModel.getTransitionMatrix().getSubmatrix(false, submatrixRows, allStates); STORM_LOG_ASSERT(data.preprocessedModel.getTransitionMatrix().getRowGroupCount() == transitionsWithNonNegativeReward.getRowGroupCount(), "Row group count mismatch."); + std::cout << "statesWithNegativeRewardForAllChoices: " << statesWithNegativeRewardForAllChoices << std::endl; storm::storage::BitVector statesNeverReachingNegativeRewardForSomeScheduler = storm::utility::graph::performProb0E(transitionsWithNonNegativeReward, transitionsWithNonNegativeReward.getRowGroupIndices(), transitionsWithNonNegativeReward.transpose(true), allStates, statesWithNegativeRewardForAllChoices); + std::cout << "statesNeverReachingNegativeRewardForSomeScheduler: " << statesNeverReachingNegativeRewardForSomeScheduler << std::endl; storm::storage::BitVector statesReachingNegativeRewardsFinitelyOftenForSomeScheduler = storm::utility::graph::performProb1E(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), data.preprocessedModel.getBackwardTransitions(), allStates, statesNeverReachingNegativeRewardForSomeScheduler); + std::cout << "statesReachingNegativeRewardsFinitelyOftenForSomeScheduler: " << statesReachingNegativeRewardsFinitelyOftenForSomeScheduler << std::endl; auto subsystemBuilderResult = storm::transformer::SubsystemBuilder::transform(data.preprocessedModel, statesReachingNegativeRewardsFinitelyOftenForSomeScheduler, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), true)); data.preprocessedModel = std::move(*subsystemBuilderResult.model);