Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ParametricDtmcPrctlModelCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
7#include "storm/api/builder.h"
13
15namespace {
16
17class EigenEnvironment {
18 public:
19 static storm::Environment createEnvironment() {
21 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
22 return env;
23 }
24};
25
26class EliminationEnvironment {
27 public:
28 static storm::Environment createEnvironment() {
30 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Elimination);
31 return env;
32 }
33};
34
35template<typename TestType>
36class ParametricDtmcPrctlModelCheckerTest : public ::testing::Test {
37 public:
38 ParametricDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
39
40 void SetUp() override {
41#ifndef STORM_HAVE_Z3
42 GTEST_SKIP() << "Z3 not available.";
43#endif
44 }
45
46 storm::Environment const& env() const {
47 return _environment;
48 }
49 storm::RationalFunctionCoefficient parseNumber(std::string const& input) const {
50 return storm::utility::convertNumber<storm::RationalFunctionCoefficient>(input);
51 }
52
53 private:
54 storm::Environment _environment;
55};
56
57typedef ::testing::Types<EigenEnvironment, EliminationEnvironment> TestingTypes;
58
59TYPED_TEST_SUITE(ParametricDtmcPrctlModelCheckerTest, TestingTypes, );
60TYPED_TEST(ParametricDtmcPrctlModelCheckerTest, Die) {
61 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm");
64 std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model =
66
67 // A parser that we use for conveniently constructing the formulas.
68
69 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
70 storm::parser::FormulaParser formulaParser(expManager);
71
72 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
73
74 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
75
76 ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
77 ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
78
79 std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> instantiation;
80 std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*dtmc);
81 ASSERT_EQ(variables.size(), 1ull);
82 instantiation.emplace(*variables.begin(), this->parseNumber("1/2"));
83
85
86 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
87
88 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
91
92 EXPECT_EQ(this->parseNumber("1/6"), quantitativeResult1[0].evaluate(instantiation));
93
94 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
95
96 result = checker.check(this->env(), *formula);
99
100 EXPECT_EQ(this->parseNumber("1/6"), quantitativeResult2[0].evaluate(instantiation));
101
102 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
103
104 result = checker.check(this->env(), *formula);
107
108 EXPECT_EQ(this->parseNumber("1/6"), quantitativeResult3[0].evaluate(instantiation));
109
110 formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
111
112 result = checker.check(this->env(), *formula);
115
116 EXPECT_EQ(this->parseNumber("11/3"), quantitativeResult4[0].evaluate(instantiation));
117}
118} // namespace
SolverEnvironment & solver()
void setLinearEquationSolverType(storm::solver::EquationSolverType const &value, bool isSetFromDefault=false)
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()
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
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.
std::set< storm::RationalFunctionVariable > getProbabilityParameters(Model< storm::RationalFunction > const &model)
Get all probability parameters occurring on transitions.
Definition Model.cpp:703
NumberType parseNumber(std::string const &value)
Parse number from string.
CoefficientType< FunctionType >::type evaluate(FunctionType const &function, Valuation< FunctionType > const &valuation)
Evaluates the given function wrt.
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46