Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MilpPermissiveSchedulerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-parsers/parser/FormulaParser.h"
5#include "storm-parsers/parser/PrismParser.h"
6#include "storm-permissive/analysis/PermissiveSchedulers.h"
7#include "storm/builder/ExplicitModelBuilder.h"
8#include "storm/environment/Environment.h"
9#include "storm/logic/Formulas.h"
10#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
11#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
12#include "storm/models/sparse/StandardRewardModel.h"
13#include "storm/solver/MinMaxLinearEquationSolver.h"
14#include "storm/storage/expressions/ExpressionManager.h"
15
16#ifdef STORM_HAVE_GUROBI
17
18TEST(MilpPermissiveSchedulerTest, DieSelection) {
19 if (storm::test::noGurobi) {
20 GTEST_SKIP();
21 }
22 storm::Environment env;
23
24 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm");
25 storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
26 std::string formulaString = "";
27 formulaString += "P>=0.10 [ F \"one\"];\n";
28 formulaString += "P>=0.17 [ F \"one\"];\n";
29 formulaString += "P<=0.10 [ F \"one\"];\n";
30 formulaString += "P<=0.17 [ F \"one\"];\n";
31 auto formulas = formulaParser.parseFromString(formulaString);
32
33 auto const& formula02 = formulas[0].getRawFormula()->asProbabilityOperatorFormula();
34 ASSERT_TRUE(storm::logic::isLowerBound(formula02.getComparisonType()));
35 auto const& formula001 = formulas[1].getRawFormula()->asProbabilityOperatorFormula();
36 auto const& formula02b = formulas[2].getRawFormula()->asProbabilityOperatorFormula();
37 auto const& formula001b = formulas[3].getRawFormula()->asProbabilityOperatorFormula();
38
39 // Customize and perform model-building.
40 storm::generator::NextStateGeneratorOptions options;
41 options.setBuildAllLabels().setBuildChoiceLabels(true);
42 std::shared_ptr<storm::models::sparse::Mdp<double>> mdp =
43 storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::Mdp<double>>();
44
45 boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02);
46 EXPECT_TRUE(perms.is_initialized());
47 boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms2 = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula001);
48 EXPECT_FALSE(perms2.is_initialized());
49
50 boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms3 = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02b);
51 EXPECT_FALSE(perms3.is_initialized());
52 boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms4 = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula001b);
53 EXPECT_TRUE(perms4.is_initialized());
54
55 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker0(*mdp);
56
57 std::unique_ptr<storm::modelchecker::CheckResult> result0 = checker0.check(env, formula02);
58 storm::modelchecker::ExplicitQualitativeCheckResult<double>& qualitativeResult0 = result0->template asExplicitQualitativeCheckResult<double>();
59
60 ASSERT_FALSE(qualitativeResult0[0]);
61
62 auto submdp = perms->apply();
63 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker1(submdp);
64
65 std::unique_ptr<storm::modelchecker::CheckResult> result1 = checker1.check(env, formula02);
66 storm::modelchecker::ExplicitQualitativeCheckResult<double>& qualitativeResult1 = result1->template asExplicitQualitativeCheckResult<double>();
67
68 EXPECT_TRUE(qualitativeResult1[0]);
69}
70
71#endif
TEST
TEST(OrderTest, Simple)
Definition OrderTest.cpp:15
storm::builder::BuilderOptions::setBuildAllLabels
BuilderOptions & setBuildAllLabels(bool newValue=true)
Should all reward models be built?
Definition BuilderOptions.cpp:228
storm::builder::BuilderOptions::setBuildChoiceLabels
BuilderOptions & setBuildChoiceLabels(bool newValue=true)
Should the choice labels be built?
Definition BuilderOptions.cpp:261
storm::builder::ExplicitModelBuilder::build
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > build()
Convert the program given at construction time to an abstract model.
Definition ExplicitModelBuilder.cpp:77
storm::expressions::ExpressionManager::getSharedPointer
std::shared_ptr< ExpressionManager > getSharedPointer()
Retrieves a shared pointer to the expression manager.
Definition ExpressionManager.cpp:341
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:13
storm::parser::PrismParser::parse
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
Definition PrismParser.cpp:5
storm::prism::Program::getManager
storm::expressions::ExpressionManager & getManager() const
Retrieves the manager responsible for the expressions of this program.
Definition Program.cpp:2378
storm::generator::NextStateGeneratorOptions
storm::builder::BuilderOptions NextStateGeneratorOptions
Definition NextStateGenerator.h:25
storm::logic::isLowerBound
bool isLowerBound(ComparisonType t)
Definition ComparisonType.h:16
storm::ps::computePermissiveSchedulerViaMILP
boost::optional< SubMDPPermissiveScheduler< RM > > computePermissiveSchedulerViaMILP(storm::models::sparse::Mdp< double, RM > const &mdp, storm::logic::ProbabilityOperatorFormula const &safeProp)
Definition PermissiveSchedulers.cpp:18
storm_gtest.h