Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NonMarkovianChainTransformerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-parsers/api/storm-parsers.h"
5#include "storm-parsers/parser/PrismParser.h"
6#include "storm/api/storm.h"
7#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
8#include "storm/storage/jani/Property.h"
9
10TEST(NonMarkovianChainTransformerTest, StreamExampleTest) {
11#ifndef STORM_HAVE_Z3
12 GTEST_SKIP() << "Z3 not available.";
13#endif
14
15 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma");
16 std::string formulasString = "Pmin=? [ F \"done\"];Pmin=? [ F<=1 \"done\"];Tmin=? [ F \"done\" ]";
17 auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
18 auto model = storm::api::buildSparseModel<double>(program, formulas)->template as<storm::models::sparse::MarkovAutomaton<double>>();
19
20 EXPECT_EQ(12ul, model->getNumberOfStates());
21 EXPECT_EQ(14ul, model->getNumberOfTransitions());
22 ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
23 size_t initState = 0;
24
25 auto labeling = model->getStateLabeling();
26 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
27 ASSERT_TRUE(labeling.getStateHasLabel("done", 10));
28
29 auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[0], true));
30 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
31 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[1], true));
32 EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
33 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[2], true));
34 EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
35
36 // Keep labels
37 auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels);
38 ASSERT_EQ(9ul, transformed.first->getNumberOfStates());
39 ASSERT_EQ(11ul, transformed.first->getNumberOfTransitions());
40 labeling = transformed.first->getStateLabeling();
41 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
42 ASSERT_TRUE(labeling.getStateHasLabel("done", 8));
43 EXPECT_EQ(2ul, transformed.second.size());
44
45 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
46 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
47 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
48 EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
49 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
50 // EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
51
52 // Merge labels
53 transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels);
54 ASSERT_EQ(8ul, transformed.first->getNumberOfStates());
55 ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions());
56 labeling = transformed.first->getStateLabeling();
57 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
58 ASSERT_TRUE(labeling.getStateHasLabel("done", 7));
59 EXPECT_EQ(2ul, transformed.second.size());
60
61 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
62 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
63 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
64 EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
65 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
66 // EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
67
68 // Delete labels
69 transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels);
70 ASSERT_EQ(8ul, transformed.first->getNumberOfStates());
71 ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions());
72 labeling = transformed.first->getStateLabeling();
73 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
74 ASSERT_TRUE(labeling.getStateHasLabel("done", 7));
75 EXPECT_EQ(2ul, transformed.second.size());
76
77 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
78 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
79 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
80 EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
81 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
82 // EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
83}
84
85TEST(NonMarkovianChainTransformerTest, ChainElimination1ExampleTest) {
86 auto model = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ma/chain_elimination1.drn")
87 ->template as<storm::models::sparse::MarkovAutomaton<double>>();
88 std::string formulasString = "Pmin=? [ F \"Fail\"];Pmin=? [ F<=300 \"Fail\"];Tmin=? [ F \"Fail\" ]";
89 auto formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulasString));
90
91 EXPECT_EQ(43ul, model->getNumberOfStates());
92 EXPECT_EQ(59ul, model->getNumberOfTransitions());
93 ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
94 size_t initState = 0;
95
96 auto labeling = model->getStateLabeling();
97 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
98 for (size_t i = 10; i < 43; ++i) {
99 ASSERT_TRUE(labeling.getStateHasLabel("Fail", i));
100 }
101
102 auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[0], true));
103 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
104 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[1], true));
105 EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
106 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[2], true));
107 EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
108
109 // Keep labels
110 auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels);
111 ASSERT_EQ(13ul, transformed.first->getNumberOfStates());
112 ASSERT_EQ(29ul, transformed.first->getNumberOfTransitions());
113 labeling = transformed.first->getStateLabeling();
114 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
115 for (size_t i = 5; i < 13; ++i) {
116 ASSERT_TRUE(labeling.getStateHasLabel("Fail", i));
117 }
118 EXPECT_EQ(2ul, transformed.second.size());
119
120 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
121 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
122 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
123 EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
124 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
125 // EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
126
127 // Merge labels
128 transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels);
129 ASSERT_EQ(8ul, transformed.first->getNumberOfStates());
130 ASSERT_EQ(24ul, transformed.first->getNumberOfTransitions());
131 labeling = transformed.first->getStateLabeling();
132 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
133 for (size_t i = 0; i < 8; ++i) {
134 ASSERT_TRUE(labeling.getStateHasLabel("Fail", i));
135 }
136 EXPECT_EQ(2ul, transformed.second.size());
137
138 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
139 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
140 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
141 EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
142 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
143 // EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
144
145 // Delete labels
146 transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels);
147 ASSERT_EQ(8ul, transformed.first->getNumberOfStates());
148 ASSERT_EQ(24ul, transformed.first->getNumberOfTransitions());
149 labeling = transformed.first->getStateLabeling();
150 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
151 ASSERT_FALSE(labeling.getStateHasLabel("Fail", 0));
152 for (size_t i = 1; i < 8; ++i) {
153 ASSERT_TRUE(labeling.getStateHasLabel("Fail", i));
154 }
155 EXPECT_EQ(2ul, transformed.second.size());
156
157 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
158 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
159 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
160 EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
161 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
162 // EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
163}
164
165TEST(NonMarkovianChainTransformerTest, ChainElimination2ExampleTest) {
166 auto model = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ma/chain_elimination2.drn")
167 ->template as<storm::models::sparse::MarkovAutomaton<double>>();
168 std::string formulasString = "Pmin=? [ F \"Fail\"];Pmin=? [ F<=300 \"Fail\"];Tmin=? [ F \"Fail\" ]";
169 auto formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulasString));
170
171 EXPECT_EQ(10ul, model->getNumberOfStates());
172 EXPECT_EQ(14ul, model->getNumberOfTransitions());
173 ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
174 size_t initState = 0;
175
176 auto labeling = model->getStateLabeling();
177 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
178 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4));
179 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 7));
180 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 8));
181 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 9));
182
183 auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[0], true));
184 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
185 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[1], true));
186 EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
187 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[2], true));
188 EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
189
190 // Keep labels
191 auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels);
192 ASSERT_EQ(7ul, transformed.first->getNumberOfStates());
193 ASSERT_EQ(11ul, transformed.first->getNumberOfTransitions());
194 labeling = transformed.first->getStateLabeling();
195 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
196 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 2));
197 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 5));
198 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 6));
199 EXPECT_EQ(2ul, transformed.second.size());
200
201 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
202 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
203 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
204 EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
205 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
206 // EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
207
208 // Merge labels
209 transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels);
210 ASSERT_EQ(5ul, transformed.first->getNumberOfStates());
211 ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions());
212 labeling = transformed.first->getStateLabeling();
213 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
214 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 1));
215 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 2));
216 ASSERT_FALSE(labeling.getStateHasLabel("Fail", 3));
217 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4));
218 EXPECT_EQ(2ul, transformed.second.size());
219
220 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
221 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
222 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
223 EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
224 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
225 // EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
226
227 // Delete labels
228 transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels);
229 ASSERT_EQ(5ul, transformed.first->getNumberOfStates());
230 ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions());
231 labeling = transformed.first->getStateLabeling();
232 ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
233 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 1));
234 ASSERT_FALSE(labeling.getStateHasLabel("Fail", 2));
235 ASSERT_FALSE(labeling.getStateHasLabel("Fail", 3));
236 ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4));
237 EXPECT_EQ(2ul, transformed.second.size());
238
239 result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
240 EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
241 result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
242 EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
243 // result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
244 // EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
245}
TEST
TEST(NonMarkovianChainTransformerTest, StreamExampleTest)
Definition NonMarkovianChainTransformerTest.cpp:10
storm::parser::DirectEncodingParser::parseModel
static std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > parseModel(std::string const &fil, DirectEncodingParserOptions const &options=DirectEncodingParserOptions())
Load a model in DRN format from a file and create the model.
Definition DirectEncodingParser.cpp:34
storm::parser::PrismParser::parse
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.
Definition PrismParser.cpp:5
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::eliminateNonMarkovianChains
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > > eliminateNonMarkovianChains(std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &ma, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, storm::transformer::EliminationLabelBehavior labelBehavior)
Eliminates chains of non-Markovian states from a given Markov Automaton.
Definition transformation.h:21
storm::api::parseProperties
std::vector< storm::jani::Property > parseProperties(storm::parser::FormulaParser &formulaParser, std::string const &inputString, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:27
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::api::verifyWithSparseEngine
std::unique_ptr< storm::modelchecker::CheckResult > verifyWithSparseEngine(storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
Definition verification.h:93
storm_gtest.h