fixed headers, allow changes in rew. model again

Former-commit-id: 4617000d30

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() {

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;
                 

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>();
+            }
          }
     }
 }

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 {