Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ConditionalDtmcPrctlModelCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
6#include "storm/api/builder.h"
12
16
17namespace {
18
19#ifdef STORM_HAVE_GMM
20class GmmxxDoubleGmresEnvironment {
21 public:
22 typedef double ValueType;
23 static const bool isExact = false;
24 static storm::Environment createEnvironment() {
26 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
27 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
28 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
29 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
30 return env;
31 }
32};
33
34class EigenDoubleDGmresEnvironment {
35 public:
36 typedef double ValueType;
37 static const bool isExact = false;
38 static storm::Environment createEnvironment() {
40 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
41 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
42 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
43 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
44 return env;
45 }
46};
47#endif
48
49class EigenRationalLUEnvironment {
50 public:
51 typedef storm::RationalNumber ValueType;
52 static const bool isExact = true;
53 static storm::Environment createEnvironment() {
55 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
56 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
57 return env;
58 }
59};
60
61class NativeSorEnvironment {
62 public:
63 typedef double ValueType;
64 static const bool isExact = false;
65 static storm::Environment createEnvironment() {
67 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
68 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
69 env.solver().native().setSorOmega(storm::utility::convertNumber<storm::RationalNumber>(0.9));
70 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
71 return env;
72 }
73};
74
75class NativePowerEnvironment {
76 public:
77 typedef double ValueType;
78 static const bool isExact = false;
79 static storm::Environment createEnvironment() {
81 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
82 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
83 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
84 return env;
85 }
86};
87
88class NativeWalkerChaeEnvironment {
89 public:
90 typedef double ValueType;
91 static const bool isExact = false;
92 static storm::Environment createEnvironment() {
94 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
95 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
96 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
98 return env;
99 }
100};
101
102template<typename TestType>
103class ConditionalDtmcPrctlModelCheckerTest : public ::testing::Test {
104 public:
105 typedef typename TestType::ValueType ValueType;
106 ConditionalDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
107
108 void SetUp() override {
109#ifndef STORM_HAVE_Z3
110 GTEST_SKIP() << "Z3 not available.";
111#endif
112 }
113
114 storm::Environment const& env() const {
115 return _environment;
116 }
117 ValueType parseNumber(std::string const& input) const {
118 return storm::utility::convertNumber<ValueType>(input);
119 }
120 ValueType precision() const {
121 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
122 }
123
124 private:
125 storm::Environment _environment;
126};
127
128typedef ::testing::Types<
129#ifdef STORM_HAVE_GMM
130 GmmxxDoubleGmresEnvironment, EigenDoubleDGmresEnvironment,
131#endif
132 EigenRationalLUEnvironment, NativeSorEnvironment, NativePowerEnvironment, NativeWalkerChaeEnvironment>
134
135TYPED_TEST_SUITE(ConditionalDtmcPrctlModelCheckerTest, TestingTypes, );
136
137TYPED_TEST(ConditionalDtmcPrctlModelCheckerTest, Conditional) {
138 typedef typename TestFixture::ValueType ValueType;
139
140 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/test_conditional.pm");
141
144 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = storm::builder::ExplicitModelBuilder<ValueType>(program, options).build();
145 ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
146 ASSERT_EQ(4ul, model->getNumberOfStates());
147 ASSERT_EQ(5ul, model->getNumberOfTransitions());
148
149 std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
150
152
153 // A parser that we use for conveniently constructing the formulas.
154
155 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
156 storm::parser::FormulaParser formulaParser(expManager);
157 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\"]");
158
159 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
161 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
162
163 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\" || F \"condition\"]");
164
165 result = checker.check(this->env(), *formula);
167 EXPECT_NEAR(storm::utility::one<ValueType>(), quantitativeResult2[0], this->precision());
168
169 formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\"]");
170
171 result = checker.check(this->env(), *formula);
173 EXPECT_EQ(storm::utility::infinity<ValueType>(), quantitativeResult3[0]);
174
175 formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\" || F \"condition\"]");
176
177 result = checker.check(this->env(), *formula);
179 EXPECT_NEAR(storm::utility::one<ValueType>(), quantitativeResult4[0], this->precision());
180}
181} // namespace
void setPrecision(storm::RationalNumber value)
void setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner value)
void setMethod(storm::solver::EigenLinearEquationSolverMethod value)
SolverEnvironment & solver()
void setMethod(storm::solver::GmmxxLinearEquationSolverMethod value)
void setPrecision(storm::RationalNumber value)
void setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner value)
void setSorOmega(storm::RationalNumber const &value)
void setMaximalNumberOfIterations(uint64_t value)
void setMethod(storm::solver::NativeLinearEquationSolverMethod value)
void setPrecision(storm::RationalNumber value)
void setLinearEquationSolverType(storm::solver::EquationSolverType const &value, bool isSetFromDefault=false)
EigenSolverEnvironment & eigen()
NativeSolverEnvironment & native()
GmmxxSolverEnvironment & gmmxx()
BuilderOptions & setBuildAllLabels(bool newValue=true)
Should all reward models be built? If not set, only required reward models are build.
BuilderOptions & setBuildAllRewardModels(bool newValue=true)
Should all reward models be built? If not set, only required reward models are build.
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > build()
Convert the program given at construction time to an abstract model.
ExplicitQuantitativeCheckResult< ValueType > & asExplicitQuantitativeCheckResult()
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.
SFTBDDChecker::ValueType ValueType
NumberType parseNumber(std::string const &value)
Parse number from string.
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46