Storm 1.10.0.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
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<
127#ifdef STORM_HAVE_GMM
128 GmmxxDoubleGmresEnvironment, EigenDoubleDGmresEnvironment,
129#endif
130 EigenRationalLUEnvironment, NativeSorEnvironment, NativePowerEnvironment, NativeWalkerChaeEnvironment>
132
133TYPED_TEST_SUITE(ConditionalDtmcPrctlModelCheckerTest, TestingTypes, );
134
135TYPED_TEST(ConditionalDtmcPrctlModelCheckerTest, Conditional) {
136 typedef typename TestFixture::ValueType ValueType;
137
138 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/test_conditional.pm");
139
142 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = storm::builder::ExplicitModelBuilder<ValueType>(program, options).build();
143 ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
144 ASSERT_EQ(4ul, model->getNumberOfStates());
145 ASSERT_EQ(5ul, model->getNumberOfTransitions());
146
147 std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
148
150
151 // A parser that we use for conveniently constructing the formulas.
152
153 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
154 storm::parser::FormulaParser formulaParser(expManager);
155 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\"]");
156
157 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
159 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
160
161 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\" || F \"condition\"]");
162
163 result = checker.check(this->env(), *formula);
165 EXPECT_NEAR(storm::utility::one<ValueType>(), quantitativeResult2[0], this->precision());
166
167 formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\"]");
168
169 result = checker.check(this->env(), *formula);
171 EXPECT_EQ(storm::utility::infinity<ValueType>(), quantitativeResult3[0]);
172
173 formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\" || F \"condition\"]");
174
175 result = checker.check(this->env(), *formula);
177 EXPECT_NEAR(storm::utility::one<ValueType>(), quantitativeResult4[0], this->precision());
178}
179} // 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