|
|
@ -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<storm::ps::SubMDPPermissiveScheduler<>> perms4 = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula001b); |
|
|
|
EXPECT_NE(perms4, boost::none); |
|
|
|
|
|
|
|
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker0(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::StandardMinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverType::Native))); |
|
|
|
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker0(*mdp); |
|
|
|
|
|
|
|
std::unique_ptr<storm::modelchecker::CheckResult> result0 = checker0.check(formula02); |
|
|
|
std::unique_ptr<storm::modelchecker::CheckResult> result0 = checker0.check(env, formula02); |
|
|
|
storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult0 = result0->asExplicitQualitativeCheckResult(); |
|
|
|
|
|
|
|
ASSERT_FALSE(qualitativeResult0[0]); |
|
|
|
|
|
|
|
auto submdp = perms->apply(); |
|
|
|
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker1(submdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverType::Native))); |
|
|
|
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker1(submdp); |
|
|
|
|
|
|
|
std::unique_ptr<storm::modelchecker::CheckResult> result1 = checker1.check(formula02); |
|
|
|
std::unique_ptr<storm::modelchecker::CheckResult> result1 = checker1.check(env, formula02); |
|
|
|
storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult1 = result1->asExplicitQualitativeCheckResult(); |
|
|
|
|
|
|
|
EXPECT_TRUE(qualitativeResult1[0]); |
|
|
|