1#include "storm-config.h"
18enum class CtmcEngine { JaniSparse };
20class SparseGmmxxGmresIluEnvironment {
22 static const CtmcEngine engine = CtmcEngine::JaniSparse;
23 static const bool isExact =
false;
37class SparseSoundEvtEnvironment {
39 static const CtmcEngine engine = CtmcEngine::JaniSparse;
40 static const bool isExact =
false;
51class SparseClassicEnvironment {
53 static const CtmcEngine engine = CtmcEngine::JaniSparse;
54 static const bool isExact =
false;
64class SparseEigenRationalLuEnvironment {
66 static const CtmcEngine engine = CtmcEngine::JaniSparse;
67 static const bool isExact =
true;
79template<
typename TestType>
80class SteadyStateCtmcCslModelCheckerTest :
public ::testing::Test {
82 typedef typename TestType::ValueType
ValueType;
85 SteadyStateCtmcCslModelCheckerTest() : _environment(TestType::createEnvironment()) {}
90 return storm::utility::convertNumber<ValueType>(input);
95 bool isSparseModel()
const {
96 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
98 CtmcEngine getEngine()
const {
99 return TestType::engine;
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 {
106 janiDescr = janiDescr.preprocess(constantDefinitionString);
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);
123typedef ::testing::Types<SparseGmmxxGmresIluEnvironment, SparseSoundEvtEnvironment, SparseClassicEnvironment, SparseEigenRationalLuEnvironment>
TestingTypes;
127TYPED_TEST(SteadyStateCtmcCslModelCheckerTest, steadystatetest) {
128 typedef typename TestFixture::ValueType
ValueType;
130 auto model = this->buildJaniModel(STORM_TEST_RESOURCES_DIR
"/ctmc/steadystatetest.jani");
131 EXPECT_EQ(8ul, model->getNumberOfStates());
132 EXPECT_EQ(12ul, model->getNumberOfTransitions());
134 auto checker = this->createModelChecker(model);
135 auto result = checker->computeSteadyStateDistribution(this->env());
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>())
143 EXPECT_EQ(sortedVector[1], storm::utility::zero<ValueType>())
145 EXPECT_EQ(sortedVector[2], storm::utility::zero<ValueType>())
147 EXPECT_NEAR(sortedVector[3], this->
parseNumber(
"1/35"), this->precision())
149 EXPECT_NEAR(sortedVector[4], this->
parseNumber(
"2/35"), this->precision())
151 EXPECT_NEAR(sortedVector[5], this->
parseNumber(
"4/35"), this->precision())
153 EXPECT_NEAR(sortedVector[6], this->
parseNumber(
"1/5"), this->precision())
155 EXPECT_NEAR(sortedVector[7], this->
parseNumber(
"3/5"), this->precision())
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()
void setForceSoundness(bool value)
GmmxxSolverEnvironment & gmmxx()
void setForceExact(bool value)
This class represents a continuous-time Markov chain.
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.
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes