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