Storm
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
19class GmmxxDoubleGmresEnvironment {
20 public:
21 typedef double ValueType;
22 static const bool isExact = false;
23 static storm::Environment createEnvironment() {
25 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
26 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
27 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
28 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
29 return env;
30 }
31};
32
33class EigenDoubleDGmresEnvironment {
34 public:
35 typedef double ValueType;
36 static const bool isExact = false;
37 static storm::Environment createEnvironment() {
39 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
40 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
41 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
42 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
43 return env;
44 }
45};
46
47class EigenRationalLUEnvironment {
48 public:
49 typedef storm::RationalNumber ValueType;
50 static const bool isExact = true;
51 static storm::Environment createEnvironment() {
53 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
54 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
55 return env;
56 }
57};
58
59class NativeSorEnvironment {
60 public:
61 typedef double ValueType;
62 static const bool isExact = false;
63 static storm::Environment createEnvironment() {
65 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
66 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
67 env.solver().native().setSorOmega(storm::utility::convertNumber<storm::RationalNumber>(0.9));
68 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
69 return env;
70 }
71};
72
73class NativePowerEnvironment {
74 public:
75 typedef double ValueType;
76 static const bool isExact = false;
77 static storm::Environment createEnvironment() {
79 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
80 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
81 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
82 return env;
83 }
84};
85
86class NativeWalkerChaeEnvironment {
87 public:
88 typedef double ValueType;
89 static const bool isExact = false;
90 static storm::Environment createEnvironment() {
92 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
93 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
94 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
96 return env;
97 }
98};
99
100template<typename TestType>
101class ConditionalDtmcPrctlModelCheckerTest : public ::testing::Test {
102 public:
103 typedef typename TestType::ValueType ValueType;
104 ConditionalDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
105
106 void SetUp() override {
107#ifndef STORM_HAVE_Z3
108 GTEST_SKIP() << "Z3 not available.";
109#endif
110 }
111
112 storm::Environment const& env() const {
113 return _environment;
114 }
115 ValueType parseNumber(std::string const& input) const {
116 return storm::utility::convertNumber<ValueType>(input);
117 }
118 ValueType precision() const {
119 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
120 }
121
122 private:
123 storm::Environment _environment;
124};
125
126typedef ::testing::Types<GmmxxDoubleGmresEnvironment, EigenDoubleDGmresEnvironment, EigenRationalLUEnvironment, NativeSorEnvironment, NativePowerEnvironment,
127 NativeWalkerChaeEnvironment>
129
130TYPED_TEST_SUITE(ConditionalDtmcPrctlModelCheckerTest, TestingTypes, );
131
132TYPED_TEST(ConditionalDtmcPrctlModelCheckerTest, Conditional) {
133 typedef typename TestFixture::ValueType ValueType;
134
135 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/test_conditional.pm");
136
139 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = storm::builder::ExplicitModelBuilder<ValueType>(program, options).build();
140 ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
141 ASSERT_EQ(4ul, model->getNumberOfStates());
142 ASSERT_EQ(5ul, model->getNumberOfTransitions());
143
144 std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
145
147
148 // A parser that we use for conveniently constructing the formulas.
149
150 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
151 storm::parser::FormulaParser formulaParser(expManager);
152 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\"]");
153
154 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
156 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
157
158 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\" || F \"condition\"]");
159
160 result = checker.check(this->env(), *formula);
162 EXPECT_NEAR(storm::utility::one<ValueType>(), quantitativeResult2[0], this->precision());
163
164 formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\"]");
165
166 result = checker.check(this->env(), *formula);
168 EXPECT_EQ(storm::utility::infinity<ValueType>(), quantitativeResult3[0]);
169
170 formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\" || F \"condition\"]");
171
172 result = checker.check(this->env(), *formula);
174 EXPECT_NEAR(storm::utility::one<ValueType>(), quantitativeResult4[0], this->precision());
175}
176} // 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