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