diff --git a/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp index 155212770..e9dc268b6 100644 --- a/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ b/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp @@ -3,9 +3,11 @@ #include "storm-config.h" #include "storm/parser/PrismParser.h" #include "storm/parser/FormulaParser.h" +#include "storm/storage/expressions/ExpressionManager.h" #include "storm/logic/Formulas.h" #include "storm/permissivesched/PermissiveSchedulers.h" #include "storm/builder/ExplicitModelBuilder.h" +#include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" @@ -13,7 +15,7 @@ #ifdef STORM_HAVE_GUROBI TEST(MilpPermissiveSchedulerTest, DieSelection) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/builder/die_c1.nm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm"); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); auto formula02 = formulaParser.parseSingleFormulaFromString("P>=0.10 [ F \"one\"]")->asProbabilityOperatorFormula(); @@ -38,7 +40,7 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) { boost::optional> perms4 = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula001b); EXPECT_NE(perms4, boost::none); - storm::modelchecker::SparseMdpPrctlModelChecker> checker0(*mdp, std::unique_ptr>(new storm::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); + storm::modelchecker::SparseMdpPrctlModelChecker> checker0(*mdp, std::unique_ptr>(new storm::solver::StandardMinMaxLinearEquationSolverFactory(storm::solver::EquationSolverType::Native))); std::unique_ptr result0 = checker0.check(formula02); storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult0 = result0->asExplicitQualitativeCheckResult(); @@ -46,15 +48,13 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) { ASSERT_FALSE(qualitativeResult0[0]); auto submdp = perms->apply(); - storm::modelchecker::SparseMdpPrctlModelChecker> checker1(submdp, std::unique_ptr>(new storm::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); + storm::modelchecker::SparseMdpPrctlModelChecker> checker1(submdp, std::unique_ptr>(new storm::solver::StandardMinMaxLinearEquationSolverFactory(storm::solver::EquationSolverType::Native))); std::unique_ptr result1 = checker1.check(formula02); storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult1 = result1->asExplicitQualitativeCheckResult(); EXPECT_TRUE(qualitativeResult1[0]); - // - } #endif