diff --git a/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp index 912b55976..20707d33e 100644 --- a/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ b/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp @@ -8,13 +8,15 @@ #include "storm/permissivesched/PermissiveSchedulers.h" #include "storm/builder/ExplicitModelBuilder.h" #include "storm/solver/MinMaxLinearEquationSolver.h" - +#include "storm/environment/Environment.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #ifdef STORM_HAVE_GUROBI TEST(MilpPermissiveSchedulerTest, DieSelection) { + storm::Environment env; + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm"); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); @@ -40,17 +42,17 @@ 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::StandardMinMaxLinearEquationSolverFactory(storm::solver::EquationSolverType::Native))); + storm::modelchecker::SparseMdpPrctlModelChecker> checker0(*mdp); - std::unique_ptr result0 = checker0.check(formula02); + std::unique_ptr result0 = checker0.check(env, formula02); storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult0 = result0->asExplicitQualitativeCheckResult(); ASSERT_FALSE(qualitativeResult0[0]); auto submdp = perms->apply(); - storm::modelchecker::SparseMdpPrctlModelChecker> checker1(submdp, std::unique_ptr>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory(storm::solver::EquationSolverType::Native))); + storm::modelchecker::SparseMdpPrctlModelChecker> checker1(submdp); - std::unique_ptr result1 = checker1.check(formula02); + std::unique_ptr result1 = checker1.check(env, formula02); storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult1 = result1->asExplicitQualitativeCheckResult(); EXPECT_TRUE(qualitativeResult1[0]); diff --git a/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp index ae9fad1d2..b19f82618 100644 --- a/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp +++ b/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp @@ -6,6 +6,7 @@ #include "storm/logic/Formulas.h" #include "storm/permissivesched/PermissiveSchedulers.h" #include "storm/builder/ExplicitModelBuilder.h" +#include "storm/environment/Environment.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" @@ -16,6 +17,7 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) { #else TEST(SmtPermissiveSchedulerTest, DISABLED_DieSelection) { #endif + storm::Environment env; storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm"); storm::parser::FormulaParser formulaParser(program); @@ -43,7 +45,7 @@ TEST(SmtPermissiveSchedulerTest, DISABLED_DieSelection) { storm::modelchecker::SparseMdpPrctlModelChecker> checker0(*mdp); - std::unique_ptr result0 = checker0.check(formula02b); + std::unique_ptr result0 = checker0.check(env, formula02b); storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult0 = result0->asExplicitQualitativeCheckResult(); ASSERT_FALSE(qualitativeResult0[0]); @@ -51,7 +53,7 @@ TEST(SmtPermissiveSchedulerTest, DISABLED_DieSelection) { auto submdp = perms3->apply(); storm::modelchecker::SparseMdpPrctlModelChecker> checker1(submdp); - std::unique_ptr result1 = checker1.check(formula02b); + std::unique_ptr result1 = checker1.check(env, formula02b); storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult1 = result1->asExplicitQualitativeCheckResult(); EXPECT_TRUE(qualitativeResult1[0]);