Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SteadyStateCtmcCslModelCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
5#include "storm/api/builder.h"
15
16namespace {
17
18enum class CtmcEngine { JaniSparse };
19
20class SparseGmmxxGmresIluEnvironment {
21 public:
22 static const CtmcEngine engine = CtmcEngine::JaniSparse;
23 static const bool isExact = false;
24 typedef double ValueType;
26 static storm::Environment createEnvironment() {
28 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
29 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
30 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
31 // env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6)); // Need to increase precision because eq sys yields
32 // incorrect results
33 return env;
34 }
35};
36
37class SparseSoundEvtEnvironment {
38 public:
39 static const CtmcEngine engine = CtmcEngine::JaniSparse;
40 static const bool isExact = false;
41 typedef double ValueType;
43 static storm::Environment createEnvironment() {
46 env.solver().setForceSoundness(true);
47 return env;
48 }
49};
50
51class SparseClassicEnvironment {
52 public:
53 static const CtmcEngine engine = CtmcEngine::JaniSparse;
54 static const bool isExact = false;
55 typedef double ValueType;
57 static storm::Environment createEnvironment() {
60 return env;
61 }
62};
63
64class SparseEigenRationalLuEnvironment {
65 public:
66 static const CtmcEngine engine = CtmcEngine::JaniSparse;
67 static const bool isExact = true;
68 typedef storm::RationalNumber ValueType;
70 static storm::Environment createEnvironment() {
72 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
73 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
74 env.solver().setForceExact(true);
75 return env;
76 }
77};
78
79template<typename TestType>
80class SteadyStateCtmcCslModelCheckerTest : public ::testing::Test {
81 public:
82 typedef typename TestType::ValueType ValueType;
83 typedef typename storm::models::sparse::Ctmc<ValueType> SparseModelType;
84
85 SteadyStateCtmcCslModelCheckerTest() : _environment(TestType::createEnvironment()) {}
86 storm::Environment const& env() const {
87 return _environment;
88 }
89 ValueType parseNumber(std::string const& input) const {
90 return storm::utility::convertNumber<ValueType>(input);
91 }
92 ValueType precision() const {
93 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
94 }
95 bool isSparseModel() const {
96 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
97 }
98 CtmcEngine getEngine() const {
99 return TestType::engine;
100 }
101
102 template<typename MT = typename TestType::ModelType>
103 typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<MT>>::type buildJaniModel(
104 std::string const& pathToJaniModel, std::string const& constantDefinitionString = "") const {
105 auto janiDescr = storm::storage::SymbolicModelDescription(storm::api::parseJaniModel(pathToJaniModel).first);
106 janiDescr = janiDescr.preprocess(constantDefinitionString);
107 return storm::api::buildSparseModel<ValueType>(janiDescr, storm::builder::BuilderOptions())->template as<MT>();
108 }
109
110 template<typename MT = typename TestType::ModelType>
111 typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::SparseCtmcCslModelChecker<MT>>>::type
112 createModelChecker(std::shared_ptr<MT> const& model) const {
113 if (TestType::engine == CtmcEngine::JaniSparse) {
114 return std::make_shared<storm::modelchecker::SparseCtmcCslModelChecker<SparseModelType>>(*model);
115 }
116 return nullptr;
117 }
118
119 private:
120 storm::Environment _environment;
121};
122
123typedef ::testing::Types<SparseGmmxxGmresIluEnvironment, SparseSoundEvtEnvironment, SparseClassicEnvironment, SparseEigenRationalLuEnvironment> TestingTypes;
124
125TYPED_TEST_SUITE(SteadyStateCtmcCslModelCheckerTest, TestingTypes, );
126
127TYPED_TEST(SteadyStateCtmcCslModelCheckerTest, steadystatetest) {
128 typedef typename TestFixture::ValueType ValueType;
129
130 auto model = this->buildJaniModel(STORM_TEST_RESOURCES_DIR "/ctmc/steadystatetest.jani");
131 EXPECT_EQ(8ul, model->getNumberOfStates());
132 EXPECT_EQ(12ul, model->getNumberOfTransitions());
133 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
134 auto checker = this->createModelChecker(model);
135 auto result = checker->computeSteadyStateDistribution(this->env());
136
137 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
138 auto resultVector = result->template asExplicitQuantitativeCheckResult<ValueType>().getValueVector();
139 auto sortedVector = resultVector;
140 std::sort(sortedVector.begin(), sortedVector.end());
141 EXPECT_EQ(sortedVector[0], storm::utility::zero<ValueType>())
142 << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << '\n';
143 EXPECT_EQ(sortedVector[1], storm::utility::zero<ValueType>())
144 << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << '\n';
145 EXPECT_EQ(sortedVector[2], storm::utility::zero<ValueType>())
146 << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << '\n';
147 EXPECT_NEAR(sortedVector[3], this->parseNumber("1/35"), this->precision())
148 << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << '\n';
149 EXPECT_NEAR(sortedVector[4], this->parseNumber("2/35"), this->precision())
150 << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << '\n';
151 EXPECT_NEAR(sortedVector[5], this->parseNumber("4/35"), this->precision())
152 << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << '\n';
153 EXPECT_NEAR(sortedVector[6], this->parseNumber("1/5"), this->precision())
154 << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << '\n';
155 EXPECT_NEAR(sortedVector[7], this->parseNumber("3/5"), this->precision())
156 << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << '\n';
157}
158} // namespace
void setMethod(storm::solver::EigenLinearEquationSolverMethod value)
SolverEnvironment & solver()
ModelCheckerEnvironment & modelchecker()
void setMethod(storm::solver::GmmxxLinearEquationSolverMethod value)
void setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner value)
void setSteadyStateDistributionAlgorithm(SteadyStateDistributionAlgorithm value)
void setLinearEquationSolverType(storm::solver::EquationSolverType const &value, bool isSetFromDefault=false)
EigenSolverEnvironment & eigen()
GmmxxSolverEnvironment & gmmxx()
This class represents a continuous-time Markov chain.
Definition Ctmc.h:15
std::pair< storm::jani::Model, std::vector< storm::jani::Property > > parseJaniModel(std::string const &filename, boost::optional< std::vector< std::string > > const &propertyFilter)
SFTBDDChecker::ValueType ValueType
NumberType parseNumber(std::string const &value)
Parse number from string.
std::string toString(std::vector< ValueType > const &vector)
Output vector as string.
Definition vector.h:1298
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46