compiles again

Former-commit-id: 1c09323cd1

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 {

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

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) {
+             
+         }
     }
 }

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