Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ModelInstantiatorTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-pars/utility/ModelInstantiator.h"
5#include "storm-parsers/api/storm-parsers.h"
6#include "storm/adapters/RationalFunctionAdapter.h"
7#include "storm/api/storm.h"
8#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
9#include "storm/models/sparse/Dtmc.h"
10#include "storm/models/sparse/Mdp.h"
11#include "storm/models/sparse/Model.h"
12#include "storm/settings/SettingsManager.h"
13#include "storm/settings/modules/GeneralSettings.h"
14
15class ModelInstantiatorTest : public ::testing::Test {
16 protected:
17 void SetUp() override {
18#ifndef STORM_HAVE_Z3
19 GTEST_SKIP() << "Z3 not available.";
20#endif
21 }
22};
23
24TEST_F(ModelInstantiatorTest, BrpProb) {
25 carl::VariablePool::getInstance().clear();
26
27 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
28 std::string formulaAsString = "P=? [F s=5 ]";
29
30 // Program and formula
31 storm::prism::Program program = storm::api::parseProgram(programFile);
32 program.checkValidity();
33 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
34 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
35 ASSERT_TRUE(formulas.size() == 1);
36 // Parametric model
37 storm::generator::NextStateGeneratorOptions options(*formulas.front());
38 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc =
39 storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
40
41 storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
42 EXPECT_FALSE(dtmc->hasRewardModel());
43
44 {
45 std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
46 storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
47 ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
48 storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
49 ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
50 valuation.insert(std::make_pair(pL, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.8)));
51 valuation.insert(std::make_pair(pK, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.9)));
52
53 storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
54
55 ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices());
56 for (std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup) {
57 for (std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup];
58 row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup + 1]; ++row) {
59 auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin();
60 for (auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)) {
61 EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn());
62 double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation));
63 EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue());
64 ++instantiatedEntry;
65 }
66 EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(), instantiatedEntry);
67 }
68 }
69 EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling());
70 EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling());
71
72 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> modelchecker(instantiated);
73 std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
74 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
75 EXPECT_NEAR(0.2989278941, quantitativeChkResult[*instantiated.getInitialStates().begin()],
76 storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
77 }
78
79 {
80 std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
81 storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
82 ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
83 storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
84 ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
85 valuation.insert(std::make_pair(pL, storm::utility::one<storm::RationalFunctionCoefficient>()));
86 valuation.insert(std::make_pair(pK, storm::utility::one<storm::RationalFunctionCoefficient>()));
87
88 storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
89
90 ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices());
91 for (std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup) {
92 for (std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup];
93 row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup + 1]; ++row) {
94 auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin();
95 for (auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)) {
96 EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn());
97 double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation));
98 EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue());
99 ++instantiatedEntry;
100 }
101 EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(), instantiatedEntry);
102 }
103 }
104 EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling());
105 EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling());
106
107 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> modelchecker(instantiated);
108 std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
109 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
110 EXPECT_EQ(0.0, quantitativeChkResult[*instantiated.getInitialStates().begin()]);
111 }
112
113 {
114 std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
115 storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
116 ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
117 storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
118 ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
119 valuation.insert(std::make_pair(pL, storm::utility::one<storm::RationalFunctionCoefficient>()));
120 valuation.insert(std::make_pair(pK, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.9)));
121
122 storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
123
124 ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices());
125 for (std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup) {
126 for (std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup];
127 row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup + 1]; ++row) {
128 auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin();
129 for (auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)) {
130 EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn());
131 double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation));
132 EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue());
133 ++instantiatedEntry;
134 }
135 EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(), instantiatedEntry);
136 }
137 }
138 EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling());
139 EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling());
140
141 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> modelchecker(instantiated);
142 std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
143 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
144 EXPECT_NEAR(0.01588055832, quantitativeChkResult[*instantiated.getInitialStates().begin()],
145 storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
146 }
147}
148
149TEST_F(ModelInstantiatorTest, Brp_Rew) {
150 carl::VariablePool::getInstance().clear();
151
152 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
153 std::string formulaAsString = "R=? [F ((s=5) | (s=0&srep=3)) ]";
154
155 // Program and formula
156 storm::prism::Program program = storm::api::parseProgram(programFile);
157 program.checkValidity();
158 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
159 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
160 ASSERT_TRUE(formulas.size() == 1);
161 // Parametric model
162 storm::generator::NextStateGeneratorOptions options(*formulas.front());
163 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc =
164 storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
165
166 storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
167
168 {
169 std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
170 storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
171 ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
172 storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
173 ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
174 storm::RationalFunctionVariable const& TOMsg = carl::VariablePool::getInstance().findVariableWithName("TOMsg");
175 ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
176 storm::RationalFunctionVariable const& TOAck = carl::VariablePool::getInstance().findVariableWithName("TOAck");
177 ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
178 valuation.insert(std::make_pair(pL, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.9)));
179 valuation.insert(std::make_pair(pK, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.3)));
180 valuation.insert(std::make_pair(TOMsg, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.3)));
181 valuation.insert(std::make_pair(TOAck, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.5)));
182
183 storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
184
185 ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices());
186 for (std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup) {
187 for (std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup];
188 row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup + 1]; ++row) {
189 auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin();
190 for (auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)) {
191 EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn());
192 double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation));
193 EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue());
194 ++instantiatedEntry;
195 }
196 EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(), instantiatedEntry);
197 }
198 }
199 ASSERT_TRUE(instantiated.hasUniqueRewardModel());
200 EXPECT_FALSE(instantiated.getUniqueRewardModel().hasStateRewards());
201 EXPECT_FALSE(instantiated.getUniqueRewardModel().hasTransitionRewards());
202 EXPECT_TRUE(instantiated.getUniqueRewardModel().hasStateActionRewards());
203 ASSERT_TRUE(dtmc->getUniqueRewardModel().hasStateActionRewards());
204 std::size_t stateActionEntries = dtmc->getUniqueRewardModel().getStateActionRewardVector().size();
205 ASSERT_EQ(stateActionEntries, instantiated.getUniqueRewardModel().getStateActionRewardVector().size());
206 for (std::size_t i = 0; i < stateActionEntries; ++i) {
207 double evaluatedValue = carl::toDouble(dtmc->getUniqueRewardModel().getStateActionRewardVector()[i].evaluate(valuation));
208 EXPECT_EQ(evaluatedValue, instantiated.getUniqueRewardModel().getStateActionRewardVector()[i]);
209 }
210 EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling());
211 EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling());
212
213 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> modelchecker(instantiated);
214 std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
215 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
216 EXPECT_NEAR(1.308324495, quantitativeChkResult[*instantiated.getInitialStates().begin()],
217 storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
218 }
219}
220
221TEST_F(ModelInstantiatorTest, Consensus) {
222 carl::VariablePool::getInstance().clear();
223
224 std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/coin2_2.nm";
225 std::string formulaAsString = "Pmin=? [F \"finished\"&\"all_coins_equal_1\" ]";
226
227 // Program and formula
228 storm::prism::Program program = storm::api::parseProgram(programFile);
229 program.checkValidity();
230 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
231 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
232 ASSERT_TRUE(formulas.size() == 1);
233 // Parametric model
234 storm::generator::NextStateGeneratorOptions options(*formulas.front());
235 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> mdp =
236 storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build()->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
237
238 storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>> modelInstantiator(*mdp);
239
240 std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> valuation;
241 storm::RationalFunctionVariable const& p1 = carl::VariablePool::getInstance().findVariableWithName("p1");
242 ASSERT_NE(p1, carl::Variable::NO_VARIABLE);
243 storm::RationalFunctionVariable const& p2 = carl::VariablePool::getInstance().findVariableWithName("p2");
244 ASSERT_NE(p2, carl::Variable::NO_VARIABLE);
245 valuation.insert(std::make_pair(p1, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.51)));
246 valuation.insert(std::make_pair(p2, storm::utility::convertNumber<storm::RationalFunctionCoefficient>(0.49)));
247 storm::models::sparse::Mdp<double> const& instantiated(modelInstantiator.instantiate(valuation));
248
249 ASSERT_EQ(mdp->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices());
250 for (std::size_t rowGroup = 0; rowGroup < mdp->getTransitionMatrix().getRowGroupCount(); ++rowGroup) {
251 for (std::size_t row = mdp->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < mdp->getTransitionMatrix().getRowGroupIndices()[rowGroup + 1];
252 ++row) {
253 auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin();
254 for (auto const& paramEntry : mdp->getTransitionMatrix().getRow(row)) {
255 EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn());
256 double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation));
257 EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue());
258 ++instantiatedEntry;
259 }
260 EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(), instantiatedEntry);
261 }
262 }
263 EXPECT_EQ(mdp->getStateLabeling(), instantiated.getStateLabeling());
264 EXPECT_EQ(mdp->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling());
265
266 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> modelchecker(instantiated);
267 std::unique_ptr<storm::modelchecker::CheckResult> chkResult = modelchecker.check(*formulas[0]);
268 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult<double>();
269 EXPECT_NEAR(0.3526577219, quantitativeChkResult[*instantiated.getInitialStates().begin()],
270 storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
271}
TEST_F
TEST_F(ModelInstantiatorTest, BrpProb)
Definition ModelInstantiatorTest.cpp:24
storm::builder::ExplicitModelBuilder::build
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > build()
Convert the program given at construction time to an abstract model.
Definition ExplicitModelBuilder.cpp:77
storm::modelchecker::AbstractModelChecker::check
virtual std::unique_ptr< CheckResult > check(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
Checks the provided formula.
Definition AbstractModelChecker.cpp:49
storm::modelchecker::CheckResult::asExplicitQuantitativeCheckResult
ExplicitQuantitativeCheckResult< ValueType > & asExplicitQuantitativeCheckResult()
Definition CheckResult.cpp:89
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:13
storm::models::sparse::Model::getUniqueRewardModel
RewardModelType const & getUniqueRewardModel() const
Retrieves the unique reward model, if there exists exactly one.
Definition Model.cpp:305
storm::models::sparse::Model::getTransitionMatrix
storm::storage::SparseMatrix< ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
Definition Model.cpp:199
storm::models::sparse::Model::getStateLabeling
storm::models::sparse::StateLabeling const & getStateLabeling() const
Returns the state labeling associated with this model.
Definition Model.cpp:321
storm::models::sparse::Model::getOptionalChoiceLabeling
std::optional< storm::models::sparse::ChoiceLabeling > const & getOptionalChoiceLabeling() const
Retrieves an optional value that contains the choice labeling if there is one.
Definition Model.cpp:341
storm::models::sparse::Model::hasUniqueRewardModel
virtual bool hasUniqueRewardModel() const override
Retrieves whether the model has a unique reward model.
Definition Model.cpp:289
storm::models::sparse::Model::getInitialStates
storm::storage::BitVector const & getInitialStates() const
Retrieves the initial states of the model.
Definition Model.cpp:179
storm::prism::Program::checkValidity
void checkValidity(Program::ValidityCheckLevel lvl=Program::ValidityCheckLevel::READYFORPROCESSING) const
Checks the validity of the program.
Definition Program.cpp:1239
storm::storage::BitVector::begin
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
Definition BitVector.cpp:739
storm::utility::ModelInstantiator
This class allows efficient instantiation of the given parametric model.
Definition ModelInstantiator.h:26
storm::api::parsePropertiesForPrismProgram
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:69
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::RationalFunctionVariable
carl::Variable RationalFunctionVariable
Definition RationalFunctionForward.h:26
storm_gtest.h