From b8343255be8d2301ace57d4ed8a8197522bd507e Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Sun, 27 Sep 2015 17:51:12 +0200
Subject: [PATCH] fixed headers, allow changes in rew. model again

Former-commit-id: 4617000d307785feb881b7d5f69bd594d160e8d6
---
 src/models/sparse/NondeterministicModel.cpp  |  4 ++--
 src/models/sparse/NondeterministicModel.h    |  2 +-
 src/permissivesched/PermissiveSchedulers.cpp | 20 +++++++++++++++++---
 src/permissivesched/PermissiveSchedulers.h   |  1 +
 4 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp
index ecc350d8b..9cfbe75f9 100644
--- a/src/models/sparse/NondeterministicModel.cpp
+++ b/src/models/sparse/NondeterministicModel.cpp
@@ -47,7 +47,7 @@ namespace storm {
                 return indices[state+1] - indices[state];
             }
             
-            /*template<typename ValueType, typename RewardModelType>
+            template<typename ValueType, typename RewardModelType>
             void NondeterministicModel<ValueType, RewardModelType>::modifyStateActionRewards(RewardModelType& rewardModel, std::map<std::pair<uint_fast64_t, LabelSet>, typename RewardModelType::ValueType> const& modifications) const {
                 STORM_LOG_THROW(rewardModel.hasStateActionRewards(), storm::exceptions::InvalidOperationException, "Cannot modify state-action rewards, because the reward model does not have state-action rewards.");
                 STORM_LOG_THROW(this->hasChoiceLabeling(), storm::exceptions::InvalidOperationException, "Cannot modify state-action rewards, because the model does not have an action labeling.");
@@ -61,7 +61,7 @@ namespace storm {
                         }
                     }
                 }
-            }*/
+            }
             
             template<typename ValueType, typename RewardModelType>
             void NondeterministicModel<ValueType, RewardModelType>::reduceToStateBasedRewards() {
diff --git a/src/models/sparse/NondeterministicModel.h b/src/models/sparse/NondeterministicModel.h
index ad09143c7..5bacf6dd7 100644
--- a/src/models/sparse/NondeterministicModel.h
+++ b/src/models/sparse/NondeterministicModel.h
@@ -80,7 +80,7 @@ namespace storm {
                  * @param rewardModel The reward model whose state-action rewards to modify.
                  * @param modifications A mapping from state-action pairs to the their new reward values.
                  */
-                //void modifyStateActionRewards(RewardModelType& rewardModel, std::map<std::pair<uint_fast64_t, LabelSet>, typename RewardModelType::ValueType> const& modifications) const;
+                void modifyStateActionRewards(RewardModelType& rewardModel, std::map<std::pair<uint_fast64_t, LabelSet>, typename RewardModelType::ValueType> const& modifications) const;
                 
                 virtual void reduceToStateBasedRewards() override;
                 
diff --git a/src/permissivesched/PermissiveSchedulers.cpp b/src/permissivesched/PermissiveSchedulers.cpp
index 9bf7959ca..8cdca5f8a 100644
--- a/src/permissivesched/PermissiveSchedulers.cpp
+++ b/src/permissivesched/PermissiveSchedulers.cpp
@@ -8,6 +8,7 @@
 #include "src/exceptions/NotImplementedException.h"
 #include "src/utility/macros.h"
 
+
 namespace storm {
     namespace ps {
         
@@ -16,14 +17,14 @@ namespace storm {
             assert(safeProp.getSubformula().isEventuallyFormula());
             auto backwardTransitions = mdp->getBackwardTransitions();
             storm::storage::BitVector goalstates = propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
-            goalstates = storm::utility::graph::performProb1E(*mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates);
+            goalstates = storm::utility::graph::performProb1A(*mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates);
             storm::storage::BitVector sinkstates = storm::utility::graph::performProb0A(*mdp,backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates);
 
             auto solver = storm::utility::solver::getLpSolver("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi);
             MilpPermissiveSchedulerComputation comp(*solver, mdp, goalstates, sinkstates);
             STORM_LOG_THROW(!storm::logic::isStrict(safeProp.getComparisonType()), storm::exceptions::NotImplementedException, "Strict bounds are not supported");
             comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getBound());
-            comp.dumpLpToFile("milpdump.lp");
+            //comp.dumpLpToFile("milpdump.lp");
             std::cout << "Found Solution: " << (comp.foundSolution() ? "yes" : "no") << std::endl;
             if(comp.foundSolution()) {
                 return boost::optional<SubMDPPermissiveScheduler>(comp.getScheduler());
@@ -37,7 +38,20 @@ namespace storm {
          }
          
          boost::optional<SubMDPPermissiveScheduler> computerPermissiveSchedulerViaSMT(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
-             
+             storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Mdp<double>> propMC(*mdp);
+             assert(safeProp.getSubformula().isEventuallyFormula());
+             auto backwardTransitions = mdp->getBackwardTransitions();
+             storm::storage::BitVector goalstates = propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
+             goalstates = storm::utility::graph::performProb1A(*mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates);
+             storm::storage::BitVector sinkstates = storm::utility::graph::performProb0A(*mdp,backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates);
+
+            SmtPermissiveSchedulerComputation comp(mdp, goalstates, sinkstates)
+
+            if(comp.foundSolution()) {
+                return boost::optional<SubMDPPermissiveScheduler>(comp.getScheduler());
+            } else {
+                return boost::optional<SubMDPPermissiveScheduler>();
+            }
          }
     }
 }
diff --git a/src/permissivesched/PermissiveSchedulers.h b/src/permissivesched/PermissiveSchedulers.h
index 21c293b81..2ebcd07bf 100644
--- a/src/permissivesched/PermissiveSchedulers.h
+++ b/src/permissivesched/PermissiveSchedulers.h
@@ -5,6 +5,7 @@
 #include "../logic/ProbabilityOperatorFormula.h"
 #include "../models/sparse/Mdp.h"
 
+#include "src/models/sparse/StandardRewardModel.h"
 
 namespace storm {
     namespace ps {