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