From 6d10ba0ad0939fcea9627b8b786f86d24d1cbeab Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Tue, 1 Sep 2015 18:22:16 +0200
Subject: [PATCH] compiles again

Former-commit-id: 1c09323cd1c3c7a14582f2446f48ff2afd0be2fc
---
 .../prctl/helper/MDPModelCheckingHelperReturnType.h         | 2 +-
 src/permissivesched/MILPPermissiveSchedulers.h              | 2 +-
 src/permissivesched/PermissiveSchedulers.cpp                | 6 +++++-
 .../permissiveschedulers/MilpPermissiveSchedulerTest.cpp    | 3 +--
 4 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h b/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h
index d04dd1988..a68a5889e 100644
--- a/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h
+++ b/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h
@@ -3,7 +3,7 @@
 
 #include <vector>
 #include <memory>
-#include "src/storage/partialscheduler.h"
+#include "src/storage/PartialScheduler.h"
 
 namespace storm {
     namespace storage {
diff --git a/src/permissivesched/MILPPermissiveSchedulers.h b/src/permissivesched/MILPPermissiveSchedulers.h
index 7f0e7c5b9..d25179225 100644
--- a/src/permissivesched/MILPPermissiveSchedulers.h
+++ b/src/permissivesched/MILPPermissiveSchedulers.h
@@ -187,7 +187,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
                 createConstraints(boundary, relevantStates);
                 
                 
-                solver.setModelSense(storm::solver::LpSolver::ModelSense::Minimize);
+                solver.setOptimizationDirection(storm::OptimizationDirection::Minimize);
                 
             }
         };
diff --git a/src/permissivesched/PermissiveSchedulers.cpp b/src/permissivesched/PermissiveSchedulers.cpp
index 231d4ba14..53f1039a8 100644
--- a/src/permissivesched/PermissiveSchedulers.cpp
+++ b/src/permissivesched/PermissiveSchedulers.cpp
@@ -11,7 +11,7 @@ namespace storm {
     namespace ps {
         
          boost::optional<MemorylessDeterministicPermissiveScheduler> computePermissiveSchedulerViaMILP(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
-            storm::modelchecker::SparsePropositionalModelChecker<double> propMC(*mdp);
+            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();
@@ -31,5 +31,9 @@ namespace storm {
          boost::optional<MemorylessDeterministicPermissiveScheduler> computePermissiveSchedulerViaMC(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
              
          }
+         
+         boost::optional<MemorylessDeterministicPermissiveScheduler> computerPermissiveSchedulerViaSMT(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
+             
+         }
     }
 }
diff --git a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
index a66a6f693..ad300df32 100644
--- a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
+++ b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
@@ -11,7 +11,7 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_selection.nm");
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::cout << " We are now here " << std::endl;
-    auto formula = formulaParser.parseFromString("P<=0.2 [ F \"one\"]")->asProbabilityOperatorFormula();
+    auto formula = formulaParser.parseSingleFormulaFromString("P<=0.2 [ F \"one\"]")->asProbabilityOperatorFormula();
     std::cout << formula << std::endl;
     
     // Customize and perform model-building.
@@ -19,7 +19,6 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) {
     
     options = typename storm::builder::ExplicitPrismModelBuilder<double>::Options(formula);
     options.addConstantDefinitionsFromString(program, "");
-    options.buildRewards = false;
     options.buildCommandLabels = true;
     
     std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options)->as<storm::models::sparse::Mdp<double>>();