From df86b6c8154f9287775f01d3c4744b690c29bc25 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 6 Dec 2017 19:57:38 +0100
Subject: [PATCH] fixing issue related to relevant value restriction in
 conditional properties

---
 .../prctl/helper/SparseDtmcPrctlHelper.cpp    | 30 +++++++++++++++++++
 .../prctl/helper/SparseDtmcPrctlHelper.h      |  5 +++-
 2 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
index 0d0ec5928..781024096 100644
--- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
@@ -453,6 +453,22 @@ namespace storm {
                 
                 return result;
             }
+
+            template<typename ValueType, typename RewardModelType>
+            storm::storage::BitVector SparseDtmcPrctlHelper<ValueType, RewardModelType>::BaierTransformedModel::getNewRelevantStates() const {
+                storm::storage::BitVector newRelevantStates(transitionMatrix.get().getRowCount());
+                for (uint64_t i = 0; i < this->beforeStates.getNumberOfSetBits(); ++i) {
+                    newRelevantStates.set(i);
+                }
+                return newRelevantStates;
+            }
+            
+            template<typename ValueType, typename RewardModelType>
+            storm::storage::BitVector SparseDtmcPrctlHelper<ValueType, RewardModelType>::BaierTransformedModel::getNewRelevantStates(storm::storage::BitVector const& oldRelevantStates) const {
+                storm::storage::BitVector result = oldRelevantStates % this->beforeStates;
+                result.resize(transitionMatrix.get().getRowCount());
+                return result;
+            }
             
             template<typename ValueType, typename RewardModelType>
             std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeConditionalProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
@@ -472,6 +488,13 @@ namespace storm {
                         
                         // Now compute reachability probabilities in the transformed model.
                         storm::storage::SparseMatrix<ValueType> const& newTransitionMatrix = transformedModel.transitionMatrix.get();
+                        storm::storage::BitVector newRelevantValues;
+                        if (goal.hasRelevantValues()) {
+                            newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues());
+                        } else {
+                            newRelevantValues = transformedModel.getNewRelevantStates();
+                        }
+                        goal.setRelevantValues(std::move(newRelevantValues));
                         std::vector<ValueType> conditionalProbabilities = computeUntilProbabilities(env, std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory);
                         
                         storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities);
@@ -498,6 +521,13 @@ namespace storm {
                         
                         // Now compute reachability probabilities in the transformed model.
                         storm::storage::SparseMatrix<ValueType> const& newTransitionMatrix = transformedModel.transitionMatrix.get();
+                        storm::storage::BitVector newRelevantValues;
+                        if (goal.hasRelevantValues()) {
+                            newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues());
+                        } else {
+                            newRelevantValues = transformedModel.getNewRelevantStates();
+                        }
+                        goal.setRelevantValues(std::move(newRelevantValues));
                         std::vector<ValueType> conditionalRewards = computeReachabilityRewards(env, std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), transformedModel.stateRewards.get(), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory);
                         storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalRewards);
                     }
diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
index 6564c4f5d..0c0712723 100644
--- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
+++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
@@ -59,7 +59,10 @@ namespace storm {
                     BaierTransformedModel() : noTargetStates(false) {
                         // Intentionally left empty.
                     }
-                    
+
+                    storm::storage::BitVector getNewRelevantStates(storm::storage::BitVector const& oldRelevantStates) const;
+                    storm::storage::BitVector getNewRelevantStates() const;
+
                     storm::storage::BitVector beforeStates;
                     boost::optional<storm::storage::SparseMatrix<ValueType>> transitionMatrix;
                     boost::optional<storm::storage::BitVector> targetStates;